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 ⁢ A ≤ B
log2ublem1.2 ⊢ A ∈ ℝ
log2ublem1.3 ⊢ D ∈ ℕ 0
log2ublem1.4 ⊢ E ∈ ℕ
log2ublem1.5 ⊢ B ∈ ℕ 0
log2ublem1.6 ⊢ F ∈ ℕ 0
log2ublem1.7 ⊢ C = A + D E
log2ublem1.8 ⊢ B + F = G
log2ublem1.9 ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ D ≤ E ⁢ F
Assertion log2ublem1 ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ C ≤ G

Proof

Step Hyp Ref Expression
1 log2ublem1.1 ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ A ≤ B
2 log2ublem1.2 ⊢ A ∈ ℝ
3 log2ublem1.3 ⊢ D ∈ ℕ 0
4 log2ublem1.4 ⊢ E ∈ ℕ
5 log2ublem1.5 ⊢ B ∈ ℕ 0
6 log2ublem1.6 ⊢ F ∈ ℕ 0
7 log2ublem1.7 ⊢ C = A + D E
8 log2ublem1.8 ⊢ B + F = G
9 log2ublem1.9 ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ D ≤ E ⁢ F
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 ⊢ D ∈ ℂ
20 4 nncni ⊢ E ∈ ℂ
21 4 nnne0i ⊢ E ≠ 0
22 18 19 20 21 divassi ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ D E = 3 7 ⁢ 5 ⋅ 7 ⁢ D E
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 ⁢ D ∈ ℕ 0
29 28 nn0rei ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ D ∈ ℝ
30 6 nn0rei ⊢ F ∈ ℝ
31 4 nnrei ⊢ E ∈ ℝ
32 4 nngt0i ⊢ 0 < E
33 31 32 pm3.2i ⊢ E ∈ ℝ ∧ 0 < E
34 ledivmul ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ D ∈ ℝ ∧ F ∈ ℝ ∧ E ∈ ℝ ∧ 0 < E → 3 7 ⁢ 5 ⋅ 7 ⁢ D E ≤ F ↔ 3 7 ⁢ 5 ⋅ 7 ⁢ D ≤ E ⁢ F
35 29 30 33 34 mp3an ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ D E ≤ F ↔ 3 7 ⁢ 5 ⋅ 7 ⁢ D ≤ E ⁢ F
36 9 35 mpbir ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ D E ≤ F
37 22 36 eqbrtrri ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ D E ≤ F
38 17 nnrei ⊢ 3 7 ⁢ 5 ⋅ 7 ∈ ℝ
39 38 2 remulcli ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ A ∈ ℝ
40 3 nn0rei ⊢ D ∈ ℝ
41 nndivre ⊢ D ∈ ℝ ∧ E ∈ ℕ → D E ∈ ℝ
42 40 4 41 mp2an ⊢ D E ∈ ℝ
43 38 42 remulcli ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ D E ∈ ℝ
44 5 nn0rei ⊢ B ∈ ℝ
45 39 43 44 30 le2addi ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ A ≤ B ∧ 3 7 ⁢ 5 ⋅ 7 ⁢ D E ≤ F → 3 7 ⁢ 5 ⋅ 7 ⁢ A + 3 7 ⁢ 5 ⋅ 7 ⁢ D E ≤ B + F
46 1 37 45 mp2an ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ A + 3 7 ⁢ 5 ⋅ 7 ⁢ D E ≤ B + F
47 7 oveq2i ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ C = 3 7 ⁢ 5 ⋅ 7 ⁢ A + D E
48 2 recni ⊢ A ∈ ℂ
49 42 recni ⊢ D E ∈ ℂ
50 18 48 49 adddii ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ A + D E = 3 7 ⁢ 5 ⋅ 7 ⁢ A + 3 7 ⁢ 5 ⋅ 7 ⁢ D E
51 47 50 eqtr2i ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ A + 3 7 ⁢ 5 ⋅ 7 ⁢ D E = 3 7 ⁢ 5 ⋅ 7 ⁢ C
52 46 51 8 3brtr3i ⊢ 3 7 ⁢ 5 ⋅ 7 ⁢ C ≤ G