MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  loglesqrt Structured version   Visualization version   GIF version

Theorem loglesqrt 26606
Description: An upper bound on the logarithm. (Contributed by Mario Carneiro, 2-May-2016.) (Proof shortened by AV, 2-Aug-2021.)
Assertion
Ref Expression
loglesqrt ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log‘(𝐴 + 1)) ≤ (√‘𝐴))

Proof of Theorem loglesqrt
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0re 11223 . . . 4 0 ∈ ℝ
21a1i 11 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 0 ∈ ℝ)
3 simpl 482 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 𝐴 ∈ ℝ)
4 elicc2 13396 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥 ∈ (0[,]𝐴) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥𝐴)))
51, 3, 4sylancr 586 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥𝐴)))
65biimpa 476 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥𝐴))
76simp1d 1141 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → 𝑥 ∈ ℝ)
86simp2d 1142 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → 0 ≤ 𝑥)
97, 8ge0p1rpd 13053 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → (𝑥 + 1) ∈ ℝ+)
109fvresd 6911 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → ((log ↾ ℝ+)‘(𝑥 + 1)) = (log‘(𝑥 + 1)))
1110mpteq2dva 5248 . . . 4 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ ((log ↾ ℝ+)‘(𝑥 + 1))) = (𝑥 ∈ (0[,]𝐴) ↦ (log‘(𝑥 + 1))))
12 eqid 2731 . . . . . . . 8 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
1312cnfldtopon 24618 . . . . . . 7 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
147ex 412 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) → 𝑥 ∈ ℝ))
1514ssrdv 3988 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (0[,]𝐴) ⊆ ℝ)
16 ax-resscn 11173 . . . . . . . 8 ℝ ⊆ ℂ
1715, 16sstrdi 3994 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (0[,]𝐴) ⊆ ℂ)
18 resttopon 22984 . . . . . . 7 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (0[,]𝐴) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (0[,]𝐴)) ∈ (TopOn‘(0[,]𝐴)))
1913, 17, 18sylancr 586 . . . . . 6 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((TopOpen‘ℂfld) ↾t (0[,]𝐴)) ∈ (TopOn‘(0[,]𝐴)))
209fmpttd 7116 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)):(0[,]𝐴)⟶ℝ+)
21 rpssre 12988 . . . . . . . . . 10 + ⊆ ℝ
2221, 16sstri 3991 . . . . . . . . 9 + ⊆ ℂ
2312addcn 24700 . . . . . . . . . . 11 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
2423a1i 11 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
25 ssid 4004 . . . . . . . . . . 11 ℂ ⊆ ℂ
26 cncfmptid 24752 . . . . . . . . . . 11 (((0[,]𝐴) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (0[,]𝐴) ↦ 𝑥) ∈ ((0[,]𝐴)–cn→ℂ))
2717, 25, 26sylancl 585 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ 𝑥) ∈ ((0[,]𝐴)–cn→ℂ))
28 1cnd 11216 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 1 ∈ ℂ)
2925a1i 11 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ℂ ⊆ ℂ)
30 cncfmptc 24751 . . . . . . . . . . 11 ((1 ∈ ℂ ∧ (0[,]𝐴) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (0[,]𝐴) ↦ 1) ∈ ((0[,]𝐴)–cn→ℂ))
3128, 17, 29, 30syl3anc 1370 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ 1) ∈ ((0[,]𝐴)–cn→ℂ))
3212, 24, 27, 31cncfmpt2f 24754 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℂ))
33 cncfcdm 24737 . . . . . . . . 9 ((ℝ+ ⊆ ℂ ∧ (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℂ)) → ((𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℝ+) ↔ (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)):(0[,]𝐴)⟶ℝ+))
3422, 32, 33sylancr 586 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℝ+) ↔ (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)):(0[,]𝐴)⟶ℝ+))
3520, 34mpbird 257 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ ((0[,]𝐴)–cn→ℝ+))
36 eqid 2731 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t (0[,]𝐴)) = ((TopOpen‘ℂfld) ↾t (0[,]𝐴))
37 eqid 2731 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t+) = ((TopOpen‘ℂfld) ↾t+)
3812, 36, 37cncfcn 24749 . . . . . . . 8 (((0[,]𝐴) ⊆ ℂ ∧ ℝ+ ⊆ ℂ) → ((0[,]𝐴)–cn→ℝ+) = (((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn ((TopOpen‘ℂfld) ↾t+)))
3917, 22, 38sylancl 585 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((0[,]𝐴)–cn→ℝ+) = (((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn ((TopOpen‘ℂfld) ↾t+)))
4035, 39eleqtrd 2834 . . . . . 6 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (𝑥 + 1)) ∈ (((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn ((TopOpen‘ℂfld) ↾t+)))
41 relogcn 26485 . . . . . . . 8 (log ↾ ℝ+) ∈ (ℝ+cn→ℝ)
42 eqid 2731 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t ℝ) = ((TopOpen‘ℂfld) ↾t ℝ)
4312, 37, 42cncfcn 24749 . . . . . . . . 9 ((ℝ+ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (ℝ+cn→ℝ) = (((TopOpen‘ℂfld) ↾t+) Cn ((TopOpen‘ℂfld) ↾t ℝ)))
4422, 16, 43mp2an 689 . . . . . . . 8 (ℝ+cn→ℝ) = (((TopOpen‘ℂfld) ↾t+) Cn ((TopOpen‘ℂfld) ↾t ℝ))
4541, 44eleqtri 2830 . . . . . . 7 (log ↾ ℝ+) ∈ (((TopOpen‘ℂfld) ↾t+) Cn ((TopOpen‘ℂfld) ↾t ℝ))
4645a1i 11 . . . . . 6 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log ↾ ℝ+) ∈ (((TopOpen‘ℂfld) ↾t+) Cn ((TopOpen‘ℂfld) ↾t ℝ)))
4719, 40, 46cnmpt11f 23487 . . . . 5 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ ((log ↾ ℝ+)‘(𝑥 + 1))) ∈ (((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn ((TopOpen‘ℂfld) ↾t ℝ)))
4812, 36, 42cncfcn 24749 . . . . . 6 (((0[,]𝐴) ⊆ ℂ ∧ ℝ ⊆ ℂ) → ((0[,]𝐴)–cn→ℝ) = (((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn ((TopOpen‘ℂfld) ↾t ℝ)))
4917, 16, 48sylancl 585 . . . . 5 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((0[,]𝐴)–cn→ℝ) = (((TopOpen‘ℂfld) ↾t (0[,]𝐴)) Cn ((TopOpen‘ℂfld) ↾t ℝ)))
5047, 49eleqtrrd 2835 . . . 4 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ ((log ↾ ℝ+)‘(𝑥 + 1))) ∈ ((0[,]𝐴)–cn→ℝ))
5111, 50eqeltrrd 2833 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (log‘(𝑥 + 1))) ∈ ((0[,]𝐴)–cn→ℝ))
52 reelprrecn 11208 . . . . 5 ℝ ∈ {ℝ, ℂ}
5352a1i 11 . . . 4 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ℝ ∈ {ℝ, ℂ})
54 simpr 484 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
55 1rp 12985 . . . . . . 7 1 ∈ ℝ+
56 rpaddcl 13003 . . . . . . 7 ((𝑥 ∈ ℝ+ ∧ 1 ∈ ℝ+) → (𝑥 + 1) ∈ ℝ+)
5754, 55, 56sylancl 585 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (𝑥 + 1) ∈ ℝ+)
5857relogcld 26470 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (log‘(𝑥 + 1)) ∈ ℝ)
5958recnd 11249 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (log‘(𝑥 + 1)) ∈ ℂ)
6057rpreccld 13033 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (1 / (𝑥 + 1)) ∈ ℝ+)
61 1cnd 11216 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℂ)
62 relogcl 26423 . . . . . . . 8 (𝑦 ∈ ℝ+ → (log‘𝑦) ∈ ℝ)
6362adantl 481 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑦 ∈ ℝ+) → (log‘𝑦) ∈ ℝ)
6463recnd 11249 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑦 ∈ ℝ+) → (log‘𝑦) ∈ ℂ)
65 rpreccl 13007 . . . . . . 7 (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ+)
6665adantl 481 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑦 ∈ ℝ+) → (1 / 𝑦) ∈ ℝ+)
67 peano2re 11394 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
6867adantl 481 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ) → (𝑥 + 1) ∈ ℝ)
6968recnd 11249 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ) → (𝑥 + 1) ∈ ℂ)
70 1cnd 11216 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
7116a1i 11 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ℝ ⊆ ℂ)
7271sselda 3982 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
7353dvmptid 25808 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
74 0cnd 11214 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℂ)
7553, 28dvmptc 25809 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ 1)) = (𝑥 ∈ ℝ ↦ 0))
7653, 72, 70, 73, 70, 74, 75dvmptadd 25811 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ (𝑥 + 1))) = (𝑥 ∈ ℝ ↦ (1 + 0)))
77 1p0e1 12343 . . . . . . . . 9 (1 + 0) = 1
7877mpteq2i 5253 . . . . . . . 8 (𝑥 ∈ ℝ ↦ (1 + 0)) = (𝑥 ∈ ℝ ↦ 1)
7976, 78eqtrdi 2787 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ ↦ (𝑥 + 1))) = (𝑥 ∈ ℝ ↦ 1))
8021a1i 11 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ℝ+ ⊆ ℝ)
8112tgioo2 24638 . . . . . . 7 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
82 ioorp 13409 . . . . . . . . 9 (0(,)+∞) = ℝ+
83 iooretop 24601 . . . . . . . . 9 (0(,)+∞) ∈ (topGen‘ran (,))
8482, 83eqeltrri 2829 . . . . . . . 8 + ∈ (topGen‘ran (,))
8584a1i 11 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ℝ+ ∈ (topGen‘ran (,)))
8653, 69, 70, 79, 80, 81, 12, 85dvmptres 25814 . . . . . 6 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + 1))) = (𝑥 ∈ ℝ+ ↦ 1))
87 relogf1o 26414 . . . . . . . . . . 11 (log ↾ ℝ+):ℝ+1-1-onto→ℝ
88 f1of 6833 . . . . . . . . . . 11 ((log ↾ ℝ+):ℝ+1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
8987, 88mp1i 13 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log ↾ ℝ+):ℝ+⟶ℝ)
9089feqmptd 6960 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log ↾ ℝ+) = (𝑦 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑦)))
91 fvres 6910 . . . . . . . . . 10 (𝑦 ∈ ℝ+ → ((log ↾ ℝ+)‘𝑦) = (log‘𝑦))
9291mpteq2ia 5251 . . . . . . . . 9 (𝑦 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑦)) = (𝑦 ∈ ℝ+ ↦ (log‘𝑦))
9390, 92eqtrdi 2787 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log ↾ ℝ+) = (𝑦 ∈ ℝ+ ↦ (log‘𝑦)))
9493oveq2d 7428 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℝ D (log ↾ ℝ+)) = (ℝ D (𝑦 ∈ ℝ+ ↦ (log‘𝑦))))
95 dvrelog 26484 . . . . . . 7 (ℝ D (log ↾ ℝ+)) = (𝑦 ∈ ℝ+ ↦ (1 / 𝑦))
9694, 95eqtr3di 2786 . . . . . 6 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℝ D (𝑦 ∈ ℝ+ ↦ (log‘𝑦))) = (𝑦 ∈ ℝ+ ↦ (1 / 𝑦)))
97 fveq2 6891 . . . . . 6 (𝑦 = (𝑥 + 1) → (log‘𝑦) = (log‘(𝑥 + 1)))
98 oveq2 7420 . . . . . 6 (𝑦 = (𝑥 + 1) → (1 / 𝑦) = (1 / (𝑥 + 1)))
9953, 53, 57, 61, 64, 66, 86, 96, 97, 98dvmptco 25823 . . . . 5 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘(𝑥 + 1)))) = (𝑥 ∈ ℝ+ ↦ ((1 / (𝑥 + 1)) · 1)))
10060rpcnd 13025 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (1 / (𝑥 + 1)) ∈ ℂ)
101100mulridd 11238 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((1 / (𝑥 + 1)) · 1) = (1 / (𝑥 + 1)))
102101mpteq2dva 5248 . . . . 5 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ ℝ+ ↦ ((1 / (𝑥 + 1)) · 1)) = (𝑥 ∈ ℝ+ ↦ (1 / (𝑥 + 1))))
10399, 102eqtrd 2771 . . . 4 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘(𝑥 + 1)))) = (𝑥 ∈ ℝ+ ↦ (1 / (𝑥 + 1))))
104 ioossicc 13417 . . . . . . . . 9 (0(,)𝐴) ⊆ (0[,]𝐴)
105104sseli 3978 . . . . . . . 8 (𝑥 ∈ (0(,)𝐴) → 𝑥 ∈ (0[,]𝐴))
106105, 7sylan2 592 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ (0(,)𝐴)) → 𝑥 ∈ ℝ)
107 eliooord 13390 . . . . . . . . 9 (𝑥 ∈ (0(,)𝐴) → (0 < 𝑥𝑥 < 𝐴))
108107simpld 494 . . . . . . . 8 (𝑥 ∈ (0(,)𝐴) → 0 < 𝑥)
109108adantl 481 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ (0(,)𝐴)) → 0 < 𝑥)
110106, 109elrpd 13020 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ (0(,)𝐴)) → 𝑥 ∈ ℝ+)
111110ex 412 . . . . 5 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0(,)𝐴) → 𝑥 ∈ ℝ+))
112111ssrdv 3988 . . . 4 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (0(,)𝐴) ⊆ ℝ+)
113 iooretop 24601 . . . . 5 (0(,)𝐴) ∈ (topGen‘ran (,))
114113a1i 11 . . . 4 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (0(,)𝐴) ∈ (topGen‘ran (,)))
11553, 59, 60, 103, 112, 81, 12, 114dvmptres 25814 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℝ D (𝑥 ∈ (0(,)𝐴) ↦ (log‘(𝑥 + 1)))) = (𝑥 ∈ (0(,)𝐴) ↦ (1 / (𝑥 + 1))))
116 elrege0 13438 . . . . . . . . 9 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
1177, 8, 116sylanbrc 582 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ (0[,]𝐴)) → 𝑥 ∈ (0[,)+∞))
118117ex 412 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) → 𝑥 ∈ (0[,)+∞)))
119118ssrdv 3988 . . . . . 6 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (0[,]𝐴) ⊆ (0[,)+∞))
120119resabs1d 6012 . . . . 5 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√ ↾ (0[,)+∞)) ↾ (0[,]𝐴)) = (√ ↾ (0[,]𝐴)))
121 sqrtf 15317 . . . . . . 7 √:ℂ⟶ℂ
122121a1i 11 . . . . . 6 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → √:ℂ⟶ℂ)
123122, 17feqresmpt 6961 . . . . 5 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√ ↾ (0[,]𝐴)) = (𝑥 ∈ (0[,]𝐴) ↦ (√‘𝑥)))
124120, 123eqtrd 2771 . . . 4 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√ ↾ (0[,)+∞)) ↾ (0[,]𝐴)) = (𝑥 ∈ (0[,]𝐴) ↦ (√‘𝑥)))
125 resqrtcn 26597 . . . . 5 (√ ↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℝ)
126 rescncf 24736 . . . . 5 ((0[,]𝐴) ⊆ (0[,)+∞) → ((√ ↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℝ) → ((√ ↾ (0[,)+∞)) ↾ (0[,]𝐴)) ∈ ((0[,]𝐴)–cn→ℝ)))
127119, 125, 126mpisyl 21 . . . 4 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√ ↾ (0[,)+∞)) ↾ (0[,]𝐴)) ∈ ((0[,]𝐴)–cn→ℝ))
128124, 127eqeltrrd 2833 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑥 ∈ (0[,]𝐴) ↦ (√‘𝑥)) ∈ ((0[,]𝐴)–cn→ℝ))
129 rpcn 12991 . . . . . 6 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
130129adantl 481 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
131130sqrtcld 15391 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (√‘𝑥) ∈ ℂ)
132 2rp 12986 . . . . . 6 2 ∈ ℝ+
133 rpsqrtcl 15218 . . . . . . 7 (𝑥 ∈ ℝ+ → (√‘𝑥) ∈ ℝ+)
134133adantl 481 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (√‘𝑥) ∈ ℝ+)
135 rpmulcl 13004 . . . . . 6 ((2 ∈ ℝ+ ∧ (√‘𝑥) ∈ ℝ+) → (2 · (√‘𝑥)) ∈ ℝ+)
136132, 134, 135sylancr 586 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (2 · (√‘𝑥)) ∈ ℝ+)
137136rpreccld 13033 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (1 / (2 · (√‘𝑥))) ∈ ℝ+)
138 dvsqrt 26589 . . . . 5 (ℝ D (𝑥 ∈ ℝ+ ↦ (√‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑥))))
139138a1i 11 . . . 4 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ (√‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑥)))))
14053, 131, 137, 139, 112, 81, 12, 114dvmptres 25814 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℝ D (𝑥 ∈ (0(,)𝐴) ↦ (√‘𝑥))) = (𝑥 ∈ (0(,)𝐴) ↦ (1 / (2 · (√‘𝑥)))))
141134rpred 13023 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (√‘𝑥) ∈ ℝ)
142 1re 11221 . . . . . . . . 9 1 ∈ ℝ
143 resubcl 11531 . . . . . . . . 9 (((√‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ) → ((√‘𝑥) − 1) ∈ ℝ)
144141, 142, 143sylancl 585 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((√‘𝑥) − 1) ∈ ℝ)
145144sqge0d 14109 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 0 ≤ (((√‘𝑥) − 1)↑2))
146130sqsqrtd 15393 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((√‘𝑥)↑2) = 𝑥)
147146oveq1d 7427 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (((√‘𝑥)↑2) − (2 · (√‘𝑥))) = (𝑥 − (2 · (√‘𝑥))))
148147oveq1d 7427 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((((√‘𝑥)↑2) − (2 · (√‘𝑥))) + 1) = ((𝑥 − (2 · (√‘𝑥))) + 1))
149 binom2sub1 14191 . . . . . . . . 9 ((√‘𝑥) ∈ ℂ → (((√‘𝑥) − 1)↑2) = ((((√‘𝑥)↑2) − (2 · (√‘𝑥))) + 1))
150131, 149syl 17 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (((√‘𝑥) − 1)↑2) = ((((√‘𝑥)↑2) − (2 · (√‘𝑥))) + 1))
151136rpcnd 13025 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (2 · (√‘𝑥)) ∈ ℂ)
152130, 61, 151addsubd 11599 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((𝑥 + 1) − (2 · (√‘𝑥))) = ((𝑥 − (2 · (√‘𝑥))) + 1))
153148, 150, 1523eqtr4d 2781 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (((√‘𝑥) − 1)↑2) = ((𝑥 + 1) − (2 · (√‘𝑥))))
154145, 153breqtrd 5174 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 0 ≤ ((𝑥 + 1) − (2 · (√‘𝑥))))
15557rpred 13023 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (𝑥 + 1) ∈ ℝ)
156136rpred 13023 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (2 · (√‘𝑥)) ∈ ℝ)
157155, 156subge0d 11811 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (0 ≤ ((𝑥 + 1) − (2 · (√‘𝑥))) ↔ (2 · (√‘𝑥)) ≤ (𝑥 + 1)))
158154, 157mpbid 231 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (2 · (√‘𝑥)) ≤ (𝑥 + 1))
159136, 57lerecd 13042 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((2 · (√‘𝑥)) ≤ (𝑥 + 1) ↔ (1 / (𝑥 + 1)) ≤ (1 / (2 · (√‘𝑥)))))
160158, 159mpbid 231 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (1 / (𝑥 + 1)) ≤ (1 / (2 · (√‘𝑥))))
161110, 160syldan 590 . . 3 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑥 ∈ (0(,)𝐴)) → (1 / (𝑥 + 1)) ≤ (1 / (2 · (√‘𝑥))))
162 rexr 11267 . . . 4 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
163 0xr 11268 . . . . 5 0 ∈ ℝ*
164 lbicc2 13448 . . . . 5 ((0 ∈ ℝ*𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 0 ∈ (0[,]𝐴))
165163, 164mp3an1 1447 . . . 4 ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 0 ∈ (0[,]𝐴))
166162, 165sylan 579 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 0 ∈ (0[,]𝐴))
167 ubicc2 13449 . . . . 5 ((0 ∈ ℝ*𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ∈ (0[,]𝐴))
168163, 167mp3an1 1447 . . . 4 ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ∈ (0[,]𝐴))
169162, 168sylan 579 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 𝐴 ∈ (0[,]𝐴))
170 simpr 484 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 0 ≤ 𝐴)
171 fv0p1e1 12342 . . . 4 (𝑥 = 0 → (log‘(𝑥 + 1)) = (log‘1))
172 log1 26433 . . . 4 (log‘1) = 0
173171, 172eqtrdi 2787 . . 3 (𝑥 = 0 → (log‘(𝑥 + 1)) = 0)
174 fveq2 6891 . . . 4 (𝑥 = 0 → (√‘𝑥) = (√‘0))
175 sqrt0 15195 . . . 4 (√‘0) = 0
176174, 175eqtrdi 2787 . . 3 (𝑥 = 0 → (√‘𝑥) = 0)
177 fvoveq1 7435 . . 3 (𝑥 = 𝐴 → (log‘(𝑥 + 1)) = (log‘(𝐴 + 1)))
178 fveq2 6891 . . 3 (𝑥 = 𝐴 → (√‘𝑥) = (√‘𝐴))
1792, 3, 51, 115, 128, 140, 161, 166, 169, 170, 173, 176, 177, 178dvle 25859 . 2 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((log‘(𝐴 + 1)) − 0) ≤ ((√‘𝐴) − 0))
180 ge0p1rp 13012 . . . 4 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 + 1) ∈ ℝ+)
181180relogcld 26470 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log‘(𝐴 + 1)) ∈ ℝ)
182 resqrtcl 15207 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈ ℝ)
183181, 182, 2lesub1d 11828 . 2 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((log‘(𝐴 + 1)) ≤ (√‘𝐴) ↔ ((log‘(𝐴 + 1)) − 0) ≤ ((√‘𝐴) − 0)))
184179, 183mpbird 257 1 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log‘(𝐴 + 1)) ≤ (√‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1086   = wceq 1540  wcel 2105  wss 3948  {cpr 4630   class class class wbr 5148  cmpt 5231  ran crn 5677  cres 5678  wf 6539  1-1-ontowf1o 6542  cfv 6543  (class class class)co 7412  cc 11114  cr 11115  0cc0 11116  1c1 11117   + caddc 11119   · cmul 11121  +∞cpnf 11252  *cxr 11254   < clt 11255  cle 11256  cmin 11451   / cdiv 11878  2c2 12274  +crp 12981  (,)cioo 13331  [,)cico 13333  [,]cicc 13334  cexp 14034  csqrt 15187  t crest 17373  TopOpenctopn 17374  topGenctg 17390  fldccnfld 21232  TopOnctopon 22731   Cn ccn 23047   ×t ctx 23383  cnccncf 24715   D cdv 25711  logclog 26402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-inf2 9642  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193  ax-pre-sup 11194  ax-addf 11195
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7674  df-om 7860  df-1st 7979  df-2nd 7980  df-supp 8152  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-1o 8472  df-2o 8473  df-er 8709  df-map 8828  df-pm 8829  df-ixp 8898  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-fsupp 9368  df-fi 9412  df-sup 9443  df-inf 9444  df-oi 9511  df-card 9940  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-div 11879  df-nn 12220  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12480  df-z 12566  df-dec 12685  df-uz 12830  df-q 12940  df-rp 12982  df-xneg 13099  df-xadd 13100  df-xmul 13101  df-ioo 13335  df-ioc 13336  df-ico 13337  df-icc 13338  df-fz 13492  df-fzo 13635  df-fl 13764  df-mod 13842  df-seq 13974  df-exp 14035  df-fac 14241  df-bc 14270  df-hash 14298  df-shft 15021  df-cj 15053  df-re 15054  df-im 15055  df-sqrt 15189  df-abs 15190  df-limsup 15422  df-clim 15439  df-rlim 15440  df-sum 15640  df-ef 16018  df-sin 16020  df-cos 16021  df-tan 16022  df-pi 16023  df-struct 17087  df-sets 17104  df-slot 17122  df-ndx 17134  df-base 17152  df-ress 17181  df-plusg 17217  df-mulr 17218  df-starv 17219  df-sca 17220  df-vsca 17221  df-ip 17222  df-tset 17223  df-ple 17224  df-ds 17226  df-unif 17227  df-hom 17228  df-cco 17229  df-rest 17375  df-topn 17376  df-0g 17394  df-gsum 17395  df-topgen 17396  df-pt 17397  df-prds 17400  df-xrs 17455  df-qtop 17460  df-imas 17461  df-xps 17463  df-mre 17537  df-mrc 17538  df-acs 17540  df-mgm 18571  df-sgrp 18650  df-mnd 18666  df-submnd 18712  df-mulg 18994  df-cntz 19229  df-cmn 19698  df-psmet 21224  df-xmet 21225  df-met 21226  df-bl 21227  df-mopn 21228  df-fbas 21229  df-fg 21230  df-cnfld 21233  df-top 22715  df-topon 22732  df-topsp 22754  df-bases 22768  df-cld 22842  df-ntr 22843  df-cls 22844  df-nei 22921  df-lp 22959  df-perf 22960  df-cn 23050  df-cnp 23051  df-haus 23138  df-cmp 23210  df-tx 23385  df-hmeo 23578  df-fil 23669  df-fm 23761  df-flim 23762  df-flf 23763  df-xms 24145  df-ms 24146  df-tms 24147  df-cncf 24717  df-limc 25714  df-dv 25715  df-log 26404  df-cxp 26405
This theorem is referenced by:  rplogsumlem1  27329
  Copyright terms: Public domain W3C validator