Metamath Proof Explorer

Theorem dveflem

Description: Derivative of the exponential function at 0. The key step in the proof is eftlub , to show that abs ( exp ( x ) - 1 - x ) <_ abs ( x ) ^ 2 x. ( 3 / 4 ) . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016)

Ref Expression
Assertion dveflem 
|- 0 ( CC _D exp ) 1

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 2 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
4 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
5 4 ntrtop 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( int ` ( TopOpen ` CCfld ) ) ` CC ) = CC )
6 3 5 ax-mp 
 |-  ( ( int ` ( TopOpen ` CCfld ) ) ` CC ) = CC
7 1 6 eleqtrri 
 |-  0 e. ( ( int ` ( TopOpen ` CCfld ) ) ` CC )
8 ax-1cn 
 |-  1 e. CC
9 1rp 
 |-  1 e. RR+
10 ifcl 
 |-  ( ( x e. RR+ /\ 1 e. RR+ ) -> if ( x <_ 1 , x , 1 ) e. RR+ )
11 9 10 mpan2 
 |-  ( x e. RR+ -> if ( x <_ 1 , x , 1 ) e. RR+ )
12 eldifsn 
 |-  ( w e. ( CC \ { 0 } ) <-> ( w e. CC /\ w =/= 0 ) )
13 simprl 
 |-  ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) -> w e. CC )
14 13 subid1d 
 |-  ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) -> ( w - 0 ) = w )
15 14 fveq2d 
 |-  ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) -> ( abs ` ( w - 0 ) ) = ( abs ` w ) )
16 15 breq1d 
 |-  ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) -> ( ( abs ` ( w - 0 ) ) < if ( x <_ 1 , x , 1 ) <-> ( abs ` w ) < if ( x <_ 1 , x , 1 ) ) )
17 13 abscld 
 |-  ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) -> ( abs ` w ) e. RR )
18 rpre 
 |-  ( x e. RR+ -> x e. RR )
19 18 adantr 
 |-  ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) -> x e. RR )
20 1red 
 |-  ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) -> 1 e. RR )
21 ltmin 
 |-  ( ( ( abs ` w ) e. RR /\ x e. RR /\ 1 e. RR ) -> ( ( abs ` w ) < if ( x <_ 1 , x , 1 ) <-> ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) )
22 17 19 20 21 syl3anc 
 |-  ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) -> ( ( abs ` w ) < if ( x <_ 1 , x , 1 ) <-> ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) )
23 16 22 bitrd 
 |-  ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) -> ( ( abs ` ( w - 0 ) ) < if ( x <_ 1 , x , 1 ) <-> ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) )
24 simplr 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( w e. CC /\ w =/= 0 ) )
25 24 12 sylibr 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> w e. ( CC \ { 0 } ) )
26 fveq2 
 |-  ( z = w -> ( exp ` z ) = ( exp ` w ) )
27 26 oveq1d 
 |-  ( z = w -> ( ( exp ` z ) - 1 ) = ( ( exp ` w ) - 1 ) )
28 id 
 |-  ( z = w -> z = w )
29 27 28 oveq12d 
 |-  ( z = w -> ( ( ( exp ` z ) - 1 ) / z ) = ( ( ( exp ` w ) - 1 ) / w ) )
30 eqid 
 |-  ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) = ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) )
31 ovex 
 |-  ( ( ( exp ` w ) - 1 ) / w ) e. _V
32 29 30 31 fvmpt 
 |-  ( w e. ( CC \ { 0 } ) -> ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) = ( ( ( exp ` w ) - 1 ) / w ) )
