Step | Hyp | Ref
| Expression |
1 | | lgamgulm.r |
. . . . . . . 8
โข (๐ โ ๐
โ โ) |
2 | | lgamgulm.u |
. . . . . . . 8
โข ๐ = {๐ฅ โ โ โฃ ((absโ๐ฅ) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฅ + ๐)))} |
3 | 1, 2 | lgamgulmlem1 26415 |
. . . . . . 7
โข (๐ โ ๐ โ (โ โ (โค โ
โ))) |
4 | | lgamgulm.a |
. . . . . . 7
โข (๐ โ ๐ด โ ๐) |
5 | 3, 4 | sseldd 3948 |
. . . . . 6
โข (๐ โ ๐ด โ (โ โ (โค โ
โ))) |
6 | 5 | eldifad 3925 |
. . . . 5
โข (๐ โ ๐ด โ โ) |
7 | | lgamgulm.n |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
8 | 7 | peano2nnd 12179 |
. . . . . . . . 9
โข (๐ โ (๐ + 1) โ โ) |
9 | 8 | nnrpd 12964 |
. . . . . . . 8
โข (๐ โ (๐ + 1) โ
โ+) |
10 | 7 | nnrpd 12964 |
. . . . . . . 8
โข (๐ โ ๐ โ
โ+) |
11 | 9, 10 | rpdivcld 12983 |
. . . . . . 7
โข (๐ โ ((๐ + 1) / ๐) โ
โ+) |
12 | 11 | relogcld 26015 |
. . . . . 6
โข (๐ โ (logโ((๐ + 1) / ๐)) โ โ) |
13 | 12 | recnd 11192 |
. . . . 5
โข (๐ โ (logโ((๐ + 1) / ๐)) โ โ) |
14 | 6, 13 | mulcld 11184 |
. . . 4
โข (๐ โ (๐ด ยท (logโ((๐ + 1) / ๐))) โ โ) |
15 | 7 | nncnd 12178 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
16 | 7 | nnne0d 12212 |
. . . . . . 7
โข (๐ โ ๐ โ 0) |
17 | 6, 15, 16 | divcld 11940 |
. . . . . 6
โข (๐ โ (๐ด / ๐) โ โ) |
18 | | 1cnd 11159 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
19 | 17, 18 | addcld 11183 |
. . . . 5
โข (๐ โ ((๐ด / ๐) + 1) โ โ) |
20 | 5, 7 | dmgmdivn0 26414 |
. . . . 5
โข (๐ โ ((๐ด / ๐) + 1) โ 0) |
21 | 19, 20 | logcld 25963 |
. . . 4
โข (๐ โ (logโ((๐ด / ๐) + 1)) โ โ) |
22 | 14, 21 | subcld 11521 |
. . 3
โข (๐ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ โ) |
23 | 22 | abscld 15333 |
. 2
โข (๐ โ (absโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) โ โ) |
24 | 14, 17 | subcld 11521 |
. . . 4
โข (๐ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด / ๐)) โ โ) |
25 | 24 | abscld 15333 |
. . 3
โข (๐ โ (absโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด / ๐))) โ โ) |
26 | 17, 21 | subcld 11521 |
. . . 4
โข (๐ โ ((๐ด / ๐) โ (logโ((๐ด / ๐) + 1))) โ โ) |
27 | 26 | abscld 15333 |
. . 3
โข (๐ โ (absโ((๐ด / ๐) โ (logโ((๐ด / ๐) + 1)))) โ โ) |
28 | 25, 27 | readdcld 11193 |
. 2
โข (๐ โ ((absโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด / ๐))) + (absโ((๐ด / ๐) โ (logโ((๐ด / ๐) + 1))))) โ โ) |
29 | 1 | nnred 12177 |
. . 3
โข (๐ โ ๐
โ โ) |
30 | | 2re 12236 |
. . . . . 6
โข 2 โ
โ |
31 | 30 | a1i 11 |
. . . . 5
โข (๐ โ 2 โ
โ) |
32 | | 1red 11165 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
33 | 29, 32 | readdcld 11193 |
. . . . 5
โข (๐ โ (๐
+ 1) โ โ) |
34 | 31, 33 | remulcld 11194 |
. . . 4
โข (๐ โ (2 ยท (๐
+ 1)) โ
โ) |
35 | 7 | nnsqcld 14157 |
. . . 4
โข (๐ โ (๐โ2) โ โ) |
36 | 34, 35 | nndivred 12216 |
. . 3
โข (๐ โ ((2 ยท (๐
+ 1)) / (๐โ2)) โ โ) |
37 | 29, 36 | remulcld 11194 |
. 2
โข (๐ โ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))) โ โ) |
38 | 14, 21, 17 | abs3difd 15357 |
. 2
โข (๐ โ (absโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) โค ((absโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด / ๐))) + (absโ((๐ด / ๐) โ (logโ((๐ด / ๐) + 1)))))) |
39 | 7 | nnrecred 12213 |
. . . . . 6
โข (๐ โ (1 / ๐) โ โ) |
40 | 8 | nnrecred 12213 |
. . . . . 6
โข (๐ โ (1 / (๐ + 1)) โ โ) |
41 | 39, 40 | resubcld 11592 |
. . . . 5
โข (๐ โ ((1 / ๐) โ (1 / (๐ + 1))) โ โ) |
42 | 29, 41 | remulcld 11194 |
. . . 4
โข (๐ โ (๐
ยท ((1 / ๐) โ (1 / (๐ + 1)))) โ โ) |
43 | 31, 29 | remulcld 11194 |
. . . . . . . . 9
โข (๐ โ (2 ยท ๐
) โ
โ) |
44 | 7 | nnred 12177 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
45 | 1 | nnrpd 12964 |
. . . . . . . . . . 11
โข (๐ โ ๐
โ
โ+) |
46 | 29, 45 | ltaddrpd 12999 |
. . . . . . . . . 10
โข (๐ โ ๐
< (๐
+ ๐
)) |
47 | 1 | nncnd 12178 |
. . . . . . . . . . 11
โข (๐ โ ๐
โ โ) |
48 | 47 | 2timesd 12405 |
. . . . . . . . . 10
โข (๐ โ (2 ยท ๐
) = (๐
+ ๐
)) |
49 | 46, 48 | breqtrrd 5138 |
. . . . . . . . 9
โข (๐ โ ๐
< (2 ยท ๐
)) |
50 | | lgamgulm.l |
. . . . . . . . 9
โข (๐ โ (2 ยท ๐
) โค ๐) |
51 | 29, 43, 44, 49, 50 | ltletrd 11324 |
. . . . . . . 8
โข (๐ โ ๐
< ๐) |
52 | | difrp 12962 |
. . . . . . . . 9
โข ((๐
โ โ โง ๐ โ โ) โ (๐
< ๐ โ (๐ โ ๐
) โ
โ+)) |
53 | 29, 44, 52 | syl2anc 584 |
. . . . . . . 8
โข (๐ โ (๐
< ๐ โ (๐ โ ๐
) โ
โ+)) |
54 | 51, 53 | mpbid 231 |
. . . . . . 7
โข (๐ โ (๐ โ ๐
) โ
โ+) |
55 | 54 | rprecred 12977 |
. . . . . 6
โข (๐ โ (1 / (๐ โ ๐
)) โ โ) |
56 | 55, 39 | resubcld 11592 |
. . . . 5
โข (๐ โ ((1 / (๐ โ ๐
)) โ (1 / ๐)) โ โ) |
57 | 29, 56 | remulcld 11194 |
. . . 4
โข (๐ โ (๐
ยท ((1 / (๐ โ ๐
)) โ (1 / ๐))) โ โ) |
58 | 42, 57 | readdcld 11193 |
. . 3
โข (๐ โ ((๐
ยท ((1 / ๐) โ (1 / (๐ + 1)))) + (๐
ยท ((1 / (๐ โ ๐
)) โ (1 / ๐)))) โ โ) |
59 | 6, 15, 16 | divrecd 11943 |
. . . . . . . . 9
โข (๐ โ (๐ด / ๐) = (๐ด ยท (1 / ๐))) |
60 | 59 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด / ๐)) = ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด ยท (1 / ๐)))) |
61 | 39 | recnd 11192 |
. . . . . . . . 9
โข (๐ โ (1 / ๐) โ โ) |
62 | 6, 13, 61 | subdid 11620 |
. . . . . . . 8
โข (๐ โ (๐ด ยท ((logโ((๐ + 1) / ๐)) โ (1 / ๐))) = ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด ยท (1 / ๐)))) |
63 | 60, 62 | eqtr4d 2774 |
. . . . . . 7
โข (๐ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด / ๐)) = (๐ด ยท ((logโ((๐ + 1) / ๐)) โ (1 / ๐)))) |
64 | 63 | fveq2d 6851 |
. . . . . 6
โข (๐ โ (absโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด / ๐))) = (absโ(๐ด ยท ((logโ((๐ + 1) / ๐)) โ (1 / ๐))))) |
65 | 13, 61 | subcld 11521 |
. . . . . . 7
โข (๐ โ ((logโ((๐ + 1) / ๐)) โ (1 / ๐)) โ โ) |
66 | 6, 65 | absmuld 15351 |
. . . . . 6
โข (๐ โ (absโ(๐ด ยท ((logโ((๐ + 1) / ๐)) โ (1 / ๐)))) = ((absโ๐ด) ยท (absโ((logโ((๐ + 1) / ๐)) โ (1 / ๐))))) |
67 | 64, 66 | eqtrd 2771 |
. . . . 5
โข (๐ โ (absโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด / ๐))) = ((absโ๐ด) ยท (absโ((logโ((๐ + 1) / ๐)) โ (1 / ๐))))) |
68 | 6 | abscld 15333 |
. . . . . 6
โข (๐ โ (absโ๐ด) โ
โ) |
69 | 65 | abscld 15333 |
. . . . . 6
โข (๐ โ
(absโ((logโ((๐
+ 1) / ๐)) โ (1 /
๐))) โ
โ) |
70 | 6 | absge0d 15341 |
. . . . . 6
โข (๐ โ 0 โค (absโ๐ด)) |
71 | 65 | absge0d 15341 |
. . . . . 6
โข (๐ โ 0 โค
(absโ((logโ((๐
+ 1) / ๐)) โ (1 /
๐)))) |
72 | | fveq2 6847 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ด โ (absโ๐ฅ) = (absโ๐ด)) |
73 | 72 | breq1d 5120 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ด โ ((absโ๐ฅ) โค ๐
โ (absโ๐ด) โค ๐
)) |
74 | | fvoveq1 7385 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ด โ (absโ(๐ฅ + ๐)) = (absโ(๐ด + ๐))) |
75 | 74 | breq2d 5122 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ด โ ((1 / ๐
) โค (absโ(๐ฅ + ๐)) โ (1 / ๐
) โค (absโ(๐ด + ๐)))) |
76 | 75 | ralbidv 3170 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ด โ (โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฅ + ๐)) โ โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ด + ๐)))) |
77 | 73, 76 | anbi12d 631 |
. . . . . . . . . 10
โข (๐ฅ = ๐ด โ (((absโ๐ฅ) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฅ + ๐))) โ ((absโ๐ด) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ด + ๐))))) |
78 | 77, 2 | elrab2 3651 |
. . . . . . . . 9
โข (๐ด โ ๐ โ (๐ด โ โ โง ((absโ๐ด) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ด + ๐))))) |
79 | 78 | simprbi 497 |
. . . . . . . 8
โข (๐ด โ ๐ โ ((absโ๐ด) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ด + ๐)))) |
80 | 4, 79 | syl 17 |
. . . . . . 7
โข (๐ โ ((absโ๐ด) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ด + ๐)))) |
81 | 80 | simpld 495 |
. . . . . 6
โข (๐ โ (absโ๐ด) โค ๐
) |
82 | 9, 10 | relogdivd 26018 |
. . . . . . . . 9
โข (๐ โ (logโ((๐ + 1) / ๐)) = ((logโ(๐ + 1)) โ (logโ๐))) |
83 | | logdifbnd 26380 |
. . . . . . . . . 10
โข (๐ โ โ+
โ ((logโ(๐ + 1))
โ (logโ๐)) โค
(1 / ๐)) |
84 | 10, 83 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((logโ(๐ + 1)) โ (logโ๐)) โค (1 / ๐)) |
85 | 82, 84 | eqbrtrd 5132 |
. . . . . . . 8
โข (๐ โ (logโ((๐ + 1) / ๐)) โค (1 / ๐)) |
86 | 12, 39, 85 | abssuble0d 15329 |
. . . . . . 7
โข (๐ โ
(absโ((logโ((๐
+ 1) / ๐)) โ (1 /
๐))) = ((1 / ๐) โ (logโ((๐ + 1) / ๐)))) |
87 | | logdiflbnd 26381 |
. . . . . . . . . 10
โข (๐ โ โ+
โ (1 / (๐ + 1)) โค
((logโ(๐ + 1))
โ (logโ๐))) |
88 | 10, 87 | syl 17 |
. . . . . . . . 9
โข (๐ โ (1 / (๐ + 1)) โค ((logโ(๐ + 1)) โ (logโ๐))) |
89 | 88, 82 | breqtrrd 5138 |
. . . . . . . 8
โข (๐ โ (1 / (๐ + 1)) โค (logโ((๐ + 1) / ๐))) |
90 | 40, 12, 39, 89 | lesub2dd 11781 |
. . . . . . 7
โข (๐ โ ((1 / ๐) โ (logโ((๐ + 1) / ๐))) โค ((1 / ๐) โ (1 / (๐ + 1)))) |
91 | 86, 90 | eqbrtrd 5132 |
. . . . . 6
โข (๐ โ
(absโ((logโ((๐
+ 1) / ๐)) โ (1 /
๐))) โค ((1 / ๐) โ (1 / (๐ + 1)))) |
92 | 68, 29, 69, 41, 70, 71, 81, 91 | lemul12ad 12106 |
. . . . 5
โข (๐ โ ((absโ๐ด) ยท
(absโ((logโ((๐
+ 1) / ๐)) โ (1 /
๐)))) โค (๐
ยท ((1 / ๐) โ (1 / (๐ + 1))))) |
93 | 67, 92 | eqbrtrd 5132 |
. . . 4
โข (๐ โ (absโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด / ๐))) โค (๐
ยท ((1 / ๐) โ (1 / (๐ + 1))))) |
94 | 1, 2, 7, 4, 50 | lgamgulmlem2 26416 |
. . . 4
โข (๐ โ (absโ((๐ด / ๐) โ (logโ((๐ด / ๐) + 1)))) โค (๐
ยท ((1 / (๐ โ ๐
)) โ (1 / ๐)))) |
95 | 25, 27, 42, 57, 93, 94 | le2addd 11783 |
. . 3
โข (๐ โ ((absโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด / ๐))) + (absโ((๐ด / ๐) โ (logโ((๐ด / ๐) + 1))))) โค ((๐
ยท ((1 / ๐) โ (1 / (๐ + 1)))) + (๐
ยท ((1 / (๐ โ ๐
)) โ (1 / ๐))))) |
96 | 15, 47 | subcld 11521 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐
) โ โ) |
97 | 15, 18 | addcld 11183 |
. . . . . . . 8
โข (๐ โ (๐ + 1) โ โ) |
98 | 29, 51 | gtned 11299 |
. . . . . . . . 9
โข (๐ โ ๐ โ ๐
) |
99 | 15, 47, 98 | subne0d 11530 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐
) โ 0) |
100 | 8 | nnne0d 12212 |
. . . . . . . 8
โข (๐ โ (๐ + 1) โ 0) |
101 | 96, 97, 99, 100 | subrecd 11995 |
. . . . . . 7
โข (๐ โ ((1 / (๐ โ ๐
)) โ (1 / (๐ + 1))) = (((๐ + 1) โ (๐ โ ๐
)) / ((๐ โ ๐
) ยท (๐ + 1)))) |
102 | 15, 18, 47 | pnncand 11560 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1) โ (๐ โ ๐
)) = (1 + ๐
)) |
103 | 18, 47, 102 | comraddd 11378 |
. . . . . . . 8
โข (๐ โ ((๐ + 1) โ (๐ โ ๐
)) = (๐
+ 1)) |
104 | 103 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ (((๐ + 1) โ (๐ โ ๐
)) / ((๐ โ ๐
) ยท (๐ + 1))) = ((๐
+ 1) / ((๐ โ ๐
) ยท (๐ + 1)))) |
105 | 101, 104 | eqtr2d 2772 |
. . . . . 6
โข (๐ โ ((๐
+ 1) / ((๐ โ ๐
) ยท (๐ + 1))) = ((1 / (๐ โ ๐
)) โ (1 / (๐ + 1)))) |
106 | 105 | oveq2d 7378 |
. . . . 5
โข (๐ โ (๐
ยท ((๐
+ 1) / ((๐ โ ๐
) ยท (๐ + 1)))) = (๐
ยท ((1 / (๐ โ ๐
)) โ (1 / (๐ + 1))))) |
107 | 97, 100 | reccld 11933 |
. . . . . . . 8
โข (๐ โ (1 / (๐ + 1)) โ โ) |
108 | 96, 99 | reccld 11933 |
. . . . . . . 8
โข (๐ โ (1 / (๐ โ ๐
)) โ โ) |
109 | 61, 107, 108 | npncan3d 11557 |
. . . . . . 7
โข (๐ โ (((1 / ๐) โ (1 / (๐ + 1))) + ((1 / (๐ โ ๐
)) โ (1 / ๐))) = ((1 / (๐ โ ๐
)) โ (1 / (๐ + 1)))) |
110 | 109 | eqcomd 2737 |
. . . . . 6
โข (๐ โ ((1 / (๐ โ ๐
)) โ (1 / (๐ + 1))) = (((1 / ๐) โ (1 / (๐ + 1))) + ((1 / (๐ โ ๐
)) โ (1 / ๐)))) |
111 | 110 | oveq2d 7378 |
. . . . 5
โข (๐ โ (๐
ยท ((1 / (๐ โ ๐
)) โ (1 / (๐ + 1)))) = (๐
ยท (((1 / ๐) โ (1 / (๐ + 1))) + ((1 / (๐ โ ๐
)) โ (1 / ๐))))) |
112 | 41 | recnd 11192 |
. . . . . 6
โข (๐ โ ((1 / ๐) โ (1 / (๐ + 1))) โ โ) |
113 | 56 | recnd 11192 |
. . . . . 6
โข (๐ โ ((1 / (๐ โ ๐
)) โ (1 / ๐)) โ โ) |
114 | 47, 112, 113 | adddid 11188 |
. . . . 5
โข (๐ โ (๐
ยท (((1 / ๐) โ (1 / (๐ + 1))) + ((1 / (๐ โ ๐
)) โ (1 / ๐)))) = ((๐
ยท ((1 / ๐) โ (1 / (๐ + 1)))) + (๐
ยท ((1 / (๐ โ ๐
)) โ (1 / ๐))))) |
115 | 106, 111,
114 | 3eqtrd 2775 |
. . . 4
โข (๐ โ (๐
ยท ((๐
+ 1) / ((๐ โ ๐
) ยท (๐ + 1)))) = ((๐
ยท ((1 / ๐) โ (1 / (๐ + 1)))) + (๐
ยท ((1 / (๐ โ ๐
)) โ (1 / ๐))))) |
116 | 54, 9 | rpmulcld 12982 |
. . . . . 6
โข (๐ โ ((๐ โ ๐
) ยท (๐ + 1)) โ
โ+) |
117 | 33, 116 | rerpdivcld 12997 |
. . . . 5
โข (๐ โ ((๐
+ 1) / ((๐ โ ๐
) ยท (๐ + 1))) โ โ) |
118 | 45 | rpge0d 12970 |
. . . . 5
โข (๐ โ 0 โค ๐
) |
119 | | 2z 12544 |
. . . . . . . . . 10
โข 2 โ
โค |
120 | 119 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 2 โ
โค) |
121 | 10, 120 | rpexpcld 14160 |
. . . . . . . 8
โข (๐ โ (๐โ2) โ
โ+) |
122 | 121 | rphalfcld 12978 |
. . . . . . 7
โข (๐ โ ((๐โ2) / 2) โ
โ+) |
123 | | 0le1 11687 |
. . . . . . . . 9
โข 0 โค
1 |
124 | 123 | a1i 11 |
. . . . . . . 8
โข (๐ โ 0 โค 1) |
125 | 29, 32, 118, 124 | addge0d 11740 |
. . . . . . 7
โข (๐ โ 0 โค (๐
+ 1)) |
126 | 15 | sqvald 14058 |
. . . . . . . . . 10
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
127 | 126 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ ((๐โ2) / 2) = ((๐ ยท ๐) / 2)) |
128 | 31 | recnd 11192 |
. . . . . . . . . 10
โข (๐ โ 2 โ
โ) |
129 | | 2ne0 12266 |
. . . . . . . . . . 11
โข 2 โ
0 |
130 | 129 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 2 โ 0) |
131 | 15, 15, 128, 130 | div23d 11977 |
. . . . . . . . 9
โข (๐ โ ((๐ ยท ๐) / 2) = ((๐ / 2) ยท ๐)) |
132 | 127, 131 | eqtrd 2771 |
. . . . . . . 8
โข (๐ โ ((๐โ2) / 2) = ((๐ / 2) ยท ๐)) |
133 | 44 | rehalfcld 12409 |
. . . . . . . . 9
โข (๐ โ (๐ / 2) โ โ) |
134 | 44, 29 | resubcld 11592 |
. . . . . . . . 9
โข (๐ โ (๐ โ ๐
) โ โ) |
135 | 44, 32 | readdcld 11193 |
. . . . . . . . 9
โข (๐ โ (๐ + 1) โ โ) |
136 | | 2rp 12929 |
. . . . . . . . . . 11
โข 2 โ
โ+ |
137 | 136 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 2 โ
โ+) |
138 | 10 | rpge0d 12970 |
. . . . . . . . . 10
โข (๐ โ 0 โค ๐) |
139 | 44, 137, 138 | divge0d 13006 |
. . . . . . . . 9
โข (๐ โ 0 โค (๐ / 2)) |
140 | 29, 44, 137 | lemuldiv2d 13016 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ๐
) โค ๐ โ ๐
โค (๐ / 2))) |
141 | 50, 140 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ ๐
โค (๐ / 2)) |
142 | 15 | 2halvesd 12408 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ / 2) + (๐ / 2)) = ๐) |
143 | 133 | recnd 11192 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ / 2) โ โ) |
144 | 15, 143, 143 | subaddd 11539 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ โ (๐ / 2)) = (๐ / 2) โ ((๐ / 2) + (๐ / 2)) = ๐)) |
145 | 142, 144 | mpbird 256 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ (๐ / 2)) = (๐ / 2)) |
146 | 141, 145 | breqtrrd 5138 |
. . . . . . . . . 10
โข (๐ โ ๐
โค (๐ โ (๐ / 2))) |
147 | 29, 44, 133, 146 | lesubd 11768 |
. . . . . . . . 9
โข (๐ โ (๐ / 2) โค (๐ โ ๐
)) |
148 | 44 | lep1d 12095 |
. . . . . . . . 9
โข (๐ โ ๐ โค (๐ + 1)) |
149 | 133, 134,
44, 135, 139, 138, 147, 148 | lemul12ad 12106 |
. . . . . . . 8
โข (๐ โ ((๐ / 2) ยท ๐) โค ((๐ โ ๐
) ยท (๐ + 1))) |
150 | 132, 149 | eqbrtrd 5132 |
. . . . . . 7
โข (๐ โ ((๐โ2) / 2) โค ((๐ โ ๐
) ยท (๐ + 1))) |
151 | 122, 116,
33, 125, 150 | lediv2ad 12988 |
. . . . . 6
โข (๐ โ ((๐
+ 1) / ((๐ โ ๐
) ยท (๐ + 1))) โค ((๐
+ 1) / ((๐โ2) / 2))) |
152 | 1 | peano2nnd 12179 |
. . . . . . . . 9
โข (๐ โ (๐
+ 1) โ โ) |
153 | 152 | nncnd 12178 |
. . . . . . . 8
โข (๐ โ (๐
+ 1) โ โ) |
154 | 35 | nncnd 12178 |
. . . . . . . 8
โข (๐ โ (๐โ2) โ โ) |
155 | 35 | nnne0d 12212 |
. . . . . . . 8
โข (๐ โ (๐โ2) โ 0) |
156 | 153, 154,
128, 155, 130 | divdiv2d 11972 |
. . . . . . 7
โข (๐ โ ((๐
+ 1) / ((๐โ2) / 2)) = (((๐
+ 1) ยท 2) / (๐โ2))) |
157 | 153, 128 | mulcomd 11185 |
. . . . . . . 8
โข (๐ โ ((๐
+ 1) ยท 2) = (2 ยท (๐
+ 1))) |
158 | 157 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ (((๐
+ 1) ยท 2) / (๐โ2)) = ((2 ยท (๐
+ 1)) / (๐โ2))) |
159 | 156, 158 | eqtr2d 2772 |
. . . . . 6
โข (๐ โ ((2 ยท (๐
+ 1)) / (๐โ2)) = ((๐
+ 1) / ((๐โ2) / 2))) |
160 | 151, 159 | breqtrrd 5138 |
. . . . 5
โข (๐ โ ((๐
+ 1) / ((๐ โ ๐
) ยท (๐ + 1))) โค ((2 ยท (๐
+ 1)) / (๐โ2))) |
161 | 117, 36, 29, 118, 160 | lemul2ad 12104 |
. . . 4
โข (๐ โ (๐
ยท ((๐
+ 1) / ((๐ โ ๐
) ยท (๐ + 1)))) โค (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))) |
162 | 115, 161 | eqbrtrrd 5134 |
. . 3
โข (๐ โ ((๐
ยท ((1 / ๐) โ (1 / (๐ + 1)))) + (๐
ยท ((1 / (๐ โ ๐
)) โ (1 / ๐)))) โค (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))) |
163 | 28, 58, 37, 95, 162 | letrd 11321 |
. 2
โข (๐ โ ((absโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (๐ด / ๐))) + (absโ((๐ด / ๐) โ (logโ((๐ด / ๐) + 1))))) โค (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))) |
164 | 23, 28, 37, 38, 163 | letrd 11321 |
1
โข (๐ โ (absโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) โค (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))) |