Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
๐ด โ
โ+) |
2 | 1 | rprege0d 12972 |
. . . . . . . . . . 11
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(๐ด โ โ โง 0
โค ๐ด)) |
3 | | flge0nn0 13734 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 โค
๐ด) โ
(โโ๐ด) โ
โ0) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โโ๐ด) โ
โ0) |
5 | 4 | faccld 14193 |
. . . . . . . . 9
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(!โ(โโ๐ด))
โ โ) |
6 | 5 | nnrpd 12963 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(!โ(โโ๐ด))
โ โ+) |
7 | | relogcl 25954 |
. . . . . . . 8
โข
((!โ(โโ๐ด)) โ โ+ โ
(logโ(!โ(โโ๐ด))) โ โ) |
8 | 6, 7 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(!โ(โโ๐ด))) โ โ) |
9 | | rpre 12931 |
. . . . . . . . 9
โข (๐ด โ โ+
โ ๐ด โ
โ) |
10 | 9 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
๐ด โ
โ) |
11 | | relogcl 25954 |
. . . . . . . . . 10
โข (๐ด โ โ+
โ (logโ๐ด) โ
โ) |
12 | 11 | adantr 482 |
. . . . . . . . 9
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ๐ด) โ
โ) |
13 | | peano2rem 11476 |
. . . . . . . . 9
โข
((logโ๐ด)
โ โ โ ((logโ๐ด) โ 1) โ
โ) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((logโ๐ด) โ 1)
โ โ) |
15 | 10, 14 | remulcld 11193 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(๐ด ยท
((logโ๐ด) โ 1))
โ โ) |
16 | 8, 15 | resubcld 11591 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ
โ) |
17 | 16 | recnd 11191 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ
โ) |
18 | 17 | abscld 15330 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โ
โ) |
19 | | peano2rem 11476 |
. . . 4
โข
((absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โ โ โ
((absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โ 1) โ
โ) |
20 | 18, 19 | syl 17 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โ 1) โ
โ) |
21 | | ax-1cn 11117 |
. . . . 5
โข 1 โ
โ |
22 | | subcl 11408 |
. . . . 5
โข
((((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ โ โง 1 โ
โ) โ (((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ 1) โ
โ) |
23 | 17, 21, 22 | sylancl 587 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ 1) โ
โ) |
24 | 23 | abscld 15330 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(absโ(((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ 1)) โ
โ) |
25 | | abs1 15191 |
. . . . 5
โข
(absโ1) = 1 |
26 | 25 | oveq2i 7372 |
. . . 4
โข
((absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โ (absโ1)) =
((absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โ 1) |
27 | | abs2dif 15226 |
. . . . 5
โข
((((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ โ โง 1 โ
โ) โ ((absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โ (absโ1)) โค
(absโ(((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ 1))) |
28 | 17, 21, 27 | sylancl 587 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โ (absโ1)) โค
(absโ(((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ 1))) |
29 | 26, 28 | eqbrtrrid 5145 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โ 1) โค
(absโ(((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ 1))) |
30 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ด โ (โโ๐ฅ) = (โโ๐ด)) |
31 | 30 | oveq2d 7377 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ด โ (1...(โโ๐ฅ)) = (1...(โโ๐ด))) |
32 | 31 | sumeq1d 15594 |
. . . . . . . . . 10
โข (๐ฅ = ๐ด โ ฮฃ๐ โ (1...(โโ๐ฅ))(logโ๐) = ฮฃ๐ โ (1...(โโ๐ด))(logโ๐)) |
33 | | id 22 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ด โ ๐ฅ = ๐ด) |
34 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ด โ (logโ๐ฅ) = (logโ๐ด)) |
35 | 34 | oveq1d 7376 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ด โ ((logโ๐ฅ) โ 1) = ((logโ๐ด) โ 1)) |
36 | 33, 35 | oveq12d 7379 |
. . . . . . . . . 10
โข (๐ฅ = ๐ด โ (๐ฅ ยท ((logโ๐ฅ) โ 1)) = (๐ด ยท ((logโ๐ด) โ 1))) |
37 | 32, 36 | oveq12d 7379 |
. . . . . . . . 9
โข (๐ฅ = ๐ด โ (ฮฃ๐ โ (1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))) = (ฮฃ๐ โ (1...(โโ๐ด))(logโ๐) โ (๐ด ยท ((logโ๐ด) โ 1)))) |
38 | | eqid 2733 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) = (๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) |
39 | | ovex 7394 |
. . . . . . . . 9
โข
(ฮฃ๐ โ
(1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))) โ V |
40 | 37, 38, 39 | fvmpt3i 6957 |
. . . . . . . 8
โข (๐ด โ โ+
โ ((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))))โ๐ด) = (ฮฃ๐ โ (1...(โโ๐ด))(logโ๐) โ (๐ด ยท ((logโ๐ด) โ 1)))) |
41 | 40 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))))โ๐ด) = (ฮฃ๐ โ (1...(โโ๐ด))(logโ๐) โ (๐ด ยท ((logโ๐ด) โ 1)))) |
42 | | logfac 25979 |
. . . . . . . . 9
โข
((โโ๐ด)
โ โ0 โ (logโ(!โ(โโ๐ด))) = ฮฃ๐ โ (1...(โโ๐ด))(logโ๐)) |
43 | 4, 42 | syl 17 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ(!โ(โโ๐ด))) = ฮฃ๐ โ (1...(โโ๐ด))(logโ๐)) |
44 | 43 | oveq1d 7376 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) = (ฮฃ๐ โ (1...(โโ๐ด))(logโ๐) โ (๐ด ยท ((logโ๐ด) โ 1)))) |
45 | 41, 44 | eqtr4d 2776 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))))โ๐ด) =
((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) |
46 | | 1rp 12927 |
. . . . . . 7
โข 1 โ
โ+ |
47 | | fveq2 6846 |
. . . . . . . . . . . . . 14
โข (๐ฅ = 1 โ (โโ๐ฅ) =
(โโ1)) |
48 | | 1z 12541 |
. . . . . . . . . . . . . . 15
โข 1 โ
โค |
49 | | flid 13722 |
. . . . . . . . . . . . . . 15
โข (1 โ
โค โ (โโ1) = 1) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
โข
(โโ1) = 1 |
51 | 47, 50 | eqtrdi 2789 |
. . . . . . . . . . . . 13
โข (๐ฅ = 1 โ (โโ๐ฅ) = 1) |
52 | 51 | oveq2d 7377 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ
(1...(โโ๐ฅ)) =
(1...1)) |
53 | 52 | sumeq1d 15594 |
. . . . . . . . . . 11
โข (๐ฅ = 1 โ ฮฃ๐ โ
(1...(โโ๐ฅ))(logโ๐) = ฮฃ๐ โ (1...1)(logโ๐)) |
54 | | 0cn 11155 |
. . . . . . . . . . . 12
โข 0 โ
โ |
55 | | fveq2 6846 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ (logโ๐) =
(logโ1)) |
56 | | log1 25964 |
. . . . . . . . . . . . . 14
โข
(logโ1) = 0 |
57 | 55, 56 | eqtrdi 2789 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ (logโ๐) = 0) |
58 | 57 | fsum1 15640 |
. . . . . . . . . . . 12
โข ((1
โ โค โง 0 โ โ) โ ฮฃ๐ โ (1...1)(logโ๐) = 0) |
59 | 48, 54, 58 | mp2an 691 |
. . . . . . . . . . 11
โข
ฮฃ๐ โ
(1...1)(logโ๐) =
0 |
60 | 53, 59 | eqtrdi 2789 |
. . . . . . . . . 10
โข (๐ฅ = 1 โ ฮฃ๐ โ
(1...(โโ๐ฅ))(logโ๐) = 0) |
61 | | id 22 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ ๐ฅ = 1) |
62 | | fveq2 6846 |
. . . . . . . . . . . . . 14
โข (๐ฅ = 1 โ (logโ๐ฅ) =
(logโ1)) |
63 | 62, 56 | eqtrdi 2789 |
. . . . . . . . . . . . 13
โข (๐ฅ = 1 โ (logโ๐ฅ) = 0) |
64 | 63 | oveq1d 7376 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ ((logโ๐ฅ) โ 1) = (0 โ
1)) |
65 | 61, 64 | oveq12d 7379 |
. . . . . . . . . . 11
โข (๐ฅ = 1 โ (๐ฅ ยท ((logโ๐ฅ) โ 1)) = (1 ยท (0 โ
1))) |
66 | 54, 21 | subcli 11485 |
. . . . . . . . . . . 12
โข (0
โ 1) โ โ |
67 | 66 | mulid2i 11168 |
. . . . . . . . . . 11
โข (1
ยท (0 โ 1)) = (0 โ 1) |
68 | 65, 67 | eqtrdi 2789 |
. . . . . . . . . 10
โข (๐ฅ = 1 โ (๐ฅ ยท ((logโ๐ฅ) โ 1)) = (0 โ
1)) |
69 | 60, 68 | oveq12d 7379 |
. . . . . . . . 9
โข (๐ฅ = 1 โ (ฮฃ๐ โ
(1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))) = (0 โ (0 โ
1))) |
70 | | nncan 11438 |
. . . . . . . . . 10
โข ((0
โ โ โง 1 โ โ) โ (0 โ (0 โ 1)) =
1) |
71 | 54, 21, 70 | mp2an 691 |
. . . . . . . . 9
โข (0
โ (0 โ 1)) = 1 |
72 | 69, 71 | eqtrdi 2789 |
. . . . . . . 8
โข (๐ฅ = 1 โ (ฮฃ๐ โ
(1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))) = 1) |
73 | 72, 38, 39 | fvmpt3i 6957 |
. . . . . . 7
โข (1 โ
โ+ โ ((๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))))โ1) =
1) |
74 | 46, 73 | mp1i 13 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))))โ1) =
1) |
75 | 45, 74 | oveq12d 7379 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))))โ๐ด) โ ((๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))))โ1)) =
(((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ 1)) |
76 | 75 | fveq2d 6850 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(absโ(((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))))โ๐ด) โ ((๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))))โ1))) =
(absโ(((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ 1))) |
77 | | ioorp 13351 |
. . . . . 6
โข
(0(,)+โ) = โ+ |
78 | 77 | eqcomi 2742 |
. . . . 5
โข
โ+ = (0(,)+โ) |
79 | | nnuz 12814 |
. . . . 5
โข โ =
(โคโฅโ1) |
80 | 48 | a1i 11 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โ โค) |
81 | | 1re 11163 |
. . . . . 6
โข 1 โ
โ |
82 | 81 | a1i 11 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โ โ) |
83 | | pnfxr 11217 |
. . . . . 6
โข +โ
โ โ* |
84 | 83 | a1i 11 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
+โ โ โ*) |
85 | | 1nn0 12437 |
. . . . . . 7
โข 1 โ
โ0 |
86 | 81, 85 | nn0addge1i 12469 |
. . . . . 6
โข 1 โค (1
+ 1) |
87 | 86 | a1i 11 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โค (1 + 1)) |
88 | | 0red 11166 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 0
โ โ) |
89 | | rpre 12931 |
. . . . . . 7
โข (๐ฅ โ โ+
โ ๐ฅ โ
โ) |
90 | 89 | adantl 483 |
. . . . . 6
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ๐ฅ โ
โ) |
91 | | relogcl 25954 |
. . . . . . . 8
โข (๐ฅ โ โ+
โ (logโ๐ฅ) โ
โ) |
92 | 91 | adantl 483 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (logโ๐ฅ) โ
โ) |
93 | | peano2rem 11476 |
. . . . . . 7
โข
((logโ๐ฅ)
โ โ โ ((logโ๐ฅ) โ 1) โ โ) |
94 | 92, 93 | syl 17 |
. . . . . 6
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ((logโ๐ฅ)
โ 1) โ โ) |
95 | 90, 94 | remulcld 11193 |
. . . . 5
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (๐ฅ ยท
((logโ๐ฅ) โ 1))
โ โ) |
96 | | nnrp 12934 |
. . . . . 6
โข (๐ฅ โ โ โ ๐ฅ โ
โ+) |
97 | 96, 92 | sylan2 594 |
. . . . 5
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ) โ
(logโ๐ฅ) โ
โ) |
98 | | advlog 26032 |
. . . . . 6
โข (โ
D (๐ฅ โ
โ+ โฆ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) = (๐ฅ โ โ+ โฆ
(logโ๐ฅ)) |
99 | 98 | a1i 11 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ+ โฆ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) = (๐ฅ โ โ+ โฆ
(logโ๐ฅ))) |
100 | | fveq2 6846 |
. . . . 5
โข (๐ฅ = ๐ โ (logโ๐ฅ) = (logโ๐)) |
101 | | simp32 1211 |
. . . . . 6
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ ๐ฅ โค ๐) |
102 | | logleb 25981 |
. . . . . . 7
โข ((๐ฅ โ โ+
โง ๐ โ
โ+) โ (๐ฅ โค ๐ โ (logโ๐ฅ) โค (logโ๐))) |
103 | 102 | 3ad2ant2 1135 |
. . . . . 6
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ (๐ฅ โค ๐ โ (logโ๐ฅ) โค (logโ๐))) |
104 | 101, 103 | mpbid 231 |
. . . . 5
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ (logโ๐ฅ) โค (logโ๐)) |
105 | | simprr 772 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง 1 โค ๐ฅ)) โ 1 โค ๐ฅ) |
106 | | simprl 770 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง 1 โค ๐ฅ)) โ ๐ฅ โ โ+) |
107 | | logleb 25981 |
. . . . . . . 8
โข ((1
โ โ+ โง ๐ฅ โ โ+) โ (1 โค
๐ฅ โ (logโ1) โค
(logโ๐ฅ))) |
108 | 46, 106, 107 | sylancr 588 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง 1 โค ๐ฅ)) โ (1 โค ๐ฅ โ (logโ1) โค (logโ๐ฅ))) |
109 | 105, 108 | mpbid 231 |
. . . . . 6
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง 1 โค ๐ฅ)) โ (logโ1) โค (logโ๐ฅ)) |
110 | 56, 109 | eqbrtrrid 5145 |
. . . . 5
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง 1 โค ๐ฅ)) โ 0 โค (logโ๐ฅ)) |
111 | 46 | a1i 11 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โ โ+) |
112 | | 1le1 11791 |
. . . . . 6
โข 1 โค
1 |
113 | 112 | a1i 11 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โค 1) |
114 | | simpr 486 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โค ๐ด) |
115 | 10 | rexrd 11213 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
๐ด โ
โ*) |
116 | | pnfge 13059 |
. . . . . 6
โข (๐ด โ โ*
โ ๐ด โค
+โ) |
117 | 115, 116 | syl 17 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
๐ด โค
+โ) |
118 | 78, 79, 80, 82, 84, 87, 88, 95, 92, 97, 99, 100, 104, 38, 110, 111, 1, 113, 114, 117, 34 | dvfsum2 25421 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(absโ(((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))))โ๐ด) โ ((๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))(logโ๐) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))))โ1))) โค
(logโ๐ด)) |
119 | 76, 118 | eqbrtrrd 5133 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(absโ(((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1))) โ 1)) โค
(logโ๐ด)) |
120 | 20, 24, 12, 29, 119 | letrd 11320 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โ 1) โค
(logโ๐ด)) |
121 | 18, 82, 12 | lesubaddd 11760 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(((absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โ 1) โค
(logโ๐ด) โ
(absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โค ((logโ๐ด) + 1))) |
122 | 120, 121 | mpbid 231 |
1
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(absโ((logโ(!โ(โโ๐ด))) โ (๐ด ยท ((logโ๐ด) โ 1)))) โค ((logโ๐ด) + 1)) |