Step | Hyp | Ref
| Expression |
1 | | iooref1o.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (1 / (1 +
(exp‘𝑥)))) |
2 | | 1rp 9542 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
3 | 2 | a1i 9 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → 1 ∈
ℝ+) |
4 | | rpefcl 11559 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
(exp‘𝑥) ∈
ℝ+) |
5 | 3, 4 | rpaddcld 9597 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → (1 +
(exp‘𝑥)) ∈
ℝ+) |
6 | 5 | rpreccld 9592 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → (1 / (1 +
(exp‘𝑥))) ∈
ℝ+) |
7 | 6 | rpred 9581 |
. . . . 5
⊢ (𝑥 ∈ ℝ → (1 / (1 +
(exp‘𝑥))) ∈
ℝ) |
8 | 6 | rpgt0d 9584 |
. . . . 5
⊢ (𝑥 ∈ ℝ → 0 < (1
/ (1 + (exp‘𝑥)))) |
9 | | 1red 7872 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → 1 ∈
ℝ) |
10 | 9, 4 | ltaddrpd 9615 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → 1 < (1
+ (exp‘𝑥))) |
11 | 5 | recgt1d 9596 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → (1 <
(1 + (exp‘𝑥)) ↔
(1 / (1 + (exp‘𝑥)))
< 1)) |
12 | 10, 11 | mpbid 146 |
. . . . 5
⊢ (𝑥 ∈ ℝ → (1 / (1 +
(exp‘𝑥))) <
1) |
13 | | 0xr 7903 |
. . . . . 6
⊢ 0 ∈
ℝ* |
14 | | 1re 7856 |
. . . . . . 7
⊢ 1 ∈
ℝ |
15 | 14 | rexri 7914 |
. . . . . 6
⊢ 1 ∈
ℝ* |
16 | | elioo2 9803 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ*) → ((1 / (1
+ (exp‘𝑥))) ∈
(0(,)1) ↔ ((1 / (1 + (exp‘𝑥))) ∈ ℝ ∧ 0 < (1 / (1 +
(exp‘𝑥))) ∧ (1 /
(1 + (exp‘𝑥))) <
1))) |
17 | 13, 15, 16 | mp2an 423 |
. . . . 5
⊢ ((1 / (1
+ (exp‘𝑥))) ∈
(0(,)1) ↔ ((1 / (1 + (exp‘𝑥))) ∈ ℝ ∧ 0 < (1 / (1 +
(exp‘𝑥))) ∧ (1 /
(1 + (exp‘𝑥))) <
1)) |
18 | 7, 8, 12, 17 | syl3anbrc 1166 |
. . . 4
⊢ (𝑥 ∈ ℝ → (1 / (1 +
(exp‘𝑥))) ∈
(0(,)1)) |
19 | 18 | adantl 275 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (1 / (1 + (exp‘𝑥))) ∈ (0(,)1)) |
20 | | elioore 9794 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0(,)1) → 𝑦 ∈
ℝ) |
21 | | eliooord 9810 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0(,)1) → (0 <
𝑦 ∧ 𝑦 < 1)) |
22 | 21 | simpld 111 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0(,)1) → 0 <
𝑦) |
23 | 20, 22 | elrpd 9578 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0(,)1) → 𝑦 ∈
ℝ+) |
24 | 23 | rpreccld 9592 |
. . . . . . . 8
⊢ (𝑦 ∈ (0(,)1) → (1 /
𝑦) ∈
ℝ+) |
25 | 24 | rpred 9581 |
. . . . . . 7
⊢ (𝑦 ∈ (0(,)1) → (1 /
𝑦) ∈
ℝ) |
26 | | 1red 7872 |
. . . . . . 7
⊢ (𝑦 ∈ (0(,)1) → 1 ∈
ℝ) |
27 | 25, 26 | resubcld 8235 |
. . . . . 6
⊢ (𝑦 ∈ (0(,)1) → ((1 /
𝑦) − 1) ∈
ℝ) |
28 | 21 | simprd 113 |
. . . . . . . 8
⊢ (𝑦 ∈ (0(,)1) → 𝑦 < 1) |
29 | 23 | reclt1d 9595 |
. . . . . . . 8
⊢ (𝑦 ∈ (0(,)1) → (𝑦 < 1 ↔ 1 < (1 / 𝑦))) |
30 | 28, 29 | mpbid 146 |
. . . . . . 7
⊢ (𝑦 ∈ (0(,)1) → 1 < (1
/ 𝑦)) |
31 | 26, 25 | posdifd 8386 |
. . . . . . 7
⊢ (𝑦 ∈ (0(,)1) → (1 <
(1 / 𝑦) ↔ 0 < ((1 /
𝑦) −
1))) |
32 | 30, 31 | mpbid 146 |
. . . . . 6
⊢ (𝑦 ∈ (0(,)1) → 0 <
((1 / 𝑦) −
1)) |
33 | 27, 32 | elrpd 9578 |
. . . . 5
⊢ (𝑦 ∈ (0(,)1) → ((1 /
𝑦) − 1) ∈
ℝ+) |
34 | 33 | relogcld 13142 |
. . . 4
⊢ (𝑦 ∈ (0(,)1) →
(log‘((1 / 𝑦) −
1)) ∈ ℝ) |
35 | 34 | adantl 275 |
. . 3
⊢
((⊤ ∧ 𝑦
∈ (0(,)1)) → (log‘((1 / 𝑦) − 1)) ∈
ℝ) |
36 | | 1cnd 7873 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → 1 ∈
ℂ) |
37 | 4 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) →
(exp‘𝑥) ∈
ℝ+) |
38 | 37 | rpcnd 9583 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) →
(exp‘𝑥) ∈
ℂ) |
39 | 36, 38 | addcld 7876 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → (1 +
(exp‘𝑥)) ∈
ℂ) |
40 | 23 | adantl 275 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → 𝑦 ∈
ℝ+) |
41 | 40 | rpcnd 9583 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → 𝑦 ∈
ℂ) |
42 | 40 | rpap0d 9587 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → 𝑦 # 0) |
43 | 36, 39, 41, 42 | divmulap2d 8676 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → ((1 /
𝑦) = (1 + (exp‘𝑥)) ↔ 1 = (𝑦 · (1 + (exp‘𝑥))))) |
44 | 24 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → (1 /
𝑦) ∈
ℝ+) |
45 | 44 | rpcnd 9583 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → (1 /
𝑦) ∈
ℂ) |
46 | 36, 38, 45 | addrsub 8225 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → ((1 +
(exp‘𝑥)) = (1 / 𝑦) ↔ (exp‘𝑥) = ((1 / 𝑦) − 1))) |
47 | 33 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → ((1 /
𝑦) − 1) ∈
ℝ+) |
48 | 47 | reeflogd 13143 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) →
(exp‘(log‘((1 / 𝑦) − 1))) = ((1 / 𝑦) − 1)) |
49 | 48 | eqeq2d 2166 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) →
((exp‘𝑥) =
(exp‘(log‘((1 / 𝑦) − 1))) ↔ (exp‘𝑥) = ((1 / 𝑦) − 1))) |
50 | | reef11 11573 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧
(log‘((1 / 𝑦) −
1)) ∈ ℝ) → ((exp‘𝑥) = (exp‘(log‘((1 / 𝑦) − 1))) ↔ 𝑥 = (log‘((1 / 𝑦) − 1)))) |
51 | 34, 50 | sylan2 284 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) →
((exp‘𝑥) =
(exp‘(log‘((1 / 𝑦) − 1))) ↔ 𝑥 = (log‘((1 / 𝑦) − 1)))) |
52 | 46, 49, 51 | 3bitr2rd 216 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → (𝑥 = (log‘((1 / 𝑦) − 1)) ↔ (1 +
(exp‘𝑥)) = (1 / 𝑦))) |
53 | | eqcom 2156 |
. . . . . . 7
⊢ ((1 +
(exp‘𝑥)) = (1 / 𝑦) ↔ (1 / 𝑦) = (1 + (exp‘𝑥))) |
54 | 52, 53 | bitrdi 195 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → (𝑥 = (log‘((1 / 𝑦) − 1)) ↔ (1 / 𝑦) = (1 + (exp‘𝑥)))) |
55 | 5 | adantr 274 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → (1 +
(exp‘𝑥)) ∈
ℝ+) |
56 | 55 | rpap0d 9587 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → (1 +
(exp‘𝑥)) #
0) |
57 | 36, 41, 39, 56 | divmulap3d 8677 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → ((1 / (1
+ (exp‘𝑥))) = 𝑦 ↔ 1 = (𝑦 · (1 + (exp‘𝑥))))) |
58 | 43, 54, 57 | 3bitr4d 219 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → (𝑥 = (log‘((1 / 𝑦) − 1)) ↔ (1 / (1 +
(exp‘𝑥))) = 𝑦)) |
59 | | eqcom 2156 |
. . . . 5
⊢ ((1 / (1
+ (exp‘𝑥))) = 𝑦 ↔ 𝑦 = (1 / (1 + (exp‘𝑥)))) |
60 | 58, 59 | bitrdi 195 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ (0(,)1)) → (𝑥 = (log‘((1 / 𝑦) − 1)) ↔ 𝑦 = (1 / (1 + (exp‘𝑥))))) |
61 | 60 | adantl 275 |
. . 3
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 𝑦
∈ (0(,)1))) → (𝑥
= (log‘((1 / 𝑦)
− 1)) ↔ 𝑦 = (1 /
(1 + (exp‘𝑥))))) |
62 | 1, 19, 35, 61 | f1o2d 6015 |
. 2
⊢ (⊤
→ 𝐹:ℝ–1-1-onto→(0(,)1)) |
63 | 62 | mptru 1341 |
1
⊢ 𝐹:ℝ–1-1-onto→(0(,)1) |