logdivlti - Intuitionistic Logic Explorer

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

Theorem logdivlti 13141

Description: The

function is strictly decreasing on the reals greater than

. (Contributed by Mario Carneiro, 14-Mar-2014.)

**Assertion**
Ref	Expression
logdivlti	$/\$ $/\$ $/\$

**Proof of Theorem logdivlti**
Step	Hyp	Ref	Expression
1		simpl2 986	. . . . . . . 8 $/\$ $/\$ $/\$
2		simpl3 987	. . . . . . . . . 10 $/\$ $/\$ $/\$
3		simpr 109	. . . . . . . . . 10 $/\$ $/\$ $/\$
4		ere 11544	. . . . . . . . . . 11
5		simpl1 985	. . . . . . . . . . 11 $/\$ $/\$ $/\$
6		lelttr 7944	. . . . . . . . . . 11 $/\$ $/\$ $/\$
7	4, 5, 1, 6	mp3an2i 1321	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
8	2, 3, 7	mp2and 430	. . . . . . . . 9 $/\$ $/\$ $/\$
9		epos 11654	. . . . . . . . . 10
10		0re 7857	. . . . . . . . . . 11
11		lttr 7930	. . . . . . . . . . 11 $/\$ $/\$ $/\$
12	10, 4, 1, 11	mp3an12i 1320	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
13	9, 12	mpani 427	. . . . . . . . 9 $/\$ $/\$ $/\$
14	8, 13	mpd 13	. . . . . . . 8 $/\$ $/\$ $/\$
15	1, 14	elrpd 9578	. . . . . . 7 $/\$ $/\$ $/\$
16		ltletr 7945	. . . . . . . . . . 11 $/\$ $/\$ $/\$
17	10, 4, 5, 16	mp3an12i 1320	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18	9, 17	mpani 427	. . . . . . . . 9 $/\$ $/\$ $/\$
19	2, 18	mpd 13	. . . . . . . 8 $/\$ $/\$ $/\$
20	5, 19	elrpd 9578	. . . . . . 7 $/\$ $/\$ $/\$
21	15, 20	rpdivcld 9599	. . . . . 6 $/\$ $/\$ $/\$
22		relogcl 13122	. . . . . 6
23	21, 22	syl 14	. . . . 5 $/\$ $/\$ $/\$
24	1, 20	rerpdivcld 9613	. . . . . 6 $/\$ $/\$ $/\$
25		1re 7856	. . . . . 6
26		resubcl 8118	. . . . . 6 $/\$
27	24, 25, 26	sylancl 410	. . . . 5 $/\$ $/\$ $/\$
28		relogcl 13122	. . . . . . 7
29	20, 28	syl 14	. . . . . 6 $/\$ $/\$ $/\$
30	27, 29	remulcld 7887	. . . . 5 $/\$ $/\$ $/\$
31		reeflog 13123	. . . . . . . . 9
32	21, 31	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$
33		ax-1cn 7804	. . . . . . . . 9
34	24	recnd 7885	. . . . . . . . 9 $/\$ $/\$ $/\$
35		pncan3 8062	. . . . . . . . 9 $/\$
36	33, 34, 35	sylancr 411	. . . . . . . 8 $/\$ $/\$ $/\$
37	32, 36	eqtr4d 2190	. . . . . . 7 $/\$ $/\$ $/\$
38	5	recnd 7885	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
39	38	mulid2d 7875	. . . . . . . . . . 11 $/\$ $/\$ $/\$
40	39, 3	eqbrtrd 3982	. . . . . . . . . 10 $/\$ $/\$ $/\$
41		1red 7872	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42		ltmuldiv 8724	. . . . . . . . . . 11 $/\$ $/\$ $/\$
43	41, 1, 5, 19, 42	syl112anc 1221	. . . . . . . . . 10 $/\$ $/\$ $/\$
44	40, 43	mpbid 146	. . . . . . . . 9 $/\$ $/\$ $/\$
45		difrp 9577	. . . . . . . . . 10 $/\$
46	25, 24, 45	sylancr 411	. . . . . . . . 9 $/\$ $/\$ $/\$
47	44, 46	mpbid 146	. . . . . . . 8 $/\$ $/\$ $/\$
48		efgt1p 11570	. . . . . . . 8
49	47, 48	syl 14	. . . . . . 7 $/\$ $/\$ $/\$
50	37, 49	eqbrtrd 3982	. . . . . 6 $/\$ $/\$ $/\$
51		eflt 13035	. . . . . . 7 $/\$
52	23, 27, 51	syl2anc 409	. . . . . 6 $/\$ $/\$ $/\$
53	50, 52	mpbird 166	. . . . 5 $/\$ $/\$ $/\$
54	27	recnd 7885	. . . . . . 7 $/\$ $/\$ $/\$
55	54	mulid1d 7874	. . . . . 6 $/\$ $/\$ $/\$
56		df-e 11523	. . . . . . . . 9
57		reeflog 13123	. . . . . . . . . . 11
58	20, 57	syl 14	. . . . . . . . . 10 $/\$ $/\$ $/\$
59	2, 58	breqtrrd 3988	. . . . . . . . 9 $/\$ $/\$ $/\$
60	56, 59	eqbrtrrid 3996	. . . . . . . 8 $/\$ $/\$ $/\$
61		efle 13036	. . . . . . . . 9 $/\$
62	25, 29, 61	sylancr 411	. . . . . . . 8 $/\$ $/\$ $/\$
63	60, 62	mpbird 166	. . . . . . 7 $/\$ $/\$ $/\$
64		posdif 8309	. . . . . . . . . 10 $/\$
65	25, 24, 64	sylancr 411	. . . . . . . . 9 $/\$ $/\$ $/\$
66	44, 65	mpbid 146	. . . . . . . 8 $/\$ $/\$ $/\$
67		lemul2 8707	. . . . . . . 8 $/\$ $/\$ $/\$
68	41, 29, 27, 66, 67	syl112anc 1221	. . . . . . 7 $/\$ $/\$ $/\$
69	63, 68	mpbid 146	. . . . . 6 $/\$ $/\$ $/\$
70	55, 69	eqbrtrrd 3984	. . . . 5 $/\$ $/\$ $/\$
71	23, 27, 30, 53, 70	ltletrd 8277	. . . 4 $/\$ $/\$ $/\$
72		relogdiv 13130	. . . . 5 $/\$
73	15, 20, 72	syl2anc 409	. . . 4 $/\$ $/\$ $/\$
74		1cnd 7873	. . . . . 6 $/\$ $/\$ $/\$
75	29	recnd 7885	. . . . . 6 $/\$ $/\$ $/\$
76	34, 74, 75	subdird 8269	. . . . 5 $/\$ $/\$ $/\$
77	1	recnd 7885	. . . . . . 7 $/\$ $/\$ $/\$
78	20	rpap0d 9587	. . . . . . 7 $/\$ $/\$ $/\$ #
79	77, 38, 75, 78	div32apd 8666	. . . . . 6 $/\$ $/\$ $/\$
80	75	mulid2d 7875	. . . . . 6 $/\$ $/\$ $/\$
81	79, 80	oveq12d 5832	. . . . 5 $/\$ $/\$ $/\$
82	76, 81	eqtrd 2187	. . . 4 $/\$ $/\$ $/\$
83	71, 73, 82	3brtr3d 3991	. . 3 $/\$ $/\$ $/\$
84		relogcl 13122	. . . . 5
85	15, 84	syl 14	. . . 4 $/\$ $/\$ $/\$
86	29, 20	rerpdivcld 9613	. . . . 5 $/\$ $/\$ $/\$
87	1, 86	remulcld 7887	. . . 4 $/\$ $/\$ $/\$
88	85, 87, 29	ltsub1d 8408	. . 3 $/\$ $/\$ $/\$
89	83, 88	mpbird 166	. 2 $/\$ $/\$ $/\$
90	85, 86, 15	ltdivmuld 9633	. 2 $/\$ $/\$ $/\$
91	89, 90	mpbird 166	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $/\$ w3a 963