33 25 32 syl 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) = ( ( ( exp ` w ) - 1 ) / w ) )
34 33 fvoveq1d 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) = ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) )
35 simplrl 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> w e. CC )
36 efcl 
 |-  ( w e. CC -> ( exp ` w ) e. CC )
37 35 36 syl 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( exp ` w ) e. CC )
38 1cnd 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> 1 e. CC )
39 37 38 subcld 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( ( exp ` w ) - 1 ) e. CC )
40 simplrr 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> w =/= 0 )
41 39 35 40 divcld 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( ( ( exp ` w ) - 1 ) / w ) e. CC )
42 41 38 subcld 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) e. CC )
43 42 abscld 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) e. RR )
44 35 abscld 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( abs ` w ) e. RR )
45 simpll 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> x e. RR+ )
46 45 rpred 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> x e. RR )
47 abscl 
 |-  ( w e. CC -> ( abs ` w ) e. RR )
48 47 ad2antrr 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( abs ` w ) e. RR )
49 36 ad2antrr 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( exp ` w ) e. CC )
50 subcl 
 |-  ( ( ( exp ` w ) e. CC /\ 1 e. CC ) -> ( ( exp ` w ) - 1 ) e. CC )
51 49 8 50 sylancl 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( exp ` w ) - 1 ) e. CC )
52 simpll 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> w e. CC )
53 simplr 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> w =/= 0 )
54 51 52 53 divcld 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( ( exp ` w ) - 1 ) / w ) e. CC )
55 1cnd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> 1 e. CC )
56 54 55 subcld 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) e. CC )
57 56 abscld 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) e. RR )
58 48 57 remulcld 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( abs ` w ) x. ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) ) e. RR )
59 48 resqcld 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( abs ` w ) ^ 2 ) e. RR )
60 3re 
 |-  3 e. RR
61 4nn 
 |-  4 e. NN
62 nndivre 
 |-  ( ( 3 e. RR /\ 4 e. NN ) -> ( 3 / 4 ) e. RR )
63 60 61 62 mp2an 
 |-  ( 3 / 4 ) e. RR
64 remulcl 
 |-  ( ( ( ( abs ` w ) ^ 2 ) e. RR /\ ( 3 / 4 ) e. RR ) -> ( ( ( abs ` w ) ^ 2 ) x. ( 3 / 4 ) ) e. RR )
65 59 63 64 sylancl 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( ( abs ` w ) ^ 2 ) x. ( 3 / 4 ) ) e. RR )
66 51 52 subcld 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( ( exp ` w ) - 1 ) - w ) e. CC )
67 66 52 53 divcan2d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( w x. ( ( ( ( exp ` w ) - 1 ) - w ) / w ) ) = ( ( ( exp ` w ) - 1 ) - w ) )
68 51 52 52 53 divsubdird 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( ( ( exp ` w ) - 1 ) - w ) / w ) = ( ( ( ( exp ` w ) - 1 ) / w ) - ( w / w ) ) )
69 52 53 dividd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( w / w ) = 1 )
70 69 oveq2d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( ( ( exp ` w ) - 1 ) / w ) - ( w / w ) ) = ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) )
71 68 70 eqtrd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( ( ( exp ` w ) - 1 ) - w ) / w ) = ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) )
72 71 oveq2d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( w x. ( ( ( ( exp ` w ) - 1 ) - w ) / w ) ) = ( w x. ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) )
73 49 55 52 subsub4d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( ( exp ` w ) - 1 ) - w ) = ( ( exp ` w ) - ( 1 + w ) ) )
74 addcl 
 |-  ( ( 1 e. CC /\ w e. CC ) -> ( 1 + w ) e. CC )
75 8 52 74 sylancr 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( 1 + w ) e. CC )
76 2nn0 
 |-  2 e. NN0
77 eqid 
 |-  ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) )
78 77 eftlcl 
 |-  ( ( w e. CC /\ 2 e. NN0 ) -> sum_ k e. ( ZZ>= ` 2 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) e. CC )
79 52 76 78 sylancl 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> sum_ k e. ( ZZ>= ` 2 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) e. CC )
80 df-2 
 |-  2 = ( 1 + 1 )
81 1nn0 
 |-  1 e. NN0
82 1e0p1 
 |-  1 = ( 0 + 1 )
83 0nn0 
 |-  0 e. NN0
