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 ) x. ( 5 x. 7 ) ) x. A ) <_ B
log2ublem1.2 
|- A e. RR
log2ublem1.3 
|- D e. NN0
log2ublem1.4 
|- E e. NN
log2ublem1.5 
|- B e. NN0
log2ublem1.6 
|- F e. NN0
log2ublem1.7 
|- C = ( A + ( D / E ) )
log2ublem1.8 
|- ( B + F ) = G
log2ublem1.9 
|- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) <_ ( E x. F )
Assertion log2ublem1 
|- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. C ) <_ G

Proof

Step Hyp Ref Expression
1 log2ublem1.1 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) <_ B
2 log2ublem1.2 
 |-  A e. RR
3 log2ublem1.3 
 |-  D e. NN0
4 log2ublem1.4 
 |-  E e. NN
5 log2ublem1.5 
 |-  B e. NN0
6 log2ublem1.6 
 |-  F e. NN0
7 log2ublem1.7 
 |-  C = ( A + ( D / E ) )
8 log2ublem1.8 
 |-  ( B + F ) = G
9 log2ublem1.9 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) <_ ( E x. F )
10 3nn 
 |-  3 e. NN
11 7nn0 
 |-  7 e. NN0
12 nnexpcl 
 |-  ( ( 3 e. NN /\ 7 e. NN0 ) -> ( 3 ^ 7 ) e. NN )
13 10 11 12 mp2an 
 |-  ( 3 ^ 7 ) e. NN
14 5nn 
 |-  5 e. NN
15 7nn 
 |-  7 e. NN
16 14 15 nnmulcli 
 |-  ( 5 x. 7 ) e. NN
17 13 16 nnmulcli 
 |-  ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. NN
18 17 nncni 
 |-  ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. CC
19 3 nn0cni 
 |-  D e. CC
20 4 nncni 
 |-  E e. CC
21 4 nnne0i 
 |-  E =/= 0
22 18 19 20 21 divassi 
 |-  ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) / E ) = ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) )
23 3nn0 
 |-  3 e. NN0
24 23 11 nn0expcli 
 |-  ( 3 ^ 7 ) e. NN0
25 5nn0 
 |-  5 e. NN0
26 25 11 nn0mulcli 
 |-  ( 5 x. 7 ) e. NN0
27 24 26 nn0mulcli 
 |-  ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. NN0
28 27 3 nn0mulcli 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) e. NN0
29 28 nn0rei 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) e. RR
30 6 nn0rei 
 |-  F e. RR
31 4 nnrei 
 |-  E e. RR
32 4 nngt0i 
 |-  0 < E
33 31 32 pm3.2i 
 |-  ( E e. RR /\ 0 < E )
34 ledivmul 
 |-  ( ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) e. RR /\ F e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) / E ) <_ F <-> ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) <_ ( E x. F ) ) )
35 29 30 33 34 mp3an 
 |-  ( ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) / E ) <_ F <-> ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) <_ ( E x. F ) )
36 9 35 mpbir 
 |-  ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) / E ) <_ F
37 22 36 eqbrtrri 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) <_ F
38 17 nnrei 
 |-  ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. RR
39 38 2 remulcli 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) e. RR
40 3 nn0rei 
 |-  D e. RR
41 nndivre 
 |-  ( ( D e. RR /\ E e. NN ) -> ( D / E ) e. RR )
42 40 4 41 mp2an 
 |-  ( D / E ) e. RR
43 38 42 remulcli 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) e. RR
44 5 nn0rei 
 |-  B e. RR
45 39 43 44 30 le2addi 
 |-  ( ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) <_ B /\ ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) <_ F ) -> ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) + ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) ) <_ ( B + F ) )
46 1 37 45 mp2an 
 |-  ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) + ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) ) <_ ( B + F )
47 7 oveq2i 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. C ) = ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( A + ( D / E ) ) )
48 2 recni 
 |-  A e. CC
49 42 recni 
 |-  ( D / E ) e. CC
50 18 48 49 adddii 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( A + ( D / E ) ) ) = ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) + ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) )
51 47 50 eqtr2i 
 |-  ( ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) + ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. ( D / E ) ) ) = ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. C )
52 46 51 8 3brtr3i 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. C ) <_ G