Metamath Proof Explorer


Theorem rmym1

Description: Subtraction of 1 formula for Y sequence. Part 2 of equation 2.10 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 19-Oct-2014)

Ref Expression
Assertion rmym1 A 2 N A Y rm N 1 = A Y rm N A A X rm N

Proof

Step Hyp Ref Expression
1 zcn N N
2 1 adantl A 2 N N
3 ax-1cn 1
4 negsub N 1 N + -1 = N 1
5 2 3 4 sylancl A 2 N N + -1 = N 1
6 5 eqcomd A 2 N N 1 = N + -1
7 6 oveq2d A 2 N A Y rm N 1 = A Y rm N + -1
8 neg1z 1
9 rmyadd A 2 N 1 A Y rm N + -1 = A Y rm N A X rm -1 + A X rm N A Y rm -1
10 8 9 mp3an3 A 2 N A Y rm N + -1 = A Y rm N A X rm -1 + A X rm N A Y rm -1
11 1z 1
12 rmxneg A 2 1 A X rm -1 = A X rm 1
13 11 12 mpan2 A 2 A X rm -1 = A X rm 1
14 rmx1 A 2 A X rm 1 = A
15 13 14 eqtrd A 2 A X rm -1 = A
16 15 adantr A 2 N A X rm -1 = A
17 16 oveq2d A 2 N A Y rm N A X rm -1 = A Y rm N A
18 rmyneg A 2 1 A Y rm -1 = A Y rm 1
19 11 18 mpan2 A 2 A Y rm -1 = A Y rm 1
20 rmy1 A 2 A Y rm 1 = 1
21 20 negeqd A 2 A Y rm 1 = 1
22 19 21 eqtrd A 2 A Y rm -1 = 1
23 22 adantr A 2 N A Y rm -1 = 1
24 23 oveq2d A 2 N A X rm N A Y rm -1 = A X rm N -1
25 frmx X rm : 2 × 0
26 25 fovcl A 2 N A X rm N 0
27 26 nn0cnd A 2 N A X rm N
28 neg1cn 1
29 mulcom A X rm N 1 A X rm N -1 = -1 A X rm N
30 27 28 29 sylancl A 2 N A X rm N -1 = -1 A X rm N
31 27 mulm1d A 2 N -1 A X rm N = A X rm N
32 24 30 31 3eqtrd A 2 N A X rm N A Y rm -1 = A X rm N
33 17 32 oveq12d A 2 N A Y rm N A X rm -1 + A X rm N A Y rm -1 = A Y rm N A + A X rm N
34 frmy Y rm : 2 ×
35 34 fovcl A 2 N A Y rm N
36 35 zcnd A 2 N A Y rm N
37 eluzelcn A 2 A
38 37 adantr A 2 N A
39 36 38 mulcld A 2 N A Y rm N A
40 39 27 negsubd A 2 N A Y rm N A + A X rm N = A Y rm N A A X rm N
41 33 40 eqtrd A 2 N A Y rm N A X rm -1 + A X rm N A Y rm -1 = A Y rm N A A X rm N
42 7 10 41 3eqtrd A 2 N A Y rm N 1 = A Y rm N A A X rm N