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 · 7 ) ) · 𝐴 ) ≤ 𝐵
	log2ublem1.2	⊢ 𝐴 ∈ ℝ
	log2ublem1.3	⊢ 𝐷 ∈ ℕ0
	log2ublem1.4	⊢ 𝐸 ∈ ℕ
	log2ublem1.5	⊢ 𝐵 ∈ ℕ0
	log2ublem1.6	⊢ 𝐹 ∈ ℕ0
	log2ublem1.7	⊢ 𝐶 = ( 𝐴 + ( 𝐷 / 𝐸 ) )
	log2ublem1.8	⊢ ( 𝐵 + 𝐹 ) = 𝐺
	log2ublem1.9	⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐷 ) ≤ ( 𝐸 · 𝐹 )
Assertion	log2ublem1	⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐶 ) ≤ 𝐺

Proof

Step	Hyp	Ref	Expression
1		log2ublem1.1	⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐴 ) ≤ 𝐵
2		log2ublem1.2	⊢ 𝐴 ∈ ℝ
3		log2ublem1.3	⊢ 𝐷 ∈ ℕ0
4		log2ublem1.4	⊢ 𝐸 ∈ ℕ
5		log2ublem1.5	⊢ 𝐵 ∈ ℕ0
6		log2ublem1.6	⊢ 𝐹 ∈ ℕ0
7		log2ublem1.7	⊢ 𝐶 = ( 𝐴 + ( 𝐷 / 𝐸 ) )
8		log2ublem1.8	⊢ ( 𝐵 + 𝐹 ) = 𝐺
9		log2ublem1.9	⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐷 ) ≤ ( 𝐸 · 𝐹 )
10		3nn	⊢ 3 ∈ ℕ
11		7nn0	⊢ 7 ∈ ℕ0
12		nnexpcl	⊢ ( ( 3 ∈ ℕ ∧ 7 ∈ ℕ0 ) → ( 3 ↑ 7 ) ∈ ℕ )
13	10 11 12	mp2an	⊢ ( 3 ↑ 7 ) ∈ ℕ
14		5nn	⊢ 5 ∈ ℕ
15		7nn	⊢ 7 ∈ ℕ
16	14 15	nnmulcli	⊢ ( 5 · 7 ) ∈ ℕ
17	13 16	nnmulcli	⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℕ
18	17	nncni	⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℂ
19	3	nn0cni	⊢ 𝐷 ∈ ℂ
20	4	nncni	⊢ 𝐸 ∈ ℂ
21	4	nnne0i	⊢ 𝐸 ≠ 0
22	18 19 20 21	divassi	⊢ ( ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐷 ) / 𝐸 ) = ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( 𝐷 / 𝐸 ) )
23		3nn0	⊢ 3 ∈ ℕ0
24	23 11	nn0expcli	⊢ ( 3 ↑ 7 ) ∈ ℕ0
25		5nn0	⊢ 5 ∈ ℕ0
26	25 11	nn0mulcli	⊢ ( 5 · 7 ) ∈ ℕ0
27	24 26	nn0mulcli	⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℕ0
28	27 3	nn0mulcli	⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐷 ) ∈ ℕ0
29	28	nn0rei	⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐷 ) ∈ ℝ
30	6	nn0rei	⊢ 𝐹 ∈ ℝ
31	4	nnrei	⊢ 𝐸 ∈ ℝ
32	4	nngt0i	⊢ 0 < 𝐸
33	31 32	pm3.2i	⊢ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 )
34		ledivmul	⊢ ( ( ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐷 ) ∈ ℝ ∧ 𝐹 ∈ ℝ ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( ( ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐷 ) / 𝐸 ) ≤ 𝐹 ↔ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐷 ) ≤ ( 𝐸 · 𝐹 ) ) )
35	29 30 33 34	mp3an	⊢ ( ( ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐷 ) / 𝐸 ) ≤ 𝐹 ↔ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐷 ) ≤ ( 𝐸 · 𝐹 ) )
36	9 35	mpbir	⊢ ( ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐷 ) / 𝐸 ) ≤ 𝐹
37	22 36	eqbrtrri	⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( 𝐷 / 𝐸 ) ) ≤ 𝐹
38	17	nnrei	⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℝ
39	38 2	remulcli	⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐴 ) ∈ ℝ
40	3	nn0rei	⊢ 𝐷 ∈ ℝ
41		nndivre	⊢ ( ( 𝐷 ∈ ℝ ∧ 𝐸 ∈ ℕ ) → ( 𝐷 / 𝐸 ) ∈ ℝ )
42	40 4 41	mp2an	⊢ ( 𝐷 / 𝐸 ) ∈ ℝ
43	38 42	remulcli	⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( 𝐷 / 𝐸 ) ) ∈ ℝ
44	5	nn0rei	⊢ 𝐵 ∈ ℝ
45	39 43 44 30	le2addi	⊢ ( ( ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐴 ) ≤ 𝐵 ∧ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( 𝐷 / 𝐸 ) ) ≤ 𝐹 ) → ( ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐴 ) + ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( 𝐷 / 𝐸 ) ) ) ≤ ( 𝐵 + 𝐹 ) )
46	1 37 45	mp2an	⊢ ( ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐴 ) + ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( 𝐷 / 𝐸 ) ) ) ≤ ( 𝐵 + 𝐹 )
47	7	oveq2i	⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐶 ) = ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( 𝐴 + ( 𝐷 / 𝐸 ) ) )
48	2	recni	⊢ 𝐴 ∈ ℂ
49	42	recni	⊢ ( 𝐷 / 𝐸 ) ∈ ℂ
50	18 48 49	adddii	⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( 𝐴 + ( 𝐷 / 𝐸 ) ) ) = ( ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐴 ) + ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( 𝐷 / 𝐸 ) ) )
51	47 50	eqtr2i	⊢ ( ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐴 ) + ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( 𝐷 / 𝐸 ) ) ) = ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐶 )
52	46 51 8	3brtr3i	⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 𝐶 ) ≤ 𝐺