84 0cnd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> 0 e. CC )
85 77 efval2 
 |-  ( w e. CC -> ( exp ` w ) = sum_ k e. NN0 ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) )
86 85 ad2antrr 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( exp ` w ) = sum_ k e. NN0 ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) )
87 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
88 87 sumeq1i 
 |-  sum_ k e. NN0 ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) = sum_ k e. ( ZZ>= ` 0 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k )
89 86 88 eqtr2di 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> sum_ k e. ( ZZ>= ` 0 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) = ( exp ` w ) )
90 89 oveq2d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( 0 + sum_ k e. ( ZZ>= ` 0 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) ) = ( 0 + ( exp ` w ) ) )
91 49 addid2d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( 0 + ( exp ` w ) ) = ( exp ` w ) )
92 90 91 eqtr2d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( exp ` w ) = ( 0 + sum_ k e. ( ZZ>= ` 0 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) ) )
93 eft0val 
 |-  ( w e. CC -> ( ( w ^ 0 ) / ( ! ` 0 ) ) = 1 )
94 93 ad2antrr 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( w ^ 0 ) / ( ! ` 0 ) ) = 1 )
95 94 oveq2d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( 0 + ( ( w ^ 0 ) / ( ! ` 0 ) ) ) = ( 0 + 1 ) )
96 95 82 eqtr4di 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( 0 + ( ( w ^ 0 ) / ( ! ` 0 ) ) ) = 1 )
97 77 82 83 52 84 92 96 efsep 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( exp ` w ) = ( 1 + sum_ k e. ( ZZ>= ` 1 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) ) )
98 exp1 
 |-  ( w e. CC -> ( w ^ 1 ) = w )
99 98 ad2antrr 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( w ^ 1 ) = w )
100 99 oveq1d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( w ^ 1 ) / ( ! ` 1 ) ) = ( w / ( ! ` 1 ) ) )
101 fac1 
 |-  ( ! ` 1 ) = 1
102 101 oveq2i 
 |-  ( w / ( ! ` 1 ) ) = ( w / 1 )
103 100 102 eqtrdi 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( w ^ 1 ) / ( ! ` 1 ) ) = ( w / 1 ) )
104 div1 
 |-  ( w e. CC -> ( w / 1 ) = w )
105 104 ad2antrr 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( w / 1 ) = w )
106 103 105 eqtrd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( w ^ 1 ) / ( ! ` 1 ) ) = w )
107 106 oveq2d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( 1 + ( ( w ^ 1 ) / ( ! ` 1 ) ) ) = ( 1 + w ) )
108 77 80 81 52 55 97 107 efsep 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( exp ` w ) = ( ( 1 + w ) + sum_ k e. ( ZZ>= ` 2 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) ) )
109 75 79 108 mvrladdd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( exp ` w ) - ( 1 + w ) ) = sum_ k e. ( ZZ>= ` 2 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) )
110 73 109 eqtrd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( ( exp ` w ) - 1 ) - w ) = sum_ k e. ( ZZ>= ` 2 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) )
111 67 72 110 3eqtr3d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( w x. ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) = sum_ k e. ( ZZ>= ` 2 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) )
112 111 fveq2d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( abs ` ( w x. ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) ) = ( abs ` sum_ k e. ( ZZ>= ` 2 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) ) )
113 52 56 absmuld 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( abs ` ( w x. ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) ) = ( ( abs ` w ) x. ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) ) )
114 112 113 eqtr3d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 2 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) ) = ( ( abs ` w ) x. ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) ) )
115 eqid 
 |-  ( n e. NN0 |-> ( ( ( abs ` w ) ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( ( abs ` w ) ^ n ) / ( ! ` n ) ) )