wceq 1332

wcel 2125 class class class wbr 3961

cfv 5163 (class class class)co 5814

cc 7709

cr 7710

cc0 7711

c1 7712

caddc 7714

cmul 7716

clt 7891

cle 7892

cmin 8025

cdiv 8524

crp 9538

ce 11516

ceu 11517

clog 13116

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-13 2127 ax-14 2128 ax-ext 2136 ax-coll 4075 ax-sep 4078 ax-nul 4086 ax-pow 4130 ax-pr 4164 ax-un 4388 ax-setind 4490 ax-iinf 4541 ax-cnex 7802 ax-resscn 7803 ax-1cn 7804 ax-1re 7805 ax-icn 7806 ax-addcl 7807 ax-addrcl 7808 ax-mulcl 7809 ax-mulrcl 7810 ax-addcom 7811 ax-mulcom 7812 ax-addass 7813 ax-mulass 7814 ax-distr 7815 ax-i2m1 7816 ax-0lt1 7817 ax-1rid 7818 ax-0id 7819 ax-rnegex 7820 ax-precex 7821 ax-cnre 7822 ax-pre-ltirr 7823 ax-pre-ltwlin 7824 ax-pre-lttrn 7825 ax-pre-apti 7826 ax-pre-ltadd 7827 ax-pre-mulgt0 7828 ax-pre-mulext 7829 ax-arch 7830 ax-caucvg 7831 ax-pre-suploc 7832 ax-addf 7833 ax-mulf 7834

