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 ∈ ℝ ∧ 1 < U → ∃ x ∈ ℝ e x = U

Proof

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