rmxdbl

Description: "Double-angle formula" for X-values. Equation 2.13 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 2-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ N \in ℤ \to N \in ℂ$
2	1	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to N \in ℂ$
3	2	2timesd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 \cdot N = N + N$
4	3	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} 2 \cdot N = A X_{rm} (N + N)$
5		rmxadd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land N \in ℤ) \to A X_{rm} (N + N) = (A X_{rm} N) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} N)$
6	5	3anidm23	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} (N + N) = (A X_{rm} N) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} N)$
7		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
8	7	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
9	8	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℂ$
10	9	sqcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A X_{rm} N)}^{2} \in ℂ$
11		rmspecnonsq	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in (ℕ ∖ ◻_{ℕ})$
12	11	eldifad	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℕ$
13	12	nncnd	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℂ$
14	13	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A^{2} - 1 \in ℂ$
15		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
16	15	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
17	16	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℂ$
18	17	sqcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A Y_{rm} N)}^{2} \in ℂ$
19	14 18	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A^{2} - 1) {(A Y_{rm} N)}^{2} \in ℂ$
20	10 10 19	pnncand	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A X_{rm} N)}^{2} + {(A X_{rm} N)}^{2} - ({(A X_{rm} N)}^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2}) = {(A X_{rm} N)}^{2} + (A^{2} - 1) {(A Y_{rm} N)}^{2}$
21	10	2timesd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 {(A X_{rm} N)}^{2} = {(A X_{rm} N)}^{2} + {(A X_{rm} N)}^{2}$
22	21	eqcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A X_{rm} N)}^{2} + {(A X_{rm} N)}^{2} = 2 {(A X_{rm} N)}^{2}$
23		rmxynorm	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A X_{rm} N)}^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} = 1$
24	22 23	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A X_{rm} N)}^{2} + {(A X_{rm} N)}^{2} - ({(A X_{rm} N)}^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2}) = 2 {(A X_{rm} N)}^{2} - 1$
25	9	sqvald	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A X_{rm} N)}^{2} = (A X_{rm} N) (A X_{rm} N)$
26	17	sqvald	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A Y_{rm} N)}^{2} = (A Y_{rm} N) (A Y_{rm} N)$
27	26	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A^{2} - 1) {(A Y_{rm} N)}^{2} = (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} N)$
28	25 27	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A X_{rm} N)}^{2} + (A^{2} - 1) {(A Y_{rm} N)}^{2} = (A X_{rm} N) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} N)$
29	20 24 28	3eqtr3rd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) (A X_{rm} N) + (A^{2} - 1) (A Y_{rm} N) (A Y_{rm} N) = 2 {(A X_{rm} N)}^{2} - 1$
30	4 6 29	3eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} 2 \cdot N = 2 {(A X_{rm} N)}^{2} - 1$

Metamath Proof Explorer

Theorem rmxdbl

Proof