logdivlti - Intuitionistic Logic Explorer

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

Theorem logdivlti 15403

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 1004	. . . . . . . 8 $/\$ $/\$ $/\$
2		simpl3 1005	. . . . . . . . . 10 $/\$ $/\$ $/\$
3		simpr 110	. . . . . . . . . 10 $/\$ $/\$ $/\$
4		ere 12031	. . . . . . . . . . 11
5		simpl1 1003	. . . . . . . . . . 11 $/\$ $/\$ $/\$
6		lelttr 8174	. . . . . . . . . . 11 $/\$ $/\$ $/\$
7	4, 5, 1, 6	mp3an2i 1355	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
8	2, 3, 7	mp2and 433	. . . . . . . . 9 $/\$ $/\$ $/\$
9		epos 12142	. . . . . . . . . 10
10		0re 8085	. . . . . . . . . . 11
11		lttr 8159	. . . . . . . . . . 11 $/\$ $/\$ $/\$
12	10, 4, 1, 11	mp3an12i 1354	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
13	9, 12	mpani 430	. . . . . . . . 9 $/\$ $/\$ $/\$
14	8, 13	mpd 13	. . . . . . . 8 $/\$ $/\$ $/\$
15	1, 14	elrpd 9828	. . . . . . 7 $/\$ $/\$ $/\$
16		ltletr 8175	. . . . . . . . . . 11 $/\$ $/\$ $/\$
17	10, 4, 5, 16	mp3an12i 1354	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18	9, 17	mpani 430	. . . . . . . . 9 $/\$ $/\$ $/\$
19	2, 18	mpd 13	. . . . . . . 8 $/\$ $/\$ $/\$
20	5, 19	elrpd 9828	. . . . . . 7 $/\$ $/\$ $/\$
21	15, 20	rpdivcld 9849	. . . . . 6 $/\$ $/\$ $/\$
22		relogcl 15384	. . . . . 6
23	21, 22	syl 14	. . . . 5 $/\$ $/\$ $/\$
24	1, 20	rerpdivcld 9863	. . . . . 6 $/\$ $/\$ $/\$
25		1re 8084	. . . . . 6
26		resubcl 8349	. . . . . 6 $/\$
27	24, 25, 26	sylancl 413	. . . . 5 $/\$ $/\$ $/\$
28		relogcl 15384	. . . . . . 7
29	20, 28	syl 14	. . . . . 6 $/\$ $/\$ $/\$
30	27, 29	remulcld 8116	. . . . 5 $/\$ $/\$ $/\$
31		reeflog 15385	. . . . . . . . 9
32	21, 31	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$
33		ax-1cn 8031	. . . . . . . . 9
34	24	recnd 8114	. . . . . . . . 9 $/\$ $/\$ $/\$
35		pncan3 8293	. . . . . . . . 9 $/\$
36	33, 34, 35	sylancr 414	. . . . . . . 8 $/\$ $/\$ $/\$
37	32, 36	eqtr4d 2242	. . . . . . 7 $/\$ $/\$ $/\$
38	5	recnd 8114	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
39	38	mulid2d 8104	. . . . . . . . . . 11 $/\$ $/\$ $/\$
40	39, 3	eqbrtrd 4070	. . . . . . . . . 10 $/\$ $/\$ $/\$
41		1red 8100	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42		ltmuldiv 8960	. . . . . . . . . . 11 $/\$ $/\$ $/\$
43	41, 1, 5, 19, 42	syl112anc 1254	. . . . . . . . . 10 $/\$ $/\$ $/\$
44	40, 43	mpbid 147	. . . . . . . . 9 $/\$ $/\$ $/\$
45		difrp 9827	. . . . . . . . . 10 $/\$
46	25, 24, 45	sylancr 414	. . . . . . . . 9 $/\$ $/\$ $/\$
47	44, 46	mpbid 147	. . . . . . . 8 $/\$ $/\$ $/\$
48		efgt1p 12057	. . . . . . . 8
49	47, 48	syl 14	. . . . . . 7 $/\$ $/\$ $/\$
50	37, 49	eqbrtrd 4070	. . . . . 6 $/\$ $/\$ $/\$
51		eflt 15297	. . . . . . 7 $/\$
52	23, 27, 51	syl2anc 411	. . . . . 6 $/\$ $/\$ $/\$
53	50, 52	mpbird 167	. . . . 5 $/\$ $/\$ $/\$
54	27	recnd 8114	. . . . . . 7 $/\$ $/\$ $/\$
55	54	mulridd 8102	. . . . . 6 $/\$ $/\$ $/\$
56		df-e 12010	. . . . . . . . 9
57		reeflog 15385	. . . . . . . . . . 11
58	20, 57	syl 14	. . . . . . . . . 10 $/\$ $/\$ $/\$
59	2, 58	breqtrrd 4076	. . . . . . . . 9 $/\$ $/\$ $/\$
60	56, 59	eqbrtrrid 4084	. . . . . . . 8 $/\$ $/\$ $/\$
61		efle 15298	. . . . . . . . 9 $/\$
62	25, 29, 61	sylancr 414	. . . . . . . 8 $/\$ $/\$ $/\$
63	60, 62	mpbird 167	. . . . . . 7 $/\$ $/\$ $/\$
64		posdif 8541	. . . . . . . . . 10 $/\$
65	25, 24, 64	sylancr 414	. . . . . . . . 9 $/\$ $/\$ $/\$
66	44, 65	mpbid 147	. . . . . . . 8 $/\$ $/\$ $/\$
67		lemul2 8943	. . . . . . . 8 $/\$ $/\$ $/\$
68	41, 29, 27, 66, 67	syl112anc 1254	. . . . . . 7 $/\$ $/\$ $/\$
69	63, 68	mpbid 147	. . . . . 6 $/\$ $/\$ $/\$
70	55, 69	eqbrtrrd 4072	. . . . 5 $/\$ $/\$ $/\$
71	23, 27, 30, 53, 70	ltletrd 8509	. . . 4 $/\$ $/\$ $/\$
72		relogdiv 15392	. . . . 5 $/\$
73	15, 20, 72	syl2anc 411	. . . 4 $/\$ $/\$ $/\$
74		1cnd 8101	. . . . . 6 $/\$ $/\$ $/\$
75	29	recnd 8114	. . . . . 6 $/\$ $/\$ $/\$
76	34, 74, 75	subdird 8500	. . . . 5 $/\$ $/\$ $/\$
77	1	recnd 8114	. . . . . . 7 $/\$ $/\$ $/\$
78	20	rpap0d 9837	. . . . . . 7 $/\$ $/\$ $/\$ #
79	77, 38, 75, 78	div32apd 8900	. . . . . 6 $/\$ $/\$ $/\$
80	75	mulid2d 8104	. . . . . 6 $/\$ $/\$ $/\$
81	79, 80	oveq12d 5972	. . . . 5 $/\$ $/\$ $/\$
82	76, 81	eqtrd 2239	. . . 4 $/\$ $/\$ $/\$
83	71, 73, 82	3brtr3d 4079	. . 3 $/\$ $/\$ $/\$
84		relogcl 15384	. . . . 5
85	15, 84	syl 14	. . . 4 $/\$ $/\$ $/\$
86	29, 20	rerpdivcld 9863	. . . . 5 $/\$ $/\$ $/\$
87	1, 86	remulcld 8116	. . . 4 $/\$ $/\$ $/\$
88	85, 87, 29	ltsub1d 8640	. . 3 $/\$ $/\$ $/\$
89	83, 88	mpbird 167	. 2 $/\$ $/\$ $/\$
90	85, 86, 15	ltdivmuld 9883	. 2 $/\$ $/\$ $/\$
91	89, 90	mpbird 167	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 981

