Step | Hyp | Ref
| Expression |
1 | | flid 13720 |
. . . . 5
โข (๐ด โ โค โ
(โโ๐ด) = ๐ด) |
2 | 1 | oveq2d 7378 |
. . . 4
โข (๐ด โ โค โ
(1...(โโ๐ด)) =
(1...๐ด)) |
3 | 2 | sumeq1d 15593 |
. . 3
โข (๐ด โ โค โ
ฮฃ๐ โ
(1...(โโ๐ด))(((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) / ๐) = ฮฃ๐ โ (1...๐ด)(((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) / ๐)) |
4 | | fveq2 6847 |
. . . . . 6
โข (๐ = (๐โ๐) โ (ฮโ๐) = (ฮโ(๐โ๐))) |
5 | | eleq1 2826 |
. . . . . . 7
โข (๐ = (๐โ๐) โ (๐ โ โ โ (๐โ๐) โ โ)) |
6 | | fveq2 6847 |
. . . . . . 7
โข (๐ = (๐โ๐) โ (logโ๐) = (logโ(๐โ๐))) |
7 | 5, 6 | ifbieq1d 4515 |
. . . . . 6
โข (๐ = (๐โ๐) โ if(๐ โ โ, (logโ๐), 0) = if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) |
8 | 4, 7 | oveq12d 7380 |
. . . . 5
โข (๐ = (๐โ๐) โ ((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) = ((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0))) |
9 | | id 22 |
. . . . 5
โข (๐ = (๐โ๐) โ ๐ = (๐โ๐)) |
10 | 8, 9 | oveq12d 7380 |
. . . 4
โข (๐ = (๐โ๐) โ (((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) / ๐) = (((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐))) |
11 | | zre 12510 |
. . . 4
โข (๐ด โ โค โ ๐ด โ
โ) |
12 | | elfznn 13477 |
. . . . . . . . 9
โข (๐ โ
(1...(โโ๐ด))
โ ๐ โ
โ) |
13 | 12 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ
(1...(โโ๐ด)))
โ ๐ โ
โ) |
14 | | vmacl 26483 |
. . . . . . . 8
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
15 | 13, 14 | syl 17 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ
(1...(โโ๐ด)))
โ (ฮโ๐)
โ โ) |
16 | 13 | nnrpd 12962 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ
(1...(โโ๐ด)))
โ ๐ โ
โ+) |
17 | 16 | relogcld 25994 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ
(1...(โโ๐ด)))
โ (logโ๐) โ
โ) |
18 | | 0re 11164 |
. . . . . . . 8
โข 0 โ
โ |
19 | | ifcl 4536 |
. . . . . . . 8
โข
(((logโ๐)
โ โ โง 0 โ โ) โ if(๐ โ โ, (logโ๐), 0) โ
โ) |
20 | 17, 18, 19 | sylancl 587 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ
(1...(โโ๐ด)))
โ if(๐ โ โ,
(logโ๐), 0) โ
โ) |
21 | 15, 20 | resubcld 11590 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ
(1...(โโ๐ด)))
โ ((ฮโ๐)
โ if(๐ โ
โ, (logโ๐), 0))
โ โ) |
22 | 21, 13 | nndivred 12214 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ
(1...(โโ๐ด)))
โ (((ฮโ๐)
โ if(๐ โ
โ, (logโ๐), 0))
/ ๐) โ
โ) |
23 | 22 | recnd 11190 |
. . . 4
โข ((๐ด โ โค โง ๐ โ
(1...(โโ๐ด)))
โ (((ฮโ๐)
โ if(๐ โ
โ, (logโ๐), 0))
/ ๐) โ
โ) |
24 | | simprr 772 |
. . . . . . . 8
โข ((๐ด โ โค โง (๐ โ
(1...(โโ๐ด))
โง (ฮโ๐) =
0)) โ (ฮโ๐) = 0) |
25 | | vmaprm 26482 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(ฮโ๐) =
(logโ๐)) |
26 | | prmnn 16557 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ) |
27 | 26 | nnred 12175 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ) |
28 | | prmgt1 16580 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ 1 <
๐) |
29 | 27, 28 | rplogcld 26000 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(logโ๐) โ
โ+) |
30 | 25, 29 | eqeltrd 2838 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
(ฮโ๐) โ
โ+) |
31 | 30 | rpne0d 12969 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(ฮโ๐) โ
0) |
32 | 31 | necon2bi 2975 |
. . . . . . . . . 10
โข
((ฮโ๐)
= 0 โ ยฌ ๐ โ
โ) |
33 | 32 | ad2antll 728 |
. . . . . . . . 9
โข ((๐ด โ โค โง (๐ โ
(1...(โโ๐ด))
โง (ฮโ๐) =
0)) โ ยฌ ๐ โ
โ) |
34 | 33 | iffalsed 4502 |
. . . . . . . 8
โข ((๐ด โ โค โง (๐ โ
(1...(โโ๐ด))
โง (ฮโ๐) =
0)) โ if(๐ โ
โ, (logโ๐), 0)
= 0) |
35 | 24, 34 | oveq12d 7380 |
. . . . . . 7
โข ((๐ด โ โค โง (๐ โ
(1...(โโ๐ด))
โง (ฮโ๐) =
0)) โ ((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) = (0 โ
0)) |
36 | | 0m0e0 12280 |
. . . . . . 7
โข (0
โ 0) = 0 |
37 | 35, 36 | eqtrdi 2793 |
. . . . . 6
โข ((๐ด โ โค โง (๐ โ
(1...(โโ๐ด))
โง (ฮโ๐) =
0)) โ ((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) = 0) |
38 | 37 | oveq1d 7377 |
. . . . 5
โข ((๐ด โ โค โง (๐ โ
(1...(โโ๐ด))
โง (ฮโ๐) =
0)) โ (((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) / ๐) = (0 / ๐)) |
39 | 12 | ad2antrl 727 |
. . . . . . . 8
โข ((๐ด โ โค โง (๐ โ
(1...(โโ๐ด))
โง (ฮโ๐) =
0)) โ ๐ โ
โ) |
40 | 39 | nnrpd 12962 |
. . . . . . 7
โข ((๐ด โ โค โง (๐ โ
(1...(โโ๐ด))
โง (ฮโ๐) =
0)) โ ๐ โ
โ+) |
41 | 40 | rpcnne0d 12973 |
. . . . . 6
โข ((๐ด โ โค โง (๐ โ
(1...(โโ๐ด))
โง (ฮโ๐) =
0)) โ (๐ โ
โ โง ๐ โ
0)) |
42 | | div0 11850 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ 0) โ (0 / ๐) = 0) |
43 | 41, 42 | syl 17 |
. . . . 5
โข ((๐ด โ โค โง (๐ โ
(1...(โโ๐ด))
โง (ฮโ๐) =
0)) โ (0 / ๐) =
0) |
44 | 38, 43 | eqtrd 2777 |
. . . 4
โข ((๐ด โ โค โง (๐ โ
(1...(โโ๐ด))
โง (ฮโ๐) =
0)) โ (((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) / ๐) = 0) |
45 | 10, 11, 23, 44 | fsumvma2 26578 |
. . 3
โข (๐ด โ โค โ
ฮฃ๐ โ
(1...(โโ๐ด))(((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) / ๐) = ฮฃ๐ โ ((0[,]๐ด) โฉ โ)ฮฃ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐))) |
46 | 3, 45 | eqtr3d 2779 |
. 2
โข (๐ด โ โค โ
ฮฃ๐ โ (1...๐ด)(((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) / ๐) = ฮฃ๐ โ ((0[,]๐ด) โฉ โ)ฮฃ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐))) |
47 | | fzfid 13885 |
. . . . 5
โข (๐ด โ โค โ
(2...((absโ๐ด) + 1))
โ Fin) |
48 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ โ ((0[,]๐ด) โฉ โ)) |
49 | 48 | elin2d 4164 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ โ โ) |
50 | | prmnn 16557 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ โ โ) |
52 | 51 | nnred 12175 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ โ โ) |
53 | 11 | adantr 482 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ด โ โ) |
54 | | zcn 12511 |
. . . . . . . . . . . 12
โข (๐ด โ โค โ ๐ด โ
โ) |
55 | 54 | abscld 15328 |
. . . . . . . . . . 11
โข (๐ด โ โค โ
(absโ๐ด) โ
โ) |
56 | | peano2re 11335 |
. . . . . . . . . . 11
โข
((absโ๐ด)
โ โ โ ((absโ๐ด) + 1) โ โ) |
57 | 55, 56 | syl 17 |
. . . . . . . . . 10
โข (๐ด โ โค โ
((absโ๐ด) + 1) โ
โ) |
58 | 57 | adantr 482 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((absโ๐ด) + 1) โ
โ) |
59 | | elinel1 4160 |
. . . . . . . . . . . 12
โข (๐ โ ((0[,]๐ด) โฉ โ) โ ๐ โ (0[,]๐ด)) |
60 | | elicc2 13336 |
. . . . . . . . . . . . 13
โข ((0
โ โ โง ๐ด
โ โ) โ (๐
โ (0[,]๐ด) โ
(๐ โ โ โง 0
โค ๐ โง ๐ โค ๐ด))) |
61 | 18, 11, 60 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ด โ โค โ (๐ โ (0[,]๐ด) โ (๐ โ โ โง 0 โค ๐ โง ๐ โค ๐ด))) |
62 | 59, 61 | imbitrid 243 |
. . . . . . . . . . 11
โข (๐ด โ โค โ (๐ โ ((0[,]๐ด) โฉ โ) โ (๐ โ โ โง 0 โค ๐ โง ๐ โค ๐ด))) |
63 | 62 | imp 408 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (๐ โ โ โง 0 โค ๐ โง ๐ โค ๐ด)) |
64 | 63 | simp3d 1145 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ โค ๐ด) |
65 | 54 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ด โ โ) |
66 | 65 | abscld 15328 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (absโ๐ด) โ
โ) |
67 | 53 | leabsd 15306 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ด โค (absโ๐ด)) |
68 | 66 | lep1d 12093 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (absโ๐ด) โค ((absโ๐ด) + 1)) |
69 | 53, 66, 58, 67, 68 | letrd 11319 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ด โค ((absโ๐ด) + 1)) |
70 | 52, 53, 58, 64, 69 | letrd 11319 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ โค ((absโ๐ด) + 1)) |
71 | | prmuz2 16579 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
72 | 49, 71 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ โ
(โคโฅโ2)) |
73 | | nn0abscl 15204 |
. . . . . . . . . . . 12
โข (๐ด โ โค โ
(absโ๐ด) โ
โ0) |
74 | | nn0p1nn 12459 |
. . . . . . . . . . . 12
โข
((absโ๐ด)
โ โ0 โ ((absโ๐ด) + 1) โ โ) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . 11
โข (๐ด โ โค โ
((absโ๐ด) + 1) โ
โ) |
76 | 75 | nnzd 12533 |
. . . . . . . . . 10
โข (๐ด โ โค โ
((absโ๐ด) + 1) โ
โค) |
77 | 76 | adantr 482 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((absโ๐ด) + 1) โ
โค) |
78 | | elfz5 13440 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ2) โง ((absโ๐ด) + 1) โ โค) โ (๐ โ (2...((absโ๐ด) + 1)) โ ๐ โค ((absโ๐ด) + 1))) |
79 | 72, 77, 78 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (๐ โ (2...((absโ๐ด) + 1)) โ ๐ โค ((absโ๐ด) + 1))) |
80 | 70, 79 | mpbird 257 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ โ (2...((absโ๐ด) + 1))) |
81 | 80 | ex 414 |
. . . . . 6
โข (๐ด โ โค โ (๐ โ ((0[,]๐ด) โฉ โ) โ ๐ โ (2...((absโ๐ด) + 1)))) |
82 | 81 | ssrdv 3955 |
. . . . 5
โข (๐ด โ โค โ
((0[,]๐ด) โฉ โ)
โ (2...((absโ๐ด)
+ 1))) |
83 | 47, 82 | ssfid 9218 |
. . . 4
โข (๐ด โ โค โ
((0[,]๐ด) โฉ โ)
โ Fin) |
84 | | fzfid 13885 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
(1...(โโ((logโ๐ด) / (logโ๐)))) โ Fin) |
85 | | simprl 770 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ ๐ โ ((0[,]๐ด) โฉ โ)) |
86 | 85 | elin2d 4164 |
. . . . . . . . . 10
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ ๐ โ โ) |
87 | | elfznn 13477 |
. . . . . . . . . . 11
โข (๐ โ
(1...(โโ((logโ๐ด) / (logโ๐)))) โ ๐ โ โ) |
88 | 87 | ad2antll 728 |
. . . . . . . . . 10
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ ๐ โ โ) |
89 | | vmappw 26481 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ
(ฮโ(๐โ๐)) = (logโ๐)) |
90 | 86, 88, 89 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ
(ฮโ(๐โ๐)) = (logโ๐)) |
91 | 51 | adantrr 716 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ ๐ โ โ) |
92 | 91 | nnrpd 12962 |
. . . . . . . . . 10
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ ๐ โ โ+) |
93 | 92 | relogcld 25994 |
. . . . . . . . 9
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ (logโ๐) โ
โ) |
94 | 90, 93 | eqeltrd 2838 |
. . . . . . . 8
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ
(ฮโ(๐โ๐)) โ โ) |
95 | 88 | nnnn0d 12480 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ ๐ โ โ0) |
96 | | nnexpcl 13987 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
97 | 91, 95, 96 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ (๐โ๐) โ โ) |
98 | 97 | nnrpd 12962 |
. . . . . . . . . 10
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ (๐โ๐) โ
โ+) |
99 | 98 | relogcld 25994 |
. . . . . . . . 9
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ (logโ(๐โ๐)) โ โ) |
100 | | ifcl 4536 |
. . . . . . . . 9
โข
(((logโ(๐โ๐)) โ โ โง 0 โ โ)
โ if((๐โ๐) โ โ,
(logโ(๐โ๐)), 0) โ
โ) |
101 | 99, 18, 100 | sylancl 587 |
. . . . . . . 8
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0) โ โ) |
102 | 94, 101 | resubcld 11590 |
. . . . . . 7
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ
((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) โ โ) |
103 | 102, 97 | nndivred 12214 |
. . . . . 6
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ
(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) โ โ) |
104 | 103 | anassrs 469 |
. . . . 5
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))) โ
(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) โ โ) |
105 | 84, 104 | fsumrecl 15626 |
. . . 4
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ
(1...(โโ((logโ๐ด) / (logโ๐))))(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) โ โ) |
106 | 83, 105 | fsumrecl 15626 |
. . 3
โข (๐ด โ โค โ
ฮฃ๐ โ ((0[,]๐ด) โฉ โ)ฮฃ๐ โ
(1...(โโ((logโ๐ด) / (logโ๐))))(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) โ โ) |
107 | 51 | nnrpd 12962 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ โ โ+) |
108 | 107 | relogcld 25994 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (logโ๐) โ
โ) |
109 | | uz2m1nn 12855 |
. . . . . . 7
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
110 | 72, 109 | syl 17 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (๐ โ 1) โ โ) |
111 | 51, 110 | nnmulcld 12213 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (๐ ยท (๐ โ 1)) โ โ) |
112 | 108, 111 | nndivred 12214 |
. . . 4
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((logโ๐) / (๐ ยท (๐ โ 1))) โ
โ) |
113 | 83, 112 | fsumrecl 15626 |
. . 3
โข (๐ด โ โค โ
ฮฃ๐ โ ((0[,]๐ด) โฉ
โ)((logโ๐) /
(๐ ยท (๐ โ 1))) โ
โ) |
114 | | 2re 12234 |
. . . 4
โข 2 โ
โ |
115 | 114 | a1i 11 |
. . 3
โข (๐ด โ โค โ 2 โ
โ) |
116 | 18 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ 0 โ
โ) |
117 | 51 | nngt0d 12209 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ 0 < ๐) |
118 | 116, 52, 53, 117, 64 | ltletrd 11322 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ 0 < ๐ด) |
119 | 53, 118 | elrpd 12961 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ด โ
โ+) |
120 | 119 | relogcld 25994 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (logโ๐ด) โ
โ) |
121 | | prmgt1 16580 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 1 <
๐) |
122 | 49, 121 | syl 17 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ 1 < ๐) |
123 | 52, 122 | rplogcld 26000 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (logโ๐) โ
โ+) |
124 | 120, 123 | rerpdivcld 12995 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((logโ๐ด) / (logโ๐)) โ
โ) |
125 | 123 | rpcnd 12966 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (logโ๐) โ
โ) |
126 | 125 | mulid2d 11180 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (1 ยท
(logโ๐)) =
(logโ๐)) |
127 | 107, 119 | logled 25998 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (๐ โค ๐ด โ (logโ๐) โค (logโ๐ด))) |
128 | 64, 127 | mpbid 231 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (logโ๐) โค (logโ๐ด)) |
129 | 126, 128 | eqbrtrd 5132 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (1 ยท
(logโ๐)) โค
(logโ๐ด)) |
130 | | 1re 11162 |
. . . . . . . . . . . 12
โข 1 โ
โ |
131 | 130 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ 1 โ
โ) |
132 | 131, 120,
123 | lemuldivd 13013 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((1 ยท
(logโ๐)) โค
(logโ๐ด) โ 1 โค
((logโ๐ด) /
(logโ๐)))) |
133 | 129, 132 | mpbid 231 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ 1 โค
((logโ๐ด) /
(logโ๐))) |
134 | | flge1nn 13733 |
. . . . . . . . 9
โข
((((logโ๐ด) /
(logโ๐)) โ
โ โง 1 โค ((logโ๐ด) / (logโ๐))) โ (โโ((logโ๐ด) / (logโ๐))) โ
โ) |
135 | 124, 133,
134 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
(โโ((logโ๐ด) / (logโ๐))) โ โ) |
136 | | nnuz 12813 |
. . . . . . . 8
โข โ =
(โคโฅโ1) |
137 | 135, 136 | eleqtrdi 2848 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
(โโ((logโ๐ด) / (logโ๐))) โ
(โคโฅโ1)) |
138 | 103 | recnd 11190 |
. . . . . . . 8
โข ((๐ด โ โค โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ
(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) โ โ) |
139 | 138 | anassrs 469 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))) โ
(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) โ โ) |
140 | | oveq2 7370 |
. . . . . . . . . 10
โข (๐ = 1 โ (๐โ๐) = (๐โ1)) |
141 | 140 | fveq2d 6851 |
. . . . . . . . 9
โข (๐ = 1 โ
(ฮโ(๐โ๐)) = (ฮโ(๐โ1))) |
142 | 140 | eleq1d 2823 |
. . . . . . . . . 10
โข (๐ = 1 โ ((๐โ๐) โ โ โ (๐โ1) โ โ)) |
143 | 140 | fveq2d 6851 |
. . . . . . . . . 10
โข (๐ = 1 โ (logโ(๐โ๐)) = (logโ(๐โ1))) |
144 | 142, 143 | ifbieq1d 4515 |
. . . . . . . . 9
โข (๐ = 1 โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0) = if((๐โ1) โ โ, (logโ(๐โ1)), 0)) |
145 | 141, 144 | oveq12d 7380 |
. . . . . . . 8
โข (๐ = 1 โ
((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) = ((ฮโ(๐โ1)) โ if((๐โ1) โ โ,
(logโ(๐โ1)),
0))) |
146 | 145, 140 | oveq12d 7380 |
. . . . . . 7
โข (๐ = 1 โ
(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) = (((ฮโ(๐โ1)) โ if((๐โ1) โ โ, (logโ(๐โ1)), 0)) / (๐โ1))) |
147 | 137, 139,
146 | fsum1p 15645 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ
(1...(โโ((logโ๐ด) / (logโ๐))))(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) = ((((ฮโ(๐โ1)) โ if((๐โ1) โ โ, (logโ(๐โ1)), 0)) / (๐โ1)) + ฮฃ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)))) |
148 | 51 | nncnd 12176 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ โ โ) |
149 | 148 | exp1d 14053 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (๐โ1) = ๐) |
150 | 149 | fveq2d 6851 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
(ฮโ(๐โ1))
= (ฮโ๐)) |
151 | | vmaprm 26482 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(ฮโ๐) =
(logโ๐)) |
152 | 49, 151 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
(ฮโ๐) =
(logโ๐)) |
153 | 150, 152 | eqtrd 2777 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
(ฮโ(๐โ1))
= (logโ๐)) |
154 | 149, 49 | eqeltrd 2838 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (๐โ1) โ โ) |
155 | 154 | iftrued 4499 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ if((๐โ1) โ โ,
(logโ(๐โ1)), 0)
= (logโ(๐โ1))) |
156 | 149 | fveq2d 6851 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (logโ(๐โ1)) = (logโ๐)) |
157 | 155, 156 | eqtrd 2777 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ if((๐โ1) โ โ,
(logโ(๐โ1)), 0)
= (logโ๐)) |
158 | 153, 157 | oveq12d 7380 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
((ฮโ(๐โ1)) โ if((๐โ1) โ โ, (logโ(๐โ1)), 0)) =
((logโ๐) โ
(logโ๐))) |
159 | 125 | subidd 11507 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((logโ๐) โ (logโ๐)) = 0) |
160 | 158, 159 | eqtrd 2777 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
((ฮโ(๐โ1)) โ if((๐โ1) โ โ, (logโ(๐โ1)), 0)) =
0) |
161 | 160, 149 | oveq12d 7380 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
(((ฮโ(๐โ1)) โ if((๐โ1) โ โ, (logโ(๐โ1)), 0)) / (๐โ1)) = (0 / ๐)) |
162 | 107 | rpcnne0d 12973 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (๐ โ โ โง ๐ โ 0)) |
163 | | div0 11850 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ 0) โ (0 / ๐) = 0) |
164 | 162, 163 | syl 17 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (0 / ๐) = 0) |
165 | 161, 164 | eqtrd 2777 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
(((ฮโ(๐โ1)) โ if((๐โ1) โ โ, (logโ(๐โ1)), 0)) / (๐โ1)) = 0) |
166 | | 1p1e2 12285 |
. . . . . . . . . 10
โข (1 + 1) =
2 |
167 | 166 | oveq1i 7372 |
. . . . . . . . 9
โข ((1 +
1)...(โโ((logโ๐ด) / (logโ๐)))) = (2...(โโ((logโ๐ด) / (logโ๐)))) |
168 | 167 | a1i 11 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐)))) = (2...(โโ((logโ๐ด) / (logโ๐))))) |
169 | | elfzuz 13444 |
. . . . . . . . . . . . . 14
โข (๐ โ
(2...(โโ((logโ๐ด) / (logโ๐)))) โ ๐ โ
(โคโฅโ2)) |
170 | | eluz2nn 12816 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ
(2...(โโ((logโ๐ด) / (logโ๐)))) โ ๐ โ โ) |
172 | 171, 167 | eleq2s 2856 |
. . . . . . . . . . . 12
โข (๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐)))) โ ๐ โ โ) |
173 | 49, 172, 89 | syl2an 597 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))) โ (ฮโ(๐โ๐)) = (logโ๐)) |
174 | 51 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))) โ ๐ โ โ) |
175 | | nnq 12894 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ) |
176 | 174, 175 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))) โ ๐ โ โ) |
177 | 169, 167 | eleq2s 2856 |
. . . . . . . . . . . . . 14
โข (๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐)))) โ ๐ โ
(โคโฅโ2)) |
178 | 177 | adantl 483 |
. . . . . . . . . . . . 13
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))) โ ๐ โ
(โคโฅโ2)) |
179 | | expnprm 16781 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ
(โคโฅโ2)) โ ยฌ (๐โ๐) โ โ) |
180 | 176, 178,
179 | syl2anc 585 |
. . . . . . . . . . . 12
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))) โ ยฌ (๐โ๐) โ โ) |
181 | 180 | iffalsed 4502 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0) = 0) |
182 | 173, 181 | oveq12d 7380 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))) โ ((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) = ((logโ๐) โ 0)) |
183 | 125 | subid1d 11508 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((logโ๐) โ 0) = (logโ๐)) |
184 | 183 | adantr 482 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))) โ ((logโ๐) โ 0) = (logโ๐)) |
185 | 182, 184 | eqtrd 2777 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))) โ ((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) = (logโ๐)) |
186 | 185 | oveq1d 7377 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))) โ (((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) = ((logโ๐) / (๐โ๐))) |
187 | 168, 186 | sumeq12dv 15598 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) = ฮฃ๐ โ (2...(โโ((logโ๐ด) / (logโ๐))))((logโ๐) / (๐โ๐))) |
188 | 165, 187 | oveq12d 7380 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
((((ฮโ(๐โ1)) โ if((๐โ1) โ โ, (logโ(๐โ1)), 0)) / (๐โ1)) + ฮฃ๐ โ ((1 +
1)...(โโ((logโ๐ด) / (logโ๐))))(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐))) = (0 + ฮฃ๐ โ (2...(โโ((logโ๐ด) / (logโ๐))))((logโ๐) / (๐โ๐)))) |
189 | | fzfid 13885 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
(2...(โโ((logโ๐ด) / (logโ๐)))) โ Fin) |
190 | 108 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ (logโ๐) โ
โ) |
191 | | nnnn0 12427 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ0) |
192 | 51, 191, 96 | syl2an 597 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ (๐โ๐) โ โ) |
193 | 190, 192 | nndivred 12214 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ ((logโ๐) / (๐โ๐)) โ โ) |
194 | 171, 193 | sylan2 594 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ (2...(โโ((logโ๐ด) / (logโ๐))))) โ ((logโ๐) / (๐โ๐)) โ โ) |
195 | 189, 194 | fsumrecl 15626 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ
(2...(โโ((logโ๐ด) / (logโ๐))))((logโ๐) / (๐โ๐)) โ โ) |
196 | 195 | recnd 11190 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ
(2...(โโ((logโ๐ด) / (logโ๐))))((logโ๐) / (๐โ๐)) โ โ) |
197 | 196 | addid2d 11363 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (0 + ฮฃ๐ โ
(2...(โโ((logโ๐ด) / (logโ๐))))((logโ๐) / (๐โ๐))) = ฮฃ๐ โ (2...(โโ((logโ๐ด) / (logโ๐))))((logโ๐) / (๐โ๐))) |
198 | 147, 188,
197 | 3eqtrd 2781 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ
(1...(โโ((logโ๐ด) / (logโ๐))))(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) = ฮฃ๐ โ (2...(โโ((logโ๐ด) / (logโ๐))))((logโ๐) / (๐โ๐))) |
199 | 107 | rpreccld 12974 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (1 / ๐) โ
โ+) |
200 | 124 | flcld 13710 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
(โโ((logโ๐ด) / (logโ๐))) โ โค) |
201 | 200 | peano2zd 12617 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
((โโ((logโ๐ด) / (logโ๐))) + 1) โ โค) |
202 | 199, 201 | rpexpcld 14157 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1)) โ
โ+) |
203 | 202 | rpge0d 12968 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ 0 โค ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) |
204 | 51 | nnrecred 12211 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (1 / ๐) โ
โ) |
205 | 204 | resqcld 14037 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((1 / ๐)โ2) โ
โ) |
206 | 135 | peano2nnd 12177 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
((โโ((logโ๐ด) / (logโ๐))) + 1) โ โ) |
207 | 206 | nnnn0d 12480 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
((โโ((logโ๐ด) / (logโ๐))) + 1) โ
โ0) |
208 | 204, 207 | reexpcld 14075 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1)) โ
โ) |
209 | 205, 208 | subge02d 11754 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (0 โค ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1)) โ (((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) โค ((1 / ๐)โ2))) |
210 | 203, 209 | mpbid 231 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) โค ((1 / ๐)โ2)) |
211 | 110 | nnrpd 12962 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (๐ โ 1) โ
โ+) |
212 | 211 | rpcnne0d 12973 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((๐ โ 1) โ โ โง
(๐ โ 1) โ
0)) |
213 | 199 | rpcnd 12966 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (1 / ๐) โ
โ) |
214 | | dmdcan 11872 |
. . . . . . . . . . 11
โข ((((๐ โ 1) โ โ โง
(๐ โ 1) โ 0) โง
(๐ โ โ โง
๐ โ 0) โง (1 / ๐) โ โ) โ
(((๐ โ 1) / ๐) ยท ((1 / ๐) / (๐ โ 1))) = ((1 / ๐) / ๐)) |
215 | 212, 162,
213, 214 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (((๐ โ 1) / ๐) ยท ((1 / ๐) / (๐ โ 1))) = ((1 / ๐) / ๐)) |
216 | 131 | recnd 11190 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ 1 โ
โ) |
217 | | divsubdir 11856 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง 1 โ
โ โง (๐ โ
โ โง ๐ โ 0))
โ ((๐ โ 1) /
๐) = ((๐ / ๐) โ (1 / ๐))) |
218 | 148, 216,
162, 217 | syl3anc 1372 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((๐ โ 1) / ๐) = ((๐ / ๐) โ (1 / ๐))) |
219 | | divid 11849 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ 0) โ (๐ / ๐) = 1) |
220 | 162, 219 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (๐ / ๐) = 1) |
221 | 220 | oveq1d 7377 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((๐ / ๐) โ (1 / ๐)) = (1 โ (1 / ๐))) |
222 | 218, 221 | eqtrd 2777 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((๐ โ 1) / ๐) = (1 โ (1 / ๐))) |
223 | | divdiv1 11873 |
. . . . . . . . . . . 12
โข ((1
โ โ โง (๐
โ โ โง ๐ โ
0) โง ((๐ โ 1)
โ โ โง (๐
โ 1) โ 0)) โ ((1 / ๐) / (๐ โ 1)) = (1 / (๐ ยท (๐ โ 1)))) |
224 | 216, 162,
212, 223 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((1 / ๐) / (๐ โ 1)) = (1 / (๐ ยท (๐ โ 1)))) |
225 | 222, 224 | oveq12d 7380 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (((๐ โ 1) / ๐) ยท ((1 / ๐) / (๐ โ 1))) = ((1 โ (1 / ๐)) ยท (1 / (๐ ยท (๐ โ 1))))) |
226 | 51 | nnne0d 12210 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ๐ โ 0) |
227 | 213, 148,
226 | divrecd 11941 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((1 / ๐) / ๐) = ((1 / ๐) ยท (1 / ๐))) |
228 | 213 | sqvald 14055 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((1 / ๐)โ2) = ((1 / ๐) ยท (1 / ๐))) |
229 | 227, 228 | eqtr4d 2780 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((1 / ๐) / ๐) = ((1 / ๐)โ2)) |
230 | 215, 225,
229 | 3eqtr3d 2785 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((1 โ (1 /
๐)) ยท (1 / (๐ ยท (๐ โ 1)))) = ((1 / ๐)โ2)) |
231 | 210, 230 | breqtrrd 5138 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) โค ((1 โ (1 /
๐)) ยท (1 / (๐ ยท (๐ โ 1))))) |
232 | 205, 208 | resubcld 11590 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) โ
โ) |
233 | 111 | nnrecred 12211 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (1 / (๐ ยท (๐ โ 1))) โ
โ) |
234 | | resubcl 11472 |
. . . . . . . . . 10
โข ((1
โ โ โง (1 / ๐) โ โ) โ (1 โ (1 /
๐)) โ
โ) |
235 | 130, 204,
234 | sylancr 588 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (1 โ (1 /
๐)) โ
โ) |
236 | | recgt1 12058 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 0 <
๐) โ (1 < ๐ โ (1 / ๐) < 1)) |
237 | 52, 117, 236 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (1 < ๐ โ (1 / ๐) < 1)) |
238 | 122, 237 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (1 / ๐) < 1) |
239 | | posdif 11655 |
. . . . . . . . . . 11
โข (((1 /
๐) โ โ โง 1
โ โ) โ ((1 / ๐) < 1 โ 0 < (1 โ (1 / ๐)))) |
240 | 204, 130,
239 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((1 / ๐) < 1 โ 0 < (1
โ (1 / ๐)))) |
241 | 238, 240 | mpbid 231 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ 0 < (1 โ
(1 / ๐))) |
242 | | ledivmul 12038 |
. . . . . . . . 9
โข (((((1 /
๐)โ2) โ ((1 /
๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) โ โ โง
(1 / (๐ ยท (๐ โ 1))) โ โ
โง ((1 โ (1 / ๐))
โ โ โง 0 < (1 โ (1 / ๐)))) โ (((((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) / (1 โ (1 /
๐))) โค (1 / (๐ ยท (๐ โ 1))) โ (((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) โค ((1 โ (1 /
๐)) ยท (1 / (๐ ยท (๐ โ 1)))))) |
243 | 232, 233,
235, 241, 242 | syl112anc 1375 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (((((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) / (1 โ (1 /
๐))) โค (1 / (๐ ยท (๐ โ 1))) โ (((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) โค ((1 โ (1 /
๐)) ยท (1 / (๐ ยท (๐ โ 1)))))) |
244 | 231, 243 | mpbird 257 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) / (1 โ (1 /
๐))) โค (1 / (๐ ยท (๐ โ 1)))) |
245 | 235, 241 | elrpd 12961 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (1 โ (1 /
๐)) โ
โ+) |
246 | 232, 245 | rerpdivcld 12995 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) / (1 โ (1 /
๐))) โ
โ) |
247 | 246, 233,
123 | lemul2d 13008 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (((((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) / (1 โ (1 /
๐))) โค (1 / (๐ ยท (๐ โ 1))) โ ((logโ๐) ยท ((((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) / (1 โ (1 /
๐)))) โค
((logโ๐) ยท (1
/ (๐ ยท (๐ โ
1)))))) |
248 | 244, 247 | mpbid 231 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((logโ๐) ยท ((((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) / (1 โ (1 /
๐)))) โค
((logโ๐) ยท (1
/ (๐ ยท (๐ โ 1))))) |
249 | 125 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ (logโ๐) โ
โ) |
250 | 192 | nncnd 12176 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ (๐โ๐) โ โ) |
251 | 192 | nnne0d 12210 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ (๐โ๐) โ 0) |
252 | 249, 250,
251 | divrecd 11941 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ ((logโ๐) / (๐โ๐)) = ((logโ๐) ยท (1 / (๐โ๐)))) |
253 | 148 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ ๐ โ โ) |
254 | 51 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ ๐ โ โ) |
255 | 254 | nnne0d 12210 |
. . . . . . . . . . . 12
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ ๐ โ 0) |
256 | | nnz 12527 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โค) |
257 | 256 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ ๐ โ โค) |
258 | 253, 255,
257 | exprecd 14066 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ ((1 / ๐)โ๐) = (1 / (๐โ๐))) |
259 | 258 | oveq2d 7378 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ ((logโ๐) ยท ((1 / ๐)โ๐)) = ((logโ๐) ยท (1 / (๐โ๐)))) |
260 | 252, 259 | eqtr4d 2780 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ โ) โ ((logโ๐) / (๐โ๐)) = ((logโ๐) ยท ((1 / ๐)โ๐))) |
261 | 171, 260 | sylan2 594 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ (2...(โโ((logโ๐ด) / (logโ๐))))) โ ((logโ๐) / (๐โ๐)) = ((logโ๐) ยท ((1 / ๐)โ๐))) |
262 | 261 | sumeq2dv 15595 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ
(2...(โโ((logโ๐ด) / (logโ๐))))((logโ๐) / (๐โ๐)) = ฮฃ๐ โ (2...(โโ((logโ๐ด) / (logโ๐))))((logโ๐) ยท ((1 / ๐)โ๐))) |
263 | 171 | nnnn0d 12480 |
. . . . . . . . 9
โข (๐ โ
(2...(โโ((logโ๐ด) / (logโ๐)))) โ ๐ โ โ0) |
264 | | expcl 13992 |
. . . . . . . . 9
โข (((1 /
๐) โ โ โง
๐ โ
โ0) โ ((1 / ๐)โ๐) โ โ) |
265 | 213, 263,
264 | syl2an 597 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โง ๐ โ (2...(โโ((logโ๐ด) / (logโ๐))))) โ ((1 / ๐)โ๐) โ โ) |
266 | 189, 125,
265 | fsummulc2 15676 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((logโ๐) ยท ฮฃ๐ โ
(2...(โโ((logโ๐ด) / (logโ๐))))((1 / ๐)โ๐)) = ฮฃ๐ โ (2...(โโ((logโ๐ด) / (logโ๐))))((logโ๐) ยท ((1 / ๐)โ๐))) |
267 | | fzval3 13648 |
. . . . . . . . . . 11
โข
((โโ((logโ๐ด) / (logโ๐))) โ โค โ
(2...(โโ((logโ๐ด) / (logโ๐)))) = (2..^((โโ((logโ๐ด) / (logโ๐))) + 1))) |
268 | 200, 267 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
(2...(โโ((logโ๐ด) / (logโ๐)))) = (2..^((โโ((logโ๐ด) / (logโ๐))) + 1))) |
269 | 268 | sumeq1d 15593 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ
(2...(โโ((logโ๐ด) / (logโ๐))))((1 / ๐)โ๐) = ฮฃ๐ โ
(2..^((โโ((logโ๐ด) / (logโ๐))) + 1))((1 / ๐)โ๐)) |
270 | 204, 238 | ltned 11298 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (1 / ๐) โ 1) |
271 | | 2nn0 12437 |
. . . . . . . . . . 11
โข 2 โ
โ0 |
272 | 271 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ 2 โ
โ0) |
273 | | eluzp1p1 12798 |
. . . . . . . . . . . 12
โข
((โโ((logโ๐ด) / (logโ๐))) โ (โคโฅโ1)
โ ((โโ((logโ๐ด) / (logโ๐))) + 1) โ
(โคโฅโ(1 + 1))) |
274 | 137, 273 | syl 17 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
((โโ((logโ๐ด) / (logโ๐))) + 1) โ
(โคโฅโ(1 + 1))) |
275 | | df-2 12223 |
. . . . . . . . . . . 12
โข 2 = (1 +
1) |
276 | 275 | fveq2i 6850 |
. . . . . . . . . . 11
โข
(โคโฅโ2) = (โคโฅโ(1 +
1)) |
277 | 274, 276 | eleqtrrdi 2849 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ
((โโ((logโ๐ด) / (logโ๐))) + 1) โ
(โคโฅโ2)) |
278 | 213, 270,
272, 277 | geoserg 15758 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ
(2..^((โโ((logโ๐ด) / (logโ๐))) + 1))((1 / ๐)โ๐) = ((((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) / (1 โ (1 /
๐)))) |
279 | 269, 278 | eqtrd 2777 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ
(2...(โโ((logโ๐ด) / (logโ๐))))((1 / ๐)โ๐) = ((((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) / (1 โ (1 /
๐)))) |
280 | 279 | oveq2d 7378 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((logโ๐) ยท ฮฃ๐ โ
(2...(โโ((logโ๐ด) / (logโ๐))))((1 / ๐)โ๐)) = ((logโ๐) ยท ((((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) / (1 โ (1 /
๐))))) |
281 | 262, 266,
280 | 3eqtr2d 2783 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ
(2...(โโ((logโ๐ด) / (logโ๐))))((logโ๐) / (๐โ๐)) = ((logโ๐) ยท ((((1 / ๐)โ2) โ ((1 / ๐)โ((โโ((logโ๐ด) / (logโ๐))) + 1))) / (1 โ (1 /
๐))))) |
282 | 111 | nncnd 12176 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (๐ ยท (๐ โ 1)) โ โ) |
283 | 111 | nnne0d 12210 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ (๐ ยท (๐ โ 1)) โ 0) |
284 | 125, 282,
283 | divrecd 11941 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ((logโ๐) / (๐ ยท (๐ โ 1))) = ((logโ๐) ยท (1 / (๐ ยท (๐ โ 1))))) |
285 | 248, 281,
284 | 3brtr4d 5142 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ
(2...(โโ((logโ๐ด) / (logโ๐))))((logโ๐) / (๐โ๐)) โค ((logโ๐) / (๐ ยท (๐ โ 1)))) |
286 | 198, 285 | eqbrtrd 5132 |
. . . 4
โข ((๐ด โ โค โง ๐ โ ((0[,]๐ด) โฉ โ)) โ ฮฃ๐ โ
(1...(โโ((logโ๐ด) / (logโ๐))))(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) โค ((logโ๐) / (๐ ยท (๐ โ 1)))) |
287 | 83, 105, 112, 286 | fsumle 15691 |
. . 3
โข (๐ด โ โค โ
ฮฃ๐ โ ((0[,]๐ด) โฉ โ)ฮฃ๐ โ
(1...(โโ((logโ๐ด) / (logโ๐))))(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) โค ฮฃ๐ โ ((0[,]๐ด) โฉ โ)((logโ๐) / (๐ ยท (๐ โ 1)))) |
288 | | elfzuz 13444 |
. . . . . . . . . . 11
โข (๐ โ (2...((absโ๐ด) + 1)) โ ๐ โ
(โคโฅโ2)) |
289 | | eluz2nn 12816 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
290 | 288, 289 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (2...((absโ๐ด) + 1)) โ ๐ โ
โ) |
291 | 290 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ (2...((absโ๐ด) + 1))) โ ๐ โ
โ) |
292 | 291 | nnred 12175 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ (2...((absโ๐ด) + 1))) โ ๐ โ
โ) |
293 | 288 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ (2...((absโ๐ด) + 1))) โ ๐ โ
(โคโฅโ2)) |
294 | | eluz2gt1 12852 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ2) โ 1 < ๐) |
295 | 293, 294 | syl 17 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ (2...((absโ๐ด) + 1))) โ 1 < ๐) |
296 | 292, 295 | rplogcld 26000 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ (2...((absโ๐ด) + 1))) โ (logโ๐) โ
โ+) |
297 | 293, 109 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ (2...((absโ๐ด) + 1))) โ (๐ โ 1) โ
โ) |
298 | 291, 297 | nnmulcld 12213 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ (2...((absโ๐ด) + 1))) โ (๐ ยท (๐ โ 1)) โ โ) |
299 | 298 | nnrpd 12962 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ (2...((absโ๐ด) + 1))) โ (๐ ยท (๐ โ 1)) โ
โ+) |
300 | 296, 299 | rpdivcld 12981 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ (2...((absโ๐ด) + 1))) โ
((logโ๐) / (๐ ยท (๐ โ 1))) โ
โ+) |
301 | 300 | rpred 12964 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ (2...((absโ๐ด) + 1))) โ
((logโ๐) / (๐ ยท (๐ โ 1))) โ
โ) |
302 | 47, 301 | fsumrecl 15626 |
. . . 4
โข (๐ด โ โค โ
ฮฃ๐ โ
(2...((absโ๐ด) +
1))((logโ๐) / (๐ ยท (๐ โ 1))) โ
โ) |
303 | 300 | rpge0d 12968 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ (2...((absโ๐ด) + 1))) โ 0 โค
((logโ๐) / (๐ ยท (๐ โ 1)))) |
304 | 47, 301, 303, 82 | fsumless 15688 |
. . . 4
โข (๐ด โ โค โ
ฮฃ๐ โ ((0[,]๐ด) โฉ
โ)((logโ๐) /
(๐ ยท (๐ โ 1))) โค ฮฃ๐ โ (2...((absโ๐ด) + 1))((logโ๐) / (๐ ยท (๐ โ 1)))) |
305 | | rplogsumlem1 26848 |
. . . . 5
โข
(((absโ๐ด) + 1)
โ โ โ ฮฃ๐ โ (2...((absโ๐ด) + 1))((logโ๐) / (๐ ยท (๐ โ 1))) โค 2) |
306 | 75, 305 | syl 17 |
. . . 4
โข (๐ด โ โค โ
ฮฃ๐ โ
(2...((absโ๐ด) +
1))((logโ๐) / (๐ ยท (๐ โ 1))) โค 2) |
307 | 113, 302,
115, 304, 306 | letrd 11319 |
. . 3
โข (๐ด โ โค โ
ฮฃ๐ โ ((0[,]๐ด) โฉ
โ)((logโ๐) /
(๐ ยท (๐ โ 1))) โค
2) |
308 | 106, 113,
115, 287, 307 | letrd 11319 |
. 2
โข (๐ด โ โค โ
ฮฃ๐ โ ((0[,]๐ด) โฉ โ)ฮฃ๐ โ
(1...(โโ((logโ๐ด) / (logโ๐))))(((ฮโ(๐โ๐)) โ if((๐โ๐) โ โ, (logโ(๐โ๐)), 0)) / (๐โ๐)) โค 2) |
309 | 46, 308 | eqbrtrd 5132 |
1
โข (๐ด โ โค โ
ฮฃ๐ โ (1...๐ด)(((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) / ๐) โค 2) |