Step | Hyp | Ref
| Expression |
1 | | 0re 10040 |
. . . 4
⊢ 0 ∈
ℝ |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 0 ∈
ℝ) |
3 | | simpl 473 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 𝐴 ∈ ℝ) |
4 | | elicc2 12238 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑥
∈ (0[,]𝐴) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥 ∧ 𝑥 ≤ 𝐴))) |
5 | 1, 3, 4 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴))) |
6 | 5 | biimpa 501 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴)) |
7 | 6 | simp1d 1073 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → 𝑥 ∈ ℝ) |
8 | 6 | simp2d 1074 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → 0 ≤ 𝑥) |
9 | 7, 8 | ge0p1rpd 11902 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → (𝑥 + 1) ∈
ℝ+) |
10 | 9 | fvresd 6208 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → ((log ↾
ℝ+)‘(𝑥 + 1)) = (log‘(𝑥 + 1))) |
11 | 10 | mpteq2dva 4744 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ ((log ↾
ℝ+)‘(𝑥 + 1))) = (𝑥 ∈ (0[,]𝐴) ↦ (log‘(𝑥 + 1)))) |
12 | | eqid 2622 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
13 | 12 | cnfldtopon 22586 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
14 | 7 | ex 450 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) → 𝑥 ∈ ℝ)) |
15 | 14 | ssrdv 3609 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (0[,]𝐴) ⊆
ℝ) |
16 | | ax-resscn 9993 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
17 | 15, 16 | syl6ss 3615 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (0[,]𝐴) ⊆
ℂ) |
18 | | resttopon 20965 |
. . . . . . 7
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (0[,]𝐴) ⊆
ℂ) → ((TopOpen‘ℂfld) ↾t
(0[,]𝐴)) ∈
(TopOn‘(0[,]𝐴))) |
19 | 13, 17, 18 | sylancr 695 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
((TopOpen‘ℂfld) ↾t (0[,]𝐴)) ∈
(TopOn‘(0[,]𝐴))) |
20 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) = (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) |
21 | 9, 20 | fmptd 6385 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)):(0[,]𝐴)⟶ℝ+) |
22 | | rpssre 11843 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ ℝ |
23 | 22, 16 | sstri 3612 |
. . . . . . . . 9
⊢
ℝ+ ⊆ ℂ |
24 | 12 | addcn 22668 |
. . . . . . . . . . 11
⊢ + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
26 | | ssid 3624 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
27 | | cncfmptid 22715 |
. . . . . . . . . . 11
⊢
(((0[,]𝐴) ⊆
ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (0[,]𝐴) ↦ 𝑥) ∈ ((0[,]𝐴)–cn→ℂ)) |
28 | 17, 26, 27 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ 𝑥) ∈ ((0[,]𝐴)–cn→ℂ)) |
29 | | 1cnd 10056 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 1 ∈
ℂ) |
30 | 26 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ℂ ⊆
ℂ) |
31 | | cncfmptc 22714 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (0[,]𝐴) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑥 ∈
(0[,]𝐴) ↦ 1) ∈
((0[,]𝐴)–cn→ℂ)) |
32 | 29, 17, 30, 31 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ 1) ∈ ((0[,]𝐴)–cn→ℂ)) |
33 | 12, 25, 28, 32 | cncfmpt2f 22717 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℂ)) |
34 | | cncffvrn 22701 |
. . . . . . . . 9
⊢
((ℝ+ ⊆ ℂ ∧ (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℂ)) → ((𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℝ+) ↔ (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)):(0[,]𝐴)⟶ℝ+)) |
35 | 23, 33, 34 | sylancr 695 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℝ+) ↔ (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)):(0[,]𝐴)⟶ℝ+)) |
36 | 21, 35 | mpbird 247 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℝ+)) |
37 | | eqid 2622 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t (0[,]𝐴)) =
((TopOpen‘ℂfld) ↾t (0[,]𝐴)) |
38 | | eqid 2622 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t
ℝ+) = ((TopOpen‘ℂfld)
↾t ℝ+) |
39 | 12, 37, 38 | cncfcn 22712 |
. . . . . . . 8
⊢
(((0[,]𝐴) ⊆
ℂ ∧ ℝ+ ⊆ ℂ) → ((0[,]𝐴)–cn→ℝ+) =
(((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn
((TopOpen‘ℂfld) ↾t
ℝ+))) |
40 | 17, 23, 39 | sylancl 694 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((0[,]𝐴)–cn→ℝ+) =
(((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn
((TopOpen‘ℂfld) ↾t
ℝ+))) |
41 | 36, 40 | eleqtrd 2703 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈
(((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn
((TopOpen‘ℂfld) ↾t
ℝ+))) |
42 | | relogcn 24384 |
. . . . . . . 8
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℝ) |
43 | | eqid 2622 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ℝ) =
((TopOpen‘ℂfld) ↾t
ℝ) |
44 | 12, 38, 43 | cncfcn 22712 |
. . . . . . . . 9
⊢
((ℝ+ ⊆ ℂ ∧ ℝ ⊆ ℂ)
→ (ℝ+–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t
ℝ+) Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
45 | 23, 16, 44 | mp2an 708 |
. . . . . . . 8
⊢
(ℝ+–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t
ℝ+) Cn ((TopOpen‘ℂfld)
↾t ℝ)) |
46 | 42, 45 | eleqtri 2699 |
. . . . . . 7
⊢ (log
↾ ℝ+) ∈ (((TopOpen‘ℂfld)
↾t ℝ+) Cn
((TopOpen‘ℂfld) ↾t
ℝ)) |
47 | 46 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (log ↾
ℝ+) ∈ (((TopOpen‘ℂfld)
↾t ℝ+) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
48 | 19, 41, 47 | cnmpt11f 21467 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ ((log ↾
ℝ+)‘(𝑥 + 1))) ∈
(((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
49 | 12, 37, 43 | cncfcn 22712 |
. . . . . 6
⊢
(((0[,]𝐴) ⊆
ℂ ∧ ℝ ⊆ ℂ) → ((0[,]𝐴)–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
50 | 17, 16, 49 | sylancl 694 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((0[,]𝐴)–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
51 | 48, 50 | eleqtrrd 2704 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ ((log ↾
ℝ+)‘(𝑥 + 1))) ∈ ((0[,]𝐴)–cn→ℝ)) |
52 | 11, 51 | eqeltrrd 2702 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (log‘(𝑥 + 1))) ∈ ((0[,]𝐴)–cn→ℝ)) |
53 | | reelprrecn 10028 |
. . . . 5
⊢ ℝ
∈ {ℝ, ℂ} |
54 | 53 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ℝ ∈
{ℝ, ℂ}) |
55 | | simpr 477 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
56 | | 1rp 11836 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
57 | | rpaddcl 11854 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ∈ ℝ+) → (𝑥 + 1) ∈
ℝ+) |
58 | 55, 56, 57 | sylancl 694 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (𝑥 + 1) ∈
ℝ+) |
59 | 58 | relogcld 24369 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝑥 + 1)) ∈
ℝ) |
60 | 59 | recnd 10068 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝑥 + 1)) ∈
ℂ) |
61 | 58 | rpreccld 11882 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥 + 1)) ∈
ℝ+) |
62 | | 1cnd 10056 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℂ) |
63 | | relogcl 24322 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ (log‘𝑦) ∈
ℝ) |
64 | 63 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ+) →
(log‘𝑦) ∈
ℝ) |
65 | 64 | recnd 10068 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ+) →
(log‘𝑦) ∈
ℂ) |
66 | | rpreccl 11857 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℝ+) |
67 | 66 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ+) → (1 /
𝑦) ∈
ℝ+) |
68 | | peano2re 10209 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
69 | 68 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ) → (𝑥 + 1) ∈ ℝ) |
70 | 69 | recnd 10068 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ) → (𝑥 + 1) ∈ ℂ) |
71 | | 1cnd 10056 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) |
72 | 16 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ℝ ⊆
ℂ) |
73 | 72 | sselda 3603 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
74 | 54 | dvmptid 23720 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1)) |
75 | | 0cnd 10033 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ) → 0 ∈
ℂ) |
76 | 54, 29 | dvmptc 23721 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ 1)) =
(𝑥 ∈ ℝ ↦
0)) |
77 | 54, 73, 71, 74, 71, 75, 76 | dvmptadd 23723 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ (𝑥 + 1))) = (𝑥 ∈ ℝ ↦ (1 +
0))) |
78 | | 1p0e1 11133 |
. . . . . . . . 9
⊢ (1 + 0) =
1 |
79 | 78 | mpteq2i 4741 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ (1 + 0))
= (𝑥 ∈ ℝ ↦
1) |
80 | 77, 79 | syl6eq 2672 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ (𝑥 + 1))) = (𝑥 ∈ ℝ ↦ 1)) |
81 | 22 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
ℝ+ ⊆ ℝ) |
82 | 12 | tgioo2 22606 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
83 | | ioorp 12251 |
. . . . . . . . 9
⊢
(0(,)+∞) = ℝ+ |
84 | | iooretop 22569 |
. . . . . . . . 9
⊢
(0(,)+∞) ∈ (topGen‘ran (,)) |
85 | 83, 84 | eqeltrri 2698 |
. . . . . . . 8
⊢
ℝ+ ∈ (topGen‘ran (,)) |
86 | 85 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
ℝ+ ∈ (topGen‘ran (,))) |
87 | 54, 70, 71, 80, 81, 82, 12, 86 | dvmptres 23726 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ+
↦ (𝑥 + 1))) = (𝑥 ∈ ℝ+
↦ 1)) |
88 | | dvrelog 24383 |
. . . . . . 7
⊢ (ℝ
D (log ↾ ℝ+)) = (𝑦 ∈ ℝ+ ↦ (1 /
𝑦)) |
89 | | relogf1o 24313 |
. . . . . . . . . . 11
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ |
90 | | f1of 6137 |
. . . . . . . . . . 11
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) |
91 | 89, 90 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (log ↾
ℝ+):ℝ+⟶ℝ) |
92 | 91 | feqmptd 6249 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (log ↾
ℝ+) = (𝑦
∈ ℝ+ ↦ ((log ↾
ℝ+)‘𝑦))) |
93 | | fvres 6207 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ+
→ ((log ↾ ℝ+)‘𝑦) = (log‘𝑦)) |
94 | 93 | mpteq2ia 4740 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
↦ ((log ↾ ℝ+)‘𝑦)) = (𝑦 ∈ ℝ+ ↦
(log‘𝑦)) |
95 | 92, 94 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (log ↾
ℝ+) = (𝑦
∈ ℝ+ ↦ (log‘𝑦))) |
96 | 95 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (log
↾ ℝ+)) = (ℝ D (𝑦 ∈ ℝ+ ↦
(log‘𝑦)))) |
97 | 88, 96 | syl5reqr 2671 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑦 ∈ ℝ+
↦ (log‘𝑦))) =
(𝑦 ∈
ℝ+ ↦ (1 / 𝑦))) |
98 | | fveq2 6191 |
. . . . . 6
⊢ (𝑦 = (𝑥 + 1) → (log‘𝑦) = (log‘(𝑥 + 1))) |
99 | | oveq2 6658 |
. . . . . 6
⊢ (𝑦 = (𝑥 + 1) → (1 / 𝑦) = (1 / (𝑥 + 1))) |
100 | 54, 54, 58, 62, 65, 67, 87, 97, 98, 99 | dvmptco 23735 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ+
↦ (log‘(𝑥 +
1)))) = (𝑥 ∈
ℝ+ ↦ ((1 / (𝑥 + 1)) · 1))) |
101 | 61 | rpcnd 11874 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥 + 1)) ∈
ℂ) |
102 | 101 | mulid1d 10057 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → ((1 /
(𝑥 + 1)) · 1) = (1 /
(𝑥 + 1))) |
103 | 102 | mpteq2dva 4744 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ ℝ+
↦ ((1 / (𝑥 + 1))
· 1)) = (𝑥 ∈
ℝ+ ↦ (1 / (𝑥 + 1)))) |
104 | 100, 103 | eqtrd 2656 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ+
↦ (log‘(𝑥 +
1)))) = (𝑥 ∈
ℝ+ ↦ (1 / (𝑥 + 1)))) |
105 | | ioossicc 12259 |
. . . . . . . . 9
⊢
(0(,)𝐴) ⊆
(0[,]𝐴) |
106 | 105 | sseli 3599 |
. . . . . . . 8
⊢ (𝑥 ∈ (0(,)𝐴) → 𝑥 ∈ (0[,]𝐴)) |
107 | 106, 7 | sylan2 491 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0(,)𝐴)) → 𝑥 ∈ ℝ) |
108 | | eliooord 12233 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,)𝐴) → (0 < 𝑥 ∧ 𝑥 < 𝐴)) |
109 | 108 | simpld 475 |
. . . . . . . 8
⊢ (𝑥 ∈ (0(,)𝐴) → 0 < 𝑥) |
110 | 109 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0(,)𝐴)) → 0 < 𝑥) |
111 | 107, 110 | elrpd 11869 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0(,)𝐴)) → 𝑥 ∈ ℝ+) |
112 | 111 | ex 450 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0(,)𝐴) → 𝑥 ∈
ℝ+)) |
113 | 112 | ssrdv 3609 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (0(,)𝐴) ⊆
ℝ+) |
114 | | iooretop 22569 |
. . . . 5
⊢
(0(,)𝐴) ∈
(topGen‘ran (,)) |
115 | 114 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (0(,)𝐴) ∈ (topGen‘ran
(,))) |
116 | 54, 60, 61, 104, 113, 82, 12, 115 | dvmptres 23726 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ (0(,)𝐴) ↦ (log‘(𝑥 + 1)))) = (𝑥 ∈ (0(,)𝐴) ↦ (1 / (𝑥 + 1)))) |
117 | | elrege0 12278 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
118 | 7, 8, 117 | sylanbrc 698 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → 𝑥 ∈ (0[,)+∞)) |
119 | 118 | ex 450 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) → 𝑥 ∈ (0[,)+∞))) |
120 | 119 | ssrdv 3609 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (0[,]𝐴) ⊆
(0[,)+∞)) |
121 | 120 | resabs1d 5428 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((√ ↾
(0[,)+∞)) ↾ (0[,]𝐴)) = (√ ↾ (0[,]𝐴))) |
122 | | sqrtf 14103 |
. . . . . . 7
⊢
√:ℂ⟶ℂ |
123 | 122 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
√:ℂ⟶ℂ) |
124 | 123, 17 | feqresmpt 6250 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (√ ↾
(0[,]𝐴)) = (𝑥 ∈ (0[,]𝐴) ↦ (√‘𝑥))) |
125 | 121, 124 | eqtrd 2656 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((√ ↾
(0[,)+∞)) ↾ (0[,]𝐴)) = (𝑥 ∈ (0[,]𝐴) ↦ (√‘𝑥))) |
126 | | resqrtcn 24490 |
. . . . 5
⊢ (√
↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℝ) |
127 | | rescncf 22700 |
. . . . 5
⊢
((0[,]𝐴) ⊆
(0[,)+∞) → ((√ ↾ (0[,)+∞)) ∈
((0[,)+∞)–cn→ℝ)
→ ((√ ↾ (0[,)+∞)) ↾ (0[,]𝐴)) ∈ ((0[,]𝐴)–cn→ℝ))) |
128 | 120, 126,
127 | mpisyl 21 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((√ ↾
(0[,)+∞)) ↾ (0[,]𝐴)) ∈ ((0[,]𝐴)–cn→ℝ)) |
129 | 125, 128 | eqeltrrd 2702 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (√‘𝑥)) ∈ ((0[,]𝐴)–cn→ℝ)) |
130 | | rpcn 11841 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
131 | 130 | adantl 482 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
132 | 131 | sqrtcld 14176 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℂ) |
133 | | 2rp 11837 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
134 | | rpsqrtcl 14005 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (√‘𝑥)
∈ ℝ+) |
135 | 134 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ+) |
136 | | rpmulcl 11855 |
. . . . . 6
⊢ ((2
∈ ℝ+ ∧ (√‘𝑥) ∈ ℝ+) → (2
· (√‘𝑥))
∈ ℝ+) |
137 | 133, 135,
136 | sylancr 695 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (2
· (√‘𝑥))
∈ ℝ+) |
138 | 137 | rpreccld 11882 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (1 / (2
· (√‘𝑥))) ∈
ℝ+) |
139 | | dvsqrt 24483 |
. . . . 5
⊢ (ℝ
D (𝑥 ∈
ℝ+ ↦ (√‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 / (2
· (√‘𝑥)))) |
140 | 139 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ+
↦ (√‘𝑥)))
= (𝑥 ∈
ℝ+ ↦ (1 / (2 · (√‘𝑥))))) |
141 | 54, 132, 138, 140, 113, 82, 12, 115 | dvmptres 23726 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ (0(,)𝐴) ↦ (√‘𝑥))) = (𝑥 ∈ (0(,)𝐴) ↦ (1 / (2 ·
(√‘𝑥))))) |
142 | 135 | rpred 11872 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ) |
143 | | 1re 10039 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
144 | | resubcl 10345 |
. . . . . . . . 9
⊢
(((√‘𝑥)
∈ ℝ ∧ 1 ∈ ℝ) → ((√‘𝑥) − 1) ∈
ℝ) |
145 | 142, 143,
144 | sylancl 694 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
((√‘𝑥) −
1) ∈ ℝ) |
146 | 145 | sqge0d 13036 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → 0 ≤
(((√‘𝑥) −
1)↑2)) |
147 | 131 | sqsqrtd 14178 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
((√‘𝑥)↑2)
= 𝑥) |
148 | 147 | oveq1d 6665 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(((√‘𝑥)↑2)
− (2 · (√‘𝑥))) = (𝑥 − (2 · (√‘𝑥)))) |
149 | 148 | oveq1d 6665 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
((((√‘𝑥)↑2) − (2 ·
(√‘𝑥))) + 1) =
((𝑥 − (2 ·
(√‘𝑥))) +
1)) |
150 | | binom2sub1 12982 |
. . . . . . . . 9
⊢
((√‘𝑥)
∈ ℂ → (((√‘𝑥) − 1)↑2) =
((((√‘𝑥)↑2) − (2 ·
(√‘𝑥))) +
1)) |
151 | 132, 150 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(((√‘𝑥) −
1)↑2) = ((((√‘𝑥)↑2) − (2 ·
(√‘𝑥))) +
1)) |
152 | 137 | rpcnd 11874 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (2
· (√‘𝑥))
∈ ℂ) |
153 | 131, 62, 152 | addsubd 10413 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → ((𝑥 + 1) − (2 ·
(√‘𝑥))) =
((𝑥 − (2 ·
(√‘𝑥))) +
1)) |
154 | 149, 151,
153 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(((√‘𝑥) −
1)↑2) = ((𝑥 + 1)
− (2 · (√‘𝑥)))) |
155 | 146, 154 | breqtrd 4679 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → 0 ≤
((𝑥 + 1) − (2
· (√‘𝑥)))) |
156 | 58 | rpred 11872 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (𝑥 + 1) ∈
ℝ) |
157 | 137 | rpred 11872 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (2
· (√‘𝑥))
∈ ℝ) |
158 | 156, 157 | subge0d 10617 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (0 ≤
((𝑥 + 1) − (2
· (√‘𝑥))) ↔ (2 · (√‘𝑥)) ≤ (𝑥 + 1))) |
159 | 155, 158 | mpbid 222 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (2
· (√‘𝑥))
≤ (𝑥 +
1)) |
160 | 137, 58 | lerecd 11891 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → ((2
· (√‘𝑥))
≤ (𝑥 + 1) ↔ (1 /
(𝑥 + 1)) ≤ (1 / (2
· (√‘𝑥))))) |
161 | 159, 160 | mpbid 222 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥 + 1)) ≤ (1 / (2
· (√‘𝑥)))) |
162 | 111, 161 | syldan 487 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0(,)𝐴)) → (1 / (𝑥 + 1)) ≤ (1 / (2 ·
(√‘𝑥)))) |
163 | | rexr 10085 |
. . . 4
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
164 | | 0xr 10086 |
. . . . 5
⊢ 0 ∈
ℝ* |
165 | | lbicc2 12288 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 ≤
𝐴) → 0 ∈
(0[,]𝐴)) |
166 | 164, 165 | mp3an1 1411 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) → 0
∈ (0[,]𝐴)) |
167 | 163, 166 | sylan 488 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 0 ∈
(0[,]𝐴)) |
168 | | ubicc2 12289 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 ≤
𝐴) → 𝐴 ∈ (0[,]𝐴)) |
169 | 164, 168 | mp3an1 1411 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) →
𝐴 ∈ (0[,]𝐴)) |
170 | 163, 169 | sylan 488 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 𝐴 ∈ (0[,]𝐴)) |
171 | | simpr 477 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 0 ≤ 𝐴) |
172 | | oveq1 6657 |
. . . . . 6
⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1)) |
173 | | 0p1e1 11132 |
. . . . . 6
⊢ (0 + 1) =
1 |
174 | 172, 173 | syl6eq 2672 |
. . . . 5
⊢ (𝑥 = 0 → (𝑥 + 1) = 1) |
175 | 174 | fveq2d 6195 |
. . . 4
⊢ (𝑥 = 0 → (log‘(𝑥 + 1)) =
(log‘1)) |
176 | | log1 24332 |
. . . 4
⊢
(log‘1) = 0 |
177 | 175, 176 | syl6eq 2672 |
. . 3
⊢ (𝑥 = 0 → (log‘(𝑥 + 1)) = 0) |
178 | | fveq2 6191 |
. . . 4
⊢ (𝑥 = 0 → (√‘𝑥) =
(√‘0)) |
179 | | sqrt0 13982 |
. . . 4
⊢
(√‘0) = 0 |
180 | 178, 179 | syl6eq 2672 |
. . 3
⊢ (𝑥 = 0 → (√‘𝑥) = 0) |
181 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥 + 1) = (𝐴 + 1)) |
182 | 181 | fveq2d 6195 |
. . 3
⊢ (𝑥 = 𝐴 → (log‘(𝑥 + 1)) = (log‘(𝐴 + 1))) |
183 | | fveq2 6191 |
. . 3
⊢ (𝑥 = 𝐴 → (√‘𝑥) = (√‘𝐴)) |
184 | 2, 3, 52, 116, 129, 141, 162, 167, 170, 171, 177, 180, 182, 183 | dvle 23770 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
((log‘(𝐴 + 1))
− 0) ≤ ((√‘𝐴) − 0)) |
185 | | ge0p1rp 11862 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝐴 + 1) ∈
ℝ+) |
186 | 185 | relogcld 24369 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (log‘(𝐴 + 1)) ∈
ℝ) |
187 | | resqrtcl 13994 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(√‘𝐴) ∈
ℝ) |
188 | 186, 187,
2 | lesub1d 10634 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
((log‘(𝐴 + 1)) ≤
(√‘𝐴) ↔
((log‘(𝐴 + 1))
− 0) ≤ ((√‘𝐴) − 0))) |
189 | 184, 188 | mpbird 247 |
1
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (log‘(𝐴 + 1)) ≤ (√‘𝐴)) |