Step | Hyp | Ref
| Expression |
1 | | 2re 12282 |
. . . . . 6
โข 2 โ
โ |
2 | | ostth2lem1.2 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
3 | 2 | adantr 481 |
. . . . . 6
โข ((๐ โง 1 < ๐ด) โ ๐ต โ โ) |
4 | | remulcl 11191 |
. . . . . 6
โข ((2
โ โ โง ๐ต
โ โ) โ (2 ยท ๐ต) โ โ) |
5 | 1, 3, 4 | sylancr 587 |
. . . . 5
โข ((๐ โง 1 < ๐ด) โ (2 ยท ๐ต) โ โ) |
6 | | simpr 485 |
. . . . . 6
โข ((๐ โง 1 < ๐ด) โ 1 < ๐ด) |
7 | | 1re 11210 |
. . . . . . 7
โข 1 โ
โ |
8 | | ostth2lem1.1 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
9 | 8 | adantr 481 |
. . . . . . 7
โข ((๐ โง 1 < ๐ด) โ ๐ด โ โ) |
10 | | difrp 13008 |
. . . . . . 7
โข ((1
โ โ โง ๐ด
โ โ) โ (1 < ๐ด โ (๐ด โ 1) โ
โ+)) |
11 | 7, 9, 10 | sylancr 587 |
. . . . . 6
โข ((๐ โง 1 < ๐ด) โ (1 < ๐ด โ (๐ด โ 1) โ
โ+)) |
12 | 6, 11 | mpbid 231 |
. . . . 5
โข ((๐ โง 1 < ๐ด) โ (๐ด โ 1) โ
โ+) |
13 | 5, 12 | rerpdivcld 13043 |
. . . 4
โข ((๐ โง 1 < ๐ด) โ ((2 ยท ๐ต) / (๐ด โ 1)) โ
โ) |
14 | | expnbnd 14191 |
. . . 4
โข ((((2
ยท ๐ต) / (๐ด โ 1)) โ โ
โง ๐ด โ โ
โง 1 < ๐ด) โ
โ๐ โ โ ((2
ยท ๐ต) / (๐ด โ 1)) < (๐ดโ๐)) |
15 | 13, 9, 6, 14 | syl3anc 1371 |
. . 3
โข ((๐ โง 1 < ๐ด) โ โ๐ โ โ ((2 ยท ๐ต) / (๐ด โ 1)) < (๐ดโ๐)) |
16 | | nnnn0 12475 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ0) |
17 | | reexpcl 14040 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
18 | 9, 16, 17 | syl2an 596 |
. . . . 5
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (๐ดโ๐) โ โ) |
19 | 13 | adantr 481 |
. . . . 5
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ((2 ยท ๐ต) / (๐ด โ 1)) โ
โ) |
20 | 12 | rpred 13012 |
. . . . . . . . . . . 12
โข ((๐ โง 1 < ๐ด) โ (๐ด โ 1) โ โ) |
21 | 20 | adantr 481 |
. . . . . . . . . . 11
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (๐ด โ 1) โ โ) |
22 | | nnre 12215 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
23 | 22 | adantl 482 |
. . . . . . . . . . 11
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ๐ โ โ) |
24 | 21, 23 | remulcld 11240 |
. . . . . . . . . 10
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ((๐ด โ 1) ยท ๐) โ โ) |
25 | 24, 18 | remulcld 11240 |
. . . . . . . . 9
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (((๐ด โ 1) ยท ๐) ยท (๐ดโ๐)) โ โ) |
26 | 8 | ad2antrr 724 |
. . . . . . . . . 10
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ๐ด โ โ) |
27 | | 2nn 12281 |
. . . . . . . . . . . 12
โข 2 โ
โ |
28 | | simpr 485 |
. . . . . . . . . . . 12
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ๐ โ โ) |
29 | | nnmulcl 12232 |
. . . . . . . . . . . 12
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
30 | 27, 28, 29 | sylancr 587 |
. . . . . . . . . . 11
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (2 ยท ๐) โ
โ) |
31 | 30 | nnnn0d 12528 |
. . . . . . . . . 10
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (2 ยท ๐) โ
โ0) |
32 | 26, 31 | reexpcld 14124 |
. . . . . . . . 9
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (๐ดโ(2 ยท ๐)) โ โ) |
33 | 30 | nnred 12223 |
. . . . . . . . . 10
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (2 ยท ๐) โ
โ) |
34 | 2 | ad2antrr 724 |
. . . . . . . . . 10
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ๐ต โ โ) |
35 | 33, 34 | remulcld 11240 |
. . . . . . . . 9
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ((2 ยท ๐) ยท ๐ต) โ โ) |
36 | | 0red 11213 |
. . . . . . . . . . . . . 14
โข ((๐ โง 1 < ๐ด) โ 0 โ โ) |
37 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ โง 1 < ๐ด) โ 1 โ โ) |
38 | | 0lt1 11732 |
. . . . . . . . . . . . . . 15
โข 0 <
1 |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ โง 1 < ๐ด) โ 0 < 1) |
40 | 36, 37, 9, 39, 6 | lttrd 11371 |
. . . . . . . . . . . . 13
โข ((๐ โง 1 < ๐ด) โ 0 < ๐ด) |
41 | 9, 40 | elrpd 13009 |
. . . . . . . . . . . 12
โข ((๐ โง 1 < ๐ด) โ ๐ด โ
โ+) |
42 | | nnz 12575 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โค) |
43 | | rpexpcl 14042 |
. . . . . . . . . . . 12
โข ((๐ด โ โ+
โง ๐ โ โค)
โ (๐ดโ๐) โ
โ+) |
44 | 41, 42, 43 | syl2an 596 |
. . . . . . . . . . 11
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (๐ดโ๐) โ
โ+) |
45 | | peano2re 11383 |
. . . . . . . . . . . . 13
โข (((๐ด โ 1) ยท ๐) โ โ โ (((๐ด โ 1) ยท ๐) + 1) โ
โ) |
46 | 24, 45 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (((๐ด โ 1) ยท ๐) + 1) โ โ) |
47 | 24 | ltp1d 12140 |
. . . . . . . . . . . 12
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ((๐ด โ 1) ยท ๐) < (((๐ด โ 1) ยท ๐) + 1)) |
48 | 16 | adantl 482 |
. . . . . . . . . . . . 13
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ๐ โ โ0) |
49 | 41 | adantr 481 |
. . . . . . . . . . . . . 14
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ๐ด โ
โ+) |
50 | 49 | rpge0d 13016 |
. . . . . . . . . . . . 13
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ 0 โค ๐ด) |
51 | | bernneq2 14189 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ โ โ0
โง 0 โค ๐ด) โ
(((๐ด โ 1) ยท
๐) + 1) โค (๐ดโ๐)) |
52 | 26, 48, 50, 51 | syl3anc 1371 |
. . . . . . . . . . . 12
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (((๐ด โ 1) ยท ๐) + 1) โค (๐ดโ๐)) |
53 | 24, 46, 18, 47, 52 | ltletrd 11370 |
. . . . . . . . . . 11
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ((๐ด โ 1) ยท ๐) < (๐ดโ๐)) |
54 | 24, 18, 44, 53 | ltmul1dd 13067 |
. . . . . . . . . 10
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (((๐ด โ 1) ยท ๐) ยท (๐ดโ๐)) < ((๐ดโ๐) ยท (๐ดโ๐))) |
55 | 23 | recnd 11238 |
. . . . . . . . . . . . 13
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ๐ โ โ) |
56 | 55 | 2timesd 12451 |
. . . . . . . . . . . 12
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (2 ยท ๐) = (๐ + ๐)) |
57 | 56 | oveq2d 7421 |
. . . . . . . . . . 11
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (๐ดโ(2 ยท ๐)) = (๐ดโ(๐ + ๐))) |
58 | 26 | recnd 11238 |
. . . . . . . . . . . 12
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ๐ด โ โ) |
59 | 58, 48, 48 | expaddd 14109 |
. . . . . . . . . . 11
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) |
60 | 57, 59 | eqtrd 2772 |
. . . . . . . . . 10
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (๐ดโ(2 ยท ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) |
61 | 54, 60 | breqtrrd 5175 |
. . . . . . . . 9
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (((๐ด โ 1) ยท ๐) ยท (๐ดโ๐)) < (๐ดโ(2 ยท ๐))) |
62 | | oveq2 7413 |
. . . . . . . . . . 11
โข (๐ = (2 ยท ๐) โ (๐ดโ๐) = (๐ดโ(2 ยท ๐))) |
63 | | oveq1 7412 |
. . . . . . . . . . 11
โข (๐ = (2 ยท ๐) โ (๐ ยท ๐ต) = ((2 ยท ๐) ยท ๐ต)) |
64 | 62, 63 | breq12d 5160 |
. . . . . . . . . 10
โข (๐ = (2 ยท ๐) โ ((๐ดโ๐) โค (๐ ยท ๐ต) โ (๐ดโ(2 ยท ๐)) โค ((2 ยท ๐) ยท ๐ต))) |
65 | | ostth2lem1.3 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ) โ (๐ดโ๐) โค (๐ ยท ๐ต)) |
66 | 65 | ralrimiva 3146 |
. . . . . . . . . . 11
โข (๐ โ โ๐ โ โ (๐ดโ๐) โค (๐ ยท ๐ต)) |
67 | 66 | ad2antrr 724 |
. . . . . . . . . 10
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ โ๐ โ โ (๐ดโ๐) โค (๐ ยท ๐ต)) |
68 | 64, 67, 30 | rspcdva 3613 |
. . . . . . . . 9
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (๐ดโ(2 ยท ๐)) โค ((2 ยท ๐) ยท ๐ต)) |
69 | 25, 32, 35, 61, 68 | ltletrd 11370 |
. . . . . . . 8
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (((๐ด โ 1) ยท ๐) ยท (๐ดโ๐)) < ((2 ยท ๐) ยท ๐ต)) |
70 | 21 | recnd 11238 |
. . . . . . . . 9
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (๐ด โ 1) โ โ) |
71 | 18 | recnd 11238 |
. . . . . . . . 9
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (๐ดโ๐) โ โ) |
72 | 70, 71, 55 | mul32d 11420 |
. . . . . . . 8
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (((๐ด โ 1) ยท (๐ดโ๐)) ยท ๐) = (((๐ด โ 1) ยท ๐) ยท (๐ดโ๐))) |
73 | | 2cnd 12286 |
. . . . . . . . 9
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ 2 โ
โ) |
74 | 34 | recnd 11238 |
. . . . . . . . 9
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ๐ต โ โ) |
75 | 73, 74, 55 | mul32d 11420 |
. . . . . . . 8
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ((2 ยท ๐ต) ยท ๐) = ((2 ยท ๐) ยท ๐ต)) |
76 | 69, 72, 75 | 3brtr4d 5179 |
. . . . . . 7
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (((๐ด โ 1) ยท (๐ดโ๐)) ยท ๐) < ((2 ยท ๐ต) ยท ๐)) |
77 | 21, 18 | remulcld 11240 |
. . . . . . . 8
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ((๐ด โ 1) ยท (๐ดโ๐)) โ โ) |
78 | 5 | adantr 481 |
. . . . . . . 8
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (2 ยท ๐ต) โ
โ) |
79 | | nngt0 12239 |
. . . . . . . . 9
โข (๐ โ โ โ 0 <
๐) |
80 | 79 | adantl 482 |
. . . . . . . 8
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ 0 < ๐) |
81 | | ltmul1 12060 |
. . . . . . . 8
โข ((((๐ด โ 1) ยท (๐ดโ๐)) โ โ โง (2 ยท ๐ต) โ โ โง (๐ โ โ โง 0 <
๐)) โ (((๐ด โ 1) ยท (๐ดโ๐)) < (2 ยท ๐ต) โ (((๐ด โ 1) ยท (๐ดโ๐)) ยท ๐) < ((2 ยท ๐ต) ยท ๐))) |
82 | 77, 78, 23, 80, 81 | syl112anc 1374 |
. . . . . . 7
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (((๐ด โ 1) ยท (๐ดโ๐)) < (2 ยท ๐ต) โ (((๐ด โ 1) ยท (๐ดโ๐)) ยท ๐) < ((2 ยท ๐ต) ยท ๐))) |
83 | 76, 82 | mpbird 256 |
. . . . . 6
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ((๐ด โ 1) ยท (๐ดโ๐)) < (2 ยท ๐ต)) |
84 | 12 | rpgt0d 13015 |
. . . . . . . 8
โข ((๐ โง 1 < ๐ด) โ 0 < (๐ด โ 1)) |
85 | 84 | adantr 481 |
. . . . . . 7
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ 0 < (๐ด โ 1)) |
86 | | ltmuldiv2 12084 |
. . . . . . 7
โข (((๐ดโ๐) โ โ โง (2 ยท ๐ต) โ โ โง ((๐ด โ 1) โ โ โง
0 < (๐ด โ 1)))
โ (((๐ด โ 1)
ยท (๐ดโ๐)) < (2 ยท ๐ต) โ (๐ดโ๐) < ((2 ยท ๐ต) / (๐ด โ 1)))) |
87 | 18, 78, 21, 85, 86 | syl112anc 1374 |
. . . . . 6
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (((๐ด โ 1) ยท (๐ดโ๐)) < (2 ยท ๐ต) โ (๐ดโ๐) < ((2 ยท ๐ต) / (๐ด โ 1)))) |
88 | 83, 87 | mpbid 231 |
. . . . 5
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ (๐ดโ๐) < ((2 ยท ๐ต) / (๐ด โ 1))) |
89 | 18, 19, 88 | ltnsymd 11359 |
. . . 4
โข (((๐ โง 1 < ๐ด) โง ๐ โ โ) โ ยฌ ((2 ยท
๐ต) / (๐ด โ 1)) < (๐ดโ๐)) |
90 | 89 | nrexdv 3149 |
. . 3
โข ((๐ โง 1 < ๐ด) โ ยฌ โ๐ โ โ ((2 ยท ๐ต) / (๐ด โ 1)) < (๐ดโ๐)) |
91 | 15, 90 | pm2.65da 815 |
. 2
โข (๐ โ ยฌ 1 < ๐ด) |
92 | | lenlt 11288 |
. . 3
โข ((๐ด โ โ โง 1 โ
โ) โ (๐ด โค 1
โ ยฌ 1 < ๐ด)) |
93 | 8, 7, 92 | sylancl 586 |
. 2
โข (๐ โ (๐ด โค 1 โ ยฌ 1 < ๐ด)) |
94 | 91, 93 | mpbird 256 |
1
โข (๐ โ ๐ด โค 1) |