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 )