rprelogbdiv - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > rprelogbdiv		GIF version

Theorem rprelogbdiv 15499

Description: The logarithm of the quotient of two positive real numbers is the difference of logarithms. Property 3 of [Cohen4] p. 361. (Contributed by AV, 29-May-2020.)

**Assertion**
Ref	Expression
rprelogbdiv	⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → (𝐵 log_b (𝐴 / 𝐶)) = ((𝐵 log_b 𝐴) − (𝐵 log_b 𝐶)))

**Proof of Theorem rprelogbdiv**
Step	Hyp	Ref	Expression
1		neg1rr 9157	. . 3 ⊢ -1 ∈ ℝ
2		rprelogbmulexp 15498	. . 3 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺ ∧ -1 ∈ ℝ)) → (𝐵 log_b (𝐴 · (𝐶↑_𝑐-1))) = ((𝐵 log_b 𝐴) + (-1 · (𝐵 log_b 𝐶))))
3	1, 2	mp3anr3 1349	. 2 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → (𝐵 log_b (𝐴 · (𝐶↑_𝑐-1))) = ((𝐵 log_b 𝐴) + (-1 · (𝐵 log_b 𝐶))))
4		rpcn 9799	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℂ)
5	4	adantr 276	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺) → 𝐴 ∈ ℂ)
6		rpcn 9799	. . . . . . 7 ⊢ (𝐶 ∈ ℝ⁺ → 𝐶 ∈ ℂ)
7	6	adantl 277	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺) → 𝐶 ∈ ℂ)
8		rpap0 9807	. . . . . . 7 ⊢ (𝐶 ∈ ℝ⁺ → 𝐶 # 0)
9	8	adantl 277	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺) → 𝐶 # 0)
10	5, 7, 9	divrecapd 8881	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺) → (𝐴 / 𝐶) = (𝐴 · (1 / 𝐶)))
11		ax-1cn 8033	. . . . . . . . 9 ⊢ 1 ∈ ℂ
12		rpcxpneg 15449	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℝ⁺ ∧ 1 ∈ ℂ) → (𝐶↑_𝑐-1) = (1 / (𝐶↑_𝑐1)))
13	11, 12	mpan2 425	. . . . . . . 8 ⊢ (𝐶 ∈ ℝ⁺ → (𝐶↑_𝑐-1) = (1 / (𝐶↑_𝑐1)))
14		rpcxp1 15441	. . . . . . . . 9 ⊢ (𝐶 ∈ ℝ⁺ → (𝐶↑_𝑐1) = 𝐶)
15	14	oveq2d 5972	. . . . . . . 8 ⊢ (𝐶 ∈ ℝ⁺ → (1 / (𝐶↑_𝑐1)) = (1 / 𝐶))
16	13, 15	eqtrd 2239	. . . . . . 7 ⊢ (𝐶 ∈ ℝ⁺ → (𝐶↑_𝑐-1) = (1 / 𝐶))
17	16	adantl 277	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺) → (𝐶↑_𝑐-1) = (1 / 𝐶))
18	17	oveq2d 5972	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺) → (𝐴 · (𝐶↑_𝑐-1)) = (𝐴 · (1 / 𝐶)))
19	10, 18	eqtr4d 2242	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺) → (𝐴 / 𝐶) = (𝐴 · (𝐶↑_𝑐-1)))
20	19	adantl 277	. . 3 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → (𝐴 / 𝐶) = (𝐴 · (𝐶↑_𝑐-1)))
21	20	oveq2d 5972	. 2 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → (𝐵 log_b (𝐴 / 𝐶)) = (𝐵 log_b (𝐴 · (𝐶↑_𝑐-1))))
22		simpll 527	. . . . 5 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → 𝐵 ∈ ℝ⁺)
23		simplr 528	. . . . 5 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → 𝐵 # 1)
24		simprr 531	. . . . 5 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → 𝐶 ∈ ℝ⁺)
25		rplogbcl 15488	. . . . 5 ⊢ ((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1 ∧ 𝐶 ∈ ℝ⁺) → (𝐵 log_b 𝐶) ∈ ℝ)
26	22, 23, 24, 25	syl3anc 1250	. . . 4 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → (𝐵 log_b 𝐶) ∈ ℝ)
27		recn 8073	. . . 4 ⊢ ((𝐵 log_b 𝐶) ∈ ℝ → (𝐵 log_b 𝐶) ∈ ℂ)
28		mulm1 8487	. . . . 5 ⊢ ((𝐵 log_b 𝐶) ∈ ℂ → (-1 · (𝐵 log_b 𝐶)) = -(𝐵 log_b 𝐶))
29	28	oveq2d 5972	. . . 4 ⊢ ((𝐵 log_b 𝐶) ∈ ℂ → ((𝐵 log_b 𝐴) + (-1 · (𝐵 log_b 𝐶))) = ((𝐵 log_b 𝐴) + -(𝐵 log_b 𝐶)))
30	26, 27, 29	3syl 17	. . 3 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → ((𝐵 log_b 𝐴) + (-1 · (𝐵 log_b 𝐶))) = ((𝐵 log_b 𝐴) + -(𝐵 log_b 𝐶)))
31		simprl 529	. . . . . 6 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → 𝐴 ∈ ℝ⁺)
32		rplogbcl 15488	. . . . . 6 ⊢ ((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1 ∧ 𝐴 ∈ ℝ⁺) → (𝐵 log_b 𝐴) ∈ ℝ)
33	22, 23, 31, 32	syl3anc 1250	. . . . 5 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → (𝐵 log_b 𝐴) ∈ ℝ)
34	33	recnd 8116	. . . 4 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → (𝐵 log_b 𝐴) ∈ ℂ)
35	26	recnd 8116	. . . 4 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → (𝐵 log_b 𝐶) ∈ ℂ)
36	34, 35	negsubd 8404	. . 3 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → ((𝐵 log_b 𝐴) + -(𝐵 log_b 𝐶)) = ((𝐵 log_b 𝐴) − (𝐵 log_b 𝐶)))
37	30, 36	eqtr2d 2240	. 2 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → ((𝐵 log_b 𝐴) − (𝐵 log_b 𝐶)) = ((𝐵 log_b 𝐴) + (-1 · (𝐵 log_b 𝐶))))
38	3, 21, 37	3eqtr4d 2249	1 ⊢ (((𝐵 ∈ ℝ⁺ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ⁺ ∧ 𝐶 ∈ ℝ⁺)) → (𝐵 log_b (𝐴 / 𝐶)) = ((𝐵 log_b 𝐴) − (𝐵 log_b 𝐶)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1373 ∈ wcel 2177 class class class wbr 4050 (class class class)co 5956 ℂcc 7938 ℝcr 7939 0cc0 7940 1c1 7941 + caddc 7943 · cmul 7945 − cmin 8258 -cneg 8259 # cap 8669 / cdiv 8760 ℝ⁺crp 9790 ↑_𝑐ccxp 15399 log_b clogb 15485

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4166 ax-sep 4169 ax-nul 4177 ax-pow 4225 ax-pr 4260 ax-un 4487 ax-setind 4592 ax-iinf 4643 ax-cnex 8031 ax-resscn 8032 ax-1cn 8033 ax-1re 8034 ax-icn 8035 ax-addcl 8036 ax-addrcl 8037 ax-mulcl 8038 ax-mulrcl 8039 ax-addcom 8040 ax-mulcom 8041 ax-addass 8042 ax-mulass 8043 ax-distr 8044 ax-i2m1 8045 ax-0lt1 8046 ax-1rid 8047 ax-0id 8048 ax-rnegex 8049 ax-precex 8050 ax-cnre 8051 ax-pre-ltirr 8052 ax-pre-ltwlin 8053 ax-pre-lttrn 8054 ax-pre-apti 8055 ax-pre-ltadd 8056 ax-pre-mulgt0 8057 ax-pre-mulext 8058 ax-arch 8059 ax-caucvg 8060 ax-pre-suploc 8061 ax-addf 8062 ax-mulf 8063

This theorem depends on definitions: df-bi 117 df-stab 833 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-nul 3465 df-if 3576 df-pw 3622 df-sn 3643 df-pr 3644 df-op 3646 df-uni 3856 df-int 3891 df-iun 3934 df-disj 4027 df-br 4051 df-opab 4113 df-mpt 4114 df-tr 4150 df-id 4347 df-po 4350 df-iso 4351 df-iord 4420 df-on 4422 df-ilim 4423 df-suc 4425 df-iom 4646 df-xp 4688 df-rel 4689 df-cnv 4690 df-co 4691 df-dm 4692 df-rn 4693 df-res 4694 df-ima 4695 df-iota 5240 df-fun 5281 df-fn 5282 df-f 5283 df-f1 5284 df-fo 5285 df-f1o 5286 df-fv 5287 df-isom 5288 df-riota 5911 df-ov 5959 df-oprab 5960 df-mpo 5961 df-of 6170 df-1st 6238 df-2nd 6239 df-recs 6403 df-irdg 6468 df-frec 6489 df-1o 6514 df-oadd 6518 df-er 6632 df-map 6749 df-pm 6750 df-en 6840 df-dom 6841 df-fin 6842 df-sup 7100 df-inf 7101 df-pnf 8124 df-mnf 8125 df-xr 8126 df-ltxr 8127 df-le 8128 df-sub 8260 df-neg 8261 df-reap 8663 df-ap 8670 df-div 8761 df-inn 9052 df-2 9110 df-3 9111 df-4 9112 df-n0 9311 df-z 9388 df-uz 9664 df-q 9756 df-rp 9791 df-xneg 9909 df-xadd 9910 df-ioo 10029 df-ico 10031 df-icc 10032 df-fz 10146 df-fzo 10280 df-seqfrec 10610 df-exp 10701 df-fac 10888 df-bc 10910 df-ihash 10938 df-shft 11196 df-cj 11223 df-re 11224 df-im 11225 df-rsqrt 11379 df-abs 11380 df-clim 11660 df-sumdc 11735 df-ef 12029 df-e 12030 df-rest 13143 df-topgen 13162 df-psmet 14375 df-xmet 14376 df-met 14377 df-bl 14378 df-mopn 14379 df-top 14540 df-topon 14553 df-bases 14585 df-ntr 14638 df-cn 14730 df-cnp 14731 df-tx 14795 df-cncf 15113 df-limced 15198 df-dvap 15199 df-relog 15400 df-rpcxp 15401 df-logb 15486

This theorem is referenced by: logbrec 15502

W3C validator