Metamath Proof Explorer

Theorem rmxfval

Description: Value of the X sequence. Not used after rmxyval is proved. (Contributed by Stefan O'Rear, 21-Sep-2014)

		Ref	Expression
	Assertion	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}))$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ a = A \to a^{2} = A^{2}$
2	1	fvoveq1d	$⊢ a = A \to \sqrt{a^{2} - 1} = \sqrt{A^{2} - 1}$
3	2	oveq1d	$⊢ a = A \to \sqrt{a^{2} - 1} 2^{nd} (b) = \sqrt{A^{2} - 1} 2^{nd} (b)$
4	3	oveq2d	$⊢ a = A \to 1^{st} (b) + \sqrt{a^{2} - 1} 2^{nd} (b) = 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)$
5	4	mpteq2dv	$⊢ a = A \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))$
6	5	cnveqd	$⊢ a = A \to {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{a^{2} - 1} 2^{nd} (b))}^{-1} = {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1}$
7	6	adantr	$⊢ (a = A \land n = N) \to {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{a^{2} - 1} 2^{nd} (b))}^{-1} = {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1}$
8		id	$⊢ a = A \to a = A$
9	8 2	oveq12d	$⊢ a = A \to a + \sqrt{a^{2} - 1} = A + \sqrt{A^{2} - 1}$
10		id	$⊢ n = N \to n = N$
11	9 10	oveqan12d	$⊢ (a = A \land n = N) \to {(a + \sqrt{a^{2} - 1})}^{n} = {(A + \sqrt{A^{2} - 1})}^{N}$
12	7 11	fveq12d	$⊢ (a = A \land n = N) \to {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{a^{2} - 1} 2^{nd} (b))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{n}) = {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N})$
13	12	fveq2d	$⊢ (a = A \land n = N) \to 1^{st} ({(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}))$
14		df-rmx	$⊢ X_{rm} = (a \in ℤ_{\geq 2}, n \in ℤ ⟼ 1^{st} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{a^{2} - 1} 2^{nd} (b))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{n})))$
15		fvex	$⊢ 1^{st} ({(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N})) \in V$
16	13 14 15	ovmpoa	$⊢ (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}))$