Theorem log2ublem1 20739

Description: Lemma for log2ub 20742. The proof of log2ub 20742, which is simply the evaluation of log2tlbnd 20738 for N = 4, takes the form of the addition of five fractions and showing this is less than another fraction. We could just perform exact arithmetic on these fractions, get a large rational number, and just multiply everything to verify the claim, but as anyone who uses decimal numbers for this task knows, it is often better to pick a common denominator d (usually a large power of 10) and work with the closest approximations of the form n / d for some integer n instead. It turns out that for our purposes it is sufficient to take d = ( 3 ^ 7 ) x. 5 x. 7, which is also nice because it shares many factors in common with the fractions in question. (Contributed by Mario Carneiro, 17-Apr-2015.)

Hypotheses

Ref	Expression
log2ublem1.1	|- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) <_ B
log2ublem1.2	|- A e. RR
log2ublem1.3	|- D e. NN0
log2ublem1.4	|- E e. NN
log2ublem1.5	|- B e. NN0
log2ublem1.6	|- F e. NN0
log2ublem1.7	|- C = ( A + ( D / E ) )
log2ublem1.8	|- ( B + F ) = G
log2ublem1.9	|- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) <_ ( E x. F )

Assertion

Ref	Expression
log2ublem1	|- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. C ) <_ G

Proof of Theorem log2ublem1

Step	Hyp	Ref	Expression
1		log2ublem1.1	. . 3 |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) <_ B
2		3nn 10090	. . . . . . . 8 |- 3 e. NN
3		7nn0 10199	. . . . . . . 8 |- 7 e. NN0
4		nnexpcl 11349	. . . . . . . 8 |- ( ( 3 e. NN /\ 7 e. NN0 ) -> ( 3 ^ 7 ) e. NN )
5	2, 3, 4	mp2an 654	. . . . . . 7 |- ( 3 ^ 7 ) e. NN
6		5nn 10092	. . . . . . . 8 |- 5 e. NN
7		7nn 10094	. . . . . . . 8 |- 7 e. NN
8	6, 7	nnmulcli 9980	. . . . . . 7 |- ( 5 x. 7 ) e. NN
9	5, 8	nnmulcli 9980	. . . . . 6 |- ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. NN
10	9	nncni 9966	. . . . 5 |- ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. CC
11		log2ublem1.3	. . . . . 6 |- D e. NN0
12	11	nn0cni 10189	. . . . 5 |- D e. CC
13		log2ublem1.4	. . . . . 6 |- E e. NN
14	13	nncni 9966	. . . . 5 |- E e. CC
15	13	nnne0i 9990	. . . . 5 |- E =/= 0
16	10, 12, 14, 15	divassi 9726	. . . 4 |- ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) / E ) = ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) )
17		log2ublem1.9	. . . . 5 |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) <_ ( E x. F )
18		3nn0 10195	. . . . . . . . . 10 |- 3 e. NN0
19	18, 3	nn0expcli 11362	. . . . . . . . 9 |- ( 3 ^ 7 ) e. NN0
20		5nn0 10197	. . . . . . . . . 10 |- 5 e. NN0
21	20, 3	nn0mulcli 10214	. . . . . . . . 9 |- ( 5 x. 7 ) e. NN0
22	19, 21	nn0mulcli 10214	. . . . . . . 8 |- ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. NN0
23	22, 11	nn0mulcli 10214	. . . . . . 7 |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) e. NN0
24	23	nn0rei 10188	. . . . . 6 |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) e. RR
25		log2ublem1.6	. . . . . . 7 |- F e. NN0
26	25	nn0rei 10188	. . . . . 6 |- F e. RR
27	13	nnrei 9965	. . . . . . 7 |- E e. RR
28	13	nngt0i 9989	. . . . . . 7 |- 0 < E
29	27, 28	pm3.2i 442	. . . . . 6 |- ( E e. RR /\ 0 < E )
30		ledivmul 9839	. . . . . 6 |- ( ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) e. RR /\ F e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) / E ) <_ F <-> ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) <_ ( E x. F ) ) )
31	24, 26, 29, 30	mp3an 1279	. . . . 5 |- ( ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) / E ) <_ F <-> ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) <_ ( E x. F ) )
32	17, 31	mpbir 201	. . . 4 |- ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) / E ) <_ F
33	16, 32	eqbrtrri 4193	. . 3 |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) <_ F
34	9	nnrei 9965	. . . . 5 |- ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. RR
35		log2ublem1.2	. . . . 5 |- A e. RR
36	34, 35	remulcli 9060	. . . 4 |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) e. RR
37	11	nn0rei 10188	. . . . . 6 |- D e. RR
38		nndivre 9991	. . . . . 6 |- ( ( D e. RR /\ E e. NN ) -> ( D / E ) e. RR )
39	37, 13, 38	mp2an 654	. . . . 5 |- ( D / E ) e. RR
40	34, 39	remulcli 9060	. . . 4 |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) e. RR
41		log2ublem1.5	. . . . 5 |- B e. NN0
42	41	nn0rei 10188	. . . 4 |- B e. RR
43	36, 40, 42, 26	le2addi 9546	. . 3 |- ( ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) <_ B /\ ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) <_ F ) -> ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) + ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) ) <_ ( B + F ) )
44	1, 33, 43	mp2an 654	. 2 |- ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) + ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) ) <_ ( B + F )
45		log2ublem1.7	. . . 4 |- C = ( A + ( D / E ) )
46	45	oveq2i 6051	. . 3 |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. C ) = ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( A + ( D / E ) ) )
47	35	recni 9058	. . . 4 |- A e. CC
48	39	recni 9058	. . . 4 |- ( D / E ) e. CC
49	10, 47, 48	adddii 9056	. . 3 |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( A + ( D / E ) ) ) = ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) + ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) )
50	46, 49	eqtr2i 2425	. 2 |- ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) + ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) ) = ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. C )
51		log2ublem1.8	. 2 |- ( B + F ) = G
52	44, 50, 51	3brtr3i 4199	1 |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. C ) <_ G

Syntax hints:   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   class class class wbr 4172  (class class class)co 6040   RRcr 8945   0cc0 8946   + caddc 8949   x. cmul 8951   < clt 9076   <_ cle 9077   / cdiv 9633   NNcn 9956   3c3 10006   5c5 10008   7c7 10010   NN0cn0 10177   ^cexp 11337

This theorem is referenced by:  log2ublem2  20740  log2ub  20742

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-n0 10178  df-z 10239  df-uz 10445  df-seq 11279  df-exp 11338