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

Theorem mpodvdsmulf1o 27081
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 27083 using maps-to notation, which does not require ax-mulf 11192. (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 11207 . . . . . . 7 (π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)):(β„‚ Γ— β„‚)βŸΆβ„‚
2 ffn 6711 . . . . . . 7 ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)):(β„‚ Γ— β„‚)βŸΆβ„‚ β†’ (π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) Fn (β„‚ Γ— β„‚))
31, 2ax-mp 5 . . . . . 6 (π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) Fn (β„‚ Γ— β„‚)
4 mpodvdsmulf1o.x . . . . . . . . 9 𝑋 = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑀}
54ssrab3 4075 . . . . . . . 8 𝑋 βŠ† β„•
6 nnsscn 12221 . . . . . . . 8 β„• βŠ† β„‚
75, 6sstri 3986 . . . . . . 7 𝑋 βŠ† β„‚
8 mpodvdsmulf1o.y . . . . . . . . 9 π‘Œ = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑁}
98ssrab3 4075 . . . . . . . 8 π‘Œ βŠ† β„•
109, 6sstri 3986 . . . . . . 7 π‘Œ βŠ† β„‚
11 xpss12 5684 . . . . . . 7 ((𝑋 βŠ† β„‚ ∧ π‘Œ βŠ† β„‚) β†’ (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚))
127, 10, 11mp2an 689 . . . . . 6 (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚)
13 fnssres 6667 . . . . . 6 (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) Fn (β„‚ Γ— β„‚) ∧ (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚)) β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)) Fn (𝑋 Γ— π‘Œ))
143, 12, 13mp2an 689 . . . . 5 ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)) Fn (𝑋 Γ— π‘Œ)
1514a1i 11 . . . 4 (πœ‘ β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)) Fn (𝑋 Γ— π‘Œ))
16 ovres 7570 . . . . . . 7 ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ) β†’ (𝑖((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))𝑗) = (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗))
1716adantl 481 . . . . . 6 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))𝑗) = (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗))
187sseli 3973 . . . . . . . . . 10 (𝑖 ∈ 𝑋 β†’ 𝑖 ∈ β„‚)
1918adantr 480 . . . . . . . . 9 ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ) β†’ 𝑖 ∈ β„‚)
2010sseli 3973 . . . . . . . . . 10 (𝑗 ∈ π‘Œ β†’ 𝑗 ∈ β„‚)
2120adantl 481 . . . . . . . . 9 ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ) β†’ 𝑗 ∈ β„‚)
22 ovmpot 7565 . . . . . . . . . 10 ((𝑖 ∈ β„‚ ∧ 𝑗 ∈ β„‚) β†’ (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (𝑖 Β· 𝑗))
2322eqcomd 2732 . . . . . . . . 9 ((𝑖 ∈ β„‚ ∧ 𝑗 ∈ β„‚) β†’ (𝑖 Β· 𝑗) = (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗))
2419, 21, 23syl2anc 583 . . . . . . . 8 ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ) β†’ (𝑖 Β· 𝑗) = (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗))
2524adantl 481 . . . . . . 7 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) = (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗))
265sseli 3973 . . . . . . . . . 10 (𝑖 ∈ 𝑋 β†’ 𝑖 ∈ β„•)
2726ad2antrl 725 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑖 ∈ β„•)
289sseli 3973 . . . . . . . . . 10 (𝑗 ∈ π‘Œ β†’ 𝑗 ∈ β„•)
2928ad2antll 726 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑗 ∈ β„•)
3027, 29nnmulcld 12269 . . . . . . . 8 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) ∈ β„•)
31 breq1 5144 . . . . . . . . . . . 12 (π‘₯ = 𝑗 β†’ (π‘₯ βˆ₯ 𝑁 ↔ 𝑗 βˆ₯ 𝑁))
3231, 8elrab2 3681 . . . . . . . . . . 11 (𝑗 ∈ π‘Œ ↔ (𝑗 ∈ β„• ∧ 𝑗 βˆ₯ 𝑁))
3332simprbi 496 . . . . . . . . . 10 (𝑗 ∈ π‘Œ β†’ 𝑗 βˆ₯ 𝑁)
3433ad2antll 726 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑗 βˆ₯ 𝑁)
35 breq1 5144 . . . . . . . . . . . 12 (π‘₯ = 𝑖 β†’ (π‘₯ βˆ₯ 𝑀 ↔ 𝑖 βˆ₯ 𝑀))
3635, 4elrab2 3681 . . . . . . . . . . 11 (𝑖 ∈ 𝑋 ↔ (𝑖 ∈ β„• ∧ 𝑖 βˆ₯ 𝑀))
3736simprbi 496 . . . . . . . . . 10 (𝑖 ∈ 𝑋 β†’ 𝑖 βˆ₯ 𝑀)
3837ad2antrl 725 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑖 βˆ₯ 𝑀)
3929nnzd 12589 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑗 ∈ β„€)
40 mpodvdsmulf1o.2 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ β„•)
4140adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑁 ∈ β„•)
4241nnzd 12589 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑁 ∈ β„€)
4327nnzd 12589 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑖 ∈ β„€)
44 dvdscmul 16233 . . . . . . . . . . 11 ((𝑗 ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ 𝑖 ∈ β„€) β†’ (𝑗 βˆ₯ 𝑁 β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑖 Β· 𝑁)))
4539, 42, 43, 44syl3anc 1368 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑗 βˆ₯ 𝑁 β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑖 Β· 𝑁)))
46 mpodvdsmulf1o.1 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ β„•)
4746adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑀 ∈ β„•)
4847nnzd 12589 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ 𝑀 ∈ β„€)
49 dvdsmulc 16234 . . . . . . . . . . 11 ((𝑖 ∈ β„€ ∧ 𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑖 βˆ₯ 𝑀 β†’ (𝑖 Β· 𝑁) βˆ₯ (𝑀 Β· 𝑁)))
5043, 48, 42, 49syl3anc 1368 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 βˆ₯ 𝑀 β†’ (𝑖 Β· 𝑁) βˆ₯ (𝑀 Β· 𝑁)))
5130nnzd 12589 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) ∈ β„€)
5243, 42zmulcld 12676 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑁) ∈ β„€)
5348, 42zmulcld 12676 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑀 Β· 𝑁) ∈ β„€)
54 dvdstr 16244 . . . . . . . . . . 11 (((𝑖 Β· 𝑗) ∈ β„€ ∧ (𝑖 Β· 𝑁) ∈ β„€ ∧ (𝑀 Β· 𝑁) ∈ β„€) β†’ (((𝑖 Β· 𝑗) βˆ₯ (𝑖 Β· 𝑁) ∧ (𝑖 Β· 𝑁) βˆ₯ (𝑀 Β· 𝑁)) β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
5551, 52, 53, 54syl3anc 1368 . . . . . . . . . 10 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (((𝑖 Β· 𝑗) βˆ₯ (𝑖 Β· 𝑁) ∧ (𝑖 Β· 𝑁) βˆ₯ (𝑀 Β· 𝑁)) β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
5645, 50, 55syl2and 607 . . . . . . . . 9 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ ((𝑗 βˆ₯ 𝑁 ∧ 𝑖 βˆ₯ 𝑀) β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
5734, 38, 56mp2and 696 . . . . . . . 8 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁))
58 breq1 5144 . . . . . . . . 9 (π‘₯ = (𝑖 Β· 𝑗) β†’ (π‘₯ βˆ₯ (𝑀 Β· 𝑁) ↔ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
59 mpodvdsmulf1o.z . . . . . . . . 9 𝑍 = {π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ (𝑀 Β· 𝑁)}
6058, 59elrab2 3681 . . . . . . . 8 ((𝑖 Β· 𝑗) ∈ 𝑍 ↔ ((𝑖 Β· 𝑗) ∈ β„• ∧ (𝑖 Β· 𝑗) βˆ₯ (𝑀 Β· 𝑁)))
6130, 57, 60sylanbrc 582 . . . . . . 7 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖 Β· 𝑗) ∈ 𝑍)
6225, 61eqeltrrd 2828 . . . . . 6 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) ∈ 𝑍)
6317, 62eqeltrd 2827 . . . . 5 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ (𝑖((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))𝑗) ∈ 𝑍)
6463ralrimivva 3194 . . . 4 (πœ‘ β†’ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ (𝑖((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))𝑗) ∈ 𝑍)
65 ffnov 7531 . . . 4 (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)βŸΆπ‘ ↔ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)) Fn (𝑋 Γ— π‘Œ) ∧ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ (𝑖((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))𝑗) ∈ 𝑍))
6615, 64, 65sylanbrc 582 . . 3 (πœ‘ β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)βŸΆπ‘)
6719ad2antlr 724 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ 𝑖 ∈ β„‚)
6821ad2antlr 724 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ 𝑗 ∈ β„‚)
6967, 68, 22syl2anc 583 . . . . . . . 8 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (𝑖 Β· 𝑗))
707sseli 3973 . . . . . . . . . 10 (π‘š ∈ 𝑋 β†’ π‘š ∈ β„‚)
7170ad2antrl 725 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ π‘š ∈ β„‚)
7210sseli 3973 . . . . . . . . . 10 (𝑛 ∈ π‘Œ β†’ 𝑛 ∈ β„‚)
7372ad2antll 726 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ 𝑛 ∈ β„‚)
74 ovmpot 7565 . . . . . . . . 9 ((π‘š ∈ β„‚ ∧ 𝑛 ∈ β„‚) β†’ (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) = (π‘š Β· 𝑛))
7571, 73, 74syl2anc 583 . . . . . . . 8 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) = (π‘š Β· 𝑛))
7669, 75eqeq12d 2742 . . . . . . 7 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) ↔ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛)))
7727adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 ∈ β„•)
7877nnnn0d 12536 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 ∈ β„•0)
79 simprll 776 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ 𝑋)
805, 79sselid 3975 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ β„•)
8180nnnn0d 12536 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ β„•0)
8277nnzd 12589 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 ∈ β„€)
8329adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 ∈ β„•)
8483nnzd 12589 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 ∈ β„€)
85 dvdsmul1 16228 . . . . . . . . . . . . 13 ((𝑖 ∈ β„€ ∧ 𝑗 ∈ β„€) β†’ 𝑖 βˆ₯ (𝑖 Β· 𝑗))
8682, 84, 85syl2anc 583 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 βˆ₯ (𝑖 Β· 𝑗))
87 simprr 770 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))
887, 79sselid 3975 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ β„‚)
89 simprlr 777 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 ∈ π‘Œ)
9010, 89sselid 3975 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 ∈ β„‚)
9188, 90mulcomd 11239 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š Β· 𝑛) = (𝑛 Β· π‘š))
9287, 91eqtrd 2766 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑗) = (𝑛 Β· π‘š))
9386, 92breqtrd 5167 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 βˆ₯ (𝑛 Β· π‘š))
949, 89sselid 3975 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 ∈ β„•)
9594nnzd 12589 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 ∈ β„€)
9642adantr 480 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑁 ∈ β„€)
9782, 96gcdcomd 16462 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
9848adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑀 ∈ β„€)
9940nnzd 12589 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑁 ∈ β„€)
10046nnzd 12589 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑀 ∈ β„€)
10199, 100gcdcomd 16462 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
102 mpodvdsmulf1o.3 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑀 gcd 𝑁) = 1)
103101, 102eqtrd 2766 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑁 gcd 𝑀) = 1)
104103ad2antrr 723 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑁 gcd 𝑀) = 1)
10538adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 βˆ₯ 𝑀)
106 rpdvds 16604 . . . . . . . . . . . . . 14 (((𝑁 ∈ β„€ ∧ 𝑖 ∈ β„€ ∧ 𝑀 ∈ β„€) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑖 βˆ₯ 𝑀)) β†’ (𝑁 gcd 𝑖) = 1)
10796, 82, 98, 104, 105, 106syl32anc 1375 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑁 gcd 𝑖) = 1)
10897, 107eqtrd 2766 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 gcd 𝑁) = 1)
109 breq1 5144 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑛 β†’ (π‘₯ βˆ₯ 𝑁 ↔ 𝑛 βˆ₯ 𝑁))
110109, 8elrab2 3681 . . . . . . . . . . . . . 14 (𝑛 ∈ π‘Œ ↔ (𝑛 ∈ β„• ∧ 𝑛 βˆ₯ 𝑁))
111110simprbi 496 . . . . . . . . . . . . 13 (𝑛 ∈ π‘Œ β†’ 𝑛 βˆ₯ 𝑁)
11289, 111syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑛 βˆ₯ 𝑁)
113 rpdvds 16604 . . . . . . . . . . . 12 (((𝑖 ∈ β„€ ∧ 𝑛 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ ((𝑖 gcd 𝑁) = 1 ∧ 𝑛 βˆ₯ 𝑁)) β†’ (𝑖 gcd 𝑛) = 1)
11482, 95, 96, 108, 112, 113syl32anc 1375 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 gcd 𝑛) = 1)
11580nnzd 12589 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š ∈ β„€)
116 coprmdvds 16597 . . . . . . . . . . . 12 ((𝑖 ∈ β„€ ∧ 𝑛 ∈ β„€ ∧ π‘š ∈ β„€) β†’ ((𝑖 βˆ₯ (𝑛 Β· π‘š) ∧ (𝑖 gcd 𝑛) = 1) β†’ 𝑖 βˆ₯ π‘š))
11782, 95, 115, 116syl3anc 1368 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ ((𝑖 βˆ₯ (𝑛 Β· π‘š) ∧ (𝑖 gcd 𝑛) = 1) β†’ 𝑖 βˆ₯ π‘š))
11893, 114, 117mp2and 696 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 βˆ₯ π‘š)
119 dvdsmul1 16228 . . . . . . . . . . . . 13 ((π‘š ∈ β„€ ∧ 𝑛 ∈ β„€) β†’ π‘š βˆ₯ (π‘š Β· 𝑛))
120115, 95, 119syl2anc 583 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š βˆ₯ (π‘š Β· 𝑛))
12177nncnd 12232 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 ∈ β„‚)
12283nncnd 12232 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 ∈ β„‚)
123121, 122mulcomd 11239 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑗) = (𝑗 Β· 𝑖))
12487, 123eqtr3d 2768 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š Β· 𝑛) = (𝑗 Β· 𝑖))
125120, 124breqtrd 5167 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š βˆ₯ (𝑗 Β· 𝑖))
126115, 96gcdcomd 16462 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š gcd 𝑁) = (𝑁 gcd π‘š))
127 breq1 5144 . . . . . . . . . . . . . . . . 17 (π‘₯ = π‘š β†’ (π‘₯ βˆ₯ 𝑀 ↔ π‘š βˆ₯ 𝑀))
128127, 4elrab2 3681 . . . . . . . . . . . . . . . 16 (π‘š ∈ 𝑋 ↔ (π‘š ∈ β„• ∧ π‘š βˆ₯ 𝑀))
129128simprbi 496 . . . . . . . . . . . . . . 15 (π‘š ∈ 𝑋 β†’ π‘š βˆ₯ 𝑀)
13079, 129syl 17 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š βˆ₯ 𝑀)
131 rpdvds 16604 . . . . . . . . . . . . . 14 (((𝑁 ∈ β„€ ∧ π‘š ∈ β„€ ∧ 𝑀 ∈ β„€) ∧ ((𝑁 gcd 𝑀) = 1 ∧ π‘š βˆ₯ 𝑀)) β†’ (𝑁 gcd π‘š) = 1)
13296, 115, 98, 104, 130, 131syl32anc 1375 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑁 gcd π‘š) = 1)
133126, 132eqtrd 2766 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š gcd 𝑁) = 1)
13434adantr 480 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 βˆ₯ 𝑁)
135 rpdvds 16604 . . . . . . . . . . . 12 (((π‘š ∈ β„€ ∧ 𝑗 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ ((π‘š gcd 𝑁) = 1 ∧ 𝑗 βˆ₯ 𝑁)) β†’ (π‘š gcd 𝑗) = 1)
136115, 84, 96, 133, 134, 135syl32anc 1375 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (π‘š gcd 𝑗) = 1)
137 coprmdvds 16597 . . . . . . . . . . . 12 ((π‘š ∈ β„€ ∧ 𝑗 ∈ β„€ ∧ 𝑖 ∈ β„€) β†’ ((π‘š βˆ₯ (𝑗 Β· 𝑖) ∧ (π‘š gcd 𝑗) = 1) β†’ π‘š βˆ₯ 𝑖))
138115, 84, 82, 137syl3anc 1368 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ ((π‘š βˆ₯ (𝑗 Β· 𝑖) ∧ (π‘š gcd 𝑗) = 1) β†’ π‘š βˆ₯ 𝑖))
139125, 136, 138mp2and 696 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ π‘š βˆ₯ 𝑖)
140 dvdseq 16264 . . . . . . . . . 10 (((𝑖 ∈ β„•0 ∧ π‘š ∈ β„•0) ∧ (𝑖 βˆ₯ π‘š ∧ π‘š βˆ₯ 𝑖)) β†’ 𝑖 = π‘š)
14178, 81, 118, 139, 140syl22anc 836 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 = π‘š)
14277nnne0d 12266 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑖 β‰  0)
143141oveq1d 7420 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑛) = (π‘š Β· 𝑛))
14487, 143eqtr4d 2769 . . . . . . . . . 10 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ (𝑖 Β· 𝑗) = (𝑖 Β· 𝑛))
145122, 90, 121, 142, 144mulcanad 11853 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ 𝑗 = 𝑛)
146141, 145opeq12d 4876 . . . . . . . 8 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ ((π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ) ∧ (𝑖 Β· 𝑗) = (π‘š Β· 𝑛))) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©)
147146expr 456 . . . . . . 7 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ ((𝑖 Β· 𝑗) = (π‘š Β· 𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
14876, 147sylbid 239 . . . . . 6 (((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) ∧ (π‘š ∈ 𝑋 ∧ 𝑛 ∈ π‘Œ)) β†’ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
149148ralrimivva 3194 . . . . 5 ((πœ‘ ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ π‘Œ)) β†’ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
150149ralrimivva 3194 . . . 4 (πœ‘ β†’ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
151 fvres 6904 . . . . . . . . 9 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’))
152 fvres 6904 . . . . . . . . 9 (𝑣 ∈ (𝑋 Γ— π‘Œ) β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£))
153151, 152eqeqan12d 2740 . . . . . . . 8 ((𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (𝑋 Γ— π‘Œ)) β†’ ((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) ↔ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£)))
154153imbi1d 341 . . . . . . 7 ((𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (𝑋 Γ— π‘Œ)) β†’ (((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣)))
155154ralbidva 3169 . . . . . 6 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣)))
156155ralbiia 3085 . . . . 5 (βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣))
157 fveq2 6885 . . . . . . . . . . 11 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨π‘š, π‘›βŸ©))
158 df-ov 7408 . . . . . . . . . . 11 (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨π‘š, π‘›βŸ©)
159157, 158eqtr4di 2784 . . . . . . . . . 10 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛))
160159eqeq2d 2737 . . . . . . . . 9 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) ↔ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛)))
161 eqeq2 2738 . . . . . . . . 9 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ (𝑒 = 𝑣 ↔ 𝑒 = βŸ¨π‘š, π‘›βŸ©))
162160, 161imbi12d 344 . . . . . . . 8 (𝑣 = βŸ¨π‘š, π‘›βŸ© β†’ ((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ 𝑒 = βŸ¨π‘š, π‘›βŸ©)))
163162ralxp 5835 . . . . . . 7 (βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ 𝑒 = βŸ¨π‘š, π‘›βŸ©))
164 fveq2 6885 . . . . . . . . . . 11 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨π‘–, π‘—βŸ©))
165 df-ov 7408 . . . . . . . . . . 11 (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨π‘–, π‘—βŸ©)
166164, 165eqtr4di 2784 . . . . . . . . . 10 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗))
167166eqeq1d 2728 . . . . . . . . 9 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) ↔ (𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛)))
168 eqeq1 2730 . . . . . . . . 9 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ (𝑒 = βŸ¨π‘š, π‘›βŸ© ↔ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
169167, 168imbi12d 344 . . . . . . . 8 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ ((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ 𝑒 = βŸ¨π‘š, π‘›βŸ©) ↔ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©)))
1701692ralbidv 3212 . . . . . . 7 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ (βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ 𝑒 = βŸ¨π‘š, π‘›βŸ©) ↔ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©)))
171163, 170bitrid 283 . . . . . 6 (𝑒 = βŸ¨π‘–, π‘—βŸ© β†’ (βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©)))
172171ralxp 5835 . . . . 5 (βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)(((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘’) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
173156, 172bitri 275 . . . 4 (βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣) ↔ βˆ€π‘– ∈ 𝑋 βˆ€π‘— ∈ π‘Œ βˆ€π‘š ∈ 𝑋 βˆ€π‘› ∈ π‘Œ ((𝑖(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑗) = (π‘š(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))𝑛) β†’ βŸ¨π‘–, π‘—βŸ© = βŸ¨π‘š, π‘›βŸ©))
174150, 173sylibr 233 . . 3 (πœ‘ β†’ βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣))
175 dff13 7250 . . 3 (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1→𝑍 ↔ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)βŸΆπ‘ ∧ βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)βˆ€π‘£ ∈ (𝑋 Γ— π‘Œ)((((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘£) β†’ 𝑒 = 𝑣)))
17666, 174, 175sylanbrc 582 . 2 (πœ‘ β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1→𝑍)
177 breq1 5144 . . . . . . . . . . . 12 (π‘₯ = 𝑀 β†’ (π‘₯ βˆ₯ (𝑀 Β· 𝑁) ↔ 𝑀 βˆ₯ (𝑀 Β· 𝑁)))
178177, 59elrab2 3681 . . . . . . . . . . 11 (𝑀 ∈ 𝑍 ↔ (𝑀 ∈ β„• ∧ 𝑀 βˆ₯ (𝑀 Β· 𝑁)))
179178simplbi 497 . . . . . . . . . 10 (𝑀 ∈ 𝑍 β†’ 𝑀 ∈ β„•)
180179adantl 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 ∈ β„•)
181180nnzd 12589 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 ∈ β„€)
18246adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 ∈ β„•)
183182nnzd 12589 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 ∈ β„€)
184182nnne0d 12266 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 β‰  0)
185 simpr 484 . . . . . . . . . 10 ((𝑀 = 0 ∧ 𝑀 = 0) β†’ 𝑀 = 0)
186185necon3ai 2959 . . . . . . . . 9 (𝑀 β‰  0 β†’ Β¬ (𝑀 = 0 ∧ 𝑀 = 0))
187184, 186syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ Β¬ (𝑀 = 0 ∧ 𝑀 = 0))
188 gcdn0cl 16450 . . . . . . . 8 (((𝑀 ∈ β„€ ∧ 𝑀 ∈ β„€) ∧ Β¬ (𝑀 = 0 ∧ 𝑀 = 0)) β†’ (𝑀 gcd 𝑀) ∈ β„•)
189181, 183, 187, 188syl21anc 835 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑀) ∈ β„•)
190 gcddvds 16451 . . . . . . . . 9 ((𝑀 ∈ β„€ ∧ 𝑀 ∈ β„€) β†’ ((𝑀 gcd 𝑀) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑀) βˆ₯ 𝑀))
191181, 183, 190syl2anc 583 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd 𝑀) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑀) βˆ₯ 𝑀))
192191simprd 495 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑀) βˆ₯ 𝑀)
193 breq1 5144 . . . . . . . 8 (π‘₯ = (𝑀 gcd 𝑀) β†’ (π‘₯ βˆ₯ 𝑀 ↔ (𝑀 gcd 𝑀) βˆ₯ 𝑀))
194193, 4elrab2 3681 . . . . . . 7 ((𝑀 gcd 𝑀) ∈ 𝑋 ↔ ((𝑀 gcd 𝑀) ∈ β„• ∧ (𝑀 gcd 𝑀) βˆ₯ 𝑀))
195189, 192, 194sylanbrc 582 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑀) ∈ 𝑋)
19640adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑁 ∈ β„•)
197196nnzd 12589 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑁 ∈ β„€)
198196nnne0d 12266 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑁 β‰  0)
199 simpr 484 . . . . . . . . . 10 ((𝑀 = 0 ∧ 𝑁 = 0) β†’ 𝑁 = 0)
200199necon3ai 2959 . . . . . . . . 9 (𝑁 β‰  0 β†’ Β¬ (𝑀 = 0 ∧ 𝑁 = 0))
201198, 200syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ Β¬ (𝑀 = 0 ∧ 𝑁 = 0))
202 gcdn0cl 16450 . . . . . . . 8 (((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ Β¬ (𝑀 = 0 ∧ 𝑁 = 0)) β†’ (𝑀 gcd 𝑁) ∈ β„•)
203181, 197, 201, 202syl21anc 835 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) ∈ β„•)
204 gcddvds 16451 . . . . . . . . 9 ((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ ((𝑀 gcd 𝑁) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
205181, 197, 204syl2anc 583 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd 𝑁) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
206205simprd 495 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) βˆ₯ 𝑁)
207 breq1 5144 . . . . . . . 8 (π‘₯ = (𝑀 gcd 𝑁) β†’ (π‘₯ βˆ₯ 𝑁 ↔ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
208207, 8elrab2 3681 . . . . . . 7 ((𝑀 gcd 𝑁) ∈ π‘Œ ↔ ((𝑀 gcd 𝑁) ∈ β„• ∧ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
209203, 206, 208sylanbrc 582 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) ∈ π‘Œ)
210195, 209opelxpd 5708 . . . . 5 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ⟨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩ ∈ (𝑋 Γ— π‘Œ))
211210fvresd 6905 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
212 df-ov 7408 . . . . . . . 8 ((𝑀 gcd 𝑀)(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))(𝑀 gcd 𝑁)) = ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩)
213189nncnd 12232 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑀) ∈ β„‚)
214203nncnd 12232 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) ∈ β„‚)
215 ovmpot 7565 . . . . . . . . 9 (((𝑀 gcd 𝑀) ∈ β„‚ ∧ (𝑀 gcd 𝑁) ∈ β„‚) β†’ ((𝑀 gcd 𝑀)(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))(𝑀 gcd 𝑁)) = ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)))
216213, 214, 215syl2anc 583 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd 𝑀)(π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))(𝑀 gcd 𝑁)) = ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)))
217212, 216eqtr3id 2780 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩) = ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)))
218 df-ov 7408 . . . . . . . 8 ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)) = ( Β· β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩)
219218a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)) = ( Β· β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
220211, 217, 2193eqtrd 2770 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩) = ( Β· β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
221102adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd 𝑁) = 1)
222 rpmulgcd2 16600 . . . . . . . 8 (((𝑀 ∈ β„€ ∧ 𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ (𝑀 gcd 𝑁) = 1) β†’ (𝑀 gcd (𝑀 Β· 𝑁)) = ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)))
223181, 183, 197, 221, 222syl31anc 1370 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd (𝑀 Β· 𝑁)) = ((𝑀 gcd 𝑀) Β· (𝑀 gcd 𝑁)))
224223, 218eqtrdi 2782 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd (𝑀 Β· 𝑁)) = ( Β· β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
225178simprbi 496 . . . . . . . 8 (𝑀 ∈ 𝑍 β†’ 𝑀 βˆ₯ (𝑀 Β· 𝑁))
226225adantl 481 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 βˆ₯ (𝑀 Β· 𝑁))
22746, 40nnmulcld 12269 . . . . . . . 8 (πœ‘ β†’ (𝑀 Β· 𝑁) ∈ β„•)
228 gcdeq 16502 . . . . . . . 8 ((𝑀 ∈ β„• ∧ (𝑀 Β· 𝑁) ∈ β„•) β†’ ((𝑀 gcd (𝑀 Β· 𝑁)) = 𝑀 ↔ 𝑀 βˆ₯ (𝑀 Β· 𝑁)))
229179, 227, 228syl2anr 596 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ ((𝑀 gcd (𝑀 Β· 𝑁)) = 𝑀 ↔ 𝑀 βˆ₯ (𝑀 Β· 𝑁)))
230226, 229mpbird 257 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ (𝑀 gcd (𝑀 Β· 𝑁)) = 𝑀)
231220, 224, 2303eqtr2rd 2773 . . . . 5 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ 𝑀 = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
232 fveq2 6885 . . . . . 6 (𝑒 = ⟨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩ β†’ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’) = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩))
233232rspceeqv 3628 . . . . 5 ((⟨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩ ∈ (𝑋 Γ— π‘Œ) ∧ 𝑀 = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜βŸ¨(𝑀 gcd 𝑀), (𝑀 gcd 𝑁)⟩)) β†’ βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)𝑀 = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’))
234210, 231, 233syl2anc 583 . . . 4 ((πœ‘ ∧ 𝑀 ∈ 𝑍) β†’ βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)𝑀 = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’))
235234ralrimiva 3140 . . 3 (πœ‘ β†’ βˆ€π‘€ ∈ 𝑍 βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)𝑀 = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’))
236 dffo3 7097 . . 3 (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–onto→𝑍 ↔ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)βŸΆπ‘ ∧ βˆ€π‘€ ∈ 𝑍 βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)𝑀 = (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ))β€˜π‘’)))
23766, 235, 236sylanbrc 582 . 2 (πœ‘ β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–onto→𝑍)
238 df-f1o 6544 . 2 (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1-onto→𝑍 ↔ (((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1→𝑍 ∧ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–onto→𝑍))
239176, 237, 238sylanbrc 582 1 (πœ‘ β†’ ((π‘₯ ∈ β„‚, 𝑦 ∈ β„‚ ↦ (π‘₯ Β· 𝑦)) β†Ύ (𝑋 Γ— π‘Œ)):(𝑋 Γ— π‘Œ)–1-1-onto→𝑍)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098   β‰  wne 2934  βˆ€wral 3055  βˆƒwrex 3064  {crab 3426   βŠ† wss 3943  βŸ¨cop 4629   class class class wbr 5141   Γ— cxp 5667   β†Ύ cres 5671   Fn wfn 6532  βŸΆwf 6533  β€“1-1β†’wf1 6534  β€“ontoβ†’wfo 6535  β€“1-1-ontoβ†’wf1o 6536  β€˜cfv 6537  (class class class)co 7405   ∈ cmpo 7407  β„‚cc 11110  0cc0 11112  1c1 11113   Β· cmul 11117  β„•cn 12216  β„•0cn0 12476  β„€cz 12562   βˆ₯ cdvds 16204   gcd cgcd 16442
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 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  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 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-rp 12981  df-fl 13763  df-mod 13841  df-seq 13973  df-exp 14033  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-dvds 16205  df-gcd 16443
This theorem is referenced by:  fsumdvdsmul  27082
  Copyright terms: Public domain W3C validator