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 A 2 N A Y rm 2 N = 2 A X rm N A Y rm N

Proof

Step Hyp Ref Expression
1 zcn N N
2 1 adantl A 2 N N
3 2 2timesd A 2 N 2 N = N + N
4 3 oveq2d A 2 N A Y rm 2 N = A Y rm N + N
5 rmyadd A 2 N N 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 2 N A Y rm N + N = A Y rm N A X rm N + A X rm N A Y rm N
7 2cnd A 2 N 2
8 frmx X rm : 2 × 0
9 8 fovcl A 2 N A X rm N 0
10 9 nn0cnd A 2 N A X rm N
11 frmy Y rm : 2 ×
12 11 fovcl A 2 N A Y rm N
13 12 zcnd A 2 N A Y rm N
14 7 10 13 mulassd A 2 N 2 A X rm N A Y rm N = 2 A X rm N A Y rm N
15 10 13 mulcld A 2 N A X rm N A Y rm N
16 15 2timesd A 2 N 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 2 N A X rm N A Y rm N = A Y rm N A X rm N
18 17 oveq1d A 2 N 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 2 N 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 2 N A Y rm 2 N = 2 A X rm N A Y rm N