Theorem log2ublem1

Description: Lemma for log2ub . The proof of log2ub , which is simply the evaluation of log2tlbnd 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 1 0 ) 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)

	Ref	Expression
Hypotheses	log2ublem1.1	$$⊢3^{7}5\cdot 7A\le B$$
	log2ublem1.2	$$⊢A\in ℝ$$
	log2ublem1.3	$$⊢D\in {\mathbb{N}}_0$$
	log2ublem1.4	$$⊢E\in \mathbb{N}$$
	log2ublem1.5	$$⊢B\in {\mathbb{N}}_0$$
	log2ublem1.6	$$⊢F\in {\mathbb{N}}_0$$
	log2ublem1.7	$$⊢C=A+\left(\frac{D}{E}\right)$$
	log2ublem1.8	$$⊢B+F=G$$
	log2ublem1.9	$$⊢3^{7}5\cdot 7D\le EF$$
Assertion	log2ublem1	$$⊢3^{7}5\cdot 7C\le G$$

Proof

Step	Hyp	Ref	Expression
1		log2ublem1.1	$$⊢3^{7}5\cdot 7A\le B$$
2		log2ublem1.2	$$⊢A\in ℝ$$
3		log2ublem1.3	$$⊢D\in {\mathbb{N}}_0$$
4		log2ublem1.4	$$⊢E\in \mathbb{N}$$
5		log2ublem1.5	$$⊢B\in {\mathbb{N}}_0$$
6		log2ublem1.6	$$⊢F\in {\mathbb{N}}_0$$
7		log2ublem1.7	$$⊢C=A+\left(\frac{D}{E}\right)$$
8		log2ublem1.8	$$⊢B+F=G$$
9		log2ublem1.9	$$⊢3^{7}5\cdot 7D\le EF$$
10		3nn	$$⊢3\in \mathbb{N}$$
11		7nn0	$$⊢7\in {\mathbb{N}}_0$$
12		nnexpcl	$$⊢\left(3\in \mathbb{N}\wedge 7\in {\mathbb{N}}_0\right)\to 3^7\in \mathbb{N}$$
13	10 11 12	mp2an	$$⊢3^7\in \mathbb{N}$$
14		5nn	$$⊢5\in \mathbb{N}$$
15		7nn	$$⊢7\in \mathbb{N}$$
16	14 15	nnmulcli	$$⊢5\cdot 7\in \mathbb{N}$$
17	13 16	nnmulcli	$$⊢3^{7}5\cdot 7\in \mathbb{N}$$
18	17	nncni	$$⊢3^{7}5\cdot 7\in ℂ$$
19	3	nn0cni	$$⊢D\in ℂ$$
20	4	nncni	$$⊢E\in ℂ$$
21	4	nnne0i	$$⊢E\ne 0$$
22	18 19 20 21	divassi	$$⊢\frac{3^{7}5\cdot 7D}{E}=3^{7}5\cdot 7\left(\frac{D}{E}\right)$$
23		3nn0	$$⊢3\in {\mathbb{N}}_0$$
24	23 11	nn0expcli	$$⊢3^7\in {\mathbb{N}}_0$$
25		5nn0	$$⊢5\in {\mathbb{N}}_0$$
26	25 11	nn0mulcli	$$⊢5\cdot 7\in {\mathbb{N}}_0$$
27	24 26	nn0mulcli	$$⊢3^{7}5\cdot 7\in {\mathbb{N}}_0$$
28	27 3	nn0mulcli	$$⊢3^{7}5\cdot 7D\in {\mathbb{N}}_0$$
29	28	nn0rei	$$⊢3^{7}5\cdot 7D\in ℝ$$
30	6	nn0rei	$$⊢F\in ℝ$$
31	4	nnrei	$$⊢E\in ℝ$$
32	4	nngt0i	$$⊢0<E$$
33	31 32	pm3.2i	$$⊢\left(E\in ℝ\wedge 0<E\right)$$
34		ledivmul	$$⊢\left(3^{7}5\cdot 7D\in ℝ\wedge F\in ℝ\wedge \left(E\in ℝ\wedge 0<E\right)\right)\to \left(\frac{3^{7}5\cdot 7D}{E}\le F\leftrightarrow 3^{7}5\cdot 7D\le EF\right)$$
35	29 30 33 34	mp3an	$$⊢\frac{3^{7}5\cdot 7D}{E}\le F\leftrightarrow 3^{7}5\cdot 7D\le EF$$
36	9 35	mpbir	$$⊢\frac{3^{7}5\cdot 7D}{E}\le F$$
37	22 36	eqbrtrri	$$⊢3^{7}5\cdot 7\left(\frac{D}{E}\right)\le F$$
38	17	nnrei	$$⊢3^{7}5\cdot 7\in ℝ$$
39	38 2	remulcli	$$⊢3^{7}5\cdot 7A\in ℝ$$
40	3	nn0rei	$$⊢D\in ℝ$$
41		nndivre	$$⊢\left(D\in ℝ\wedge E\in \mathbb{N}\right)\to \frac{D}{E}\in ℝ$$
42	40 4 41	mp2an	$$⊢\frac{D}{E}\in ℝ$$
43	38 42	remulcli	$$⊢3^{7}5\cdot 7\left(\frac{D}{E}\right)\in ℝ$$
44	5	nn0rei	$$⊢B\in ℝ$$
45	39 43 44 30	le2addi	$$⊢\left(3^{7}5\cdot 7A\le B\wedge 3^{7}5\cdot 7\left(\frac{D}{E}\right)\le F\right)\to 3^{7}5\cdot 7A+3^{7}5\cdot 7\left(\frac{D}{E}\right)\le B+F$$
46	1 37 45	mp2an	$$⊢3^{7}5\cdot 7A+3^{7}5\cdot 7\left(\frac{D}{E}\right)\le B+F$$
47	7	oveq2i	$$⊢3^{7}5\cdot 7C=3^{7}5\cdot 7\left(A+\left(\frac{D}{E}\right)\right)$$
48	2	recni	$$⊢A\in ℂ$$
49	42	recni	$$⊢\frac{D}{E}\in ℂ$$
50	18 48 49	adddii	$$⊢3^{7}5\cdot 7\left(A+\left(\frac{D}{E}\right)\right)=3^{7}5\cdot 7A+3^{7}5\cdot 7\left(\frac{D}{E}\right)$$
51	47 50	eqtr2i	$$⊢3^{7}5\cdot 7A+3^{7}5\cdot 7\left(\frac{D}{E}\right)=3^{7}5\cdot 7C$$
52	46 51 8	3brtr3i	$$⊢3^{7}5\cdot 7C\le G$$