Hi again,
Spoiler, I tried to do the proof, you can check the attachment if, but
only if, you need some inspiration ;-)
(I also wanted to be extra sure that my formalization was correct!)
BR,
_
Thierry
PS. Re-reading your original mail, I see you were looking for the base
of ( Z/nZ ), the relevant theorem is ~znbas, which shows that the base
you need is the quotient set.
On 09/06/2021 23:07, Thierry Arnoux wrote:
Hi Kunhao,
As stated by `zncrng`, ( Z/nZ `5 ) is already the ring itself, so you
can work within the ring Y = ( Z/nZ `5 ), and with its multiplicative
inverse operation I = ( invr ` Y ).
The elements of that ring are not exactly the integers, they are
equivalence classes, so your final statement will rather look like
( I ` [ 3 ] R ) = [ 2 ] R
Where R is the underlying equivalence relation.
I hope this puts you on the track!
BR,
_
Thierry
On 09/06/2021 18:53, Kunhao Zheng wrote:
Hello all,
Currently, I am stuck on formalization some exercise of number
theory involving the multiplication inverse in Z/nZ. Like, compute
3^{-1} in Z/5Z, which gives 2 (because 6 mod 5 = 1).
It's easy to translate them into the relation of modulo. For
example cheating like
|- ( ph -> X e. NN0 )
|- ( ph-> ( ( X x. 3 ) mod 5 ) = 1 )
|- ( ph -> ( X mod 5 ) = 2 )
However, I want to know if I can directly provide the information of
inverse, my attempt is something like
|- R = ( CCfld |` ( Z/nZ ` 5 ) )
|- I = ( invr ` R )
|- ( ph -> ( I ` 3 ) = 2 )
Since the best way to test if a formalization is correct or not is
trying to prove it, I tried but I failed, and I struggle a lot in
providing extra def like "B = ( Base ` R )". Do you have any
suggestion on the formalization? Thank you a lot!
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it,
send an email to [email protected]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/5e9d1415-8e81-493d-9a93-5d04edb4a1d9n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/5e9d1415-8e81-493d-9a93-5d04edb4a1d9n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send
an email to [email protected]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/2a25c673-3780-b43c-8ad2-15ccd04322dc%40gmx.net
<https://groups.google.com/d/msgid/metamath/2a25c673-3780-b43c-8ad2-15ccd04322dc%40gmx.net?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/c766c4d3-046f-593f-8cc2-b3ee85818728%40gmx.net.
$( <MM> <PROOF_ASST> THEOREM=z5_zkh LOC_AFTER=?
h1::z5_zkh.1 |- Y = ( Z/nZ ` 5 )
h2::z5_zkh.2 |- I = ( invr ` Y )
h3::z5_zkh.3 |- R = ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) )
d1::eqid |- ( Base ` Y ) = ( Base ` Y )
d11::eqid |- ( RSpan ` ZZring ) = ( RSpan ` ZZring )
d2::eqid |- ( .r ` Y ) = ( .r ` Y )
d3::eqid |- ( 1r ` Y ) = ( 1r ` Y )
d4::eqid |- ( Unit ` Y ) = ( Unit ` Y )
d28::eqid |- ( ZRHom ` Y ) = ( ZRHom ` Y )
d34::eqid |- ( LIdeal ` ZZring ) = ( LIdeal ` ZZring )
4::2z |- 2 e. ZZ
5::3z |- 3 e. ZZ
7::5nn0 |- 5 e. NN0
7a::1z |- 1 e. ZZ
7b::6nn |- 6 e. NN
7c:7b:nnzi |- 6 e. ZZ
7d:7:nn0zi |- 5 e. ZZ
8:1:zncrng |- ( 5 e. NN0 -> Y e. CRing )
9::crngring |- ( Y e. CRing -> Y e. Ring )
10:7,8,9:mp2b |- Y e. Ring
d6:10:a1i |- ( T. -> Y e. Ring )
**
11:d11,1,3:znbas |- ( 5 e. NN0 -> ( ZZ /. R ) = ( Base ` Y ) )
20:7,11:ax-mp |- ( ZZ /. R ) = ( Base ` Y )
21::ovex |- ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) e. _V
d12:3,21:eqeltri |- R e. _V
30:d12:ecelqsi |- ( 2 e. ZZ -> [ 2 ] R e. ( ZZ /. R ) )
40:d12:ecelqsi |- ( 3 e. ZZ -> [ 3 ] R e. ( ZZ /. R ) )
35:4,30:ax-mp |- [ 2 ] R e. ( ZZ /. R )
45:5,40:ax-mp |- [ 3 ] R e. ( ZZ /. R )
37:35,20:eleqtri |- [ 2 ] R e. ( Base ` Y )
47:45,20:eleqtri |- [ 3 ] R e. ( Base ` Y )
d7:47:a1i |- ( T. -> [ 3 ] R e. ( Base ` Y ) )
d8:37:a1i |- ( T. -> [ 2 ] R e. ( Base ` Y ) )
*
50:7,8:ax-mp |- Y e. CRing
d16::eqid |- ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) )
) = ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) )
60:d11,d16,1:znmul |- ( 5 e. NN0 -> ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan `
ZZring ) ` { 5 } ) ) ) ) = ( .r ` Y ) )
61:7,60:ax-mp |- ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` {
5 } ) ) ) ) = ( .r ` Y )
62:61:oveqi |- ( [ 3 ] R ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan `
ZZring ) ` { 5 } ) ) ) ) [ 2 ] R ) = ( [ 3 ] R ( .r ` Y ) [ 2 ] R )
d32:3:a1i |- ( T. -> R = ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) )
)
d25:d32:eqcomd |- ( T. -> ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) = R
)
d17:d25:oveq2d |- ( T. -> ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` {
5 } ) ) ) = ( ZZring /s R ) )
d26::zringbas |- ZZ = ( Base ` ZZring )
149::zringring |- ZZring e. Ring
d18:d26:a1i |- ( T. -> ZZ = ( Base ` ZZring ) )
29:d26,3:eqger |- ( ( ( RSpan ` ZZring ) ` { 5 } ) e. ( SubGrp ` ZZring )
-> R Er ZZ )
150:d11:znlidl |- ( 5 e. ZZ -> ( ( RSpan ` ZZring ) ` { 5 } ) e. ( LIdeal `
ZZring ) )
151:7d,150:ax-mp |- ( ( RSpan ` ZZring ) ` { 5 } ) e. ( LIdeal ` ZZring )
152:d34:lidlsubg |- ( ( ZZring e. Ring /\ ( ( RSpan ` ZZring ) ` { 5 } ) e. (
LIdeal ` ZZring ) ) -> ( ( RSpan ` ZZring ) ` { 5 } ) e. ( SubGrp ` ZZring ) )
298:149,151,152:mp2an |- ( ( RSpan ` ZZring ) ` { 5 } ) e. ( SubGrp ` ZZring )
299:298,29:ax-mp |- R Er ZZ
d19:299:a1i |- ( T. -> R Er ZZ )
d20:149:a1i |- ( T. -> ZZring e. Ring )
d24::eqid |- ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` {
5 } ) ) ) ) = ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) )
) )
590:d28:zrhrhm |- ( Y e. Ring -> ( ZRHom ` Y ) e. ( ZZring RingHom Y ) )
595:10,590:ax-mp |- ( ZRHom ` Y ) e. ( ZZring RingHom Y )
d35::zringmulr |- x. = ( .r ` ZZring )
600:d26,d35,d2:rhmmul |- ( ( ( ZRHom ` Y ) e. ( ZZring RingHom Y ) /\ 3 e. ZZ
/\ 2 e. ZZ ) -> ( ( ZRHom ` Y ) ` ( 3 x. 2 ) ) = ( ( ( ZRHom ` Y ) ` 3 ) ( .r `
Y ) ( ( ZRHom ` Y ) ` 2 ) ) )
601:595,5,4,600:mp3an |- ( ( ZRHom ` Y ) ` ( 3 x. 2 ) ) = ( ( ( ZRHom ` Y ) ` 3
) ( .r ` Y ) ( ( ZRHom ` Y ) ` 2 ) )
66::tru |- T.
72::3t2e6 |- ( 3 x. 2 ) = 6
73::fveq2 |- ( ( 3 x. 2 ) = 6 -> ( ( ZRHom ` Y ) ` ( 3 x. 2 ) ) = ( (
ZRHom ` Y ) ` 6 ) )
75:72,73:ax-mp |- ( ( ZRHom ` Y ) ` ( 3 x. 2 ) ) = ( ( ZRHom ` Y ) ` 6 )
80:1,d28:zndvds |- ( ( 5 e. NN0 /\ 6 e. ZZ /\ 1 e. ZZ ) -> ( ( ( ZRHom ` Y )
` 6 ) = ( ( ZRHom ` Y ) ` 1 ) <-> 5 || ( 6 - 1 ) ) )
81:7,7c,7a,80:mp3an |- ( ( ( ZRHom ` Y ) ` 6 ) = ( ( ZRHom ` Y ) ` 1 ) <-> 5 ||
( 6 - 1 ) )
300::iddvds |- ( 5 e. ZZ -> 5 || 5 )
310:7d,300:ax-mp |- 5 || 5
d29::5cn |- 5 e. CC
d30::ax1cn |- 1 e. CC
d31::5p1e6 |- ( 5 + 1 ) = 6
311:d29,d30,d31:mvlraddi
|- 5 = ( 6 - 1 )
320:311:eqcomi |- ( 6 - 1 ) = 5
330:320:breq2i |- ( 5 || ( 6 - 1 ) <-> 5 || 5 )
335:310,330:mpbir |- 5 || ( 6 - 1 )
340:335,81:mpbir |- ( ( ZRHom ` Y ) ` 6 ) = ( ( ZRHom ` Y ) ` 1 )
350:d11,3,1,d28:znzrhval |- ( ( 5 e. NN0 /\ 6 e. ZZ ) -> ( ( ZRHom ` Y ) ` 6 )
= [ 6 ] R )
390:d11,3,1,d28:znzrhval |- ( ( 5 e. NN0 /\ 3 e. ZZ ) -> ( ( ZRHom ` Y ) ` 3 )
= [ 3 ] R )
380:d11,3,1,d28:znzrhval |- ( ( 5 e. NN0 /\ 2 e. ZZ ) -> ( ( ZRHom ` Y ) ` 2 )
= [ 2 ] R )
200:d11,3,1,d28:znzrhval |- ( ( 5 e. NN0 /\ 1 e. ZZ ) -> ( ( ZRHom ` Y ) ` 1 )
= [ 1 ] R )
360:7,7c,350:mp2an |- ( ( ZRHom ` Y ) ` 6 ) = [ 6 ] R
361:7,5,390:mp2an |- ( ( ZRHom ` Y ) ` 3 ) = [ 3 ] R
36:7,4,380:mp2an |- ( ( ZRHom ` Y ) ` 2 ) = [ 2 ] R
370:7,7a,200:mp2an |- ( ( ZRHom ` Y ) ` 1 ) = [ 1 ] R
82:340,360,370:3eqtr3i |- [ 6 ] R = [ 1 ] R
201:7,7a,200:mp2an |- ( ( ZRHom ` Y ) ` 1 ) = [ 1 ] R
210:d28,d3:zrh1 |- ( Y e. Ring -> ( ( ZRHom ` Y ) ` 1 ) = ( 1r ` Y ) )
215:10,210:ax-mp |- ( ( ZRHom ` Y ) ` 1 ) = ( 1r ` Y )
220:215,201:eqtr3i |- ( 1r ` Y ) = [ 1 ] R
400:361,36:oveq12i |- ( ( ( ZRHom ` Y ) ` 3 ) ( .r ` Y ) ( ( ZRHom ` Y ) ` 2 )
) = ( [ 3 ] R ( .r ` Y ) [ 2 ] R )
401:75,601,340:3eqtr3i |- ( ( ( ZRHom ` Y ) ` 3 ) ( .r ` Y ) ( ( ZRHom ` Y ) `
2 ) ) = ( ( ZRHom ` Y ) ` 1 )
d13:401,400,215:3eqtr3i |- ( [ 3 ] R ( .r ` Y ) [ 2 ] R ) = ( 1r ` Y )
*
90:d1,d2:crngcom |- ( ( Y e. CRing /\ [ 3 ] R e. ( Base ` Y ) /\ [ 2 ] R e. (
Base ` Y ) ) -> ( [ 3 ] R ( .r ` Y ) [ 2 ] R ) = ( [ 2 ] R ( .r ` Y ) [ 3 ] R )
)
95:50,47,37,90:mp3an |- ( [ 3 ] R ( .r ` Y ) [ 2 ] R ) = ( [ 2 ] R ( .r ` Y ) [
3 ] R )
d14:95,d13:eqtr3i |- ( [ 2 ] R ( .r ` Y ) [ 3 ] R ) = ( 1r ` Y )
d9:d13:a1i |- ( T. -> ( [ 3 ] R ( .r ` Y ) [ 2 ] R ) = ( 1r ` Y ) )
d10:d14:a1i |- ( T. -> ( [ 2 ] R ( .r ` Y ) [ 3 ] R ) = ( 1r ` Y ) )
100:d1,d2,d3,d4,2,d6,d7,d8,d9,d10:invrvald
|- ( T. -> ( [ 3 ] R e. ( Unit ` Y ) /\ ( I ` [ 3 ] R ) = [
2 ] R ) )
110:100:trud |- ( [ 3 ] R e. ( Unit ` Y ) /\ ( I ` [ 3 ] R ) = [ 2 ] R )
qed:110:simpri |- ( I ` [ 3 ] R ) = [ 2 ] R
$= ( z5_zkh.1 c3 cfv wcel c2 wceq wtru eqid c5 5nn0 a1i cz zring co ax-mp c1
c6 z5_zkh.2 z5_zkh.3 cec cui wa cbs cmulr cur crg ccrg zncrng crngring mp2b
cn0 cqs 3z csn crsp cqg cvv ovex eqeltri ecelqsi znbas eleqtri 2z czrh cmul
3t2e6 fveq2 crh zrhrhm zringbas zringmulr rhmmul mp3an cmin cdvds wbr nn0zi
iddvds 5cn ax1cn 5p1e6 mvlraddi eqcomi breq2i mpbir 6nn nnzi zndvds 3eqtr3i
wb 1z znzrhval mp2an oveq12i zrh1 crngcom eqtr3i invrvald trud simpri ) EAU
CZCUDFZGZXDBFHAUCZIZXFXHUEJCUFFZCCUGFZXECUHFZBXDXGXIKZXJKZXKKZXEKUACUIGZJLU
NGZCUJGZXOMLCDUKZCULUMZNXDXIGZJXDOAUOZXIEOGZXDYAGUPOEAAPLUQPURFZFZUSQUTUBPY
DUSVAVBZVCRXPYAXIIMAYCLCYCKZDUBVDRZVEZNXGXIGZJXGYAXIHOGZXGYAGVFOHAYEVCRYGVE
ZNXDXGXJQZXKIJECVGFZFZHYMFZXJQZSYMFZYLXKEHVHQZYMFZTYMFZYPYQYRTIYSYTIVIYRTYM
VJRYMPCVKQGZYBYJYSYPIXOUUAXSCYMYMKZVLRUPVFEHPCVHXJYMOVMVNXMVOVPYTYQIZLTSVQQ
ZVRVSZUUELLVRVSZLOGUUFLMVTLWARUUDLLVRLUUDLSTWBWCWDWEWFWGWHXPTOGSOGUUCUUEWMM
TWIWJWNTSYMLCDUUBWKVPWHWLYNXDYOXGXJXPYBYNXDIMUPEAYCYMLCYFUBDUUBWOWPXPYJYOXG
IMVFHAYCYMLCYFUBDUUBWOWPWQXOYQXKIXSCXKYMUUBXNWRRWLZNXGXDXJQZXKIJYLUUHXKXQXT
YIYLUUHIXPXQMXRRYHYKXICXJXDXGXLXMWSVPUUGWTNXAXBXC $.
$)