wceq 1373

wcel 2177 class class class wbr 4048

cfv 5277 (class class class)co 5954

cc 7936

cr 7937

cc0 7938

c1 7939

caddc 7941

cmul 7943

clt 8120

cle 8121

cmin 8256

cdiv 8758

crp 9788

ce 12003

ceu 12004

clog 15378

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 4164 ax-sep 4167 ax-nul 4175 ax-pow 4223 ax-pr 4258 ax-un 4485 ax-setind 4590 ax-iinf 4641 ax-cnex 8029 ax-resscn 8030 ax-1cn 8031 ax-1re 8032 ax-icn 8033 ax-addcl 8034 ax-addrcl 8035 ax-mulcl 8036 ax-mulrcl 8037 ax-addcom 8038 ax-mulcom 8039 ax-addass 8040 ax-mulass 8041 ax-distr 8042 ax-i2m1 8043 ax-0lt1 8044 ax-1rid 8045 ax-0id 8046 ax-rnegex 8047 ax-precex 8048 ax-cnre 8049 ax-pre-ltirr 8050 ax-pre-ltwlin 8051 ax-pre-lttrn 8052 ax-pre-apti 8053 ax-pre-ltadd 8054 ax-pre-mulgt0 8055 ax-pre-mulext 8056 ax-arch 8057 ax-caucvg 8058 ax-pre-suploc 8059 ax-addf 8060 ax-mulf 8061

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 3001 df-csb 3096 df-dif 3170 df-un 3172 df-in 3174 df-ss 3181 df-nul 3463 df-if 3574 df-pw 3620 df-sn 3641 df-pr 3642 df-op 3644 df-uni 3854 df-int 3889 df-iun 3932 df-disj 4025 df-br 4049 df-opab 4111 df-mpt 4112 df-tr 4148 df-id 4345 df-po 4348 df-iso 4349 df-iord 4418 df-on 4420 df-ilim 4421 df-suc 4423 df-iom 4644 df-xp 4686 df-rel 4687 df-cnv 4688 df-co 4689 df-dm 4690 df-rn 4691 df-res 4692 df-ima 4693 df-iota 5238 df-fun 5279 df-fn 5280 df-f 5281 df-f1 5282 df-fo 5283 df-f1o 5284 df-fv 5285 df-isom 5286 df-riota 5909 df-ov 5957 df-oprab 5958 df-mpo 5959 df-of 6168 df-1st 6236 df-2nd 6237 df-recs 6401 df-irdg 6466 df-frec 6487 df-1o 6512 df-oadd 6516 df-er 6630 df-map 6747 df-pm 6748 df-en 6838 df-dom 6839 df-fin 6840 df-sup 7098 df-inf 7099 df-pnf 8122 df-mnf 8123 df-xr 8124 df-ltxr 8125 df-le 8126 df-sub 8258 df-neg 8259 df-reap 8661 df-ap 8668 df-div 8759 df-inn 9050 df-2 9108 df-3 9109 df-4 9110 df-n0 9309 df-z 9386 df-uz 9662 df-q 9754 df-rp 9789 df-xneg 9907 df-xadd 9908 df-ioo 10027 df-ico 10029 df-icc 10030 df-fz 10144 df-fzo 10278 df-seqfrec 10606 df-exp 10697 df-fac 10884 df-bc 10906 df-ihash 10934 df-shft 11176 df-cj 11203 df-re 11204 df-im 11205 df-rsqrt 11359 df-abs 11360 df-clim 11640 df-sumdc 11715 df-ef 12009 df-e 12010 df-rest 13123 df-topgen 13142 df-psmet 14355 df-xmet 14356 df-met 14357 df-bl 14358 df-mopn 14359 df-top 14520 df-topon 14533 df-bases 14565 df-ntr 14618 df-cn 14710 df-cnp 14711 df-tx 14775 df-cncf 15093 df-limced 15178 df-dvap 15179 df-relog 15380

This theorem is referenced by: (None)

W3C validator