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	$⊢ A \in ℤ_{\geq 2} \to (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) : ℕ_{0} \times ℤ \underset{1-1 onto}{⟶} \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$

Proof

Step	Hyp	Ref	Expression
1		ovex	$⊢ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b) \in V$
2		eqid	$⊢ (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) = (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))$
3	1 2	fnmpti	$⊢ (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) Fn (ℕ_{0} \times ℤ)$
4	3	a1i	$⊢ A \in ℤ_{\geq 2} \to (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) Fn (ℕ_{0} \times ℤ)$
5	2	rnmpt	$⊢ ran (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) = \{a \| \exists b \in (ℕ_{0} \times ℤ) a = 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)\}$
6		vex	$⊢ c \in V$
7		vex	$⊢ d \in V$
8	6 7	op1std	$⊢ b = ⟨c, d⟩ \to 1^{st} (b) = c$
9	6 7	op2ndd	$⊢ b = ⟨c, d⟩ \to 2^{nd} (b) = d$
10	9	oveq2d	$⊢ b = ⟨c, d⟩ \to \sqrt{A^{2} - 1} 2^{nd} (b) = \sqrt{A^{2} - 1} d$
11	8 10	oveq12d	$⊢ b = ⟨c, d⟩ \to 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b) = c + \sqrt{A^{2} - 1} d$
12	11	eqeq2d	$⊢ b = ⟨c, d⟩ \to (a = 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b) \leftrightarrow a = c + \sqrt{A^{2} - 1} d)$
13	12	rexxp	$⊢ \exists b \in (ℕ_{0} \times ℤ) a = 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b) \leftrightarrow \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d$
14	13	bicomi	$⊢ \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d \leftrightarrow \exists b \in (ℕ_{0} \times ℤ) a = 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)$
15	14	a1i	$⊢ A \in ℤ_{\geq 2} \to (\exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d \leftrightarrow \exists b \in (ℕ_{0} \times ℤ) a = 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))$
16	15	abbidv	$⊢ A \in ℤ_{\geq 2} \to \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\} = \{a \| \exists b \in (ℕ_{0} \times ℤ) a = 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)\}$
17	5 16	eqtr4id	$⊢ A \in ℤ_{\geq 2} \to ran (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) = \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$
18		fveq2	$⊢ b = c \to 1^{st} (b) = 1^{st} (c)$
19		fveq2	$⊢ b = c \to 2^{nd} (b) = 2^{nd} (c)$
20	19	oveq2d	$⊢ b = c \to \sqrt{A^{2} - 1} 2^{nd} (b) = \sqrt{A^{2} - 1} 2^{nd} (c)$
21	18 20	oveq12d	$⊢ b = c \to 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b) = 1^{st} (c) + \sqrt{A^{2} - 1} 2^{nd} (c)$
22		ovex	$⊢ 1^{st} (c) + \sqrt{A^{2} - 1} 2^{nd} (c) \in V$
23	21 2 22	fvmpt	$⊢ c \in (ℕ_{0} \times ℤ) \to (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) (c) = 1^{st} (c) + \sqrt{A^{2} - 1} 2^{nd} (c)$
24	23	ad2antrl	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) (c) = 1^{st} (c) + \sqrt{A^{2} - 1} 2^{nd} (c)$
25		fveq2	$⊢ b = d \to 1^{st} (b) = 1^{st} (d)$
26		fveq2	$⊢ b = d \to 2^{nd} (b) = 2^{nd} (d)$
27	26	oveq2d	$⊢ b = d \to \sqrt{A^{2} - 1} 2^{nd} (b) = \sqrt{A^{2} - 1} 2^{nd} (d)$
28	25 27	oveq12d	$⊢ b = d \to 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b) = 1^{st} (d) + \sqrt{A^{2} - 1} 2^{nd} (d)$
29		ovex	$⊢ 1^{st} (d) + \sqrt{A^{2} - 1} 2^{nd} (d) \in V$
30	28 2 29	fvmpt	$⊢ d \in (ℕ_{0} \times ℤ) \to (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) (d) = 1^{st} (d) + \sqrt{A^{2} - 1} 2^{nd} (d)$
31	30	ad2antll	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) (d) = 1^{st} (d) + \sqrt{A^{2} - 1} 2^{nd} (d)$
32	24 31	eqeq12d	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to ((b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) (c) = (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) (d) \leftrightarrow 1^{st} (c) + \sqrt{A^{2} - 1} 2^{nd} (c) = 1^{st} (d) + \sqrt{A^{2} - 1} 2^{nd} (d))$
33		rmspecsqrtnq	$⊢ A \in ℤ_{\geq 2} \to \sqrt{A^{2} - 1} \in (ℂ ∖ ℚ)$
34	33	adantr	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to \sqrt{A^{2} - 1} \in (ℂ ∖ ℚ)$
35		nn0ssq	$⊢ ℕ_{0} \subseteq ℚ$
36		xp1st	$⊢ c \in (ℕ_{0} \times ℤ) \to 1^{st} (c) \in ℕ_{0}$
37	36	ad2antrl	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to 1^{st} (c) \in ℕ_{0}$
38	35 37	sseldi	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to 1^{st} (c) \in ℚ$
39		xp2nd	$⊢ c \in (ℕ_{0} \times ℤ) \to 2^{nd} (c) \in ℤ$
40	39	ad2antrl	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to 2^{nd} (c) \in ℤ$
41		zq	$⊢ 2^{nd} (c) \in ℤ \to 2^{nd} (c) \in ℚ$
42	40 41	syl	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to 2^{nd} (c) \in ℚ$
43		xp1st	$⊢ d \in (ℕ_{0} \times ℤ) \to 1^{st} (d) \in ℕ_{0}$
44	43	ad2antll	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to 1^{st} (d) \in ℕ_{0}$
45	35 44	sseldi	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to 1^{st} (d) \in ℚ$
46		xp2nd	$⊢ d \in (ℕ_{0} \times ℤ) \to 2^{nd} (d) \in ℤ$
47	46	ad2antll	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to 2^{nd} (d) \in ℤ$
48		zq	$⊢ 2^{nd} (d) \in ℤ \to 2^{nd} (d) \in ℚ$
49	47 48	syl	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to 2^{nd} (d) \in ℚ$
50		qirropth	$⊢ (\sqrt{A^{2} - 1} \in (ℂ ∖ ℚ) \land (1^{st} (c) \in ℚ \land 2^{nd} (c) \in ℚ) \land (1^{st} (d) \in ℚ \land 2^{nd} (d) \in ℚ)) \to (1^{st} (c) + \sqrt{A^{2} - 1} 2^{nd} (c) = 1^{st} (d) + \sqrt{A^{2} - 1} 2^{nd} (d) \leftrightarrow (1^{st} (c) = 1^{st} (d) \land 2^{nd} (c) = 2^{nd} (d)))$
51	34 38 42 45 49 50	syl122anc	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to (1^{st} (c) + \sqrt{A^{2} - 1} 2^{nd} (c) = 1^{st} (d) + \sqrt{A^{2} - 1} 2^{nd} (d) \leftrightarrow (1^{st} (c) = 1^{st} (d) \land 2^{nd} (c) = 2^{nd} (d)))$
52	51	biimpd	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to (1^{st} (c) + \sqrt{A^{2} - 1} 2^{nd} (c) = 1^{st} (d) + \sqrt{A^{2} - 1} 2^{nd} (d) \to (1^{st} (c) = 1^{st} (d) \land 2^{nd} (c) = 2^{nd} (d)))$
53		xpopth	$⊢ (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ)) \to ((1^{st} (c) = 1^{st} (d) \land 2^{nd} (c) = 2^{nd} (d)) \leftrightarrow c = d)$
54	53	adantl	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to ((1^{st} (c) = 1^{st} (d) \land 2^{nd} (c) = 2^{nd} (d)) \leftrightarrow c = d)$
55	52 54	sylibd	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to (1^{st} (c) + \sqrt{A^{2} - 1} 2^{nd} (c) = 1^{st} (d) + \sqrt{A^{2} - 1} 2^{nd} (d) \to c = d)$
56	32 55	sylbid	$⊢ (A \in ℤ_{\geq 2} \land (c \in (ℕ_{0} \times ℤ) \land d \in (ℕ_{0} \times ℤ))) \to ((b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) (c) = (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) (d) \to c = d)$
57	56	ralrimivva	$⊢ A \in ℤ_{\geq 2} \to \forall c \in (ℕ_{0} \times ℤ) \forall d \in (ℕ_{0} \times ℤ) ((b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) (c) = (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) (d) \to c = d)$
58		dff1o6	$⊢ (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) : ℕ_{0} \times ℤ \underset{1-1 onto}{⟶} \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\} \leftrightarrow ((b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) Fn (ℕ_{0} \times ℤ) \land ran (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) = \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\} \land \forall c \in (ℕ_{0} \times ℤ) \forall d \in (ℕ_{0} \times ℤ) ((b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) (c) = (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) (d) \to c = d))$
59	4 17 57 58	syl3anbrc	$⊢ A \in ℤ_{\geq 2} \to (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) : ℕ_{0} \times ℤ \underset{1-1 onto}{⟶} \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$

Metamath Proof Explorer

Theorem rmxypairf1o

Proof