Step | Hyp | Ref
| Expression |
1 | | 2re 12287 |
. . . . . 6
β’ 2 β
β |
2 | | eluzelre 12834 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
3 | 2 | adantr 480 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π΄ β β) |
4 | | remulcl 11194 |
. . . . . 6
β’ ((2
β β β§ π΄
β β) β (2 Β· π΄) β β) |
5 | 1, 3, 4 | sylancr 586 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (2 Β· π΄) β
β) |
6 | | nnz 12580 |
. . . . . . . 8
β’ (π β β β π β
β€) |
7 | 6 | adantl 481 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π β β€) |
8 | 7 | peano2zd 12670 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π + 1) β β€) |
9 | | frmy 42213 |
. . . . . . . 8
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
10 | 9 | fovcl 7532 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ (π + 1) β β€) β (π΄ Yrm (π + 1)) β
β€) |
11 | 10 | zred 12667 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ (π + 1) β β€) β (π΄ Yrm (π + 1)) β
β) |
12 | 8, 11 | syldan 590 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm (π + 1)) β β) |
13 | 5, 12 | remulcld 11245 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β β) |
14 | | nncn 12221 |
. . . . . . . 8
β’ (π β β β π β
β) |
15 | 14 | adantl 481 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π β β) |
16 | | ax-1cn 11167 |
. . . . . . 7
β’ 1 β
β |
17 | | pncan 11467 |
. . . . . . 7
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
18 | 15, 16, 17 | sylancl 585 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π + 1) β 1) = π) |
19 | 18 | oveq2d 7420 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm ((π + 1) β 1)) = (π΄ Yrm π)) |
20 | 9 | fovcl 7532 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
21 | 20 | zred 12667 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β) |
22 | 6, 21 | sylan2 592 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm π) β β) |
23 | 19, 22 | eqeltrd 2827 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm ((π + 1) β 1)) β
β) |
24 | 13, 23 | resubcld 11643 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β (π΄ Yrm ((π + 1) β 1))) β
β) |
25 | | nnnn0 12480 |
. . . . . 6
β’ (π β β β π β
β0) |
26 | 25 | adantl 481 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π β
β0) |
27 | 5, 26 | reexpcld 14130 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((2 Β· π΄)βπ) β β) |
28 | 5, 27 | remulcld 11245 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((2 Β· π΄) Β· ((2 Β· π΄)βπ)) β β) |
29 | | rmy0 42228 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β (π΄ Yrm 0) = 0) |
30 | 29 | adantr 480 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm 0) = 0) |
31 | | nngt0 12244 |
. . . . . . . 8
β’ (π β β β 0 <
π) |
32 | 31 | adantl 481 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β 0 < π) |
33 | | simpl 482 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π΄ β
(β€β₯β2)) |
34 | | 0zd 12571 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β) β 0 β
β€) |
35 | | ltrmy 42251 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ 0 β β€ β§ π β β€) β (0 < π β (π΄ Yrm 0) < (π΄ Yrm π))) |
36 | 33, 34, 7, 35 | syl3anc 1368 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (0 < π β (π΄ Yrm 0) < (π΄ Yrm π))) |
37 | 32, 36 | mpbid 231 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm 0) < (π΄ Yrm π)) |
38 | 30, 37 | eqbrtrrd 5165 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β 0 < (π΄ Yrm π)) |
39 | 38, 19 | breqtrrd 5169 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β 0 < (π΄ Yrm ((π + 1) β
1))) |
40 | 23, 13 | ltsubposd 11801 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (0 < (π΄ Yrm ((π + 1) β 1)) β (((2
Β· π΄) Β· (π΄ Yrm (π + 1))) β (π΄ Yrm ((π + 1) β 1))) < ((2
Β· π΄) Β· (π΄ Yrm (π + 1))))) |
41 | 39, 40 | mpbid 231 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β (π΄ Yrm ((π + 1) β 1))) < ((2 Β· π΄) Β· (π΄ Yrm (π + 1)))) |
42 | | jm2.17b 42260 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Yrm (π + 1)) β€ ((2 Β· π΄)βπ)) |
43 | 25, 42 | sylan2 592 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm (π + 1)) β€ ((2 Β· π΄)βπ)) |
44 | | 2nn 12286 |
. . . . . . . 8
β’ 2 β
β |
45 | | eluz2nn 12869 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
46 | | nnmulcl 12237 |
. . . . . . . 8
β’ ((2
β β β§ π΄
β β) β (2 Β· π΄) β β) |
47 | 44, 45, 46 | sylancr 586 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β (2 Β· π΄) β β) |
48 | 47 | nngt0d 12262 |
. . . . . 6
β’ (π΄ β
(β€β₯β2) β 0 < (2 Β· π΄)) |
49 | 48 | adantr 480 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β) β 0 < (2 Β·
π΄)) |
50 | | lemul2 12068 |
. . . . 5
β’ (((π΄ Yrm (π + 1)) β β β§ ((2
Β· π΄)βπ) β β β§ ((2
Β· π΄) β β
β§ 0 < (2 Β· π΄))) β ((π΄ Yrm (π + 1)) β€ ((2 Β· π΄)βπ) β ((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β€ ((2 Β· π΄) Β· ((2 Β· π΄)βπ)))) |
51 | 12, 27, 5, 49, 50 | syl112anc 1371 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((π΄ Yrm (π + 1)) β€ ((2 Β· π΄)βπ) β ((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β€ ((2 Β· π΄) Β· ((2 Β· π΄)βπ)))) |
52 | 43, 51 | mpbid 231 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β€ ((2 Β· π΄) Β· ((2 Β· π΄)βπ))) |
53 | 24, 13, 28, 41, 52 | ltletrd 11375 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β (π΄ Yrm ((π + 1) β 1))) < ((2 Β· π΄) Β· ((2 Β· π΄)βπ))) |
54 | | rmyluc2 42237 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ (π + 1) β β€) β (π΄ Yrm ((π + 1) + 1)) = (((2 Β·
π΄) Β· (π΄ Yrm (π + 1))) β (π΄ Yrm ((π + 1) β
1)))) |
55 | 8, 54 | syldan 590 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm ((π + 1) + 1)) = (((2 Β· π΄) Β· (π΄ Yrm (π + 1))) β (π΄ Yrm ((π + 1) β 1)))) |
56 | 5 | recnd 11243 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (2 Β· π΄) β
β) |
57 | 56, 26 | expp1d 14114 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((2 Β· π΄)β(π + 1)) = (((2 Β· π΄)βπ) Β· (2 Β· π΄))) |
58 | 27 | recnd 11243 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((2 Β· π΄)βπ) β β) |
59 | 58, 56 | mulcomd 11236 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (((2 Β· π΄)βπ) Β· (2 Β· π΄)) = ((2 Β· π΄) Β· ((2 Β· π΄)βπ))) |
60 | 57, 59 | eqtrd 2766 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β) β ((2 Β· π΄)β(π + 1)) = ((2 Β· π΄) Β· ((2 Β· π΄)βπ))) |
61 | 53, 55, 60 | 3brtr4d 5173 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β) β (π΄ Yrm ((π + 1) + 1)) < ((2 Β· π΄)β(π + 1))) |