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