Step | Hyp | Ref
| Expression |
1 | | 1re 11163 |
. . . . 5
โข 1 โ
โ |
2 | 1 | a1i 11 |
. . . 4
โข (๐ โ 1 โ
โ) |
3 | | stoweidlem1.5 |
. . . . . 6
โข (๐ โ ๐ด โ
โ+) |
4 | 3 | rpred 12965 |
. . . . 5
โข (๐ โ ๐ด โ โ) |
5 | | stoweidlem1.1 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
6 | 5 | nnnn0d 12481 |
. . . . 5
โข (๐ โ ๐ โ
โ0) |
7 | 4, 6 | reexpcld 14077 |
. . . 4
โข (๐ โ (๐ดโ๐) โ โ) |
8 | 2, 7 | resubcld 11591 |
. . 3
โข (๐ โ (1 โ (๐ดโ๐)) โ โ) |
9 | | stoweidlem1.2 |
. . . . 5
โข (๐ โ ๐พ โ โ) |
10 | 9 | nnnn0d 12481 |
. . . 4
โข (๐ โ ๐พ โ
โ0) |
11 | 10, 6 | nn0expcld 14158 |
. . 3
โข (๐ โ (๐พโ๐) โ
โ0) |
12 | 8, 11 | reexpcld 14077 |
. 2
โข (๐ โ ((1 โ (๐ดโ๐))โ(๐พโ๐)) โ โ) |
13 | | 2nn0 12438 |
. . . . . . . 8
โข 2 โ
โ0 |
14 | 13 | a1i 11 |
. . . . . . 7
โข (๐ โ 2 โ
โ0) |
15 | 14, 6 | nn0mulcld 12486 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ
โ0) |
16 | 4, 15 | reexpcld 14077 |
. . . . 5
โข (๐ โ (๐ดโ(2 ยท ๐)) โ โ) |
17 | 2, 16 | resubcld 11591 |
. . . 4
โข (๐ โ (1 โ (๐ดโ(2 ยท ๐))) โ
โ) |
18 | 17, 11 | reexpcld 14077 |
. . 3
โข (๐ โ ((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) โ โ) |
19 | 9 | nnred 12176 |
. . . . 5
โข (๐ โ ๐พ โ โ) |
20 | 19, 4 | remulcld 11193 |
. . . 4
โข (๐ โ (๐พ ยท ๐ด) โ โ) |
21 | 20, 6 | reexpcld 14077 |
. . 3
โข (๐ โ ((๐พ ยท ๐ด)โ๐) โ โ) |
22 | 9 | nncnd 12177 |
. . . . 5
โข (๐ โ ๐พ โ โ) |
23 | 3 | rpcnd 12967 |
. . . . 5
โข (๐ โ ๐ด โ โ) |
24 | 9 | nnne0d 12211 |
. . . . 5
โข (๐ โ ๐พ โ 0) |
25 | 3 | rpne0d 12970 |
. . . . 5
โข (๐ โ ๐ด โ 0) |
26 | 22, 23, 24, 25 | mulne0d 11815 |
. . . 4
โข (๐ โ (๐พ ยท ๐ด) โ 0) |
27 | 22, 23 | mulcld 11183 |
. . . . 5
โข (๐ โ (๐พ ยท ๐ด) โ โ) |
28 | | expne0 14008 |
. . . . 5
โข (((๐พ ยท ๐ด) โ โ โง ๐ โ โ) โ (((๐พ ยท ๐ด)โ๐) โ 0 โ (๐พ ยท ๐ด) โ 0)) |
29 | 27, 5, 28 | syl2anc 585 |
. . . 4
โข (๐ โ (((๐พ ยท ๐ด)โ๐) โ 0 โ (๐พ ยท ๐ด) โ 0)) |
30 | 26, 29 | mpbird 257 |
. . 3
โข (๐ โ ((๐พ ยท ๐ด)โ๐) โ 0) |
31 | 18, 21, 30 | redivcld 11991 |
. 2
โข (๐ โ (((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) / ((๐พ ยท ๐ด)โ๐)) โ โ) |
32 | | stoweidlem1.3 |
. . . . . 6
โข (๐ โ ๐ท โ
โ+) |
33 | 32 | rpred 12965 |
. . . . 5
โข (๐ โ ๐ท โ โ) |
34 | 19, 33 | remulcld 11193 |
. . . 4
โข (๐ โ (๐พ ยท ๐ท) โ โ) |
35 | 34, 6 | reexpcld 14077 |
. . 3
โข (๐ โ ((๐พ ยท ๐ท)โ๐) โ โ) |
36 | 32 | rpcnd 12967 |
. . . . 5
โข (๐ โ ๐ท โ โ) |
37 | 32 | rpne0d 12970 |
. . . . 5
โข (๐ โ ๐ท โ 0) |
38 | 22, 36, 24, 37 | mulne0d 11815 |
. . . 4
โข (๐ โ (๐พ ยท ๐ท) โ 0) |
39 | 22, 36 | mulcld 11183 |
. . . . 5
โข (๐ โ (๐พ ยท ๐ท) โ โ) |
40 | | expne0 14008 |
. . . . 5
โข (((๐พ ยท ๐ท) โ โ โง ๐ โ โ) โ (((๐พ ยท ๐ท)โ๐) โ 0 โ (๐พ ยท ๐ท) โ 0)) |
41 | 39, 5, 40 | syl2anc 585 |
. . . 4
โข (๐ โ (((๐พ ยท ๐ท)โ๐) โ 0 โ (๐พ ยท ๐ท) โ 0)) |
42 | 38, 41 | mpbird 257 |
. . 3
โข (๐ โ ((๐พ ยท ๐ท)โ๐) โ 0) |
43 | 2, 35, 42 | redivcld 11991 |
. 2
โข (๐ โ (1 / ((๐พ ยท ๐ท)โ๐)) โ โ) |
44 | 19, 6 | reexpcld 14077 |
. . . . . . . 8
โข (๐ โ (๐พโ๐) โ โ) |
45 | 44, 7 | remulcld 11193 |
. . . . . . 7
โข (๐ โ ((๐พโ๐) ยท (๐ดโ๐)) โ โ) |
46 | 2, 45 | readdcld 11192 |
. . . . . 6
โข (๐ โ (1 + ((๐พโ๐) ยท (๐ดโ๐))) โ โ) |
47 | 12, 46 | remulcld 11193 |
. . . . 5
โข (๐ โ (((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท (1 + ((๐พโ๐) ยท (๐ดโ๐)))) โ โ) |
48 | 47, 21, 30 | redivcld 11991 |
. . . 4
โข (๐ โ ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท (1 + ((๐พโ๐) ยท (๐ดโ๐)))) / ((๐พ ยท ๐ด)โ๐)) โ โ) |
49 | 2, 7 | readdcld 11192 |
. . . . . . 7
โข (๐ โ (1 + (๐ดโ๐)) โ โ) |
50 | 49, 11 | reexpcld 14077 |
. . . . . 6
โข (๐ โ ((1 + (๐ดโ๐))โ(๐พโ๐)) โ โ) |
51 | 12, 50 | remulcld 11193 |
. . . . 5
โข (๐ โ (((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐))) โ โ) |
52 | 51, 21, 30 | redivcld 11991 |
. . . 4
โข (๐ โ ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐))) / ((๐พ ยท ๐ด)โ๐)) โ โ) |
53 | 46, 21, 30 | redivcld 11991 |
. . . . . 6
โข (๐ โ ((1 + ((๐พโ๐) ยท (๐ดโ๐))) / ((๐พ ยท ๐ด)โ๐)) โ โ) |
54 | | stoweidlem1.6 |
. . . . . . . . 9
โข (๐ โ 0 โค ๐ด) |
55 | | stoweidlem1.7 |
. . . . . . . . 9
โข (๐ โ ๐ด โค 1) |
56 | | exple1 14090 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด โง ๐ด โค 1) โง ๐ โ โ0) โ (๐ดโ๐) โค 1) |
57 | 4, 54, 55, 6, 56 | syl31anc 1374 |
. . . . . . . 8
โข (๐ โ (๐ดโ๐) โค 1) |
58 | 2, 7 | subge0d 11753 |
. . . . . . . 8
โข (๐ โ (0 โค (1 โ (๐ดโ๐)) โ (๐ดโ๐) โค 1)) |
59 | 57, 58 | mpbird 257 |
. . . . . . 7
โข (๐ โ 0 โค (1 โ (๐ดโ๐))) |
60 | 8, 11, 59 | expge0d 14078 |
. . . . . 6
โข (๐ โ 0 โค ((1 โ (๐ดโ๐))โ(๐พโ๐))) |
61 | 27, 6 | expcld 14060 |
. . . . . . . . 9
โข (๐ โ ((๐พ ยท ๐ด)โ๐) โ โ) |
62 | 61, 30 | dividd 11937 |
. . . . . . . 8
โข (๐ โ (((๐พ ยท ๐ด)โ๐) / ((๐พ ยท ๐ด)โ๐)) = 1) |
63 | 61 | addid2d 11364 |
. . . . . . . . . 10
โข (๐ โ (0 + ((๐พ ยท ๐ด)โ๐)) = ((๐พ ยท ๐ด)โ๐)) |
64 | | 0red 11166 |
. . . . . . . . . . 11
โข (๐ โ 0 โ
โ) |
65 | | 0le1 11686 |
. . . . . . . . . . . 12
โข 0 โค
1 |
66 | 65 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 0 โค 1) |
67 | 64, 2, 21, 66 | leadd1dd 11777 |
. . . . . . . . . 10
โข (๐ โ (0 + ((๐พ ยท ๐ด)โ๐)) โค (1 + ((๐พ ยท ๐ด)โ๐))) |
68 | 63, 67 | eqbrtrrd 5133 |
. . . . . . . . 9
โข (๐ โ ((๐พ ยท ๐ด)โ๐) โค (1 + ((๐พ ยท ๐ด)โ๐))) |
69 | 2, 21 | readdcld 11192 |
. . . . . . . . . 10
โข (๐ โ (1 + ((๐พ ยท ๐ด)โ๐)) โ โ) |
70 | 5 | nnzd 12534 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โค) |
71 | 9 | nngt0d 12210 |
. . . . . . . . . . . 12
โข (๐ โ 0 < ๐พ) |
72 | 3 | rpgt0d 12968 |
. . . . . . . . . . . 12
โข (๐ โ 0 < ๐ด) |
73 | 19, 4, 71, 72 | mulgt0d 11318 |
. . . . . . . . . . 11
โข (๐ โ 0 < (๐พ ยท ๐ด)) |
74 | | expgt0 14010 |
. . . . . . . . . . 11
โข (((๐พ ยท ๐ด) โ โ โง ๐ โ โค โง 0 < (๐พ ยท ๐ด)) โ 0 < ((๐พ ยท ๐ด)โ๐)) |
75 | 20, 70, 73, 74 | syl3anc 1372 |
. . . . . . . . . 10
โข (๐ โ 0 < ((๐พ ยท ๐ด)โ๐)) |
76 | | lediv1 12028 |
. . . . . . . . . 10
โข ((((๐พ ยท ๐ด)โ๐) โ โ โง (1 + ((๐พ ยท ๐ด)โ๐)) โ โ โง (((๐พ ยท ๐ด)โ๐) โ โ โง 0 < ((๐พ ยท ๐ด)โ๐))) โ (((๐พ ยท ๐ด)โ๐) โค (1 + ((๐พ ยท ๐ด)โ๐)) โ (((๐พ ยท ๐ด)โ๐) / ((๐พ ยท ๐ด)โ๐)) โค ((1 + ((๐พ ยท ๐ด)โ๐)) / ((๐พ ยท ๐ด)โ๐)))) |
77 | 21, 69, 21, 75, 76 | syl112anc 1375 |
. . . . . . . . 9
โข (๐ โ (((๐พ ยท ๐ด)โ๐) โค (1 + ((๐พ ยท ๐ด)โ๐)) โ (((๐พ ยท ๐ด)โ๐) / ((๐พ ยท ๐ด)โ๐)) โค ((1 + ((๐พ ยท ๐ด)โ๐)) / ((๐พ ยท ๐ด)โ๐)))) |
78 | 68, 77 | mpbid 231 |
. . . . . . . 8
โข (๐ โ (((๐พ ยท ๐ด)โ๐) / ((๐พ ยท ๐ด)โ๐)) โค ((1 + ((๐พ ยท ๐ด)โ๐)) / ((๐พ ยท ๐ด)โ๐))) |
79 | 62, 78 | eqbrtrrd 5133 |
. . . . . . 7
โข (๐ โ 1 โค ((1 + ((๐พ ยท ๐ด)โ๐)) / ((๐พ ยท ๐ด)โ๐))) |
80 | 22, 23, 6 | mulexpd 14075 |
. . . . . . . . 9
โข (๐ โ ((๐พ ยท ๐ด)โ๐) = ((๐พโ๐) ยท (๐ดโ๐))) |
81 | 80 | oveq2d 7377 |
. . . . . . . 8
โข (๐ โ (1 + ((๐พ ยท ๐ด)โ๐)) = (1 + ((๐พโ๐) ยท (๐ดโ๐)))) |
82 | 81 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ ((1 + ((๐พ ยท ๐ด)โ๐)) / ((๐พ ยท ๐ด)โ๐)) = ((1 + ((๐พโ๐) ยท (๐ดโ๐))) / ((๐พ ยท ๐ด)โ๐))) |
83 | 79, 82 | breqtrd 5135 |
. . . . . 6
โข (๐ โ 1 โค ((1 + ((๐พโ๐) ยท (๐ดโ๐))) / ((๐พ ยท ๐ด)โ๐))) |
84 | 12, 53, 60, 83 | lemulge11d 12100 |
. . . . 5
โข (๐ โ ((1 โ (๐ดโ๐))โ(๐พโ๐)) โค (((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + ((๐พโ๐) ยท (๐ดโ๐))) / ((๐พ ยท ๐ด)โ๐)))) |
85 | | 1cnd 11158 |
. . . . . . . 8
โข (๐ โ 1 โ
โ) |
86 | 23, 6 | expcld 14060 |
. . . . . . . 8
โข (๐ โ (๐ดโ๐) โ โ) |
87 | 85, 86 | subcld 11520 |
. . . . . . 7
โข (๐ โ (1 โ (๐ดโ๐)) โ โ) |
88 | 87, 11 | expcld 14060 |
. . . . . 6
โข (๐ โ ((1 โ (๐ดโ๐))โ(๐พโ๐)) โ โ) |
89 | 22, 6 | expcld 14060 |
. . . . . . . 8
โข (๐ โ (๐พโ๐) โ โ) |
90 | 89, 86 | mulcld 11183 |
. . . . . . 7
โข (๐ โ ((๐พโ๐) ยท (๐ดโ๐)) โ โ) |
91 | 85, 90 | addcld 11182 |
. . . . . 6
โข (๐ โ (1 + ((๐พโ๐) ยท (๐ดโ๐))) โ โ) |
92 | 88, 91, 61, 30 | divassd 11974 |
. . . . 5
โข (๐ โ ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท (1 + ((๐พโ๐) ยท (๐ดโ๐)))) / ((๐พ ยท ๐ด)โ๐)) = (((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + ((๐พโ๐) ยท (๐ดโ๐))) / ((๐พ ยท ๐ด)โ๐)))) |
93 | 84, 92 | breqtrrd 5137 |
. . . 4
โข (๐ โ ((1 โ (๐ดโ๐))โ(๐พโ๐)) โค ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท (1 + ((๐พโ๐) ยท (๐ดโ๐)))) / ((๐พ ยท ๐ด)โ๐))) |
94 | 89, 86 | mulcomd 11184 |
. . . . . . . 8
โข (๐ โ ((๐พโ๐) ยท (๐ดโ๐)) = ((๐ดโ๐) ยท (๐พโ๐))) |
95 | 94 | oveq2d 7377 |
. . . . . . 7
โข (๐ โ (1 + ((๐พโ๐) ยท (๐ดโ๐))) = (1 + ((๐ดโ๐) ยท (๐พโ๐)))) |
96 | 2 | renegcld 11590 |
. . . . . . . . 9
โข (๐ โ -1 โ
โ) |
97 | | le0neg2 11672 |
. . . . . . . . . . . 12
โข (1 โ
โ โ (0 โค 1 โ -1 โค 0)) |
98 | 1, 97 | ax-mp 5 |
. . . . . . . . . . 11
โข (0 โค 1
โ -1 โค 0) |
99 | 65, 98 | mpbi 229 |
. . . . . . . . . 10
โข -1 โค
0 |
100 | 99 | a1i 11 |
. . . . . . . . 9
โข (๐ โ -1 โค
0) |
101 | 4, 6, 54 | expge0d 14078 |
. . . . . . . . 9
โข (๐ โ 0 โค (๐ดโ๐)) |
102 | 96, 64, 7, 100, 101 | letrd 11320 |
. . . . . . . 8
โข (๐ โ -1 โค (๐ดโ๐)) |
103 | | bernneq 14141 |
. . . . . . . 8
โข (((๐ดโ๐) โ โ โง (๐พโ๐) โ โ0 โง -1 โค
(๐ดโ๐)) โ (1 + ((๐ดโ๐) ยท (๐พโ๐))) โค ((1 + (๐ดโ๐))โ(๐พโ๐))) |
104 | 7, 11, 102, 103 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ (1 + ((๐ดโ๐) ยท (๐พโ๐))) โค ((1 + (๐ดโ๐))โ(๐พโ๐))) |
105 | 95, 104 | eqbrtrd 5131 |
. . . . . 6
โข (๐ โ (1 + ((๐พโ๐) ยท (๐ดโ๐))) โค ((1 + (๐ดโ๐))โ(๐พโ๐))) |
106 | 46, 50, 12, 60, 105 | lemul2ad 12103 |
. . . . 5
โข (๐ โ (((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท (1 + ((๐พโ๐) ยท (๐ดโ๐)))) โค (((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐)))) |
107 | | lediv1 12028 |
. . . . . 6
โข (((((1
โ (๐ดโ๐))โ(๐พโ๐)) ยท (1 + ((๐พโ๐) ยท (๐ดโ๐)))) โ โ โง (((1 โ
(๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐))) โ โ โง (((๐พ ยท ๐ด)โ๐) โ โ โง 0 < ((๐พ ยท ๐ด)โ๐))) โ ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท (1 + ((๐พโ๐) ยท (๐ดโ๐)))) โค (((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐))) โ ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท (1 + ((๐พโ๐) ยท (๐ดโ๐)))) / ((๐พ ยท ๐ด)โ๐)) โค ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐))) / ((๐พ ยท ๐ด)โ๐)))) |
108 | 47, 51, 21, 75, 107 | syl112anc 1375 |
. . . . 5
โข (๐ โ ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท (1 + ((๐พโ๐) ยท (๐ดโ๐)))) โค (((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐))) โ ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท (1 + ((๐พโ๐) ยท (๐ดโ๐)))) / ((๐พ ยท ๐ด)โ๐)) โค ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐))) / ((๐พ ยท ๐ด)โ๐)))) |
109 | 106, 108 | mpbid 231 |
. . . 4
โข (๐ โ ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท (1 + ((๐พโ๐) ยท (๐ดโ๐)))) / ((๐พ ยท ๐ด)โ๐)) โค ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐))) / ((๐พ ยท ๐ด)โ๐))) |
110 | 12, 48, 52, 93, 109 | letrd 11320 |
. . 3
โข (๐ โ ((1 โ (๐ดโ๐))โ(๐พโ๐)) โค ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐))) / ((๐พ ยท ๐ด)โ๐))) |
111 | 85, 86 | addcld 11182 |
. . . . . . 7
โข (๐ โ (1 + (๐ดโ๐)) โ โ) |
112 | 87, 111 | mulcomd 11184 |
. . . . . 6
โข (๐ โ ((1 โ (๐ดโ๐)) ยท (1 + (๐ดโ๐))) = ((1 + (๐ดโ๐)) ยท (1 โ (๐ดโ๐)))) |
113 | 112 | oveq1d 7376 |
. . . . 5
โข (๐ โ (((1 โ (๐ดโ๐)) ยท (1 + (๐ดโ๐)))โ(๐พโ๐)) = (((1 + (๐ดโ๐)) ยท (1 โ (๐ดโ๐)))โ(๐พโ๐))) |
114 | 87, 111, 11 | mulexpd 14075 |
. . . . 5
โข (๐ โ (((1 โ (๐ดโ๐)) ยท (1 + (๐ดโ๐)))โ(๐พโ๐)) = (((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐)))) |
115 | | subsq 14123 |
. . . . . . . 8
โข ((1
โ โ โง (๐ดโ๐) โ โ) โ ((1โ2) โ
((๐ดโ๐)โ2)) = ((1 + (๐ดโ๐)) ยท (1 โ (๐ดโ๐)))) |
116 | 85, 86, 115 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ((1โ2) โ
((๐ดโ๐)โ2)) = ((1 + (๐ดโ๐)) ยท (1 โ (๐ดโ๐)))) |
117 | | sq1 14108 |
. . . . . . . . 9
โข
(1โ2) = 1 |
118 | 117 | a1i 11 |
. . . . . . . 8
โข (๐ โ (1โ2) =
1) |
119 | 23, 14, 6 | expmuld 14063 |
. . . . . . . . 9
โข (๐ โ (๐ดโ(๐ ยท 2)) = ((๐ดโ๐)โ2)) |
120 | 5 | nncnd 12177 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
121 | | 2cnd 12239 |
. . . . . . . . . . 11
โข (๐ โ 2 โ
โ) |
122 | 120, 121 | mulcomd 11184 |
. . . . . . . . . 10
โข (๐ โ (๐ ยท 2) = (2 ยท ๐)) |
123 | 122 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ โ (๐ดโ(๐ ยท 2)) = (๐ดโ(2 ยท ๐))) |
124 | 119, 123 | eqtr3d 2775 |
. . . . . . . 8
โข (๐ โ ((๐ดโ๐)โ2) = (๐ดโ(2 ยท ๐))) |
125 | 118, 124 | oveq12d 7379 |
. . . . . . 7
โข (๐ โ ((1โ2) โ
((๐ดโ๐)โ2)) = (1 โ (๐ดโ(2 ยท ๐)))) |
126 | 116, 125 | eqtr3d 2775 |
. . . . . 6
โข (๐ โ ((1 + (๐ดโ๐)) ยท (1 โ (๐ดโ๐))) = (1 โ (๐ดโ(2 ยท ๐)))) |
127 | 126 | oveq1d 7376 |
. . . . 5
โข (๐ โ (((1 + (๐ดโ๐)) ยท (1 โ (๐ดโ๐)))โ(๐พโ๐)) = ((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐))) |
128 | 113, 114,
127 | 3eqtr3d 2781 |
. . . 4
โข (๐ โ (((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐))) = ((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐))) |
129 | 128 | oveq1d 7376 |
. . 3
โข (๐ โ ((((1 โ (๐ดโ๐))โ(๐พโ๐)) ยท ((1 + (๐ดโ๐))โ(๐พโ๐))) / ((๐พ ยท ๐ด)โ๐)) = (((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) / ((๐พ ยท ๐ด)โ๐))) |
130 | 110, 129 | breqtrd 5135 |
. 2
โข (๐ โ ((1 โ (๐ดโ๐))โ(๐พโ๐)) โค (((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) / ((๐พ ยท ๐ด)โ๐))) |
131 | 18, 2 | jca 513 |
. . . 4
โข (๐ โ (((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) โ โ โง 1 โ
โ)) |
132 | | exple1 14090 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด โง ๐ด โค 1) โง (2 ยท ๐) โ โ0) โ (๐ดโ(2 ยท ๐)) โค 1) |
133 | 4, 54, 55, 15, 132 | syl31anc 1374 |
. . . . . 6
โข (๐ โ (๐ดโ(2 ยท ๐)) โค 1) |
134 | 2, 16 | subge0d 11753 |
. . . . . 6
โข (๐ โ (0 โค (1 โ (๐ดโ(2 ยท ๐))) โ (๐ดโ(2 ยท ๐)) โค 1)) |
135 | 133, 134 | mpbird 257 |
. . . . 5
โข (๐ โ 0 โค (1 โ (๐ดโ(2 ยท ๐)))) |
136 | 17, 11, 135 | expge0d 14078 |
. . . 4
โข (๐ โ 0 โค ((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐))) |
137 | | 1m1e0 12233 |
. . . . . . 7
โข (1
โ 1) = 0 |
138 | 4, 15, 54 | expge0d 14078 |
. . . . . . 7
โข (๐ โ 0 โค (๐ดโ(2 ยท ๐))) |
139 | 137, 138 | eqbrtrid 5144 |
. . . . . 6
โข (๐ โ (1 โ 1) โค (๐ดโ(2 ยท ๐))) |
140 | 2, 2, 16, 139 | subled 11766 |
. . . . 5
โข (๐ โ (1 โ (๐ดโ(2 ยท ๐))) โค 1) |
141 | | exple1 14090 |
. . . . 5
โข ((((1
โ (๐ดโ(2 ยท
๐))) โ โ โง 0
โค (1 โ (๐ดโ(2
ยท ๐))) โง (1
โ (๐ดโ(2 ยท
๐))) โค 1) โง (๐พโ๐) โ โ0) โ ((1
โ (๐ดโ(2 ยท
๐)))โ(๐พโ๐)) โค 1) |
142 | 17, 135, 140, 11, 141 | syl31anc 1374 |
. . . 4
โข (๐ โ ((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) โค 1) |
143 | 131, 136,
142 | jca32 517 |
. . 3
โข (๐ โ ((((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) โ โ โง 1 โ โ)
โง (0 โค ((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) โง ((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) โค 1))) |
144 | 35, 21 | jca 513 |
. . 3
โข (๐ โ (((๐พ ยท ๐ท)โ๐) โ โ โง ((๐พ ยท ๐ด)โ๐) โ โ)) |
145 | 32 | rpgt0d 12968 |
. . . . . 6
โข (๐ โ 0 < ๐ท) |
146 | 19, 33, 71, 145 | mulgt0d 11318 |
. . . . 5
โข (๐ โ 0 < (๐พ ยท ๐ท)) |
147 | | expgt0 14010 |
. . . . 5
โข (((๐พ ยท ๐ท) โ โ โง ๐ โ โค โง 0 < (๐พ ยท ๐ท)) โ 0 < ((๐พ ยท ๐ท)โ๐)) |
148 | 34, 70, 146, 147 | syl3anc 1372 |
. . . 4
โข (๐ โ 0 < ((๐พ ยท ๐ท)โ๐)) |
149 | 64, 19, 71 | ltled 11311 |
. . . . . 6
โข (๐ โ 0 โค ๐พ) |
150 | 64, 33, 145 | ltled 11311 |
. . . . . 6
โข (๐ โ 0 โค ๐ท) |
151 | 19, 33, 149, 150 | mulge0d 11740 |
. . . . 5
โข (๐ โ 0 โค (๐พ ยท ๐ท)) |
152 | | stoweidlem1.8 |
. . . . . 6
โข (๐ โ ๐ท โค ๐ด) |
153 | 33, 4, 19, 149, 152 | lemul2ad 12103 |
. . . . 5
โข (๐ โ (๐พ ยท ๐ท) โค (๐พ ยท ๐ด)) |
154 | | leexp1a 14089 |
. . . . 5
โข ((((๐พ ยท ๐ท) โ โ โง (๐พ ยท ๐ด) โ โ โง ๐ โ โ0) โง (0 โค
(๐พ ยท ๐ท) โง (๐พ ยท ๐ท) โค (๐พ ยท ๐ด))) โ ((๐พ ยท ๐ท)โ๐) โค ((๐พ ยท ๐ด)โ๐)) |
155 | 34, 20, 6, 151, 153, 154 | syl32anc 1379 |
. . . 4
โข (๐ โ ((๐พ ยท ๐ท)โ๐) โค ((๐พ ยท ๐ด)โ๐)) |
156 | 148, 155 | jca 513 |
. . 3
โข (๐ โ (0 < ((๐พ ยท ๐ท)โ๐) โง ((๐พ ยท ๐ท)โ๐) โค ((๐พ ยท ๐ด)โ๐))) |
157 | | lediv12a 12056 |
. . 3
โข ((((((1
โ (๐ดโ(2 ยท
๐)))โ(๐พโ๐)) โ โ โง 1 โ โ)
โง (0 โค ((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) โง ((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) โค 1)) โง ((((๐พ ยท ๐ท)โ๐) โ โ โง ((๐พ ยท ๐ด)โ๐) โ โ) โง (0 < ((๐พ ยท ๐ท)โ๐) โง ((๐พ ยท ๐ท)โ๐) โค ((๐พ ยท ๐ด)โ๐)))) โ (((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) / ((๐พ ยท ๐ด)โ๐)) โค (1 / ((๐พ ยท ๐ท)โ๐))) |
158 | 143, 144,
156, 157 | syl12anc 836 |
. 2
โข (๐ โ (((1 โ (๐ดโ(2 ยท ๐)))โ(๐พโ๐)) / ((๐พ ยท ๐ด)โ๐)) โค (1 / ((๐พ ยท ๐ท)โ๐))) |
159 | 12, 31, 43, 130, 158 | letrd 11320 |
1
โข (๐ โ ((1 โ (๐ดโ๐))โ(๐พโ๐)) โค (1 / ((๐พ ยท ๐ท)โ๐))) |