116 eqid 
 |-  ( n e. NN0 |-> ( ( ( ( abs ` w ) ^ 2 ) / ( ! ` 2 ) ) x. ( ( 1 / ( 2 + 1 ) ) ^ n ) ) ) = ( n e. NN0 |-> ( ( ( ( abs ` w ) ^ 2 ) / ( ! ` 2 ) ) x. ( ( 1 / ( 2 + 1 ) ) ^ n ) ) )
117 2nn 
 |-  2 e. NN
118 117 a1i 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> 2 e. NN )
119 1red 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> 1 e. RR )
120 simpr 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( abs ` w ) < 1 )
121 48 119 120 ltled 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( abs ` w ) <_ 1 )
122 77 115 116 118 52 121 eftlub 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 2 ) ( ( n e. NN0 |-> ( ( w ^ n ) / ( ! ` n ) ) ) ` k ) ) <_ ( ( ( abs ` w ) ^ 2 ) x. ( ( 2 + 1 ) / ( ( ! ` 2 ) x. 2 ) ) ) )
123 114 122 eqbrtrrd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( abs ` w ) x. ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) ) <_ ( ( ( abs ` w ) ^ 2 ) x. ( ( 2 + 1 ) / ( ( ! ` 2 ) x. 2 ) ) ) )
124 df-3 
 |-  3 = ( 2 + 1 )
125 fac2 
 |-  ( ! ` 2 ) = 2
126 125 oveq1i 
 |-  ( ( ! ` 2 ) x. 2 ) = ( 2 x. 2 )
127 2t2e4 
 |-  ( 2 x. 2 ) = 4
128 126 127 eqtr2i 
 |-  4 = ( ( ! ` 2 ) x. 2 )
129 124 128 oveq12i 
 |-  ( 3 / 4 ) = ( ( 2 + 1 ) / ( ( ! ` 2 ) x. 2 ) )
130 129 oveq2i 
 |-  ( ( ( abs ` w ) ^ 2 ) x. ( 3 / 4 ) ) = ( ( ( abs ` w ) ^ 2 ) x. ( ( 2 + 1 ) / ( ( ! ` 2 ) x. 2 ) ) )
131 123 130 breqtrrdi 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( abs ` w ) x. ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) ) <_ ( ( ( abs ` w ) ^ 2 ) x. ( 3 / 4 ) ) )
132 63 a1i 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( 3 / 4 ) e. RR )
133 48 sqge0d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> 0 <_ ( ( abs ` w ) ^ 2 ) )
134 1re 
 |-  1 e. RR
135 3lt4 
 |-  3 < 4
136 4cn 
 |-  4 e. CC
137 136 mulid1i 
 |-  ( 4 x. 1 ) = 4
138 135 137 breqtrri 
 |-  3 < ( 4 x. 1 )
139 4re 
 |-  4 e. RR
140 4pos 
 |-  0 < 4
141 139 140 pm3.2i 
 |-  ( 4 e. RR /\ 0 < 4 )
142 ltdivmul 
 |-  ( ( 3 e. RR /\ 1 e. RR /\ ( 4 e. RR /\ 0 < 4 ) ) -> ( ( 3 / 4 ) < 1 <-> 3 < ( 4 x. 1 ) ) )
143 60 134 141 142 mp3an 
 |-  ( ( 3 / 4 ) < 1 <-> 3 < ( 4 x. 1 ) )
144 138 143 mpbir 
 |-  ( 3 / 4 ) < 1
145 63 134 144 ltleii 
 |-  ( 3 / 4 ) <_ 1
146 145 a1i 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( 3 / 4 ) <_ 1 )
147 132 119 59 133 146 lemul2ad 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( ( abs ` w ) ^ 2 ) x. ( 3 / 4 ) ) <_ ( ( ( abs ` w ) ^ 2 ) x. 1 ) )
148 48 recnd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( abs ` w ) e. CC )
149 148 sqcld 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( abs ` w ) ^ 2 ) e. CC )
150 149 mulid1d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( ( abs ` w ) ^ 2 ) x. 1 ) = ( ( abs ` w ) ^ 2 ) )
151 147 150 breqtrd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( ( abs ` w ) ^ 2 ) x. ( 3 / 4 ) ) <_ ( ( abs ` w ) ^ 2 ) )
152 58 65 59 131 151 letrd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( abs ` w ) x. ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) ) <_ ( ( abs ` w ) ^ 2 ) )
153 148 sqvald 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( abs ` w ) ^ 2 ) = ( ( abs ` w ) x. ( abs ` w ) ) )
154 152 153 breqtrd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( abs ` w ) x. ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) ) <_ ( ( abs ` w ) x. ( abs ` w ) ) )
155 absgt0 
 |-  ( w e. CC -> ( w =/= 0 <-> 0 < ( abs ` w ) ) )
