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

Theorem mpodvdsmulf1o 27142
Description: If 𝑀 and 𝑁 are two coprime integers, multiplication forms a bijection from the set of pairs βŸ¨π‘—, π‘˜βŸ© where 𝑗 βˆ₯ 𝑀 and π‘˜ βˆ₯ 𝑁, to the set of divisors of 𝑀 Β· 𝑁. Version of dvdsmulf1o 27144 using maps-to notation, which does not require ax-mulf 11216. (Contributed by GG, 18-Apr-2025.)
Hypotheses
Ref Expression
mpodvdsmulf1o.1 (πœ‘ β†’ 𝑀 ∈ β„•)
mpodvdsmulf1o.2 (πœ‘ β†’ 𝑁 ∈ β„•)
mpodvdsmulf1o.3 (πœ‘ β†’ (𝑀 gcd 𝑁) = 1)
mpodvdsmulf1o.x 𝑋 = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑀}
mpodvdsmulf1o.y π‘Œ = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑁}
mpodvdsmulf1o.z 𝑍 = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ (𝑀 Β· 𝑁)}
Assertion
Ref Expression
mpodvdsmulf1o (πœ‘ β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1-onto→𝑍)
Distinct variable groups:   π‘₯,𝑦,𝑀   π‘₯,𝑁,𝑦
Allowed substitution hints:   πœ‘(π‘₯,𝑦)   𝑋(π‘₯,𝑦)   π‘Œ(π‘₯,𝑦)   𝑍(π‘₯,𝑦)

