Metamath Proof Explorer

Theorem mpodvdsmulf1o

Description: If M and N are two coprime integers, multiplication forms a bijection from the set of pairs <. j , k >. where j || M and k || N , to the set of divisors of M x. N . Version of dvdsmulf1o using maps-to notation, which does not require ax-mulf . (Contributed by GG, 18-Apr-2025)

Ref Expression
Hypotheses mpodvdsmulf1o.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
mpodvdsmulf1o.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
mpodvdsmulf1o.3 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
mpodvdsmulf1o.x ⊢ 𝑋 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 }
mpodvdsmulf1o.y ⊢ 𝑌 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
mpodvdsmulf1o.z ⊢ 𝑍 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) }
Assertion mpodvdsmulf1o ( 𝜑 → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1-onto→ 𝑍 )

Proof

Step Hyp Ref Expression
1 mpodvdsmulf1o.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 mpodvdsmulf1o.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 mpodvdsmulf1o.3 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
4 mpodvdsmulf1o.x ⊢ 𝑋 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 }
5 mpodvdsmulf1o.y ⊢ 𝑌 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
6 mpodvdsmulf1o.z ⊢ 𝑍 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) }
7 mpomulf ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ
8 ffn ⊢ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) Fn ( ℂ × ℂ ) )
9 7 8 ax-mp ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) Fn ( ℂ × ℂ )
10 4 ssrab3 ⊢ 𝑋 ⊆ ℕ
11 nnsscn ⊢ ℕ ⊆ ℂ
12 10 11 sstri ⊢ 𝑋 ⊆ ℂ
13 5 ssrab3 ⊢ 𝑌 ⊆ ℕ
14 13 11 sstri ⊢ 𝑌 ⊆ ℂ
15 xpss12 ⊢ ( ( 𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ ) → ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ ) )
16 12 14 15 mp2an ⊢ ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ )
17 fnssres ⊢ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) Fn ( ℂ × ℂ ) ∧ ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ ) ) → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) )
18 9 16 17 mp2an ⊢ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 )
19 18 a1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) )
20 ovres ⊢ ( ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) 𝑗 ) = ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑖 ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) 𝑗 ) = ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) )
22 12 sseli ⊢ ( 𝑖 ∈ 𝑋 → 𝑖 ∈ ℂ )
23 22 adantr ⊢ ( ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) → 𝑖 ∈ ℂ )
24 14 sseli ⊢ ( 𝑗 ∈ 𝑌 → 𝑗 ∈ ℂ )
25 24 adantl ⊢ ( ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) → 𝑗 ∈ ℂ )
26 ovmpot ⊢ ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( 𝑖 · 𝑗 ) )
27 26 eqcomd ⊢ ( ( 𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝑖 · 𝑗 ) = ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) )
28 23 25 27 syl2anc ⊢ ( ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 · 𝑗 ) = ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) )
29 28 adantl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑖 · 𝑗 ) = ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) )
30 10 sseli ⊢ ( 𝑖 ∈ 𝑋 → 𝑖 ∈ ℕ )
31 30 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → 𝑖 ∈ ℕ )
32 13 sseli ⊢ ( 𝑗 ∈ 𝑌 → 𝑗 ∈ ℕ )
33 32 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → 𝑗 ∈ ℕ )
34 31 33 nnmulcld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑖 · 𝑗 ) ∈ ℕ )
35 breq1 ⊢ ( 𝑥 = 𝑗 → ( 𝑥 ∥ 𝑁 ↔ 𝑗 ∥ 𝑁 ) )
36 35 5 elrab2 ⊢ ( 𝑗 ∈ 𝑌 ↔ ( 𝑗 ∈ ℕ ∧ 𝑗 ∥ 𝑁 ) )
37 36 simprbi ⊢ ( 𝑗 ∈ 𝑌 → 𝑗 ∥ 𝑁 )
38 37 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → 𝑗 ∥ 𝑁 )
39 breq1 ⊢ ( 𝑥 = 𝑖 → ( 𝑥 ∥ 𝑀 ↔ 𝑖 ∥ 𝑀 ) )
40 39 4 elrab2 ⊢ ( 𝑖 ∈ 𝑋 ↔ ( 𝑖 ∈ ℕ ∧ 𝑖 ∥ 𝑀 ) )
41 40 simprbi ⊢ ( 𝑖 ∈ 𝑋 → 𝑖 ∥ 𝑀 )
42 41 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → 𝑖 ∥ 𝑀 )
43 33 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → 𝑗 ∈ ℤ )
44 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → 𝑁 ∈ ℕ )
45 44 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → 𝑁 ∈ ℤ )
46 31 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → 𝑖 ∈ ℤ )
47 dvdscmul ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑗 ∥ 𝑁 → ( 𝑖 · 𝑗 ) ∥ ( 𝑖 · 𝑁 ) ) )
48 43 45 46 47 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑗 ∥ 𝑁 → ( 𝑖 · 𝑗 ) ∥ ( 𝑖 · 𝑁 ) ) )
49 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → 𝑀 ∈ ℕ )
50 49 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → 𝑀 ∈ ℤ )
51 dvdsmulc ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑖 ∥ 𝑀 → ( 𝑖 · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) )
52 46 50 45 51 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑖 ∥ 𝑀 → ( 𝑖 · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) )
53 34 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑖 · 𝑗 ) ∈ ℤ )
54 46 45 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑖 · 𝑁 ) ∈ ℤ )
55 50 45 zmulcld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
56 dvdstr ⊢ ( ( ( 𝑖 · 𝑗 ) ∈ ℤ ∧ ( 𝑖 · 𝑁 ) ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( ( 𝑖 · 𝑗 ) ∥ ( 𝑖 · 𝑁 ) ∧ ( 𝑖 · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) → ( 𝑖 · 𝑗 ) ∥ ( 𝑀 · 𝑁 ) ) )
57 53 54 55 56 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( ( ( 𝑖 · 𝑗 ) ∥ ( 𝑖 · 𝑁 ) ∧ ( 𝑖 · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) → ( 𝑖 · 𝑗 ) ∥ ( 𝑀 · 𝑁 ) ) )
58 48 52 57 syl2and ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( ( 𝑗 ∥ 𝑁 ∧ 𝑖 ∥ 𝑀 ) → ( 𝑖 · 𝑗 ) ∥ ( 𝑀 · 𝑁 ) ) )
59 38 42 58 mp2and ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑖 · 𝑗 ) ∥ ( 𝑀 · 𝑁 ) )
60 breq1 ⊢ ( 𝑥 = ( 𝑖 · 𝑗 ) → ( 𝑥 ∥ ( 𝑀 · 𝑁 ) ↔ ( 𝑖 · 𝑗 ) ∥ ( 𝑀 · 𝑁 ) ) )
61 60 6 elrab2 ⊢ ( ( 𝑖 · 𝑗 ) ∈ 𝑍 ↔ ( ( 𝑖 · 𝑗 ) ∈ ℕ ∧ ( 𝑖 · 𝑗 ) ∥ ( 𝑀 · 𝑁 ) ) )
62 34 59 61 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑖 · 𝑗 ) ∈ 𝑍 )
63 29 62 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) ∈ 𝑍 )
64 21 63 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑖 ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) 𝑗 ) ∈ 𝑍 )
65 64 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑌 ( 𝑖 ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) 𝑗 ) ∈ 𝑍 )
66 ffnov ⊢ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ↔ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) ∧ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑌 ( 𝑖 ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) 𝑗 ) ∈ 𝑍 ) )
67 19 65 66 sylanbrc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 )
68 23 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ) → 𝑖 ∈ ℂ )
69 25 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ) → 𝑗 ∈ ℂ )
70 68 69 26 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ) → ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( 𝑖 · 𝑗 ) )
71 12 sseli ⊢ ( 𝑚 ∈ 𝑋 → 𝑚 ∈ ℂ )
72 71 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ) → 𝑚 ∈ ℂ )
73 14 sseli ⊢ ( 𝑛 ∈ 𝑌 → 𝑛 ∈ ℂ )
74 73 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ) → 𝑛 ∈ ℂ )
75 ovmpot ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) = ( 𝑚 · 𝑛 ) )
76 72 74 75 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ) → ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) = ( 𝑚 · 𝑛 ) )
77 70 76 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ) → ( ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) ↔ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) )
78 31 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∈ ℕ )
79 78 nnnn0d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∈ ℕ0 )
80 simprll ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∈ 𝑋 )
81 10 80 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∈ ℕ )
82 81 nnnn0d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∈ ℕ0 )
83 78 nnzd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∈ ℤ )
84 33 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑗 ∈ ℕ )
85 84 nnzd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑗 ∈ ℤ )
86 dvdsmul1 ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → 𝑖 ∥ ( 𝑖 · 𝑗 ) )
87 83 85 86 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∥ ( 𝑖 · 𝑗 ) )
88 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) )
89 12 80 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∈ ℂ )
90 simprlr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑛 ∈ 𝑌 )
91 14 90 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑛 ∈ ℂ )
92 89 91 mulcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑚 · 𝑛 ) = ( 𝑛 · 𝑚 ) )
93 88 92 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 · 𝑗 ) = ( 𝑛 · 𝑚 ) )
94 87 93 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∥ ( 𝑛 · 𝑚 ) )
95 13 90 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑛 ∈ ℕ )
96 95 nnzd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑛 ∈ ℤ )
97 45 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑁 ∈ ℤ )
98 83 97 gcdcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 gcd 𝑁 ) = ( 𝑁 gcd 𝑖 ) )
99 50 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑀 ∈ ℤ )
100 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
101 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
102 100 101 gcdcomd ⊢ ( 𝜑 → ( 𝑁 gcd 𝑀 ) = ( 𝑀 gcd 𝑁 ) )
103 102 3 eqtrd ⊢ ( 𝜑 → ( 𝑁 gcd 𝑀 ) = 1 )
104 103 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑁 gcd 𝑀 ) = 1 )
105 42 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∥ 𝑀 )
106 rpdvds ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( ( 𝑁 gcd 𝑀 ) = 1 ∧ 𝑖 ∥ 𝑀 ) ) → ( 𝑁 gcd 𝑖 ) = 1 )
107 97 83 99 104 105 106 syl32anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑁 gcd 𝑖 ) = 1 )
108 98 107 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 gcd 𝑁 ) = 1 )
109 breq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∥ 𝑁 ↔ 𝑛 ∥ 𝑁 ) )
110 109 5 elrab2 ⊢ ( 𝑛 ∈ 𝑌 ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝑁 ) )
111 110 simprbi ⊢ ( 𝑛 ∈ 𝑌 → 𝑛 ∥ 𝑁 )
112 90 111 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑛 ∥ 𝑁 )
113 rpdvds ⊢ ( ( ( 𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑖 gcd 𝑁 ) = 1 ∧ 𝑛 ∥ 𝑁 ) ) → ( 𝑖 gcd 𝑛 ) = 1 )
114 83 96 97 108 112 113 syl32anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 gcd 𝑛 ) = 1 )
115 81 nnzd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∈ ℤ )
116 coprmdvds ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( 𝑖 ∥ ( 𝑛 · 𝑚 ) ∧ ( 𝑖 gcd 𝑛 ) = 1 ) → 𝑖 ∥ 𝑚 ) )
117 83 96 115 116 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( ( 𝑖 ∥ ( 𝑛 · 𝑚 ) ∧ ( 𝑖 gcd 𝑛 ) = 1 ) → 𝑖 ∥ 𝑚 ) )
118 94 114 117 mp2and ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∥ 𝑚 )
119 dvdsmul1 ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑚 ∥ ( 𝑚 · 𝑛 ) )
120 115 96 119 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∥ ( 𝑚 · 𝑛 ) )
121 78 nncnd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∈ ℂ )
122 84 nncnd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑗 ∈ ℂ )
123 121 122 mulcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 · 𝑗 ) = ( 𝑗 · 𝑖 ) )
124 88 123 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑚 · 𝑛 ) = ( 𝑗 · 𝑖 ) )
125 120 124 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∥ ( 𝑗 · 𝑖 ) )
126 115 97 gcdcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑚 gcd 𝑁 ) = ( 𝑁 gcd 𝑚 ) )
127 breq1 ⊢ ( 𝑥 = 𝑚 → ( 𝑥 ∥ 𝑀 ↔ 𝑚 ∥ 𝑀 ) )
128 127 4 elrab2 ⊢ ( 𝑚 ∈ 𝑋 ↔ ( 𝑚 ∈ ℕ ∧ 𝑚 ∥ 𝑀 ) )
129 128 simprbi ⊢ ( 𝑚 ∈ 𝑋 → 𝑚 ∥ 𝑀 )
130 80 129 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∥ 𝑀 )
131 rpdvds ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( ( 𝑁 gcd 𝑀 ) = 1 ∧ 𝑚 ∥ 𝑀 ) ) → ( 𝑁 gcd 𝑚 ) = 1 )
132 97 115 99 104 130 131 syl32anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑁 gcd 𝑚 ) = 1 )
133 126 132 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑚 gcd 𝑁 ) = 1 )
134 38 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑗 ∥ 𝑁 )
135 rpdvds ⊢ ( ( ( 𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑚 gcd 𝑁 ) = 1 ∧ 𝑗 ∥ 𝑁 ) ) → ( 𝑚 gcd 𝑗 ) = 1 )
136 115 85 97 133 134 135 syl32anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑚 gcd 𝑗 ) = 1 )
137 coprmdvds ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( 𝑚 ∥ ( 𝑗 · 𝑖 ) ∧ ( 𝑚 gcd 𝑗 ) = 1 ) → 𝑚 ∥ 𝑖 ) )
138 115 85 83 137 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( ( 𝑚 ∥ ( 𝑗 · 𝑖 ) ∧ ( 𝑚 gcd 𝑗 ) = 1 ) → 𝑚 ∥ 𝑖 ) )
139 125 136 138 mp2and ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∥ 𝑖 )
140 dvdseq ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑖 ∥ 𝑚 ∧ 𝑚 ∥ 𝑖 ) ) → 𝑖 = 𝑚 )
141 79 82 118 139 140 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 = 𝑚 )
142 78 nnne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ≠ 0 )
143 141 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 · 𝑛 ) = ( 𝑚 · 𝑛 ) )
144 88 143 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 · 𝑗 ) = ( 𝑖 · 𝑛 ) )
145 122 91 121 142 144 mulcanad ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑗 = 𝑛 )
146 141 145 opeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ )
147 146 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ) → ( ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
148 77 147 sylbid ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) ∧ ( 𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌 ) ) → ( ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
149 148 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌 ) ) → ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑌 ( ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
150 149 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑌 ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑌 ( ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
151 fvres ⊢ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) → ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) )
152 fvres ⊢ ( 𝑣 ∈ ( 𝑋 × 𝑌 ) → ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑣 ) )
153 151 152 eqeqan12d ⊢ ( ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) ↔ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑣 ) ) )
154 153 imbi1d ⊢ ( ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ) )
155 154 ralbidva ⊢ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) → ( ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ) )
156 155 ralbiia ⊢ ( ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
157 fveq2 ⊢ ( 𝑣 = ⟨ 𝑚 , 𝑛 ⟩ → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑣 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑚 , 𝑛 ⟩ ) )
158 df-ov ⊢ ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑚 , 𝑛 ⟩ )
159 157 158 eqtr4di ⊢ ( 𝑣 = ⟨ 𝑚 , 𝑛 ⟩ → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑣 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) )
160 159 eqeq2d ⊢ ( 𝑣 = ⟨ 𝑚 , 𝑛 ⟩ → ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑣 ) ↔ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) ) )
161 eqeq2 ⊢ ( 𝑣 = ⟨ 𝑚 , 𝑛 ⟩ → ( 𝑢 = 𝑣 ↔ 𝑢 = ⟨ 𝑚 , 𝑛 ⟩ ) )
162 160 161 imbi12d ⊢ ( 𝑣 = ⟨ 𝑚 , 𝑛 ⟩ → ( ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) → 𝑢 = ⟨ 𝑚 , 𝑛 ⟩ ) ) )
163 162 ralxp ⊢ ( ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑌 ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) → 𝑢 = ⟨ 𝑚 , 𝑛 ⟩ ) )
164 fveq2 ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑖 , 𝑗 ⟩ ) )
165 df-ov ⊢ ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑖 , 𝑗 ⟩ )
166 164 165 eqtr4di ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) )
167 166 eqeq1d ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) ↔ ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) ) )
168 eqeq1 ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑢 = ⟨ 𝑚 , 𝑛 ⟩ ↔ ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
169 167 168 imbi12d ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) → 𝑢 = ⟨ 𝑚 , 𝑛 ⟩ ) ↔ ( ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) ) )
170 169 2ralbidv ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑌 ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) → 𝑢 = ⟨ 𝑚 , 𝑛 ⟩ ) ↔ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑌 ( ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) ) )
171 163 170 bitrid ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑌 ( ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) ) )
172 171 ralxp ⊢ ( ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑌 ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑌 ( ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
173 156 172 bitri ⊢ ( ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑖 ∈ 𝑋 ∀ 𝑗 ∈ 𝑌 ∀ 𝑚 ∈ 𝑋 ∀ 𝑛 ∈ 𝑌 ( ( 𝑖 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑗 ) = ( 𝑚 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
174 150 173 sylibr ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
175 dff13 ⊢ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1→ 𝑍 ↔ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ) )
176 67 174 175 sylanbrc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1→ 𝑍 )
177 breq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∥ ( 𝑀 · 𝑁 ) ↔ 𝑤 ∥ ( 𝑀 · 𝑁 ) ) )
178 177 6 elrab2 ⊢ ( 𝑤 ∈ 𝑍 ↔ ( 𝑤 ∈ ℕ ∧ 𝑤 ∥ ( 𝑀 · 𝑁 ) ) )
179 178 simplbi ⊢ ( 𝑤 ∈ 𝑍 → 𝑤 ∈ ℕ )
180 179 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑤 ∈ ℕ )
181 180 nnzd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑤 ∈ ℤ )
182 1 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑀 ∈ ℕ )
183 182 nnzd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑀 ∈ ℤ )
184 182 nnne0d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑀 ≠ 0 )
185 simpr ⊢ ( ( 𝑤 = 0 ∧ 𝑀 = 0 ) → 𝑀 = 0 )
186 185 necon3ai ⊢ ( 𝑀 ≠ 0 → ¬ ( 𝑤 = 0 ∧ 𝑀 = 0 ) )
187 184 186 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ¬ ( 𝑤 = 0 ∧ 𝑀 = 0 ) )
188 gcdn0cl ⊢ ( ( ( 𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ¬ ( 𝑤 = 0 ∧ 𝑀 = 0 ) ) → ( 𝑤 gcd 𝑀 ) ∈ ℕ )
189 181 183 187 188 syl21anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 gcd 𝑀 ) ∈ ℕ )
190 gcddvds ⊢ ( ( 𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑤 gcd 𝑀 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑀 ) ∥ 𝑀 ) )
191 181 183 190 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( ( 𝑤 gcd 𝑀 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑀 ) ∥ 𝑀 ) )
192 191 simprd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 gcd 𝑀 ) ∥ 𝑀 )
193 breq1 ⊢ ( 𝑥 = ( 𝑤 gcd 𝑀 ) → ( 𝑥 ∥ 𝑀 ↔ ( 𝑤 gcd 𝑀 ) ∥ 𝑀 ) )
194 193 4 elrab2 ⊢ ( ( 𝑤 gcd 𝑀 ) ∈ 𝑋 ↔ ( ( 𝑤 gcd 𝑀 ) ∈ ℕ ∧ ( 𝑤 gcd 𝑀 ) ∥ 𝑀 ) )
195 189 192 194 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 gcd 𝑀 ) ∈ 𝑋 )
196 2 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑁 ∈ ℕ )
197 196 nnzd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑁 ∈ ℤ )
198 196 nnne0d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑁 ≠ 0 )
199 simpr ⊢ ( ( 𝑤 = 0 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
200 199 necon3ai ⊢ ( 𝑁 ≠ 0 → ¬ ( 𝑤 = 0 ∧ 𝑁 = 0 ) )
201 198 200 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ¬ ( 𝑤 = 0 ∧ 𝑁 = 0 ) )
202 gcdn0cl ⊢ ( ( ( 𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑤 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑤 gcd 𝑁 ) ∈ ℕ )
203 181 197 201 202 syl21anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 gcd 𝑁 ) ∈ ℕ )
204 gcddvds ⊢ ( ( 𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑤 gcd 𝑁 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑁 ) ∥ 𝑁 ) )
205 181 197 204 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( ( 𝑤 gcd 𝑁 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑁 ) ∥ 𝑁 ) )
206 205 simprd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 gcd 𝑁 ) ∥ 𝑁 )
207 breq1 ⊢ ( 𝑥 = ( 𝑤 gcd 𝑁 ) → ( 𝑥 ∥ 𝑁 ↔ ( 𝑤 gcd 𝑁 ) ∥ 𝑁 ) )
208 207 5 elrab2 ⊢ ( ( 𝑤 gcd 𝑁 ) ∈ 𝑌 ↔ ( ( 𝑤 gcd 𝑁 ) ∈ ℕ ∧ ( 𝑤 gcd 𝑁 ) ∥ 𝑁 ) )
209 203 206 208 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 gcd 𝑁 ) ∈ 𝑌 )
210 195 209 opelxpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
211 210 fvresd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) )
212 df-ov ⊢ ( ( 𝑤 gcd 𝑀 ) ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ( 𝑤 gcd 𝑁 ) ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ )
213 189 nncnd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 gcd 𝑀 ) ∈ ℂ )
214 203 nncnd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 gcd 𝑁 ) ∈ ℂ )
215 ovmpot ⊢ ( ( ( 𝑤 gcd 𝑀 ) ∈ ℂ ∧ ( 𝑤 gcd 𝑁 ) ∈ ℂ ) → ( ( 𝑤 gcd 𝑀 ) ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ( 𝑤 gcd 𝑁 ) ) = ( ( 𝑤 gcd 𝑀 ) · ( 𝑤 gcd 𝑁 ) ) )
216 213 214 215 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( ( 𝑤 gcd 𝑀 ) ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ( 𝑤 gcd 𝑁 ) ) = ( ( 𝑤 gcd 𝑀 ) · ( 𝑤 gcd 𝑁 ) ) )
217 212 216 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) = ( ( 𝑤 gcd 𝑀 ) · ( 𝑤 gcd 𝑁 ) ) )
218 df-ov ⊢ ( ( 𝑤 gcd 𝑀 ) · ( 𝑤 gcd 𝑁 ) ) = ( · ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ )
219 218 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( ( 𝑤 gcd 𝑀 ) · ( 𝑤 gcd 𝑁 ) ) = ( · ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) )
220 211 217 219 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) = ( · ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) )
221 3 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑀 gcd 𝑁 ) = 1 )
222 rpmulgcd2 ⊢ ( ( ( 𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = ( ( 𝑤 gcd 𝑀 ) · ( 𝑤 gcd 𝑁 ) ) )
223 181 183 197 221 222 syl31anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = ( ( 𝑤 gcd 𝑀 ) · ( 𝑤 gcd 𝑁 ) ) )
224 223 218 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = ( · ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) )
225 178 simprbi ⊢ ( 𝑤 ∈ 𝑍 → 𝑤 ∥ ( 𝑀 · 𝑁 ) )
226 225 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑤 ∥ ( 𝑀 · 𝑁 ) )
227 1 2 nnmulcld ⊢ ( 𝜑 → ( 𝑀 · 𝑁 ) ∈ ℕ )
228 gcdeq ⊢ ( ( 𝑤 ∈ ℕ ∧ ( 𝑀 · 𝑁 ) ∈ ℕ ) → ( ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = 𝑤 ↔ 𝑤 ∥ ( 𝑀 · 𝑁 ) ) )
229 179 227 228 syl2anr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = 𝑤 ↔ 𝑤 ∥ ( 𝑀 · 𝑁 ) ) )
230 226 229 mpbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = 𝑤 )
231 220 224 230 3eqtr2rd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑤 = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) )
232 fveq2 ⊢ ( 𝑢 = ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ → ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) )
233 232 rspceeqv ⊢ ( ( ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ 𝑤 = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) ) → ∃ 𝑢 ∈ ( 𝑋 × 𝑌 ) 𝑤 = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) )
234 210 231 233 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ∃ 𝑢 ∈ ( 𝑋 × 𝑌 ) 𝑤 = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) )
235 234 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑍 ∃ 𝑢 ∈ ( 𝑋 × 𝑌 ) 𝑤 = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) )
236 dffo3 ⊢ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑍 ↔ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑤 ∈ 𝑍 ∃ 𝑢 ∈ ( 𝑋 × 𝑌 ) 𝑤 = ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) ) )
237 67 235 236 sylanbrc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑍 )
238 df-f1o ⊢ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1-onto→ 𝑍 ↔ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1→ 𝑍 ∧ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑍 ) )
239 176 237 238 sylanbrc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1-onto→ 𝑍 )