Step | Hyp | Ref
| Expression |
1 | | neg1z 12547 |
. . . 4
β’ -1 β
β€ |
2 | | rmxadd 41298 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ -1 β β€)
β (π΄ Xrm
(π + -1)) = (((π΄ Xrm π) Β· (π΄ Xrm -1)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm -1))))) |
3 | 1, 2 | mp3an3 1451 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm (π + -1)) = (((π΄ Xrm π) Β· (π΄ Xrm -1)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm -1))))) |
4 | | 1z 12541 |
. . . . . . . . 9
β’ 1 β
β€ |
5 | | rmxneg 41295 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ 1 β β€) β (π΄ Xrm -1) = (π΄ Xrm
1)) |
6 | 4, 5 | mpan2 690 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β (π΄ Xrm -1) = (π΄ Xrm 1)) |
7 | | rmx1 41297 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β (π΄ Xrm 1) = π΄) |
8 | 6, 7 | eqtrd 2773 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β (π΄ Xrm -1) = π΄) |
9 | 8 | adantr 482 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm -1) = π΄) |
10 | 9 | oveq2d 7377 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Xrm -1)) = ((π΄ Xrm π) Β· π΄)) |
11 | | frmx 41284 |
. . . . . . . 8
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
12 | 11 | fovcl 7488 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
13 | 12 | nn0cnd 12483 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β β) |
14 | | eluzelcn 12783 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
15 | 14 | adantr 482 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β π΄ β β) |
16 | 13, 15 | mulcomd 11184 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) Β· π΄) = (π΄ Β· (π΄ Xrm π))) |
17 | 10, 16 | eqtrd 2773 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Xrm -1)) = (π΄ Β· (π΄ Xrm π))) |
18 | | rmyneg 41299 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ 1 β β€) β (π΄ Yrm -1) = -(π΄ Yrm
1)) |
19 | 4, 18 | mpan2 690 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm -1) = -(π΄ Yrm 1)) |
20 | | rmy1 41301 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm 1) = 1) |
21 | 20 | negeqd 11403 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β -(π΄ Yrm 1) = -1) |
22 | 19, 21 | eqtrd 2773 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm -1) = -1) |
23 | 22 | oveq2d 7377 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β ((π΄ Yrm π) Β· (π΄ Yrm -1)) = ((π΄ Yrm π) Β· -1)) |
24 | 23 | adantr 482 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Yrm π) Β· (π΄ Yrm -1)) = ((π΄ Yrm π) Β· -1)) |
25 | | frmy 41285 |
. . . . . . . . . . 11
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
26 | 25 | fovcl 7488 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
27 | 26 | zcnd 12616 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β) |
28 | | ax-1cn 11117 |
. . . . . . . . 9
β’ 1 β
β |
29 | | mulneg2 11600 |
. . . . . . . . 9
β’ (((π΄ Yrm π) β β β§ 1 β
β) β ((π΄
Yrm π) Β·
-1) = -((π΄ Yrm
π) Β·
1)) |
30 | 27, 28, 29 | sylancl 587 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Yrm π) Β· -1) = -((π΄ Yrm π) Β· 1)) |
31 | 27 | mulid1d 11180 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Yrm π) Β· 1) = (π΄ Yrm π)) |
32 | 31 | negeqd 11403 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β -((π΄ Yrm π) Β· 1) = -(π΄ Yrm π)) |
33 | 30, 32 | eqtrd 2773 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Yrm π) Β· -1) = -(π΄ Yrm π)) |
34 | 24, 33 | eqtrd 2773 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Yrm π) Β· (π΄ Yrm -1)) = -(π΄ Yrm π)) |
35 | 34 | oveq2d 7377 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm -1))) = (((π΄β2) β 1) Β· -(π΄ Yrm π))) |
36 | | rmspecnonsq 41277 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β (β β
β»NN)) |
37 | 36 | eldifad 3926 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β) |
38 | 37 | nncnd 12177 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β) |
39 | 38 | adantr 482 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄β2) β 1) β
β) |
40 | 39, 27 | mulneg2d 11617 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄β2) β 1) Β· -(π΄ Yrm π)) = -(((π΄β2) β 1) Β· (π΄ Yrm π))) |
41 | 35, 40 | eqtrd 2773 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm -1))) = -(((π΄β2) β 1) Β·
(π΄ Yrm π))) |
42 | 17, 41 | oveq12d 7379 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄ Xrm π) Β· (π΄ Xrm -1)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm -1)))) = ((π΄ Β· (π΄ Xrm π)) + -(((π΄β2) β 1) Β· (π΄ Yrm π)))) |
43 | 3, 42 | eqtrd 2773 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm (π + -1)) = ((π΄ Β· (π΄ Xrm π)) + -(((π΄β2) β 1) Β· (π΄ Yrm π)))) |
44 | | zcn 12512 |
. . . . 5
β’ (π β β€ β π β
β) |
45 | 44 | adantl 483 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β π β β) |
46 | | negsub 11457 |
. . . 4
β’ ((π β β β§ 1 β
β) β (π + -1) =
(π β
1)) |
47 | 45, 28, 46 | sylancl 587 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π + -1) = (π β 1)) |
48 | 47 | oveq2d 7377 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm (π + -1)) = (π΄ Xrm (π β 1))) |
49 | 15, 13 | mulcld 11183 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Β· (π΄ Xrm π)) β β) |
50 | 39, 27 | mulcld 11183 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄β2) β 1) Β· (π΄ Yrm π)) β
β) |
51 | 49, 50 | negsubd 11526 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Β· (π΄ Xrm π)) + -(((π΄β2) β 1) Β· (π΄ Yrm π))) = ((π΄ Β· (π΄ Xrm π)) β (((π΄β2) β 1) Β· (π΄ Yrm π)))) |
52 | 43, 48, 51 | 3eqtr3d 2781 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm (π β 1)) = ((π΄ Β· (π΄ Xrm π)) β (((π΄β2) β 1) Β· (π΄ Yrm π)))) |