Step | Hyp | Ref
| Expression |
1 | | ere 11544 |
. . . . 5
⊢ e ∈
ℝ |
2 | 1 | a1i 9 |
. . . 4
⊢ (𝑈 ∈ (0(,)e) → e ∈
ℝ) |
3 | | elioore 9794 |
. . . 4
⊢ (𝑈 ∈ (0(,)e) → 𝑈 ∈
ℝ) |
4 | | 0xr 7903 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
5 | 1 | rexri 7914 |
. . . . . . 7
⊢ e ∈
ℝ* |
6 | | elioo2 9803 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ e ∈ ℝ*) → (𝑈 ∈ (0(,)e) ↔ (𝑈 ∈ ℝ ∧ 0 <
𝑈 ∧ 𝑈 < e))) |
7 | 4, 5, 6 | mp2an 423 |
. . . . . 6
⊢ (𝑈 ∈ (0(,)e) ↔ (𝑈 ∈ ℝ ∧ 0 <
𝑈 ∧ 𝑈 < e)) |
8 | 7 | simp2bi 998 |
. . . . 5
⊢ (𝑈 ∈ (0(,)e) → 0 <
𝑈) |
9 | 3, 8 | gt0ap0d 8483 |
. . . 4
⊢ (𝑈 ∈ (0(,)e) → 𝑈 # 0) |
10 | 2, 3, 9 | redivclapd 8686 |
. . 3
⊢ (𝑈 ∈ (0(,)e) → (e /
𝑈) ∈
ℝ) |
11 | 3 | recnd 7885 |
. . . . . 6
⊢ (𝑈 ∈ (0(,)e) → 𝑈 ∈
ℂ) |
12 | 11 | mulid2d 7875 |
. . . . 5
⊢ (𝑈 ∈ (0(,)e) → (1
· 𝑈) = 𝑈) |
13 | 7 | simp3bi 999 |
. . . . 5
⊢ (𝑈 ∈ (0(,)e) → 𝑈 < e) |
14 | 12, 13 | eqbrtrd 3982 |
. . . 4
⊢ (𝑈 ∈ (0(,)e) → (1
· 𝑈) <
e) |
15 | | 1red 7872 |
. . . . 5
⊢ (𝑈 ∈ (0(,)e) → 1 ∈
ℝ) |
16 | | ltmuldiv 8724 |
. . . . 5
⊢ ((1
∈ ℝ ∧ e ∈ ℝ ∧ (𝑈 ∈ ℝ ∧ 0 < 𝑈)) → ((1 · 𝑈) < e ↔ 1 < (e /
𝑈))) |
17 | 15, 2, 3, 8, 16 | syl112anc 1221 |
. . . 4
⊢ (𝑈 ∈ (0(,)e) → ((1
· 𝑈) < e ↔ 1
< (e / 𝑈))) |
18 | 14, 17 | mpbid 146 |
. . 3
⊢ (𝑈 ∈ (0(,)e) → 1 < (e
/ 𝑈)) |
19 | | reeff1olem 13031 |
. . 3
⊢ (((e /
𝑈) ∈ ℝ ∧ 1
< (e / 𝑈)) →
∃𝑦 ∈ ℝ
(exp‘𝑦) = (e / 𝑈)) |
20 | 10, 18, 19 | syl2anc 409 |
. 2
⊢ (𝑈 ∈ (0(,)e) →
∃𝑦 ∈ ℝ
(exp‘𝑦) = (e / 𝑈)) |
21 | | 1red 7872 |
. . . 4
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → 1 ∈
ℝ) |
22 | | simprl 521 |
. . . 4
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → 𝑦 ∈ ℝ) |
23 | 21, 22 | resubcld 8235 |
. . 3
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → (1 − 𝑦) ∈
ℝ) |
24 | | 1cnd 7873 |
. . . . 5
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → 1 ∈
ℂ) |
25 | 22 | recnd 7885 |
. . . . 5
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → 𝑦 ∈ ℂ) |
26 | | efsub 11555 |
. . . . 5
⊢ ((1
∈ ℂ ∧ 𝑦
∈ ℂ) → (exp‘(1 − 𝑦)) = ((exp‘1) / (exp‘𝑦))) |
27 | 24, 25, 26 | syl2anc 409 |
. . . 4
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → (exp‘(1 −
𝑦)) = ((exp‘1) /
(exp‘𝑦))) |
28 | | simprr 522 |
. . . . . . 7
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → (exp‘𝑦) = (e / 𝑈)) |
29 | | df-e 11523 |
. . . . . . . 8
⊢ e =
(exp‘1) |
30 | 29 | oveq1i 5824 |
. . . . . . 7
⊢ (e /
𝑈) = ((exp‘1) / 𝑈) |
31 | 28, 30 | eqtr2di 2204 |
. . . . . 6
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → ((exp‘1) /
𝑈) = (exp‘𝑦)) |
32 | | efcl 11538 |
. . . . . . . 8
⊢ (1 ∈
ℂ → (exp‘1) ∈ ℂ) |
33 | 24, 32 | syl 14 |
. . . . . . 7
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → (exp‘1) ∈
ℂ) |
34 | | efcl 11538 |
. . . . . . . 8
⊢ (𝑦 ∈ ℂ →
(exp‘𝑦) ∈
ℂ) |
35 | 25, 34 | syl 14 |
. . . . . . 7
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → (exp‘𝑦) ∈
ℂ) |
36 | 11 | adantr 274 |
. . . . . . 7
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → 𝑈 ∈ ℂ) |
37 | 9 | adantr 274 |
. . . . . . 7
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → 𝑈 # 0) |
38 | 33, 35, 36, 37 | divmulap2d 8676 |
. . . . . 6
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → (((exp‘1) /
𝑈) = (exp‘𝑦) ↔ (exp‘1) = (𝑈 · (exp‘𝑦)))) |
39 | 31, 38 | mpbid 146 |
. . . . 5
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → (exp‘1) =
(𝑈 ·
(exp‘𝑦))) |
40 | 22 | rpefcld 11560 |
. . . . . . 7
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → (exp‘𝑦) ∈
ℝ+) |
41 | 40 | rpap0d 9587 |
. . . . . 6
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → (exp‘𝑦) # 0) |
42 | 33, 36, 35, 41 | divmulap3d 8677 |
. . . . 5
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → (((exp‘1) /
(exp‘𝑦)) = 𝑈 ↔ (exp‘1) = (𝑈 · (exp‘𝑦)))) |
43 | 39, 42 | mpbird 166 |
. . . 4
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → ((exp‘1) /
(exp‘𝑦)) = 𝑈) |
44 | 27, 43 | eqtrd 2187 |
. . 3
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → (exp‘(1 −
𝑦)) = 𝑈) |
45 | | fveqeq2 5470 |
. . . 4
⊢ (𝑥 = (1 − 𝑦) → ((exp‘𝑥) = 𝑈 ↔ (exp‘(1 − 𝑦)) = 𝑈)) |
46 | 45 | rspcev 2813 |
. . 3
⊢ (((1
− 𝑦) ∈ ℝ
∧ (exp‘(1 − 𝑦)) = 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈) |
47 | 23, 44, 46 | syl2anc 409 |
. 2
⊢ ((𝑈 ∈ (0(,)e) ∧ (𝑦 ∈ ℝ ∧
(exp‘𝑦) = (e / 𝑈))) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈) |
48 | 20, 47 | rexlimddv 2576 |
1
⊢ (𝑈 ∈ (0(,)e) →
∃𝑥 ∈ ℝ
(exp‘𝑥) = 𝑈) |