This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reeff1olem

Description: Lemma for reeff1o . (Contributed by Paul Chapman, 18-Oct-2007) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Assertion reeff1olem 
|- ( ( U e. RR /\ 1 < U ) -> E. x e. RR ( exp ` x ) = U )

Proof

Step Hyp Ref Expression
1 ioossicc 
 |-  ( 0 (,) U ) C_ ( 0 [,] U )
2 0re 
 |-  0 e. RR
3 iccssre 
 |-  ( ( 0 e. RR /\ U e. RR ) -> ( 0 [,] U ) C_ RR )
4 2 3 mpan 
 |-  ( U e. RR -> ( 0 [,] U ) C_ RR )
5 4 adantr 
 |-  ( ( U e. RR /\ 1 < U ) -> ( 0 [,] U ) C_ RR )
6 1 5 sstrid 
 |-  ( ( U e. RR /\ 1 < U ) -> ( 0 (,) U ) C_ RR )
7 2 a1i 
 |-  ( ( U e. RR /\ 1 < U ) -> 0 e. RR )
8 simpl 
 |-  ( ( U e. RR /\ 1 < U ) -> U e. RR )
9 0lt1 
 |-  0 < 1
10 1re 
 |-  1 e. RR
11 lttr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ U e. RR ) -> ( ( 0 < 1 /\ 1 < U ) -> 0 < U ) )
12 2 10 11 mp3an12 
 |-  ( U e. RR -> ( ( 0 < 1 /\ 1 < U ) -> 0 < U ) )
13 9 12 mpani 
 |-  ( U e. RR -> ( 1 < U -> 0 < U ) )
14 13 imp 
 |-  ( ( U e. RR /\ 1 < U ) -> 0 < U )
15 ax-resscn 
 |-  RR C_ CC
16 5 15 sstrdi 
 |-  ( ( U e. RR /\ 1 < U ) -> ( 0 [,] U ) C_ CC )
17 efcn 
 |-  exp e. ( CC -cn-> CC )
18 17 a1i 
 |-  ( ( U e. RR /\ 1 < U ) -> exp e. ( CC -cn-> CC ) )
19 ssel2 
 |-  ( ( ( 0 [,] U ) C_ RR /\ y e. ( 0 [,] U ) ) -> y e. RR )
20 19 reefcld 
 |-  ( ( ( 0 [,] U ) C_ RR /\ y e. ( 0 [,] U ) ) -> ( exp ` y ) e. RR )
21 5 20 sylan 
 |-  ( ( ( U e. RR /\ 1 < U ) /\ y e. ( 0 [,] U ) ) -> ( exp ` y ) e. RR )
22 ef0 
 |-  ( exp ` 0 ) = 1
23 simpr 
 |-  ( ( U e. RR /\ 1 < U ) -> 1 < U )
24 22 23 eqbrtrid 
 |-  ( ( U e. RR /\ 1 < U ) -> ( exp ` 0 ) < U )
25 peano2re 
 |-  ( U e. RR -> ( U + 1 ) e. RR )
26 25 adantr 
 |-  ( ( U e. RR /\ 1 < U ) -> ( U + 1 ) e. RR )
27 reefcl 
 |-  ( U e. RR -> ( exp ` U ) e. RR )
28 27 adantr 
 |-  ( ( U e. RR /\ 1 < U ) -> ( exp ` U ) e. RR )
29 ltp1 
 |-  ( U e. RR -> U < ( U + 1 ) )
30 29 adantr 
 |-  ( ( U e. RR /\ 1 < U ) -> U < ( U + 1 ) )
31 8 recnd 
 |-  ( ( U e. RR /\ 1 < U ) -> U e. CC )
32 ax-1cn 
 |-  1 e. CC
33 addcom 
 |-  ( ( U e. CC /\ 1 e. CC ) -> ( U + 1 ) = ( 1 + U ) )
34 31 32 33 sylancl 
 |-  ( ( U e. RR /\ 1 < U ) -> ( U + 1 ) = ( 1 + U ) )
35 8 14 elrpd 
 |-  ( ( U e. RR /\ 1 < U ) -> U e. RR+ )
36 efgt1p 
 |-  ( U e. RR+ -> ( 1 + U ) < ( exp ` U ) )
37 35 36 syl 
 |-  ( ( U e. RR /\ 1 < U ) -> ( 1 + U ) < ( exp ` U ) )
38 34 37 eqbrtrd 
 |-  ( ( U e. RR /\ 1 < U ) -> ( U + 1 ) < ( exp ` U ) )
39 8 26 28 30 38 lttrd 
 |-  ( ( U e. RR /\ 1 < U ) -> U < ( exp ` U ) )
40 24 39 jca 
 |-  ( ( U e. RR /\ 1 < U ) -> ( ( exp ` 0 ) < U /\ U < ( exp ` U ) ) )
41 7 8 8 14 16 18 21 40 ivth 
 |-  ( ( U e. RR /\ 1 < U ) -> E. x e. ( 0 (,) U ) ( exp ` x ) = U )
42 ssrexv 
 |-  ( ( 0 (,) U ) C_ RR -> ( E. x e. ( 0 (,) U ) ( exp ` x ) = U -> E. x e. RR ( exp ` x ) = U ) )
43 6 41 42 sylc 
 |-  ( ( U e. RR /\ 1 < U ) -> E. x e. RR ( exp ` x ) = U )