| Step |
Hyp |
Ref |
Expression |
| 1 |
|
xrge0iifhmeo.1 |
⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) |
| 2 |
|
0xr |
⊢ 0 ∈ ℝ* |
| 3 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
| 4 |
|
0lepnf |
⊢ 0 ≤ +∞ |
| 5 |
|
ubicc2 |
⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞ ) → +∞ ∈ ( 0 [,] +∞ ) ) |
| 6 |
2 3 4 5
|
mp3an |
⊢ +∞ ∈ ( 0 [,] +∞ ) |
| 7 |
6
|
a1i |
⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 = 0 ) → +∞ ∈ ( 0 [,] +∞ ) ) |
| 8 |
|
icossicc |
⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) |
| 9 |
|
uncom |
⊢ ( { 0 } ∪ ( 0 (,] 1 ) ) = ( ( 0 (,] 1 ) ∪ { 0 } ) |
| 10 |
|
1xr |
⊢ 1 ∈ ℝ* |
| 11 |
|
0le1 |
⊢ 0 ≤ 1 |
| 12 |
|
snunioc |
⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1 ) → ( { 0 } ∪ ( 0 (,] 1 ) ) = ( 0 [,] 1 ) ) |
| 13 |
2 10 11 12
|
mp3an |
⊢ ( { 0 } ∪ ( 0 (,] 1 ) ) = ( 0 [,] 1 ) |
| 14 |
9 13
|
eqtr3i |
⊢ ( ( 0 (,] 1 ) ∪ { 0 } ) = ( 0 [,] 1 ) |
| 15 |
14
|
eleq2i |
⊢ ( 𝑥 ∈ ( ( 0 (,] 1 ) ∪ { 0 } ) ↔ 𝑥 ∈ ( 0 [,] 1 ) ) |
| 16 |
|
elun |
⊢ ( 𝑥 ∈ ( ( 0 (,] 1 ) ∪ { 0 } ) ↔ ( 𝑥 ∈ ( 0 (,] 1 ) ∨ 𝑥 ∈ { 0 } ) ) |
| 17 |
15 16
|
bitr3i |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↔ ( 𝑥 ∈ ( 0 (,] 1 ) ∨ 𝑥 ∈ { 0 } ) ) |
| 18 |
|
pm2.53 |
⊢ ( ( 𝑥 ∈ ( 0 (,] 1 ) ∨ 𝑥 ∈ { 0 } ) → ( ¬ 𝑥 ∈ ( 0 (,] 1 ) → 𝑥 ∈ { 0 } ) ) |
| 19 |
17 18
|
sylbi |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → ( ¬ 𝑥 ∈ ( 0 (,] 1 ) → 𝑥 ∈ { 0 } ) ) |
| 20 |
|
elsni |
⊢ ( 𝑥 ∈ { 0 } → 𝑥 = 0 ) |
| 21 |
19 20
|
syl6 |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → ( ¬ 𝑥 ∈ ( 0 (,] 1 ) → 𝑥 = 0 ) ) |
| 22 |
21
|
con1d |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → ( ¬ 𝑥 = 0 → 𝑥 ∈ ( 0 (,] 1 ) ) ) |
| 23 |
22
|
imp |
⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 0 ) → 𝑥 ∈ ( 0 (,] 1 ) ) |
| 24 |
|
0le0 |
⊢ 0 ≤ 0 |
| 25 |
|
1re |
⊢ 1 ∈ ℝ |
| 26 |
|
ltpnf |
⊢ ( 1 ∈ ℝ → 1 < +∞ ) |
| 27 |
25 26
|
ax-mp |
⊢ 1 < +∞ |
| 28 |
|
iocssioo |
⊢ ( ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 0 ≤ 0 ∧ 1 < +∞ ) ) → ( 0 (,] 1 ) ⊆ ( 0 (,) +∞ ) ) |
| 29 |
2 3 24 27 28
|
mp4an |
⊢ ( 0 (,] 1 ) ⊆ ( 0 (,) +∞ ) |
| 30 |
|
ioorp |
⊢ ( 0 (,) +∞ ) = ℝ+ |
| 31 |
29 30
|
sseqtri |
⊢ ( 0 (,] 1 ) ⊆ ℝ+ |
| 32 |
31
|
sseli |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → 𝑥 ∈ ℝ+ ) |
| 33 |
32
|
relogcld |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → ( log ‘ 𝑥 ) ∈ ℝ ) |
| 34 |
33
|
renegcld |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → - ( log ‘ 𝑥 ) ∈ ℝ ) |
| 35 |
34
|
rexrd |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → - ( log ‘ 𝑥 ) ∈ ℝ* ) |
| 36 |
|
elioc1 |
⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( 𝑥 ∈ ( 0 (,] 1 ) ↔ ( 𝑥 ∈ ℝ* ∧ 0 < 𝑥 ∧ 𝑥 ≤ 1 ) ) ) |
| 37 |
2 10 36
|
mp2an |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) ↔ ( 𝑥 ∈ ℝ* ∧ 0 < 𝑥 ∧ 𝑥 ≤ 1 ) ) |
| 38 |
37
|
simp3bi |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → 𝑥 ≤ 1 ) |
| 39 |
|
1rp |
⊢ 1 ∈ ℝ+ |
| 40 |
39
|
a1i |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → 1 ∈ ℝ+ ) |
| 41 |
32 40
|
logled |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → ( 𝑥 ≤ 1 ↔ ( log ‘ 𝑥 ) ≤ ( log ‘ 1 ) ) ) |
| 42 |
38 41
|
mpbid |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → ( log ‘ 𝑥 ) ≤ ( log ‘ 1 ) ) |
| 43 |
|
log1 |
⊢ ( log ‘ 1 ) = 0 |
| 44 |
42 43
|
breqtrdi |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → ( log ‘ 𝑥 ) ≤ 0 ) |
| 45 |
33
|
le0neg1d |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → ( ( log ‘ 𝑥 ) ≤ 0 ↔ 0 ≤ - ( log ‘ 𝑥 ) ) ) |
| 46 |
44 45
|
mpbid |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → 0 ≤ - ( log ‘ 𝑥 ) ) |
| 47 |
|
ltpnf |
⊢ ( - ( log ‘ 𝑥 ) ∈ ℝ → - ( log ‘ 𝑥 ) < +∞ ) |
| 48 |
34 47
|
syl |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → - ( log ‘ 𝑥 ) < +∞ ) |
| 49 |
|
elico1 |
⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( - ( log ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( - ( log ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ - ( log ‘ 𝑥 ) ∧ - ( log ‘ 𝑥 ) < +∞ ) ) ) |
| 50 |
2 3 49
|
mp2an |
⊢ ( - ( log ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( - ( log ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ - ( log ‘ 𝑥 ) ∧ - ( log ‘ 𝑥 ) < +∞ ) ) |
| 51 |
35 46 48 50
|
syl3anbrc |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → - ( log ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) |
| 52 |
23 51
|
syl |
⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 0 ) → - ( log ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) |
| 53 |
8 52
|
sselid |
⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 0 ) → - ( log ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) |
| 54 |
7 53
|
ifclda |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ∈ ( 0 [,] +∞ ) ) |
| 55 |
54
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ∈ ( 0 [,] +∞ ) ) |
| 56 |
|
0elunit |
⊢ 0 ∈ ( 0 [,] 1 ) |
| 57 |
56
|
a1i |
⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ 𝑦 = +∞ ) → 0 ∈ ( 0 [,] 1 ) ) |
| 58 |
|
iocssicc |
⊢ ( 0 (,] 1 ) ⊆ ( 0 [,] 1 ) |
| 59 |
|
snunico |
⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞ ) → ( ( 0 [,) +∞ ) ∪ { +∞ } ) = ( 0 [,] +∞ ) ) |
| 60 |
2 3 4 59
|
mp3an |
⊢ ( ( 0 [,) +∞ ) ∪ { +∞ } ) = ( 0 [,] +∞ ) |
| 61 |
60
|
eleq2i |
⊢ ( 𝑦 ∈ ( ( 0 [,) +∞ ) ∪ { +∞ } ) ↔ 𝑦 ∈ ( 0 [,] +∞ ) ) |
| 62 |
|
elun |
⊢ ( 𝑦 ∈ ( ( 0 [,) +∞ ) ∪ { +∞ } ) ↔ ( 𝑦 ∈ ( 0 [,) +∞ ) ∨ 𝑦 ∈ { +∞ } ) ) |
| 63 |
61 62
|
bitr3i |
⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) ↔ ( 𝑦 ∈ ( 0 [,) +∞ ) ∨ 𝑦 ∈ { +∞ } ) ) |
| 64 |
|
pm2.53 |
⊢ ( ( 𝑦 ∈ ( 0 [,) +∞ ) ∨ 𝑦 ∈ { +∞ } ) → ( ¬ 𝑦 ∈ ( 0 [,) +∞ ) → 𝑦 ∈ { +∞ } ) ) |
| 65 |
63 64
|
sylbi |
⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → ( ¬ 𝑦 ∈ ( 0 [,) +∞ ) → 𝑦 ∈ { +∞ } ) ) |
| 66 |
|
elsni |
⊢ ( 𝑦 ∈ { +∞ } → 𝑦 = +∞ ) |
| 67 |
65 66
|
syl6 |
⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → ( ¬ 𝑦 ∈ ( 0 [,) +∞ ) → 𝑦 = +∞ ) ) |
| 68 |
67
|
con1d |
⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → ( ¬ 𝑦 = +∞ → 𝑦 ∈ ( 0 [,) +∞ ) ) ) |
| 69 |
68
|
imp |
⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → 𝑦 ∈ ( 0 [,) +∞ ) ) |
| 70 |
|
rge0ssre |
⊢ ( 0 [,) +∞ ) ⊆ ℝ |
| 71 |
70
|
sseli |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → 𝑦 ∈ ℝ ) |
| 72 |
71
|
renegcld |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → - 𝑦 ∈ ℝ ) |
| 73 |
72
|
reefcld |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → ( exp ‘ - 𝑦 ) ∈ ℝ ) |
| 74 |
73
|
rexrd |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → ( exp ‘ - 𝑦 ) ∈ ℝ* ) |
| 75 |
|
efgt0 |
⊢ ( - 𝑦 ∈ ℝ → 0 < ( exp ‘ - 𝑦 ) ) |
| 76 |
72 75
|
syl |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → 0 < ( exp ‘ - 𝑦 ) ) |
| 77 |
|
elico1 |
⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑦 ∈ ( 0 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ* ∧ 0 ≤ 𝑦 ∧ 𝑦 < +∞ ) ) ) |
| 78 |
2 3 77
|
mp2an |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ* ∧ 0 ≤ 𝑦 ∧ 𝑦 < +∞ ) ) |
| 79 |
78
|
simp2bi |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → 0 ≤ 𝑦 ) |
| 80 |
71
|
le0neg2d |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → ( 0 ≤ 𝑦 ↔ - 𝑦 ≤ 0 ) ) |
| 81 |
79 80
|
mpbid |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → - 𝑦 ≤ 0 ) |
| 82 |
|
0re |
⊢ 0 ∈ ℝ |
| 83 |
|
efle |
⊢ ( ( - 𝑦 ∈ ℝ ∧ 0 ∈ ℝ ) → ( - 𝑦 ≤ 0 ↔ ( exp ‘ - 𝑦 ) ≤ ( exp ‘ 0 ) ) ) |
| 84 |
72 82 83
|
sylancl |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → ( - 𝑦 ≤ 0 ↔ ( exp ‘ - 𝑦 ) ≤ ( exp ‘ 0 ) ) ) |
| 85 |
81 84
|
mpbid |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → ( exp ‘ - 𝑦 ) ≤ ( exp ‘ 0 ) ) |
| 86 |
|
ef0 |
⊢ ( exp ‘ 0 ) = 1 |
| 87 |
85 86
|
breqtrdi |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → ( exp ‘ - 𝑦 ) ≤ 1 ) |
| 88 |
|
elioc1 |
⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( exp ‘ - 𝑦 ) ∈ ( 0 (,] 1 ) ↔ ( ( exp ‘ - 𝑦 ) ∈ ℝ* ∧ 0 < ( exp ‘ - 𝑦 ) ∧ ( exp ‘ - 𝑦 ) ≤ 1 ) ) ) |
| 89 |
2 10 88
|
mp2an |
⊢ ( ( exp ‘ - 𝑦 ) ∈ ( 0 (,] 1 ) ↔ ( ( exp ‘ - 𝑦 ) ∈ ℝ* ∧ 0 < ( exp ‘ - 𝑦 ) ∧ ( exp ‘ - 𝑦 ) ≤ 1 ) ) |
| 90 |
74 76 87 89
|
syl3anbrc |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → ( exp ‘ - 𝑦 ) ∈ ( 0 (,] 1 ) ) |
| 91 |
69 90
|
syl |
⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → ( exp ‘ - 𝑦 ) ∈ ( 0 (,] 1 ) ) |
| 92 |
58 91
|
sselid |
⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → ( exp ‘ - 𝑦 ) ∈ ( 0 [,] 1 ) ) |
| 93 |
57 92
|
ifclda |
⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) ∈ ( 0 [,] 1 ) ) |
| 94 |
93
|
adantl |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) ∈ ( 0 [,] 1 ) ) |
| 95 |
|
eqeq2 |
⊢ ( 0 = if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) → ( 𝑥 = 0 ↔ 𝑥 = if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) ) ) |
| 96 |
95
|
bibi1d |
⊢ ( 0 = if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) → ( ( 𝑥 = 0 ↔ 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ↔ ( 𝑥 = if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) ↔ 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ) ) |
| 97 |
|
eqeq2 |
⊢ ( ( exp ‘ - 𝑦 ) = if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) → ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 𝑥 = if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) ) ) |
| 98 |
97
|
bibi1d |
⊢ ( ( exp ‘ - 𝑦 ) = if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) → ( ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ↔ ( 𝑥 = if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) ↔ 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ) ) |
| 99 |
|
simpr |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → 𝑦 = +∞ ) |
| 100 |
|
iftrue |
⊢ ( 𝑥 = 0 → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) = +∞ ) |
| 101 |
100
|
eqeq2d |
⊢ ( 𝑥 = 0 → ( 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ↔ 𝑦 = +∞ ) ) |
| 102 |
99 101
|
syl5ibrcom |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( 𝑥 = 0 → 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ) |
| 103 |
|
ubico |
⊢ ( ( 0 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ¬ +∞ ∈ ( 0 [,) +∞ ) ) |
| 104 |
82 3 103
|
mp2an |
⊢ ¬ +∞ ∈ ( 0 [,) +∞ ) |
| 105 |
104
|
nelir |
⊢ +∞ ∉ ( 0 [,) +∞ ) |
| 106 |
|
neleq1 |
⊢ ( 𝑦 = +∞ → ( 𝑦 ∉ ( 0 [,) +∞ ) ↔ +∞ ∉ ( 0 [,) +∞ ) ) ) |
| 107 |
106
|
adantl |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( 𝑦 ∉ ( 0 [,) +∞ ) ↔ +∞ ∉ ( 0 [,) +∞ ) ) ) |
| 108 |
105 107
|
mpbiri |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → 𝑦 ∉ ( 0 [,) +∞ ) ) |
| 109 |
|
neleq1 |
⊢ ( 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) → ( 𝑦 ∉ ( 0 [,) +∞ ) ↔ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ∉ ( 0 [,) +∞ ) ) ) |
| 110 |
108 109
|
syl5ibcom |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ∉ ( 0 [,) +∞ ) ) ) |
| 111 |
|
df-nel |
⊢ ( if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ∉ ( 0 [,) +∞ ) ↔ ¬ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ∈ ( 0 [,) +∞ ) ) |
| 112 |
|
iffalse |
⊢ ( ¬ 𝑥 = 0 → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) = - ( log ‘ 𝑥 ) ) |
| 113 |
112
|
adantl |
⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 0 ) → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) = - ( log ‘ 𝑥 ) ) |
| 114 |
113 52
|
eqeltrd |
⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 0 ) → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ∈ ( 0 [,) +∞ ) ) |
| 115 |
114
|
ex |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → ( ¬ 𝑥 = 0 → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ∈ ( 0 [,) +∞ ) ) ) |
| 116 |
115
|
ad2antrr |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( ¬ 𝑥 = 0 → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ∈ ( 0 [,) +∞ ) ) ) |
| 117 |
116
|
con1d |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( ¬ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ∈ ( 0 [,) +∞ ) → 𝑥 = 0 ) ) |
| 118 |
111 117
|
biimtrid |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ∉ ( 0 [,) +∞ ) → 𝑥 = 0 ) ) |
| 119 |
110 118
|
syld |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) → 𝑥 = 0 ) ) |
| 120 |
102 119
|
impbid |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 𝑦 = +∞ ) → ( 𝑥 = 0 ↔ 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ) |
| 121 |
|
eqeq2 |
⊢ ( +∞ = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) → ( 𝑦 = +∞ ↔ 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ) |
| 122 |
121
|
bibi2d |
⊢ ( +∞ = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) → ( ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 𝑦 = +∞ ) ↔ ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ) ) |
| 123 |
|
eqeq2 |
⊢ ( - ( log ‘ 𝑥 ) = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) → ( 𝑦 = - ( log ‘ 𝑥 ) ↔ 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ) |
| 124 |
123
|
bibi2d |
⊢ ( - ( log ‘ 𝑥 ) = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) → ( ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 𝑦 = - ( log ‘ 𝑥 ) ) ↔ ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ) ) |
| 125 |
82
|
a1i |
⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → 0 ∈ ℝ ) |
| 126 |
69 76
|
syl |
⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → 0 < ( exp ‘ - 𝑦 ) ) |
| 127 |
125 126
|
ltned |
⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) → 0 ≠ ( exp ‘ - 𝑦 ) ) |
| 128 |
127
|
adantll |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) → 0 ≠ ( exp ‘ - 𝑦 ) ) |
| 129 |
128
|
neneqd |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) → ¬ 0 = ( exp ‘ - 𝑦 ) ) |
| 130 |
|
eqeq1 |
⊢ ( 𝑥 = 0 → ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 0 = ( exp ‘ - 𝑦 ) ) ) |
| 131 |
130
|
notbid |
⊢ ( 𝑥 = 0 → ( ¬ 𝑥 = ( exp ‘ - 𝑦 ) ↔ ¬ 0 = ( exp ‘ - 𝑦 ) ) ) |
| 132 |
129 131
|
syl5ibrcom |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) → ( 𝑥 = 0 → ¬ 𝑥 = ( exp ‘ - 𝑦 ) ) ) |
| 133 |
132
|
imp |
⊢ ( ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) ∧ 𝑥 = 0 ) → ¬ 𝑥 = ( exp ‘ - 𝑦 ) ) |
| 134 |
|
simplr |
⊢ ( ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) ∧ 𝑥 = 0 ) → ¬ 𝑦 = +∞ ) |
| 135 |
133 134
|
2falsed |
⊢ ( ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) ∧ 𝑥 = 0 ) → ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 𝑦 = +∞ ) ) |
| 136 |
|
eqcom |
⊢ ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ ( exp ‘ - 𝑦 ) = 𝑥 ) |
| 137 |
136
|
a1i |
⊢ ( ( 𝑥 ∈ ( 0 (,] 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ ( exp ‘ - 𝑦 ) = 𝑥 ) ) |
| 138 |
|
relogeftb |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ - 𝑦 ∈ ℝ ) → ( ( log ‘ 𝑥 ) = - 𝑦 ↔ ( exp ‘ - 𝑦 ) = 𝑥 ) ) |
| 139 |
32 72 138
|
syl2an |
⊢ ( ( 𝑥 ∈ ( 0 (,] 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( ( log ‘ 𝑥 ) = - 𝑦 ↔ ( exp ‘ - 𝑦 ) = 𝑥 ) ) |
| 140 |
33
|
recnd |
⊢ ( 𝑥 ∈ ( 0 (,] 1 ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
| 141 |
71
|
recnd |
⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) → 𝑦 ∈ ℂ ) |
| 142 |
|
negcon2 |
⊢ ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( log ‘ 𝑥 ) = - 𝑦 ↔ 𝑦 = - ( log ‘ 𝑥 ) ) ) |
| 143 |
140 141 142
|
syl2an |
⊢ ( ( 𝑥 ∈ ( 0 (,] 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( ( log ‘ 𝑥 ) = - 𝑦 ↔ 𝑦 = - ( log ‘ 𝑥 ) ) ) |
| 144 |
137 139 143
|
3bitr2d |
⊢ ( ( 𝑥 ∈ ( 0 (,] 1 ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 𝑦 = - ( log ‘ 𝑥 ) ) ) |
| 145 |
23 69 144
|
syl2an |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 = 0 ) ∧ ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝑦 = +∞ ) ) → ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 𝑦 = - ( log ‘ 𝑥 ) ) ) |
| 146 |
145
|
an4s |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ( ¬ 𝑥 = 0 ∧ ¬ 𝑦 = +∞ ) ) → ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 𝑦 = - ( log ‘ 𝑥 ) ) ) |
| 147 |
146
|
anass1rs |
⊢ ( ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) ∧ ¬ 𝑥 = 0 ) → ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 𝑦 = - ( log ‘ 𝑥 ) ) ) |
| 148 |
122 124 135 147
|
ifbothda |
⊢ ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑦 = +∞ ) → ( 𝑥 = ( exp ‘ - 𝑦 ) ↔ 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ) |
| 149 |
96 98 120 148
|
ifbothda |
⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 = if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) ↔ 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ) |
| 150 |
149
|
adantl |
⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑥 = if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) ↔ 𝑦 = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ) |
| 151 |
1 55 94 150
|
f1ocnv2d |
⊢ ( ⊤ → ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ ) ∧ ◡ 𝐹 = ( 𝑦 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) ) ) ) |
| 152 |
151
|
mptru |
⊢ ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ ) ∧ ◡ 𝐹 = ( 𝑦 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) ) ) |