logdivlti - Intuitionistic Logic Explorer

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

Theorem logdivlti 15540

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 1025	. . . . . . . 8 $/\$ $/\$ $/\$
2		simpl3 1026	. . . . . . . . . 10 $/\$ $/\$ $/\$
3		simpr 110	. . . . . . . . . 10 $/\$ $/\$ $/\$
4		ere 12167	. . . . . . . . . . 11
5		simpl1 1024	. . . . . . . . . . 11 $/\$ $/\$ $/\$
6		lelttr 8223	. . . . . . . . . . 11 $/\$ $/\$ $/\$
7	4, 5, 1, 6	mp3an2i 1376	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
8	2, 3, 7	mp2and 433	. . . . . . . . 9 $/\$ $/\$ $/\$
9		epos 12278	. . . . . . . . . 10
10		0re 8134	. . . . . . . . . . 11
11		lttr 8208	. . . . . . . . . . 11 $/\$ $/\$ $/\$
12	10, 4, 1, 11	mp3an12i 1375	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
13	9, 12	mpani 430	. . . . . . . . 9 $/\$ $/\$ $/\$
14	8, 13	mpd 13	. . . . . . . 8 $/\$ $/\$ $/\$
15	1, 14	elrpd 9877	. . . . . . 7 $/\$ $/\$ $/\$
16		ltletr 8224	. . . . . . . . . . 11 $/\$ $/\$ $/\$
17	10, 4, 5, 16	mp3an12i 1375	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18	9, 17	mpani 430	. . . . . . . . 9 $/\$ $/\$ $/\$
19	2, 18	mpd 13	. . . . . . . 8 $/\$ $/\$ $/\$
20	5, 19	elrpd 9877	. . . . . . 7 $/\$ $/\$ $/\$
21	15, 20	rpdivcld 9898	. . . . . 6 $/\$ $/\$ $/\$
22		relogcl 15521	. . . . . 6
23	21, 22	syl 14	. . . . 5 $/\$ $/\$ $/\$
24	1, 20	rerpdivcld 9912	. . . . . 6 $/\$ $/\$ $/\$
25		1re 8133	. . . . . 6
26		resubcl 8398	. . . . . 6 $/\$
27	24, 25, 26	sylancl 413	. . . . 5 $/\$ $/\$ $/\$
28		relogcl 15521	. . . . . . 7
29	20, 28	syl 14	. . . . . 6 $/\$ $/\$ $/\$
30	27, 29	remulcld 8165	. . . . 5 $/\$ $/\$ $/\$
31		reeflog 15522	. . . . . . . . 9
32	21, 31	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$
33		ax-1cn 8080	. . . . . . . . 9
34	24	recnd 8163	. . . . . . . . 9 $/\$ $/\$ $/\$
35		pncan3 8342	. . . . . . . . 9 $/\$
36	33, 34, 35	sylancr 414	. . . . . . . 8 $/\$ $/\$ $/\$
37	32, 36	eqtr4d 2265	. . . . . . 7 $/\$ $/\$ $/\$
38	5	recnd 8163	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
39	38	mulid2d 8153	. . . . . . . . . . 11 $/\$ $/\$ $/\$
40	39, 3	eqbrtrd 4104	. . . . . . . . . 10 $/\$ $/\$ $/\$
41		1red 8149	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42		ltmuldiv 9009	. . . . . . . . . . 11 $/\$ $/\$ $/\$
43	41, 1, 5, 19, 42	syl112anc 1275	. . . . . . . . . 10 $/\$ $/\$ $/\$
44	40, 43	mpbid 147	. . . . . . . . 9 $/\$ $/\$ $/\$
45		difrp 9876	. . . . . . . . . 10 $/\$
46	25, 24, 45	sylancr 414	. . . . . . . . 9 $/\$ $/\$ $/\$
47	44, 46	mpbid 147	. . . . . . . 8 $/\$ $/\$ $/\$
48		efgt1p 12193	. . . . . . . 8
49	47, 48	syl 14	. . . . . . 7 $/\$ $/\$ $/\$
50	37, 49	eqbrtrd 4104	. . . . . 6 $/\$ $/\$ $/\$
51		eflt 15434	. . . . . . 7 $/\$
52	23, 27, 51	syl2anc 411	. . . . . 6 $/\$ $/\$ $/\$
53	50, 52	mpbird 167	. . . . 5 $/\$ $/\$ $/\$
54	27	recnd 8163	. . . . . . 7 $/\$ $/\$ $/\$
55	54	mulridd 8151	. . . . . 6 $/\$ $/\$ $/\$
56		df-e 12146	. . . . . . . . 9
57		reeflog 15522	. . . . . . . . . . 11
58	20, 57	syl 14	. . . . . . . . . 10 $/\$ $/\$ $/\$
59	2, 58	breqtrrd 4110	. . . . . . . . 9 $/\$ $/\$ $/\$
60	56, 59	eqbrtrrid 4118	. . . . . . . 8 $/\$ $/\$ $/\$
61		efle 15435	. . . . . . . . 9 $/\$
62	25, 29, 61	sylancr 414	. . . . . . . 8 $/\$ $/\$ $/\$
63	60, 62	mpbird 167	. . . . . . 7 $/\$ $/\$ $/\$
64		posdif 8590	. . . . . . . . . 10 $/\$
65	25, 24, 64	sylancr 414	. . . . . . . . 9 $/\$ $/\$ $/\$
66	44, 65	mpbid 147	. . . . . . . 8 $/\$ $/\$ $/\$
67		lemul2 8992	. . . . . . . 8 $/\$ $/\$ $/\$
68	41, 29, 27, 66, 67	syl112anc 1275	. . . . . . 7 $/\$ $/\$ $/\$
69	63, 68	mpbid 147	. . . . . 6 $/\$ $/\$ $/\$
70	55, 69	eqbrtrrd 4106	. . . . 5 $/\$ $/\$ $/\$
71	23, 27, 30, 53, 70	ltletrd 8558	. . . 4 $/\$ $/\$ $/\$
72		relogdiv 15529	. . . . 5 $/\$
73	15, 20, 72	syl2anc 411	. . . 4 $/\$ $/\$ $/\$
74		1cnd 8150	. . . . . 6 $/\$ $/\$ $/\$
75	29	recnd 8163	. . . . . 6 $/\$ $/\$ $/\$
76	34, 74, 75	subdird 8549	. . . . 5 $/\$ $/\$ $/\$
77	1	recnd 8163	. . . . . . 7 $/\$ $/\$ $/\$
78	20	rpap0d 9886	. . . . . . 7 $/\$ $/\$ $/\$ #
79	77, 38, 75, 78	div32apd 8949	. . . . . 6 $/\$ $/\$ $/\$
80	75	mulid2d 8153	. . . . . 6 $/\$ $/\$ $/\$
81	79, 80	oveq12d 6012	. . . . 5 $/\$ $/\$ $/\$
82	76, 81	eqtrd 2262	. . . 4 $/\$ $/\$ $/\$
83	71, 73, 82	3brtr3d 4113	. . 3 $/\$ $/\$ $/\$
84		relogcl 15521	. . . . 5
85	15, 84	syl 14	. . . 4 $/\$ $/\$ $/\$
86	29, 20	rerpdivcld 9912	. . . . 5 $/\$ $/\$ $/\$
87	1, 86	remulcld 8165	. . . 4 $/\$ $/\$ $/\$
88	85, 87, 29	ltsub1d 8689	. . 3 $/\$ $/\$ $/\$
89	83, 88	mpbird 167	. 2 $/\$ $/\$ $/\$
90	85, 86, 15	ltdivmuld 9932	. 2 $/\$ $/\$ $/\$
91	89, 90	mpbird 167	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 1002