156 155 ad2antrr 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( w =/= 0 <-> 0 < ( abs ` w ) ) )
157 53 156 mpbid 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> 0 < ( abs ` w ) )
158 48 157 elrpd 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( abs ` w ) e. RR+ )
159 57 48 158 lemul2d 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) <_ ( abs ` w ) <-> ( ( abs ` w ) x. ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) ) <_ ( ( abs ` w ) x. ( abs ` w ) ) ) )
160 154 159 mpbird 
 |-  ( ( ( w e. CC /\ w =/= 0 ) /\ ( abs ` w ) < 1 ) -> ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) <_ ( abs ` w ) )
161 160 ad2ant2l 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) <_ ( abs ` w ) )
162 simprl 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( abs ` w ) < x )
163 43 44 46 161 162 lelttrd 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( abs ` ( ( ( ( exp ` w ) - 1 ) / w ) - 1 ) ) < x )
164 34 163 eqbrtrd 
 |-  ( ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) /\ ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) < x )
165 164 ex 
 |-  ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) -> ( ( ( abs ` w ) < x /\ ( abs ` w ) < 1 ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) < x ) )
166 23 165 sylbid 
 |-  ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) -> ( ( abs ` ( w - 0 ) ) < if ( x <_ 1 , x , 1 ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) < x ) )
167 166 adantld 
 |-  ( ( x e. RR+ /\ ( w e. CC /\ w =/= 0 ) ) -> ( ( w =/= 0 /\ ( abs ` ( w - 0 ) ) < if ( x <_ 1 , x , 1 ) ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) < x ) )
168 12 167 sylan2b 
 |-  ( ( x e. RR+ /\ w e. ( CC \ { 0 } ) ) -> ( ( w =/= 0 /\ ( abs ` ( w - 0 ) ) < if ( x <_ 1 , x , 1 ) ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) < x ) )
169 168 ralrimiva 
 |-  ( x e. RR+ -> A. w e. ( CC \ { 0 } ) ( ( w =/= 0 /\ ( abs ` ( w - 0 ) ) < if ( x <_ 1 , x , 1 ) ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) < x ) )
170 brimralrspcev 
 |-  ( ( if ( x <_ 1 , x , 1 ) e. RR+ /\ A. w e. ( CC \ { 0 } ) ( ( w =/= 0 /\ ( abs ` ( w - 0 ) ) < if ( x <_ 1 , x , 1 ) ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) < x ) ) -> E. y e. RR+ A. w e. ( CC \ { 0 } ) ( ( w =/= 0 /\ ( abs ` ( w - 0 ) ) < y ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) < x ) )
171 11 169 170 syl2anc 
 |-  ( x e. RR+ -> E. y e. RR+ A. w e. ( CC \ { 0 } ) ( ( w =/= 0 /\ ( abs ` ( w - 0 ) ) < y ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) < x ) )
172 171 rgen 
 |-  A. x e. RR+ E. y e. RR+ A. w e. ( CC \ { 0 } ) ( ( w =/= 0 /\ ( abs ` ( w - 0 ) ) < y ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) < x )
173 eldifi 
 |-  ( z e. ( CC \ { 0 } ) -> z e. CC )
174 efcl 
 |-  ( z e. CC -> ( exp ` z ) e. CC )
175 173 174 syl 
 |-  ( z e. ( CC \ { 0 } ) -> ( exp ` z ) e. CC )
176 1cnd 
 |-  ( z e. ( CC \ { 0 } ) -> 1 e. CC )
177 175 176 subcld 
 |-  ( z e. ( CC \ { 0 } ) -> ( ( exp ` z ) - 1 ) e. CC )
178 eldifsni 
 |-  ( z e. ( CC \ { 0 } ) -> z =/= 0 )
179 177 173 178 divcld 
 |-  ( z e. ( CC \ { 0 } ) -> ( ( ( exp ` z ) - 1 ) / z ) e. CC )
180 30 179 fmpti 
 |-  ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) : ( CC \ { 0 } ) --> CC
181 180 a1i 
 |-  ( T. -> ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) : ( CC \ { 0 } ) --> CC )
182 difssd 
 |-  ( T. -> ( CC \ { 0 } ) C_ CC )
183 0cnd 
 |-  ( T. -> 0 e. CC )
184 181 182 183 ellimc3 
 |-  ( T. -> ( 1 e. ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) limCC 0 ) <-> ( 1 e. CC /\ A. x e. RR+ E. y e. RR+ A. w e. ( CC \ { 0 } ) ( ( w =/= 0 /\ ( abs ` ( w - 0 ) ) < y ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) < x ) ) ) )
