dvrelog2 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvrelog2		Structured version Visualization version GIF version

Theorem dvrelog2 42864

Description: The derivative of the logarithm, ftc2 26234 version. (Contributed by metakunt, 11-Aug-2024.)

**Hypotheses**
Ref	Expression
dvrelog2.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
dvrelog2.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
dvrelog2.3	⊢ (𝜑 → 0 < 𝐴)
dvrelog2.4	⊢ (𝜑 → 𝐴 ≤ 𝐵)
dvrelog2.5	⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥))
dvrelog2.6	⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥))

**Assertion**
Ref	Expression
dvrelog2	⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝜑,𝑥 Allowed substitution hints: 𝐹(𝑥) 𝐺(𝑥)

Proof of Theorem dvrelog2 Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvrelog2.5	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥))
2	1	a1i 11	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥)))
3	2	oveq2d 7432	. . 3 ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥))))
4		reelprrecn 11203	. . . . 5 ⊢ ℝ ∈ {ℝ, ℂ}
5	4	a1i 11	. . . 4 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
6		rpssre 13036	. . . . . . . 8 ⊢ ℝ⁺ ⊆ ℝ
7		ax-resscn 11168	. . . . . . . 8 ⊢ ℝ ⊆ ℂ
8	6, 7	sstri 3947	. . . . . . 7 ⊢ ℝ⁺ ⊆ ℂ
9	8	sseli 3934	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
10	9	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
11		rpne0 13045	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
12	11	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ≠ 0)
13	10, 12	logcld 26766	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℂ)
14		1red 11220	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → 1 ∈ ℝ)
15	6	sseli 3934	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
16	14, 15, 11	redivcld 12054	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ → (1 / 𝑥) ∈ ℝ)
17	16	adantl 487	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (1 / 𝑥) ∈ ℝ)
18		logf1o 26760	. . . . . . . . . 10 ⊢ log:(ℂ ∖ {0})–1-1-onto→ran log
19		f1of 6824	. . . . . . . . . 10 ⊢ (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
20	18, 19	ax-mp 5	. . . . . . . . 9 ⊢ log:(ℂ ∖ {0})⟶ran log
21	20	a1i 11	. . . . . . . 8 ⊢ (𝜑 → log:(ℂ ∖ {0})⟶ran log)
22		0nrp 13065	. . . . . . . . . . . 12 ⊢ ¬ 0 ∈ ℝ⁺
23		disjsn 4679	. . . . . . . . . . . 12 ⊢ ((ℝ⁺ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℝ⁺)
24	22, 23	mpbir 234	. . . . . . . . . . 11 ⊢ (ℝ⁺ ∩ {0}) = ∅
25		disjdif2 4443	. . . . . . . . . . 11 ⊢ ((ℝ⁺ ∩ {0}) = ∅ → (ℝ⁺ ∖ {0}) = ℝ⁺)
26	24, 25	ax-mp 5	. . . . . . . . . 10 ⊢ (ℝ⁺ ∖ {0}) = ℝ⁺
27		ssdif 4098	. . . . . . . . . . 11 ⊢ (ℝ⁺ ⊆ ℂ → (ℝ⁺ ∖ {0}) ⊆ (ℂ ∖ {0}))
28	8, 27	ax-mp 5	. . . . . . . . . 10 ⊢ (ℝ⁺ ∖ {0}) ⊆ (ℂ ∖ {0})
29	26, 28	eqsstrri 3985	. . . . . . . . 9 ⊢ ℝ⁺ ⊆ (ℂ ∖ {0})
30	29	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ⁺ ⊆ (ℂ ∖ {0}))
31	21, 30	feqresmpt 6954	. . . . . . 7 ⊢ (𝜑 → (log ↾ ℝ⁺) = (𝑥 ∈ ℝ⁺ ↦ (log‘𝑥)))
32	31	eqcomd 2771	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (log‘𝑥)) = (log ↾ ℝ⁺))
33	32	oveq2d 7432	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ⁺ ↦ (log‘𝑥))) = (ℝ D (log ↾ ℝ⁺)))
34		dvrelog 26833	. . . . . 6 ⊢ (ℝ D (log ↾ ℝ⁺)) = (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥))
35	34	a1i 11	. . . . 5 ⊢ (𝜑 → (ℝ D (log ↾ ℝ⁺)) = (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)))
36	33, 35	eqtrd 2800	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ⁺ ↦ (log‘𝑥))) = (𝑥 ∈ ℝ⁺ ↦ (1 / 𝑥)))
37		dvrelog2.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
38		dvrelog2.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
39		elicc2 13450	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)))
40	37, 38, 39	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)))
41	40	biimpa 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))
42	41	simp1d 1160	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ)
43		0red 11222	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 0 ∈ ℝ)
44	37	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
45		dvrelog2.3	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝐴)
46	45	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 0 < 𝐴)
47	41	simp2d 1161	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑦)
48	43, 44, 42, 46, 47	ltletrd 11381	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 0 < 𝑦)
49	42, 48	jca 521	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ ℝ ∧ 0 < 𝑦))
50		elrp 13030	. . . . . . 7 ⊢ (𝑦 ∈ ℝ⁺ ↔ (𝑦 ∈ ℝ ∧ 0 < 𝑦))
51	49, 50	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ⁺)
52	51	ex 418	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) → 𝑦 ∈ ℝ⁺))
53	52	ssrdv 3944	. . . 4 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ⁺)
54		tgioo4 24993	. . . 4 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
55		eqid 2765	. . . 4 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
56		iccntr 25010	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
57	37, 38, 56	syl2anc 596	. . . 4 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
58	5, 13, 17, 36, 53, 54, 55, 57	dvmptres2 26152	. . 3 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥)))
59	3, 58	eqtrd 2800	. 2 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥)))
60		dvrelog2.6	. . . 4 ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥))
61	60	a1i 11	. . 3 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥)))
62	61	eqcomd 2771	. 2 ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥)) = 𝐺)
63	59, 62	eqtrd 2800	1 ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∖ cdif 3903 ∩ cin 3905 ⊆ wss 3906 ∅c0 4286 {csn 4591 {cpr 4593 class class class wbr 5111 ↦ cmpt 5194 ran crn 5664 ↾ cres 5665 ⟶wf 6536 –1-1-onto→wf1o 6539 ‘cfv 6540 (class class class)co 7416 ℂcc 11109 ℝcr 11110 0cc0 11111 1c1 11112 < clt 11254 ≤ cle 11255 / cdiv 11882 ℝ⁺crp 13028 (,)cioo 13384 [,]cicc 13387 TopOpenctopn 17492 topGenctg 17508 ℂ_fldccnfld 21552 intcnt 23204 D cdv 26053 logclog 26750

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7738 ax-inf2 9613 ax-cnex 11167 ax-resscn 11168 ax-1cn 11169 ax-icn 11170 ax-addcl 11171 ax-addrcl 11172 ax-mulcl 11173 ax-mulrcl 11174 ax-mulcom 11175 ax-addass 11176 ax-mulass 11177 ax-distr 11178 ax-i2m1 11179 ax-1ne0 11180 ax-1rid 11181 ax-rnegex 11182 ax-rrecex 11183 ax-cnre 11184 ax-pre-lttri 11185 ax-pre-lttrn 11186 ax-pre-ltadd 11187 ax-pre-mulgt0 11188 ax-pre-sup 11189 ax-addf 11190

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7680 df-om 7865 df-1st 7988 df-2nd 7989 df-supp 8159 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-er 8696 df-map 8828 df-pm 8829 df-ixp 8898 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fsupp 9325 df-fi 9374 df-sup 9405 df-inf 9406 df-oi 9475 df-card 9937 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11454 df-neg 11455 df-div 11883 df-nn 12245 df-2 12314 df-3 12315 df-4 12316 df-5 12317 df-6 12318 df-7 12319 df-8 12320 df-9 12321 df-n0 12516 df-z 12603 df-dec 12724 df-uz 12875 df-q 12985 df-rp 13029 df-xneg 13149 df-xadd 13150 df-xmul 13151 df-ioo 13388 df-ioc 13389 df-ico 13390 df-icc 13391 df-fz 13548 df-fzo 13696 df-fl 13839 df-mod 13917 df-seq 14052 df-exp 14112 df-fac 14324 df-bc 14353 df-hash 14381 df-shft 15124 df-cj 15170 df-re 15171 df-im 15172 df-sqrt 15306 df-abs 15307 df-limsup 15542 df-clim 15559 df-rlim 15560 df-sum 15758 df-ef 16139 df-sin 16141 df-cos 16142 df-pi 16144 df-struct 17225 df-sets 17242 df-slot 17260 df-ndx 17272 df-base 17288 df-ress 17309 df-plusg 17341 df-mulr 17342 df-starv 17343 df-sca 17344 df-vsca 17345 df-ip 17346 df-tset 17347 df-ple 17348 df-ds 17350 df-unif 17351 df-hom 17352 df-cco 17353 df-rest 17493 df-topn 17494 df-0g 17512 df-gsum 17513 df-topgen 17514 df-pt 17515 df-prds 17518 df-xrs 17574 df-qtop 17579 df-imas 17580 df-xps 17582 df-mre 17656 df-mrc 17657 df-acs 17659 df-mgm 18716 df-sgrp 18799 df-mnd 18815 df-submnd 18866 df-mulg 19158 df-cntz 19411 df-cmn 19876 df-psmet 21544 df-xmet 21545 df-met 21546 df-bl 21547 df-mopn 21548 df-fbas 21549 df-fg 21550 df-cnfld 21553 df-top 23081 df-topon 23098 df-topsp 23120 df-bases 23133 df-cld 23206 df-ntr 23207 df-cls 23208 df-nei 23285 df-lp 23323 df-perf 23324 df-cn 23414 df-cnp 23415 df-haus 23502 df-cmp 23574 df-tx 23750 df-hmeo 23943 df-fil 24034 df-fm 24126 df-flim 24127 df-flf 24128 df-xms 24508 df-ms 24509 df-tms 24510 df-cncf 25068 df-limc 26056 df-dv 26057 df-log 26752

This theorem is used by: (None)

W3C validator