ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dveflem Unicode version

Theorem dveflem 12844
Description: Derivative of the exponential function at 0. The key step in the proof is eftlub 11385, 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.)
Assertion
Ref Expression
dveflem  |-  0
( CC  _D  exp ) 1

Proof of Theorem dveflem
Dummy variables  k  n  w  u  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0cn 7751 . . 3  |-  0  e.  CC
2 eqid 2137 . . . . 5  |-  ( MetOpen `  ( abs  o.  -  )
)  =  ( MetOpen `  ( abs  o.  -  )
)
32cntoptop 12691 . . . 4  |-  ( MetOpen `  ( abs  o.  -  )
)  e.  Top
4 unicntopcntop 12694 . . . . 5  |-  CC  =  U. ( MetOpen `  ( abs  o. 
-  ) )
54ntrtop 12286 . . . 4  |-  ( (
MetOpen `  ( abs  o.  -  ) )  e. 
Top  ->  ( ( int `  ( MetOpen `  ( abs  o. 
-  ) ) ) `
 CC )  =  CC )
63, 5ax-mp 5 . . 3  |-  ( ( int `  ( MetOpen `  ( abs  o.  -  )
) ) `  CC )  =  CC
71, 6eleqtrri 2213 . 2  |-  0  e.  ( ( int `  ( MetOpen
`  ( abs  o.  -  ) ) ) `
 CC )
8 ax-1cn 7706 . . 3  |-  1  e.  CC
9 1rp 9438 . . . . . 6  |-  1  e.  RR+
10 rpmincl 11002 . . . . . 6  |-  ( ( x  e.  RR+  /\  1  e.  RR+ )  -> inf ( { x ,  1 } ,  RR ,  <  )  e.  RR+ )
119, 10mpan2 421 . . . . 5  |-  ( x  e.  RR+  -> inf ( { x ,  1 } ,  RR ,  <  )  e.  RR+ )
12 breq1 3927 . . . . . . . 8  |-  ( u  =  w  ->  (
u #  0  <->  w #  0
) )
1312elrab 2835 . . . . . . 7  |-  ( w  e.  { u  e.  CC  |  u #  0 }  <->  ( w  e.  CC  /\  w #  0 ) )
14 simprl 520 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  ->  w  e.  CC )
1514subid1d 8055 . . . . . . . . . . . 12  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  -> 
( w  -  0 )  =  w )
1615fveq2d 5418 . . . . . . . . . . 11  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  -> 
( abs `  (
w  -  0 ) )  =  ( abs `  w ) )
1716breq1d 3934 . . . . . . . . . 10  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  -> 
( ( abs `  (
w  -  0 ) )  < inf ( {
x ,  1 } ,  RR ,  <  )  <-> 
( abs `  w
)  < inf ( {
x ,  1 } ,  RR ,  <  ) ) )
1814abscld 10946 . . . . . . . . . . 11  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  -> 
( abs `  w
)  e.  RR )
19 rpre 9441 . . . . . . . . . . . 12  |-  ( x  e.  RR+  ->  x  e.  RR )
2019adantr 274 . . . . . . . . . . 11  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  ->  x  e.  RR )
21 1red 7774 . . . . . . . . . . 11  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  -> 
1  e.  RR )
22 ltmininf 10999 . . . . . . . . . . 11  |-  ( ( ( abs `  w
)  e.  RR  /\  x  e.  RR  /\  1  e.  RR )  ->  (
( abs `  w
)  < inf ( {
x ,  1 } ,  RR ,  <  )  <-> 
( ( abs `  w
)  <  x  /\  ( abs `  w )  <  1 ) ) )
2318, 20, 21, 22syl3anc 1216 . . . . . . . . . 10  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  -> 
( ( abs `  w
)  < inf ( {
x ,  1 } ,  RR ,  <  )  <-> 
( ( abs `  w
)  <  x  /\  ( abs `  w )  <  1 ) ) )
2417, 23bitrd 187 . . . . . . . . 9  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  -> 
( ( abs `  (
w  -  0 ) )  < inf ( {
x ,  1 } ,  RR ,  <  )  <-> 
( ( abs `  w
)  <  x  /\  ( abs `  w )  <  1 ) ) )
25 eqid 2137 . . . . . . . . . . . . 13  |-  ( z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) )  =  ( z  e.  {
u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z
)  -  1 )  /  z ) )
26 fveq2 5414 . . . . . . . . . . . . . . 15  |-  ( z  =  w  ->  ( exp `  z )  =  ( exp `  w
) )
2726oveq1d 5782 . . . . . . . . . . . . . 14  |-  ( z  =  w  ->  (
( exp `  z
)  -  1 )  =  ( ( exp `  w )  -  1 ) )
28 id 19 . . . . . . . . . . . . . 14  |-  ( z  =  w  ->  z  =  w )
2927, 28oveq12d 5785 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
( ( exp `  z
)  -  1 )  /  z )  =  ( ( ( exp `  w )  -  1 )  /  w ) )
30 simplr 519 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  ( w  e.  CC  /\  w #  0 ) )
3130, 13sylibr 133 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  w  e.  { u  e.  CC  |  u #  0 } )
32 efcl 11359 . . . . . . . . . . . . . . . 16  |-  ( w  e.  CC  ->  ( exp `  w )  e.  CC )
33 peano2cnm 8021 . . . . . . . . . . . . . . . 16  |-  ( ( exp `  w )  e.  CC  ->  (
( exp `  w
)  -  1 )  e.  CC )
3414, 32, 333syl 17 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  -> 
( ( exp `  w
)  -  1 )  e.  CC )
35 simprr 521 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  ->  w #  0 )
3634, 14, 35divclapd 8543 . . . . . . . . . . . . . 14  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  -> 
( ( ( exp `  w )  -  1 )  /  w )  e.  CC )
3736adantr 274 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  ( (
( exp `  w
)  -  1 )  /  w )  e.  CC )
3825, 29, 31, 37fvmptd3 5507 . . . . . . . . . . . 12  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  ( (
z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) ) `  w )  =  ( ( ( exp `  w
)  -  1 )  /  w ) )
3938fvoveq1d 5789 . . . . . . . . . . 11  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  ( abs `  ( ( ( z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) ) `  w )  -  1 ) )  =  ( abs `  ( ( ( ( exp `  w
)  -  1 )  /  w )  - 
1 ) ) )
40 1cnd 7775 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  1  e.  CC )
4137, 40subcld 8066 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  ( (
( ( exp `  w
)  -  1 )  /  w )  - 
1 )  e.  CC )
4241abscld 10946 . . . . . . . . . . . 12  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  ( abs `  ( ( ( ( exp `  w )  -  1 )  /  w )  -  1 ) )  e.  RR )
43 simplrl 524 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  w  e.  CC )
4443abscld 10946 . . . . . . . . . . . 12  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  ( abs `  w )  e.  RR )
45 simpll 518 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  x  e.  RR+ )
4645rpred 9476 . . . . . . . . . . . 12  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  x  e.  RR )
47 abscl 10816 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  CC  ->  ( abs `  w )  e.  RR )
4847ad2antrr 479 . . . . . . . . . . . . . . . . 17  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( abs `  w
)  e.  RR )
4932ad2antrr 479 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( exp `  w
)  e.  CC )
50 subcl 7954 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( exp `  w
)  e.  CC  /\  1  e.  CC )  ->  ( ( exp `  w
)  -  1 )  e.  CC )
5149, 8, 50sylancl 409 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( exp `  w
)  -  1 )  e.  CC )
52 simpll 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  ->  w  e.  CC )
53 simplr 519 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  ->  w #  0 )
5451, 52, 53divclapd 8543 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( ( exp `  w )  -  1 )  /  w )  e.  CC )
55 1cnd 7775 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
1  e.  CC )
5654, 55subcld 8066 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( ( ( exp `  w )  -  1 )  /  w )  -  1 )  e.  CC )
5756abscld 10946 . . . . . . . . . . . . . . . . 17  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( abs `  (
( ( ( exp `  w )  -  1 )  /  w )  -  1 ) )  e.  RR )
5848, 57remulcld 7789 . . . . . . . . . . . . . . . 16  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( abs `  w
)  x.  ( abs `  ( ( ( ( exp `  w )  -  1 )  /  w )  -  1 ) ) )  e.  RR )
5948resqcld 10443 . . . . . . . . . . . . . . . . 17  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( abs `  w
) ^ 2 )  e.  RR )
60 3re 8787 . . . . . . . . . . . . . . . . . 18  |-  3  e.  RR
61 4nn 8876 . . . . . . . . . . . . . . . . . 18  |-  4  e.  NN
62 nndivre 8749 . . . . . . . . . . . . . . . . . 18  |-  ( ( 3  e.  RR  /\  4  e.  NN )  ->  ( 3  /  4
)  e.  RR )
6360, 61, 62mp2an 422 . . . . . . . . . . . . . . . . 17  |-  ( 3  /  4 )  e.  RR
64 remulcl 7741 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( abs `  w
) ^ 2 )  e.  RR  /\  (
3  /  4 )  e.  RR )  -> 
( ( ( abs `  w ) ^ 2 )  x.  ( 3  /  4 ) )  e.  RR )
6559, 63, 64sylancl 409 . . . . . . . . . . . . . . . 16  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( ( abs `  w ) ^ 2 )  x.  ( 3  /  4 ) )  e.  RR )
6651, 52subcld 8066 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( ( exp `  w )  -  1 )  -  w )  e.  CC )
6766, 52, 53divcanap2d 8545 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( w  x.  (
( ( ( exp `  w )  -  1 )  -  w )  /  w ) )  =  ( ( ( exp `  w )  -  1 )  -  w ) )
6851, 52, 52, 53divsubdirapd 8583 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( ( ( exp `  w )  -  1 )  -  w )  /  w
)  =  ( ( ( ( exp `  w
)  -  1 )  /  w )  -  ( w  /  w
) ) )
6952, 53dividapd 8539 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( w  /  w
)  =  1 )
7069oveq2d 5783 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( ( ( exp `  w )  -  1 )  /  w )  -  (
w  /  w ) )  =  ( ( ( ( exp `  w
)  -  1 )  /  w )  - 
1 ) )
7168, 70eqtrd 2170 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( ( ( exp `  w )  -  1 )  -  w )  /  w
)  =  ( ( ( ( exp `  w
)  -  1 )  /  w )  - 
1 ) )
7271oveq2d 5783 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( w  x.  (
( ( ( exp `  w )  -  1 )  -  w )  /  w ) )  =  ( w  x.  ( ( ( ( exp `  w )  -  1 )  /  w )  -  1 ) ) )
7349, 55, 52subsub4d 8097 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( ( exp `  w )  -  1 )  -  w )  =  ( ( exp `  w )  -  (
1  +  w ) ) )
74 addcl 7738 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 1  e.  CC  /\  w  e.  CC )  ->  ( 1  +  w
)  e.  CC )
758, 52, 74sylancr 410 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( 1  +  w
)  e.  CC )
76 2nn0 8987 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  e.  NN0
77 eqid 2137 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  NN0  |->  ( ( w ^ n )  /  ( ! `  n ) ) )  =  ( n  e. 
NN0  |->  ( ( w ^ n )  / 
( ! `  n
) ) )
7877eftlcl 11383 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( w  e.  CC  /\  2  e.  NN0 )  ->  sum_ k  e.  ( ZZ>= ` 
2 ) ( ( n  e.  NN0  |->  ( ( w ^ n )  /  ( ! `  n ) ) ) `
 k )  e.  CC )
7952, 76, 78sylancl 409 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 8772 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  =  ( 1  +  1 )
81 1nn0 8986 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  e.  NN0
82 1e0p1 9216 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  =  ( 0  +  1 )
83 0nn0 8985 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  e.  NN0
84 0cnd 7752 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
0  e.  CC )
8577efval2 11360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  e.  CC  ->  ( exp `  w )  = 
sum_ k  e.  NN0  ( ( n  e. 
NN0  |->  ( ( w ^ n )  / 
( ! `  n
) ) ) `  k ) )
8685ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( exp `  w
)  =  sum_ k  e.  NN0  ( ( n  e.  NN0  |->  ( ( w ^ n )  /  ( ! `  n ) ) ) `
 k ) )
87 nn0uz 9353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  NN0  =  ( ZZ>= `  0 )
8887sumeq1i 11125 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  sum_ k  e.  NN0  ( ( n  e.  NN0  |->  ( ( w ^ n )  /  ( ! `  n ) ) ) `
 k )  = 
sum_ k  e.  (
ZZ>= `  0 ) ( ( n  e.  NN0  |->  ( ( w ^
n )  /  ( ! `  n )
) ) `  k
)
8986, 88syl6req 2187 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  ->  sum_ k  e.  ( ZZ>= ` 
0 ) ( ( n  e.  NN0  |->  ( ( w ^ n )  /  ( ! `  n ) ) ) `
 k )  =  ( exp `  w
) )
9089oveq2d 5783 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( 0  +  sum_ k  e.  ( ZZ>= ` 
0 ) ( ( n  e.  NN0  |->  ( ( w ^ n )  /  ( ! `  n ) ) ) `
 k ) )  =  ( 0  +  ( exp `  w
) ) )
9149addid2d 7905 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( 0  +  ( exp `  w ) )  =  ( exp `  w ) )
9290, 91eqtr2d 2171 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 11388 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  e.  CC  ->  (
( w ^ 0 )  /  ( ! `
 0 ) )  =  1 )
9493ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( w ^
0 )  /  ( ! `  0 )
)  =  1 )
9594oveq2d 5783 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( 0  +  ( ( w ^ 0 )  /  ( ! `
 0 ) ) )  =  ( 0  +  1 ) )
9695, 82syl6eqr 2188 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( 0  +  ( ( w ^ 0 )  /  ( ! `
 0 ) ) )  =  1 )
