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 ) → ( 𝑏 ∈ ( ℕ₀ × ℤ ) ↦ ( ( 1^st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2^nd ‘ 𝑏 ) ) ) ) : ( ℕ₀ × ℤ ) –1-1-onto→ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ₀ ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )

Proof

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

Metamath Proof Explorer

Theorem rmxypairf1o

Proof