Step | Hyp | Ref
| Expression |
1 | | 0cn 7948 |
. . 3
β’ 0 β
β |
2 | | eqid 2177 |
. . . . 5
β’
(MetOpenβ(abs β β )) = (MetOpenβ(abs β
β )) |
3 | 2 | cntoptop 14003 |
. . . 4
β’
(MetOpenβ(abs β β )) β Top |
4 | | unicntopcntop 14006 |
. . . . 5
β’ β =
βͺ (MetOpenβ(abs β β
)) |
5 | 4 | ntrtop 13598 |
. . . 4
β’
((MetOpenβ(abs β β )) β Top β
((intβ(MetOpenβ(abs β β )))ββ) =
β) |
6 | 3, 5 | ax-mp 5 |
. . 3
β’
((intβ(MetOpenβ(abs β β )))ββ) =
β |
7 | 1, 6 | eleqtrri 2253 |
. 2
β’ 0 β
((intβ(MetOpenβ(abs β β
)))ββ) |
8 | | ax-1cn 7903 |
. . 3
β’ 1 β
β |
9 | | 1rp 9656 |
. . . . . 6
β’ 1 β
β+ |
10 | | rpmincl 11245 |
. . . . . 6
β’ ((π₯ β β+
β§ 1 β β+) β inf({π₯, 1}, β, < ) β
β+) |
11 | 9, 10 | mpan2 425 |
. . . . 5
β’ (π₯ β β+
β inf({π₯, 1}, β,
< ) β β+) |
12 | | breq1 4006 |
. . . . . . . 8
β’ (π’ = π€ β (π’ # 0 β π€ # 0)) |
13 | 12 | elrab 2893 |
. . . . . . 7
β’ (π€ β {π’ β β β£ π’ # 0} β (π€ β β β§ π€ # 0)) |
14 | | simprl 529 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β π€ β
β) |
15 | 14 | subid1d 8256 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β (π€ β 0) = π€) |
16 | 15 | fveq2d 5519 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β
(absβ(π€ β 0)) =
(absβπ€)) |
17 | 16 | breq1d 4013 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β
((absβ(π€ β 0))
< inf({π₯, 1}, β,
< ) β (absβπ€)
< inf({π₯, 1}, β,
< ))) |
18 | 14 | abscld 11189 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β
(absβπ€) β
β) |
19 | | rpre 9659 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β π₯ β
β) |
20 | 19 | adantr 276 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β π₯ β
β) |
21 | | 1red 7971 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β 1
β β) |
22 | | ltmininf 11242 |
. . . . . . . . . . 11
β’
(((absβπ€)
β β β§ π₯
β β β§ 1 β β) β ((absβπ€) < inf({π₯, 1}, β, < ) β
((absβπ€) < π₯ β§ (absβπ€) < 1))) |
23 | 18, 20, 21, 22 | syl3anc 1238 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β
((absβπ€) <
inf({π₯, 1}, β, < )
β ((absβπ€) <
π₯ β§ (absβπ€) < 1))) |
24 | 17, 23 | bitrd 188 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β
((absβ(π€ β 0))
< inf({π₯, 1}, β,
< ) β ((absβπ€) < π₯ β§ (absβπ€) < 1))) |
25 | | eqid 2177 |
. . . . . . . . . . . . 13
β’ (π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§)) = (π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§)) |
26 | | fveq2 5515 |
. . . . . . . . . . . . . . 15
β’ (π§ = π€ β (expβπ§) = (expβπ€)) |
27 | 26 | oveq1d 5889 |
. . . . . . . . . . . . . 14
β’ (π§ = π€ β ((expβπ§) β 1) = ((expβπ€) β 1)) |
28 | | id 19 |
. . . . . . . . . . . . . 14
β’ (π§ = π€ β π§ = π€) |
29 | 27, 28 | oveq12d 5892 |
. . . . . . . . . . . . 13
β’ (π§ = π€ β (((expβπ§) β 1) / π§) = (((expβπ€) β 1) / π€)) |
30 | | simplr 528 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β (π€ β β β§ π€ # 0)) |
31 | 30, 13 | sylibr 134 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β π€ β {π’ β β β£ π’ # 0}) |
32 | | efcl 11671 |
. . . . . . . . . . . . . . . 16
β’ (π€ β β β
(expβπ€) β
β) |
33 | | peano2cnm 8222 |
. . . . . . . . . . . . . . . 16
β’
((expβπ€)
β β β ((expβπ€) β 1) β β) |
34 | 14, 32, 33 | 3syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β
((expβπ€) β 1)
β β) |
35 | | simprr 531 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β π€ # 0) |
36 | 34, 14, 35 | divclapd 8746 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β
(((expβπ€) β 1)
/ π€) β
β) |
37 | 36 | adantr 276 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β
(((expβπ€) β 1)
/ π€) β
β) |
38 | 25, 29, 31, 37 | fvmptd3 5609 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β ((π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§))βπ€) = (((expβπ€) β 1) / π€)) |
39 | 38 | fvoveq1d 5896 |
. . . . . . . . . . 11
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β
(absβ(((π§ β
{π’ β β β£
π’ # 0} β¦
(((expβπ§) β 1)
/ π§))βπ€) β 1)) =
(absβ((((expβπ€)
β 1) / π€) β
1))) |
40 | | 1cnd 7972 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β 1 β
β) |
41 | 37, 40 | subcld 8267 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β
((((expβπ€) β 1)
/ π€) β 1) β
β) |
42 | 41 | abscld 11189 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β
(absβ((((expβπ€)
β 1) / π€) β 1))
β β) |
43 | | simplrl 535 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β π€ β
β) |
44 | 43 | abscld 11189 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β
(absβπ€) β
β) |
45 | | simpll 527 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β π₯ β
β+) |
46 | 45 | rpred 9695 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β π₯ β
β) |
47 | | abscl 11059 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β β β
(absβπ€) β
β) |
48 | 47 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(absβπ€) β
β) |
49 | 32 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(expβπ€) β
β) |
50 | | subcl 8155 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((expβπ€)
β β β§ 1 β β) β ((expβπ€) β 1) β β) |
51 | 49, 8, 50 | sylancl 413 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((expβπ€) β 1)
β β) |
52 | | simpll 527 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β π€ β
β) |
53 | | simplr 528 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β π€ # 0) |
54 | 51, 52, 53 | divclapd 8746 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(((expβπ€) β 1)
/ π€) β
β) |
55 | | 1cnd 7972 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β 1 β
β) |
56 | 54, 55 | subcld 8267 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((((expβπ€) β 1)
/ π€) β 1) β
β) |
57 | 56 | abscld 11189 |
. . . . . . . . . . . . . . . . 17
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(absβ((((expβπ€)
β 1) / π€) β 1))
β β) |
58 | 48, 57 | remulcld 7987 |
. . . . . . . . . . . . . . . 16
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((absβπ€) Β·
(absβ((((expβπ€)
β 1) / π€) β
1))) β β) |
59 | 48 | resqcld 10679 |
. . . . . . . . . . . . . . . . 17
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((absβπ€)β2)
β β) |
60 | | 3re 8992 |
. . . . . . . . . . . . . . . . . 18
β’ 3 β
β |
61 | | 4nn 9081 |
. . . . . . . . . . . . . . . . . 18
β’ 4 β
β |
62 | | nndivre 8954 |
. . . . . . . . . . . . . . . . . 18
β’ ((3
β β β§ 4 β β) β (3 / 4) β
β) |
63 | 60, 61, 62 | mp2an 426 |
. . . . . . . . . . . . . . . . 17
β’ (3 / 4)
β β |
64 | | remulcl 7938 |
. . . . . . . . . . . . . . . . 17
β’
((((absβπ€)β2) β β β§ (3 / 4) β
β) β (((absβπ€)β2) Β· (3 / 4)) β
β) |
65 | 59, 63, 64 | sylancl 413 |
. . . . . . . . . . . . . . . 16
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(((absβπ€)β2)
Β· (3 / 4)) β β) |
66 | 51, 52 | subcld 8267 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(((expβπ€) β 1)
β π€) β
β) |
67 | 66, 52, 53 | divcanap2d 8748 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (π€ Β· ((((expβπ€) β 1) β π€) / π€)) = (((expβπ€) β 1) β π€)) |
68 | 51, 52, 52, 53 | divsubdirapd 8786 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((((expβπ€) β 1)
β π€) / π€) = ((((expβπ€) β 1) / π€) β (π€ / π€))) |
69 | 52, 53 | dividapd 8742 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (π€ / π€) = 1) |
70 | 69 | oveq2d 5890 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((((expβπ€) β 1)
/ π€) β (π€ / π€)) = ((((expβπ€) β 1) / π€) β 1)) |
71 | 68, 70 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((((expβπ€) β 1)
β π€) / π€) = ((((expβπ€) β 1) / π€) β 1)) |
72 | 71 | oveq2d 5890 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (π€ Β· ((((expβπ€) β 1) β π€) / π€)) = (π€ Β· ((((expβπ€) β 1) / π€) β 1))) |
73 | 49, 55, 52 | subsub4d 8298 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(((expβπ€) β 1)
β π€) =
((expβπ€) β (1 +
π€))) |
74 | | addcl 7935 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((1
β β β§ π€
β β) β (1 + π€) β β) |
75 | 8, 52, 74 | sylancr 414 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (1 + π€) β
β) |
76 | | 2nn0 9192 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 2 β
β0 |
77 | | eqid 2177 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β0
β¦ ((π€βπ) / (!βπ))) = (π β β0 β¦ ((π€βπ) / (!βπ))) |
78 | 77 | eftlcl 11695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π€ β β β§ 2 β
β0) β Ξ£π β
(β€β₯β2)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ) β β) |
79 | 52, 76, 78 | sylancl 413 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β Ξ£π β
(β€β₯β2)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ) β β) |
80 | | df-2 8977 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 2 = (1 +
1) |
81 | | 1nn0 9191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 1 β
β0 |
82 | | 1e0p1 9424 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 1 = (0 +
1) |
83 | | 0nn0 9190 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 0 β
β0 |
84 | | 0cnd 7949 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β 0 β
β) |
85 | 77 | efval2 11672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π€ β β β
(expβπ€) =
Ξ£π β
β0 ((π
β β0 β¦ ((π€βπ) / (!βπ)))βπ)) |
86 | 85 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(expβπ€) =
Ξ£π β
β0 ((π
β β0 β¦ ((π€βπ) / (!βπ)))βπ)) |
87 | | nn0uz 9561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
β0 = (β€β₯β0) |
88 | 87 | sumeq1i 11370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
Ξ£π β
β0 ((π
β β0 β¦ ((π€βπ) / (!βπ)))βπ) = Ξ£π β
(β€β₯β0)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ) |
89 | 86, 88 | eqtr2di 2227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β Ξ£π β
(β€β₯β0)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ) = (expβπ€)) |
90 | 89 | oveq2d 5890 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (0 +
Ξ£π β
(β€β₯β0)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ)) = (0 + (expβπ€))) |
91 | 49 | addid2d 8106 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (0 +
(expβπ€)) =
(expβπ€)) |
92 | 90, 91 | eqtr2d 2211 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(expβπ€) = (0 +
Ξ£π β
(β€β₯β0)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ))) |
93 | | eft0val 11700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π€ β β β ((π€β0) / (!β0)) =
1) |
94 | 93 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β ((π€β0) / (!β0)) =
1) |
95 | 94 | oveq2d 5890 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (0 + ((π€β0) / (!β0))) = (0 +
1)) |
96 | 95, 82 | eqtr4di 2228 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (0 + ((π€β0) / (!β0))) =
1) |
97 | 77, 82, 83, 52, 84, 92, 96 | efsep 11698 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(expβπ€) = (1 +
Ξ£π β
(β€β₯β1)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ))) |
98 | | exp1 10525 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π€ β β β (π€β1) = π€) |
99 | 98 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (π€β1) = π€) |
100 | 99 | oveq1d 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β ((π€β1) / (!β1)) = (π€ /
(!β1))) |
101 | | fac1 10708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(!β1) = 1 |
102 | 101 | oveq2i 5885 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ / (!β1)) = (π€ / 1) |
103 | 100, 102 | eqtrdi 2226 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β ((π€β1) / (!β1)) = (π€ / 1)) |
104 | | div1 8659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ β β β (π€ / 1) = π€) |
105 | 104 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (π€ / 1) = π€) |
106 | 103, 105 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β ((π€β1) / (!β1)) = π€) |
107 | 106 | oveq2d 5890 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (1 + ((π€β1) / (!β1))) = (1 +
π€)) |
108 | 77, 80, 81, 52, 55, 97, 107 | efsep 11698 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(expβπ€) = ((1 + π€) + Ξ£π β
(β€β₯β2)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ))) |
109 | 75, 79, 108 | mvrladdd 8323 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((expβπ€) β (1 +
π€)) = Ξ£π β
(β€β₯β2)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ)) |
110 | 73, 109 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(((expβπ€) β 1)
β π€) = Ξ£π β
(β€β₯β2)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ)) |
111 | 67, 72, 110 | 3eqtr3d 2218 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (π€ Β· ((((expβπ€) β 1) / π€) β 1)) = Ξ£π β
(β€β₯β2)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ)) |
112 | 111 | fveq2d 5519 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(absβ(π€ Β·
((((expβπ€) β 1)
/ π€) β 1))) =
(absβΞ£π β
(β€β₯β2)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ))) |
113 | 52, 56 | absmuld 11202 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(absβ(π€ Β·
((((expβπ€) β 1)
/ π€) β 1))) =
((absβπ€) Β·
(absβ((((expβπ€)
β 1) / π€) β
1)))) |
114 | 112, 113 | eqtr3d 2212 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(absβΞ£π β
(β€β₯β2)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ)) = ((absβπ€) Β· (absβ((((expβπ€) β 1) / π€) β 1)))) |
115 | | eqid 2177 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β¦ (((absβπ€)βπ) / (!βπ))) = (π β β0 β¦
(((absβπ€)βπ) / (!βπ))) |
116 | | eqid 2177 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β¦ ((((absβπ€)β2) / (!β2)) Β· ((1 / (2 +
1))βπ))) = (π β β0
β¦ ((((absβπ€)β2) / (!β2)) Β· ((1 / (2 +
1))βπ))) |
117 | | 2nn 9079 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
118 | 117 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β 2 β
β) |
119 | | 1red 7971 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β 1 β
β) |
120 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(absβπ€) <
1) |
121 | 48, 119, 120 | ltled 8075 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(absβπ€) β€
1) |
122 | 77, 115, 116, 118, 52, 121 | eftlub 11697 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(absβΞ£π β
(β€β₯β2)((π β β0 β¦ ((π€βπ) / (!βπ)))βπ)) β€ (((absβπ€)β2) Β· ((2 + 1) / ((!β2)
Β· 2)))) |
123 | 114, 122 | eqbrtrrd 4027 |
. . . . . . . . . . . . . . . . 17
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((absβπ€) Β·
(absβ((((expβπ€)
β 1) / π€) β
1))) β€ (((absβπ€)β2) Β· ((2 + 1) / ((!β2)
Β· 2)))) |
124 | | df-3 8978 |
. . . . . . . . . . . . . . . . . . 19
β’ 3 = (2 +
1) |
125 | | fac2 10710 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(!β2) = 2 |
126 | 125 | oveq1i 5884 |
. . . . . . . . . . . . . . . . . . . 20
β’
((!β2) Β· 2) = (2 Β· 2) |
127 | | 2t2e4 9072 |
. . . . . . . . . . . . . . . . . . . 20
β’ (2
Β· 2) = 4 |
128 | 126, 127 | eqtr2i 2199 |
. . . . . . . . . . . . . . . . . . 19
β’ 4 =
((!β2) Β· 2) |
129 | 124, 128 | oveq12i 5886 |
. . . . . . . . . . . . . . . . . 18
β’ (3 / 4) =
((2 + 1) / ((!β2) Β· 2)) |
130 | 129 | oveq2i 5885 |
. . . . . . . . . . . . . . . . 17
β’
(((absβπ€)β2) Β· (3 / 4)) =
(((absβπ€)β2)
Β· ((2 + 1) / ((!β2) Β· 2))) |
131 | 123, 130 | breqtrrdi 4045 |
. . . . . . . . . . . . . . . 16
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((absβπ€) Β·
(absβ((((expβπ€)
β 1) / π€) β
1))) β€ (((absβπ€)β2) Β· (3 / 4))) |
132 | 63 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (3 / 4) β
β) |
133 | 48 | sqge0d 10680 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β 0 β€
((absβπ€)β2)) |
134 | | 1re 7955 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 β
β |
135 | | 3lt4 9090 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 3 <
4 |
136 | | 4cn 8996 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 4 β
β |
137 | 136 | mulid1i 7958 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (4
Β· 1) = 4 |
138 | 135, 137 | breqtrri 4030 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 3 < (4
Β· 1) |
139 | | 4re 8995 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 4 β
β |
140 | | 4pos 9015 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 0 <
4 |
141 | 139, 140 | pm3.2i 272 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (4 β
β β§ 0 < 4) |
142 | | ltdivmul 8832 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((3
β β β§ 1 β β β§ (4 β β β§ 0 < 4))
β ((3 / 4) < 1 β 3 < (4 Β· 1))) |
143 | 60, 134, 141, 142 | mp3an 1337 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((3 / 4)
< 1 β 3 < (4 Β· 1)) |
144 | 138, 143 | mpbir 146 |
. . . . . . . . . . . . . . . . . . . 20
β’ (3 / 4)
< 1 |
145 | 63, 134, 144 | ltleii 8059 |
. . . . . . . . . . . . . . . . . . 19
β’ (3 / 4)
β€ 1 |
146 | 145 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (3 / 4) β€
1) |
147 | 132, 119,
59, 133, 146 | lemul2ad 8896 |
. . . . . . . . . . . . . . . . 17
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(((absβπ€)β2)
Β· (3 / 4)) β€ (((absβπ€)β2) Β· 1)) |
148 | 48 | recnd 7985 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(absβπ€) β
β) |
149 | 148 | sqcld 10651 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((absβπ€)β2)
β β) |
150 | 149 | mulridd 7973 |
. . . . . . . . . . . . . . . . 17
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(((absβπ€)β2)
Β· 1) = ((absβπ€)β2)) |
151 | 147, 150 | breqtrd 4029 |
. . . . . . . . . . . . . . . 16
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(((absβπ€)β2)
Β· (3 / 4)) β€ ((absβπ€)β2)) |
152 | 58, 65, 59, 131, 151 | letrd 8080 |
. . . . . . . . . . . . . . 15
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((absβπ€) Β·
(absβ((((expβπ€)
β 1) / π€) β
1))) β€ ((absβπ€)β2)) |
153 | 148 | sqvald 10650 |
. . . . . . . . . . . . . . 15
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((absβπ€)β2) =
((absβπ€) Β·
(absβπ€))) |
154 | 152, 153 | breqtrd 4029 |
. . . . . . . . . . . . . 14
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((absβπ€) Β·
(absβ((((expβπ€)
β 1) / π€) β
1))) β€ ((absβπ€)
Β· (absβπ€))) |
155 | | absgt0ap 11107 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β β β (π€ # 0 β 0 <
(absβπ€))) |
156 | 155 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β (π€ # 0 β 0 <
(absβπ€))) |
157 | 53, 156 | mpbid 147 |
. . . . . . . . . . . . . . . 16
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β 0 <
(absβπ€)) |
158 | 48, 157 | elrpd 9692 |
. . . . . . . . . . . . . . 15
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(absβπ€) β
β+) |
159 | 57, 48, 158 | lemul2d 9740 |
. . . . . . . . . . . . . 14
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
((absβ((((expβπ€) β 1) / π€) β 1)) β€ (absβπ€) β ((absβπ€) Β·
(absβ((((expβπ€)
β 1) / π€) β
1))) β€ ((absβπ€)
Β· (absβπ€)))) |
160 | 154, 159 | mpbird 167 |
. . . . . . . . . . . . 13
β’ (((π€ β β β§ π€ # 0) β§ (absβπ€) < 1) β
(absβ((((expβπ€)
β 1) / π€) β 1))
β€ (absβπ€)) |
161 | 160 | ad2ant2l 508 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β
(absβ((((expβπ€)
β 1) / π€) β 1))
β€ (absβπ€)) |
162 | | simprl 529 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β
(absβπ€) < π₯) |
163 | 42, 44, 46, 161, 162 | lelttrd 8081 |
. . . . . . . . . . 11
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β
(absβ((((expβπ€)
β 1) / π€) β 1))
< π₯) |
164 | 39, 163 | eqbrtrd 4025 |
. . . . . . . . . 10
β’ (((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β§
((absβπ€) < π₯ β§ (absβπ€) < 1)) β
(absβ(((π§ β
{π’ β β β£
π’ # 0} β¦
(((expβπ§) β 1)
/ π§))βπ€) β 1)) < π₯) |
165 | 164 | ex 115 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β
(((absβπ€) < π₯ β§ (absβπ€) < 1) β
(absβ(((π§ β
{π’ β β β£
π’ # 0} β¦
(((expβπ§) β 1)
/ π§))βπ€) β 1)) < π₯)) |
166 | 24, 165 | sylbid 150 |
. . . . . . . 8
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β
((absβ(π€ β 0))
< inf({π₯, 1}, β,
< ) β (absβ(((π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§))βπ€) β 1)) < π₯)) |
167 | 166 | adantld 278 |
. . . . . . 7
β’ ((π₯ β β+
β§ (π€ β β
β§ π€ # 0)) β
((π€ # 0 β§
(absβ(π€ β 0))
< inf({π₯, 1}, β,
< )) β (absβ(((π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§))βπ€) β 1)) < π₯)) |
168 | 13, 167 | sylan2b 287 |
. . . . . 6
β’ ((π₯ β β+
β§ π€ β {π’ β β β£ π’ # 0}) β ((π€ # 0 β§ (absβ(π€ β 0)) < inf({π₯, 1}, β, < )) β
(absβ(((π§ β
{π’ β β β£
π’ # 0} β¦
(((expβπ§) β 1)
/ π§))βπ€) β 1)) < π₯)) |
169 | 168 | ralrimiva 2550 |
. . . . 5
β’ (π₯ β β+
β βπ€ β
{π’ β β β£
π’ # 0} ((π€ # 0 β§ (absβ(π€ β 0)) < inf({π₯, 1}, β, < )) β
(absβ(((π§ β
{π’ β β β£
π’ # 0} β¦
(((expβπ§) β 1)
/ π§))βπ€) β 1)) < π₯)) |
170 | | brimralrspcev 4062 |
. . . . 5
β’
((inf({π₯, 1},
β, < ) β β+ β§ βπ€ β {π’ β β β£ π’ # 0} ((π€ # 0 β§ (absβ(π€ β 0)) < inf({π₯, 1}, β, < )) β
(absβ(((π§ β
{π’ β β β£
π’ # 0} β¦
(((expβπ§) β 1)
/ π§))βπ€) β 1)) < π₯)) β βπ¦ β β+
βπ€ β {π’ β β β£ π’ # 0} ((π€ # 0 β§ (absβ(π€ β 0)) < π¦) β (absβ(((π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§))βπ€) β 1)) < π₯)) |
171 | 11, 169, 170 | syl2anc 411 |
. . . 4
β’ (π₯ β β+
β βπ¦ β
β+ βπ€ β {π’ β β β£ π’ # 0} ((π€ # 0 β§ (absβ(π€ β 0)) < π¦) β (absβ(((π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§))βπ€) β 1)) < π₯)) |
172 | 171 | rgen 2530 |
. . 3
β’
βπ₯ β
β+ βπ¦ β β+ βπ€ β {π’ β β β£ π’ # 0} ((π€ # 0 β§ (absβ(π€ β 0)) < π¦) β (absβ(((π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§))βπ€) β 1)) < π₯) |
173 | | elrabi 2890 |
. . . . . . . . . 10
β’ (π§ β {π’ β β β£ π’ # 0} β π§ β β) |
174 | | efcl 11671 |
. . . . . . . . . 10
β’ (π§ β β β
(expβπ§) β
β) |
175 | 173, 174 | syl 14 |
. . . . . . . . 9
β’ (π§ β {π’ β β β£ π’ # 0} β (expβπ§) β β) |
176 | | 1cnd 7972 |
. . . . . . . . 9
β’ (π§ β {π’ β β β£ π’ # 0} β 1 β
β) |
177 | 175, 176 | subcld 8267 |
. . . . . . . 8
β’ (π§ β {π’ β β β£ π’ # 0} β ((expβπ§) β 1) β β) |
178 | | breq1 4006 |
. . . . . . . . . 10
β’ (π’ = π§ β (π’ # 0 β π§ # 0)) |
179 | 178 | elrab 2893 |
. . . . . . . . 9
β’ (π§ β {π’ β β β£ π’ # 0} β (π§ β β β§ π§ # 0)) |
180 | 179 | simprbi 275 |
. . . . . . . 8
β’ (π§ β {π’ β β β£ π’ # 0} β π§ # 0) |
181 | 177, 173,
180 | divclapd 8746 |
. . . . . . 7
β’ (π§ β {π’ β β β£ π’ # 0} β (((expβπ§) β 1) / π§) β β) |
182 | 25, 181 | fmpti 5668 |
. . . . . 6
β’ (π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§)):{π’ β β β£ π’ # 0}βΆβ |
183 | 182 | a1i 9 |
. . . . 5
β’ (β€
β (π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§)):{π’ β β β£ π’ # 0}βΆβ) |
184 | | apsscn 8603 |
. . . . . 6
β’ {π’ β β β£ π’ # 0} β
β |
185 | 184 | a1i 9 |
. . . . 5
β’ (β€
β {π’ β β
β£ π’ # 0} β
β) |
186 | | 0cnd 7949 |
. . . . 5
β’ (β€
β 0 β β) |
187 | 183, 185,
186 | ellimc3ap 14100 |
. . . 4
β’ (β€
β (1 β ((π§ β
{π’ β β β£
π’ # 0} β¦
(((expβπ§) β 1)
/ π§)) limβ
0) β (1 β β β§ βπ₯ β β+ βπ¦ β β+
βπ€ β {π’ β β β£ π’ # 0} ((π€ # 0 β§ (absβ(π€ β 0)) < π¦) β (absβ(((π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§))βπ€) β 1)) < π₯)))) |
188 | 187 | mptru 1362 |
. . 3
β’ (1 β
((π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§)) limβ 0)
β (1 β β β§ βπ₯ β β+ βπ¦ β β+
βπ€ β {π’ β β β£ π’ # 0} ((π€ # 0 β§ (absβ(π€ β 0)) < π¦) β (absβ(((π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§))βπ€) β 1)) < π₯))) |
189 | 8, 172, 188 | mpbir2an 942 |
. 2
β’ 1 β
((π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§)) limβ
0) |
190 | 2 | cntoptopon 14002 |
. . . . 5
β’
(MetOpenβ(abs β β )) β
(TopOnββ) |
191 | 190 | toponrestid 13491 |
. . . 4
β’
(MetOpenβ(abs β β )) = ((MetOpenβ(abs β
β )) βΎt β) |
192 | 173 | subid1d 8256 |
. . . . . . 7
β’ (π§ β {π’ β β β£ π’ # 0} β (π§ β 0) = π§) |
193 | 192 | oveq2d 5890 |
. . . . . 6
β’ (π§ β {π’ β β β£ π’ # 0} β (((expβπ§) β (expβ0)) / (π§ β 0)) =
(((expβπ§) β
(expβ0)) / π§)) |
194 | | ef0 11679 |
. . . . . . . 8
β’
(expβ0) = 1 |
195 | 194 | oveq2i 5885 |
. . . . . . 7
β’
((expβπ§)
β (expβ0)) = ((expβπ§) β 1) |
196 | 195 | oveq1i 5884 |
. . . . . 6
β’
(((expβπ§)
β (expβ0)) / π§)
= (((expβπ§) β
1) / π§) |
197 | 193, 196 | eqtr2di 2227 |
. . . . 5
β’ (π§ β {π’ β β β£ π’ # 0} β (((expβπ§) β 1) / π§) = (((expβπ§) β (expβ0)) / (π§ β 0))) |
198 | 197 | mpteq2ia 4089 |
. . . 4
β’ (π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§)) = (π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β (expβ0)) / (π§ β 0))) |
199 | | ssidd 3176 |
. . . 4
β’ (β€
β β β β) |
200 | | eff 11670 |
. . . . 5
β’
exp:ββΆβ |
201 | 200 | a1i 9 |
. . . 4
β’ (β€
β exp:ββΆβ) |
202 | 191, 2, 198, 199, 201, 199 | eldvap 14121 |
. . 3
β’ (β€
β (0(β D exp)1 β (0 β ((intβ(MetOpenβ(abs
β β )))ββ) β§ 1 β ((π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§)) limβ
0)))) |
203 | 202 | mptru 1362 |
. 2
β’
(0(β D exp)1 β (0 β ((intβ(MetOpenβ(abs
β β )))ββ) β§ 1 β ((π§ β {π’ β β β£ π’ # 0} β¦ (((expβπ§) β 1) / π§)) limβ
0))) |
204 | 7, 189, 203 | mpbir2an 942 |
1
β’ 0(β
D exp)1 |