185 184 mptru 
 |-  ( 1 e. ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) limCC 0 ) <-> ( 1 e. CC /\ A. x e. RR+ E. y e. RR+ A. w e. ( CC \ { 0 } ) ( ( w =/= 0 /\ ( abs ` ( w - 0 ) ) < y ) -> ( abs ` ( ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) ` w ) - 1 ) ) < x ) ) )
186 8 172 185 mpbir2an 
 |-  1 e. ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) limCC 0 )
187 2 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
188 187 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
189 173 subid1d 
 |-  ( z e. ( CC \ { 0 } ) -> ( z - 0 ) = z )
190 189 oveq2d 
 |-  ( z e. ( CC \ { 0 } ) -> ( ( ( exp ` z ) - ( exp ` 0 ) ) / ( z - 0 ) ) = ( ( ( exp ` z ) - ( exp ` 0 ) ) / z ) )
191 ef0 
 |-  ( exp ` 0 ) = 1
192 191 oveq2i 
 |-  ( ( exp ` z ) - ( exp ` 0 ) ) = ( ( exp ` z ) - 1 )
193 192 oveq1i 
 |-  ( ( ( exp ` z ) - ( exp ` 0 ) ) / z ) = ( ( ( exp ` z ) - 1 ) / z )
194 190 193 eqtr2di 
 |-  ( z e. ( CC \ { 0 } ) -> ( ( ( exp ` z ) - 1 ) / z ) = ( ( ( exp ` z ) - ( exp ` 0 ) ) / ( z - 0 ) ) )
195 194 mpteq2ia 
 |-  ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) = ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - ( exp ` 0 ) ) / ( z - 0 ) ) )
196 ssidd 
 |-  ( T. -> CC C_ CC )
197 eff 
 |-  exp : CC --> CC
198 197 a1i 
 |-  ( T. -> exp : CC --> CC )
199 188 2 195 196 198 196 eldv 
 |-  ( T. -> ( 0 ( CC _D exp ) 1 <-> ( 0 e. ( ( int ` ( TopOpen ` CCfld ) ) ` CC ) /\ 1 e. ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) limCC 0 ) ) ) )
200 199 mptru 
 |-  ( 0 ( CC _D exp ) 1 <-> ( 0 e. ( ( int ` ( TopOpen ` CCfld ) ) ` CC ) /\ 1 e. ( ( z e. ( CC \ { 0 } ) |-> ( ( ( exp ` z ) - 1 ) / z ) ) limCC 0 ) ) )
201 7 186 200 mpbir2an 
 |-  0 ( CC _D exp ) 1