Step | Hyp | Ref
| Expression |
1 | | reex 11201 |
. . . . . . 7
โข โ
โ V |
2 | | rpssre 12981 |
. . . . . . 7
โข
โ+ โ โ |
3 | 1, 2 | ssexi 5323 |
. . . . . 6
โข
โ+ โ V |
4 | 3 | a1i 11 |
. . . . 5
โข (โค
โ โ+ โ V) |
5 | | ovexd 7444 |
. . . . 5
โข
((โค โง ๐ฅ
โ โ+) โ (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ V) |
6 | | ovexd 7444 |
. . . . 5
โข
((โค โง ๐ฅ
โ โ+) โ ((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ V) |
7 | | eqidd 2734 |
. . . . 5
โข (โค
โ (๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) = (๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)))) |
8 | | eqidd 2734 |
. . . . 5
โข (โค
โ (๐ฅ โ
โ+ โฆ ((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) = (๐ฅ โ โ+ โฆ
((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)))) |
9 | 4, 5, 6, 7, 8 | offval2 7690 |
. . . 4
โข (โค
โ ((๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โf โ (๐ฅ โ โ+
โฆ ((logโ๐ฅ)
โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ)))) = (๐ฅ โ โ+ โฆ
((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ ((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))))) |
10 | 9 | mptru 1549 |
. . 3
โข ((๐ฅ โ โ+
โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โf โ (๐ฅ โ โ+
โฆ ((logโ๐ฅ)
โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ)))) = (๐ฅ โ โ+ โฆ
((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ ((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)))) |
11 | | fzfid 13938 |
. . . . . . 7
โข (๐ฅ โ โ+
โ (1...(โโ๐ฅ)) โ Fin) |
12 | | elfznn 13530 |
. . . . . . . . . 10
โข (๐ โ
(1...(โโ๐ฅ))
โ ๐ โ
โ) |
13 | 12 | adantl 483 |
. . . . . . . . 9
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ โ
โ) |
14 | | vmacl 26622 |
. . . . . . . . 9
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ (ฮโ๐)
โ โ) |
16 | 15, 13 | nndivred 12266 |
. . . . . . 7
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
/ ๐) โ
โ) |
17 | 11, 16 | fsumrecl 15680 |
. . . . . 6
โข (๐ฅ โ โ+
โ ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ โ) |
18 | 17 | recnd 11242 |
. . . . 5
โข (๐ฅ โ โ+
โ ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ โ) |
19 | | relogcl 26084 |
. . . . . 6
โข (๐ฅ โ โ+
โ (logโ๐ฅ) โ
โ) |
20 | 19 | recnd 11242 |
. . . . 5
โข (๐ฅ โ โ+
โ (logโ๐ฅ) โ
โ) |
21 | | rprege0 12989 |
. . . . . . . . . 10
โข (๐ฅ โ โ+
โ (๐ฅ โ โ
โง 0 โค ๐ฅ)) |
22 | | flge0nn0 13785 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง 0 โค
๐ฅ) โ
(โโ๐ฅ) โ
โ0) |
23 | | faccl 14243 |
. . . . . . . . . 10
โข
((โโ๐ฅ)
โ โ0 โ (!โ(โโ๐ฅ)) โ โ) |
24 | 21, 22, 23 | 3syl 18 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ (!โ(โโ๐ฅ)) โ โ) |
25 | 24 | nnrpd 13014 |
. . . . . . . 8
โข (๐ฅ โ โ+
โ (!โ(โโ๐ฅ)) โ
โ+) |
26 | 25 | relogcld 26131 |
. . . . . . 7
โข (๐ฅ โ โ+
โ (logโ(!โ(โโ๐ฅ))) โ โ) |
27 | | rerpdivcl 13004 |
. . . . . . 7
โข
(((logโ(!โ(โโ๐ฅ))) โ โ โง ๐ฅ โ โ+) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ) โ โ) |
28 | 26, 27 | mpancom 687 |
. . . . . 6
โข (๐ฅ โ โ+
โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ) โ โ) |
29 | 28 | recnd 11242 |
. . . . 5
โข (๐ฅ โ โ+
โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ) โ โ) |
30 | 18, 20, 29 | nnncan2d 11606 |
. . . 4
โข (๐ฅ โ โ+
โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ ((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) = (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ))) |
31 | 30 | mpteq2ia 5252 |
. . 3
โข (๐ฅ โ โ+
โฆ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ ((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)))) = (๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ))) |
32 | 10, 31 | eqtri 2761 |
. 2
โข ((๐ฅ โ โ+
โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โf โ (๐ฅ โ โ+
โฆ ((logโ๐ฅ)
โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ)))) = (๐ฅ โ โ+ โฆ
(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ))) |
33 | | 1red 11215 |
. . . . 5
โข (โค
โ 1 โ โ) |
34 | | chpo1ub 26983 |
. . . . . 6
โข (๐ฅ โ โ+
โฆ ((ฯโ๐ฅ) /
๐ฅ)) โ
๐(1) |
35 | 34 | a1i 11 |
. . . . 5
โข (โค
โ (๐ฅ โ
โ+ โฆ ((ฯโ๐ฅ) / ๐ฅ)) โ ๐(1)) |
36 | | rpre 12982 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ ๐ฅ โ
โ) |
37 | | chpcl 26628 |
. . . . . . . . 9
โข (๐ฅ โ โ โ
(ฯโ๐ฅ) โ
โ) |
38 | 36, 37 | syl 17 |
. . . . . . . 8
โข (๐ฅ โ โ+
โ (ฯโ๐ฅ)
โ โ) |
39 | | rerpdivcl 13004 |
. . . . . . . 8
โข
(((ฯโ๐ฅ)
โ โ โง ๐ฅ
โ โ+) โ ((ฯโ๐ฅ) / ๐ฅ) โ โ) |
40 | 38, 39 | mpancom 687 |
. . . . . . 7
โข (๐ฅ โ โ+
โ ((ฯโ๐ฅ) /
๐ฅ) โ
โ) |
41 | 40 | recnd 11242 |
. . . . . 6
โข (๐ฅ โ โ+
โ ((ฯโ๐ฅ) /
๐ฅ) โ
โ) |
42 | 41 | adantl 483 |
. . . . 5
โข
((โค โง ๐ฅ
โ โ+) โ ((ฯโ๐ฅ) / ๐ฅ) โ โ) |
43 | 18, 29 | subcld 11571 |
. . . . . 6
โข (๐ฅ โ โ+
โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ โ) |
44 | 43 | adantl 483 |
. . . . 5
โข
((โค โง ๐ฅ
โ โ+) โ (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ โ) |
45 | 36 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ฅ โ
โ) |
46 | 16, 45 | remulcld 11244 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท ๐ฅ) โ
โ) |
47 | | nndivre 12253 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ฅ / ๐) โ โ) |
48 | 36, 12, 47 | syl2an 597 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ (๐ฅ / ๐) โ
โ) |
49 | | reflcl 13761 |
. . . . . . . . . . . . 13
โข ((๐ฅ / ๐) โ โ โ (โโ(๐ฅ / ๐)) โ โ) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ (โโ(๐ฅ /
๐)) โ
โ) |
51 | 15, 50 | remulcld 11244 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท (โโ(๐ฅ
/ ๐))) โ
โ) |
52 | 46, 51 | resubcld 11642 |
. . . . . . . . . 10
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((((ฮโ๐) / ๐) ยท ๐ฅ) โ ((ฮโ๐) ยท (โโ(๐ฅ / ๐)))) โ โ) |
53 | 48, 50 | resubcld 11642 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((๐ฅ / ๐) โ (โโ(๐ฅ / ๐))) โ โ) |
54 | | 1red 11215 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ 1 โ โ) |
55 | | vmage0 26625 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ 0 โค
(ฮโ๐)) |
56 | 13, 55 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ 0 โค (ฮโ๐)) |
57 | | fracle1 13768 |
. . . . . . . . . . . . 13
โข ((๐ฅ / ๐) โ โ โ ((๐ฅ / ๐) โ (โโ(๐ฅ / ๐))) โค 1) |
58 | 48, 57 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((๐ฅ / ๐) โ (โโ(๐ฅ / ๐))) โค 1) |
59 | 53, 54, 15, 56, 58 | lemul2ad 12154 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท ((๐ฅ / ๐) โ (โโ(๐ฅ / ๐)))) โค ((ฮโ๐) ยท 1)) |
60 | 15 | recnd 11242 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ (ฮโ๐)
โ โ) |
61 | 48 | recnd 11242 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ (๐ฅ / ๐) โ
โ) |
62 | 50 | recnd 11242 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ (โโ(๐ฅ /
๐)) โ
โ) |
63 | 60, 61, 62 | subdid 11670 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท ((๐ฅ / ๐) โ (โโ(๐ฅ / ๐)))) = (((ฮโ๐) ยท (๐ฅ / ๐)) โ ((ฮโ๐) ยท (โโ(๐ฅ / ๐))))) |
64 | | rpcn 12984 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โ+
โ ๐ฅ โ
โ) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ฅ โ
โ) |
66 | 13 | nnrpd 13014 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ๐ โ
โ+) |
67 | | rpcnne0 12992 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ+
โ (๐ โ โ
โง ๐ โ
0)) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ (๐ โ โ
โง ๐ โ
0)) |
69 | | div23 11891 |
. . . . . . . . . . . . . . 15
โข
(((ฮโ๐)
โ โ โง ๐ฅ
โ โ โง (๐
โ โ โง ๐ โ
0)) โ (((ฮโ๐) ยท ๐ฅ) / ๐) = (((ฮโ๐) / ๐) ยท ๐ฅ)) |
70 | | divass 11890 |
. . . . . . . . . . . . . . 15
โข
(((ฮโ๐)
โ โ โง ๐ฅ
โ โ โง (๐
โ โ โง ๐ โ
0)) โ (((ฮโ๐) ยท ๐ฅ) / ๐) = ((ฮโ๐) ยท (๐ฅ / ๐))) |
71 | 69, 70 | eqtr3d 2775 |
. . . . . . . . . . . . . 14
โข
(((ฮโ๐)
โ โ โง ๐ฅ
โ โ โง (๐
โ โ โง ๐ โ
0)) โ (((ฮโ๐) / ๐) ยท ๐ฅ) = ((ฮโ๐) ยท (๐ฅ / ๐))) |
72 | 60, 65, 68, 71 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท ๐ฅ) = ((ฮโ๐) ยท (๐ฅ / ๐))) |
73 | 72 | oveq1d 7424 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((((ฮโ๐) / ๐) ยท ๐ฅ) โ ((ฮโ๐) ยท (โโ(๐ฅ / ๐)))) = (((ฮโ๐) ยท (๐ฅ / ๐)) โ ((ฮโ๐) ยท (โโ(๐ฅ / ๐))))) |
74 | 63, 73 | eqtr4d 2776 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท ((๐ฅ / ๐) โ (โโ(๐ฅ / ๐)))) = ((((ฮโ๐) / ๐) ยท ๐ฅ) โ ((ฮโ๐) ยท (โโ(๐ฅ / ๐))))) |
75 | 60 | mulridd 11231 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท 1) = (ฮโ๐)) |
76 | 59, 74, 75 | 3brtr3d 5180 |
. . . . . . . . . 10
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((((ฮโ๐) / ๐) ยท ๐ฅ) โ ((ฮโ๐) ยท (โโ(๐ฅ / ๐)))) โค (ฮโ๐)) |
77 | 11, 52, 15, 76 | fsumle 15745 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ ฮฃ๐ โ
(1...(โโ๐ฅ))((((ฮโ๐) / ๐) ยท ๐ฅ) โ ((ฮโ๐) ยท (โโ(๐ฅ / ๐)))) โค ฮฃ๐ โ (1...(โโ๐ฅ))(ฮโ๐)) |
78 | 16 | recnd 11242 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
/ ๐) โ
โ) |
79 | 11, 64, 78 | fsummulc1 15731 |
. . . . . . . . . . 11
โข (๐ฅ โ โ+
โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) = ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ๐ฅ)) |
80 | | logfac2 26720 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง 0 โค
๐ฅ) โ
(logโ(!โ(โโ๐ฅ))) = ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท (โโ(๐ฅ / ๐)))) |
81 | 21, 80 | syl 17 |
. . . . . . . . . . 11
โข (๐ฅ โ โ+
โ (logโ(!โ(โโ๐ฅ))) = ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท (โโ(๐ฅ / ๐)))) |
82 | 79, 81 | oveq12d 7427 |
. . . . . . . . . 10
โข (๐ฅ โ โ+
โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) = (ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ๐ฅ) โ ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท (โโ(๐ฅ / ๐))))) |
83 | 46 | recnd 11242 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ (((ฮโ๐)
/ ๐) ยท ๐ฅ) โ
โ) |
84 | 51 | recnd 11242 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ ((ฮโ๐)
ยท (โโ(๐ฅ
/ ๐))) โ
โ) |
85 | 11, 83, 84 | fsumsub 15734 |
. . . . . . . . . 10
โข (๐ฅ โ โ+
โ ฮฃ๐ โ
(1...(โโ๐ฅ))((((ฮโ๐) / ๐) ยท ๐ฅ) โ ((ฮโ๐) ยท (โโ(๐ฅ / ๐)))) = (ฮฃ๐ โ (1...(โโ๐ฅ))(((ฮโ๐) / ๐) ยท ๐ฅ) โ ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) ยท (โโ(๐ฅ / ๐))))) |
86 | 82, 85 | eqtr4d 2776 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) = ฮฃ๐ โ (1...(โโ๐ฅ))((((ฮโ๐) / ๐) ยท ๐ฅ) โ ((ฮโ๐) ยท (โโ(๐ฅ / ๐))))) |
87 | | chpval 26626 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
(ฯโ๐ฅ) =
ฮฃ๐ โ
(1...(โโ๐ฅ))(ฮโ๐)) |
88 | 36, 87 | syl 17 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ (ฯโ๐ฅ) =
ฮฃ๐ โ
(1...(โโ๐ฅ))(ฮโ๐)) |
89 | 77, 86, 88 | 3brtr4d 5181 |
. . . . . . . 8
โข (๐ฅ โ โ+
โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) โค (ฯโ๐ฅ)) |
90 | 17, 36 | remulcld 11244 |
. . . . . . . . . 10
โข (๐ฅ โ โ+
โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ โ) |
91 | 90, 26 | resubcld 11642 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) โ โ) |
92 | | rpregt0 12988 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ (๐ฅ โ โ
โง 0 < ๐ฅ)) |
93 | | lediv1 12079 |
. . . . . . . . 9
โข
((((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) โ โ โง (ฯโ๐ฅ) โ โ โง (๐ฅ โ โ โง 0 <
๐ฅ)) โ (((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) โค (ฯโ๐ฅ) โ (((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ) โค ((ฯโ๐ฅ) / ๐ฅ))) |
94 | 91, 38, 92, 93 | syl3anc 1372 |
. . . . . . . 8
โข (๐ฅ โ โ+
โ (((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) โค (ฯโ๐ฅ) โ (((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ) โค ((ฯโ๐ฅ) / ๐ฅ))) |
95 | 89, 94 | mpbid 231 |
. . . . . . 7
โข (๐ฅ โ โ+
โ (((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ) โค ((ฯโ๐ฅ) / ๐ฅ)) |
96 | 90 | recnd 11242 |
. . . . . . . . . . 11
โข (๐ฅ โ โ+
โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ โ) |
97 | 26 | recnd 11242 |
. . . . . . . . . . 11
โข (๐ฅ โ โ+
โ (logโ(!โ(โโ๐ฅ))) โ โ) |
98 | | rpcnne0 12992 |
. . . . . . . . . . 11
โข (๐ฅ โ โ+
โ (๐ฅ โ โ
โง ๐ฅ โ
0)) |
99 | | divsubdir 11908 |
. . . . . . . . . . 11
โข
(((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ โ โง
(logโ(!โ(โโ๐ฅ))) โ โ โง (๐ฅ โ โ โง ๐ฅ โ 0)) โ (((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ) = (((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) / ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) |
100 | 96, 97, 98, 99 | syl3anc 1372 |
. . . . . . . . . 10
โข (๐ฅ โ โ+
โ (((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ) = (((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) / ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) |
101 | | rpne0 12990 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ+
โ ๐ฅ โ
0) |
102 | 18, 64, 101 | divcan4d 11996 |
. . . . . . . . . . 11
โข (๐ฅ โ โ+
โ ((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) / ๐ฅ) = ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐)) |
103 | 102 | oveq1d 7424 |
. . . . . . . . . 10
โข (๐ฅ โ โ+
โ (((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) / ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) = (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) |
104 | 100, 103 | eqtr2d 2774 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) = (((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ)) |
105 | 104 | fveq2d 6896 |
. . . . . . . 8
โข (๐ฅ โ โ+
โ (absโ(ฮฃ๐
โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) = (absโ(((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ))) |
106 | | rerpdivcl 13004 |
. . . . . . . . . 10
โข
((((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) โ โ โง ๐ฅ โ โ+) โ
(((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ) โ โ) |
107 | 91, 106 | mpancom 687 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ (((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ) โ โ) |
108 | | flle 13764 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ / ๐) โ โ โ (โโ(๐ฅ / ๐)) โค (๐ฅ / ๐)) |
109 | 48, 108 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ (โโ(๐ฅ /
๐)) โค (๐ฅ / ๐)) |
110 | 48, 50 | subge0d 11804 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ (0 โค ((๐ฅ / ๐) โ (โโ(๐ฅ / ๐))) โ (โโ(๐ฅ / ๐)) โค (๐ฅ / ๐))) |
111 | 109, 110 | mpbird 257 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ 0 โค ((๐ฅ / ๐) โ (โโ(๐ฅ / ๐)))) |
112 | 15, 53, 56, 111 | mulge0d 11791 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ 0 โค ((ฮโ๐) ยท ((๐ฅ / ๐) โ (โโ(๐ฅ / ๐))))) |
113 | 112, 74 | breqtrd 5175 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ+
โง ๐ โ
(1...(โโ๐ฅ)))
โ 0 โค ((((ฮโ๐) / ๐) ยท ๐ฅ) โ ((ฮโ๐) ยท (โโ(๐ฅ / ๐))))) |
114 | 11, 52, 113 | fsumge0 15741 |
. . . . . . . . . . 11
โข (๐ฅ โ โ+
โ 0 โค ฮฃ๐
โ (1...(โโ๐ฅ))((((ฮโ๐) / ๐) ยท ๐ฅ) โ ((ฮโ๐) ยท (โโ(๐ฅ / ๐))))) |
115 | 114, 86 | breqtrrd 5177 |
. . . . . . . . . 10
โข (๐ฅ โ โ+
โ 0 โค ((ฮฃ๐
โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ))))) |
116 | | divge0 12083 |
. . . . . . . . . 10
โข
(((((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) โ โ โง 0 โค
((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ))))) โง (๐ฅ โ โ โง 0 < ๐ฅ)) โ 0 โค (((ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ)) |
117 | 91, 115, 92, 116 | syl21anc 837 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ 0 โค (((ฮฃ๐
โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ)) |
118 | 107, 117 | absidd 15369 |
. . . . . . . 8
โข (๐ฅ โ โ+
โ (absโ(((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ)) = (((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ)) |
119 | 105, 118 | eqtrd 2773 |
. . . . . . 7
โข (๐ฅ โ โ+
โ (absโ(ฮฃ๐
โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) = (((ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) ยท ๐ฅ) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ)) |
120 | | chpge0 26630 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ 0 โค
(ฯโ๐ฅ)) |
121 | 36, 120 | syl 17 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ 0 โค (ฯโ๐ฅ)) |
122 | | divge0 12083 |
. . . . . . . . 9
โข
((((ฯโ๐ฅ)
โ โ โง 0 โค (ฯโ๐ฅ)) โง (๐ฅ โ โ โง 0 < ๐ฅ)) โ 0 โค
((ฯโ๐ฅ) / ๐ฅ)) |
123 | 38, 121, 92, 122 | syl21anc 837 |
. . . . . . . 8
โข (๐ฅ โ โ+
โ 0 โค ((ฯโ๐ฅ) / ๐ฅ)) |
124 | 40, 123 | absidd 15369 |
. . . . . . 7
โข (๐ฅ โ โ+
โ (absโ((ฯโ๐ฅ) / ๐ฅ)) = ((ฯโ๐ฅ) / ๐ฅ)) |
125 | 95, 119, 124 | 3brtr4d 5181 |
. . . . . 6
โข (๐ฅ โ โ+
โ (absโ(ฮฃ๐
โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โค (absโ((ฯโ๐ฅ) / ๐ฅ))) |
126 | 125 | ad2antrl 727 |
. . . . 5
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (absโ(ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โค (absโ((ฯโ๐ฅ) / ๐ฅ))) |
127 | 33, 35, 42, 44, 126 | o1le 15599 |
. . . 4
โข (โค
โ (๐ฅ โ
โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โ ๐(1)) |
128 | 127 | mptru 1549 |
. . 3
โข (๐ฅ โ โ+
โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โ ๐(1) |
129 | | logfacrlim 26727 |
. . . 4
โข (๐ฅ โ โ+
โฆ ((logโ๐ฅ)
โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โ๐
1 |
130 | | rlimo1 15561 |
. . . 4
โข ((๐ฅ โ โ+
โฆ ((logโ๐ฅ)
โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โ๐ 1 โ
(๐ฅ โ
โ+ โฆ ((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โ ๐(1)) |
131 | 129, 130 | ax-mp 5 |
. . 3
โข (๐ฅ โ โ+
โฆ ((logโ๐ฅ)
โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โ ๐(1) |
132 | | o1sub 15560 |
. . 3
โข (((๐ฅ โ โ+
โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โ ๐(1) โง (๐ฅ โ โ+
โฆ ((logโ๐ฅ)
โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โ ๐(1)) โ ((๐ฅ โ โ+
โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โf โ (๐ฅ โ โ+
โฆ ((logโ๐ฅ)
โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ)))) โ ๐(1)) |
133 | 128, 131,
132 | mp2an 691 |
. 2
โข ((๐ฅ โ โ+
โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โf โ (๐ฅ โ โ+
โฆ ((logโ๐ฅ)
โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ)))) โ ๐(1) |
134 | 32, 133 | eqeltrri 2831 |
1
โข (๐ฅ โ โ+
โฆ (ฮฃ๐ โ
(1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ))) โ ๐(1) |