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 ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 ioossicc ⊢ ( 0 (,) 𝑈 ) ⊆ ( 0 [,] 𝑈 )
2 0re ⊢ 0 ∈ ℝ
3 iccssre ⊢ ( ( 0 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 0 [,] 𝑈 ) ⊆ ℝ )
4 2 3 mpan ⊢ ( 𝑈 ∈ ℝ → ( 0 [,] 𝑈 ) ⊆ ℝ )
5 4 adantr ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ( 0 [,] 𝑈 ) ⊆ ℝ )
6 1 5 sstrid ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ( 0 (,) 𝑈 ) ⊆ ℝ )
7 2 a1i ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → 0 ∈ ℝ )
8 simpl ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → 𝑈 ∈ ℝ )
9 0lt1 ⊢ 0 < 1
10 1re ⊢ 1 ∈ ℝ
11 lttr ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( ( 0 < 1 ∧ 1 < 𝑈 ) → 0 < 𝑈 ) )
12 2 10 11 mp3an12 ⊢ ( 𝑈 ∈ ℝ → ( ( 0 < 1 ∧ 1 < 𝑈 ) → 0 < 𝑈 ) )
13 9 12 mpani ⊢ ( 𝑈 ∈ ℝ → ( 1 < 𝑈 → 0 < 𝑈 ) )
14 13 imp ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → 0 < 𝑈 )
15 ax-resscn ⊢ ℝ ⊆ ℂ
16 5 15 sstrdi ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ( 0 [,] 𝑈 ) ⊆ ℂ )
17 efcn ⊢ exp ∈ ( ℂ –cn→ ℂ )
18 17 a1i ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → exp ∈ ( ℂ –cn→ ℂ ) )
19 ssel2 ⊢ ( ( ( 0 [,] 𝑈 ) ⊆ ℝ ∧ 𝑦 ∈ ( 0 [,] 𝑈 ) ) → 𝑦 ∈ ℝ )
20 19 reefcld ⊢ ( ( ( 0 [,] 𝑈 ) ⊆ ℝ ∧ 𝑦 ∈ ( 0 [,] 𝑈 ) ) → ( exp ‘ 𝑦 ) ∈ ℝ )
21 5 20 sylan ⊢ ( ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) ∧ 𝑦 ∈ ( 0 [,] 𝑈 ) ) → ( exp ‘ 𝑦 ) ∈ ℝ )
22 ef0 ⊢ ( exp ‘ 0 ) = 1
23 simpr ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → 1 < 𝑈 )
24 22 23 eqbrtrid ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ( exp ‘ 0 ) < 𝑈 )
25 peano2re ⊢ ( 𝑈 ∈ ℝ → ( 𝑈 + 1 ) ∈ ℝ )
26 25 adantr ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ( 𝑈 + 1 ) ∈ ℝ )
27 reefcl ⊢ ( 𝑈 ∈ ℝ → ( exp ‘ 𝑈 ) ∈ ℝ )
28 27 adantr ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ( exp ‘ 𝑈 ) ∈ ℝ )
29 ltp1 ⊢ ( 𝑈 ∈ ℝ → 𝑈 < ( 𝑈 + 1 ) )
30 29 adantr ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → 𝑈 < ( 𝑈 + 1 ) )
31 8 recnd ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → 𝑈 ∈ ℂ )
32 ax-1cn ⊢ 1 ∈ ℂ
33 addcom ⊢ ( ( 𝑈 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑈 + 1 ) = ( 1 + 𝑈 ) )
34 31 32 33 sylancl ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ( 𝑈 + 1 ) = ( 1 + 𝑈 ) )
35 8 14 elrpd ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → 𝑈 ∈ ℝ+ )
36 efgt1p ⊢ ( 𝑈 ∈ ℝ+ → ( 1 + 𝑈 ) < ( exp ‘ 𝑈 ) )
37 35 36 syl ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ( 1 + 𝑈 ) < ( exp ‘ 𝑈 ) )
38 34 37 eqbrtrd ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ( 𝑈 + 1 ) < ( exp ‘ 𝑈 ) )
39 8 26 28 30 38 lttrd ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → 𝑈 < ( exp ‘ 𝑈 ) )
40 24 39 jca ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ( ( exp ‘ 0 ) < 𝑈 ∧ 𝑈 < ( exp ‘ 𝑈 ) ) )
41 7 8 8 14 16 18 21 40 ivth ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ∃ 𝑥 ∈ ( 0 (,) 𝑈 ) ( exp ‘ 𝑥 ) = 𝑈 )
42 ssrexv ⊢ ( ( 0 (,) 𝑈 ) ⊆ ℝ → ( ∃ 𝑥 ∈ ( 0 (,) 𝑈 ) ( exp ‘ 𝑥 ) = 𝑈 → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑈 ) )
43 6 41 42 sylc ⊢ ( ( 𝑈 ∈ ℝ ∧ 1 < 𝑈 ) → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑈 )