Step | Hyp | Ref
| Expression |
1 | | fltltc.n |
. . . 4
โข (๐ โ ๐ โ
(โคโฅโ3)) |
2 | | eluzge3nn 12823 |
. . . 4
โข (๐ โ
(โคโฅโ3) โ ๐ โ โ) |
3 | 1, 2 | syl 17 |
. . 3
โข (๐ โ ๐ โ โ) |
4 | 3 | nnred 12176 |
. 2
โข (๐ โ ๐ โ โ) |
5 | | fltltc.c |
. . . . . 6
โข (๐ โ ๐ถ โ โ) |
6 | 5 | nnred 12176 |
. . . . 5
โข (๐ โ ๐ถ โ โ) |
7 | | fltltc.b |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
8 | 7 | nnred 12176 |
. . . . 5
โข (๐ โ ๐ต โ โ) |
9 | 6, 8 | resubcld 11591 |
. . . 4
โข (๐ โ (๐ถ โ ๐ต) โ โ) |
10 | | uzuzle23 12822 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ3) โ ๐ โ
(โคโฅโ2)) |
11 | | uz2m1nn 12856 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
12 | 1, 10, 11 | 3syl 18 |
. . . . . . 7
โข (๐ โ (๐ โ 1) โ โ) |
13 | 12 | nnnn0d 12481 |
. . . . . 6
โข (๐ โ (๐ โ 1) โ
โ0) |
14 | 6, 13 | reexpcld 14077 |
. . . . 5
โข (๐ โ (๐ถโ(๐ โ 1)) โ
โ) |
15 | 12 | nnred 12176 |
. . . . . 6
โข (๐ โ (๐ โ 1) โ โ) |
16 | 8, 13 | reexpcld 14077 |
. . . . . 6
โข (๐ โ (๐ตโ(๐ โ 1)) โ
โ) |
17 | 15, 16 | remulcld 11193 |
. . . . 5
โข (๐ โ ((๐ โ 1) ยท (๐ตโ(๐ โ 1))) โ
โ) |
18 | 14, 17 | readdcld 11192 |
. . . 4
โข (๐ โ ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) โ
โ) |
19 | 9, 18 | remulcld 11193 |
. . 3
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) โ
โ) |
20 | | fltltc.a |
. . . . 5
โข (๐ โ ๐ด โ โ) |
21 | 20 | nnrpd 12963 |
. . . 4
โข (๐ โ ๐ด โ
โ+) |
22 | 12 | nnzd 12534 |
. . . 4
โข (๐ โ (๐ โ 1) โ โค) |
23 | 21, 22 | rpexpcld 14159 |
. . 3
โข (๐ โ (๐ดโ(๐ โ 1)) โ
โ+) |
24 | 19, 23 | rerpdivcld 12996 |
. 2
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1))) โ
โ) |
25 | 20 | nnred 12176 |
. 2
โข (๐ โ ๐ด โ โ) |
26 | 16, 17 | readdcld 11192 |
. . . . 5
โข (๐ โ ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) โ
โ) |
27 | 9, 26 | remulcld 11193 |
. . . 4
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) โ
โ) |
28 | 27, 23 | rerpdivcld 12996 |
. . 3
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1))) โ
โ) |
29 | 9, 4 | remulcld 11193 |
. . . . 5
โข (๐ โ ((๐ถ โ ๐ต) ยท ๐) โ โ) |
30 | | 1cnd 11158 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ) |
31 | 12 | nncnd 12177 |
. . . . . . . . . 10
โข (๐ โ (๐ โ 1) โ โ) |
32 | 16 | recnd 11191 |
. . . . . . . . . 10
โข (๐ โ (๐ตโ(๐ โ 1)) โ
โ) |
33 | 30, 31, 32 | adddird 11188 |
. . . . . . . . 9
โข (๐ โ ((1 + (๐ โ 1)) ยท (๐ตโ(๐ โ 1))) = ((1 ยท (๐ตโ(๐ โ 1))) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) |
34 | 3 | nncnd 12177 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
35 | 30, 34 | pncan3d 11523 |
. . . . . . . . . 10
โข (๐ โ (1 + (๐ โ 1)) = ๐) |
36 | 35 | oveq1d 7376 |
. . . . . . . . 9
โข (๐ โ ((1 + (๐ โ 1)) ยท (๐ตโ(๐ โ 1))) = (๐ ยท (๐ตโ(๐ โ 1)))) |
37 | 32 | mulid2d 11181 |
. . . . . . . . . 10
โข (๐ โ (1 ยท (๐ตโ(๐ โ 1))) = (๐ตโ(๐ โ 1))) |
38 | 37 | oveq1d 7376 |
. . . . . . . . 9
โข (๐ โ ((1 ยท (๐ตโ(๐ โ 1))) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) = ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) |
39 | 33, 36, 38 | 3eqtr3rd 2782 |
. . . . . . . 8
โข (๐ โ ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) = (๐ ยท (๐ตโ(๐ โ 1)))) |
40 | 39 | oveq2d 7377 |
. . . . . . 7
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) = ((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1))))) |
41 | 40 | oveq1d 7376 |
. . . . . 6
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1))) = (((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1)))) / (๐ดโ(๐ โ 1)))) |
42 | 41, 28 | eqeltrrd 2835 |
. . . . 5
โข (๐ โ (((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1)))) / (๐ดโ(๐ โ 1))) โ
โ) |
43 | 3 | nnnn0d 12481 |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
44 | 43 | nn0ge0d 12484 |
. . . . . 6
โข (๐ โ 0 โค ๐) |
45 | | 1red 11164 |
. . . . . . 7
โข (๐ โ 1 โ
โ) |
46 | | fltltc.1 |
. . . . . . . . 9
โข (๐ โ ((๐ดโ๐) + (๐ตโ๐)) = (๐ถโ๐)) |
47 | 20, 7, 5, 1, 46 | fltltc 41046 |
. . . . . . . 8
โข (๐ โ ๐ต < ๐ถ) |
48 | | nnltp1le 12567 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต < ๐ถ โ (๐ต + 1) โค ๐ถ)) |
49 | 7, 5, 48 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ (๐ต < ๐ถ โ (๐ต + 1) โค ๐ถ)) |
50 | 47, 49 | mpbid 231 |
. . . . . . 7
โข (๐ โ (๐ต + 1) โค ๐ถ) |
51 | 8 | leidd 11729 |
. . . . . . 7
โข (๐ โ ๐ต โค ๐ต) |
52 | 6, 8, 45, 8, 50, 51 | lesub3d 11781 |
. . . . . 6
โข (๐ โ 1 โค (๐ถ โ ๐ต)) |
53 | 4, 9, 44, 52 | lemulge12d 12101 |
. . . . 5
โข (๐ โ ๐ โค ((๐ถ โ ๐ต) ยท ๐)) |
54 | 9 | recnd 11191 |
. . . . . . . . 9
โข (๐ โ (๐ถ โ ๐ต) โ โ) |
55 | 23 | rpred 12965 |
. . . . . . . . . 10
โข (๐ โ (๐ดโ(๐ โ 1)) โ
โ) |
56 | 55 | recnd 11191 |
. . . . . . . . 9
โข (๐ โ (๐ดโ(๐ โ 1)) โ
โ) |
57 | 54, 34, 56 | mulassd 11186 |
. . . . . . . 8
โข (๐ โ (((๐ถ โ ๐ต) ยท ๐) ยท (๐ดโ(๐ โ 1))) = ((๐ถ โ ๐ต) ยท (๐ ยท (๐ดโ(๐ โ 1))))) |
58 | 57 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ ((((๐ถ โ ๐ต) ยท ๐) ยท (๐ดโ(๐ โ 1))) / (๐ดโ(๐ โ 1))) = (((๐ถ โ ๐ต) ยท (๐ ยท (๐ดโ(๐ โ 1)))) / (๐ดโ(๐ โ 1)))) |
59 | 54, 34 | mulcld 11183 |
. . . . . . . 8
โข (๐ โ ((๐ถ โ ๐ต) ยท ๐) โ โ) |
60 | 20 | nncnd 12177 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
61 | 20 | nnne0d 12211 |
. . . . . . . . 9
โข (๐ โ ๐ด โ 0) |
62 | 60, 61, 22 | expne0d 14066 |
. . . . . . . 8
โข (๐ โ (๐ดโ(๐ โ 1)) โ 0) |
63 | 59, 56, 62 | divcan4d 11945 |
. . . . . . 7
โข (๐ โ ((((๐ถ โ ๐ต) ยท ๐) ยท (๐ดโ(๐ โ 1))) / (๐ดโ(๐ โ 1))) = ((๐ถ โ ๐ต) ยท ๐)) |
64 | 58, 63 | eqtr3d 2775 |
. . . . . 6
โข (๐ โ (((๐ถ โ ๐ต) ยท (๐ ยท (๐ดโ(๐ โ 1)))) / (๐ดโ(๐ โ 1))) = ((๐ถ โ ๐ต) ยท ๐)) |
65 | 4, 55 | remulcld 11193 |
. . . . . . . 8
โข (๐ โ (๐ ยท (๐ดโ(๐ โ 1))) โ
โ) |
66 | 9, 65 | remulcld 11193 |
. . . . . . 7
โข (๐ โ ((๐ถ โ ๐ต) ยท (๐ ยท (๐ดโ(๐ โ 1)))) โ
โ) |
67 | 40, 27 | eqeltrrd 2835 |
. . . . . . 7
โข (๐ โ ((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1)))) โ
โ) |
68 | 39, 26 | eqeltrrd 2835 |
. . . . . . . 8
โข (๐ โ (๐ ยท (๐ตโ(๐ โ 1))) โ
โ) |
69 | | difrp 12961 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต < ๐ถ โ (๐ถ โ ๐ต) โ
โ+)) |
70 | 8, 6, 69 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (๐ต < ๐ถ โ (๐ถ โ ๐ต) โ
โ+)) |
71 | 47, 70 | mpbid 231 |
. . . . . . . 8
โข (๐ โ (๐ถ โ ๐ต) โ
โ+) |
72 | 3 | nnrpd 12963 |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ+) |
73 | 7 | nnrpd 12963 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ
โ+) |
74 | | fltnlta.1 |
. . . . . . . . . 10
โข (๐ โ ๐ด < ๐ต) |
75 | 21, 73, 12, 74 | ltexp1dd 40856 |
. . . . . . . . 9
โข (๐ โ (๐ดโ(๐ โ 1)) < (๐ตโ(๐ โ 1))) |
76 | 55, 16, 72, 75 | ltmul2dd 13021 |
. . . . . . . 8
โข (๐ โ (๐ ยท (๐ดโ(๐ โ 1))) < (๐ ยท (๐ตโ(๐ โ 1)))) |
77 | 65, 68, 71, 76 | ltmul2dd 13021 |
. . . . . . 7
โข (๐ โ ((๐ถ โ ๐ต) ยท (๐ ยท (๐ดโ(๐ โ 1)))) < ((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1))))) |
78 | 66, 67, 23, 77 | ltdiv1dd 13022 |
. . . . . 6
โข (๐ โ (((๐ถ โ ๐ต) ยท (๐ ยท (๐ดโ(๐ โ 1)))) / (๐ดโ(๐ โ 1))) < (((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1)))) / (๐ดโ(๐ โ 1)))) |
79 | 64, 78 | eqbrtrrd 5133 |
. . . . 5
โข (๐ โ ((๐ถ โ ๐ต) ยท ๐) < (((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1)))) / (๐ดโ(๐ โ 1)))) |
80 | 4, 29, 42, 53, 79 | lelttrd 11321 |
. . . 4
โข (๐ โ ๐ < (((๐ถ โ ๐ต) ยท (๐ ยท (๐ตโ(๐ โ 1)))) / (๐ดโ(๐ โ 1)))) |
81 | 80, 41 | breqtrrd 5137 |
. . 3
โข (๐ โ ๐ < (((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1)))) |
82 | 5 | nnrpd 12963 |
. . . . . . 7
โข (๐ โ ๐ถ โ
โ+) |
83 | 73, 82, 12, 47 | ltexp1dd 40856 |
. . . . . 6
โข (๐ โ (๐ตโ(๐ โ 1)) < (๐ถโ(๐ โ 1))) |
84 | 16, 14, 17, 83 | ltadd1dd 11774 |
. . . . 5
โข (๐ โ ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) < ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) |
85 | 26, 18, 71, 84 | ltmul2dd 13021 |
. . . 4
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) < ((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))))) |
86 | 27, 19, 23, 85 | ltdiv1dd 13022 |
. . 3
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐ตโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1))) < (((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1)))) |
87 | 4, 28, 24, 81, 86 | lttrd 11324 |
. 2
โข (๐ โ ๐ < (((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1)))) |
88 | 25, 43 | reexpcld 14077 |
. . . 4
โข (๐ โ (๐ดโ๐) โ โ) |
89 | 20, 7, 5, 1, 46 | fltnltalem 41047 |
. . . 4
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) < (๐ดโ๐)) |
90 | 19, 88, 23, 89 | ltdiv1dd 13022 |
. . 3
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1))) < ((๐ดโ๐) / (๐ดโ(๐ โ 1)))) |
91 | 34, 30 | nncand 11525 |
. . . . 5
โข (๐ โ (๐ โ (๐ โ 1)) = 1) |
92 | 91 | oveq2d 7377 |
. . . 4
โข (๐ โ (๐ดโ(๐ โ (๐ โ 1))) = (๐ดโ1)) |
93 | 3 | nnzd 12534 |
. . . . 5
โข (๐ โ ๐ โ โค) |
94 | 60, 61, 22, 93 | expsubd 14071 |
. . . 4
โข (๐ โ (๐ดโ(๐ โ (๐ โ 1))) = ((๐ดโ๐) / (๐ดโ(๐ โ 1)))) |
95 | 60 | exp1d 14055 |
. . . 4
โข (๐ โ (๐ดโ1) = ๐ด) |
96 | 92, 94, 95 | 3eqtr3d 2781 |
. . 3
โข (๐ โ ((๐ดโ๐) / (๐ดโ(๐ โ 1))) = ๐ด) |
97 | 90, 96 | breqtrd 5135 |
. 2
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) / (๐ดโ(๐ โ 1))) < ๐ด) |
98 | 4, 24, 25, 87, 97 | lttrd 11324 |
1
โข (๐ โ ๐ < ๐ด) |