rmydbl

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

		Ref	Expression
	Assertion	rmydbl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} 2 \cdot N = 2 (A X_{rm} N) (A Y_{rm} N)$

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 Y_{rm} 2 \cdot N = A Y_{rm} (N + N)$
5		rmyadd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land N \in ℤ) \to A Y_{rm} (N + N) = (A Y_{rm} N) (A X_{rm} N) + (A X_{rm} N) (A Y_{rm} N)$
6	5	3anidm23	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N + N) = (A Y_{rm} N) (A X_{rm} N) + (A X_{rm} N) (A Y_{rm} N)$
7		2cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 \in ℂ$
8		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
9	8	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
10	9	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℂ$
11		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
12	11	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
13	12	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℂ$
14	7 10 13	mulassd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 (A X_{rm} N) (A Y_{rm} N) = 2 (A X_{rm} N) (A Y_{rm} N)$
15	10 13	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) (A Y_{rm} N) \in ℂ$
16	15	2timesd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to 2 (A X_{rm} N) (A Y_{rm} N) = (A X_{rm} N) (A Y_{rm} N) + (A X_{rm} N) (A Y_{rm} N)$
17	10 13	mulcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) (A Y_{rm} N) = (A Y_{rm} N) (A X_{rm} N)$
18	17	oveq1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) (A Y_{rm} N) + (A X_{rm} N) (A Y_{rm} N) = (A Y_{rm} N) (A X_{rm} N) + (A X_{rm} N) (A Y_{rm} N)$
19	14 16 18	3eqtrrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} N) (A X_{rm} N) + (A X_{rm} N) (A Y_{rm} N) = 2 (A X_{rm} N) (A Y_{rm} N)$
20	4 6 19	3eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} 2 \cdot N = 2 (A X_{rm} N) (A Y_{rm} N)$

Metamath Proof Explorer

Theorem rmydbl

Proof