This theorem depends on definitions: df-bi 116 df-stab 817 df-dc 821 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1740 df-eu 2006 df-mo 2007 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ne 2325 df-nel 2420 df-ral 2437 df-rex 2438 df-reu 2439 df-rmo 2440 df-rab 2441 df-v 2711 df-sbc 2934 df-csb 3028 df-dif 3100 df-un 3102 df-in 3104 df-ss 3111 df-nul 3391 df-if 3502 df-pw 3541 df-sn 3562 df-pr 3563 df-op 3565 df-uni 3769 df-int 3804 df-iun 3847 df-disj 3939 df-br 3962 df-opab 4022 df-mpt 4023 df-tr 4059 df-id 4248 df-po 4251 df-iso 4252 df-iord 4321 df-on 4323 df-ilim 4324 df-suc 4326 df-iom 4544 df-xp 4585 df-rel 4586 df-cnv 4587 df-co 4588 df-dm 4589 df-rn 4590 df-res 4591 df-ima 4592 df-iota 5128 df-fun 5165 df-fn 5166 df-f 5167 df-f1 5168 df-fo 5169 df-f1o 5170 df-fv 5171 df-isom 5172 df-riota 5770 df-ov 5817 df-oprab 5818 df-mpo 5819 df-of 6022 df-1st 6078 df-2nd 6079 df-recs 6242 df-irdg 6307 df-frec 6328 df-1o 6353 df-oadd 6357 df-er 6469 df-map 6584 df-pm 6585 df-en 6675 df-dom 6676 df-fin 6677 df-sup 6916 df-inf 6917 df-pnf 7893 df-mnf 7894 df-xr 7895 df-ltxr 7896 df-le 7897 df-sub 8027 df-neg 8028 df-reap 8429 df-ap 8436 df-div 8525 df-inn 8813 df-2 8871 df-3 8872 df-4 8873 df-n0 9070 df-z 9147 df-uz 9419 df-q 9507 df-rp 9539 df-xneg 9657 df-xadd 9658 df-ioo 9774 df-ico 9776 df-icc 9777 df-fz 9891 df-fzo 10020 df-seqfrec 10323 df-exp 10397 df-fac 10577 df-bc 10599 df-ihash 10627 df-shft 10692 df-cj 10719 df-re 10720 df-im 10721 df-rsqrt 10875 df-abs 10876 df-clim 11153 df-sumdc 11228 df-ef 11522 df-e 11523 df-rest 12292 df-topgen 12311 df-psmet 12326 df-xmet 12327 df-met 12328 df-bl 12329 df-mopn 12330 df-top 12335 df-topon 12348 df-bases 12380 df-ntr 12435 df-cn 12527 df-cnp 12528 df-tx 12592 df-cncf 12897 df-limced 12964 df-dvap 12965 df-relog 13118

This theorem is referenced by: (None)

W3C validator