9777, 82, 83, 52, 84, 92, 96efsep 11386 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 10292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  e.  CC  ->  (
w ^ 1 )  =  w )
9998ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( w ^ 1 )  =  w )
10099oveq1d 5782 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( w ^
1 )  /  ( ! `  1 )
)  =  ( w  /  ( ! ` 
1 ) ) )
101 fac1 10468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ! `
 1 )  =  1
102101oveq2i 5778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  /  ( ! ` 
1 ) )  =  ( w  /  1
)
103100, 102syl6eq 2186 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( w ^
1 )  /  ( ! `  1 )
)  =  ( w  /  1 ) )
104 div1 8456 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  CC  ->  (
w  /  1 )  =  w )
105104ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( w  /  1
)  =  w )
106103, 105eqtrd 2170 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( w ^
1 )  /  ( ! `  1 )
)  =  w )
107106oveq2d 5783 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( 1  +  ( ( w ^ 1 )  /  ( ! `
 1 ) ) )  =  ( 1  +  w ) )
10877, 80, 81, 52, 55, 97, 107efsep 11386 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( exp `  w
)  =  ( ( 1  +  w )  +  sum_ k  e.  (
ZZ>= `  2 ) ( ( n  e.  NN0  |->  ( ( w ^
n )  /  ( ! `  n )
) ) `  k
) ) )
10975, 79, 108mvrladdd 8122 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( exp `  w
)  -  ( 1  +  w ) )  =  sum_ k  e.  (
ZZ>= `  2 ) ( ( n  e.  NN0  |->  ( ( w ^
n )  /  ( ! `  n )
) ) `  k
) )
11073, 109eqtrd 2170 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( ( exp `  w )  -  1 )  -  w )  =  sum_ k  e.  (
ZZ>= `  2 ) ( ( n  e.  NN0  |->  ( ( w ^
n )  /  ( ! `  n )
) ) `  k
) )
11167, 72, 1103eqtr3d 2178 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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
) )
112111fveq2d 5418 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) ) )
11352, 56absmuld 10959 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) ) ) )
114112, 113eqtr3d 2172 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 2137 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN0  |->  ( ( ( abs `  w
) ^ n )  /  ( ! `  n ) ) )  =  ( n  e. 
NN0  |->  ( ( ( abs `  w ) ^ n )  / 
( ! `  n
) ) )
116 eqid 2137 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 8874 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  NN
118117a1i 9 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
2  e.  NN )
119 1red 7774 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
1  e.  RR )
120 simpr 109 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( abs `  w
)  <  1 )
12148, 119, 120ltled 7874 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( abs `  w
)  <_  1 )
12277, 115, 116, 118, 52, 121eftlub 11385 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) ) )
123114, 122eqbrtrrd 3947 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 8773 . . . . . . . . . . . . . . . . . . 19  |-  3  =  ( 2  +  1 )
125 fac2 10470 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ! `
 2 )  =  2
