Step | Hyp | Ref
| Expression |
1 | | 0re 10714 |
. . . 4
⊢ 0 ∈
ℝ |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 0 ∈
ℝ) |
3 | | simpl 486 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 𝐴 ∈ ℝ) |
4 | | elicc2 12879 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑥
∈ (0[,]𝐴) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥 ∧ 𝑥 ≤ 𝐴))) |
5 | 1, 3, 4 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴))) |
6 | 5 | biimpa 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴)) |
7 | 6 | simp1d 1143 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → 𝑥 ∈ ℝ) |
8 | 6 | simp2d 1144 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → 0 ≤ 𝑥) |
9 | 7, 8 | ge0p1rpd 12537 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → (𝑥 + 1) ∈
ℝ+) |
10 | 9 | fvresd 6688 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → ((log ↾
ℝ+)‘(𝑥 + 1)) = (log‘(𝑥 + 1))) |
11 | 10 | mpteq2dva 5122 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ ((log ↾
ℝ+)‘(𝑥 + 1))) = (𝑥 ∈ (0[,]𝐴) ↦ (log‘(𝑥 + 1)))) |
12 | | eqid 2738 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
13 | 12 | cnfldtopon 23528 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
14 | 7 | ex 416 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) → 𝑥 ∈ ℝ)) |
15 | 14 | ssrdv 3881 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (0[,]𝐴) ⊆
ℝ) |
16 | | ax-resscn 10665 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
17 | 15, 16 | sstrdi 3887 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (0[,]𝐴) ⊆
ℂ) |
18 | | resttopon 21905 |
. . . . . . 7
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (0[,]𝐴) ⊆
ℂ) → ((TopOpen‘ℂfld) ↾t
(0[,]𝐴)) ∈
(TopOn‘(0[,]𝐴))) |
19 | 13, 17, 18 | sylancr 590 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
((TopOpen‘ℂfld) ↾t (0[,]𝐴)) ∈
(TopOn‘(0[,]𝐴))) |
20 | 9 | fmpttd 6883 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)):(0[,]𝐴)⟶ℝ+) |
21 | | rpssre 12472 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ ℝ |
22 | 21, 16 | sstri 3884 |
. . . . . . . . 9
⊢
ℝ+ ⊆ ℂ |
23 | 12 | addcn 23610 |
. . . . . . . . . . 11
⊢ + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
24 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
25 | | ssid 3897 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
26 | | cncfmptid 23658 |
. . . . . . . . . . 11
⊢
(((0[,]𝐴) ⊆
ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (0[,]𝐴) ↦ 𝑥) ∈ ((0[,]𝐴)–cn→ℂ)) |
27 | 17, 25, 26 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ 𝑥) ∈ ((0[,]𝐴)–cn→ℂ)) |
28 | | 1cnd 10707 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 1 ∈
ℂ) |
29 | 25 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ℂ ⊆
ℂ) |
30 | | cncfmptc 23657 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (0[,]𝐴) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑥 ∈
(0[,]𝐴) ↦ 1) ∈
((0[,]𝐴)–cn→ℂ)) |
31 | 28, 17, 29, 30 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ 1) ∈ ((0[,]𝐴)–cn→ℂ)) |
32 | 12, 24, 27, 31 | cncfmpt2f 23660 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℂ)) |
33 | | cncffvrn 23643 |
. . . . . . . . 9
⊢
((ℝ+ ⊆ ℂ ∧ (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℂ)) → ((𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℝ+) ↔ (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)):(0[,]𝐴)⟶ℝ+)) |
34 | 22, 32, 33 | sylancr 590 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℝ+) ↔ (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)):(0[,]𝐴)⟶ℝ+)) |
35 | 20, 34 | mpbird 260 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℝ+)) |
36 | | eqid 2738 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t (0[,]𝐴)) =
((TopOpen‘ℂfld) ↾t (0[,]𝐴)) |
37 | | eqid 2738 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t
ℝ+) = ((TopOpen‘ℂfld)
↾t ℝ+) |
38 | 12, 36, 37 | cncfcn 23655 |
. . . . . . . 8
⊢
(((0[,]𝐴) ⊆
ℂ ∧ ℝ+ ⊆ ℂ) → ((0[,]𝐴)–cn→ℝ+) =
(((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn
((TopOpen‘ℂfld) ↾t
ℝ+))) |
39 | 17, 22, 38 | sylancl 589 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((0[,]𝐴)–cn→ℝ+) =
(((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn
((TopOpen‘ℂfld) ↾t
ℝ+))) |
40 | 35, 39 | eleqtrd 2835 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈
(((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn
((TopOpen‘ℂfld) ↾t
ℝ+))) |
41 | | relogcn 25373 |
. . . . . . . 8
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℝ) |
42 | | eqid 2738 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ℝ) =
((TopOpen‘ℂfld) ↾t
ℝ) |
43 | 12, 37, 42 | cncfcn 23655 |
. . . . . . . . 9
⊢
((ℝ+ ⊆ ℂ ∧ ℝ ⊆ ℂ)
→ (ℝ+–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t
ℝ+) Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
44 | 22, 16, 43 | mp2an 692 |
. . . . . . . 8
⊢
(ℝ+–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t
ℝ+) Cn ((TopOpen‘ℂfld)
↾t ℝ)) |
45 | 41, 44 | eleqtri 2831 |
. . . . . . 7
⊢ (log
↾ ℝ+) ∈ (((TopOpen‘ℂfld)
↾t ℝ+) Cn
((TopOpen‘ℂfld) ↾t
ℝ)) |
46 | 45 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (log ↾
ℝ+) ∈ (((TopOpen‘ℂfld)
↾t ℝ+) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
47 | 19, 40, 46 | cnmpt11f 22408 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ ((log ↾
ℝ+)‘(𝑥 + 1))) ∈
(((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
48 | 12, 36, 42 | cncfcn 23655 |
. . . . . 6
⊢
(((0[,]𝐴) ⊆
ℂ ∧ ℝ ⊆ ℂ) → ((0[,]𝐴)–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
49 | 17, 16, 48 | sylancl 589 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((0[,]𝐴)–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
50 | 47, 49 | eleqtrrd 2836 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ ((log ↾
ℝ+)‘(𝑥 + 1))) ∈ ((0[,]𝐴)–cn→ℝ)) |
51 | 11, 50 | eqeltrrd 2834 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (log‘(𝑥 + 1))) ∈ ((0[,]𝐴)–cn→ℝ)) |
52 | | reelprrecn 10700 |
. . . . 5
⊢ ℝ
∈ {ℝ, ℂ} |
53 | 52 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ℝ ∈
{ℝ, ℂ}) |
54 | | simpr 488 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
55 | | 1rp 12469 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
56 | | rpaddcl 12487 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ∈ ℝ+) → (𝑥 + 1) ∈
ℝ+) |
57 | 54, 55, 56 | sylancl 589 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (𝑥 + 1) ∈
ℝ+) |
58 | 57 | relogcld 25358 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝑥 + 1)) ∈
ℝ) |
59 | 58 | recnd 10740 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝑥 + 1)) ∈
ℂ) |
60 | 57 | rpreccld 12517 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥 + 1)) ∈
ℝ+) |
61 | | 1cnd 10707 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℂ) |
62 | | relogcl 25311 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ (log‘𝑦) ∈
ℝ) |
63 | 62 | adantl 485 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ+) →
(log‘𝑦) ∈
ℝ) |
64 | 63 | recnd 10740 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ+) →
(log‘𝑦) ∈
ℂ) |
65 | | rpreccl 12491 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℝ+) |
66 | 65 | adantl 485 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ+) → (1 /
𝑦) ∈
ℝ+) |
67 | | peano2re 10884 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
68 | 67 | adantl 485 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ) → (𝑥 + 1) ∈ ℝ) |
69 | 68 | recnd 10740 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ) → (𝑥 + 1) ∈ ℂ) |
70 | | 1cnd 10707 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) |
71 | 16 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ℝ ⊆
ℂ) |
72 | 71 | sselda 3875 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
73 | 53 | dvmptid 24701 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1)) |
74 | | 0cnd 10705 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ) → 0 ∈
ℂ) |
75 | 53, 28 | dvmptc 24702 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ 1)) =
(𝑥 ∈ ℝ ↦
0)) |
76 | 53, 72, 70, 73, 70, 74, 75 | dvmptadd 24704 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ (𝑥 + 1))) = (𝑥 ∈ ℝ ↦ (1 +
0))) |
77 | | 1p0e1 11833 |
. . . . . . . . 9
⊢ (1 + 0) =
1 |
78 | 77 | mpteq2i 5119 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ (1 + 0))
= (𝑥 ∈ ℝ ↦
1) |
79 | 76, 78 | eqtrdi 2789 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ (𝑥 + 1))) = (𝑥 ∈ ℝ ↦ 1)) |
80 | 21 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
ℝ+ ⊆ ℝ) |
81 | 12 | tgioo2 23548 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
82 | | ioorp 12892 |
. . . . . . . . 9
⊢
(0(,)+∞) = ℝ+ |
83 | | iooretop 23511 |
. . . . . . . . 9
⊢
(0(,)+∞) ∈ (topGen‘ran (,)) |
84 | 82, 83 | eqeltrri 2830 |
. . . . . . . 8
⊢
ℝ+ ∈ (topGen‘ran (,)) |
85 | 84 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
ℝ+ ∈ (topGen‘ran (,))) |
86 | 53, 69, 70, 79, 80, 81, 12, 85 | dvmptres 24707 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ+
↦ (𝑥 + 1))) = (𝑥 ∈ ℝ+
↦ 1)) |
87 | | dvrelog 25372 |
. . . . . . 7
⊢ (ℝ
D (log ↾ ℝ+)) = (𝑦 ∈ ℝ+ ↦ (1 /
𝑦)) |
88 | | relogf1o 25302 |
. . . . . . . . . . 11
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ |
89 | | f1of 6612 |
. . . . . . . . . . 11
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) |
90 | 88, 89 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (log ↾
ℝ+):ℝ+⟶ℝ) |
91 | 90 | feqmptd 6731 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (log ↾
ℝ+) = (𝑦
∈ ℝ+ ↦ ((log ↾
ℝ+)‘𝑦))) |
92 | | fvres 6687 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ+
→ ((log ↾ ℝ+)‘𝑦) = (log‘𝑦)) |
93 | 92 | mpteq2ia 5118 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
↦ ((log ↾ ℝ+)‘𝑦)) = (𝑦 ∈ ℝ+ ↦
(log‘𝑦)) |
94 | 91, 93 | eqtrdi 2789 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (log ↾
ℝ+) = (𝑦
∈ ℝ+ ↦ (log‘𝑦))) |
95 | 94 | oveq2d 7180 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (log
↾ ℝ+)) = (ℝ D (𝑦 ∈ ℝ+ ↦
(log‘𝑦)))) |
96 | 87, 95 | syl5reqr 2788 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑦 ∈ ℝ+
↦ (log‘𝑦))) =
(𝑦 ∈
ℝ+ ↦ (1 / 𝑦))) |
97 | | fveq2 6668 |
. . . . . 6
⊢ (𝑦 = (𝑥 + 1) → (log‘𝑦) = (log‘(𝑥 + 1))) |
98 | | oveq2 7172 |
. . . . . 6
⊢ (𝑦 = (𝑥 + 1) → (1 / 𝑦) = (1 / (𝑥 + 1))) |
99 | 53, 53, 57, 61, 64, 66, 86, 96, 97, 98 | dvmptco 24716 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ+
↦ (log‘(𝑥 +
1)))) = (𝑥 ∈
ℝ+ ↦ ((1 / (𝑥 + 1)) · 1))) |
100 | 60 | rpcnd 12509 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥 + 1)) ∈
ℂ) |
101 | 100 | mulid1d 10729 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → ((1 /
(𝑥 + 1)) · 1) = (1 /
(𝑥 + 1))) |
102 | 101 | mpteq2dva 5122 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ ℝ+
↦ ((1 / (𝑥 + 1))
· 1)) = (𝑥 ∈
ℝ+ ↦ (1 / (𝑥 + 1)))) |
103 | 99, 102 | eqtrd 2773 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ+
↦ (log‘(𝑥 +
1)))) = (𝑥 ∈
ℝ+ ↦ (1 / (𝑥 + 1)))) |
104 | | ioossicc 12900 |
. . . . . . . . 9
⊢
(0(,)𝐴) ⊆
(0[,]𝐴) |
105 | 104 | sseli 3871 |
. . . . . . . 8
⊢ (𝑥 ∈ (0(,)𝐴) → 𝑥 ∈ (0[,]𝐴)) |
106 | 105, 7 | sylan2 596 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0(,)𝐴)) → 𝑥 ∈ ℝ) |
107 | | eliooord 12873 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,)𝐴) → (0 < 𝑥 ∧ 𝑥 < 𝐴)) |
108 | 107 | simpld 498 |
. . . . . . . 8
⊢ (𝑥 ∈ (0(,)𝐴) → 0 < 𝑥) |
109 | 108 | adantl 485 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0(,)𝐴)) → 0 < 𝑥) |
110 | 106, 109 | elrpd 12504 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0(,)𝐴)) → 𝑥 ∈ ℝ+) |
111 | 110 | ex 416 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0(,)𝐴) → 𝑥 ∈
ℝ+)) |
112 | 111 | ssrdv 3881 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (0(,)𝐴) ⊆
ℝ+) |
113 | | iooretop 23511 |
. . . . 5
⊢
(0(,)𝐴) ∈
(topGen‘ran (,)) |
114 | 113 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (0(,)𝐴) ∈ (topGen‘ran
(,))) |
115 | 53, 59, 60, 103, 112, 81, 12, 114 | dvmptres 24707 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ (0(,)𝐴) ↦ (log‘(𝑥 + 1)))) = (𝑥 ∈ (0(,)𝐴) ↦ (1 / (𝑥 + 1)))) |
116 | | elrege0 12921 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
117 | 7, 8, 116 | sylanbrc 586 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → 𝑥 ∈ (0[,)+∞)) |
118 | 117 | ex 416 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) → 𝑥 ∈ (0[,)+∞))) |
119 | 118 | ssrdv 3881 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (0[,]𝐴) ⊆
(0[,)+∞)) |
120 | 119 | resabs1d 5850 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((√ ↾
(0[,)+∞)) ↾ (0[,]𝐴)) = (√ ↾ (0[,]𝐴))) |
121 | | sqrtf 14806 |
. . . . . . 7
⊢
√:ℂ⟶ℂ |
122 | 121 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
√:ℂ⟶ℂ) |
123 | 122, 17 | feqresmpt 6732 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (√ ↾
(0[,]𝐴)) = (𝑥 ∈ (0[,]𝐴) ↦ (√‘𝑥))) |
124 | 120, 123 | eqtrd 2773 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((√ ↾
(0[,)+∞)) ↾ (0[,]𝐴)) = (𝑥 ∈ (0[,]𝐴) ↦ (√‘𝑥))) |
125 | | resqrtcn 25482 |
. . . . 5
⊢ (√
↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℝ) |
126 | | rescncf 23642 |
. . . . 5
⊢
((0[,]𝐴) ⊆
(0[,)+∞) → ((√ ↾ (0[,)+∞)) ∈
((0[,)+∞)–cn→ℝ)
→ ((√ ↾ (0[,)+∞)) ↾ (0[,]𝐴)) ∈ ((0[,]𝐴)–cn→ℝ))) |
127 | 119, 125,
126 | mpisyl 21 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((√ ↾
(0[,)+∞)) ↾ (0[,]𝐴)) ∈ ((0[,]𝐴)–cn→ℝ)) |
128 | 124, 127 | eqeltrrd 2834 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (√‘𝑥)) ∈ ((0[,]𝐴)–cn→ℝ)) |
129 | | rpcn 12475 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
130 | 129 | adantl 485 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
131 | 130 | sqrtcld 14880 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℂ) |
132 | | 2rp 12470 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
133 | | rpsqrtcl 14707 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (√‘𝑥)
∈ ℝ+) |
134 | 133 | adantl 485 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ+) |
135 | | rpmulcl 12488 |
. . . . . 6
⊢ ((2
∈ ℝ+ ∧ (√‘𝑥) ∈ ℝ+) → (2
· (√‘𝑥))
∈ ℝ+) |
136 | 132, 134,
135 | sylancr 590 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (2
· (√‘𝑥))
∈ ℝ+) |
137 | 136 | rpreccld 12517 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (1 / (2
· (√‘𝑥))) ∈
ℝ+) |
138 | | dvsqrt 25475 |
. . . . 5
⊢ (ℝ
D (𝑥 ∈
ℝ+ ↦ (√‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 / (2
· (√‘𝑥)))) |
139 | 138 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ ℝ+
↦ (√‘𝑥)))
= (𝑥 ∈
ℝ+ ↦ (1 / (2 · (√‘𝑥))))) |
140 | 53, 131, 137, 139, 112, 81, 12, 114 | dvmptres 24707 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℝ D (𝑥 ∈ (0(,)𝐴) ↦ (√‘𝑥))) = (𝑥 ∈ (0(,)𝐴) ↦ (1 / (2 ·
(√‘𝑥))))) |
141 | 134 | rpred 12507 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ) |
142 | | 1re 10712 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
143 | | resubcl 11021 |
. . . . . . . . 9
⊢
(((√‘𝑥)
∈ ℝ ∧ 1 ∈ ℝ) → ((√‘𝑥) − 1) ∈
ℝ) |
144 | 141, 142,
143 | sylancl 589 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
((√‘𝑥) −
1) ∈ ℝ) |
145 | 144 | sqge0d 13697 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → 0 ≤
(((√‘𝑥) −
1)↑2)) |
146 | 130 | sqsqrtd 14882 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
((√‘𝑥)↑2)
= 𝑥) |
147 | 146 | oveq1d 7179 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(((√‘𝑥)↑2)
− (2 · (√‘𝑥))) = (𝑥 − (2 · (√‘𝑥)))) |
148 | 147 | oveq1d 7179 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
((((√‘𝑥)↑2) − (2 ·
(√‘𝑥))) + 1) =
((𝑥 − (2 ·
(√‘𝑥))) +
1)) |
149 | | binom2sub1 13667 |
. . . . . . . . 9
⊢
((√‘𝑥)
∈ ℂ → (((√‘𝑥) − 1)↑2) =
((((√‘𝑥)↑2) − (2 ·
(√‘𝑥))) +
1)) |
150 | 131, 149 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(((√‘𝑥) −
1)↑2) = ((((√‘𝑥)↑2) − (2 ·
(√‘𝑥))) +
1)) |
151 | 136 | rpcnd 12509 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (2
· (√‘𝑥))
∈ ℂ) |
152 | 130, 61, 151 | addsubd 11089 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → ((𝑥 + 1) − (2 ·
(√‘𝑥))) =
((𝑥 − (2 ·
(√‘𝑥))) +
1)) |
153 | 148, 150,
152 | 3eqtr4d 2783 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) →
(((√‘𝑥) −
1)↑2) = ((𝑥 + 1)
− (2 · (√‘𝑥)))) |
154 | 145, 153 | breqtrd 5053 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → 0 ≤
((𝑥 + 1) − (2
· (√‘𝑥)))) |
155 | 57 | rpred 12507 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (𝑥 + 1) ∈
ℝ) |
156 | 136 | rpred 12507 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (2
· (√‘𝑥))
∈ ℝ) |
157 | 155, 156 | subge0d 11301 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (0 ≤
((𝑥 + 1) − (2
· (√‘𝑥))) ↔ (2 · (√‘𝑥)) ≤ (𝑥 + 1))) |
158 | 154, 157 | mpbid 235 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (2
· (√‘𝑥))
≤ (𝑥 +
1)) |
159 | 136, 57 | lerecd 12526 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → ((2
· (√‘𝑥))
≤ (𝑥 + 1) ↔ (1 /
(𝑥 + 1)) ≤ (1 / (2
· (√‘𝑥))))) |
160 | 158, 159 | mpbid 235 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥 + 1)) ≤ (1 / (2
· (√‘𝑥)))) |
161 | 110, 160 | syldan 594 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ (0(,)𝐴)) → (1 / (𝑥 + 1)) ≤ (1 / (2 ·
(√‘𝑥)))) |
162 | | rexr 10758 |
. . . 4
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
163 | | 0xr 10759 |
. . . . 5
⊢ 0 ∈
ℝ* |
164 | | lbicc2 12931 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 ≤
𝐴) → 0 ∈
(0[,]𝐴)) |
165 | 163, 164 | mp3an1 1449 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) → 0
∈ (0[,]𝐴)) |
166 | 162, 165 | sylan 583 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 0 ∈
(0[,]𝐴)) |
167 | | ubicc2 12932 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 ≤
𝐴) → 𝐴 ∈ (0[,]𝐴)) |
168 | 163, 167 | mp3an1 1449 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) →
𝐴 ∈ (0[,]𝐴)) |
169 | 162, 168 | sylan 583 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 𝐴 ∈ (0[,]𝐴)) |
170 | | simpr 488 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 0 ≤ 𝐴) |
171 | | fv0p1e1 11832 |
. . . 4
⊢ (𝑥 = 0 → (log‘(𝑥 + 1)) =
(log‘1)) |
172 | | log1 25321 |
. . . 4
⊢
(log‘1) = 0 |
173 | 171, 172 | eqtrdi 2789 |
. . 3
⊢ (𝑥 = 0 → (log‘(𝑥 + 1)) = 0) |
174 | | fveq2 6668 |
. . . 4
⊢ (𝑥 = 0 → (√‘𝑥) =
(√‘0)) |
175 | | sqrt0 14684 |
. . . 4
⊢
(√‘0) = 0 |
176 | 174, 175 | eqtrdi 2789 |
. . 3
⊢ (𝑥 = 0 → (√‘𝑥) = 0) |
177 | | fvoveq1 7187 |
. . 3
⊢ (𝑥 = 𝐴 → (log‘(𝑥 + 1)) = (log‘(𝐴 + 1))) |
178 | | fveq2 6668 |
. . 3
⊢ (𝑥 = 𝐴 → (√‘𝑥) = (√‘𝐴)) |
179 | 2, 3, 51, 115, 128, 140, 161, 166, 169, 170, 173, 176, 177, 178 | dvle 24751 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
((log‘(𝐴 + 1))
− 0) ≤ ((√‘𝐴) − 0)) |
180 | | ge0p1rp 12496 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝐴 + 1) ∈
ℝ+) |
181 | 180 | relogcld 25358 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (log‘(𝐴 + 1)) ∈
ℝ) |
182 | | resqrtcl 14696 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(√‘𝐴) ∈
ℝ) |
183 | 181, 182,
2 | lesub1d 11318 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
((log‘(𝐴 + 1)) ≤
(√‘𝐴) ↔
((log‘(𝐴 + 1))
− 0) ≤ ((√‘𝐴) − 0))) |
184 | 179, 183 | mpbird 260 |
1
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (log‘(𝐴 + 1)) ≤ (√‘𝐴)) |