Metamath Proof Explorer

Theorem jm2.21

Description: Lemma for jm2.20nn . Express X and Y values as a binomial. (Contributed by Stefan O'Rear, 26-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		rmbaserp	$⊢ A \in ℤ_{\geq 2} \to A + \sqrt{A^{2} - 1} \in ℝ^{+}$
2	1	rpcnne0d	$⊢ A \in ℤ_{\geq 2} \to (A + \sqrt{A^{2} - 1} \in ℂ \land A + \sqrt{A^{2} - 1} \neq 0)$
3		expmulz	$⊢ ((A + \sqrt{A^{2} - 1} \in ℂ \land A + \sqrt{A^{2} - 1} \neq 0) \land (N \in ℤ \land J \in ℤ)) \to {(A + \sqrt{A^{2} - 1})}^{N \cdot J} = {({(A + \sqrt{A^{2} - 1})}^{N})}^{J}$
4	2 3	sylan	$⊢ (A \in ℤ_{\geq 2} \land (N \in ℤ \land J \in ℤ)) \to {(A + \sqrt{A^{2} - 1})}^{N \cdot J} = {({(A + \sqrt{A^{2} - 1})}^{N})}^{J}$
5		zmulcl	$⊢ (N \in ℤ \land J \in ℤ) \to N \cdot J \in ℤ$
6		rmxyval	$⊢ (A \in ℤ_{\geq 2} \land N \cdot J \in ℤ) \to (A X_{rm} N \cdot J) + \sqrt{A^{2} - 1} (A Y_{rm} N \cdot J) = {(A + \sqrt{A^{2} - 1})}^{N \cdot J}$
7	5 6	sylan2	$⊢ (A \in ℤ_{\geq 2} \land (N \in ℤ \land J \in ℤ)) \to (A X_{rm} N \cdot J) + \sqrt{A^{2} - 1} (A Y_{rm} N \cdot J) = {(A + \sqrt{A^{2} - 1})}^{N \cdot J}$
8		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}$
9	8	adantrr	$⊢ (A \in ℤ_{\geq 2} \land (N \in ℤ \land J \in ℤ)) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) = {(A + \sqrt{A^{2} - 1})}^{N}$
10	9	oveq1d	$⊢ (A \in ℤ_{\geq 2} \land (N \in ℤ \land J \in ℤ)) \to {((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N))}^{J} = {({(A + \sqrt{A^{2} - 1})}^{N})}^{J}$
11	4 7 10	3eqtr4d	$⊢ (A \in ℤ_{\geq 2} \land (N \in ℤ \land J \in ℤ)) \to (A X_{rm} N \cdot J) + \sqrt{A^{2} - 1} (A Y_{rm} N \cdot J) = {((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N))}^{J}$
12	11	3impb	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℤ) \to (A X_{rm} N \cdot J) + \sqrt{A^{2} - 1} (A Y_{rm} N \cdot J) = {((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N))}^{J}$