rmxyval

Description: Main definition of the X and Y sequences. Compare definition 2.3 of JonesMatijasevic p. 694. (Contributed by Stefan O'Rear, 19-Oct-2014)

		Ref	Expression
	Assertion	rmxyval	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) = {(A + \sqrt{A^{2} - 1})}^{N}$

Proof

Step	Hyp	Ref	Expression
1		rmxfval	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N = 1^{st} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}))$
2		rmyfval	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N = 2^{nd} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}))$
3	2	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \sqrt{A^{2} - 1} (A Y_{rm} N) = \sqrt{A^{2} - 1} 2^{nd} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}))$
4	1 3	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) = 1^{st} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N})) + \sqrt{A^{2} - 1} 2^{nd} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}))$
5		rmxyelxp	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}) \in (ℕ_{0} \times ℤ)$
6		fveq2	$⊢ a = {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}) \to 1^{st} (a) = 1^{st} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}))$
7		fveq2	$⊢ a = {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}) \to 2^{nd} (a) = 2^{nd} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}))$
8	7	oveq2d	$⊢ a = {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}) \to \sqrt{A^{2} - 1} 2^{nd} (a) = \sqrt{A^{2} - 1} 2^{nd} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}))$
9	6 8	oveq12d	$⊢ a = {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}) \to 1^{st} (a) + \sqrt{A^{2} - 1} 2^{nd} (a) = 1^{st} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N})) + \sqrt{A^{2} - 1} 2^{nd} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}))$
10		fveq2	$⊢ b = a \to 1^{st} (b) = 1^{st} (a)$
11		fveq2	$⊢ b = a \to 2^{nd} (b) = 2^{nd} (a)$
12	11	oveq2d	$⊢ b = a \to \sqrt{A^{2} - 1} 2^{nd} (b) = \sqrt{A^{2} - 1} 2^{nd} (a)$
13	10 12	oveq12d	$⊢ b = a \to 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b) = 1^{st} (a) + \sqrt{A^{2} - 1} 2^{nd} (a)$
14	13	cbvmptv	$⊢ (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) = (a \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (a) + \sqrt{A^{2} - 1} 2^{nd} (a))$
15		ovex	$⊢ 1^{st} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N})) + \sqrt{A^{2} - 1} 2^{nd} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N})) \in V$
16	9 14 15	fvmpt	$⊢ {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}) \in (ℕ_{0} \times ℤ) \to (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))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N})) = 1^{st} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N})) + \sqrt{A^{2} - 1} 2^{nd} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}))$
17	5 16	syl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (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))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N})) = 1^{st} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N})) + \sqrt{A^{2} - 1} 2^{nd} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}))$
18		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\}$
19	18	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \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\}$
20		rmxyelqirr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{N} \in \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$
21		f1ocnvfv2	$⊢ ((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\} \land {(A + \sqrt{A^{2} - 1})}^{N} \in \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}) \to (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))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N})) = {(A + \sqrt{A^{2} - 1})}^{N}$
22	19 20 21	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (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))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N})) = {(A + \sqrt{A^{2} - 1})}^{N}$
23	4 17 22	3eqtr2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) = {(A + \sqrt{A^{2} - 1})}^{N}$

Metamath Proof Explorer

Theorem rmxyval

Proof