Proof of Theorem xrge0iifcnv
| Step | Hyp | Ref
| Expression |
| 1 | | xrge0iifhmeo.1 |
. . 3
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥))) |
| 2 | | 0xr 11308 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
| 3 | | pnfxr 11315 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
| 4 | | 0lepnf 13175 |
. . . . . . 7
⊢ 0 ≤
+∞ |
| 5 | | ubicc2 13505 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
≤ +∞) → +∞ ∈ (0[,]+∞)) |
| 6 | 2, 3, 4, 5 | mp3an 1463 |
. . . . . 6
⊢ +∞
∈ (0[,]+∞) |
| 7 | 6 | a1i 11 |
. . . . 5
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 = 0) → +∞ ∈
(0[,]+∞)) |
| 8 | | icossicc 13476 |
. . . . . 6
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
| 9 | | uncom 4158 |
. . . . . . . . . . . . . 14
⊢ ({0}
∪ (0(,]1)) = ((0(,]1) ∪ {0}) |
| 10 | | 1xr 11320 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ* |
| 11 | | 0le1 11786 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
1 |
| 12 | | snunioc 13520 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1)
→ ({0} ∪ (0(,]1)) = (0[,]1)) |
| 13 | 2, 10, 11, 12 | mp3an 1463 |
. . . . . . . . . . . . . 14
⊢ ({0}
∪ (0(,]1)) = (0[,]1) |
| 14 | 9, 13 | eqtr3i 2767 |
. . . . . . . . . . . . 13
⊢ ((0(,]1)
∪ {0}) = (0[,]1) |
| 15 | 14 | eleq2i 2833 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((0(,]1) ∪ {0})
↔ 𝑥 ∈
(0[,]1)) |
| 16 | | elun 4153 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((0(,]1) ∪ {0})
↔ (𝑥 ∈ (0(,]1)
∨ 𝑥 ∈
{0})) |
| 17 | 15, 16 | bitr3i 277 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ (0(,]1) ∨ 𝑥 ∈ {0})) |
| 18 | | pm2.53 852 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (0(,]1) ∨ 𝑥 ∈ {0}) → (¬ 𝑥 ∈ (0(,]1) → 𝑥 ∈ {0})) |
| 19 | 17, 18 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]1) → (¬
𝑥 ∈ (0(,]1) →
𝑥 ∈
{0})) |
| 20 | | elsni 4643 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {0} → 𝑥 = 0) |
| 21 | 19, 20 | syl6 35 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,]1) → (¬
𝑥 ∈ (0(,]1) →
𝑥 = 0)) |
| 22 | 21 | con1d 145 |
. . . . . . . 8
⊢ (𝑥 ∈ (0[,]1) → (¬
𝑥 = 0 → 𝑥 ∈
(0(,]1))) |
| 23 | 22 | imp 406 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 = 0) → 𝑥 ∈
(0(,]1)) |
| 24 | | 0le0 12367 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
0 |
| 25 | | 1re 11261 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
| 26 | | ltpnf 13162 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℝ → 1 < +∞) |
| 27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 1 <
+∞ |
| 28 | | iocssioo 13479 |
. . . . . . . . . . . . . 14
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
≤ 0 ∧ 1 < +∞)) → (0(,]1) ⊆
(0(,)+∞)) |
| 29 | 2, 3, 24, 27, 28 | mp4an 693 |
. . . . . . . . . . . . 13
⊢ (0(,]1)
⊆ (0(,)+∞) |
| 30 | | ioorp 13465 |
. . . . . . . . . . . . 13
⊢
(0(,)+∞) = ℝ+ |
| 31 | 29, 30 | sseqtri 4032 |
. . . . . . . . . . . 12
⊢ (0(,]1)
⊆ ℝ+ |
| 32 | 31 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0(,]1) → 𝑥 ∈
ℝ+) |
| 33 | 32 | relogcld 26665 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0(,]1) →
(log‘𝑥) ∈
ℝ) |
| 34 | 33 | renegcld 11690 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,]1) →
-(log‘𝑥) ∈
ℝ) |
| 35 | 34 | rexrd 11311 |
. . . . . . . 8
⊢ (𝑥 ∈ (0(,]1) →
-(log‘𝑥) ∈
ℝ*) |
| 36 | | elioc1 13429 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑥 ∈ (0(,]1) ↔ (𝑥 ∈ ℝ*
∧ 0 < 𝑥 ∧ 𝑥 ≤ 1))) |
| 37 | 2, 10, 36 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0(,]1) ↔ (𝑥 ∈ ℝ*
∧ 0 < 𝑥 ∧ 𝑥 ≤ 1)) |
| 38 | 37 | simp3bi 1148 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0(,]1) → 𝑥 ≤ 1) |
| 39 | | 1rp 13038 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
| 40 | 39 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0(,]1) → 1 ∈
ℝ+) |
| 41 | 32, 40 | logled 26669 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0(,]1) → (𝑥 ≤ 1 ↔ (log‘𝑥) ≤
(log‘1))) |
| 42 | 38, 41 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0(,]1) →
(log‘𝑥) ≤
(log‘1)) |
| 43 | | log1 26627 |
. . . . . . . . . 10
⊢
(log‘1) = 0 |
| 44 | 42, 43 | breqtrdi 5184 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,]1) →
(log‘𝑥) ≤
0) |
| 45 | 33 | le0neg1d 11834 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,]1) →
((log‘𝑥) ≤ 0
↔ 0 ≤ -(log‘𝑥))) |
| 46 | 44, 45 | mpbid 232 |
. . . . . . . 8
⊢ (𝑥 ∈ (0(,]1) → 0 ≤
-(log‘𝑥)) |
| 47 | | ltpnf 13162 |
. . . . . . . . 9
⊢
(-(log‘𝑥)
∈ ℝ → -(log‘𝑥) < +∞) |
| 48 | 34, 47 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (0(,]1) →
-(log‘𝑥) <
+∞) |
| 49 | | elico1 13430 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
(-(log‘𝑥) ∈
(0[,)+∞) ↔ (-(log‘𝑥) ∈ ℝ* ∧ 0 ≤
-(log‘𝑥) ∧
-(log‘𝑥) <
+∞))) |
| 50 | 2, 3, 49 | mp2an 692 |
. . . . . . . 8
⊢
(-(log‘𝑥)
∈ (0[,)+∞) ↔ (-(log‘𝑥) ∈ ℝ* ∧ 0 ≤
-(log‘𝑥) ∧
-(log‘𝑥) <
+∞)) |
| 51 | 35, 46, 48, 50 | syl3anbrc 1344 |
. . . . . . 7
⊢ (𝑥 ∈ (0(,]1) →
-(log‘𝑥) ∈
(0[,)+∞)) |
| 52 | 23, 51 | syl 17 |
. . . . . 6
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 = 0) →
-(log‘𝑥) ∈
(0[,)+∞)) |
| 53 | 8, 52 | sselid 3981 |
. . . . 5
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 = 0) →
-(log‘𝑥) ∈
(0[,]+∞)) |
| 54 | 7, 53 | ifclda 4561 |
. . . 4
⊢ (𝑥 ∈ (0[,]1) → if(𝑥 = 0, +∞,
-(log‘𝑥)) ∈
(0[,]+∞)) |
| 55 | 54 | adantl 481 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ (0[,]1)) → if(𝑥
= 0, +∞, -(log‘𝑥)) ∈ (0[,]+∞)) |
| 56 | | 0elunit 13509 |
. . . . . 6
⊢ 0 ∈
(0[,]1) |
| 57 | 56 | a1i 11 |
. . . . 5
⊢ ((𝑦 ∈ (0[,]+∞) ∧
𝑦 = +∞) → 0
∈ (0[,]1)) |
| 58 | | iocssicc 13477 |
. . . . . 6
⊢ (0(,]1)
⊆ (0[,]1) |
| 59 | | snunico 13519 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
≤ +∞) → ((0[,)+∞) ∪ {+∞}) =
(0[,]+∞)) |
| 60 | 2, 3, 4, 59 | mp3an 1463 |
. . . . . . . . . . . . 13
⊢
((0[,)+∞) ∪ {+∞}) = (0[,]+∞) |
| 61 | 60 | eleq2i 2833 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((0[,)+∞) ∪
{+∞}) ↔ 𝑦 ∈
(0[,]+∞)) |
| 62 | | elun 4153 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((0[,)+∞) ∪
{+∞}) ↔ (𝑦
∈ (0[,)+∞) ∨ 𝑦 ∈ {+∞})) |
| 63 | 61, 62 | bitr3i 277 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0[,]+∞) ↔
(𝑦 ∈ (0[,)+∞)
∨ 𝑦 ∈
{+∞})) |
| 64 | | pm2.53 852 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ (0[,)+∞) ∨
𝑦 ∈ {+∞}) →
(¬ 𝑦 ∈
(0[,)+∞) → 𝑦
∈ {+∞})) |
| 65 | 63, 64 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0[,]+∞) →
(¬ 𝑦 ∈
(0[,)+∞) → 𝑦
∈ {+∞})) |
| 66 | | elsni 4643 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {+∞} → 𝑦 = +∞) |
| 67 | 65, 66 | syl6 35 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,]+∞) →
(¬ 𝑦 ∈
(0[,)+∞) → 𝑦 =
+∞)) |
| 68 | 67 | con1d 145 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]+∞) →
(¬ 𝑦 = +∞ →
𝑦 ∈
(0[,)+∞))) |
| 69 | 68 | imp 406 |
. . . . . . 7
⊢ ((𝑦 ∈ (0[,]+∞) ∧
¬ 𝑦 = +∞) →
𝑦 ∈
(0[,)+∞)) |
| 70 | | rge0ssre 13496 |
. . . . . . . . . . . 12
⊢
(0[,)+∞) ⊆ ℝ |
| 71 | 70 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0[,)+∞) →
𝑦 ∈
ℝ) |
| 72 | 71 | renegcld 11690 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0[,)+∞) →
-𝑦 ∈
ℝ) |
| 73 | 72 | reefcld 16124 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,)+∞) →
(exp‘-𝑦) ∈
ℝ) |
| 74 | 73 | rexrd 11311 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,)+∞) →
(exp‘-𝑦) ∈
ℝ*) |
| 75 | | efgt0 16139 |
. . . . . . . . 9
⊢ (-𝑦 ∈ ℝ → 0 <
(exp‘-𝑦)) |
| 76 | 72, 75 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,)+∞) → 0
< (exp‘-𝑦)) |
| 77 | | elico1 13430 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
(𝑦 ∈ (0[,)+∞)
↔ (𝑦 ∈
ℝ* ∧ 0 ≤ 𝑦 ∧ 𝑦 < +∞))) |
| 78 | 2, 3, 77 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0[,)+∞) ↔
(𝑦 ∈
ℝ* ∧ 0 ≤ 𝑦 ∧ 𝑦 < +∞)) |
| 79 | 78 | simp2bi 1147 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0[,)+∞) → 0
≤ 𝑦) |
| 80 | 71 | le0neg2d 11835 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0[,)+∞) → (0
≤ 𝑦 ↔ -𝑦 ≤ 0)) |
| 81 | 79, 80 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0[,)+∞) →
-𝑦 ≤ 0) |
| 82 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 83 | | efle 16154 |
. . . . . . . . . . 11
⊢ ((-𝑦 ∈ ℝ ∧ 0 ∈
ℝ) → (-𝑦 ≤ 0
↔ (exp‘-𝑦) ≤
(exp‘0))) |
| 84 | 72, 82, 83 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0[,)+∞) →
(-𝑦 ≤ 0 ↔
(exp‘-𝑦) ≤
(exp‘0))) |
| 85 | 81, 84 | mpbid 232 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,)+∞) →
(exp‘-𝑦) ≤
(exp‘0)) |
| 86 | | ef0 16127 |
. . . . . . . . 9
⊢
(exp‘0) = 1 |
| 87 | 85, 86 | breqtrdi 5184 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,)+∞) →
(exp‘-𝑦) ≤
1) |
| 88 | | elioc1 13429 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ*) →
((exp‘-𝑦) ∈
(0(,]1) ↔ ((exp‘-𝑦) ∈ ℝ* ∧ 0 <
(exp‘-𝑦) ∧
(exp‘-𝑦) ≤
1))) |
| 89 | 2, 10, 88 | mp2an 692 |
. . . . . . . 8
⊢
((exp‘-𝑦)
∈ (0(,]1) ↔ ((exp‘-𝑦) ∈ ℝ* ∧ 0 <
(exp‘-𝑦) ∧
(exp‘-𝑦) ≤
1)) |
| 90 | 74, 76, 87, 89 | syl3anbrc 1344 |
. . . . . . 7
⊢ (𝑦 ∈ (0[,)+∞) →
(exp‘-𝑦) ∈
(0(,]1)) |
| 91 | 69, 90 | syl 17 |
. . . . . 6
⊢ ((𝑦 ∈ (0[,]+∞) ∧
¬ 𝑦 = +∞) →
(exp‘-𝑦) ∈
(0(,]1)) |
| 92 | 58, 91 | sselid 3981 |
. . . . 5
⊢ ((𝑦 ∈ (0[,]+∞) ∧
¬ 𝑦 = +∞) →
(exp‘-𝑦) ∈
(0[,]1)) |
| 93 | 57, 92 | ifclda 4561 |
. . . 4
⊢ (𝑦 ∈ (0[,]+∞) →
if(𝑦 = +∞, 0,
(exp‘-𝑦)) ∈
(0[,]1)) |
| 94 | 93 | adantl 481 |
. . 3
⊢
((⊤ ∧ 𝑦
∈ (0[,]+∞)) → if(𝑦 = +∞, 0, (exp‘-𝑦)) ∈
(0[,]1)) |
| 95 | | eqeq2 2749 |
. . . . . 6
⊢ (0 =
if(𝑦 = +∞, 0,
(exp‘-𝑦)) →
(𝑥 = 0 ↔ 𝑥 = if(𝑦 = +∞, 0, (exp‘-𝑦)))) |
| 96 | 95 | bibi1d 343 |
. . . . 5
⊢ (0 =
if(𝑦 = +∞, 0,
(exp‘-𝑦)) →
((𝑥 = 0 ↔ 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥))) ↔ (𝑥 = if(𝑦 = +∞, 0, (exp‘-𝑦)) ↔ 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥))))) |
| 97 | | eqeq2 2749 |
. . . . . 6
⊢
((exp‘-𝑦) =
if(𝑦 = +∞, 0,
(exp‘-𝑦)) →
(𝑥 = (exp‘-𝑦) ↔ 𝑥 = if(𝑦 = +∞, 0, (exp‘-𝑦)))) |
| 98 | 97 | bibi1d 343 |
. . . . 5
⊢
((exp‘-𝑦) =
if(𝑦 = +∞, 0,
(exp‘-𝑦)) →
((𝑥 = (exp‘-𝑦) ↔ 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥))) ↔ (𝑥 = if(𝑦 = +∞, 0, (exp‘-𝑦)) ↔ 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥))))) |
| 99 | | simpr 484 |
. . . . . . 7
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑦 = +∞) → 𝑦 = +∞) |
| 100 | | iftrue 4531 |
. . . . . . . 8
⊢ (𝑥 = 0 → if(𝑥 = 0, +∞,
-(log‘𝑥)) =
+∞) |
| 101 | 100 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑥 = 0 → (𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥)) ↔ 𝑦 = +∞)) |
| 102 | 99, 101 | syl5ibrcom 247 |
. . . . . 6
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑦 = +∞) → (𝑥 = 0 → 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥)))) |
| 103 | | ubico 32777 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → ¬ +∞
∈ (0[,)+∞)) |
| 104 | 82, 3, 103 | mp2an 692 |
. . . . . . . . . 10
⊢ ¬
+∞ ∈ (0[,)+∞) |
| 105 | 104 | nelir 3049 |
. . . . . . . . 9
⊢ +∞
∉ (0[,)+∞) |
| 106 | | neleq1 3052 |
. . . . . . . . . 10
⊢ (𝑦 = +∞ → (𝑦 ∉ (0[,)+∞) ↔
+∞ ∉ (0[,)+∞))) |
| 107 | 106 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑦 = +∞) → (𝑦 ∉ (0[,)+∞) ↔
+∞ ∉ (0[,)+∞))) |
| 108 | 105, 107 | mpbiri 258 |
. . . . . . . 8
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑦 = +∞) → 𝑦 ∉
(0[,)+∞)) |
| 109 | | neleq1 3052 |
. . . . . . . 8
⊢ (𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥)) → (𝑦 ∉ (0[,)+∞) ↔ if(𝑥 = 0, +∞,
-(log‘𝑥)) ∉
(0[,)+∞))) |
| 110 | 108, 109 | syl5ibcom 245 |
. . . . . . 7
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑦 = +∞) → (𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥)) → if(𝑥 = 0, +∞, -(log‘𝑥)) ∉
(0[,)+∞))) |
| 111 | | df-nel 3047 |
. . . . . . . 8
⊢ (if(𝑥 = 0, +∞,
-(log‘𝑥)) ∉
(0[,)+∞) ↔ ¬ if(𝑥 = 0, +∞, -(log‘𝑥)) ∈
(0[,)+∞)) |
| 112 | | iffalse 4534 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 = 0 → if(𝑥 = 0, +∞,
-(log‘𝑥)) =
-(log‘𝑥)) |
| 113 | 112 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 = 0) → if(𝑥 = 0, +∞,
-(log‘𝑥)) =
-(log‘𝑥)) |
| 114 | 113, 52 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 = 0) → if(𝑥 = 0, +∞,
-(log‘𝑥)) ∈
(0[,)+∞)) |
| 115 | 114 | ex 412 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]1) → (¬
𝑥 = 0 → if(𝑥 = 0, +∞,
-(log‘𝑥)) ∈
(0[,)+∞))) |
| 116 | 115 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑦 = +∞) → (¬
𝑥 = 0 → if(𝑥 = 0, +∞,
-(log‘𝑥)) ∈
(0[,)+∞))) |
| 117 | 116 | con1d 145 |
. . . . . . . 8
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑦 = +∞) → (¬
if(𝑥 = 0, +∞,
-(log‘𝑥)) ∈
(0[,)+∞) → 𝑥 =
0)) |
| 118 | 111, 117 | biimtrid 242 |
. . . . . . 7
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑦 = +∞) →
(if(𝑥 = 0, +∞,
-(log‘𝑥)) ∉
(0[,)+∞) → 𝑥 =
0)) |
| 119 | 110, 118 | syld 47 |
. . . . . 6
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑦 = +∞) → (𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥)) → 𝑥 = 0)) |
| 120 | 102, 119 | impbid 212 |
. . . . 5
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑦 = +∞) → (𝑥 = 0 ↔ 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥)))) |
| 121 | | eqeq2 2749 |
. . . . . . 7
⊢ (+∞
= if(𝑥 = 0, +∞,
-(log‘𝑥)) →
(𝑦 = +∞ ↔ 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥)))) |
| 122 | 121 | bibi2d 342 |
. . . . . 6
⊢ (+∞
= if(𝑥 = 0, +∞,
-(log‘𝑥)) →
((𝑥 = (exp‘-𝑦) ↔ 𝑦 = +∞) ↔ (𝑥 = (exp‘-𝑦) ↔ 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥))))) |
| 123 | | eqeq2 2749 |
. . . . . . 7
⊢
(-(log‘𝑥) =
if(𝑥 = 0, +∞,
-(log‘𝑥)) →
(𝑦 = -(log‘𝑥) ↔ 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥)))) |
| 124 | 123 | bibi2d 342 |
. . . . . 6
⊢
(-(log‘𝑥) =
if(𝑥 = 0, +∞,
-(log‘𝑥)) →
((𝑥 = (exp‘-𝑦) ↔ 𝑦 = -(log‘𝑥)) ↔ (𝑥 = (exp‘-𝑦) ↔ 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥))))) |
| 125 | 82 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ (0[,]+∞) ∧
¬ 𝑦 = +∞) →
0 ∈ ℝ) |
| 126 | 69, 76 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ (0[,]+∞) ∧
¬ 𝑦 = +∞) →
0 < (exp‘-𝑦)) |
| 127 | 125, 126 | ltned 11397 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ (0[,]+∞) ∧
¬ 𝑦 = +∞) →
0 ≠ (exp‘-𝑦)) |
| 128 | 127 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
¬ 𝑦 = +∞) →
0 ≠ (exp‘-𝑦)) |
| 129 | 128 | neneqd 2945 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
¬ 𝑦 = +∞) →
¬ 0 = (exp‘-𝑦)) |
| 130 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (𝑥 = (exp‘-𝑦) ↔ 0 = (exp‘-𝑦))) |
| 131 | 130 | notbid 318 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (¬ 𝑥 = (exp‘-𝑦) ↔ ¬ 0 =
(exp‘-𝑦))) |
| 132 | 129, 131 | syl5ibrcom 247 |
. . . . . . . 8
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
¬ 𝑦 = +∞) →
(𝑥 = 0 → ¬ 𝑥 = (exp‘-𝑦))) |
| 133 | 132 | imp 406 |
. . . . . . 7
⊢ ((((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
¬ 𝑦 = +∞) ∧
𝑥 = 0) → ¬ 𝑥 = (exp‘-𝑦)) |
| 134 | | simplr 769 |
. . . . . . 7
⊢ ((((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
¬ 𝑦 = +∞) ∧
𝑥 = 0) → ¬ 𝑦 = +∞) |
| 135 | 133, 134 | 2falsed 376 |
. . . . . 6
⊢ ((((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
¬ 𝑦 = +∞) ∧
𝑥 = 0) → (𝑥 = (exp‘-𝑦) ↔ 𝑦 = +∞)) |
| 136 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (𝑥 = (exp‘-𝑦) ↔ (exp‘-𝑦) = 𝑥) |
| 137 | 136 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (0(,]1) ∧ 𝑦 ∈ (0[,)+∞)) →
(𝑥 = (exp‘-𝑦) ↔ (exp‘-𝑦) = 𝑥)) |
| 138 | | relogeftb 26626 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ -𝑦 ∈ ℝ)
→ ((log‘𝑥) =
-𝑦 ↔ (exp‘-𝑦) = 𝑥)) |
| 139 | 32, 72, 138 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (0(,]1) ∧ 𝑦 ∈ (0[,)+∞)) →
((log‘𝑥) = -𝑦 ↔ (exp‘-𝑦) = 𝑥)) |
| 140 | 33 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0(,]1) →
(log‘𝑥) ∈
ℂ) |
| 141 | 71 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0[,)+∞) →
𝑦 ∈
ℂ) |
| 142 | | negcon2 11562 |
. . . . . . . . . . 11
⊢
(((log‘𝑥)
∈ ℂ ∧ 𝑦
∈ ℂ) → ((log‘𝑥) = -𝑦 ↔ 𝑦 = -(log‘𝑥))) |
| 143 | 140, 141,
142 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (0(,]1) ∧ 𝑦 ∈ (0[,)+∞)) →
((log‘𝑥) = -𝑦 ↔ 𝑦 = -(log‘𝑥))) |
| 144 | 137, 139,
143 | 3bitr2d 307 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (0(,]1) ∧ 𝑦 ∈ (0[,)+∞)) →
(𝑥 = (exp‘-𝑦) ↔ 𝑦 = -(log‘𝑥))) |
| 145 | 23, 69, 144 | syl2an 596 |
. . . . . . . 8
⊢ (((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 = 0) ∧ (𝑦 ∈ (0[,]+∞) ∧
¬ 𝑦 = +∞)) →
(𝑥 = (exp‘-𝑦) ↔ 𝑦 = -(log‘𝑥))) |
| 146 | 145 | an4s 660 |
. . . . . . 7
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
(¬ 𝑥 = 0 ∧ ¬
𝑦 = +∞)) →
(𝑥 = (exp‘-𝑦) ↔ 𝑦 = -(log‘𝑥))) |
| 147 | 146 | anass1rs 655 |
. . . . . 6
⊢ ((((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
¬ 𝑦 = +∞) ∧
¬ 𝑥 = 0) → (𝑥 = (exp‘-𝑦) ↔ 𝑦 = -(log‘𝑥))) |
| 148 | 122, 124,
135, 147 | ifbothda 4564 |
. . . . 5
⊢ (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧
¬ 𝑦 = +∞) →
(𝑥 = (exp‘-𝑦) ↔ 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥)))) |
| 149 | 96, 98, 120, 148 | ifbothda 4564 |
. . . 4
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) →
(𝑥 = if(𝑦 = +∞, 0, (exp‘-𝑦)) ↔ 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥)))) |
| 150 | 149 | adantl 481 |
. . 3
⊢
((⊤ ∧ (𝑥
∈ (0[,]1) ∧ 𝑦
∈ (0[,]+∞))) → (𝑥 = if(𝑦 = +∞, 0, (exp‘-𝑦)) ↔ 𝑦 = if(𝑥 = 0, +∞, -(log‘𝑥)))) |
| 151 | 1, 55, 94, 150 | f1ocnv2d 7686 |
. 2
⊢ (⊤
→ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 0,
(exp‘-𝑦))))) |
| 152 | 151 | mptru 1547 |
1
⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 0,
(exp‘-𝑦)))) |