Metamath Proof Explorer


Theorem rmxypairf1o

Description: The function used to extract rational and irrational parts in df-rmx and df-rmy in fact achieves a one-to-one mapping from the quadratic irrationals to pairs of integers. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion rmxypairf1o ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) : ( ℕ0 × ℤ ) –1-1-onto→ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )

Proof

Step Hyp Ref Expression
1 ovex ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ∈ V
2 eqid ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) = ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) )
3 1 2 fnmpti ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) Fn ( ℕ0 × ℤ )
4 3 a1i ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) Fn ( ℕ0 × ℤ ) )
5 vex 𝑐 ∈ V
6 vex 𝑑 ∈ V
7 5 6 op1std ( 𝑏 = ⟨ 𝑐 , 𝑑 ⟩ → ( 1st𝑏 ) = 𝑐 )
8 5 6 op2ndd ( 𝑏 = ⟨ 𝑐 , 𝑑 ⟩ → ( 2nd𝑏 ) = 𝑑 )
9 8 oveq2d ( 𝑏 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) )
10 7 9 oveq12d ( 𝑏 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) )
11 10 eqeq2d ( 𝑏 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑎 = ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ↔ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ) )
12 11 rexxp ( ∃ 𝑏 ∈ ( ℕ0 × ℤ ) 𝑎 = ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ↔ ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) )
13 12 bicomi ( ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ↔ ∃ 𝑏 ∈ ( ℕ0 × ℤ ) 𝑎 = ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) )
14 13 a1i ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ↔ ∃ 𝑏 ∈ ( ℕ0 × ℤ ) 𝑎 = ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) )
15 14 abbidv ( 𝐴 ∈ ( ℤ ‘ 2 ) → { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } = { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 × ℤ ) 𝑎 = ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) } )
16 2 rnmpt ran ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) = { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 × ℤ ) 𝑎 = ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) }
17 15 16 syl6reqr ( 𝐴 ∈ ( ℤ ‘ 2 ) → ran ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) = { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
18 fveq2 ( 𝑏 = 𝑐 → ( 1st𝑏 ) = ( 1st𝑐 ) )
19 fveq2 ( 𝑏 = 𝑐 → ( 2nd𝑏 ) = ( 2nd𝑐 ) )
20 19 oveq2d ( 𝑏 = 𝑐 → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑐 ) ) )
21 18 20 oveq12d ( 𝑏 = 𝑐 → ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) = ( ( 1st𝑐 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑐 ) ) ) )
22 ovex ( ( 1st𝑐 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑐 ) ) ) ∈ V
23 21 2 22 fvmpt ( 𝑐 ∈ ( ℕ0 × ℤ ) → ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ 𝑐 ) = ( ( 1st𝑐 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑐 ) ) ) )
24 23 ad2antrl ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ 𝑐 ) = ( ( 1st𝑐 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑐 ) ) ) )
25 fveq2 ( 𝑏 = 𝑑 → ( 1st𝑏 ) = ( 1st𝑑 ) )
26 fveq2 ( 𝑏 = 𝑑 → ( 2nd𝑏 ) = ( 2nd𝑑 ) )
27 26 oveq2d ( 𝑏 = 𝑑 → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑑 ) ) )
28 25 27 oveq12d ( 𝑏 = 𝑑 → ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) = ( ( 1st𝑑 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑑 ) ) ) )
29 ovex ( ( 1st𝑑 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑑 ) ) ) ∈ V
30 28 2 29 fvmpt ( 𝑑 ∈ ( ℕ0 × ℤ ) → ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ 𝑑 ) = ( ( 1st𝑑 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑑 ) ) ) )
31 30 ad2antll ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ 𝑑 ) = ( ( 1st𝑑 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑑 ) ) ) )
32 24 31 eqeq12d ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ 𝑐 ) = ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ 𝑑 ) ↔ ( ( 1st𝑐 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑐 ) ) ) = ( ( 1st𝑑 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑑 ) ) ) ) )
33 rmspecsqrtnq ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) )
34 33 adantr ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) )
35 nn0ssq 0 ⊆ ℚ
36 xp1st ( 𝑐 ∈ ( ℕ0 × ℤ ) → ( 1st𝑐 ) ∈ ℕ0 )
37 36 ad2antrl ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( 1st𝑐 ) ∈ ℕ0 )
38 35 37 sseldi ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( 1st𝑐 ) ∈ ℚ )
39 xp2nd ( 𝑐 ∈ ( ℕ0 × ℤ ) → ( 2nd𝑐 ) ∈ ℤ )
40 39 ad2antrl ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( 2nd𝑐 ) ∈ ℤ )
41 zq ( ( 2nd𝑐 ) ∈ ℤ → ( 2nd𝑐 ) ∈ ℚ )
42 40 41 syl ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( 2nd𝑐 ) ∈ ℚ )
43 xp1st ( 𝑑 ∈ ( ℕ0 × ℤ ) → ( 1st𝑑 ) ∈ ℕ0 )
44 43 ad2antll ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( 1st𝑑 ) ∈ ℕ0 )
45 35 44 sseldi ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( 1st𝑑 ) ∈ ℚ )
46 xp2nd ( 𝑑 ∈ ( ℕ0 × ℤ ) → ( 2nd𝑑 ) ∈ ℤ )
47 46 ad2antll ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( 2nd𝑑 ) ∈ ℤ )
48 zq ( ( 2nd𝑑 ) ∈ ℤ → ( 2nd𝑑 ) ∈ ℚ )
49 47 48 syl ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( 2nd𝑑 ) ∈ ℚ )
50 qirropth ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) ∧ ( ( 1st𝑐 ) ∈ ℚ ∧ ( 2nd𝑐 ) ∈ ℚ ) ∧ ( ( 1st𝑑 ) ∈ ℚ ∧ ( 2nd𝑑 ) ∈ ℚ ) ) → ( ( ( 1st𝑐 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑐 ) ) ) = ( ( 1st𝑑 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑑 ) ) ) ↔ ( ( 1st𝑐 ) = ( 1st𝑑 ) ∧ ( 2nd𝑐 ) = ( 2nd𝑑 ) ) ) )
51 34 38 42 45 49 50 syl122anc ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( ( ( 1st𝑐 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑐 ) ) ) = ( ( 1st𝑑 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑑 ) ) ) ↔ ( ( 1st𝑐 ) = ( 1st𝑑 ) ∧ ( 2nd𝑐 ) = ( 2nd𝑑 ) ) ) )
52 51 biimpd ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( ( ( 1st𝑐 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑐 ) ) ) = ( ( 1st𝑑 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑑 ) ) ) → ( ( 1st𝑐 ) = ( 1st𝑑 ) ∧ ( 2nd𝑐 ) = ( 2nd𝑑 ) ) ) )
53 xpopth ( ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) → ( ( ( 1st𝑐 ) = ( 1st𝑑 ) ∧ ( 2nd𝑐 ) = ( 2nd𝑑 ) ) ↔ 𝑐 = 𝑑 ) )
54 53 adantl ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( ( ( 1st𝑐 ) = ( 1st𝑑 ) ∧ ( 2nd𝑐 ) = ( 2nd𝑑 ) ) ↔ 𝑐 = 𝑑 ) )
55 52 54 sylibd ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( ( ( 1st𝑐 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑐 ) ) ) = ( ( 1st𝑑 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑑 ) ) ) → 𝑐 = 𝑑 ) )
56 32 55 sylbid ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑐 ∈ ( ℕ0 × ℤ ) ∧ 𝑑 ∈ ( ℕ0 × ℤ ) ) ) → ( ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ 𝑐 ) = ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ 𝑑 ) → 𝑐 = 𝑑 ) )
57 56 ralrimivva ( 𝐴 ∈ ( ℤ ‘ 2 ) → ∀ 𝑐 ∈ ( ℕ0 × ℤ ) ∀ 𝑑 ∈ ( ℕ0 × ℤ ) ( ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ 𝑐 ) = ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ 𝑑 ) → 𝑐 = 𝑑 ) )
58 dff1o6 ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) : ( ℕ0 × ℤ ) –1-1-onto→ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } ↔ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) Fn ( ℕ0 × ℤ ) ∧ ran ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) = { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } ∧ ∀ 𝑐 ∈ ( ℕ0 × ℤ ) ∀ 𝑑 ∈ ( ℕ0 × ℤ ) ( ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ 𝑐 ) = ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ 𝑑 ) → 𝑐 = 𝑑 ) ) )
59 4 17 57 58 syl3anbrc ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) : ( ℕ0 × ℤ ) –1-1-onto→ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )