Step | Hyp | Ref
| Expression |
1 | | fltltc.n |
. . . 4
โข (๐ โ ๐ โ
(โคโฅโ3)) |
2 | | eluzge3nn 12873 |
. . . 4
โข (๐ โ
(โคโฅโ3) โ ๐ โ โ) |
3 | 1, 2 | syl 17 |
. . 3
โข (๐ โ ๐ โ โ) |
4 | 3 | nnred 12226 |
. 2
โข (๐ โ ๐ โ โ) |
5 | | fltltc.c |
. . . . . 6
โข (๐ โ ๐ถ โ โ) |
6 | 5 | nnred 12226 |
. . . . 5
โข (๐ โ ๐ถ โ โ) |
7 | | fltltc.b |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
8 | 7 | nnred 12226 |
. . . . 5
โข (๐ โ ๐ต โ โ) |
9 | 6, 8 | resubcld 11641 |
. . . 4
โข (๐ โ (๐ถ โ ๐ต) โ โ) |
10 | | uzuzle23 12872 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ3) โ ๐ โ
(โคโฅโ2)) |
11 | | uz2m1nn 12906 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
12 | 1, 10, 11 | 3syl 18 |
. . . . . . 7
โข (๐ โ (๐ โ 1) โ โ) |
13 | 12 | nnnn0d 12531 |
. . . . . 6
โข (๐ โ (๐ โ 1) โ
โ0) |
14 | 6, 13 | reexpcld 14127 |
. . . . 5
โข (๐ โ (๐ถโ(๐ โ 1)) โ
โ) |
15 | 12 | nnred 12226 |
. . . . . 6
โข (๐ โ (๐ โ 1) โ โ) |
16 | 8, 13 | reexpcld 14127 |
. . . . . 6
โข (๐ โ (๐ตโ(๐ โ 1)) โ
โ) |
17 | 15, 16 | remulcld 11243 |
. . . . 5
โข (๐ โ ((๐ โ 1) ยท (๐ตโ(๐ โ 1))) โ
โ) |
18 | 14, 17 | readdcld 11242 |
. . . 4
โข (๐ โ ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) โ
โ) |
19 | 9, 18 | remulcld 11243 |
. . 3
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) โ
โ) |
20 | | fltltc.a |
. . . . 5
โข (๐ โ ๐ด โ โ) |
21 | 20 | nnrpd 13013 |
. . . 4
โข (๐ โ ๐ด โ
โ+) |
22 | 12 | nnzd 12584 |
. . . 4
โข (๐ โ (๐ โ 1) โ โค) |
23 | 21, 22 | rpexpcld 14209 |
. . 3
โข (๐ โ (๐ดโ(๐ โ 1)) โ
โ+) |
24 | 19, 23 | rerpdivcld 13046 |
. 2
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1))) โ
โ) |
25 | 20 | nnred 12226 |
. 2
โข (๐ โ ๐ด โ โ) |
26 | 16, 17 | readdcld 11242 |
. . . . 5
โข (๐ โ ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) โ
โ) |
27 | 9, 26 | remulcld 11243 |
. . . 4
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) โ
โ) |
28 | 27, 23 | rerpdivcld 13046 |
. . 3
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1))) โ
โ) |
29 | 9, 4 | remulcld 11243 |
. . . . 5
โข (๐ โ ((๐ถ โ ๐ต) ยท ๐) โ โ) |
30 | | 1cnd 11208 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ) |
31 | 12 | nncnd 12227 |
. . . . . . . . . 10
โข (๐ โ (๐ โ 1) โ โ) |
32 | 16 | recnd 11241 |
. . . . . . . . . 10
โข (๐ โ (๐ตโ(๐ โ 1)) โ
โ) |
33 | 30, 31, 32 | adddird 11238 |
. . . . . . . . 9
โข (๐ โ ((1 + (๐ โ 1)) ยท (๐ตโ(๐ โ 1))) = ((1 ยท (๐ตโ(๐ โ 1))) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) |
34 | 3 | nncnd 12227 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
35 | 30, 34 | pncan3d 11573 |
. . . . . . . . . 10
โข (๐ โ (1 + (๐ โ 1)) = ๐) |
36 | 35 | oveq1d 7423 |
. . . . . . . . 9
โข (๐ โ ((1 + (๐ โ 1)) ยท (๐ตโ(๐ โ 1))) = (๐ ยท (๐ตโ(๐ โ 1)))) |
37 | 32 | mullidd 11231 |
. . . . . . . . . 10
โข (๐ โ (1 ยท (๐ตโ(๐ โ 1))) = (๐ตโ(๐ โ 1))) |
38 | 37 | oveq1d 7423 |
. . . . . . . . 9
โข (๐ โ ((1 ยท (๐ตโ(๐ โ 1))) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) = ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) |
39 | 33, 36, 38 | 3eqtr3rd 2781 |
. . . . . . . 8
โข (๐ โ ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) = (๐ ยท (๐ตโ(๐ โ 1)))) |
40 | 39 | oveq2d 7424 |
. . . . . . 7
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) = ((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1))))) |
41 | 40 | oveq1d 7423 |
. . . . . 6
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1))) = (((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1)))) / (๐ดโ(๐ โ 1)))) |
42 | 41, 28 | eqeltrrd 2834 |
. . . . 5
โข (๐ โ (((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1)))) / (๐ดโ(๐ โ 1))) โ
โ) |
43 | 3 | nnnn0d 12531 |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
44 | 43 | nn0ge0d 12534 |
. . . . . 6
โข (๐ โ 0 โค ๐) |
45 | | 1red 11214 |
. . . . . . 7
โข (๐ โ 1 โ
โ) |
46 | | fltltc.1 |
. . . . . . . . 9
โข (๐ โ ((๐ดโ๐) + (๐ตโ๐)) = (๐ถโ๐)) |
47 | 20, 7, 5, 1, 46 | fltltc 41404 |
. . . . . . . 8
โข (๐ โ ๐ต < ๐ถ) |
48 | | nnltp1le 12617 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต < ๐ถ โ (๐ต + 1) โค ๐ถ)) |
49 | 7, 5, 48 | syl2anc 584 |
. . . . . . . 8
โข (๐ โ (๐ต < ๐ถ โ (๐ต + 1) โค ๐ถ)) |
50 | 47, 49 | mpbid 231 |
. . . . . . 7
โข (๐ โ (๐ต + 1) โค ๐ถ) |
51 | 8 | leidd 11779 |
. . . . . . 7
โข (๐ โ ๐ต โค ๐ต) |
52 | 6, 8, 45, 8, 50, 51 | lesub3d 11831 |
. . . . . 6
โข (๐ โ 1 โค (๐ถ โ ๐ต)) |
53 | 4, 9, 44, 52 | lemulge12d 12151 |
. . . . 5
โข (๐ โ ๐ โค ((๐ถ โ ๐ต) ยท ๐)) |
54 | 9 | recnd 11241 |
. . . . . . . . 9
โข (๐ โ (๐ถ โ ๐ต) โ โ) |
55 | 23 | rpred 13015 |
. . . . . . . . . 10
โข (๐ โ (๐ดโ(๐ โ 1)) โ
โ) |
56 | 55 | recnd 11241 |
. . . . . . . . 9
โข (๐ โ (๐ดโ(๐ โ 1)) โ
โ) |
57 | 54, 34, 56 | mulassd 11236 |
. . . . . . . 8
โข (๐ โ (((๐ถ โ ๐ต) ยท ๐) ยท (๐ดโ(๐ โ 1))) = ((๐ถ โ ๐ต) ยท (๐ ยท (๐ดโ(๐ โ 1))))) |
58 | 57 | oveq1d 7423 |
. . . . . . 7
โข (๐ โ ((((๐ถ โ ๐ต) ยท ๐) ยท (๐ดโ(๐ โ 1))) / (๐ดโ(๐ โ 1))) = (((๐ถ โ ๐ต) ยท (๐ ยท (๐ดโ(๐ โ 1)))) / (๐ดโ(๐ โ 1)))) |
59 | 54, 34 | mulcld 11233 |
. . . . . . . 8
โข (๐ โ ((๐ถ โ ๐ต) ยท ๐) โ โ) |
60 | 20 | nncnd 12227 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
61 | 20 | nnne0d 12261 |
. . . . . . . . 9
โข (๐ โ ๐ด โ 0) |
62 | 60, 61, 22 | expne0d 14116 |
. . . . . . . 8
โข (๐ โ (๐ดโ(๐ โ 1)) โ 0) |
63 | 59, 56, 62 | divcan4d 11995 |
. . . . . . 7
โข (๐ โ ((((๐ถ โ ๐ต) ยท ๐) ยท (๐ดโ(๐ โ 1))) / (๐ดโ(๐ โ 1))) = ((๐ถ โ ๐ต) ยท ๐)) |
64 | 58, 63 | eqtr3d 2774 |
. . . . . 6
โข (๐ โ (((๐ถ โ ๐ต) ยท (๐ ยท (๐ดโ(๐ โ 1)))) / (๐ดโ(๐ โ 1))) = ((๐ถ โ ๐ต) ยท ๐)) |
65 | 4, 55 | remulcld 11243 |
. . . . . . . 8
โข (๐ โ (๐ ยท (๐ดโ(๐ โ 1))) โ
โ) |
66 | 9, 65 | remulcld 11243 |
. . . . . . 7
โข (๐ โ ((๐ถ โ ๐ต) ยท (๐ ยท (๐ดโ(๐ โ 1)))) โ
โ) |
67 | 40, 27 | eqeltrrd 2834 |
. . . . . . 7
โข (๐ โ ((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1)))) โ
โ) |
68 | 39, 26 | eqeltrrd 2834 |
. . . . . . . 8
โข (๐ โ (๐ ยท (๐ตโ(๐ โ 1))) โ
โ) |
69 | | difrp 13011 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต < ๐ถ โ (๐ถ โ ๐ต) โ
โ+)) |
70 | 8, 6, 69 | syl2anc 584 |
. . . . . . . . 9
โข (๐ โ (๐ต < ๐ถ โ (๐ถ โ ๐ต) โ
โ+)) |
71 | 47, 70 | mpbid 231 |
. . . . . . . 8
โข (๐ โ (๐ถ โ ๐ต) โ
โ+) |
72 | 3 | nnrpd 13013 |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ+) |
73 | 7 | nnrpd 13013 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ
โ+) |
74 | | fltnlta.1 |
. . . . . . . . . 10
โข (๐ โ ๐ด < ๐ต) |
75 | 21, 73, 12, 74 | ltexp1dd 41214 |
. . . . . . . . 9
โข (๐ โ (๐ดโ(๐ โ 1)) < (๐ตโ(๐ โ 1))) |
76 | 55, 16, 72, 75 | ltmul2dd 13071 |
. . . . . . . 8
โข (๐ โ (๐ ยท (๐ดโ(๐ โ 1))) < (๐ ยท (๐ตโ(๐ โ 1)))) |
77 | 65, 68, 71, 76 | ltmul2dd 13071 |
. . . . . . 7
โข (๐ โ ((๐ถ โ ๐ต) ยท (๐ ยท (๐ดโ(๐ โ 1)))) < ((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1))))) |
78 | 66, 67, 23, 77 | ltdiv1dd 13072 |
. . . . . 6
โข (๐ โ (((๐ถ โ ๐ต) ยท (๐ ยท (๐ดโ(๐ โ 1)))) / (๐ดโ(๐ โ 1))) < (((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1)))) / (๐ดโ(๐ โ 1)))) |
79 | 64, 78 | eqbrtrrd 5172 |
. . . . 5
โข (๐ โ ((๐ถ โ ๐ต) ยท ๐) < (((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1)))) / (๐ดโ(๐ โ 1)))) |
80 | 4, 29, 42, 53, 79 | lelttrd 11371 |
. . . 4
โข (๐ โ ๐ < (((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1)))) / (๐ดโ(๐ โ 1)))) |
81 | 80, 41 | breqtrrd 5176 |
. . 3
โข (๐ โ ๐ < (((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1)))) |
82 | 5 | nnrpd 13013 |
. . . . . . 7
โข (๐ โ ๐ถ โ
โ+) |
83 | 73, 82, 12, 47 | ltexp1dd 41214 |
. . . . . 6
โข (๐ โ (๐ตโ(๐ โ 1)) < (๐ถโ(๐ โ 1))) |
84 | 16, 14, 17, 83 | ltadd1dd 11824 |
. . . . 5
โข (๐ โ ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) < ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) |
85 | 26, 18, 71, 84 | ltmul2dd 13071 |
. . . 4
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) < ((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))))) |
86 | 27, 19, 23, 85 | ltdiv1dd 13072 |
. . 3
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1))) < (((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1)))) |
87 | 4, 28, 24, 81, 86 | lttrd 11374 |
. 2
โข (๐ โ ๐ < (((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1)))) |
88 | 25, 43 | reexpcld 14127 |
. . . 4
โข (๐ โ (๐ดโ๐) โ โ) |
89 | 20, 7, 5, 1, 46 | fltnltalem 41405 |
. . . 4
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) < (๐ดโ๐)) |
90 | 19, 88, 23, 89 | ltdiv1dd 13072 |
. . 3
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1))) < ((๐ดโ๐) / (๐ดโ(๐ โ 1)))) |
91 | 34, 30 | nncand 11575 |
. . . . 5
โข (๐ โ (๐ โ (๐ โ 1)) = 1) |
92 | 91 | oveq2d 7424 |
. . . 4
โข (๐ โ (๐ดโ(๐ โ (๐ โ 1))) = (๐ดโ1)) |
93 | 3 | nnzd 12584 |
. . . . 5
โข (๐ โ ๐ โ โค) |
94 | 60, 61, 22, 93 | expsubd 14121 |
. . . 4
โข (๐ โ (๐ดโ(๐ โ (๐ โ 1))) = ((๐ดโ๐) / (๐ดโ(๐ โ 1)))) |
95 | 60 | exp1d 14105 |
. . . 4
โข (๐ โ (๐ดโ1) = ๐ด) |
96 | 92, 94, 95 | 3eqtr3d 2780 |
. . 3
โข (๐ โ ((๐ดโ๐) / (๐ดโ(๐ โ 1))) = ๐ด) |
97 | 90, 96 | breqtrd 5174 |
. 2
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1))) < ๐ด) |
98 | 4, 24, 25, 87, 97 | lttrd 11374 |
1
โข (๐ โ ๐ < ๐ด) |