126125oveq1i 5777 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ! `  2 )  x.  2 )  =  ( 2  x.  2 )
127 2t2e4 8867 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2  x.  2 )  =  4
128126, 127eqtr2i 2159 . . . . . . . . . . . . . . . . . . 19  |-  4  =  ( ( ! `
 2 )  x.  2 )
129124, 128oveq12i 5779 . . . . . . . . . . . . . . . . . 18  |-  ( 3  /  4 )  =  ( ( 2  +  1 )  /  (
( ! `  2
)  x.  2 ) )
130129oveq2i 5778 . . . . . . . . . . . . . . . . 17  |-  ( ( ( abs `  w
) ^ 2 )  x.  ( 3  / 
4 ) )  =  ( ( ( abs `  w ) ^ 2 )  x.  ( ( 2  +  1 )  /  ( ( ! `
 2 )  x.  2 ) ) )
131123, 130breqtrrdi 3965 . . . . . . . . . . . . . . . 16  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( abs `  w
)  x.  ( abs `  ( ( ( ( exp `  w )  -  1 )  /  w )  -  1 ) ) )  <_ 
( ( ( abs `  w ) ^ 2 )  x.  ( 3  /  4 ) ) )
13263a1i 9 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( 3  /  4
)  e.  RR )
13348sqge0d 10444 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
0  <_  ( ( abs `  w ) ^
2 ) )
134 1re 7758 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR
135 3lt4 8885 . . . . . . . . . . . . . . . . . . . . . 22  |-  3  <  4
136 4cn 8791 . . . . . . . . . . . . . . . . . . . . . . 23  |-  4  e.  CC
137136mulid1i 7761 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 4  x.  1 )  =  4
138135, 137breqtrri 3950 . . . . . . . . . . . . . . . . . . . . 21  |-  3  <  ( 4  x.  1 )
139 4re 8790 . . . . . . . . . . . . . . . . . . . . . . 23  |-  4  e.  RR
140 4pos 8810 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  <  4
141139, 140pm3.2i 270 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 4  e.  RR  /\  0  <  4 )
142 ltdivmul 8627 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 3  e.  RR  /\  1  e.  RR  /\  (
4  e.  RR  /\  0  <  4 ) )  ->  ( ( 3  /  4 )  <  1  <->  3  <  (
4  x.  1 ) ) )
14360, 134, 141, 142mp3an 1315 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 3  /  4 )  <  1  <->  3  <  ( 4  x.  1 ) )
144138, 143mpbir 145 . . . . . . . . . . . . . . . . . . . 20  |-  ( 3  /  4 )  <  1
14563, 134, 144ltleii 7859 . . . . . . . . . . . . . . . . . . 19  |-  ( 3  /  4 )  <_ 
1
146145a1i 9 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( 3  /  4
)  <_  1 )
147132, 119, 59, 133, 146lemul2ad 8691 . . . . . . . . . . . . . . . . 17  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( ( abs `  w ) ^ 2 )  x.  ( 3  /  4 ) )  <_  ( ( ( abs `  w ) ^ 2 )  x.  1 ) )
14848recnd 7787 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( abs `  w
)  e.  CC )
149148sqcld 10415 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( abs `  w
) ^ 2 )  e.  CC )
150149mulid1d 7776 . . . . . . . . . . . . . . . . 17  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( ( abs `  w ) ^ 2 )  x.  1 )  =  ( ( abs `  w ) ^ 2 ) )
151147, 150breqtrd 3949 . . . . . . . . . . . . . . . 16  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( ( abs `  w ) ^ 2 )  x.  ( 3  /  4 ) )  <_  ( ( abs `  w ) ^ 2 ) )
15258, 65, 59, 131, 151letrd 7879 . . . . . . . . . . . . . . 15  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( abs `  w
)  x.  ( abs `  ( ( ( ( exp `  w )  -  1 )  /  w )  -  1 ) ) )  <_ 
( ( abs `  w
) ^ 2 ) )
153148sqvald 10414 . . . . . . . . . . . . . . 15  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( abs `  w
) ^ 2 )  =  ( ( abs `  w )  x.  ( abs `  w ) ) )
154152, 153breqtrd 3949 . . . . . . . . . . . . . 14  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( ( abs `  w
)  x.  ( abs `  ( ( ( ( exp `  w )  -  1 )  /  w )  -  1 ) ) )  <_ 
( ( abs `  w
)  x.  ( abs `  w ) ) )
155 absgt0ap 10864 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  CC  ->  (
w #  0  <->  0  <  ( abs `  w ) ) )
156155ad2antrr 479 . . . . . . . . . . . . . . . . 17  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( w #  0  <->  0  <  ( abs `  w
) ) )
15753, 156mpbid 146 . . . . . . . . . . . . . . . 16  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
0  <  ( abs `  w ) )
15848, 157elrpd 9474 . . . . . . . . . . . . . . 15  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( abs `  w
)  e.  RR+ )
15957, 48, 158lemul2d 9521 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) ) )
160154, 159mpbird 166 . . . . . . . . . . . . 13  |-  ( ( ( w  e.  CC  /\  w #  0 )  /\  ( abs `  w )  <  1 )  -> 
( abs `  (
( ( ( exp `  w )  -  1 )  /  w )  -  1 ) )  <_  ( abs `  w
) )
161160ad2ant2l 499 . . . . . . . . . . . 12  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  ( abs `  ( ( ( ( exp `  w )  -  1 )  /  w )  -  1 ) )  <_  ( abs `  w ) )
162 simprl 520 . . . . . . . . . . . 12  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  ( abs `  w )  <  x
)
16342, 44, 46, 161, 162lelttrd 7880 . . . . . . . . . . 11  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  ( abs `  ( ( ( ( exp `  w )  -  1 )  /  w )  -  1 ) )  <  x
)
16439, 163eqbrtrd 3945 . . . . . . . . . 10  |-  ( ( ( x  e.  RR+  /\  ( w  e.  CC  /\  w #  0 ) )  /\  ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 ) )  ->  ( abs `  ( ( ( z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) ) `  w )  -  1 ) )  <  x
)
165164ex 114 . . . . . . . . 9  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  -> 
( ( ( abs `  w )  <  x  /\  ( abs `  w
)  <  1 )  ->  ( abs `  (
( ( z  e. 
{ u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  /  z ) ) `  w )  -  1 ) )  <  x ) )
16624, 165sylbid 149 . . . . . . . 8  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  -> 
( ( abs `  (
w  -  0 ) )  < inf ( {
x ,  1 } ,  RR ,  <  )  ->  ( abs `  (
( ( z  e. 
{ u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  /  z ) ) `  w )  -  1 ) )  <  x ) )
167166adantld 276 . . . . . . 7  |-  ( ( x  e.  RR+  /\  (
w  e.  CC  /\  w #  0 ) )  -> 
( ( w #  0  /\  ( abs `  (
w  -  0 ) )  < inf ( {
x ,  1 } ,  RR ,  <  ) )  ->  ( abs `  ( ( ( z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) ) `  w )  -  1 ) )  <  x
) )
16813, 167sylan2b 285 . . . . . 6  |-  ( ( x  e.  RR+  /\  w  e.  { u  e.  CC  |  u #  0 }
)  ->  ( (
w #  0  /\  ( abs `  ( w  - 
0 ) )  < inf ( { x ,  1 } ,  RR ,  <  ) )  ->  ( abs `  ( ( ( z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) ) `  w )  -  1 ) )  <  x
) )
169168ralrimiva 2503 . . . . 5  |-  ( x  e.  RR+  ->  A. w  e.  { u  e.  CC  |  u #  0 } 
( ( w #  0  /\  ( abs `  (
w  -  0 ) )  < inf ( {
x ,  1 } ,  RR ,  <  ) )  ->  ( abs `  ( ( ( z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) ) `  w )  -  1 ) )  <  x
) )
170 brimralrspcev 3982 . . . . 5  |-  ( (inf ( { x ,  1 } ,  RR ,  <  )  e.  RR+  /\ 
A. w  e.  {
u  e.  CC  |  u #  0 }  ( ( w #  0  /\  ( abs `  ( w  - 
0 ) )  < inf ( { x ,  1 } ,  RR ,  <  ) )  ->  ( abs `  ( ( ( z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) ) `  w )  -  1 ) )  <  x
) )  ->  E. y  e.  RR+  A. w  e. 
{ u  e.  CC  |  u #  0 } 
( ( w #  0  /\  ( abs `  (
w  -  0 ) )  <  y )  ->  ( abs `  (
( ( z  e. 
{ u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  /  z ) ) `  w )  -  1 ) )  <  x ) )
17111, 169, 170syl2anc 408 . . . 4  |-  ( x  e.  RR+  ->  E. y  e.  RR+  A. w  e. 
{ u  e.  CC  |  u #  0 } 
( ( w #  0  /\  ( abs `  (
w  -  0 ) )  <  y )  ->  ( abs `  (
( ( z  e. 
{ u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  /  z ) ) `  w )  -  1 ) )  <  x ) )
172171rgen 2483 . . 3  |-  A. x  e.  RR+  E. y  e.  RR+  A. w  e.  {
u  e.  CC  |  u #  0 }  ( ( w #  0  /\  ( abs `  ( w  - 
0 ) )  < 
y )  ->  ( abs `  ( ( ( z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) ) `  w )  -  1 ) )  <  x
)
173 elrabi 2832 . . . . . . . . . 10  |-  ( z  e.  { u  e.  CC  |  u #  0 }  ->  z  e.  CC )
174 efcl 11359 . . . . . . . . . 10  |-  ( z  e.  CC  ->  ( exp `  z )  e.  CC )
175173, 174syl 14 . . . . . . . . 9  |-  ( z  e.  { u  e.  CC  |  u #  0 }  ->  ( exp `  z )  e.  CC )
176 1cnd 7775 . . . . . . . . 9  |-  ( z  e.  { u  e.  CC  |  u #  0 }  ->  1  e.  CC )
177175, 176subcld 8066 . . . . . . . 8  |-  ( z  e.  { u  e.  CC  |  u #  0 }  ->  ( ( exp `  z )  - 
1 )  e.  CC )
178 breq1 3927 . . . . . . . . . 10  |-  ( u  =  z  ->  (
u #  0  <->  z #  0
) )
179178elrab 2835 . . . . . . . . 9  |-  ( z  e.  { u  e.  CC  |  u #  0 }  <->  ( z  e.  CC  /\  z #  0 ) )
180179simprbi 273 . . . . . . . 8  |-  ( z  e.  { u  e.  CC  |  u #  0 }  ->  z #  0
)
181177, 173, 180divclapd 8543 . . . . . . 7  |-  ( z  e.  { u  e.  CC  |  u #  0 }  ->  ( (
( exp `  z
)  -  1 )  /  z )  e.  CC )
18225, 181fmpti 5565 . . . . . 6  |-  ( z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) ) : { u  e.  CC  |  u #  0 } --> CC
183182a1i 9 . . . . 5  |-  ( T. 
->  ( z  e.  {
u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z
)  -  1 )  /  z ) ) : { u  e.  CC  |  u #  0 } --> CC )
184 apsscn 8402 . . . . . 6  |-  { u  e.  CC  |  u #  0 }  C_  CC
185184a1i 9 . . . . 5  |-  ( T. 
->  { u  e.  CC  |  u #  0 }  C_  CC )
186 0cnd 7752 . . . . 5  |-  ( T. 
->  0  e.  CC )
187183, 185, 186ellimc3ap 12788 . . . 4  |-  ( T. 
->  ( 1  e.  ( ( z  e.  {
u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z
)  -  1 )  /  z ) ) lim
CC  0 )  <->  ( 1  e.  CC  /\  A. x  e.  RR+  E. y  e.  RR+  A. w  e. 
{ u  e.  CC  |  u #  0 } 
( ( w #  0  /\  ( abs `  (
w  -  0 ) )  <  y )  ->  ( abs `  (
( ( z  e. 
{ u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  /  z ) ) `  w )  -  1 ) )  <  x ) ) ) )
188187mptru 1340 . . 3  |-  ( 1  e.  ( ( z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) ) lim CC  0 )  <->  ( 1  e.  CC  /\  A. x  e.  RR+  E. y  e.  RR+  A. w  e. 
{ u  e.  CC  |  u #  0 } 
( ( w #  0  /\  ( abs `  (
w  -  0 ) )  <  y )  ->  ( abs `  (
( ( z  e. 
{ u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  /  z ) ) `  w )  -  1 ) )  <  x ) ) )
1898, 172, 188mpbir2an 926 . 2  |-  1  e.  ( ( z  e. 
{ u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  /  z ) ) lim CC  0 )
1902cntoptopon 12690 . . . . 5  |-  ( MetOpen `  ( abs  o.  -  )
)  e.  (TopOn `  CC )
191190toponrestid 12177 . . . 4  |-  ( MetOpen `  ( abs  o.  -  )
)  =  ( (
MetOpen `  ( abs  o.  -  ) )t  CC )
192173subid1d 8055 . . . . . . 7  |-  ( z  e.  { u  e.  CC  |  u #  0 }  ->  ( z  -  0 )  =  z )
193192oveq2d 5783 . . . . . 6  |-  ( z  e.  { u  e.  CC  |  u #  0 }  ->  ( (
( exp `  z
)  -  ( exp `  0 ) )  /  ( z  - 
0 ) )  =  ( ( ( exp `  z )  -  ( exp `  0 ) )  /  z ) )
194 ef0 11367 . . . . . . . 8  |-  ( exp `  0 )  =  1
195194oveq2i 5778 . . . . . . 7  |-  ( ( exp `  z )  -  ( exp `  0
) )  =  ( ( exp `  z
)  -  1 )
196195oveq1i 5777 . . . . . 6  |-  ( ( ( exp `  z
)  -  ( exp `  0 ) )  /  z )  =  ( ( ( exp `  z )  -  1 )  /  z )
197193, 196syl6req 2187 . . . . 5  |-  ( z  e.  { u  e.  CC  |  u #  0 }  ->  ( (
( exp `  z
)  -  1 )  /  z )  =  ( ( ( exp `  z )  -  ( exp `  0 ) )  /  ( z  - 
0 ) ) )
198197mpteq2ia 4009 . . . 4  |-  ( z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) )  =  ( z  e.  {
u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z
)  -  ( exp `  0 ) )  /  ( z  - 
0 ) ) )
199 ssidd 3113 . . . 4  |-  ( T. 
->  CC  C_  CC )
200 eff 11358 . . . . 5  |-  exp : CC
--> CC
201200a1i 9 . . . 4  |-  ( T. 
->  exp : CC --> CC )
202191, 2, 198, 199, 201, 199eldvap 12809 . . 3  |-  ( T. 
->  ( 0 ( CC 
_D  exp ) 1  <->  (
0  e.  ( ( int `  ( MetOpen `  ( abs  o.  -  )
) ) `  CC )  /\  1  e.  ( ( z  e.  {
u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z
)  -  1 )  /  z ) ) lim
CC  0 ) ) ) )
203202mptru 1340 . 2  |-  ( 0 ( CC  _D  exp ) 1  <->  ( 0  e.  ( ( int `  ( MetOpen `  ( abs  o. 
-  ) ) ) `
 CC )  /\  1  e.  ( (
z  e.  { u  e.  CC  |  u #  0 }  |->  ( ( ( exp `  z )  -  1 )  / 
z ) ) lim CC  0 ) ) )
2047, 189, 203mpbir2an 926 1  |-  0
( CC  _D  exp ) 1
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1331   T. wtru 1332    e. wcel 1480   A.wral 2414   E.wrex 2415   {crab 2418    C_ wss 3066   {cpr 3523   class class class wbr 3924    |-> cmpt 3984    o. ccom 4538   -->wf 5114   ` cfv 5118  (class class class)co 5767  infcinf 6863   CCcc 7611   RRcr 7612   0cc0 7613   1c1 7614    + caddc 7616    x. cmul 7618    < clt 7793    <_ cle 7794    - cmin 7926   # cap 8336    / cdiv 8425   NNcn 8713   2c2 8764   3c3 8765   4c4 8766   NN0cn0 8970   ZZ>=cuz 9319   RR+crp 9434   ^cexp 10285   !cfa 10464   abscabs 10762   sum_csu 11115   expce 11337   MetOpencmopn 12143   Topctop 12153   intcnt 12251   lim CC climc 12781    _D cdv 12782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-coll 4038  ax-sep 4041  ax-nul 4049  ax-pow 4093  ax-pr 4126  ax-un 4350  ax-setind 4447  ax-iinf 4497  ax-cnex 7704  ax-resscn 7705  ax-1cn 7706  ax-1re 7707  ax-icn 7708  ax-addcl 7709  ax-addrcl 7710  ax-mulcl 7711  ax-mulrcl 7712  ax-addcom 7713  ax-mulcom 7714  ax-addass 7715  ax-mulass 7716  ax-distr 7717  ax-i2m1 7718  ax-0lt1 7719  ax-1rid 7720  ax-0id 7721  ax-rnegex 7722  ax-precex 7723  ax-cnre 7724  ax-pre-ltirr 7725  ax-pre-ltwlin 7726  ax-pre-lttrn 7727  ax-pre-apti 7728  ax-pre-ltadd 7729  ax-pre-mulgt0 7730  ax-pre-mulext 7731  ax-arch 7732  ax-caucvg 7733
This theorem depends on definitions:  df-bi 116  df-stab 816  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-nel 2402  df-ral 2419  df-rex 2420  df-reu 2421  df-rmo 2422  df-rab 2423  df-v 2683  df-sbc 2905  df-csb 2999  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-if 3470  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-int 3767  df-iun 3810  df-br 3925  df-opab 3985  df-mpt 3986  df-tr 4022  df-id 4210  df-po 4213  df-iso 4214  df-iord 4283  df-on 4285  df-ilim 4286  df-suc 4288  df-iom 4500  df-xp 4540  df-rel 4541  df-cnv 4542  df-co 4543  df-dm 4544  df-rn 4545  df-res 4546  df-ima 4547  df-iota 5083  df-fun 5120  df-fn 5121  df-f 5122  df-f1 5123  df-fo 5124  df-f1o 5125  df-fv 5126  df-isom 5127  df-riota 5723  df-ov 5770  df-oprab 5771  df-mpo 5772  df-1st 6031  df-2nd 6032  df-recs 6195  df-irdg 6260  df-frec 6281  df-1o 6306  df-oadd 6310  df-er 6422  df-map 6537  df-pm 6538  df-en 6628  df-dom 6629  df-fin 6630  df-sup 6864  df-inf 6865  df-pnf 7795  df-mnf 7796  df-xr 7797  df-ltxr 7798  df-le 7799  df-sub 7928  df-neg 7929  df-reap 8330  df-ap 8337  df-div 8426  df-inn 8714  df-2 8772  df-3 8773  df-4 8774  df-n0 8971  df-z 9048  df-uz 9320  df-q 9405  df-rp 9435  df-xneg 9552  df-xadd 9553  df-ico 9670  df-fz 9784  df-fzo 9913  df-seqfrec 10212  df-exp 10286  df-fac 10465  df-ihash 10515  df-shft 10580  df-cj 10607  df-re 10608  df-im 10609  df-rsqrt 10763  df-abs 10764  df-clim 11041  df-sumdc 11116  df-ef 11343  df-rest 12111  df-topgen 12130  df-psmet 12145  df-xmet 12146  df-met 12147  df-bl 12148  df-mopn 12149  df-top 12154  df-topon 12167  df-bases 12199  df-ntr 12254  df-limced 12783  df-dvap 12784
This theorem is referenced by:  dvef  12845
  Copyright terms: Public domain W3C validator