Step | Hyp | Ref
| Expression |
1 | | nn0uz 12810 |
. . 3
โข
โ0 = (โคโฅโ0) |
2 | | 0zd 12516 |
. . 3
โข (๐ โ 0 โ
โค) |
3 | | eqid 2733 |
. . . . 5
โข (๐ โ โ0
โฆ ((๐ดโ๐) / (!โ๐))) = (๐ โ โ0 โฆ ((๐ดโ๐) / (!โ๐))) |
4 | 3 | eftval 15964 |
. . . 4
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ ((๐ดโ๐) / (!โ๐)))โ๐) = ((๐ดโ๐) / (!โ๐))) |
5 | 4 | adantl 483 |
. . 3
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((๐ดโ๐) / (!โ๐)))โ๐) = ((๐ดโ๐) / (!โ๐))) |
6 | | eflegeo.1 |
. . . 4
โข (๐ โ ๐ด โ โ) |
7 | | reeftcl 15962 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐ดโ๐) / (!โ๐)) โ โ) |
8 | 6, 7 | sylan 581 |
. . 3
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ๐) / (!โ๐)) โ โ) |
9 | | oveq2 7366 |
. . . . 5
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
10 | | eqid 2733 |
. . . . 5
โข (๐ โ โ0
โฆ (๐ดโ๐)) = (๐ โ โ0 โฆ (๐ดโ๐)) |
11 | | ovex 7391 |
. . . . 5
โข (๐ดโ๐) โ V |
12 | 9, 10, 11 | fvmpt 6949 |
. . . 4
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ (๐ดโ๐))โ๐) = (๐ดโ๐)) |
13 | 12 | adantl 483 |
. . 3
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ (๐ดโ๐))โ๐) = (๐ดโ๐)) |
14 | | reexpcl 13990 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
15 | 6, 14 | sylan 581 |
. . 3
โข ((๐ โง ๐ โ โ0) โ (๐ดโ๐) โ โ) |
16 | | faccl 14189 |
. . . . . . 7
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
17 | 16 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
โ) |
18 | 17 | nnred 12173 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
โ) |
19 | 6 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ๐ด โ
โ) |
20 | | simpr 486 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ0) |
21 | | eflegeo.2 |
. . . . . . 7
โข (๐ โ 0 โค ๐ด) |
22 | 21 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ 0 โค
๐ด) |
23 | 19, 20, 22 | expge0d 14075 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ 0 โค
(๐ดโ๐)) |
24 | 17 | nnge1d 12206 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ 1 โค
(!โ๐)) |
25 | 15, 18, 23, 24 | lemulge12d 12098 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ (๐ดโ๐) โค ((!โ๐) ยท (๐ดโ๐))) |
26 | 17 | nngt0d 12207 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ 0 <
(!โ๐)) |
27 | | ledivmul 12036 |
. . . . 5
โข (((๐ดโ๐) โ โ โง (๐ดโ๐) โ โ โง ((!โ๐) โ โ โง 0 <
(!โ๐))) โ
(((๐ดโ๐) / (!โ๐)) โค (๐ดโ๐) โ (๐ดโ๐) โค ((!โ๐) ยท (๐ดโ๐)))) |
28 | 15, 15, 18, 26, 27 | syl112anc 1375 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ (((๐ดโ๐) / (!โ๐)) โค (๐ดโ๐) โ (๐ดโ๐) โค ((!โ๐) ยท (๐ดโ๐)))) |
29 | 25, 28 | mpbird 257 |
. . 3
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ๐) / (!โ๐)) โค (๐ดโ๐)) |
30 | 6 | recnd 11188 |
. . . 4
โข (๐ โ ๐ด โ โ) |
31 | 3 | efcllem 15965 |
. . . 4
โข (๐ด โ โ โ seq0( + ,
(๐ โ
โ0 โฆ ((๐ดโ๐) / (!โ๐)))) โ dom โ ) |
32 | 30, 31 | syl 17 |
. . 3
โข (๐ โ seq0( + , (๐ โ โ0
โฆ ((๐ดโ๐) / (!โ๐)))) โ dom โ ) |
33 | 6, 21 | absidd 15313 |
. . . . . 6
โข (๐ โ (absโ๐ด) = ๐ด) |
34 | | eflegeo.3 |
. . . . . 6
โข (๐ โ ๐ด < 1) |
35 | 33, 34 | eqbrtrd 5128 |
. . . . 5
โข (๐ โ (absโ๐ด) < 1) |
36 | 30, 35, 13 | geolim 15760 |
. . . 4
โข (๐ โ seq0( + , (๐ โ โ0
โฆ (๐ดโ๐))) โ (1 / (1 โ
๐ด))) |
37 | | seqex 13914 |
. . . . 5
โข seq0( + ,
(๐ โ
โ0 โฆ (๐ดโ๐))) โ V |
38 | | ovex 7391 |
. . . . 5
โข (1 / (1
โ ๐ด)) โ
V |
39 | 37, 38 | breldm 5865 |
. . . 4
โข (seq0( +
, (๐ โ
โ0 โฆ (๐ดโ๐))) โ (1 / (1 โ ๐ด)) โ seq0( + , (๐ โ โ0 โฆ (๐ดโ๐))) โ dom โ ) |
40 | 36, 39 | syl 17 |
. . 3
โข (๐ โ seq0( + , (๐ โ โ0
โฆ (๐ดโ๐))) โ dom โ
) |
41 | 1, 2, 5, 8, 13, 15, 29, 32, 40 | isumle 15734 |
. 2
โข (๐ โ ฮฃ๐ โ โ0 ((๐ดโ๐) / (!โ๐)) โค ฮฃ๐ โ โ0 (๐ดโ๐)) |
42 | | efval 15967 |
. . 3
โข (๐ด โ โ โ
(expโ๐ด) =
ฮฃ๐ โ
โ0 ((๐ดโ๐) / (!โ๐))) |
43 | 30, 42 | syl 17 |
. 2
โข (๐ โ (expโ๐ด) = ฮฃ๐ โ โ0 ((๐ดโ๐) / (!โ๐))) |
44 | | expcl 13991 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
45 | 30, 44 | sylan 581 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ (๐ดโ๐) โ โ) |
46 | 1, 2, 13, 45, 36 | isumclim 15647 |
. . 3
โข (๐ โ ฮฃ๐ โ โ0 (๐ดโ๐) = (1 / (1 โ ๐ด))) |
47 | 46 | eqcomd 2739 |
. 2
โข (๐ โ (1 / (1 โ ๐ด)) = ฮฃ๐ โ โ0 (๐ดโ๐)) |
48 | 41, 43, 47 | 3brtr4d 5138 |
1
โข (๐ โ (expโ๐ด) โค (1 / (1 โ ๐ด))) |