This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) · 𝐶 ) ≤ 𝐺