Step | Hyp | Ref
| Expression |
1 | | peano2zm 12554 |
. . . . . 6
β’ (π β β€ β (π β 1) β
β€) |
2 | | frmx 41284 |
. . . . . . . 8
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
3 | 2 | fovcl 7488 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β€) β (π΄ Xrm (π β 1)) β
β0) |
4 | 3 | nn0cnd 12483 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β€) β (π΄ Xrm (π β 1)) β
β) |
5 | 1, 4 | sylan2 594 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm (π β 1)) β
β) |
6 | | peano2z 12552 |
. . . . . 6
β’ (π β β€ β (π + 1) β
β€) |
7 | 2 | fovcl 7488 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ (π + 1) β β€) β (π΄ Xrm (π + 1)) β
β0) |
8 | 7 | nn0cnd 12483 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ (π + 1) β β€) β (π΄ Xrm (π + 1)) β
β) |
9 | 6, 8 | sylan2 594 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm (π + 1)) β β) |
10 | 5, 9 | addcomd 11365 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm (π β 1)) + (π΄ Xrm (π + 1))) = ((π΄ Xrm (π + 1)) + (π΄ Xrm (π β 1)))) |
11 | | rmxp1 41303 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm (π + 1)) = (((π΄ Xrm π) Β· π΄) + (((π΄β2) β 1) Β· (π΄ Yrm π)))) |
12 | | rmxm1 41305 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm (π β 1)) = ((π΄ Β· (π΄ Xrm π)) β (((π΄β2) β 1) Β· (π΄ Yrm π)))) |
13 | 11, 12 | oveq12d 7379 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm (π + 1)) + (π΄ Xrm (π β 1))) = ((((π΄ Xrm π) Β· π΄) + (((π΄β2) β 1) Β· (π΄ Yrm π))) + ((π΄ Β· (π΄ Xrm π)) β (((π΄β2) β 1) Β· (π΄ Yrm π))))) |
14 | 2 | fovcl 7488 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
15 | 14 | nn0cnd 12483 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β β) |
16 | | eluzelcn 12783 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
17 | 16 | adantr 482 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β π΄ β β) |
18 | 15, 17 | mulcld 11183 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) Β· π΄) β β) |
19 | | rmspecnonsq 41277 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β (β β
β»NN)) |
20 | 19 | eldifad 3926 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β) |
21 | 20 | nncnd 12177 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β) |
22 | 21 | adantr 482 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄β2) β 1) β
β) |
23 | | frmy 41285 |
. . . . . . . . 9
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
24 | 23 | fovcl 7488 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
25 | 24 | zcnd 12616 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β) |
26 | 22, 25 | mulcld 11183 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄β2) β 1) Β· (π΄ Yrm π)) β
β) |
27 | 17, 15 | mulcld 11183 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Β· (π΄ Xrm π)) β β) |
28 | 18, 26, 27 | ppncand 11560 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((((π΄ Xrm π) Β· π΄) + (((π΄β2) β 1) Β· (π΄ Yrm π))) + ((π΄ Β· (π΄ Xrm π)) β (((π΄β2) β 1) Β· (π΄ Yrm π)))) = (((π΄ Xrm π) Β· π΄) + (π΄ Β· (π΄ Xrm π)))) |
29 | 15, 17 | mulcomd 11184 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) Β· π΄) = (π΄ Β· (π΄ Xrm π))) |
30 | 29 | oveq1d 7376 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄ Xrm π) Β· π΄) + (π΄ Β· (π΄ Xrm π))) = ((π΄ Β· (π΄ Xrm π)) + (π΄ Β· (π΄ Xrm π)))) |
31 | | 2cnd 12239 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β 2 β
β) |
32 | 31, 17, 15 | mulassd 11186 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((2 Β· π΄) Β· (π΄ Xrm π)) = (2 Β· (π΄ Β· (π΄ Xrm π)))) |
33 | 27 | 2timesd 12404 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (2 Β· (π΄ Β· (π΄ Xrm π))) = ((π΄ Β· (π΄ Xrm π)) + (π΄ Β· (π΄ Xrm π)))) |
34 | 32, 33 | eqtr2d 2774 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Β· (π΄ Xrm π)) + (π΄ Β· (π΄ Xrm π))) = ((2 Β· π΄) Β· (π΄ Xrm π))) |
35 | 28, 30, 34 | 3eqtrd 2777 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((((π΄ Xrm π) Β· π΄) + (((π΄β2) β 1) Β· (π΄ Yrm π))) + ((π΄ Β· (π΄ Xrm π)) β (((π΄β2) β 1) Β· (π΄ Yrm π)))) = ((2 Β· π΄) Β· (π΄ Xrm π))) |
36 | 10, 13, 35 | 3eqtrd 2777 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm (π β 1)) + (π΄ Xrm (π + 1))) = ((2 Β· π΄) Β· (π΄ Xrm π))) |
37 | | 2cn 12236 |
. . . . . 6
β’ 2 β
β |
38 | | mulcl 11143 |
. . . . . 6
β’ ((2
β β β§ π΄
β β) β (2 Β· π΄) β β) |
39 | 37, 17, 38 | sylancr 588 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (2 Β· π΄) β
β) |
40 | 39, 15 | mulcld 11183 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((2 Β· π΄) Β· (π΄ Xrm π)) β β) |
41 | 40, 5, 9 | subaddd 11538 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((((2 Β· π΄) Β· (π΄ Xrm π)) β (π΄ Xrm (π β 1))) = (π΄ Xrm (π + 1)) β ((π΄ Xrm (π β 1)) + (π΄ Xrm (π + 1))) = ((2 Β· π΄) Β· (π΄ Xrm π)))) |
42 | 36, 41 | mpbird 257 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((2 Β· π΄) Β· (π΄ Xrm π)) β (π΄ Xrm (π β 1))) = (π΄ Xrm (π + 1))) |
43 | 42 | eqcomd 2739 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm (π + 1)) = (((2 Β· π΄) Β· (π΄ Xrm π)) β (π΄ Xrm (π β 1)))) |