Step | Hyp | Ref
| Expression |
1 | | 2z 12540 |
. . . . . . . . . 10
β’ 2 β
β€ |
2 | | eluzelz 12778 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β π΄ β β€) |
3 | 2 | adantr 482 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β π΄ β
β€) |
4 | | zmulcl 12557 |
. . . . . . . . . 10
β’ ((2
β β€ β§ π΄
β β€) β (2 Β· π΄) β β€) |
5 | 1, 3, 4 | sylancr 588 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (2
Β· π΄) β
β€) |
6 | | nn0z 12529 |
. . . . . . . . . 10
β’ (πΎ β β0
β πΎ β
β€) |
7 | 6 | adantl 483 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β πΎ β
β€) |
8 | 5, 7 | zmulcld 12618 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((2
Β· π΄) Β· πΎ) β
β€) |
9 | | zsqcl 14040 |
. . . . . . . . 9
β’ (πΎ β β€ β (πΎβ2) β
β€) |
10 | 7, 9 | syl 17 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (πΎβ2) β
β€) |
11 | 8, 10 | zsubcld 12617 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((2
Β· π΄) Β· πΎ) β (πΎβ2)) β β€) |
12 | | peano2zm 12551 |
. . . . . . 7
β’ ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β β€ β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β
β€) |
13 | 11, 12 | syl 17 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β
β€) |
14 | | dvds0 16159 |
. . . . . 6
β’ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β
((((2 Β· π΄) Β·
πΎ) β (πΎβ2)) β 1) β₯
0) |
15 | 13, 14 | syl 17 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯
0) |
16 | | rmx0 41292 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β (π΄ Xrm 0) = 1) |
17 | 16 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (π΄ Xrm 0) =
1) |
18 | | rmy0 41296 |
. . . . . . . . . . . 12
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm 0) = 0) |
19 | 18 | adantr 482 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (π΄ Yrm 0) =
0) |
20 | 19 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((π΄ β πΎ) Β· (π΄ Yrm 0)) = ((π΄ β πΎ) Β· 0)) |
21 | 3, 7 | zsubcld 12617 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (π΄ β πΎ) β β€) |
22 | 21 | zcnd 12613 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (π΄ β πΎ) β β) |
23 | 22 | mul01d 11359 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((π΄ β πΎ) Β· 0) = 0) |
24 | 20, 23 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((π΄ β πΎ) Β· (π΄ Yrm 0)) = 0) |
25 | 17, 24 | oveq12d 7376 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((π΄ Xrm 0) β
((π΄ β πΎ) Β· (π΄ Yrm 0))) = (1 β
0)) |
26 | | 1m0e1 12279 |
. . . . . . . 8
β’ (1
β 0) = 1 |
27 | 25, 26 | eqtrdi 2789 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((π΄ Xrm 0) β
((π΄ β πΎ) Β· (π΄ Yrm 0))) = 1) |
28 | | nn0cn 12428 |
. . . . . . . . 9
β’ (πΎ β β0
β πΎ β
β) |
29 | 28 | adantl 483 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β πΎ β
β) |
30 | 29 | exp0d 14051 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (πΎβ0) = 1) |
31 | 27, 30 | oveq12d 7376 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((π΄ Xrm 0) β
((π΄ β πΎ) Β· (π΄ Yrm 0))) β (πΎβ0)) = (1 β
1)) |
32 | | 1m1e0 12230 |
. . . . . 6
β’ (1
β 1) = 0 |
33 | 31, 32 | eqtrdi 2789 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((π΄ Xrm 0) β
((π΄ β πΎ) Β· (π΄ Yrm 0))) β (πΎβ0)) = 0) |
34 | 15, 33 | breqtrrd 5134 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm 0) β
((π΄ β πΎ) Β· (π΄ Yrm 0))) β (πΎβ0))) |
35 | | rmx1 41293 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β (π΄ Xrm 1) = π΄) |
36 | 35 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (π΄ Xrm 1) = π΄) |
37 | | rmy1 41297 |
. . . . . . . . . . . 12
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm 1) = 1) |
38 | 37 | adantr 482 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (π΄ Yrm 1) =
1) |
39 | 38 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((π΄ β πΎ) Β· (π΄ Yrm 1)) = ((π΄ β πΎ) Β· 1)) |
40 | 22 | mulid1d 11177 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((π΄ β πΎ) Β· 1) = (π΄ β πΎ)) |
41 | 39, 40 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((π΄ β πΎ) Β· (π΄ Yrm 1)) = (π΄ β πΎ)) |
42 | 36, 41 | oveq12d 7376 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((π΄ Xrm 1) β
((π΄ β πΎ) Β· (π΄ Yrm 1))) = (π΄ β (π΄ β πΎ))) |
43 | 3 | zcnd 12613 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β π΄ β
β) |
44 | 43, 29 | nncand 11522 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (π΄ β (π΄ β πΎ)) = πΎ) |
45 | 42, 44 | eqtrd 2773 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((π΄ Xrm 1) β
((π΄ β πΎ) Β· (π΄ Yrm 1))) = πΎ) |
46 | 29 | exp1d 14052 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (πΎβ1) = πΎ) |
47 | 45, 46 | oveq12d 7376 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((π΄ Xrm 1) β
((π΄ β πΎ) Β· (π΄ Yrm 1))) β (πΎβ1)) = (πΎ β πΎ)) |
48 | 29 | subidd 11505 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (πΎ β πΎ) = 0) |
49 | 47, 48 | eqtrd 2773 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((π΄ Xrm 1) β
((π΄ β πΎ) Β· (π΄ Yrm 1))) β (πΎβ1)) = 0) |
50 | 15, 49 | breqtrrd 5134 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm 1) β
((π΄ β πΎ) Β· (π΄ Yrm 1))) β (πΎβ1))) |
51 | | pm3.43 475 |
. . . . 5
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1)))) β§ ((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β ((π΄ β (β€β₯β2)
β§ πΎ β
β0) β (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))))) |
52 | 13 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β
β€) |
53 | 5 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (2
Β· π΄) β
β€) |
54 | | simpll 766 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β π΄ β
(β€β₯β2)) |
55 | | nnz 12525 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
β€) |
56 | 55 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β π β
β€) |
57 | | frmx 41280 |
. . . . . . . . . . . . . . . . . 18
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
58 | 57 | fovcl 7485 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
59 | 54, 56, 58 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ Xrm π) β
β0) |
60 | 59 | nn0zd 12530 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ Xrm π) β
β€) |
61 | 21 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ β πΎ) β β€) |
62 | | frmy 41281 |
. . . . . . . . . . . . . . . . . 18
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
63 | 62 | fovcl 7485 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
64 | 54, 56, 63 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ Yrm π) β
β€) |
65 | 61, 64 | zmulcld 12618 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ β πΎ) Β· (π΄ Yrm π)) β β€) |
66 | 60, 65 | zsubcld 12617 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β β€) |
67 | 53, 66 | zmulcld 12618 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((2
Β· π΄) Β·
((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β β€) |
68 | | peano2zm 12551 |
. . . . . . . . . . . . . . . . 17
β’ (π β β€ β (π β 1) β
β€) |
69 | 56, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π β 1) β
β€) |
70 | 57 | fovcl 7485 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β€) β (π΄ Xrm (π β 1)) β
β0) |
71 | 54, 69, 70 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ Xrm (π β 1)) β
β0) |
72 | 71 | nn0zd 12530 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ Xrm (π β 1)) β
β€) |
73 | 62 | fovcl 7485 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β€) β (π΄ Yrm (π β 1)) β
β€) |
74 | 54, 69, 73 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ Yrm (π β 1)) β
β€) |
75 | 61, 74 | zmulcld 12618 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))) β
β€) |
76 | 72, 75 | zsubcld 12617 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β
β€) |
77 | 67, 76 | zsubcld 12617 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((2
Β· π΄) Β·
((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) β
β€) |
78 | 52, 77 | jca 513 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§
(((2 Β· π΄) Β·
((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) β
β€)) |
79 | 78 | adantr 482 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§
(((2 Β· π΄) Β·
((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) β
β€)) |
80 | 7 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β πΎ β
β€) |
81 | | nnnn0 12425 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β0) |
82 | 81 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β π β
β0) |
83 | | zexpcl 13988 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β β€ β§ π β β0)
β (πΎβπ) β
β€) |
84 | 80, 82, 83 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (πΎβπ) β β€) |
85 | 53, 84 | zmulcld 12618 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((2
Β· π΄) Β· (πΎβπ)) β β€) |
86 | | nnm1nn0 12459 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π β 1) β
β0) |
87 | 86 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π β 1) β
β0) |
88 | | zexpcl 13988 |
. . . . . . . . . . . . . 14
β’ ((πΎ β β€ β§ (π β 1) β
β0) β (πΎβ(π β 1)) β β€) |
89 | 80, 87, 88 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (πΎβ(π β 1)) β β€) |
90 | 85, 89 | zsubcld 12617 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((2
Β· π΄) Β· (πΎβπ)) β (πΎβ(π β 1))) β
β€) |
91 | | 0z 12515 |
. . . . . . . . . . . . . . 15
β’ 0 β
β€ |
92 | | zaddcl 12548 |
. . . . . . . . . . . . . . 15
β’ ((0
β β€ β§ (πΎβ2) β β€) β (0 + (πΎβ2)) β
β€) |
93 | 91, 10, 92 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (0 +
(πΎβ2)) β
β€) |
94 | 93 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (0 +
(πΎβ2)) β
β€) |
95 | 89, 94 | zmulcld 12618 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((πΎβ(π β 1)) Β· (0 + (πΎβ2))) β β€) |
96 | 90, 95 | jca 513 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((((2
Β· π΄) Β· (πΎβπ)) β (πΎβ(π β 1))) β β€ β§ ((πΎβ(π β 1)) Β· (0 + (πΎβ2))) β β€)) |
97 | 96 | adantr 482 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β ((((2 Β· π΄) Β· (πΎβπ)) β (πΎβ(π β 1))) β β€ β§ ((πΎβ(π β 1)) Β· (0 + (πΎβ2))) β β€)) |
98 | 52, 67, 85 | 3jca 1129 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§
((2 Β· π΄) Β·
((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β β€ β§ ((2 Β· π΄) Β· (πΎβπ)) β β€)) |
99 | 98 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§
((2 Β· π΄) Β·
((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β β€ β§ ((2 Β· π΄) Β· (πΎβπ)) β β€)) |
100 | 76, 89 | jca 513 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β β€ β§ (πΎβ(π β 1)) β
β€)) |
101 | 100 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β β€ β§ (πΎβ(π β 1)) β
β€)) |
102 | 13, 5, 5 | 3jca 1129 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§ (2
Β· π΄) β β€
β§ (2 Β· π΄) β
β€)) |
103 | 102 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§ (2
Β· π΄) β β€
β§ (2 Β· π΄) β
β€)) |
104 | 66, 84 | jca 513 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β β€ β§ (πΎβπ) β β€)) |
105 | 104 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β β€ β§ (πΎβπ) β β€)) |
106 | | congid 41338 |
. . . . . . . . . . . . . . 15
β’ ((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§ (2
Β· π΄) β β€)
β ((((2 Β· π΄)
Β· πΎ) β (πΎβ2)) β 1) β₯ ((2
Β· π΄) β (2
Β· π΄))) |
107 | 13, 5, 106 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((2 Β·
π΄) β (2 Β·
π΄))) |
108 | 107 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((2 Β·
π΄) β (2 Β·
π΄))) |
109 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) |
110 | | congmul 41334 |
. . . . . . . . . . . . 13
β’ (((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§ (2
Β· π΄) β β€
β§ (2 Β· π΄) β
β€) β§ (((π΄
Xrm π) β
((π΄ β πΎ) Β· (π΄ Yrm π))) β β€ β§ (πΎβπ) β β€) β§ (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((2 Β·
π΄) β (2 Β·
π΄)) β§ ((((2 Β·
π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((2 Β·
π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((2 Β· π΄) Β· (πΎβπ)))) |
111 | 103, 105,
108, 109, 110 | syl112anc 1375 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((2 Β·
π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((2 Β· π΄) Β· (πΎβπ)))) |
112 | 111 | adantrl 715 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((2 Β·
π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((2 Β· π΄) Β· (πΎβπ)))) |
113 | | simprl 770 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1)))) |
114 | | congsub 41337 |
. . . . . . . . . . 11
β’ (((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§
((2 Β· π΄) Β·
((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β β€ β§ ((2 Β· π΄) Β· (πΎβπ)) β β€) β§ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β β€ β§ (πΎβ(π β 1)) β β€) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((2 Β·
π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((2 Β· π΄) Β· (πΎβπ))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((2 Β·
π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) β (((2 Β· π΄) Β· (πΎβπ)) β (πΎβ(π β 1))))) |
115 | 99, 101, 112, 113, 114 | syl112anc 1375 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((2 Β·
π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) β (((2 Β· π΄) Β· (πΎβπ)) β (πΎβ(π β 1))))) |
116 | 13, 10 | zaddcld 12616 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2)) β β€) |
117 | 116 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2)) β β€) |
118 | | congid 41338 |
. . . . . . . . . . . . . 14
β’ ((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§
(πΎβ(π β 1)) β β€) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((πΎβ(π β 1)) β (πΎβ(π β 1)))) |
119 | 52, 89, 118 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((πΎβ(π β 1)) β (πΎβ(π β 1)))) |
120 | | 0zd 12516 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β 0 β
β€) |
121 | | iddvds 16157 |
. . . . . . . . . . . . . . . . 17
β’ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β
((((2 Β· π΄) Β·
πΎ) β (πΎβ2)) β 1) β₯
((((2 Β· π΄) Β·
πΎ) β (πΎβ2)) β
1)) |
122 | 13, 121 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((2 Β·
π΄) Β· πΎ) β (πΎβ2)) β 1)) |
123 | 13 | zcnd 12613 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β
β) |
124 | 123 | subid1d 11506 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β 0) = ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1)) |
125 | 122, 124 | breqtrrd 5134 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((((2 Β·
π΄) Β· πΎ) β (πΎβ2)) β 1) β
0)) |
126 | | congid 41338 |
. . . . . . . . . . . . . . . 16
β’ ((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§
(πΎβ2) β β€)
β ((((2 Β· π΄)
Β· πΎ) β (πΎβ2)) β 1) β₯
((πΎβ2) β (πΎβ2))) |
127 | 13, 10, 126 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((πΎβ2) β (πΎβ2))) |
128 | | congadd 41333 |
. . . . . . . . . . . . . . 15
β’ (((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§
((((2 Β· π΄) Β·
πΎ) β (πΎβ2)) β 1) β
β€ β§ 0 β β€) β§ ((πΎβ2) β β€ β§ (πΎβ2) β β€) β§
(((((2 Β· π΄) Β·
πΎ) β (πΎβ2)) β 1) β₯
(((((2 Β· π΄) Β·
πΎ) β (πΎβ2)) β 1) β 0)
β§ ((((2 Β· π΄)
Β· πΎ) β (πΎβ2)) β 1) β₯
((πΎβ2) β (πΎβ2)))) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2)) β (0 + (πΎβ2)))) |
129 | 13, 13, 120, 10, 10, 125, 127, 128 | syl322anc 1399 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2)) β (0 + (πΎβ2)))) |
130 | 129 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2)) β (0 + (πΎβ2)))) |
131 | | congmul 41334 |
. . . . . . . . . . . . 13
β’ (((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§
(πΎβ(π β 1)) β β€ β§ (πΎβ(π β 1)) β β€) β§ ((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2)) β β€ β§ (0 + (πΎβ2)) β β€) β§
(((((2 Β· π΄) Β·
πΎ) β (πΎβ2)) β 1) β₯
((πΎβ(π β 1)) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2)) β (0 + (πΎβ2))))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((πΎβ(π β 1)) Β· (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2))) β ((πΎβ(π β 1)) Β· (0 + (πΎβ2))))) |
132 | 52, 89, 89, 117, 94, 119, 130, 131 | syl322anc 1399 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((πΎβ(π β 1)) Β· (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2))) β ((πΎβ(π β 1)) Β· (0 + (πΎβ2))))) |
133 | 11 | zcnd 12613 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((2
Β· π΄) Β· πΎ) β (πΎβ2)) β β) |
134 | 29 | sqcld 14055 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (πΎβ2) β
β) |
135 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β 1 β
β) |
136 | 133, 134,
135 | addsubd 11538 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) + (πΎβ2)) β 1) = (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2))) |
137 | 8 | zcnd 12613 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((2
Β· π΄) Β· πΎ) β
β) |
138 | 137, 134 | npcand 11521 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) + (πΎβ2)) = ((2 Β· π΄) Β· πΎ)) |
139 | 138 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) + (πΎβ2)) β 1) = (((2 Β· π΄) Β· πΎ) β 1)) |
140 | 136, 139 | eqtr3d 2775 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2)) = (((2 Β· π΄) Β· πΎ) β 1)) |
141 | 140 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2)) = (((2 Β· π΄) Β· πΎ) β 1)) |
142 | 141 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((πΎβ(π β 1)) Β· (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2))) = ((πΎβ(π β 1)) Β· (((2 Β· π΄) Β· πΎ) β 1))) |
143 | 28 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β πΎ β
β) |
144 | 143, 87 | expcld 14057 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (πΎβ(π β 1)) β β) |
145 | 137 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((2
Β· π΄) Β· πΎ) β
β) |
146 | | 1cnd 11155 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β 1 β
β) |
147 | 144, 145,
146 | subdid 11616 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((πΎβ(π β 1)) Β· (((2 Β· π΄) Β· πΎ) β 1)) = (((πΎβ(π β 1)) Β· ((2 Β· π΄) Β· πΎ)) β ((πΎβ(π β 1)) Β· 1))) |
148 | 5 | zcnd 12613 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (2
Β· π΄) β
β) |
149 | 148 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (2
Β· π΄) β
β) |
150 | 144, 149,
143 | mul12d 11369 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((πΎβ(π β 1)) Β· ((2 Β· π΄) Β· πΎ)) = ((2 Β· π΄) Β· ((πΎβ(π β 1)) Β· πΎ))) |
151 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β π β
β) |
152 | | expm1t 14002 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β β β§ π β β) β (πΎβπ) = ((πΎβ(π β 1)) Β· πΎ)) |
153 | 143, 151,
152 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (πΎβπ) = ((πΎβ(π β 1)) Β· πΎ)) |
154 | 153 | oveq2d 7374 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((2
Β· π΄) Β· (πΎβπ)) = ((2 Β· π΄) Β· ((πΎβ(π β 1)) Β· πΎ))) |
155 | 150, 154 | eqtr4d 2776 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((πΎβ(π β 1)) Β· ((2 Β· π΄) Β· πΎ)) = ((2 Β· π΄) Β· (πΎβπ))) |
156 | 144 | mulid1d 11177 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((πΎβ(π β 1)) Β· 1) = (πΎβ(π β 1))) |
157 | 155, 156 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((πΎβ(π β 1)) Β· ((2 Β· π΄) Β· πΎ)) β ((πΎβ(π β 1)) Β· 1)) = (((2 Β·
π΄) Β· (πΎβπ)) β (πΎβ(π β 1)))) |
158 | 142, 147,
157 | 3eqtrrd 2778 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((2
Β· π΄) Β· (πΎβπ)) β (πΎβ(π β 1))) = ((πΎβ(π β 1)) Β· (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2)))) |
159 | 158 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((((2
Β· π΄) Β· (πΎβπ)) β (πΎβ(π β 1))) β ((πΎβ(π β 1)) Β· (0 + (πΎβ2)))) = (((πΎβ(π β 1)) Β· (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) + (πΎβ2))) β ((πΎβ(π β 1)) Β· (0 + (πΎβ2))))) |
160 | 132, 159 | breqtrrd 5134 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((2 Β·
π΄) Β· (πΎβπ)) β (πΎβ(π β 1))) β ((πΎβ(π β 1)) Β· (0 + (πΎβ2))))) |
161 | 160 | adantr 482 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((2 Β·
π΄) Β· (πΎβπ)) β (πΎβ(π β 1))) β ((πΎβ(π β 1)) Β· (0 + (πΎβ2))))) |
162 | | congtr 41332 |
. . . . . . . . . 10
β’ (((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β€ β§
(((2 Β· π΄) Β·
((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) β β€) β§ ((((2
Β· π΄) Β· (πΎβπ)) β (πΎβ(π β 1))) β β€ β§ ((πΎβ(π β 1)) Β· (0 + (πΎβ2))) β β€) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((2 Β·
π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) β (((2 Β· π΄) Β· (πΎβπ)) β (πΎβ(π β 1)))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((2 Β·
π΄) Β· (πΎβπ)) β (πΎβ(π β 1))) β ((πΎβ(π β 1)) Β· (0 + (πΎβ2)))))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((2 Β·
π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) β ((πΎβ(π β 1)) Β· (0 + (πΎβ2))))) |
163 | 79, 97, 115, 161, 162 | syl112anc 1375 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ ((((2 Β·
π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) β ((πΎβ(π β 1)) Β· (0 + (πΎβ2))))) |
164 | | rmxluc 41303 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm (π + 1)) = (((2 Β· π΄) Β· (π΄ Xrm π)) β (π΄ Xrm (π β 1)))) |
165 | 54, 56, 164 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ Xrm (π + 1)) = (((2 Β· π΄) Β· (π΄ Xrm π)) β (π΄ Xrm (π β 1)))) |
166 | | rmyluc 41304 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm (π + 1)) = ((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1)))) |
167 | 54, 56, 166 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ Yrm (π + 1)) = ((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1)))) |
168 | 167 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1))) = ((π΄ β πΎ) Β· ((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1))))) |
169 | 2 | zcnd 12613 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
170 | 169 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β π΄ β
β) |
171 | 170, 143 | subcld 11517 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ β πΎ) β β) |
172 | | 2cn 12233 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
173 | 63 | zcnd 12613 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β) |
174 | 54, 56, 173 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ Yrm π) β
β) |
175 | 174, 170 | mulcld 11180 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ Yrm π) Β· π΄) β β) |
176 | | mulcl 11140 |
. . . . . . . . . . . . . . . 16
β’ ((2
β β β§ ((π΄
Yrm π) Β·
π΄) β β) β
(2 Β· ((π΄
Yrm π) Β·
π΄)) β
β) |
177 | 172, 175,
176 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (2
Β· ((π΄ Yrm
π) Β· π΄)) β
β) |
178 | 73 | zcnd 12613 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β€) β (π΄ Yrm (π β 1)) β
β) |
179 | 54, 69, 178 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ Yrm (π β 1)) β
β) |
180 | 171, 177,
179 | subdid 11616 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ β πΎ) Β· ((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1)))) = (((π΄ β πΎ) Β· (2 Β· ((π΄ Yrm π) Β· π΄))) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) |
181 | | 2cnd 12236 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β 2 β
β) |
182 | 181, 174,
170 | mul12d 11369 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (2
Β· ((π΄ Yrm
π) Β· π΄)) = ((π΄ Yrm π) Β· (2 Β· π΄))) |
183 | 174, 149 | mulcomd 11181 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ Yrm π) Β· (2 Β· π΄)) = ((2 Β· π΄) Β· (π΄ Yrm π))) |
184 | 182, 183 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (2
Β· ((π΄ Yrm
π) Β· π΄)) = ((2 Β· π΄) Β· (π΄ Yrm π))) |
185 | 184 | oveq2d 7374 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ β πΎ) Β· (2 Β· ((π΄ Yrm π) Β· π΄))) = ((π΄ β πΎ) Β· ((2 Β· π΄) Β· (π΄ Yrm π)))) |
186 | 171, 149,
174 | mul12d 11369 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ β πΎ) Β· ((2 Β· π΄) Β· (π΄ Yrm π))) = ((2 Β· π΄) Β· ((π΄ β πΎ) Β· (π΄ Yrm π)))) |
187 | 185, 186 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ β πΎ) Β· (2 Β· ((π΄ Yrm π) Β· π΄))) = ((2 Β· π΄) Β· ((π΄ β πΎ) Β· (π΄ Yrm π)))) |
188 | 187 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((π΄ β πΎ) Β· (2 Β· ((π΄ Yrm π) Β· π΄))) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) = (((2 Β· π΄) Β· ((π΄ β πΎ) Β· (π΄ Yrm π))) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) |
189 | 168, 180,
188 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1))) = (((2 Β· π΄) Β· ((π΄ β πΎ) Β· (π΄ Yrm π))) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) |
190 | 165, 189 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) = ((((2 Β· π΄) Β· (π΄ Xrm π)) β (π΄ Xrm (π β 1))) β (((2 Β· π΄) Β· ((π΄ β πΎ) Β· (π΄ Yrm π))) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))))) |
191 | 58 | nn0cnd 12480 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β β) |
192 | 54, 56, 191 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ Xrm π) β
β) |
193 | 149, 192 | mulcld 11180 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((2
Β· π΄) Β· (π΄ Xrm π)) β
β) |
194 | 70 | nn0cnd 12480 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β€) β (π΄ Xrm (π β 1)) β
β) |
195 | 54, 69, 194 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (π΄ Xrm (π β 1)) β
β) |
196 | 171, 174 | mulcld 11180 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ β πΎ) Β· (π΄ Yrm π)) β β) |
197 | 149, 196 | mulcld 11180 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((2
Β· π΄) Β·
((π΄ β πΎ) Β· (π΄ Yrm π))) β β) |
198 | 171, 179 | mulcld 11180 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))) β
β) |
199 | 193, 195,
197, 198 | sub4d 11566 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((((2
Β· π΄) Β· (π΄ Xrm π)) β (π΄ Xrm (π β 1))) β (((2 Β· π΄) Β· ((π΄ β πΎ) Β· (π΄ Yrm π))) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) = ((((2 Β· π΄) Β· (π΄ Xrm π)) β ((2 Β· π΄) Β· ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))))) |
200 | 149, 192,
196 | subdid 11616 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((2
Β· π΄) Β·
((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) = (((2 Β· π΄) Β· (π΄ Xrm π)) β ((2 Β· π΄) Β· ((π΄ β πΎ) Β· (π΄ Yrm π))))) |
201 | 200 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((2
Β· π΄) Β· (π΄ Xrm π)) β ((2 Β· π΄) Β· ((π΄ β πΎ) Β· (π΄ Yrm π)))) = ((2 Β· π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))))) |
202 | 201 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((((2
Β· π΄) Β· (π΄ Xrm π)) β ((2 Β· π΄) Β· ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) = (((2 Β· π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))))) |
203 | 190, 199,
202 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) = (((2 Β· π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))))) |
204 | 143, 82 | expp1d 14058 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (πΎβ(π + 1)) = ((πΎβπ) Β· πΎ)) |
205 | | nncn 12166 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β) |
206 | 205 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β π β
β) |
207 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
208 | | npcan 11415 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ 1 β
β) β ((π β
1) + 1) = π) |
209 | 206, 207,
208 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((π β 1) + 1) = π) |
210 | 209 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (πΎβ((π β 1) + 1)) = (πΎβπ)) |
211 | 143, 87 | expp1d 14058 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (πΎβ((π β 1) + 1)) = ((πΎβ(π β 1)) Β· πΎ)) |
212 | 210, 211 | eqtr3d 2775 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (πΎβπ) = ((πΎβ(π β 1)) Β· πΎ)) |
213 | 212 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((πΎβπ) Β· πΎ) = (((πΎβ(π β 1)) Β· πΎ) Β· πΎ)) |
214 | 144, 143,
143 | mulassd 11183 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((πΎβ(π β 1)) Β· πΎ) Β· πΎ) = ((πΎβ(π β 1)) Β· (πΎ Β· πΎ))) |
215 | 134 | addid2d 11361 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (0 +
(πΎβ2)) = (πΎβ2)) |
216 | 29 | sqvald 14054 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (πΎβ2) = (πΎ Β· πΎ)) |
217 | 215, 216 | eqtr2d 2774 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0) β (πΎ Β· πΎ) = (0 + (πΎβ2))) |
218 | 217 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (πΎ Β· πΎ) = (0 + (πΎβ2))) |
219 | 218 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((πΎβ(π β 1)) Β· (πΎ Β· πΎ)) = ((πΎβ(π β 1)) Β· (0 + (πΎβ2)))) |
220 | 214, 219 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((πΎβ(π β 1)) Β· πΎ) Β· πΎ) = ((πΎβ(π β 1)) Β· (0 + (πΎβ2)))) |
221 | 204, 213,
220 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (πΎβ(π + 1)) = ((πΎβ(π β 1)) Β· (0 + (πΎβ2)))) |
222 | 203, 221 | oveq12d 7376 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β (((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) β (πΎβ(π + 1))) = ((((2 Β· π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) β ((πΎβ(π β 1)) Β· (0 + (πΎβ2))))) |
223 | 222 | adantr 482 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β (((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) β (πΎβ(π + 1))) = ((((2 Β· π΄) Β· ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) β ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) β ((πΎβ(π β 1)) Β· (0 + (πΎβ2))))) |
224 | 163, 223 | breqtrrd 5134 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β§ (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) β (πΎβ(π + 1)))) |
225 | 224 | ex 414 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β) β ((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) β (πΎβ(π + 1))))) |
226 | 225 | expcom 415 |
. . . . . 6
β’ (π β β β ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) β (πΎβ(π + 1)))))) |
227 | 226 | a2d 29 |
. . . . 5
β’ (π β β β (((π΄ β
(β€β₯β2) β§ πΎ β β0) β (((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))) β§ ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β ((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) β (πΎβ(π + 1)))))) |
228 | 51, 227 | syl5 34 |
. . . 4
β’ (π β β β ((((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1)))) β§ ((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) β ((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) β (πΎβ(π + 1)))))) |
229 | | oveq2 7366 |
. . . . . . . 8
β’ (π = 0 β (π΄ Xrm π) = (π΄ Xrm 0)) |
230 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = 0 β (π΄ Yrm π) = (π΄ Yrm 0)) |
231 | 230 | oveq2d 7374 |
. . . . . . . 8
β’ (π = 0 β ((π΄ β πΎ) Β· (π΄ Yrm π)) = ((π΄ β πΎ) Β· (π΄ Yrm 0))) |
232 | 229, 231 | oveq12d 7376 |
. . . . . . 7
β’ (π = 0 β ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) = ((π΄ Xrm 0) β ((π΄ β πΎ) Β· (π΄ Yrm 0)))) |
233 | | oveq2 7366 |
. . . . . . 7
β’ (π = 0 β (πΎβπ) = (πΎβ0)) |
234 | 232, 233 | oveq12d 7376 |
. . . . . 6
β’ (π = 0 β (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)) = (((π΄ Xrm 0) β ((π΄ β πΎ) Β· (π΄ Yrm 0))) β (πΎβ0))) |
235 | 234 | breq2d 5118 |
. . . . 5
β’ (π = 0 β (((((2 Β·
π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm 0) β
((π΄ β πΎ) Β· (π΄ Yrm 0))) β (πΎβ0)))) |
236 | 235 | imbi2d 341 |
. . . 4
β’ (π = 0 β (((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β ((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm 0) β
((π΄ β πΎ) Β· (π΄ Yrm 0))) β (πΎβ0))))) |
237 | | oveq2 7366 |
. . . . . . . 8
β’ (π = 1 β (π΄ Xrm π) = (π΄ Xrm 1)) |
238 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = 1 β (π΄ Yrm π) = (π΄ Yrm 1)) |
239 | 238 | oveq2d 7374 |
. . . . . . . 8
β’ (π = 1 β ((π΄ β πΎ) Β· (π΄ Yrm π)) = ((π΄ β πΎ) Β· (π΄ Yrm 1))) |
240 | 237, 239 | oveq12d 7376 |
. . . . . . 7
β’ (π = 1 β ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) = ((π΄ Xrm 1) β ((π΄ β πΎ) Β· (π΄ Yrm 1)))) |
241 | | oveq2 7366 |
. . . . . . 7
β’ (π = 1 β (πΎβπ) = (πΎβ1)) |
242 | 240, 241 | oveq12d 7376 |
. . . . . 6
β’ (π = 1 β (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)) = (((π΄ Xrm 1) β ((π΄ β πΎ) Β· (π΄ Yrm 1))) β (πΎβ1))) |
243 | 242 | breq2d 5118 |
. . . . 5
β’ (π = 1 β (((((2 Β·
π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm 1) β
((π΄ β πΎ) Β· (π΄ Yrm 1))) β (πΎβ1)))) |
244 | 243 | imbi2d 341 |
. . . 4
β’ (π = 1 β (((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β ((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm 1) β
((π΄ β πΎ) Β· (π΄ Yrm 1))) β (πΎβ1))))) |
245 | | oveq2 7366 |
. . . . . . . 8
β’ (π = (π β 1) β (π΄ Xrm π) = (π΄ Xrm (π β 1))) |
246 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = (π β 1) β (π΄ Yrm π) = (π΄ Yrm (π β 1))) |
247 | 246 | oveq2d 7374 |
. . . . . . . 8
β’ (π = (π β 1) β ((π΄ β πΎ) Β· (π΄ Yrm π)) = ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) |
248 | 245, 247 | oveq12d 7376 |
. . . . . . 7
β’ (π = (π β 1) β ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) = ((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1))))) |
249 | | oveq2 7366 |
. . . . . . 7
β’ (π = (π β 1) β (πΎβπ) = (πΎβ(π β 1))) |
250 | 248, 249 | oveq12d 7376 |
. . . . . 6
β’ (π = (π β 1) β (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)) = (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1)))) |
251 | 250 | breq2d 5118 |
. . . . 5
β’ (π = (π β 1) β (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1))))) |
252 | 251 | imbi2d 341 |
. . . 4
β’ (π = (π β 1) β (((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β ((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π β 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π β 1)))) β (πΎβ(π β 1)))))) |
253 | | oveq2 7366 |
. . . . . . . 8
β’ (π = π β (π΄ Xrm π) = (π΄ Xrm π)) |
254 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = π β (π΄ Yrm π) = (π΄ Yrm π)) |
255 | 254 | oveq2d 7374 |
. . . . . . . 8
β’ (π = π β ((π΄ β πΎ) Β· (π΄ Yrm π)) = ((π΄ β πΎ) Β· (π΄ Yrm π))) |
256 | 253, 255 | oveq12d 7376 |
. . . . . . 7
β’ (π = π β ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) = ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) |
257 | | oveq2 7366 |
. . . . . . 7
β’ (π = π β (πΎβπ) = (πΎβπ)) |
258 | 256, 257 | oveq12d 7376 |
. . . . . 6
β’ (π = π β (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)) = (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) |
259 | 258 | breq2d 5118 |
. . . . 5
β’ (π = π β (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) |
260 | 259 | imbi2d 341 |
. . . 4
β’ (π = π β (((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β ((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))))) |
261 | | oveq2 7366 |
. . . . . . . 8
β’ (π = (π + 1) β (π΄ Xrm π) = (π΄ Xrm (π + 1))) |
262 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = (π + 1) β (π΄ Yrm π) = (π΄ Yrm (π + 1))) |
263 | 262 | oveq2d 7374 |
. . . . . . . 8
β’ (π = (π + 1) β ((π΄ β πΎ) Β· (π΄ Yrm π)) = ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) |
264 | 261, 263 | oveq12d 7376 |
. . . . . . 7
β’ (π = (π + 1) β ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) = ((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1))))) |
265 | | oveq2 7366 |
. . . . . . 7
β’ (π = (π + 1) β (πΎβπ) = (πΎβ(π + 1))) |
266 | 264, 265 | oveq12d 7376 |
. . . . . 6
β’ (π = (π + 1) β (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)) = (((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) β (πΎβ(π + 1)))) |
267 | 266 | breq2d 5118 |
. . . . 5
β’ (π = (π + 1) β (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) β (πΎβ(π + 1))))) |
268 | 267 | imbi2d 341 |
. . . 4
β’ (π = (π + 1) β (((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β ((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm (π + 1)) β ((π΄ β πΎ) Β· (π΄ Yrm (π + 1)))) β (πΎβ(π + 1)))))) |
269 | | oveq2 7366 |
. . . . . . . 8
β’ (π = π β (π΄ Xrm π) = (π΄ Xrm π)) |
270 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = π β (π΄ Yrm π) = (π΄ Yrm π)) |
271 | 270 | oveq2d 7374 |
. . . . . . . 8
β’ (π = π β ((π΄ β πΎ) Β· (π΄ Yrm π)) = ((π΄ β πΎ) Β· (π΄ Yrm π))) |
272 | 269, 271 | oveq12d 7376 |
. . . . . . 7
β’ (π = π β ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) = ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π)))) |
273 | | oveq2 7366 |
. . . . . . 7
β’ (π = π β (πΎβπ) = (πΎβπ)) |
274 | 272, 273 | oveq12d 7376 |
. . . . . 6
β’ (π = π β (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)) = (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) |
275 | 274 | breq2d 5118 |
. . . . 5
β’ (π = π β (((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) |
276 | 275 | imbi2d 341 |
. . . 4
β’ (π = π β (((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) β ((π΄ β (β€β₯β2)
β§ πΎ β
β0) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))))) |
277 | 34, 50, 228, 236, 244, 252, 260, 268, 276 | 2nn0ind 41312 |
. . 3
β’ (π β β0
β ((π΄ β
(β€β₯β2) β§ πΎ β β0) β ((((2
Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ)))) |
278 | 277 | impcom 409 |
. 2
β’ (((π΄ β
(β€β₯β2) β§ πΎ β β0) β§ π β β0)
β ((((2 Β· π΄)
Β· πΎ) β (πΎβ2)) β 1) β₯
(((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) |
279 | 278 | 3impa 1111 |
1
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0 β§ π β β0)
β ((((2 Β· π΄)
Β· πΎ) β (πΎβ2)) β 1) β₯
(((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) |