Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . . 5
β’ (π = 0 β (((2 Β· π΄) β 1)βπ) = (((2 Β· π΄) β
1)β0)) |
2 | | oveq1 7365 |
. . . . . 6
β’ (π = 0 β (π + 1) = (0 + 1)) |
3 | 2 | oveq2d 7374 |
. . . . 5
β’ (π = 0 β (π΄ Yrm (π + 1)) = (π΄ Yrm (0 + 1))) |
4 | 1, 3 | breq12d 5119 |
. . . 4
β’ (π = 0 β ((((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1)) β (((2 Β· π΄) β 1)β0) β€ (π΄ Yrm (0 + 1)))) |
5 | 4 | imbi2d 341 |
. . 3
β’ (π = 0 β ((π΄ β (β€β₯β2)
β (((2 Β· π΄)
β 1)βπ) β€
(π΄ Yrm (π + 1))) β (π΄ β
(β€β₯β2) β (((2 Β· π΄) β 1)β0) β€ (π΄ Yrm (0 + 1))))) |
6 | | oveq2 7366 |
. . . . 5
β’ (π = π β (((2 Β· π΄) β 1)βπ) = (((2 Β· π΄) β 1)βπ)) |
7 | | oveq1 7365 |
. . . . . 6
β’ (π = π β (π + 1) = (π + 1)) |
8 | 7 | oveq2d 7374 |
. . . . 5
β’ (π = π β (π΄ Yrm (π + 1)) = (π΄ Yrm (π + 1))) |
9 | 6, 8 | breq12d 5119 |
. . . 4
β’ (π = π β ((((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1)) β (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1)))) |
10 | 9 | imbi2d 341 |
. . 3
β’ (π = π β ((π΄ β (β€β₯β2)
β (((2 Β· π΄)
β 1)βπ) β€
(π΄ Yrm (π + 1))) β (π΄ β
(β€β₯β2) β (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))))) |
11 | | oveq2 7366 |
. . . . 5
β’ (π = (π + 1) β (((2 Β· π΄) β 1)βπ) = (((2 Β· π΄) β 1)β(π + 1))) |
12 | | oveq1 7365 |
. . . . . 6
β’ (π = (π + 1) β (π + 1) = ((π + 1) + 1)) |
13 | 12 | oveq2d 7374 |
. . . . 5
β’ (π = (π + 1) β (π΄ Yrm (π + 1)) = (π΄ Yrm ((π + 1) + 1))) |
14 | 11, 13 | breq12d 5119 |
. . . 4
β’ (π = (π + 1) β ((((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1)) β (((2 Β· π΄) β 1)β(π + 1)) β€ (π΄ Yrm ((π + 1) + 1)))) |
15 | 14 | imbi2d 341 |
. . 3
β’ (π = (π + 1) β ((π΄ β (β€β₯β2)
β (((2 Β· π΄)
β 1)βπ) β€
(π΄ Yrm (π + 1))) β (π΄ β
(β€β₯β2) β (((2 Β· π΄) β 1)β(π + 1)) β€ (π΄ Yrm ((π + 1) + 1))))) |
16 | | oveq2 7366 |
. . . . 5
β’ (π = π β (((2 Β· π΄) β 1)βπ) = (((2 Β· π΄) β 1)βπ)) |
17 | | oveq1 7365 |
. . . . . 6
β’ (π = π β (π + 1) = (π + 1)) |
18 | 17 | oveq2d 7374 |
. . . . 5
β’ (π = π β (π΄ Yrm (π + 1)) = (π΄ Yrm (π + 1))) |
19 | 16, 18 | breq12d 5119 |
. . . 4
β’ (π = π β ((((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1)) β (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1)))) |
20 | 19 | imbi2d 341 |
. . 3
β’ (π = π β ((π΄ β (β€β₯β2)
β (((2 Β· π΄)
β 1)βπ) β€
(π΄ Yrm (π + 1))) β (π΄ β
(β€β₯β2) β (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))))) |
21 | | 1le1 11788 |
. . . . 5
β’ 1 β€
1 |
22 | 21 | a1i 11 |
. . . 4
β’ (π΄ β
(β€β₯β2) β 1 β€ 1) |
23 | | 2cn 12233 |
. . . . . . 7
β’ 2 β
β |
24 | | eluzelcn 12780 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
25 | | mulcl 11140 |
. . . . . . 7
β’ ((2
β β β§ π΄
β β) β (2 Β· π΄) β β) |
26 | 23, 24, 25 | sylancr 588 |
. . . . . 6
β’ (π΄ β
(β€β₯β2) β (2 Β· π΄) β β) |
27 | | ax-1cn 11114 |
. . . . . 6
β’ 1 β
β |
28 | | subcl 11405 |
. . . . . 6
β’ (((2
Β· π΄) β β
β§ 1 β β) β ((2 Β· π΄) β 1) β
β) |
29 | 26, 27, 28 | sylancl 587 |
. . . . 5
β’ (π΄ β
(β€β₯β2) β ((2 Β· π΄) β 1) β
β) |
30 | 29 | exp0d 14051 |
. . . 4
β’ (π΄ β
(β€β₯β2) β (((2 Β· π΄) β 1)β0) = 1) |
31 | | 0p1e1 12280 |
. . . . . 6
β’ (0 + 1) =
1 |
32 | 31 | oveq2i 7369 |
. . . . 5
β’ (π΄ Yrm (0 + 1)) =
(π΄ Yrm
1) |
33 | | rmy1 41297 |
. . . . 5
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm 1) = 1) |
34 | 32, 33 | eqtrid 2785 |
. . . 4
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm (0 + 1)) =
1) |
35 | 22, 30, 34 | 3brtr4d 5138 |
. . 3
β’ (π΄ β
(β€β₯β2) β (((2 Β· π΄) β 1)β0) β€ (π΄ Yrm (0 + 1))) |
36 | | 2re 12232 |
. . . . . . . . . 10
β’ 2 β
β |
37 | | eluzelre 12779 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
38 | 37 | adantl 483 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β π΄ β β) |
39 | | remulcl 11141 |
. . . . . . . . . 10
β’ ((2
β β β§ π΄
β β) β (2 Β· π΄) β β) |
40 | 36, 38, 39 | sylancr 588 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (2 Β· π΄) β β) |
41 | | 1re 11160 |
. . . . . . . . 9
β’ 1 β
β |
42 | | resubcl 11470 |
. . . . . . . . 9
β’ (((2
Β· π΄) β β
β§ 1 β β) β ((2 Β· π΄) β 1) β
β) |
43 | 40, 41, 42 | sylancl 587 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β ((2 Β· π΄) β 1) β
β) |
44 | | peano2nn0 12458 |
. . . . . . . . 9
β’ (π β β0
β (π + 1) β
β0) |
45 | 44 | adantr 482 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (π + 1) β
β0) |
46 | 43, 45 | reexpcld 14074 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (((2 Β· π΄) β 1)β(π + 1)) β β) |
47 | 46 | 3adant3 1133 |
. . . . . 6
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) β (((2 Β· π΄) β 1)β(π + 1)) β
β) |
48 | | simpr 486 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β π΄ β
(β€β₯β2)) |
49 | | nn0z 12529 |
. . . . . . . . . . 11
β’ (π β β0
β π β
β€) |
50 | 49 | adantr 482 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β π β β€) |
51 | 50 | peano2zd 12615 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (π + 1) β β€) |
52 | | frmy 41281 |
. . . . . . . . . . 11
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
53 | 52 | fovcl 7485 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ (π + 1) β β€) β (π΄ Yrm (π + 1)) β
β€) |
54 | 53 | zred 12612 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ (π + 1) β β€) β (π΄ Yrm (π + 1)) β
β) |
55 | 48, 51, 54 | syl2anc 585 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (π΄ Yrm (π + 1)) β β) |
56 | 55, 43 | remulcld 11190 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β ((π΄ Yrm (π + 1)) Β· ((2 Β· π΄) β 1)) β
β) |
57 | 56 | 3adant3 1133 |
. . . . . 6
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) β ((π΄ Yrm (π + 1)) Β· ((2 Β· π΄) β 1)) β
β) |
58 | 51 | peano2zd 12615 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β ((π + 1) + 1) β β€) |
59 | 52 | fovcl 7485 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ ((π + 1) + 1) β β€) β (π΄ Yrm ((π + 1) + 1)) β
β€) |
60 | 59 | zred 12612 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ ((π + 1) + 1) β β€) β (π΄ Yrm ((π + 1) + 1)) β
β) |
61 | 48, 58, 60 | syl2anc 585 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (π΄ Yrm ((π + 1) + 1)) β β) |
62 | 61 | 3adant3 1133 |
. . . . . 6
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) β (π΄ Yrm ((π + 1) + 1)) β β) |
63 | 29 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) β ((2 Β· π΄) β 1) β
β) |
64 | | simp1 1137 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) β π β β0) |
65 | 63, 64 | expp1d 14058 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) β (((2 Β· π΄) β 1)β(π + 1)) = ((((2 Β· π΄) β 1)βπ) Β· ((2 Β· π΄) β 1))) |
66 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β π β β0) |
67 | 43, 66 | reexpcld 14074 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (((2 Β· π΄) β 1)βπ) β β) |
68 | | 2nn 12231 |
. . . . . . . . . . . 12
β’ 2 β
β |
69 | | eluz2nn 12814 |
. . . . . . . . . . . . 13
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
70 | 69 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β π΄ β β) |
71 | | nnmulcl 12182 |
. . . . . . . . . . . 12
β’ ((2
β β β§ π΄
β β) β (2 Β· π΄) β β) |
72 | 68, 70, 71 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (2 Β· π΄) β β) |
73 | | nnm1nn0 12459 |
. . . . . . . . . . 11
β’ ((2
Β· π΄) β β
β ((2 Β· π΄)
β 1) β β0) |
74 | | nn0ge0 12443 |
. . . . . . . . . . 11
β’ (((2
Β· π΄) β 1)
β β0 β 0 β€ ((2 Β· π΄) β 1)) |
75 | 72, 73, 74 | 3syl 18 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β 0 β€ ((2 Β· π΄) β 1)) |
76 | 43, 75 | jca 513 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (((2 Β· π΄) β 1) β β β§ 0 β€ ((2
Β· π΄) β
1))) |
77 | 67, 55, 76 | 3jca 1129 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β ((((2 Β· π΄) β 1)βπ) β β β§ (π΄ Yrm (π + 1)) β β β§ (((2 Β·
π΄) β 1) β
β β§ 0 β€ ((2 Β· π΄) β 1)))) |
78 | | lemul1a 12014 |
. . . . . . . 8
β’ ((((((2
Β· π΄) β
1)βπ) β β
β§ (π΄ Yrm
(π + 1)) β β
β§ (((2 Β· π΄)
β 1) β β β§ 0 β€ ((2 Β· π΄) β 1))) β§ (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) β ((((2 Β· π΄) β 1)βπ) Β· ((2 Β· π΄) β 1)) β€ ((π΄ Yrm (π + 1)) Β· ((2 Β·
π΄) β
1))) |
79 | 77, 78 | stoic3 1779 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) β ((((2 Β· π΄) β 1)βπ) Β· ((2 Β· π΄) β 1)) β€ ((π΄ Yrm (π + 1)) Β· ((2 Β·
π΄) β
1))) |
80 | 65, 79 | eqbrtrd 5128 |
. . . . . 6
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) β (((2 Β· π΄) β 1)β(π + 1)) β€ ((π΄ Yrm (π + 1)) Β· ((2 Β· π΄) β 1))) |
81 | | nn0cn 12428 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β) |
82 | 81 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β π β β) |
83 | | pncan 11412 |
. . . . . . . . . . . 12
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
84 | 82, 27, 83 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β ((π + 1) β 1) = π) |
85 | 84 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (π΄ Yrm ((π + 1) β 1)) = (π΄ Yrm π)) |
86 | 52 | fovcl 7485 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
87 | 86 | zred 12612 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β) |
88 | 48, 50, 87 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (π΄ Yrm π) β β) |
89 | 85, 88 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (π΄ Yrm ((π + 1) β 1)) β
β) |
90 | | remulcl 11141 |
. . . . . . . . . 10
β’ (((π΄ Yrm (π + 1)) β β β§ 1
β β) β ((π΄
Yrm (π + 1))
Β· 1) β β) |
91 | 55, 41, 90 | sylancl 587 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β ((π΄ Yrm (π + 1)) Β· 1) β
β) |
92 | 40, 55 | remulcld 11190 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β ((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β β) |
93 | | nn0re 12427 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β) |
94 | 93 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β π β β) |
95 | 94 | lep1d 12091 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β π β€ (π + 1)) |
96 | | lermy 41322 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ (π + 1) β β€) β (π β€ (π + 1) β (π΄ Yrm π) β€ (π΄ Yrm (π + 1)))) |
97 | 48, 50, 51, 96 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (π β€ (π + 1) β (π΄ Yrm π) β€ (π΄ Yrm (π + 1)))) |
98 | 95, 97 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (π΄ Yrm π) β€ (π΄ Yrm (π + 1))) |
99 | 55 | recnd 11188 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (π΄ Yrm (π + 1)) β β) |
100 | 99 | mulid1d 11177 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β ((π΄ Yrm (π + 1)) Β· 1) = (π΄ Yrm (π + 1))) |
101 | 98, 85, 100 | 3brtr4d 5138 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (π΄ Yrm ((π + 1) β 1)) β€ ((π΄ Yrm (π + 1)) Β· 1)) |
102 | 89, 91, 92, 101 | lesub2dd 11777 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β ((π΄ Yrm (π + 1)) Β· 1)) β€ (((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β (π΄ Yrm ((π + 1) β 1)))) |
103 | 40 | recnd 11188 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (2 Β· π΄) β β) |
104 | 27 | a1i 11 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β 1 β β) |
105 | 99, 103, 104 | subdid 11616 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β ((π΄ Yrm (π + 1)) Β· ((2 Β· π΄) β 1)) = (((π΄ Yrm (π + 1)) Β· (2 Β·
π΄)) β ((π΄ Yrm (π + 1)) Β·
1))) |
106 | 99, 103 | mulcomd 11181 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β ((π΄ Yrm (π + 1)) Β· (2 Β· π΄)) = ((2 Β· π΄) Β· (π΄ Yrm (π + 1)))) |
107 | 106 | oveq1d 7373 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (((π΄ Yrm (π + 1)) Β· (2 Β· π΄)) β ((π΄ Yrm (π + 1)) Β· 1)) = (((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β ((π΄ Yrm (π + 1)) Β· 1))) |
108 | 105, 107 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β ((π΄ Yrm (π + 1)) Β· ((2 Β· π΄) β 1)) = (((2 Β·
π΄) Β· (π΄ Yrm (π + 1))) β ((π΄ Yrm (π + 1)) Β·
1))) |
109 | | rmyluc2 41305 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ (π + 1) β β€) β (π΄ Yrm ((π + 1) + 1)) = (((2 Β·
π΄) Β· (π΄ Yrm (π + 1))) β (π΄ Yrm ((π + 1) β
1)))) |
110 | 48, 51, 109 | syl2anc 585 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β (π΄ Yrm ((π + 1) + 1)) = (((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β (π΄ Yrm ((π + 1) β 1)))) |
111 | 102, 108,
110 | 3brtr4d 5138 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β
(β€β₯β2)) β ((π΄ Yrm (π + 1)) Β· ((2 Β· π΄) β 1)) β€ (π΄ Yrm ((π + 1) + 1))) |
112 | 111 | 3adant3 1133 |
. . . . . 6
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) β ((π΄ Yrm (π + 1)) Β· ((2 Β· π΄) β 1)) β€ (π΄ Yrm ((π + 1) + 1))) |
113 | 47, 57, 62, 80, 112 | letrd 11317 |
. . . . 5
β’ ((π β β0
β§ π΄ β
(β€β₯β2) β§ (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) β (((2 Β· π΄) β 1)β(π + 1)) β€ (π΄ Yrm ((π + 1) + 1))) |
114 | 113 | 3exp 1120 |
. . . 4
β’ (π β β0
β (π΄ β
(β€β₯β2) β ((((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1)) β (((2 Β· π΄) β 1)β(π + 1)) β€ (π΄ Yrm ((π + 1) + 1))))) |
115 | 114 | a2d 29 |
. . 3
β’ (π β β0
β ((π΄ β
(β€β₯β2) β (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) β (π΄ β (β€β₯β2)
β (((2 Β· π΄)
β 1)β(π + 1))
β€ (π΄ Yrm
((π + 1) +
1))))) |
116 | 5, 10, 15, 20, 35, 115 | nn0ind 12603 |
. 2
β’ (π β β0
β (π΄ β
(β€β₯β2) β (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1)))) |
117 | 116 | impcom 409 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (((2
Β· π΄) β
1)βπ) β€ (π΄ Yrm (π + 1))) |