Step |
Hyp |
Ref |
Expression |
1 |
|
0re |
⊢ 0 ∈ ℝ |
2 |
1
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ∈ ℝ ) |
3 |
|
simpl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℝ ) |
4 |
|
elicc2 |
⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) ) |
5 |
1 3 4
|
sylancr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) ) |
6 |
5
|
biimpa |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ( 0 [,] 𝐴 ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) |
7 |
6
|
simp1d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ( 0 [,] 𝐴 ) ) → 𝑥 ∈ ℝ ) |
8 |
6
|
simp2d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ( 0 [,] 𝐴 ) ) → 0 ≤ 𝑥 ) |
9 |
7 8
|
ge0p1rpd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ( 0 [,] 𝐴 ) ) → ( 𝑥 + 1 ) ∈ ℝ+ ) |
10 |
9
|
fvresd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ( 0 [,] 𝐴 ) ) → ( ( log ↾ ℝ+ ) ‘ ( 𝑥 + 1 ) ) = ( log ‘ ( 𝑥 + 1 ) ) ) |
11 |
10
|
mpteq2dva |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( ( log ↾ ℝ+ ) ‘ ( 𝑥 + 1 ) ) ) = ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( log ‘ ( 𝑥 + 1 ) ) ) ) |
12 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
13 |
12
|
cnfldtopon |
⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) |
14 |
7
|
ex |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) → 𝑥 ∈ ℝ ) ) |
15 |
14
|
ssrdv |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 0 [,] 𝐴 ) ⊆ ℝ ) |
16 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
17 |
15 16
|
sstrdi |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 0 [,] 𝐴 ) ⊆ ℂ ) |
18 |
|
resttopon |
⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( 0 [,] 𝐴 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 𝐴 ) ) ∈ ( TopOn ‘ ( 0 [,] 𝐴 ) ) ) |
19 |
13 17 18
|
sylancr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 𝐴 ) ) ∈ ( TopOn ‘ ( 0 [,] 𝐴 ) ) ) |
20 |
9
|
fmpttd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( 𝑥 + 1 ) ) : ( 0 [,] 𝐴 ) ⟶ ℝ+ ) |
21 |
|
rpssre |
⊢ ℝ+ ⊆ ℝ |
22 |
21 16
|
sstri |
⊢ ℝ+ ⊆ ℂ |
23 |
12
|
addcn |
⊢ + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) |
24 |
23
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ) |
25 |
|
ssid |
⊢ ℂ ⊆ ℂ |
26 |
|
cncfmptid |
⊢ ( ( ( 0 [,] 𝐴 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ 𝑥 ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℂ ) ) |
27 |
17 25 26
|
sylancl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ 𝑥 ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℂ ) ) |
28 |
|
1cnd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 1 ∈ ℂ ) |
29 |
25
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ℂ ⊆ ℂ ) |
30 |
|
cncfmptc |
⊢ ( ( 1 ∈ ℂ ∧ ( 0 [,] 𝐴 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ 1 ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℂ ) ) |
31 |
28 17 29 30
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ 1 ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℂ ) ) |
32 |
12 24 27 31
|
cncfmpt2f |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( 𝑥 + 1 ) ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℂ ) ) |
33 |
|
cncffvrn |
⊢ ( ( ℝ+ ⊆ ℂ ∧ ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( 𝑥 + 1 ) ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℂ ) ) → ( ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( 𝑥 + 1 ) ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℝ+ ) ↔ ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( 𝑥 + 1 ) ) : ( 0 [,] 𝐴 ) ⟶ ℝ+ ) ) |
34 |
22 32 33
|
sylancr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( 𝑥 + 1 ) ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℝ+ ) ↔ ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( 𝑥 + 1 ) ) : ( 0 [,] 𝐴 ) ⟶ ℝ+ ) ) |
35 |
20 34
|
mpbird |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( 𝑥 + 1 ) ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℝ+ ) ) |
36 |
|
eqid |
⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 𝐴 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 𝐴 ) ) |
37 |
|
eqid |
⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) |
38 |
12 36 37
|
cncfcn |
⊢ ( ( ( 0 [,] 𝐴 ) ⊆ ℂ ∧ ℝ+ ⊆ ℂ ) → ( ( 0 [,] 𝐴 ) –cn→ ℝ+ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 𝐴 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) ) ) |
39 |
17 22 38
|
sylancl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 0 [,] 𝐴 ) –cn→ ℝ+ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 𝐴 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) ) ) |
40 |
35 39
|
eleqtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( 𝑥 + 1 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 𝐴 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) ) ) |
41 |
|
relogcn |
⊢ ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ ) |
42 |
|
eqid |
⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
43 |
12 37 42
|
cncfcn |
⊢ ( ( ℝ+ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℝ+ –cn→ ℝ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) |
44 |
22 16 43
|
mp2an |
⊢ ( ℝ+ –cn→ ℝ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) |
45 |
41 44
|
eleqtri |
⊢ ( log ↾ ℝ+ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) |
46 |
45
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( log ↾ ℝ+ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) |
47 |
19 40 46
|
cnmpt11f |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( ( log ↾ ℝ+ ) ‘ ( 𝑥 + 1 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 𝐴 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) |
48 |
12 36 42
|
cncfcn |
⊢ ( ( ( 0 [,] 𝐴 ) ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ( 0 [,] 𝐴 ) –cn→ ℝ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 𝐴 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) |
49 |
17 16 48
|
sylancl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 0 [,] 𝐴 ) –cn→ ℝ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 𝐴 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) |
50 |
47 49
|
eleqtrrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( ( log ↾ ℝ+ ) ‘ ( 𝑥 + 1 ) ) ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℝ ) ) |
51 |
11 50
|
eqeltrrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( log ‘ ( 𝑥 + 1 ) ) ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℝ ) ) |
52 |
|
reelprrecn |
⊢ ℝ ∈ { ℝ , ℂ } |
53 |
52
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ℝ ∈ { ℝ , ℂ } ) |
54 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ ) |
55 |
|
1rp |
⊢ 1 ∈ ℝ+ |
56 |
|
rpaddcl |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ∈ ℝ+ ) → ( 𝑥 + 1 ) ∈ ℝ+ ) |
57 |
54 55 56
|
sylancl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 + 1 ) ∈ ℝ+ ) |
58 |
57
|
relogcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ ( 𝑥 + 1 ) ) ∈ ℝ ) |
59 |
58
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ ( 𝑥 + 1 ) ) ∈ ℂ ) |
60 |
57
|
rpreccld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( 1 / ( 𝑥 + 1 ) ) ∈ ℝ+ ) |
61 |
|
1cnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℂ ) |
62 |
|
relogcl |
⊢ ( 𝑦 ∈ ℝ+ → ( log ‘ 𝑦 ) ∈ ℝ ) |
63 |
62
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → ( log ‘ 𝑦 ) ∈ ℝ ) |
64 |
63
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → ( log ‘ 𝑦 ) ∈ ℂ ) |
65 |
|
rpreccl |
⊢ ( 𝑦 ∈ ℝ+ → ( 1 / 𝑦 ) ∈ ℝ+ ) |
66 |
65
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → ( 1 / 𝑦 ) ∈ ℝ+ ) |
67 |
|
peano2re |
⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ ) |
68 |
67
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + 1 ) ∈ ℝ ) |
69 |
68
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + 1 ) ∈ ℂ ) |
70 |
|
1cnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℂ ) |
71 |
16
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ℝ ⊆ ℂ ) |
72 |
71
|
sselda |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ ) |
73 |
53
|
dvmptid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℝ D ( 𝑥 ∈ ℝ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℝ ↦ 1 ) ) |
74 |
|
0cnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℂ ) |
75 |
53 28
|
dvmptc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℝ D ( 𝑥 ∈ ℝ ↦ 1 ) ) = ( 𝑥 ∈ ℝ ↦ 0 ) ) |
76 |
53 72 70 73 70 74 75
|
dvmptadd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℝ D ( 𝑥 ∈ ℝ ↦ ( 𝑥 + 1 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 1 + 0 ) ) ) |
77 |
|
1p0e1 |
⊢ ( 1 + 0 ) = 1 |
78 |
77
|
mpteq2i |
⊢ ( 𝑥 ∈ ℝ ↦ ( 1 + 0 ) ) = ( 𝑥 ∈ ℝ ↦ 1 ) |
79 |
76 78
|
eqtrdi |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℝ D ( 𝑥 ∈ ℝ ↦ ( 𝑥 + 1 ) ) ) = ( 𝑥 ∈ ℝ ↦ 1 ) ) |
80 |
21
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ℝ+ ⊆ ℝ ) |
81 |
12
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
82 |
|
ioorp |
⊢ ( 0 (,) +∞ ) = ℝ+ |
83 |
|
iooretop |
⊢ ( 0 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) |
84 |
82 83
|
eqeltrri |
⊢ ℝ+ ∈ ( topGen ‘ ran (,) ) |
85 |
84
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ℝ+ ∈ ( topGen ‘ ran (,) ) ) |
86 |
53 69 70 79 80 81 12 85
|
dvmptres |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 + 1 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ 1 ) ) |
87 |
|
relogf1o |
⊢ ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ |
88 |
|
f1of |
⊢ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ) |
89 |
87 88
|
mp1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ) |
90 |
89
|
feqmptd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( log ↾ ℝ+ ) = ( 𝑦 ∈ ℝ+ ↦ ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) ) |
91 |
|
fvres |
⊢ ( 𝑦 ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ 𝑦 ) = ( log ‘ 𝑦 ) ) |
92 |
91
|
mpteq2ia |
⊢ ( 𝑦 ∈ ℝ+ ↦ ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) = ( 𝑦 ∈ ℝ+ ↦ ( log ‘ 𝑦 ) ) |
93 |
90 92
|
eqtrdi |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( log ↾ ℝ+ ) = ( 𝑦 ∈ ℝ+ ↦ ( log ‘ 𝑦 ) ) ) |
94 |
93
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℝ D ( log ↾ ℝ+ ) ) = ( ℝ D ( 𝑦 ∈ ℝ+ ↦ ( log ‘ 𝑦 ) ) ) ) |
95 |
|
dvrelog |
⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑦 ∈ ℝ+ ↦ ( 1 / 𝑦 ) ) |
96 |
94 95
|
eqtr3di |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℝ D ( 𝑦 ∈ ℝ+ ↦ ( log ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( 1 / 𝑦 ) ) ) |
97 |
|
fveq2 |
⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( log ‘ 𝑦 ) = ( log ‘ ( 𝑥 + 1 ) ) ) |
98 |
|
oveq2 |
⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( 1 / 𝑦 ) = ( 1 / ( 𝑥 + 1 ) ) ) |
99 |
53 53 57 61 64 66 86 96 97 98
|
dvmptco |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ ( 𝑥 + 1 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( 1 / ( 𝑥 + 1 ) ) · 1 ) ) ) |
100 |
60
|
rpcnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( 1 / ( 𝑥 + 1 ) ) ∈ ℂ ) |
101 |
100
|
mulid1d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 / ( 𝑥 + 1 ) ) · 1 ) = ( 1 / ( 𝑥 + 1 ) ) ) |
102 |
101
|
mpteq2dva |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ℝ+ ↦ ( ( 1 / ( 𝑥 + 1 ) ) · 1 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( 𝑥 + 1 ) ) ) ) |
103 |
99 102
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ ( 𝑥 + 1 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( 𝑥 + 1 ) ) ) ) |
104 |
|
ioossicc |
⊢ ( 0 (,) 𝐴 ) ⊆ ( 0 [,] 𝐴 ) |
105 |
104
|
sseli |
⊢ ( 𝑥 ∈ ( 0 (,) 𝐴 ) → 𝑥 ∈ ( 0 [,] 𝐴 ) ) |
106 |
105 7
|
sylan2 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ( 0 (,) 𝐴 ) ) → 𝑥 ∈ ℝ ) |
107 |
|
eliooord |
⊢ ( 𝑥 ∈ ( 0 (,) 𝐴 ) → ( 0 < 𝑥 ∧ 𝑥 < 𝐴 ) ) |
108 |
107
|
simpld |
⊢ ( 𝑥 ∈ ( 0 (,) 𝐴 ) → 0 < 𝑥 ) |
109 |
108
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ( 0 (,) 𝐴 ) ) → 0 < 𝑥 ) |
110 |
106 109
|
elrpd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ( 0 (,) 𝐴 ) ) → 𝑥 ∈ ℝ+ ) |
111 |
110
|
ex |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 (,) 𝐴 ) → 𝑥 ∈ ℝ+ ) ) |
112 |
111
|
ssrdv |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 0 (,) 𝐴 ) ⊆ ℝ+ ) |
113 |
|
iooretop |
⊢ ( 0 (,) 𝐴 ) ∈ ( topGen ‘ ran (,) ) |
114 |
113
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 0 (,) 𝐴 ) ∈ ( topGen ‘ ran (,) ) ) |
115 |
53 59 60 103 112 81 12 114
|
dvmptres |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℝ D ( 𝑥 ∈ ( 0 (,) 𝐴 ) ↦ ( log ‘ ( 𝑥 + 1 ) ) ) ) = ( 𝑥 ∈ ( 0 (,) 𝐴 ) ↦ ( 1 / ( 𝑥 + 1 ) ) ) ) |
116 |
|
elrege0 |
⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) |
117 |
7 8 116
|
sylanbrc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ( 0 [,] 𝐴 ) ) → 𝑥 ∈ ( 0 [,) +∞ ) ) |
118 |
117
|
ex |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) → 𝑥 ∈ ( 0 [,) +∞ ) ) ) |
119 |
118
|
ssrdv |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 0 [,] 𝐴 ) ⊆ ( 0 [,) +∞ ) ) |
120 |
119
|
resabs1d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ↾ ( 0 [,) +∞ ) ) ↾ ( 0 [,] 𝐴 ) ) = ( √ ↾ ( 0 [,] 𝐴 ) ) ) |
121 |
|
sqrtf |
⊢ √ : ℂ ⟶ ℂ |
122 |
121
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → √ : ℂ ⟶ ℂ ) |
123 |
122 17
|
feqresmpt |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ↾ ( 0 [,] 𝐴 ) ) = ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( √ ‘ 𝑥 ) ) ) |
124 |
120 123
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ↾ ( 0 [,) +∞ ) ) ↾ ( 0 [,] 𝐴 ) ) = ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( √ ‘ 𝑥 ) ) ) |
125 |
|
resqrtcn |
⊢ ( √ ↾ ( 0 [,) +∞ ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℝ ) |
126 |
|
rescncf |
⊢ ( ( 0 [,] 𝐴 ) ⊆ ( 0 [,) +∞ ) → ( ( √ ↾ ( 0 [,) +∞ ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℝ ) → ( ( √ ↾ ( 0 [,) +∞ ) ) ↾ ( 0 [,] 𝐴 ) ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℝ ) ) ) |
127 |
119 125 126
|
mpisyl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ↾ ( 0 [,) +∞ ) ) ↾ ( 0 [,] 𝐴 ) ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℝ ) ) |
128 |
124 127
|
eqeltrrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↦ ( √ ‘ 𝑥 ) ) ∈ ( ( 0 [,] 𝐴 ) –cn→ ℝ ) ) |
129 |
|
rpcn |
⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ ) |
130 |
129
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ ) |
131 |
130
|
sqrtcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℂ ) |
132 |
|
2rp |
⊢ 2 ∈ ℝ+ |
133 |
|
rpsqrtcl |
⊢ ( 𝑥 ∈ ℝ+ → ( √ ‘ 𝑥 ) ∈ ℝ+ ) |
134 |
133
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℝ+ ) |
135 |
|
rpmulcl |
⊢ ( ( 2 ∈ ℝ+ ∧ ( √ ‘ 𝑥 ) ∈ ℝ+ ) → ( 2 · ( √ ‘ 𝑥 ) ) ∈ ℝ+ ) |
136 |
132 134 135
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( √ ‘ 𝑥 ) ) ∈ ℝ+ ) |
137 |
136
|
rpreccld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ∈ ℝ+ ) |
138 |
|
dvsqrt |
⊢ ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
139 |
138
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) ) |
140 |
53 131 137 139 112 81 12 114
|
dvmptres |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℝ D ( 𝑥 ∈ ( 0 (,) 𝐴 ) ↦ ( √ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 (,) 𝐴 ) ↦ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) ) |
141 |
134
|
rpred |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℝ ) |
142 |
|
1re |
⊢ 1 ∈ ℝ |
143 |
|
resubcl |
⊢ ( ( ( √ ‘ 𝑥 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( √ ‘ 𝑥 ) − 1 ) ∈ ℝ ) |
144 |
141 142 143
|
sylancl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( √ ‘ 𝑥 ) − 1 ) ∈ ℝ ) |
145 |
144
|
sqge0d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ ( ( ( √ ‘ 𝑥 ) − 1 ) ↑ 2 ) ) |
146 |
130
|
sqsqrtd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( √ ‘ 𝑥 ) ↑ 2 ) = 𝑥 ) |
147 |
146
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( √ ‘ 𝑥 ) ↑ 2 ) − ( 2 · ( √ ‘ 𝑥 ) ) ) = ( 𝑥 − ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
148 |
147
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( √ ‘ 𝑥 ) ↑ 2 ) − ( 2 · ( √ ‘ 𝑥 ) ) ) + 1 ) = ( ( 𝑥 − ( 2 · ( √ ‘ 𝑥 ) ) ) + 1 ) ) |
149 |
|
binom2sub1 |
⊢ ( ( √ ‘ 𝑥 ) ∈ ℂ → ( ( ( √ ‘ 𝑥 ) − 1 ) ↑ 2 ) = ( ( ( ( √ ‘ 𝑥 ) ↑ 2 ) − ( 2 · ( √ ‘ 𝑥 ) ) ) + 1 ) ) |
150 |
131 149
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( √ ‘ 𝑥 ) − 1 ) ↑ 2 ) = ( ( ( ( √ ‘ 𝑥 ) ↑ 2 ) − ( 2 · ( √ ‘ 𝑥 ) ) ) + 1 ) ) |
151 |
136
|
rpcnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( √ ‘ 𝑥 ) ) ∈ ℂ ) |
152 |
130 61 151
|
addsubd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑥 + 1 ) − ( 2 · ( √ ‘ 𝑥 ) ) ) = ( ( 𝑥 − ( 2 · ( √ ‘ 𝑥 ) ) ) + 1 ) ) |
153 |
148 150 152
|
3eqtr4d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( √ ‘ 𝑥 ) − 1 ) ↑ 2 ) = ( ( 𝑥 + 1 ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
154 |
145 153
|
breqtrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ ( ( 𝑥 + 1 ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
155 |
57
|
rpred |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 + 1 ) ∈ ℝ ) |
156 |
136
|
rpred |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( √ ‘ 𝑥 ) ) ∈ ℝ ) |
157 |
155 156
|
subge0d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( 0 ≤ ( ( 𝑥 + 1 ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ↔ ( 2 · ( √ ‘ 𝑥 ) ) ≤ ( 𝑥 + 1 ) ) ) |
158 |
154 157
|
mpbid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( √ ‘ 𝑥 ) ) ≤ ( 𝑥 + 1 ) ) |
159 |
136 57
|
lerecd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · ( √ ‘ 𝑥 ) ) ≤ ( 𝑥 + 1 ) ↔ ( 1 / ( 𝑥 + 1 ) ) ≤ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) ) |
160 |
158 159
|
mpbid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) → ( 1 / ( 𝑥 + 1 ) ) ≤ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
161 |
110 160
|
syldan |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑥 ∈ ( 0 (,) 𝐴 ) ) → ( 1 / ( 𝑥 + 1 ) ) ≤ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
162 |
|
rexr |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* ) |
163 |
|
0xr |
⊢ 0 ∈ ℝ* |
164 |
|
lbicc2 |
⊢ ( ( 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → 0 ∈ ( 0 [,] 𝐴 ) ) |
165 |
163 164
|
mp3an1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → 0 ∈ ( 0 [,] 𝐴 ) ) |
166 |
162 165
|
sylan |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ∈ ( 0 [,] 𝐴 ) ) |
167 |
|
ubicc2 |
⊢ ( ( 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ( 0 [,] 𝐴 ) ) |
168 |
163 167
|
mp3an1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ( 0 [,] 𝐴 ) ) |
169 |
162 168
|
sylan |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ( 0 [,] 𝐴 ) ) |
170 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ 𝐴 ) |
171 |
|
fv0p1e1 |
⊢ ( 𝑥 = 0 → ( log ‘ ( 𝑥 + 1 ) ) = ( log ‘ 1 ) ) |
172 |
|
log1 |
⊢ ( log ‘ 1 ) = 0 |
173 |
171 172
|
eqtrdi |
⊢ ( 𝑥 = 0 → ( log ‘ ( 𝑥 + 1 ) ) = 0 ) |
174 |
|
fveq2 |
⊢ ( 𝑥 = 0 → ( √ ‘ 𝑥 ) = ( √ ‘ 0 ) ) |
175 |
|
sqrt0 |
⊢ ( √ ‘ 0 ) = 0 |
176 |
174 175
|
eqtrdi |
⊢ ( 𝑥 = 0 → ( √ ‘ 𝑥 ) = 0 ) |
177 |
|
fvoveq1 |
⊢ ( 𝑥 = 𝐴 → ( log ‘ ( 𝑥 + 1 ) ) = ( log ‘ ( 𝐴 + 1 ) ) ) |
178 |
|
fveq2 |
⊢ ( 𝑥 = 𝐴 → ( √ ‘ 𝑥 ) = ( √ ‘ 𝐴 ) ) |
179 |
2 3 51 115 128 140 161 166 169 170 173 176 177 178
|
dvle |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( log ‘ ( 𝐴 + 1 ) ) − 0 ) ≤ ( ( √ ‘ 𝐴 ) − 0 ) ) |
180 |
|
ge0p1rp |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 + 1 ) ∈ ℝ+ ) |
181 |
180
|
relogcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( log ‘ ( 𝐴 + 1 ) ) ∈ ℝ ) |
182 |
|
resqrtcl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ ) |
183 |
181 182 2
|
lesub1d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( log ‘ ( 𝐴 + 1 ) ) ≤ ( √ ‘ 𝐴 ) ↔ ( ( log ‘ ( 𝐴 + 1 ) ) − 0 ) ≤ ( ( √ ‘ 𝐴 ) − 0 ) ) ) |
184 |
179 183
|
mpbird |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( log ‘ ( 𝐴 + 1 ) ) ≤ ( √ ‘ 𝐴 ) ) |