wceq 1395

wcel 2200 class class class wbr 4082

cfv 5314 (class class class)co 5994

cc 7985

cr 7986

cc0 7987

c1 7988

caddc 7990

cmul 7992

clt 8169

cle 8170

cmin 8305

cdiv 8807

crp 9837

ce 12139

ceu 12140

clog 15515

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4521 ax-setind 4626 ax-iinf 4677 ax-cnex 8078 ax-resscn 8079 ax-1cn 8080 ax-1re 8081 ax-icn 8082 ax-addcl 8083 ax-addrcl 8084 ax-mulcl 8085 ax-mulrcl 8086 ax-addcom 8087 ax-mulcom 8088 ax-addass 8089 ax-mulass 8090 ax-distr 8091 ax-i2m1 8092 ax-0lt1 8093 ax-1rid 8094 ax-0id 8095 ax-rnegex 8096 ax-precex 8097 ax-cnre 8098 ax-pre-ltirr 8099 ax-pre-ltwlin 8100 ax-pre-lttrn 8101 ax-pre-apti 8102 ax-pre-ltadd 8103 ax-pre-mulgt0 8104 ax-pre-mulext 8105 ax-arch 8106 ax-caucvg 8107 ax-pre-suploc 8108 ax-addf 8109 ax-mulf 8110

This theorem depends on definitions: df-bi 117 df-stab 836 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-disj 4059 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4381 df-po 4384 df-iso 4385 df-iord 4454 df-on 4456 df-ilim 4457 df-suc 4459 df-iom 4680 df-xp 4722 df-rel 4723 df-cnv 4724 df-co 4725 df-dm 4726 df-rn 4727 df-res 4728 df-ima 4729 df-iota 5274 df-fun 5316 df-fn 5317 df-f 5318 df-f1 5319 df-fo 5320 df-f1o 5321 df-fv 5322 df-isom 5323 df-riota 5947 df-ov 5997 df-oprab 5998 df-mpo 5999 df-of 6208 df-1st 6276 df-2nd 6277 df-recs 6441 df-irdg 6506 df-frec 6527 df-1o 6552 df-oadd 6556 df-er 6670 df-map 6787 df-pm 6788 df-en 6878 df-dom 6879 df-fin 6880 df-sup 7139 df-inf 7140 df-pnf 8171 df-mnf 8172 df-xr 8173 df-ltxr 8174 df-le 8175 df-sub 8307 df-neg 8308 df-reap 8710 df-ap 8717 df-div 8808 df-inn 9099 df-2 9157 df-3 9158 df-4 9159 df-n0 9358 df-z 9435 df-uz 9711 df-q 9803 df-rp 9838 df-xneg 9956 df-xadd 9957 df-ioo 10076 df-ico 10078 df-icc 10079 df-fz 10193 df-fzo 10327 df-seqfrec 10657 df-exp 10748 df-fac 10935 df-bc 10957 df-ihash 10985 df-shft 11312 df-cj 11339 df-re 11340 df-im 11341 df-rsqrt 11495 df-abs 11496 df-clim 11776 df-sumdc 11851 df-ef 12145 df-e 12146 df-rest 13260 df-topgen 13279 df-psmet 14492 df-xmet 14493 df-met 14494 df-bl 14495 df-mopn 14496 df-top 14657 df-topon 14670 df-bases 14702 df-ntr 14755 df-cn 14847 df-cnp 14848 df-tx 14912 df-cncf 15230 df-limced 15315 df-dvap 15316 df-relog 15517

This theorem is referenced by: (None)

W3C validator