Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
2 1 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℂ )
3 2 2timesd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
4 3 oveq2d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 2 · 𝑁 ) ) = ( 𝐴 Xrm ( 𝑁 + 𝑁 ) ) )
5 rmxadd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 𝑁 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
6 5 3anidm23 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 𝑁 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
7 frmx ⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
8 7 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
9 8 nn0cnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
10 9 sqcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ∈ ℂ )
11 rmspecnonsq ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )
12 11 eldifad ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ )
13 12 nncnd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
14 13 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
15 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
16 15 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
17 16 zcnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
18 17 sqcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℂ )
19 14 18 mulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ∈ ℂ )
20 10 10 19 pnncand ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) + ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ) − ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) )
21 10 2timesd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 2 · ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) + ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ) )
22 21 eqcomd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) + ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ) = ( 2 · ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ) )
23 rmxynorm ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = 1 )
24 22 23 oveq12d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) + ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ) − ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) ) = ( ( 2 · ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ) − 1 ) )
25 9 sqvald ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) = ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 𝑁 ) ) )
26 17 sqvald ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) = ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) )
27 26 oveq2d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
28 25 27 oveq12d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
29 20 24 28 3eqtr3rd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) = ( ( 2 · ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ) − 1 ) )
30 4 6 29 3eqtrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 2 · 𝑁 ) ) = ( ( 2 · ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ) − 1 ) )