Step | Hyp | Ref
| Expression |
1 | | fzfid 13887 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(1...(โโ๐ด))
โ Fin) |
2 | | elfznn 13479 |
. . . . . . . . . . . 12
โข (๐ โ
(1...(โโ๐ด))
โ ๐ โ
โ) |
3 | 2 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ โ
(1...(โโ๐ด)))
โ ๐ โ
โ) |
4 | 3 | nnrpd 12963 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ โ
(1...(โโ๐ด)))
โ ๐ โ
โ+) |
5 | 4 | relogcld 26001 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ โ
(1...(โโ๐ด)))
โ (logโ๐) โ
โ) |
6 | 5 | resqcld 14039 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ โ
(1...(โโ๐ด)))
โ ((logโ๐)โ2) โ โ) |
7 | 1, 6 | fsumrecl 15627 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
ฮฃ๐ โ
(1...(โโ๐ด))((logโ๐)โ2) โ โ) |
8 | | rpre 12931 |
. . . . . . . . 9
โข (๐ด โ โ+
โ ๐ด โ
โ) |
9 | 8 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
๐ด โ
โ) |
10 | | relogcl 25954 |
. . . . . . . . . . 11
โข (๐ด โ โ+
โ (logโ๐ด) โ
โ) |
11 | 10 | adantr 482 |
. . . . . . . . . 10
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(logโ๐ด) โ
โ) |
12 | 11 | resqcld 14039 |
. . . . . . . . 9
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((logโ๐ด)โ2)
โ โ) |
13 | | 2re 12235 |
. . . . . . . . . 10
โข 2 โ
โ |
14 | | remulcl 11144 |
. . . . . . . . . . 11
โข ((2
โ โ โง (logโ๐ด) โ โ) โ (2 ยท
(logโ๐ด)) โ
โ) |
15 | 13, 11, 14 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ (2
ยท (logโ๐ด))
โ โ) |
16 | | resubcl 11473 |
. . . . . . . . . 10
โข ((2
โ โ โง (2 ยท (logโ๐ด)) โ โ) โ (2 โ (2
ยท (logโ๐ด)))
โ โ) |
17 | 13, 15, 16 | sylancr 588 |
. . . . . . . . 9
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ (2
โ (2 ยท (logโ๐ด))) โ โ) |
18 | 12, 17 | readdcld 11192 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(((logโ๐ด)โ2) +
(2 โ (2 ยท (logโ๐ด)))) โ โ) |
19 | 9, 18 | remulcld 11193 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(๐ด ยท
(((logโ๐ด)โ2) +
(2 โ (2 ยท (logโ๐ด))))) โ โ) |
20 | 7, 19 | resubcld 11591 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(ฮฃ๐ โ
(1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
โ) |
21 | 20 | recnd 11191 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(ฮฃ๐ โ
(1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
โ) |
22 | 21 | abscld 15330 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(absโ(ฮฃ๐ โ
(1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โ
โ) |
23 | | resubcl 11473 |
. . . 4
โข
(((absโ(ฮฃ๐ โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โ
โ โง 2 โ โ) โ ((absโ(ฮฃ๐ โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โ
2) โ โ) |
24 | 22, 13, 23 | sylancl 587 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((absโ(ฮฃ๐
โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โ
2) โ โ) |
25 | | 2cn 12236 |
. . . . . 6
โข 2 โ
โ |
26 | 25 | negcli 11477 |
. . . . 5
โข -2 โ
โ |
27 | | subcl 11408 |
. . . . 5
โข
(((ฮฃ๐ โ
(1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
โ โง -2 โ โ) โ ((ฮฃ๐ โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
-2) โ โ) |
28 | 21, 26, 27 | sylancl 587 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((ฮฃ๐ โ
(1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
-2) โ โ) |
29 | 28 | abscld 15330 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(absโ((ฮฃ๐
โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
-2)) โ โ) |
30 | 25 | absnegi 15294 |
. . . . . 6
โข
(absโ-2) = (absโ2) |
31 | | 0le2 12263 |
. . . . . . 7
โข 0 โค
2 |
32 | | absid 15190 |
. . . . . . 7
โข ((2
โ โ โง 0 โค 2) โ (absโ2) = 2) |
33 | 13, 31, 32 | mp2an 691 |
. . . . . 6
โข
(absโ2) = 2 |
34 | 30, 33 | eqtri 2761 |
. . . . 5
โข
(absโ-2) = 2 |
35 | 34 | oveq2i 7372 |
. . . 4
โข
((absโ(ฮฃ๐ โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โ
(absโ-2)) = ((absโ(ฮฃ๐ โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โ
2) |
36 | | abs2dif 15226 |
. . . . 5
โข
(((ฮฃ๐ โ
(1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
โ โง -2 โ โ) โ ((absโ(ฮฃ๐ โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โ
(absโ-2)) โค (absโ((ฮฃ๐ โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
-2))) |
37 | 21, 26, 36 | sylancl 587 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((absโ(ฮฃ๐
โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โ
(absโ-2)) โค (absโ((ฮฃ๐ โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
-2))) |
38 | 35, 37 | eqbrtrrid 5145 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((absโ(ฮฃ๐
โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โ
2) โค (absโ((ฮฃ๐ โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
-2))) |
39 | | fveq2 6846 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ด โ (โโ๐ฅ) = (โโ๐ด)) |
40 | 39 | oveq2d 7377 |
. . . . . . . . . 10
โข (๐ฅ = ๐ด โ (1...(โโ๐ฅ)) = (1...(โโ๐ด))) |
41 | 40 | sumeq1d 15594 |
. . . . . . . . 9
โข (๐ฅ = ๐ด โ ฮฃ๐ โ (1...(โโ๐ฅ))((logโ๐)โ2) = ฮฃ๐ โ (1...(โโ๐ด))((logโ๐)โ2)) |
42 | | id 22 |
. . . . . . . . . 10
โข (๐ฅ = ๐ด โ ๐ฅ = ๐ด) |
43 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ด โ (logโ๐ฅ) = (logโ๐ด)) |
44 | 43 | oveq1d 7376 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ด โ ((logโ๐ฅ)โ2) = ((logโ๐ด)โ2)) |
45 | 43 | oveq2d 7377 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ด โ (2 ยท (logโ๐ฅ)) = (2 ยท
(logโ๐ด))) |
46 | 45 | oveq2d 7377 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ด โ (2 โ (2 ยท
(logโ๐ฅ))) = (2
โ (2 ยท (logโ๐ด)))) |
47 | 44, 46 | oveq12d 7379 |
. . . . . . . . . 10
โข (๐ฅ = ๐ด โ (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))) =
(((logโ๐ด)โ2) +
(2 โ (2 ยท (logโ๐ด))))) |
48 | 42, 47 | oveq12d 7379 |
. . . . . . . . 9
โข (๐ฅ = ๐ด โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))) = (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2
ยท (logโ๐ด)))))) |
49 | 41, 48 | oveq12d 7379 |
. . . . . . . 8
โข (๐ฅ = ๐ด โ (ฮฃ๐ โ (1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))) =
(ฮฃ๐ โ
(1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) |
50 | | eqid 2733 |
. . . . . . . 8
โข (๐ฅ โ โ+
โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))))) =
(๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))))) |
51 | | ovex 7394 |
. . . . . . . 8
โข
(ฮฃ๐ โ
(1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))) โ
V |
52 | 49, 50, 51 | fvmpt3i 6957 |
. . . . . . 7
โข (๐ด โ โ+
โ ((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))))โ๐ด) = (ฮฃ๐ โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) |
53 | 52 | adantr 482 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))))โ๐ด) = (ฮฃ๐ โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) |
54 | | 1rp 12927 |
. . . . . . 7
โข 1 โ
โ+ |
55 | | fveq2 6846 |
. . . . . . . . . . . . . 14
โข (๐ฅ = 1 โ (โโ๐ฅ) =
(โโ1)) |
56 | | 1z 12541 |
. . . . . . . . . . . . . . 15
โข 1 โ
โค |
57 | | flid 13722 |
. . . . . . . . . . . . . . 15
โข (1 โ
โค โ (โโ1) = 1) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . . . 14
โข
(โโ1) = 1 |
59 | 55, 58 | eqtrdi 2789 |
. . . . . . . . . . . . 13
โข (๐ฅ = 1 โ (โโ๐ฅ) = 1) |
60 | 59 | oveq2d 7377 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ
(1...(โโ๐ฅ)) =
(1...1)) |
61 | 60 | sumeq1d 15594 |
. . . . . . . . . . 11
โข (๐ฅ = 1 โ ฮฃ๐ โ
(1...(โโ๐ฅ))((logโ๐)โ2) = ฮฃ๐ โ (1...1)((logโ๐)โ2)) |
62 | | 0cn 11155 |
. . . . . . . . . . . 12
โข 0 โ
โ |
63 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
โข (๐ = 1 โ (logโ๐) =
(logโ1)) |
64 | | log1 25964 |
. . . . . . . . . . . . . . 15
โข
(logโ1) = 0 |
65 | 63, 64 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ (logโ๐) = 0) |
66 | 65 | sq0id 14107 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ ((logโ๐)โ2) = 0) |
67 | 66 | fsum1 15640 |
. . . . . . . . . . . 12
โข ((1
โ โค โง 0 โ โ) โ ฮฃ๐ โ (1...1)((logโ๐)โ2) = 0) |
68 | 56, 62, 67 | mp2an 691 |
. . . . . . . . . . 11
โข
ฮฃ๐ โ
(1...1)((logโ๐)โ2) = 0 |
69 | 61, 68 | eqtrdi 2789 |
. . . . . . . . . 10
โข (๐ฅ = 1 โ ฮฃ๐ โ
(1...(โโ๐ฅ))((logโ๐)โ2) = 0) |
70 | | id 22 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ ๐ฅ = 1) |
71 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = 1 โ (logโ๐ฅ) =
(logโ1)) |
72 | 71, 64 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = 1 โ (logโ๐ฅ) = 0) |
73 | 72 | sq0id 14107 |
. . . . . . . . . . . . . 14
โข (๐ฅ = 1 โ ((logโ๐ฅ)โ2) = 0) |
74 | 72 | oveq2d 7377 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = 1 โ (2 ยท
(logโ๐ฅ)) = (2
ยท 0)) |
75 | | 2t0e0 12330 |
. . . . . . . . . . . . . . . . 17
โข (2
ยท 0) = 0 |
76 | 74, 75 | eqtrdi 2789 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = 1 โ (2 ยท
(logโ๐ฅ)) =
0) |
77 | 76 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = 1 โ (2 โ (2
ยท (logโ๐ฅ))) =
(2 โ 0)) |
78 | 25 | subid1i 11481 |
. . . . . . . . . . . . . . 15
โข (2
โ 0) = 2 |
79 | 77, 78 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
โข (๐ฅ = 1 โ (2 โ (2
ยท (logโ๐ฅ))) =
2) |
80 | 73, 79 | oveq12d 7379 |
. . . . . . . . . . . . 13
โข (๐ฅ = 1 โ (((logโ๐ฅ)โ2) + (2 โ (2
ยท (logโ๐ฅ)))) =
(0 + 2)) |
81 | 25 | addid2i 11351 |
. . . . . . . . . . . . 13
โข (0 + 2) =
2 |
82 | 80, 81 | eqtrdi 2789 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ (((logโ๐ฅ)โ2) + (2 โ (2
ยท (logโ๐ฅ)))) =
2) |
83 | 70, 82 | oveq12d 7379 |
. . . . . . . . . . 11
โข (๐ฅ = 1 โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))) = (1
ยท 2)) |
84 | 25 | mulid2i 11168 |
. . . . . . . . . . 11
โข (1
ยท 2) = 2 |
85 | 83, 84 | eqtrdi 2789 |
. . . . . . . . . 10
โข (๐ฅ = 1 โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))) =
2) |
86 | 69, 85 | oveq12d 7379 |
. . . . . . . . 9
โข (๐ฅ = 1 โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))) = (0
โ 2)) |
87 | | df-neg 11396 |
. . . . . . . . 9
โข -2 = (0
โ 2) |
88 | 86, 87 | eqtr4di 2791 |
. . . . . . . 8
โข (๐ฅ = 1 โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))) =
-2) |
89 | 88, 50, 51 | fvmpt3i 6957 |
. . . . . . 7
โข (1 โ
โ+ โ ((๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))))โ1) = -2) |
90 | 54, 89 | mp1i 13 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))))โ1) = -2) |
91 | 53, 90 | oveq12d 7379 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))))โ๐ด) โ ((๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))))โ1)) = ((ฮฃ๐ โ
(1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
-2)) |
92 | 91 | fveq2d 6850 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(absโ(((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))))โ๐ด) โ ((๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))))โ1))) =
(absโ((ฮฃ๐
โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
-2))) |
93 | | ioorp 13351 |
. . . . . 6
โข
(0(,)+โ) = โ+ |
94 | 93 | eqcomi 2742 |
. . . . 5
โข
โ+ = (0(,)+โ) |
95 | | nnuz 12814 |
. . . . 5
โข โ =
(โคโฅโ1) |
96 | 56 | a1i 11 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โ โค) |
97 | | 1red 11164 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โ โ) |
98 | | pnfxr 11217 |
. . . . . 6
โข +โ
โ โ* |
99 | 98 | a1i 11 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
+โ โ โ*) |
100 | | 1re 11163 |
. . . . . . 7
โข 1 โ
โ |
101 | | 1nn0 12437 |
. . . . . . 7
โข 1 โ
โ0 |
102 | 100, 101 | nn0addge1i 12469 |
. . . . . 6
โข 1 โค (1
+ 1) |
103 | 102 | a1i 11 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โค (1 + 1)) |
104 | | 0red 11166 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 0
โ โ) |
105 | | rpre 12931 |
. . . . . . 7
โข (๐ฅ โ โ+
โ ๐ฅ โ
โ) |
106 | 105 | adantl 483 |
. . . . . 6
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ๐ฅ โ
โ) |
107 | | simpr 486 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ๐ฅ โ
โ+) |
108 | 107 | relogcld 26001 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (logโ๐ฅ) โ
โ) |
109 | 108 | resqcld 14039 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ((logโ๐ฅ)โ2) โ โ) |
110 | | remulcl 11144 |
. . . . . . . . 9
โข ((2
โ โ โง (logโ๐ฅ) โ โ) โ (2 ยท
(logโ๐ฅ)) โ
โ) |
111 | 13, 108, 110 | sylancr 588 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (2 ยท (logโ๐ฅ)) โ โ) |
112 | | resubcl 11473 |
. . . . . . . 8
โข ((2
โ โ โง (2 ยท (logโ๐ฅ)) โ โ) โ (2 โ (2
ยท (logโ๐ฅ)))
โ โ) |
113 | 13, 111, 112 | sylancr 588 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (2 โ (2 ยท (logโ๐ฅ))) โ โ) |
114 | 109, 113 | readdcld 11192 |
. . . . . 6
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))) โ
โ) |
115 | 106, 114 | remulcld 11193 |
. . . . 5
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (๐ฅ ยท
(((logโ๐ฅ)โ2) +
(2 โ (2 ยท (logโ๐ฅ))))) โ โ) |
116 | | nnrp 12934 |
. . . . . 6
โข (๐ฅ โ โ โ ๐ฅ โ
โ+) |
117 | 116, 109 | sylan2 594 |
. . . . 5
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ) โ
((logโ๐ฅ)โ2)
โ โ) |
118 | | reelprrecn 11151 |
. . . . . . . 8
โข โ
โ {โ, โ} |
119 | 118 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
โ โ {โ, โ}) |
120 | 106 | recnd 11191 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ๐ฅ โ
โ) |
121 | | 1red 11164 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ 1 โ โ) |
122 | | recn 11149 |
. . . . . . . . 9
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
123 | 122 | adantl 483 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ) โ ๐ฅ โ
โ) |
124 | | 1red 11164 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ) โ 1 โ
โ) |
125 | 119 | dvmptid 25344 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ โฆ ๐ฅ)) =
(๐ฅ โ โ โฆ
1)) |
126 | | rpssre 12930 |
. . . . . . . . 9
โข
โ+ โ โ |
127 | 126 | a1i 11 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
โ+ โ โ) |
128 | | eqid 2733 |
. . . . . . . . 9
โข
(TopOpenโโfld) =
(TopOpenโโfld) |
129 | 128 | tgioo2 24189 |
. . . . . . . 8
โข
(topGenโran (,)) = ((TopOpenโโfld)
โพt โ) |
130 | | iooretop 24152 |
. . . . . . . . . 10
โข
(0(,)+โ) โ (topGenโran (,)) |
131 | 93, 130 | eqeltrri 2831 |
. . . . . . . . 9
โข
โ+ โ (topGenโran (,)) |
132 | 131 | a1i 11 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
โ+ โ (topGenโran (,))) |
133 | 119, 123,
124, 125, 127, 129, 128, 132 | dvmptres 25350 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ+ โฆ ๐ฅ)) = (๐ฅ โ โ+ โฆ
1)) |
134 | 114 | recnd 11191 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))) โ
โ) |
135 | | resubcl 11473 |
. . . . . . . . 9
โข (((2
ยท (logโ๐ฅ))
โ โ โง 2 โ โ) โ ((2 ยท (logโ๐ฅ)) โ 2) โ
โ) |
136 | 111, 13, 135 | sylancl 587 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ((2 ยท (logโ๐ฅ)) โ 2) โ
โ) |
137 | 136, 107 | rerpdivcld 12996 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (((2 ยท (logโ๐ฅ)) โ 2) / ๐ฅ) โ โ) |
138 | 109 | recnd 11191 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ((logโ๐ฅ)โ2) โ โ) |
139 | 111 | recnd 11191 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (2 ยท (logโ๐ฅ)) โ โ) |
140 | 107 | rpreccld 12975 |
. . . . . . . . . . 11
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (1 / ๐ฅ) โ
โ+) |
141 | 140 | rpcnd 12967 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (1 / ๐ฅ) โ
โ) |
142 | 139, 141 | mulcld 11183 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ((2 ยท (logโ๐ฅ)) ยท (1 / ๐ฅ)) โ โ) |
143 | | cnelprrecn 11152 |
. . . . . . . . . . 11
โข โ
โ {โ, โ} |
144 | 143 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
โ โ {โ, โ}) |
145 | 108 | recnd 11191 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (logโ๐ฅ) โ
โ) |
146 | | sqcl 14032 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ (๐ฆโ2) โ
โ) |
147 | 146 | adantl 483 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฆ โ โ) โ (๐ฆโ2) โ
โ) |
148 | | simpr 486 |
. . . . . . . . . . 11
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฆ โ โ) โ ๐ฆ โ
โ) |
149 | | mulcl 11143 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐ฆ
โ โ) โ (2 ยท ๐ฆ) โ โ) |
150 | 25, 148, 149 | sylancr 588 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฆ โ โ) โ (2
ยท ๐ฆ) โ
โ) |
151 | | relogf1o 25945 |
. . . . . . . . . . . . . . 15
โข (log
โพ โ+):โ+โ1-1-ontoโโ |
152 | | f1of 6788 |
. . . . . . . . . . . . . . 15
โข ((log
โพ โ+):โ+โ1-1-ontoโโ โ (log โพ
โ+):โ+โถโ) |
153 | 151, 152 | mp1i 13 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ (log
โพ
โ+):โ+โถโ) |
154 | 153 | feqmptd 6914 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ (log
โพ โ+) = (๐ฅ โ โ+ โฆ ((log
โพ โ+)โ๐ฅ))) |
155 | | fvres 6865 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ+
โ ((log โพ โ+)โ๐ฅ) = (logโ๐ฅ)) |
156 | 155 | mpteq2ia 5212 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ+
โฆ ((log โพ โ+)โ๐ฅ)) = (๐ฅ โ โ+ โฆ
(logโ๐ฅ)) |
157 | 154, 156 | eqtrdi 2789 |
. . . . . . . . . . . 12
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ (log
โพ โ+) = (๐ฅ โ โ+ โฆ
(logโ๐ฅ))) |
158 | 157 | oveq2d 7377 |
. . . . . . . . . . 11
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (log โพ โ+)) = (โ D (๐ฅ โ โ+ โฆ
(logโ๐ฅ)))) |
159 | | dvrelog 26015 |
. . . . . . . . . . 11
โข (โ
D (log โพ โ+)) = (๐ฅ โ โ+ โฆ (1 /
๐ฅ)) |
160 | 158, 159 | eqtr3di 2788 |
. . . . . . . . . 10
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ+ โฆ (logโ๐ฅ))) = (๐ฅ โ โ+ โฆ (1 /
๐ฅ))) |
161 | | 2nn 12234 |
. . . . . . . . . . . 12
โข 2 โ
โ |
162 | | dvexp 25340 |
. . . . . . . . . . . 12
โข (2 โ
โ โ (โ D (๐ฆ โ โ โฆ (๐ฆโ2))) = (๐ฆ โ โ โฆ (2 ยท (๐ฆโ(2 โ
1))))) |
163 | 161, 162 | mp1i 13 |
. . . . . . . . . . 11
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฆ โ
โ โฆ (๐ฆโ2))) = (๐ฆ โ โ โฆ (2 ยท (๐ฆโ(2 โ
1))))) |
164 | | 2m1e1 12287 |
. . . . . . . . . . . . . . 15
โข (2
โ 1) = 1 |
165 | 164 | oveq2i 7372 |
. . . . . . . . . . . . . 14
โข (๐ฆโ(2 โ 1)) = (๐ฆโ1) |
166 | | exp1 13982 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (๐ฆโ1) = ๐ฆ) |
167 | 165, 166 | eqtrid 2785 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ (๐ฆโ(2 โ 1)) = ๐ฆ) |
168 | 167 | oveq2d 7377 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ (2
ยท (๐ฆโ(2 โ
1))) = (2 ยท ๐ฆ)) |
169 | 168 | mpteq2ia 5212 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โฆ (2
ยท (๐ฆโ(2 โ
1)))) = (๐ฆ โ โ
โฆ (2 ยท ๐ฆ)) |
170 | 163, 169 | eqtrdi 2789 |
. . . . . . . . . 10
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฆ โ
โ โฆ (๐ฆโ2))) = (๐ฆ โ โ โฆ (2 ยท ๐ฆ))) |
171 | | oveq1 7368 |
. . . . . . . . . 10
โข (๐ฆ = (logโ๐ฅ) โ (๐ฆโ2) = ((logโ๐ฅ)โ2)) |
172 | | oveq2 7369 |
. . . . . . . . . 10
โข (๐ฆ = (logโ๐ฅ) โ (2 ยท ๐ฆ) = (2 ยท (logโ๐ฅ))) |
173 | 119, 144,
145, 140, 147, 150, 160, 170, 171, 172 | dvmptco 25359 |
. . . . . . . . 9
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ+ โฆ ((logโ๐ฅ)โ2))) = (๐ฅ โ โ+ โฆ ((2
ยท (logโ๐ฅ))
ยท (1 / ๐ฅ)))) |
174 | 113 | recnd 11191 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (2 โ (2 ยท (logโ๐ฅ))) โ โ) |
175 | | ovexd 7396 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (0 โ (2 ยท (1 / ๐ฅ))) โ V) |
176 | | 2cnd 12239 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ 2 โ โ) |
177 | | 0red 11166 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ 0 โ โ) |
178 | | 2cnd 12239 |
. . . . . . . . . . 11
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ) โ 2 โ
โ) |
179 | | 0red 11166 |
. . . . . . . . . . 11
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ) โ 0 โ
โ) |
180 | | 2cnd 12239 |
. . . . . . . . . . . 12
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 2
โ โ) |
181 | 119, 180 | dvmptc 25345 |
. . . . . . . . . . 11
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ โฆ 2)) = (๐ฅ
โ โ โฆ 0)) |
182 | 119, 178,
179, 181, 127, 129, 128, 132 | dvmptres 25350 |
. . . . . . . . . 10
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ+ โฆ 2)) = (๐ฅ โ โ+ โฆ
0)) |
183 | | mulcl 11143 |
. . . . . . . . . . 11
โข ((2
โ โ โง (1 / ๐ฅ) โ โ) โ (2 ยท (1 /
๐ฅ)) โ
โ) |
184 | 25, 141, 183 | sylancr 588 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (2 ยท (1 / ๐ฅ))
โ โ) |
185 | 119, 145,
140, 160, 180 | dvmptcmul 25351 |
. . . . . . . . . 10
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ+ โฆ (2 ยท (logโ๐ฅ)))) = (๐ฅ โ โ+ โฆ (2
ยท (1 / ๐ฅ)))) |
186 | 119, 176,
177, 182, 139, 184, 185 | dvmptsub 25354 |
. . . . . . . . 9
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ+ โฆ (2 โ (2 ยท (logโ๐ฅ))))) = (๐ฅ โ โ+ โฆ (0
โ (2 ยท (1 / ๐ฅ))))) |
187 | 119, 138,
142, 173, 174, 175, 186 | dvmptadd 25347 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ+ โฆ (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))) = (๐ฅ โ โ+
โฆ (((2 ยท (logโ๐ฅ)) ยท (1 / ๐ฅ)) + (0 โ (2 ยท (1 / ๐ฅ)))))) |
188 | 139, 176,
141 | subdird 11620 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (((2 ยท (logโ๐ฅ)) โ 2) ยท (1 / ๐ฅ)) = (((2 ยท
(logโ๐ฅ)) ยท (1
/ ๐ฅ)) โ (2 ยท
(1 / ๐ฅ)))) |
189 | 136 | recnd 11191 |
. . . . . . . . . . 11
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ((2 ยท (logโ๐ฅ)) โ 2) โ
โ) |
190 | | rpne0 12939 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ+
โ ๐ฅ โ
0) |
191 | 190 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ๐ฅ โ
0) |
192 | 189, 120,
191 | divrecd 11942 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (((2 ยท (logโ๐ฅ)) โ 2) / ๐ฅ) = (((2 ยท (logโ๐ฅ)) โ 2) ยท (1 /
๐ฅ))) |
193 | | df-neg 11396 |
. . . . . . . . . . . 12
โข -(2
ยท (1 / ๐ฅ)) = (0
โ (2 ยท (1 / ๐ฅ))) |
194 | 193 | oveq2i 7372 |
. . . . . . . . . . 11
โข (((2
ยท (logโ๐ฅ))
ยท (1 / ๐ฅ)) + -(2
ยท (1 / ๐ฅ))) = (((2
ยท (logโ๐ฅ))
ยท (1 / ๐ฅ)) + (0
โ (2 ยท (1 / ๐ฅ)))) |
195 | 142, 184 | negsubd 11526 |
. . . . . . . . . . 11
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (((2 ยท (logโ๐ฅ)) ยท (1 / ๐ฅ)) + -(2 ยท (1 / ๐ฅ))) = (((2 ยท (logโ๐ฅ)) ยท (1 / ๐ฅ)) โ (2 ยท (1 /
๐ฅ)))) |
196 | 194, 195 | eqtr3id 2787 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (((2 ยท (logโ๐ฅ)) ยท (1 / ๐ฅ)) + (0 โ (2 ยท (1 / ๐ฅ)))) = (((2 ยท
(logโ๐ฅ)) ยท (1
/ ๐ฅ)) โ (2 ยท
(1 / ๐ฅ)))) |
197 | 188, 192,
196 | 3eqtr4rd 2784 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (((2 ยท (logโ๐ฅ)) ยท (1 / ๐ฅ)) + (0 โ (2 ยท (1 / ๐ฅ)))) = (((2 ยท
(logโ๐ฅ)) โ 2) /
๐ฅ)) |
198 | 197 | mpteq2dva 5209 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(๐ฅ โ
โ+ โฆ (((2 ยท (logโ๐ฅ)) ยท (1 / ๐ฅ)) + (0 โ (2 ยท (1 / ๐ฅ))))) = (๐ฅ โ โ+ โฆ (((2
ยท (logโ๐ฅ))
โ 2) / ๐ฅ))) |
199 | 187, 198 | eqtrd 2773 |
. . . . . . 7
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ+ โฆ (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))) = (๐ฅ โ โ+
โฆ (((2 ยท (logโ๐ฅ)) โ 2) / ๐ฅ))) |
200 | 119, 120,
121, 133, 134, 137, 199 | dvmptmul 25348 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ+ โฆ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))))) =
(๐ฅ โ
โ+ โฆ ((1 ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))) + ((((2
ยท (logโ๐ฅ))
โ 2) / ๐ฅ) ยท
๐ฅ)))) |
201 | 134 | mulid2d 11181 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (1 ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))) =
(((logโ๐ฅ)โ2) +
(2 โ (2 ยท (logโ๐ฅ))))) |
202 | 138, 139,
176 | subsub2d 11549 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (((logโ๐ฅ)โ2) โ ((2 ยท
(logโ๐ฅ)) โ 2))
= (((logโ๐ฅ)โ2) +
(2 โ (2 ยท (logโ๐ฅ))))) |
203 | 201, 202 | eqtr4d 2776 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ (1 ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))) =
(((logโ๐ฅ)โ2)
โ ((2 ยท (logโ๐ฅ)) โ 2))) |
204 | 189, 120,
191 | divcan1d 11940 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ((((2 ยท (logโ๐ฅ)) โ 2) / ๐ฅ) ยท ๐ฅ) = ((2 ยท (logโ๐ฅ)) โ 2)) |
205 | 203, 204 | oveq12d 7379 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ((1 ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))) + ((((2
ยท (logโ๐ฅ))
โ 2) / ๐ฅ) ยท
๐ฅ)) = ((((logโ๐ฅ)โ2) โ ((2 ยท
(logโ๐ฅ)) โ 2))
+ ((2 ยท (logโ๐ฅ)) โ 2))) |
206 | 138, 189 | npcand 11524 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ((((logโ๐ฅ)โ2) โ ((2 ยท
(logโ๐ฅ)) โ 2))
+ ((2 ยท (logโ๐ฅ)) โ 2)) = ((logโ๐ฅ)โ2)) |
207 | 205, 206 | eqtrd 2773 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง ๐ฅ โ โ+)
โ ((1 ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))) + ((((2
ยท (logโ๐ฅ))
โ 2) / ๐ฅ) ยท
๐ฅ)) = ((logโ๐ฅ)โ2)) |
208 | 207 | mpteq2dva 5209 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(๐ฅ โ
โ+ โฆ ((1 ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))) + ((((2
ยท (logโ๐ฅ))
โ 2) / ๐ฅ) ยท
๐ฅ))) = (๐ฅ โ โ+ โฆ
((logโ๐ฅ)โ2))) |
209 | 200, 208 | eqtrd 2773 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(โ D (๐ฅ โ
โ+ โฆ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ))))))) =
(๐ฅ โ
โ+ โฆ ((logโ๐ฅ)โ2))) |
210 | | fveq2 6846 |
. . . . . 6
โข (๐ฅ = ๐ โ (logโ๐ฅ) = (logโ๐)) |
211 | 210 | oveq1d 7376 |
. . . . 5
โข (๐ฅ = ๐ โ ((logโ๐ฅ)โ2) = ((logโ๐)โ2)) |
212 | | simp32 1211 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ ๐ฅ โค ๐) |
213 | | simp2l 1200 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ ๐ฅ โ โ+) |
214 | | simp2r 1201 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ ๐ โ โ+) |
215 | 213, 214 | logled 26005 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ (๐ฅ โค ๐ โ (logโ๐ฅ) โค (logโ๐))) |
216 | 212, 215 | mpbid 231 |
. . . . . 6
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ (logโ๐ฅ) โค (logโ๐)) |
217 | 213 | relogcld 26001 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ (logโ๐ฅ) โ
โ) |
218 | 214 | relogcld 26001 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ (logโ๐) โ
โ) |
219 | | simp31 1210 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ 1 โค ๐ฅ) |
220 | | logleb 25981 |
. . . . . . . . . 10
โข ((1
โ โ+ โง ๐ฅ โ โ+) โ (1 โค
๐ฅ โ (logโ1) โค
(logโ๐ฅ))) |
221 | 54, 213, 220 | sylancr 588 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ (1 โค ๐ฅ โ (logโ1) โค
(logโ๐ฅ))) |
222 | 219, 221 | mpbid 231 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ (logโ1) โค
(logโ๐ฅ)) |
223 | 64, 222 | eqbrtrrid 5145 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ 0 โค
(logโ๐ฅ)) |
224 | 214 | rpred 12965 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ ๐ โ โ) |
225 | | 1red 11164 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ 1 โ
โ) |
226 | 213 | rpred 12965 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ ๐ฅ โ โ) |
227 | 225, 226,
224, 219, 212 | letrd 11320 |
. . . . . . . 8
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ 1 โค ๐) |
228 | 224, 227 | logge0d 26008 |
. . . . . . 7
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ 0 โค
(logโ๐)) |
229 | 217, 218,
223, 228 | le2sqd 14169 |
. . . . . 6
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ ((logโ๐ฅ) โค (logโ๐) โ ((logโ๐ฅ)โ2) โค ((logโ๐)โ2))) |
230 | 216, 229 | mpbid 231 |
. . . . 5
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง ๐
โ โ+) โง (1 โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค +โ)) โ ((logโ๐ฅ)โ2) โค ((logโ๐)โ2)) |
231 | | relogcl 25954 |
. . . . . . 7
โข (๐ฅ โ โ+
โ (logโ๐ฅ) โ
โ) |
232 | 231 | ad2antrl 727 |
. . . . . 6
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง 1 โค ๐ฅ)) โ (logโ๐ฅ) โ โ) |
233 | 232 | sqge0d 14051 |
. . . . 5
โข (((๐ด โ โ+
โง 1 โค ๐ด) โง
(๐ฅ โ
โ+ โง 1 โค ๐ฅ)) โ 0 โค ((logโ๐ฅ)โ2)) |
234 | 54 | a1i 11 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โ โ+) |
235 | | simpl 484 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
๐ด โ
โ+) |
236 | | 1le1 11791 |
. . . . . 6
โข 1 โค
1 |
237 | 236 | a1i 11 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โค 1) |
238 | | simpr 486 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 1
โค ๐ด) |
239 | 9 | rexrd 11213 |
. . . . . 6
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
๐ด โ
โ*) |
240 | | pnfge 13059 |
. . . . . 6
โข (๐ด โ โ*
โ ๐ด โค
+โ) |
241 | 239, 240 | syl 17 |
. . . . 5
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
๐ด โค
+โ) |
242 | 94, 95, 96, 97, 99, 103, 104, 115, 109, 117, 209, 211, 230, 50, 233, 234, 235, 237, 238, 241, 44 | dvfsum2 25421 |
. . . 4
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(absโ(((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))))โ๐ด) โ ((๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))((logโ๐)โ2) โ (๐ฅ ยท (((logโ๐ฅ)โ2) + (2 โ (2 ยท
(logโ๐ฅ)))))))โ1))) โค ((logโ๐ด)โ2)) |
243 | 92, 242 | eqbrtrrd 5133 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(absโ((ฮฃ๐
โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด)))))) โ
-2)) โค ((logโ๐ด)โ2)) |
244 | 24, 29, 12, 38, 243 | letrd 11320 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
((absโ(ฮฃ๐
โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โ
2) โค ((logโ๐ด)โ2)) |
245 | 13 | a1i 11 |
. . 3
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ 2
โ โ) |
246 | 22, 245, 12 | lesubaddd 11760 |
. 2
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(((absโ(ฮฃ๐
โ (1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โ
2) โค ((logโ๐ด)โ2) โ (absโ(ฮฃ๐ โ
(1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โค
(((logโ๐ด)โ2) +
2))) |
247 | 244, 246 | mpbid 231 |
1
โข ((๐ด โ โ+
โง 1 โค ๐ด) โ
(absโ(ฮฃ๐ โ
(1...(โโ๐ด))((logโ๐)โ2) โ (๐ด ยท (((logโ๐ด)โ2) + (2 โ (2 ยท
(logโ๐ด))))))) โค
(((logโ๐ด)โ2) +
2)) |