Proof of Theorem mpodvdsmulf1o
Dummy variables 𝑀 𝑒 𝑣 𝑖 𝑗 𝑛 π‘š are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mpomulf 11231 . . . . . . 7 (π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)):(β„‚ Γ— β„‚)βŸΆβ„‚
2 ffn 6716 . . . . . . 7 ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)):(β„‚ Γ— β„‚)βŸΆβ„‚ β†’ (π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) Fn (β„‚ Γ— β„‚))
31, 2ax-mp 5 . . . . . 6 (π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) Fn (β„‚ Γ— β„‚)
4 mpodvdsmulf1o.x . . . . . . . . 9 𝑋 = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑀}
54ssrab3 4072 . . . . . . . 8 𝑋 βŠ† β„•
6 nnsscn 12245 . . . . . . . 8 β„• βŠ† β„‚
75, 6sstri 3982 . . . . . . 7 𝑋 βŠ† β„‚
8 mpodvdsmulf1o.y . . . . . . . . 9 π‘Œ = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑁}
98ssrab3 4072 . . . . . . . 8 π‘Œ βŠ† β„•
109, 6sstri 3982 . . . . . . 7 π‘Œ βŠ† β„‚
11 xpss12 5687 . . . . . . 7 ((𝑋 βŠ† β„‚ ∧ π‘Œ βŠ† β„‚) β†’ (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚))
127, 10, 11mp2an 690 . . . . . 6 (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚)
13 fnssres 6672 . . . . . 6 (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) Fn (β„‚ Γ— β„‚) ∧ (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚)) β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)) Fn (𝑋 Γ— π‘Œ))
143, 12, 13mp2an 690 . . . . 5 ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)) Fn (𝑋 Γ— π‘Œ)
1514a1i 11 . . . 4 (πœ‘ β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)) Fn (𝑋 Γ— π‘Œ))
16 ovres 7583 . . . . . . 7 ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ) β†’ (𝑖((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))𝑗) = (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗))
1716adantl 480 . . . . . 6 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))𝑗) = (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗))
187sseli 3968 . . . . . . . . . 10 (𝑖 ∈ 𝑋 β†’ 𝑖 ∈ β„‚)
1918adantr 479 . . . . . . . . 9 ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ) β†’ 𝑖 ∈ β„‚)
2010sseli 3968 . . . . . . . . . 10 (𝑗 ∈ π‘Œ β†’ 𝑗 ∈ β„‚)
2120adantl 480 . . . . . . . . 9 ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ) β†’ 𝑗 ∈ β„‚)
22 ovmpot 7578 . . . . . . . . . 10 ((𝑖 ∈ β„‚ ∧ 𝑗 ∈ β„‚) β†’ (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (𝑖 Β· 𝑗))
2322eqcomd 2731 . . . . . . . . 9 ((𝑖 ∈ β„‚ ∧ 𝑗 ∈ β„‚) β†’ (𝑖 Β· 𝑗) = (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗))
2419, 21, 23syl2anc 582 . . . . . . . 8 ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ) β†’ (𝑖 Β· 𝑗) = (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗))
2524adantl 480 . . . . . . 7 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) = (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗))
265sseli 3968 . . . . . . . . . 10 (𝑖 ∈ 𝑋 β†’ 𝑖 ∈ β„•)
2726ad2antrl 726 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑖 ∈ β„•)
289sseli 3968 . . . . . . . . . 10 (𝑗 ∈ π‘Œ β†’ 𝑗 ∈ β„•)
2928ad2antll 727 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑗 ∈ β„•)
3027, 29nnmulcld 12293 . . . . . . . 8 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) ∈ β„•)
31 breq1 5146 . . . . . . . . . . . 12 (π‘₯ = 𝑗 β†’ (π‘₯ βˆ₯ 𝑁 ↔ 𝑗 βˆ₯ 𝑁))
3231, 8elrab2 3678 . . . . . . . . . . 11 (𝑗 ∈ π‘Œ ↔ (𝑗 ∈ β„• ∧ 𝑗 βˆ₯ 𝑁))
3332simprbi 495 . . . . . . . . . 10 (𝑗 ∈ π‘Œ β†’ 𝑗 βˆ₯ 𝑁)
3433ad2antll 727 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑗 βˆ₯ 𝑁)
35 breq1 5146 . . . . . . . . . . . 12 (π‘₯ = 𝑖 β†’ (π‘₯ βˆ₯ 𝑀 ↔ 𝑖 βˆ₯ 𝑀))
3635, 4elrab2 3678 . . . . . . . . . . 11 (𝑖 ∈ 𝑋 ↔ (𝑖 ∈ β„• ∧ 𝑖 βˆ₯ 𝑀))
3736simprbi 495 . . . . . . . . . 10 (𝑖 ∈ 𝑋 β†’ 𝑖 βˆ₯ 𝑀)
3837ad2antrl 726 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑖 βˆ₯ 𝑀)
3929nnzd 12613 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑗 ∈ β„€)
40 mpodvdsmulf1o.2 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ β„•)
4140adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑁 ∈ β„•)
4241nnzd 12613 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑁 ∈ β„€)
4327nnzd 12613 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑖 ∈ β„€)
44 dvdscmul 16257 . . . . . . . . . . 11 ((𝑗 ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ 𝑖 ∈ β„€) β†’ (𝑗 βˆ₯ 𝑁 β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑖 Β· 𝑁)))
4539, 42, 43, 44syl3anc 1368 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑗 βˆ₯ 𝑁 β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑖 Β· 𝑁)))
46 mpodvdsmulf1o.1 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ β„•)
4746adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑀 ∈ β„•)
4847nnzd 12613 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑀 ∈ β„€)
49 dvdsmulc 16258 . . . . . . . . . . 11 ((𝑖 ∈ β„€ ∧ 𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑖 βˆ₯ 𝑀 β†’ (𝑖 Β· 𝑁) βˆ₯ (𝑀 Β· 𝑁)))
5043, 48, 42, 49syl3anc 1368 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 βˆ₯ 𝑀 β†’ (𝑖 Β· 𝑁) βˆ₯ (𝑀 Β· 𝑁)))
5130nnzd 12613 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) ∈ β„€)
5243, 42zmulcld 12700 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑁) ∈ β„€)
5348, 42zmulcld 12700 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑀 Β· 𝑁) ∈ β„€)
54 dvdstr 16268 . . . . . . . . . . 11 (((𝑖 Β· 𝑗) ∈ β„€ ∧ (𝑖 Β· 𝑁) ∈ β„€ ∧ (𝑀 Β· 𝑁) ∈ β„€) β†’ (((𝑖 Β· 𝑗) βˆ₯ (𝑖 Β· 𝑁) ∧ (𝑖 Β· 𝑁) βˆ₯ (𝑀 Β· 𝑁)) β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
5551, 52, 53, 54syl3anc 1368 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (((𝑖 Β· 𝑗) βˆ₯ (𝑖 Β· 𝑁) ∧ (𝑖 Β· 𝑁) βˆ₯ (𝑀 Β· 𝑁)) β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
5645, 50, 55syl2and 606 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ ((𝑗 βˆ₯ 𝑁 ∧ 𝑖 βˆ₯ 𝑀) β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
5734, 38, 56mp2and 697 . . . . . . . 8 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁))
58 breq1 5146 . . . . . . . . 9 (π‘₯ = (𝑖 Β· 𝑗) β†’ (π‘₯ βˆ₯ (𝑀 Β· 𝑁) ↔ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
59 mpodvdsmulf1o.z . . . . . . . . 9 𝑍 = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ (𝑀 Β· 𝑁)}
6058, 59elrab2 3678 . . . . . . . 8 ((𝑖 Β· 𝑗) ∈ 𝑍 ↔ ((𝑖 Β· 𝑗) ∈ β„• ∧ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
6130, 57, 60sylanbrc 581 . . . . . . 7 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) ∈ 𝑍)
6225, 61eqeltrrd 2826 . . . . . 6 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) ∈ 𝑍)
6317, 62eqeltrd 2825 . . . . 5 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))𝑗) ∈ 𝑍)
6463ralrimivva 3191 . . . 4 (πœ‘ β†’ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ (𝑖((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))𝑗) ∈ 𝑍)
65 ffnov 7543 . . . 4 (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)βŸΆπ‘ ↔ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)) Fn (𝑋 Γ— π‘Œ) ∧ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ (𝑖((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))𝑗) ∈ 𝑍))
6615, 64, 65sylanbrc 581 . . 3 (πœ‘ β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)βŸΆπ‘)
6719ad2antlr 725 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ 𝑖 ∈ β„‚)
6821ad2antlr 725 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ 𝑗 ∈ β„‚)
6967, 68, 22syl2anc 582 . . . . . . . 8 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (𝑖 Β· 𝑗))
707sseli 3968 . . . . . . . . . 10 (π‘š ∈ 𝑋 β†’ π‘š ∈ β„‚)
7170ad2antrl 726 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ π‘š ∈ β„‚)
7210sseli 3968 . . . . . . . . . 10 (𝑛 ∈ π‘Œ β†’ 𝑛 ∈ β„‚)
7372ad2antll 727 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ 𝑛 ∈ β„‚)
74 ovmpot 7578 . . . . . . . . 9 ((π‘š ∈ β„‚ ∧ 𝑛 ∈ β„‚) β†’ (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) = (π‘š Β· 𝑛))
7571, 73, 74syl2anc 582 . . . . . . . 8 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) = (π‘š Β· 𝑛))
7669, 75eqeq12d 2741 . . . . . . 7 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) ↔ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛)))
7727adantr 479 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 ∈ β„•)
7877nnnn0d 12560 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 ∈ β„•0)
79 simprll 777 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ 𝑋)
805, 79sselid 3970 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ β„•)
8180nnnn0d 12560 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ β„•0)
8277nnzd 12613 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 ∈ β„€)
8329adantr 479 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 ∈ β„•)
8483nnzd 12613 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 ∈ β„€)
85 dvdsmul1 16252 . . . . . . . . . . . . 13 ((𝑖 ∈ β„€ ∧ 𝑗 ∈ β„€) β†’ 𝑖 βˆ₯ (𝑖 Β· 𝑗))
8682, 84, 85syl2anc 582 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 βˆ₯ (𝑖 Β· 𝑗))
87 simprr 771 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))
887, 79sselid 3970 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ β„‚)
89 simprlr 778 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 ∈ π‘Œ)
9010, 89sselid 3970 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 ∈ β„‚)
9188, 90mulcomd 11263 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š Β· 𝑛) = (𝑛 Β· π‘š))
9287, 91eqtrd 2765 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑗) = (𝑛 Β· π‘š))
9386, 92breqtrd 5169 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 βˆ₯ (𝑛 Β· π‘š))
949, 89sselid 3970 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 ∈ β„•)
9594nnzd 12613 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 ∈ β„€)
9642adantr 479 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑁 ∈ β„€)
9782, 96gcdcomd 16486 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
9848adantr 479 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑀 ∈ β„€)
9940nnzd 12613 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑁 ∈ β„€)
10046nnzd 12613 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑀 ∈ β„€)
10199, 100gcdcomd 16486 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
102 mpodvdsmulf1o.3 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑀 gcd 𝑁) = 1)
103101, 102eqtrd 2765 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑁 gcd 𝑀) = 1)
104103ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑁 gcd 𝑀) = 1)
10538adantr 479 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 βˆ₯ 𝑀)
106 rpdvds 16628 . . . . . . . . . . . . . 14 (((𝑁 ∈ β„€ ∧ 𝑖 ∈ β„€ ∧ 𝑀 ∈ β„€) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑖 βˆ₯ 𝑀)) β†’ (𝑁 gcd 𝑖) = 1)
10796, 82, 98, 104, 105, 106syl32anc 1375 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑁 gcd 𝑖) = 1)
10897, 107eqtrd 2765 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 gcd 𝑁) = 1)
109 breq1 5146 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑛 β†’ (π‘₯ βˆ₯ 𝑁 ↔ 𝑛 βˆ₯ 𝑁))
110109, 8elrab2 3678 . . . . . . . . . . . . . 14 (𝑛 ∈ π‘Œ ↔ (𝑛 ∈ β„• ∧ 𝑛 βˆ₯ 𝑁))
111110simprbi 495 . . . . . . . . . . . . 13 (𝑛 ∈ π‘Œ β†’ 𝑛 βˆ₯ 𝑁)
11289, 111syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 βˆ₯ 𝑁)
113 rpdvds 16628 . . . . . . . . . . . 12 (((𝑖 ∈ β„€ ∧ 𝑛 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ ((𝑖 gcd 𝑁) = 1 ∧ 𝑛 βˆ₯ 𝑁)) β†’ (𝑖 gcd 𝑛) = 1)
11482, 95, 96, 108, 112, 113syl32anc 1375 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 gcd 𝑛) = 1)
11580nnzd 12613 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ β„€)
116 coprmdvds 16621 . . . . . . . . . . . 12 ((𝑖 ∈ β„€ ∧ 𝑛 ∈ β„€ ∧ π‘š ∈ β„€) β†’ ((𝑖 βˆ₯ (𝑛 Β· π‘š) ∧ (𝑖 gcd 𝑛) = 1) β†’ 𝑖 βˆ₯ π‘š))
11782, 95, 115, 116syl3anc 1368 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ ((𝑖 βˆ₯ (𝑛 Β· π‘š) ∧ (𝑖 gcd 𝑛) = 1) β†’ 𝑖 βˆ₯ π‘š))
11893, 114, 117mp2and 697 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 βˆ₯ π‘š)
119 dvdsmul1 16252 . . . . . . . . . . . . 13 ((π‘š ∈ β„€ ∧ 𝑛 ∈ β„€) β†’ π‘š βˆ₯ (π‘š Β· 𝑛))
120115, 95, 119syl2anc 582 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š βˆ₯ (π‘š Β· 𝑛))
12177nncnd 12256 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 ∈ β„‚)
12283nncnd 12256 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 ∈ β„‚)
123121, 122mulcomd 11263 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑗) = (𝑗 Β· 𝑖))
12487, 123eqtr3d 2767 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š Β· 𝑛) = (𝑗 Β· 𝑖))
125120, 124breqtrd 5169 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š βˆ₯ (𝑗 Β· 𝑖))
126115, 96gcdcomd 16486 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š gcd 𝑁) = (𝑁 gcd π‘š))
127 breq1 5146 . . . . . . . . . . . . . . . . 17 (π‘₯ = π‘š β†’ (π‘₯ βˆ₯ 𝑀 ↔ π‘š βˆ₯ 𝑀))
128127, 4elrab2 3678 . . . . . . . . . . . . . . . 16 (π‘š ∈ 𝑋 ↔ (π‘š ∈ β„• ∧ π‘š βˆ₯ 𝑀))
129128simprbi 495 . . . . . . . . . . . . . . 15 (π‘š ∈ 𝑋 β†’ π‘š βˆ₯ 𝑀)
13079, 129syl 17 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š βˆ₯ 𝑀)
131 rpdvds 16628 . . . . . . . . . . . . . 14 (((𝑁 ∈ β„€ ∧ π‘š ∈ β„€ ∧ 𝑀 ∈ β„€) ∧ ((𝑁 gcd 𝑀) = 1 ∧ π‘š βˆ₯ 𝑀)) β†’ (𝑁 gcd π‘š) = 1)
13296, 115, 98, 104, 130, 131syl32anc 1375 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑁 gcd π‘š) = 1)
133126, 132eqtrd 2765 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š gcd 𝑁) = 1)
13434adantr 479 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 βˆ₯ 𝑁)
135 rpdvds 16628 . . . . . . . . . . . 12 (((π‘š ∈ β„€ ∧ 𝑗 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ ((π‘š gcd 𝑁) = 1 ∧ 𝑗 βˆ₯ 𝑁)) β†’ (π‘š gcd 𝑗) = 1)
136115, 84, 96, 133, 134, 135syl32anc 1375 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š gcd 𝑗) = 1)
137 coprmdvds 16621 . . . . . . . . . . . 12 ((π‘š ∈ β„€ ∧ 𝑗 ∈ β„€ ∧ 𝑖 ∈ β„€) β†’ ((π‘š βˆ₯ (𝑗 Β· 𝑖) ∧ (π‘š gcd 𝑗) = 1) β†’ π‘š βˆ₯ 𝑖))
138115, 84, 82, 137syl3anc 1368 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ ((π‘š βˆ₯ (𝑗 Β· 𝑖) ∧ (π‘š gcd 𝑗) = 1) β†’ π‘š βˆ₯ 𝑖))
139125, 136, 138mp2and 697 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š βˆ₯ 𝑖)
140 dvdseq 16288 . . . . . . . . . 10 (((𝑖 ∈ β„•0 ∧ π‘š ∈ β„•0) ∧ (𝑖 βˆ₯ π‘š ∧ π‘š βˆ₯ 𝑖)) β†’ 𝑖 = π‘š)
14178, 81, 118, 139, 140syl22anc 837 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 = π‘š)
14277nnne0d 12290 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 β‰  0)
143141oveq1d 7430 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑛) = (π‘š Β· 𝑛))
14487, 143eqtr4d 2768 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑗) = (𝑖 Β· 𝑛))
145122, 90, 121, 142, 144mulcanad 11877 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 = 𝑛)
146141, 145opeq12d 4877 . . . . . . . 8 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©)
147146expr 455 . . . . . . 7 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ ((𝑖 Β· 𝑗) = (π‘š Β· 𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
14876, 147sylbid 239 . . . . . 6 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
149148ralrimivva 3191 . . . . 5 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
150149ralrimivva 3191 . . . 4 (πœ‘ β†’ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
151 fvres 6910 . . . . . . . . 9 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’))
152 fvres 6910 . . . . . . . . 9 (𝑣 ∈ (𝑋 Γ— π‘Œ) β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£))
153151, 152eqeqan12d 2739 . . . . . . . 8 ((𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (𝑋 Γ— π‘Œ)) β†’ ((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) ↔ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£)))
154153imbi1d 340 . . . . . . 7 ((𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (𝑋 Γ— π‘Œ)) β†’ (((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣)))
155154ralbidva 3166 . . . . . 6 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣)))
156155ralbiia 3081 . . . . 5 (βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣))
157 fveq2 6891 . . . . . . . . . . 11 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨π‘š, π‘›βŸ©))
158 df-ov 7418 . . . . . . . . . . 11 (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨π‘š, π‘›βŸ©)
159157, 158eqtr4di 2783 . . . . . . . . . 10 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛))
160159eqeq2d 2736 . . . . . . . . 9 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) ↔ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛)))
161 eqeq2 2737 . . . . . . . . 9 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ (𝑒 = 𝑣 ↔ 𝑒 = βŸ¨π‘š, π‘›βŸ©))
162160, 161imbi12d 343 . . . . . . . 8 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ ((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ 𝑒 = βŸ¨π‘š, π‘›βŸ©)))
163162ralxp 5838 . . . . . . 7 (βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ 𝑒 = βŸ¨π‘š, π‘›βŸ©))
164 fveq2 6891 . . . . . . . . . . 11 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨π‘–, π‘—βŸ©))
165 df-ov 7418 . . . . . . . . . . 11 (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨π‘–, π‘—βŸ©)
166164, 165eqtr4di 2783 . . . . . . . . . 10 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗))
167166eqeq1d 2727 . . . . . . . . 9 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) ↔ (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛)))
168 eqeq1 2729 . . . . . . . . 9 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ (𝑒 = βŸ¨π‘š, π‘›βŸ© ↔ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
169167, 168imbi12d 343 . . . . . . . 8 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ ((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ 𝑒 = βŸ¨π‘š, π‘›βŸ©) ↔ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©)))
1701692ralbidv 3209 . . . . . . 7 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ (βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ 𝑒 = βŸ¨π‘š, π‘›βŸ©) ↔ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©)))
171163, 170bitrid 282 . . . . . 6 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ (βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©)))
172171ralxp 5838 . . . . 5 (βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
173156, 172bitri 274 . . . 4 (βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
174150, 173sylibr 233 . . 3 (πœ‘ β†’ βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣))
175 dff13 7260 . . 3 (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1→𝑍 ↔ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)βŸΆπ‘ ∧ βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣)))
17666, 174, 175sylanbrc 581 . 2 (πœ‘ β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1→𝑍)
177 breq1 5146 . . . . . . . . . . . 12 (π‘₯ = 𝑀 β†’ (π‘₯ βˆ₯ (𝑀 Β· 𝑁) ↔ 𝑀 βˆ₯ (𝑀 Β· 𝑁)))
178177, 59elrab2 3678 . . . . . . . . . . 11 (𝑀 ∈ 𝑍 ↔ (𝑀 ∈ β„• ∧ 𝑀 βˆ₯ (𝑀 Β· 𝑁)))
179178simplbi 496 . . . . . . . . . 10 (𝑀 ∈ 𝑍 β†’ 𝑀 ∈ β„•)
180179adantl 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 ∈ β„•)
181180nnzd 12613 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 ∈ β„€)
18246adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 ∈ β„•)
183182nnzd 12613 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 ∈ β„€)
184182nnne0d 12290 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 β‰  0)
185 simpr 483 . . . . . . . . . 10 ((𝑀 = 0 ∧ 𝑀 = 0) β†’ 𝑀 = 0)
186185necon3ai 2955 . . . . . . . . 9 (𝑀 β‰  0 β†’ Β¬ (𝑀 = 0 ∧ 𝑀 = 0))
187184, 186syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ Β¬ (𝑀 = 0 ∧ 𝑀 = 0))
188 gcdn0cl 16474 . . . . . . . 8 (((𝑀 ∈ β„€ ∧ 𝑀 ∈ β„€) ∧ Β¬ (𝑀 = 0 ∧ 𝑀 = 0)) β†’ (𝑀 gcd 𝑀) ∈ β„•)
189181, 183, 187, 188syl21anc 836 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑀) ∈ β„•)
190 gcddvds 16475 . . . . . . . . 9 ((𝑀 ∈ β„€ ∧ 𝑀 ∈ β„€) β†’ ((𝑀 gcd 𝑀) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑀) βˆ₯ 𝑀))
191181, 183, 190syl2anc 582 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd 𝑀) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑀) βˆ₯ 𝑀))
192191simprd 494 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑀) βˆ₯ 𝑀)
193 breq1 5146 . . . . . . . 8 (π‘₯ = (𝑀 gcd 𝑀) β†’ (π‘₯ βˆ₯ 𝑀 ↔ (𝑀 gcd 𝑀) βˆ₯ 𝑀))
194193, 4elrab2 3678 . . . . . . 7 ((𝑀 gcd 𝑀) ∈ 𝑋 ↔ ((𝑀 gcd 𝑀) ∈ β„• ∧ (𝑀 gcd 𝑀) βˆ₯ 𝑀))
195189, 192, 194sylanbrc 581 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑀) ∈ 𝑋)
19640adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑁 ∈ β„•)
197196nnzd 12613 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑁 ∈ β„€)
198196nnne0d 12290 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑁 β‰  0)
199 simpr 483 . . . . . . . . . 10 ((𝑀 = 0 ∧ 𝑁 = 0) β†’ 𝑁 = 0)
200199necon3ai 2955 . . . . . . . . 9 (𝑁 β‰  0 β†’ Β¬ (𝑀 = 0 ∧ 𝑁 = 0))
201198, 200syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ Β¬ (𝑀 = 0 ∧ 𝑁 = 0))
202 gcdn0cl 16474 . . . . . . . 8 (((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ Β¬ (𝑀 = 0 ∧ 𝑁 = 0)) β†’ (𝑀 gcd 𝑁) ∈ β„•)
203181, 197, 201, 202syl21anc 836 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) ∈ β„•)
204 gcddvds 16475 . . . . . . . . 9 ((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ ((𝑀 gcd 𝑁) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
205181, 197, 204syl2anc 582 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd 𝑁) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
206205simprd 494 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) βˆ₯ 𝑁)
207 breq1 5146 . . . . . . . 8 (π‘₯ = (𝑀 gcd 𝑁) β†’ (π‘₯ βˆ₯ 𝑁 ↔ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
208207, 8elrab2 3678 . . . . . . 7 ((𝑀 gcd 𝑁) ∈ π‘Œ ↔ ((𝑀 gcd 𝑁) ∈ β„• ∧ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
209203, 206, 208sylanbrc 581 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) ∈ π‘Œ)
210195, 209opelxpd 5711 . . . . 5 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ⟨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩ ∈ (𝑋 Γ— π‘Œ))
211210fvresd 6911 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
212 df-ov 7418 . . . . . . . 8 ((𝑀 gcd 𝑀)(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))(𝑀 gcd 𝑁)) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩)
213189nncnd 12256 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑀) ∈ β„‚)
214203nncnd 12256 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) ∈ β„‚)
215 ovmpot 7578 . . . . . . . . 9 (((𝑀 gcd 𝑀) ∈ β„‚ ∧ (𝑀 gcd 𝑁) ∈ β„‚) β†’ ((𝑀 gcd 𝑀)(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))(𝑀 gcd 𝑁)) = ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)))
216213, 214, 215syl2anc 582 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd 𝑀)(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))(𝑀 gcd 𝑁)) = ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)))
217212, 216eqtr3id 2779 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩) = ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)))
218 df-ov 7418 . . . . . . . 8 ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)) = ( Β· β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩)
219218a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)) = ( Β· β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
220211, 217, 2193eqtrd 2769 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩) = ( Β· β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
221102adantr 479 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) = 1)
222 rpmulgcd2 16624 . . . . . . . 8 (((𝑀 ∈ β„€ ∧ 𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ (𝑀 gcd 𝑁) = 1) β†’ (𝑀 gcd (𝑀 Β· 𝑁)) = ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)))
223181, 183, 197, 221, 222syl31anc 1370 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd (𝑀 Β· 𝑁)) = ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)))
224223, 218eqtrdi 2781 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd (𝑀 Β· 𝑁)) = ( Β· β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
225178simprbi 495 . . . . . . . 8 (𝑀 ∈ 𝑍 β†’ 𝑀 βˆ₯ (𝑀 Β· 𝑁))
226225adantl 480 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 βˆ₯ (𝑀 Β· 𝑁))
22746, 40nnmulcld 12293 . . . . . . . 8 (πœ‘ β†’ (𝑀 Β· 𝑁) ∈ β„•)
228 gcdeq 16526 . . . . . . . 8 ((𝑀 ∈ β„• ∧ (𝑀 Β· 𝑁) ∈ β„•) β†’ ((𝑀 gcd (𝑀 Β· 𝑁)) = 𝑀 ↔ 𝑀 βˆ₯ (𝑀 Β· 𝑁)))
229179, 227, 228syl2anr 595 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd (𝑀 Β· 𝑁)) = 𝑀 ↔ 𝑀 βˆ₯ (𝑀 Β· 𝑁)))
230226, 229mpbird 256 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd (𝑀 Β· 𝑁)) = 𝑀)
231220, 224, 2303eqtr2rd 2772 . . . . 5 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
232 fveq2 6891 . . . . . 6 (𝑒 = ⟨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩ β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
233232rspceeqv 3624 . . . . 5 ((⟨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩ ∈ (𝑋 Γ— π‘Œ) ∧ 𝑀 = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩)) β†’ βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)𝑀 = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’))
234210, 231, 233syl2anc 582 . . . 4 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)𝑀 = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’))
235234ralrimiva 3136 . . 3 (πœ‘ β†’ βˆ€π‘€ ∈ 𝑍 βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)𝑀 = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’))
236 dffo3 7106 . . 3 (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–onto→𝑍 ↔ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)βŸΆπ‘ ∧ βˆ€π‘€ ∈ 𝑍 βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)𝑀 = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’)))
23766, 235, 236sylanbrc 581 . 2 (πœ‘ β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–onto→𝑍)
238 df-f1o 6549 . 2 (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1-onto→𝑍 ↔ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1→𝑍 ∧ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–onto→𝑍))
239176, 237, 238sylanbrc 581 1 (πœ‘ β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1-onto→𝑍)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098   β‰  wne 2930  βˆ€wral 3051  βˆƒwrex 3060  {crab 3419   βŠ† wss 3940  βŸ¨cop 4630   class class class wbr 5143   Γ— cxp 5670   β†Ύ cres 5674   Fn wfn 6537  βŸΆwf 6538  β€“1-1β†’wf1 6539  β€“ontoβ†’wfo 6540  β€“1-1-ontoβ†’wf1o 6541  β€˜cfv 6542  (class class class)co 7415   ∈ cmpo 7417  β„‚cc 11134  0cc0 11136  1c1 11137   Β· cmul 11141  β„•cn 12240  β„•0cn0 12500  β„€cz 12586   βˆ₯ cdvds 16228   gcd cgcd 16466
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7737  ax-cnex 11192  ax-resscn 11193  ax-1cn 11194  ax-icn 11195  ax-addcl 11196  ax-addrcl 11197  ax-mulcl 11198  ax-mulrcl 11199  ax-mulcom 11200  ax-addass 11201  ax-mulass 11202  ax-distr 11203  ax-i2m1 11204  ax-1ne0 11205  ax-1rid 11206  ax-rnegex 11207  ax-rrecex 11208  ax-cnre 11209  ax-pre-lttri 11210  ax-pre-lttrn 11211  ax-pre-ltadd 11212  ax-pre-mulgt0 11213  ax-pre-sup 11214
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3960  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-om 7868  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8388  df-rdg 8427  df-er 8721  df-en 8961  df-dom 8962  df-sdom 8963  df-sup 9463  df-inf 9464  df-pnf 11278  df-mnf 11279  df-xr 11280  df-ltxr 11281  df-le 11282  df-sub 11474  df-neg 11475  df-div 11900  df-nn 12241  df-2 12303  df-3 12304  df-n0 12501  df-z 12587  df-uz 12851  df-rp 13005  df-fl 13787  df-mod 13865  df-seq 13997  df-exp 14057  df-cj 15076  df-re 15077  df-im 15078  df-sqrt 15212  df-abs 15213  df-dvds 16229  df-gcd 16467
This theorem is referenced by:  fsumdvdsmul  27143
  Copyright terms: Public domain W3C validator