MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvdsmulf1o Structured version   Visualization version   GIF version

Theorem dvdsmulf1o 26392
Description: If 𝑀 and 𝑁 are two coprime integers, multiplication forms a bijection from the set of pairs βŸ¨π‘—, π‘˜βŸ© where 𝑗 βˆ₯ 𝑀 and π‘˜ βˆ₯ 𝑁, to the set of divisors of 𝑀 Β· 𝑁. (Contributed by Mario Carneiro, 2-Jul-2015.)
Hypotheses
Ref Expression
dvdsmulf1o.1 (πœ‘ β†’ 𝑀 ∈ β„•)
dvdsmulf1o.2 (πœ‘ β†’ 𝑁 ∈ β„•)
dvdsmulf1o.3 (πœ‘ β†’ (𝑀 gcd 𝑁) = 1)
dvdsmulf1o.x 𝑋 = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑀}
dvdsmulf1o.y π‘Œ = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑁}
dvdsmulf1o.z 𝑍 = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ (𝑀 Β· 𝑁)}
Assertion
Ref Expression
dvdsmulf1o (πœ‘ β†’ ( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1-onto→𝑍)
Distinct variable groups:   π‘₯,𝑀   π‘₯,𝑁
Allowed substitution hints:   πœ‘(π‘₯)   𝑋(π‘₯)   π‘Œ(π‘₯)   𝑍(π‘₯)

Proof of Theorem dvdsmulf1o
Dummy variables 𝑖 𝑒 𝑗 π‘š 𝑛 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-mulf 11001 . . . . . . 7 Β· :(β„‚ Γ— β„‚)βŸΆβ„‚
2 ffn 6630 . . . . . . 7 ( Β· :(β„‚ Γ— β„‚)βŸΆβ„‚ β†’ Β· Fn (β„‚ Γ— β„‚))
31, 2ax-mp 5 . . . . . 6 Β· Fn (β„‚ Γ— β„‚)
4 dvdsmulf1o.x . . . . . . . . 9 𝑋 = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑀}
54ssrab3 4021 . . . . . . . 8 𝑋 βŠ† β„•
6 nnsscn 12028 . . . . . . . 8 β„• βŠ† β„‚
75, 6sstri 3935 . . . . . . 7 𝑋 βŠ† β„‚
8 dvdsmulf1o.y . . . . . . . . 9 π‘Œ = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑁}
98ssrab3 4021 . . . . . . . 8 π‘Œ βŠ† β„•
109, 6sstri 3935 . . . . . . 7 π‘Œ βŠ† β„‚
11 xpss12 5615 . . . . . . 7 ((𝑋 βŠ† β„‚ ∧ π‘Œ βŠ† β„‚) β†’ (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚))
127, 10, 11mp2an 690 . . . . . 6 (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚)
13 fnssres 6586 . . . . . 6 (( Β· Fn (β„‚ Γ— β„‚) ∧ (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚)) β†’ ( Β· β†Ύ (𝑋 Γ— π‘Œ)) Fn (𝑋 Γ— π‘Œ))
143, 12, 13mp2an 690 . . . . 5 ( Β· β†Ύ (𝑋 Γ— π‘Œ)) Fn (𝑋 Γ— π‘Œ)
1514a1i 11 . . . 4 (πœ‘ β†’ ( Β· β†Ύ (𝑋 Γ— π‘Œ)) Fn (𝑋 Γ— π‘Œ))
16 ovres 7470 . . . . . . 7 ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ) β†’ (𝑖( Β· β†Ύ (𝑋 Γ— π‘Œ))𝑗) = (𝑖 Β· 𝑗))
1716adantl 483 . . . . . 6 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖( Β· β†Ύ (𝑋 Γ— π‘Œ))𝑗) = (𝑖 Β· 𝑗))
18 breq1 5084 . . . . . . . . . . 11 (π‘₯ = 𝑖 β†’ (π‘₯ βˆ₯ 𝑀 ↔ 𝑖 βˆ₯ 𝑀))
1918, 4elrab2 3632 . . . . . . . . . 10 (𝑖 ∈ 𝑋 ↔ (𝑖 ∈ β„• ∧ 𝑖 βˆ₯ 𝑀))
2019simplbi 499 . . . . . . . . 9 (𝑖 ∈ 𝑋 β†’ 𝑖 ∈ β„•)
2120ad2antrl 726 . . . . . . . 8 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑖 ∈ β„•)
22 breq1 5084 . . . . . . . . . . 11 (π‘₯ = 𝑗 β†’ (π‘₯ βˆ₯ 𝑁 ↔ 𝑗 βˆ₯ 𝑁))
2322, 8elrab2 3632 . . . . . . . . . 10 (𝑗 ∈ π‘Œ ↔ (𝑗 ∈ β„• ∧ 𝑗 βˆ₯ 𝑁))
2423simplbi 499 . . . . . . . . 9 (𝑗 ∈ π‘Œ β†’ 𝑗 ∈ β„•)
2524ad2antll 727 . . . . . . . 8 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑗 ∈ β„•)
2621, 25nnmulcld 12076 . . . . . . 7 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) ∈ β„•)
2723simprbi 498 . . . . . . . . 9 (𝑗 ∈ π‘Œ β†’ 𝑗 βˆ₯ 𝑁)
2827ad2antll 727 . . . . . . . 8 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑗 βˆ₯ 𝑁)
2919simprbi 498 . . . . . . . . 9 (𝑖 ∈ 𝑋 β†’ 𝑖 βˆ₯ 𝑀)
3029ad2antrl 726 . . . . . . . 8 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑖 βˆ₯ 𝑀)
3125nnzd 12475 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑗 ∈ β„€)
32 dvdsmulf1o.2 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑁 ∈ β„•)
3332adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑁 ∈ β„•)
3433nnzd 12475 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑁 ∈ β„€)
3521nnzd 12475 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑖 ∈ β„€)
36 dvdscmul 16041 . . . . . . . . . 10 ((𝑗 ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ 𝑖 ∈ β„€) β†’ (𝑗 βˆ₯ 𝑁 β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑖 Β· 𝑁)))
3731, 34, 35, 36syl3anc 1371 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑗 βˆ₯ 𝑁 β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑖 Β· 𝑁)))
38 dvdsmulf1o.1 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑀 ∈ β„•)
3938adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑀 ∈ β„•)
4039nnzd 12475 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑀 ∈ β„€)
41 dvdsmulc 16042 . . . . . . . . . 10 ((𝑖 ∈ β„€ ∧ 𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑖 βˆ₯ 𝑀 β†’ (𝑖 Β· 𝑁) βˆ₯ (𝑀 Β· 𝑁)))
4235, 40, 34, 41syl3anc 1371 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 βˆ₯ 𝑀 β†’ (𝑖 Β· 𝑁) βˆ₯ (𝑀 Β· 𝑁)))
4326nnzd 12475 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) ∈ β„€)
4435, 34zmulcld 12482 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑁) ∈ β„€)
4540, 34zmulcld 12482 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑀 Β· 𝑁) ∈ β„€)
46 dvdstr 16052 . . . . . . . . . 10 (((𝑖 Β· 𝑗) ∈ β„€ ∧ (𝑖 Β· 𝑁) ∈ β„€ ∧ (𝑀 Β· 𝑁) ∈ β„€) β†’ (((𝑖 Β· 𝑗) βˆ₯ (𝑖 Β· 𝑁) ∧ (𝑖 Β· 𝑁) βˆ₯ (𝑀 Β· 𝑁)) β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
4743, 44, 45, 46syl3anc 1371 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (((𝑖 Β· 𝑗) βˆ₯ (𝑖 Β· 𝑁) ∧ (𝑖 Β· 𝑁) βˆ₯ (𝑀 Β· 𝑁)) β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
4837, 42, 47syl2and 609 . . . . . . . 8 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ ((𝑗 βˆ₯ 𝑁 ∧ 𝑖 βˆ₯ 𝑀) β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
4928, 30, 48mp2and 697 . . . . . . 7 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁))
50 breq1 5084 . . . . . . . 8 (π‘₯ = (𝑖 Β· 𝑗) β†’ (π‘₯ βˆ₯ (𝑀 Β· 𝑁) ↔ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
51 dvdsmulf1o.z . . . . . . . 8 𝑍 = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ (𝑀 Β· 𝑁)}
5250, 51elrab2 3632 . . . . . . 7 ((𝑖 Β· 𝑗) ∈ 𝑍 ↔ ((𝑖 Β· 𝑗) ∈ β„• ∧ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
5326, 49, 52sylanbrc 584 . . . . . 6 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) ∈ 𝑍)
5417, 53eqeltrd 2837 . . . . 5 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖( Β· β†Ύ (𝑋 Γ— π‘Œ))𝑗) ∈ 𝑍)
5554ralrimivva 3194 . . . 4 (πœ‘ β†’ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ (𝑖( Β· β†Ύ (𝑋 Γ— π‘Œ))𝑗) ∈ 𝑍)
56 ffnov 7433 . . . 4 (( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)βŸΆπ‘ ↔ (( Β· β†Ύ (𝑋 Γ— π‘Œ)) Fn (𝑋 Γ— π‘Œ) ∧ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ (𝑖( Β· β†Ύ (𝑋 Γ— π‘Œ))𝑗) ∈ 𝑍))
5715, 55, 56sylanbrc 584 . . 3 (πœ‘ β†’ ( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)βŸΆπ‘)
5821adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 ∈ β„•)
5958nnnn0d 12343 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 ∈ β„•0)
60 simprll 777 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ 𝑋)
61 breq1 5084 . . . . . . . . . . . . 13 (π‘₯ = π‘š β†’ (π‘₯ βˆ₯ 𝑀 ↔ π‘š βˆ₯ 𝑀))
6261, 4elrab2 3632 . . . . . . . . . . . 12 (π‘š ∈ 𝑋 ↔ (π‘š ∈ β„• ∧ π‘š βˆ₯ 𝑀))
6362simplbi 499 . . . . . . . . . . 11 (π‘š ∈ 𝑋 β†’ π‘š ∈ β„•)
6460, 63syl 17 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ β„•)
6564nnnn0d 12343 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ β„•0)
6658nnzd 12475 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 ∈ β„€)
6725adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 ∈ β„•)
6867nnzd 12475 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 ∈ β„€)
69 dvdsmul1 16036 . . . . . . . . . . . 12 ((𝑖 ∈ β„€ ∧ 𝑗 ∈ β„€) β†’ 𝑖 βˆ₯ (𝑖 Β· 𝑗))
7066, 68, 69syl2anc 585 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 βˆ₯ (𝑖 Β· 𝑗))
71 simprr 771 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))
727, 60sselid 3924 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ β„‚)
73 simprlr 778 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 ∈ π‘Œ)
74 breq1 5084 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑛 β†’ (π‘₯ βˆ₯ 𝑁 ↔ 𝑛 βˆ₯ 𝑁))
7574, 8elrab2 3632 . . . . . . . . . . . . . . . 16 (𝑛 ∈ π‘Œ ↔ (𝑛 ∈ β„• ∧ 𝑛 βˆ₯ 𝑁))
7675simplbi 499 . . . . . . . . . . . . . . 15 (𝑛 ∈ π‘Œ β†’ 𝑛 ∈ β„•)
7773, 76syl 17 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 ∈ β„•)
7877nncnd 12039 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 ∈ β„‚)
7972, 78mulcomd 11046 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š Β· 𝑛) = (𝑛 Β· π‘š))
8071, 79eqtrd 2776 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑗) = (𝑛 Β· π‘š))
8170, 80breqtrd 5107 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 βˆ₯ (𝑛 Β· π‘š))
8277nnzd 12475 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 ∈ β„€)
8334adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑁 ∈ β„€)
8466, 83gcdcomd 16270 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
8540adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑀 ∈ β„€)
8632nnzd 12475 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑁 ∈ β„€)
8738nnzd 12475 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑀 ∈ β„€)
8886, 87gcdcomd 16270 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
89 dvdsmulf1o.3 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑀 gcd 𝑁) = 1)
9088, 89eqtrd 2776 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑁 gcd 𝑀) = 1)
9190ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑁 gcd 𝑀) = 1)
9230adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 βˆ₯ 𝑀)
93 rpdvds 16414 . . . . . . . . . . . . 13 (((𝑁 ∈ β„€ ∧ 𝑖 ∈ β„€ ∧ 𝑀 ∈ β„€) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑖 βˆ₯ 𝑀)) β†’ (𝑁 gcd 𝑖) = 1)
9483, 66, 85, 91, 92, 93syl32anc 1378 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑁 gcd 𝑖) = 1)
9584, 94eqtrd 2776 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 gcd 𝑁) = 1)
9675simprbi 498 . . . . . . . . . . . 12 (𝑛 ∈ π‘Œ β†’ 𝑛 βˆ₯ 𝑁)
9773, 96syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 βˆ₯ 𝑁)
98 rpdvds 16414 . . . . . . . . . . 11 (((𝑖 ∈ β„€ ∧ 𝑛 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ ((𝑖 gcd 𝑁) = 1 ∧ 𝑛 βˆ₯ 𝑁)) β†’ (𝑖 gcd 𝑛) = 1)
9966, 82, 83, 95, 97, 98syl32anc 1378 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 gcd 𝑛) = 1)
10064nnzd 12475 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ β„€)
101 coprmdvds 16407 . . . . . . . . . . 11 ((𝑖 ∈ β„€ ∧ 𝑛 ∈ β„€ ∧ π‘š ∈ β„€) β†’ ((𝑖 βˆ₯ (𝑛 Β· π‘š) ∧ (𝑖 gcd 𝑛) = 1) β†’ 𝑖 βˆ₯ π‘š))
10266, 82, 100, 101syl3anc 1371 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ ((𝑖 βˆ₯ (𝑛 Β· π‘š) ∧ (𝑖 gcd 𝑛) = 1) β†’ 𝑖 βˆ₯ π‘š))
10381, 99, 102mp2and 697 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 βˆ₯ π‘š)
104 dvdsmul1 16036 . . . . . . . . . . . 12 ((π‘š ∈ β„€ ∧ 𝑛 ∈ β„€) β†’ π‘š βˆ₯ (π‘š Β· 𝑛))
105100, 82, 104syl2anc 585 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š βˆ₯ (π‘š Β· 𝑛))
10658nncnd 12039 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 ∈ β„‚)
10767nncnd 12039 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 ∈ β„‚)
108106, 107mulcomd 11046 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑗) = (𝑗 Β· 𝑖))
10971, 108eqtr3d 2778 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š Β· 𝑛) = (𝑗 Β· 𝑖))
110105, 109breqtrd 5107 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š βˆ₯ (𝑗 Β· 𝑖))
111100, 83gcdcomd 16270 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š gcd 𝑁) = (𝑁 gcd π‘š))
11262simprbi 498 . . . . . . . . . . . . . 14 (π‘š ∈ 𝑋 β†’ π‘š βˆ₯ 𝑀)
11360, 112syl 17 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š βˆ₯ 𝑀)
114 rpdvds 16414 . . . . . . . . . . . . 13 (((𝑁 ∈ β„€ ∧ π‘š ∈ β„€ ∧ 𝑀 ∈ β„€) ∧ ((𝑁 gcd 𝑀) = 1 ∧ π‘š βˆ₯ 𝑀)) β†’ (𝑁 gcd π‘š) = 1)
11583, 100, 85, 91, 113, 114syl32anc 1378 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑁 gcd π‘š) = 1)
116111, 115eqtrd 2776 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š gcd 𝑁) = 1)
11728adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 βˆ₯ 𝑁)
118 rpdvds 16414 . . . . . . . . . . 11 (((π‘š ∈ β„€ ∧ 𝑗 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ ((π‘š gcd 𝑁) = 1 ∧ 𝑗 βˆ₯ 𝑁)) β†’ (π‘š gcd 𝑗) = 1)
119100, 68, 83, 116, 117, 118syl32anc 1378 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š gcd 𝑗) = 1)
120 coprmdvds 16407 . . . . . . . . . . 11 ((π‘š ∈ β„€ ∧ 𝑗 ∈ β„€ ∧ 𝑖 ∈ β„€) β†’ ((π‘š βˆ₯ (𝑗 Β· 𝑖) ∧ (π‘š gcd 𝑗) = 1) β†’ π‘š βˆ₯ 𝑖))
121100, 68, 66, 120syl3anc 1371 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ ((π‘š βˆ₯ (𝑗 Β· 𝑖) ∧ (π‘š gcd 𝑗) = 1) β†’ π‘š βˆ₯ 𝑖))
122110, 119, 121mp2and 697 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š βˆ₯ 𝑖)
123 dvdseq 16072 . . . . . . . . 9 (((𝑖 ∈ β„•0 ∧ π‘š ∈ β„•0) ∧ (𝑖 βˆ₯ π‘š ∧ π‘š βˆ₯ 𝑖)) β†’ 𝑖 = π‘š)
12459, 65, 103, 122, 123syl22anc 837 . . . . . . . 8 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 = π‘š)
12558nnne0d 12073 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 β‰  0)
126124oveq1d 7322 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑛) = (π‘š Β· 𝑛))
12771, 126eqtr4d 2779 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑗) = (𝑖 Β· 𝑛))
128107, 78, 106, 125, 127mulcanad 11660 . . . . . . . 8 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 = 𝑛)
129124, 128opeq12d 4817 . . . . . . 7 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©)
130129expr 458 . . . . . 6 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ ((𝑖 Β· 𝑗) = (π‘š Β· 𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
131130ralrimivva 3194 . . . . 5 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖 Β· 𝑗) = (π‘š Β· 𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
132131ralrimivva 3194 . . . 4 (πœ‘ β†’ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖 Β· 𝑗) = (π‘š Β· 𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
133 fvres 6823 . . . . . . . . 9 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = ( Β· β€˜π‘’))
134 fvres 6823 . . . . . . . . 9 (𝑣 ∈ (𝑋 Γ— π‘Œ) β†’ (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) = ( Β· β€˜π‘£))
135133, 134eqeqan12d 2750 . . . . . . . 8 ((𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (𝑋 Γ— π‘Œ)) β†’ ((( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) ↔ ( Β· β€˜π‘’) = ( Β· β€˜π‘£)))
136135imbi1d 342 . . . . . . 7 ((𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (𝑋 Γ— π‘Œ)) β†’ (((( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ (( Β· β€˜π‘’) = ( Β· β€˜π‘£) β†’ 𝑒 = 𝑣)))
137136ralbidva 3169 . . . . . 6 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(( Β· β€˜π‘’) = ( Β· β€˜π‘£) β†’ 𝑒 = 𝑣)))
138137ralbiia 3091 . . . . 5 (βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(( Β· β€˜π‘’) = ( Β· β€˜π‘£) β†’ 𝑒 = 𝑣))
139 fveq2 6804 . . . . . . . . . . 11 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ ( Β· β€˜π‘£) = ( Β· β€˜βŸ¨π‘š, π‘›βŸ©))
140 df-ov 7310 . . . . . . . . . . 11 (π‘š Β· 𝑛) = ( Β· β€˜βŸ¨π‘š, π‘›βŸ©)
141139, 140eqtr4di 2794 . . . . . . . . . 10 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ ( Β· β€˜π‘£) = (π‘š Β· 𝑛))
142141eqeq2d 2747 . . . . . . . . 9 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ (( Β· β€˜π‘’) = ( Β· β€˜π‘£) ↔ ( Β· β€˜π‘’) = (π‘š Β· 𝑛)))
143 eqeq2 2748 . . . . . . . . 9 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ (𝑒 = 𝑣 ↔ 𝑒 = βŸ¨π‘š, π‘›βŸ©))
144142, 143imbi12d 345 . . . . . . . 8 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ ((( Β· β€˜π‘’) = ( Β· β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ (( Β· β€˜π‘’) = (π‘š Β· 𝑛) β†’ 𝑒 = βŸ¨π‘š, π‘›βŸ©)))
145144ralxp 5763 . . . . . . 7 (βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(( Β· β€˜π‘’) = ( Β· β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ (( Β· β€˜π‘’) = (π‘š Β· 𝑛) β†’ 𝑒 = βŸ¨π‘š, π‘›βŸ©))
146 fveq2 6804 . . . . . . . . . . 11 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ ( Β· β€˜π‘’) = ( Β· β€˜βŸ¨π‘–, π‘—βŸ©))
147 df-ov 7310 . . . . . . . . . . 11 (𝑖 Β· 𝑗) = ( Β· β€˜βŸ¨π‘–, π‘—βŸ©)
148146, 147eqtr4di 2794 . . . . . . . . . 10 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ ( Β· β€˜π‘’) = (𝑖 Β· 𝑗))
149148eqeq1d 2738 . . . . . . . . 9 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ (( Β· β€˜π‘’) = (π‘š Β· 𝑛) ↔ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛)))
150 eqeq1 2740 . . . . . . . . 9 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ (𝑒 = βŸ¨π‘š, π‘›βŸ© ↔ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
151149, 150imbi12d 345 . . . . . . . 8 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ ((( Β· β€˜π‘’) = (π‘š Β· 𝑛) β†’ 𝑒 = βŸ¨π‘š, π‘›βŸ©) ↔ ((𝑖 Β· 𝑗) = (π‘š Β· 𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©)))
1521512ralbidv 3209 . . . . . . 7 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ (βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ (( Β· β€˜π‘’) = (π‘š Β· 𝑛) β†’ 𝑒 = βŸ¨π‘š, π‘›βŸ©) ↔ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖 Β· 𝑗) = (π‘š Β· 𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©)))
153145, 152bitrid 283 . . . . . 6 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ (βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(( Β· β€˜π‘’) = ( Β· β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖 Β· 𝑗) = (π‘š Β· 𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©)))
154153ralxp 5763 . . . . 5 (βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(( Β· β€˜π‘’) = ( Β· β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖 Β· 𝑗) = (π‘š Β· 𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
155138, 154bitri 275 . . . 4 (βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖 Β· 𝑗) = (π‘š Β· 𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
156132, 155sylibr 233 . . 3 (πœ‘ β†’ βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣))
157 dff13 7160 . . 3 (( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1→𝑍 ↔ (( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)βŸΆπ‘ ∧ βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣)))
15857, 156, 157sylanbrc 584 . 2 (πœ‘ β†’ ( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1→𝑍)
159 breq1 5084 . . . . . . . . . . . 12 (π‘₯ = 𝑀 β†’ (π‘₯ βˆ₯ (𝑀 Β· 𝑁) ↔ 𝑀 βˆ₯ (𝑀 Β· 𝑁)))
160159, 51elrab2 3632 . . . . . . . . . . 11 (𝑀 ∈ 𝑍 ↔ (𝑀 ∈ β„• ∧ 𝑀 βˆ₯ (𝑀 Β· 𝑁)))
161160simplbi 499 . . . . . . . . . 10 (𝑀 ∈ 𝑍 β†’ 𝑀 ∈ β„•)
162161adantl 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 ∈ β„•)
163162nnzd 12475 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 ∈ β„€)
16438adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 ∈ β„•)
165164nnzd 12475 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 ∈ β„€)
166164nnne0d 12073 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 β‰  0)
167 simpr 486 . . . . . . . . . 10 ((𝑀 = 0 ∧ 𝑀 = 0) β†’ 𝑀 = 0)
168167necon3ai 2966 . . . . . . . . 9 (𝑀 β‰  0 β†’ Β¬ (𝑀 = 0 ∧ 𝑀 = 0))
169166, 168syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ Β¬ (𝑀 = 0 ∧ 𝑀 = 0))
170 gcdn0cl 16258 . . . . . . . 8 (((𝑀 ∈ β„€ ∧ 𝑀 ∈ β„€) ∧ Β¬ (𝑀 = 0 ∧ 𝑀 = 0)) β†’ (𝑀 gcd 𝑀) ∈ β„•)
171163, 165, 169, 170syl21anc 836 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑀) ∈ β„•)
172 gcddvds 16259 . . . . . . . . 9 ((𝑀 ∈ β„€ ∧ 𝑀 ∈ β„€) β†’ ((𝑀 gcd 𝑀) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑀) βˆ₯ 𝑀))
173163, 165, 172syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd 𝑀) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑀) βˆ₯ 𝑀))
174173simprd 497 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑀) βˆ₯ 𝑀)
175 breq1 5084 . . . . . . . 8 (π‘₯ = (𝑀 gcd 𝑀) β†’ (π‘₯ βˆ₯ 𝑀 ↔ (𝑀 gcd 𝑀) βˆ₯ 𝑀))
176175, 4elrab2 3632 . . . . . . 7 ((𝑀 gcd 𝑀) ∈ 𝑋 ↔ ((𝑀 gcd 𝑀) ∈ β„• ∧ (𝑀 gcd 𝑀) βˆ₯ 𝑀))
177171, 174, 176sylanbrc 584 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑀) ∈ 𝑋)
17832adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑁 ∈ β„•)
179178nnzd 12475 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑁 ∈ β„€)
180178nnne0d 12073 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑁 β‰  0)
181 simpr 486 . . . . . . . . . 10 ((𝑀 = 0 ∧ 𝑁 = 0) β†’ 𝑁 = 0)
182181necon3ai 2966 . . . . . . . . 9 (𝑁 β‰  0 β†’ Β¬ (𝑀 = 0 ∧ 𝑁 = 0))
183180, 182syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ Β¬ (𝑀 = 0 ∧ 𝑁 = 0))
184 gcdn0cl 16258 . . . . . . . 8 (((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ Β¬ (𝑀 = 0 ∧ 𝑁 = 0)) β†’ (𝑀 gcd 𝑁) ∈ β„•)
185163, 179, 183, 184syl21anc 836 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) ∈ β„•)
186 gcddvds 16259 . . . . . . . . 9 ((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ ((𝑀 gcd 𝑁) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
187163, 179, 186syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd 𝑁) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
188187simprd 497 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) βˆ₯ 𝑁)
189 breq1 5084 . . . . . . . 8 (π‘₯ = (𝑀 gcd 𝑁) β†’ (π‘₯ βˆ₯ 𝑁 ↔ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
190189, 8elrab2 3632 . . . . . . 7 ((𝑀 gcd 𝑁) ∈ π‘Œ ↔ ((𝑀 gcd 𝑁) ∈ β„• ∧ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
191185, 188, 190sylanbrc 584 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) ∈ π‘Œ)
192177, 191opelxpd 5638 . . . . 5 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ⟨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩ ∈ (𝑋 Γ— π‘Œ))
193192fvresd 6824 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩) = ( Β· β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
19489adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) = 1)
195 rpmulgcd2 16410 . . . . . . . 8 (((𝑀 ∈ β„€ ∧ 𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ (𝑀 gcd 𝑁) = 1) β†’ (𝑀 gcd (𝑀 Β· 𝑁)) = ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)))
196163, 165, 179, 194, 195syl31anc 1373 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd (𝑀 Β· 𝑁)) = ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)))
197 df-ov 7310 . . . . . . 7 ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)) = ( Β· β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩)
198196, 197eqtrdi 2792 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd (𝑀 Β· 𝑁)) = ( Β· β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
199160simprbi 498 . . . . . . . 8 (𝑀 ∈ 𝑍 β†’ 𝑀 βˆ₯ (𝑀 Β· 𝑁))
200199adantl 483 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 βˆ₯ (𝑀 Β· 𝑁))
20138, 32nnmulcld 12076 . . . . . . . 8 (πœ‘ β†’ (𝑀 Β· 𝑁) ∈ β„•)
202 gcdeq 16312 . . . . . . . 8 ((𝑀 ∈ β„• ∧ (𝑀 Β· 𝑁) ∈ β„•) β†’ ((𝑀 gcd (𝑀 Β· 𝑁)) = 𝑀 ↔ 𝑀 βˆ₯ (𝑀 Β· 𝑁)))
203161, 201, 202syl2anr 598 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd (𝑀 Β· 𝑁)) = 𝑀 ↔ 𝑀 βˆ₯ (𝑀 Β· 𝑁)))
204200, 203mpbird 257 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd (𝑀 Β· 𝑁)) = 𝑀)
205193, 198, 2043eqtr2rd 2783 . . . . 5 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
206 fveq2 6804 . . . . . 6 (𝑒 = ⟨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩ β†’ (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
207206rspceeqv 3580 . . . . 5 ((⟨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩ ∈ (𝑋 Γ— π‘Œ) ∧ 𝑀 = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩)) β†’ βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)𝑀 = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’))
208192, 205, 207syl2anc 585 . . . 4 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)𝑀 = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’))
209208ralrimiva 3140 . . 3 (πœ‘ β†’ βˆ€π‘€ ∈ 𝑍 βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)𝑀 = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’))
210 dffo3 7010 . . 3 (( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–onto→𝑍 ↔ (( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)βŸΆπ‘ ∧ βˆ€π‘€ ∈ 𝑍 βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)𝑀 = (( Β· β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’)))
21157, 209, 210sylanbrc 584 . 2 (πœ‘ β†’ ( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–onto→𝑍)
212 df-f1o 6465 . 2 (( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1-onto→𝑍 ↔ (( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1→𝑍 ∧ ( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–onto→𝑍))
213158, 211, 212sylanbrc 584 1 (πœ‘ β†’ ( Β· β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1-onto→𝑍)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1539   ∈ wcel 2104   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3303   βŠ† wss 3892  βŸ¨cop 4571   class class class wbr 5081   Γ— cxp 5598   β†Ύ cres 5602   Fn wfn 6453  βŸΆwf 6454  β€“1-1β†’wf1 6455  β€“ontoβ†’wfo 6456  β€“1-1-ontoβ†’wf1o 6457  β€˜cfv 6458  (class class class)co 7307  β„‚cc 10919  0cc0 10921  1c1 10922   Β· cmul 10926  β„•cn 12023  β„•0cn0 12283  β„€cz 12369   βˆ₯ cdvds 16012   gcd cgcd 16250
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-cnex 10977  ax-resscn 10978  ax-1cn 10979  ax-icn 10980  ax-addcl 10981  ax-addrcl 10982  ax-mulcl 10983  ax-mulrcl 10984  ax-mulcom 10985  ax-addass 10986  ax-mulass 10987  ax-distr 10988  ax-i2m1 10989  ax-1ne0 10990  ax-1rid 10991  ax-rnegex 10992  ax-rrecex 10993  ax-cnre 10994  ax-pre-lttri 10995  ax-pre-lttrn 10996  ax-pre-ltadd 10997  ax-pre-mulgt0 10998  ax-pre-sup 10999  ax-mulf 11001
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3304  df-reu 3305  df-rab 3306  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-er 8529  df-en 8765  df-dom 8766  df-sdom 8767  df-sup 9249  df-inf 9250  df-pnf 11061  df-mnf 11062  df-xr 11063  df-ltxr 11064  df-le 11065  df-sub 11257  df-neg 11258  df-div 11683  df-nn 12024  df-2 12086  df-3 12087  df-n0 12284  df-z 12370  df-uz 12633  df-rp 12781  df-fl 13562  df-mod 13640  df-seq 13772  df-exp 13833  df-cj 14859  df-re 14860  df-im 14861  df-sqrt 14995  df-abs 14996  df-dvds 16013  df-gcd 16251
This theorem is referenced by:  fsumdvdsmul  26393
  Copyright terms: Public domain W3C validator