Metamath Proof Explorer

Theorem 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 ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 2 · 𝑁 ) ) = ( ( 2 · ( 𝐴 Xrm 𝑁 ) ) · ( 𝐴 Yrm 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
2 1 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℂ )
3 2 2timesd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
4 3 oveq2d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 2 · 𝑁 ) ) = ( 𝐴 Yrm ( 𝑁 + 𝑁 ) ) )
5 rmyadd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 𝑁 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
6 5 3anidm23 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 𝑁 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
7 2cnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 2 ∈ ℂ )
8 frmx ⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
9 8 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
10 9 nn0cnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
11 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
12 11 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
13 12 zcnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
14 7 10 13 mulassd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 2 · ( 𝐴 Xrm 𝑁 ) ) · ( 𝐴 Yrm 𝑁 ) ) = ( 2 · ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
15 10 13 mulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℂ )
16 15 2timesd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 2 · ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
17 10 13 mulcomd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) = ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑁 ) ) )
18 17 oveq1d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
19 14 16 18 3eqtrrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( 2 · ( 𝐴 Xrm 𝑁 ) ) · ( 𝐴 Yrm 𝑁 ) ) )
20 4 6 19 3eqtrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 2 · 𝑁 ) ) = ( ( 2 · ( 𝐴 Xrm 𝑁 ) ) · ( 𝐴 Yrm 𝑁 ) ) )