logdiflbnd - Metamath Proof Explorer

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

Theorem logdiflbnd 27020

Description: Lower bound on the difference of logs. (Contributed by Mario Carneiro, 3-Jul-2017.)

**Assertion**
Ref	Expression
logdiflbnd	⊢ (𝐴 ∈ ℝ⁺ → (1 / (𝐴 + 1)) ≤ ((log‘(𝐴 + 1)) − (log‘𝐴)))

**Proof of Theorem logdiflbnd**
Step	Hyp	Ref	Expression
1		rpre 13040	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ)
2		rpge0 13045	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → 0 ≤ 𝐴)
3	1, 2	ge0p1rpd 13104	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 + 1) ∈ ℝ⁺)
4	3	rprecred 13085	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → (1 / (𝐴 + 1)) ∈ ℝ)
5		1red 11266	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → 1 ∈ ℝ)
6		0le1 11788	. . . . . . 7 ⊢ 0 ≤ 1
7	6	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → 0 ≤ 1)
8	5, 3, 7	divge0d 13114	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → 0 ≤ (1 / (𝐴 + 1)))
9		id 22	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ⁺)
10	5, 9	ltaddrp2d 13108	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → 1 < (𝐴 + 1))
11	1, 5	readdcld 11294	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 + 1) ∈ ℝ)
12	11	recnd 11293	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 + 1) ∈ ℂ)
13	12	mulridd 11282	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 + 1) · 1) = (𝐴 + 1))
14	10, 13	breqtrrd 5182	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → 1 < ((𝐴 + 1) · 1))
15	5, 5, 3	ltdivmuld 13125	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → ((1 / (𝐴 + 1)) < 1 ↔ 1 < ((𝐴 + 1) · 1)))
16	14, 15	mpbird 256	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → (1 / (𝐴 + 1)) < 1)
17	4, 8, 16	eflegeo 16136	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → (exp‘(1 / (𝐴 + 1))) ≤ (1 / (1 − (1 / (𝐴 + 1)))))
18	5	recnd 11293	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → 1 ∈ ℂ)
19	3	rpne0d 13079	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 + 1) ≠ 0)
20	12, 18, 12, 19	divsubdird 12084	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → (((𝐴 + 1) − 1) / (𝐴 + 1)) = (((𝐴 + 1) / (𝐴 + 1)) − (1 / (𝐴 + 1))))
21	1	recnd 11293	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℂ)
22	21, 18	pncand 11623	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 + 1) − 1) = 𝐴)
23	22	oveq1d 7442	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → (((𝐴 + 1) − 1) / (𝐴 + 1)) = (𝐴 / (𝐴 + 1)))
24	12, 19	dividd 12043	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 + 1) / (𝐴 + 1)) = 1)
25	24	oveq1d 7442	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → (((𝐴 + 1) / (𝐴 + 1)) − (1 / (𝐴 + 1))) = (1 − (1 / (𝐴 + 1))))
26	20, 23, 25	3eqtr3rd 2778	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → (1 − (1 / (𝐴 + 1))) = (𝐴 / (𝐴 + 1)))
27	26	oveq2d 7443	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → (1 / (1 − (1 / (𝐴 + 1)))) = (1 / (𝐴 / (𝐴 + 1))))
28		rpne0 13048	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → 𝐴 ≠ 0)
29	21, 12, 28, 19	recdivd 12062	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → (1 / (𝐴 / (𝐴 + 1))) = ((𝐴 + 1) / 𝐴))
30	27, 29	eqtrd 2769	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → (1 / (1 − (1 / (𝐴 + 1)))) = ((𝐴 + 1) / 𝐴))
31	17, 30	breqtrd 5180	. . 3 ⊢ (𝐴 ∈ ℝ⁺ → (exp‘(1 / (𝐴 + 1))) ≤ ((𝐴 + 1) / 𝐴))
32	4	rpefcld 16120	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → (exp‘(1 / (𝐴 + 1))) ∈ ℝ⁺)
33	3, 9	rpdivcld 13091	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 + 1) / 𝐴) ∈ ℝ⁺)
34	32, 33	logled 26651	. . 3 ⊢ (𝐴 ∈ ℝ⁺ → ((exp‘(1 / (𝐴 + 1))) ≤ ((𝐴 + 1) / 𝐴) ↔ (log‘(exp‘(1 / (𝐴 + 1)))) ≤ (log‘((𝐴 + 1) / 𝐴))))
35	31, 34	mpbid 231	. 2 ⊢ (𝐴 ∈ ℝ⁺ → (log‘(exp‘(1 / (𝐴 + 1)))) ≤ (log‘((𝐴 + 1) / 𝐴)))
36	4	relogefd 26652	. 2 ⊢ (𝐴 ∈ ℝ⁺ → (log‘(exp‘(1 / (𝐴 + 1)))) = (1 / (𝐴 + 1)))
37	3, 9	relogdivd 26650	. 2 ⊢ (𝐴 ∈ ℝ⁺ → (log‘((𝐴 + 1) / 𝐴)) = ((log‘(𝐴 + 1)) − (log‘𝐴)))
38	35, 36, 37	3brtr3d 5185	1 ⊢ (𝐴 ∈ ℝ⁺ → (1 / (𝐴 + 1)) ≤ ((log‘(𝐴 + 1)) − (log‘𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2100 class class class wbr 5154 ‘cfv 6556 (class class class)co 7427 0cc0 11159 1c1 11160 + caddc 11162 · cmul 11164 < clt 11299 ≤ cle 11300 − cmin 11495 / cdiv 11922 ℝ⁺crp 13032 expce 16076 logclog 26578

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2102 ax-9 2110 ax-10 2133 ax-11 2150 ax-12 2170 ax-ext 2700 ax-rep 5291 ax-sep 5305 ax-nul 5312 ax-pow 5371 ax-pr 5435 ax-un 7748 ax-inf2 9685 ax-cnex 11215 ax-resscn 11216 ax-1cn 11217 ax-icn 11218 ax-addcl 11219 ax-addrcl 11220 ax-mulcl 11221 ax-mulrcl 11222 ax-mulcom 11223 ax-addass 11224 ax-mulass 11225 ax-distr 11226 ax-i2m1 11227 ax-1ne0 11228 ax-1rid 11229 ax-rnegex 11230 ax-rrecex 11231 ax-cnre 11232 ax-pre-lttri 11233 ax-pre-lttrn 11234 ax-pre-ltadd 11235 ax-pre-mulgt0 11236 ax-pre-sup 11237 ax-addf 11238

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2062 df-mo 2532 df-eu 2561 df-clab 2707 df-cleq 2721 df-clel 2806 df-nfc 2881 df-ne 2934 df-nel 3040 df-ral 3055 df-rex 3064 df-rmo 3373 df-reu 3374 df-rab 3429 df-v 3474 df-sbc 3788 df-csb 3904 df-dif 3961 df-un 3963 df-in 3965 df-ss 3975 df-pss 3978 df-nul 4334 df-if 4535 df-pw 4610 df-sn 4635 df-pr 4637 df-tp 4639 df-op 4641 df-uni 4917 df-int 4958 df-iun 5006 df-iin 5007 df-br 5155 df-opab 5217 df-mpt 5238 df-tr 5272 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5639 df-se 5640 df-we 5641 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6315 df-ord 6381 df-on 6382 df-lim 6383 df-suc 6384 df-iota 6508 df-fun 6558 df-fn 6559 df-f 6560 df-f1 6561 df-fo 6562 df-f1o 6563 df-fv 6564 df-isom 6565 df-riota 7383 df-ov 7430 df-oprab 7431 df-mpo 7432 df-of 7692 df-om 7882 df-1st 8008 df-2nd 8009 df-supp 8180 df-frecs 8300 df-wrecs 8331 df-recs 8405 df-rdg 8444 df-1o 8500 df-2o 8501 df-er 8738 df-map 8861 df-pm 8862 df-ixp 8931 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-fsupp 9407 df-fi 9455 df-sup 9486 df-inf 9487 df-oi 9554 df-card 9983 df-pnf 11301 df-mnf 11302 df-xr 11303 df-ltxr 11304 df-le 11305 df-sub 11497 df-neg 11498 df-div 11923 df-nn 12269 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-7 12336 df-8 12337 df-9 12338 df-n0 12529 df-z 12615 df-dec 12734 df-uz 12879 df-q 12989 df-rp 13033 df-xneg 13150 df-xadd 13151 df-xmul 13152 df-ioo 13386 df-ioc 13387 df-ico 13388 df-icc 13389 df-fz 13543 df-fzo 13686 df-fl 13817 df-mod 13895 df-seq 14027 df-exp 14087 df-fac 14297 df-bc 14326 df-hash 14354 df-shft 15085 df-cj 15117 df-re 15118 df-im 15119 df-sqrt 15253 df-abs 15254 df-limsup 15486 df-clim 15503 df-rlim 15504 df-sum 15704 df-ef 16082 df-sin 16084 df-cos 16085 df-pi 16087 df-struct 17162 df-sets 17179 df-slot 17197 df-ndx 17209 df-base 17227 df-ress 17256 df-plusg 17292 df-mulr 17293 df-starv 17294 df-sca 17295 df-vsca 17296 df-ip 17297 df-tset 17298 df-ple 17299 df-ds 17301 df-unif 17302 df-hom 17303 df-cco 17304 df-rest 17450 df-topn 17451 df-0g 17469 df-gsum 17470 df-topgen 17471 df-pt 17472 df-prds 17475 df-xrs 17530 df-qtop 17535 df-imas 17536 df-xps 17538 df-mre 17612 df-mrc 17613 df-acs 17615 df-mgm 18646 df-sgrp 18725 df-mnd 18741 df-submnd 18787 df-mulg 19076 df-cntz 19325 df-cmn 19792 df-psmet 21347 df-xmet 21348 df-met 21349 df-bl 21350 df-mopn 21351 df-fbas 21352 df-fg 21353 df-cnfld 21356 df-top 22887 df-topon 22904 df-topsp 22926 df-bases 22940 df-cld 23014 df-ntr 23015 df-cls 23016 df-nei 23093 df-lp 23131 df-perf 23132 df-cn 23222 df-cnp 23223 df-haus 23310 df-tx 23557 df-hmeo 23750 df-fil 23841 df-fm 23933 df-flim 23934 df-flf 23935 df-xms 24317 df-ms 24318 df-tms 24319 df-cncf 24889 df-limc 25886 df-dv 25887 df-log 26580

This theorem is referenced by: lgamgulmlem3 27056

W3C validator