Metamath Proof Explorer

Theorem log2ublem2

Description: Lemma for log2ub . (Contributed by Mario Carneiro, 17-Apr-2015)

Ref Expression
Hypotheses log2ublem2.1 
|- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. sum_ n e. ( 0 ... K ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) <_ ( 2 x. B )
log2ublem2.2 
|- B e. NN0
log2ublem2.3 
|- F e. NN0
log2ublem2.4 
|- N e. NN0
log2ublem2.5 
|- ( N - 1 ) = K
log2ublem2.6 
|- ( B + F ) = G
log2ublem2.7 
|- M e. NN0
log2ublem2.8 
|- ( M + N ) = 3
log2ublem2.9 
|- ( ( 5 x. 7 ) x. ( 9 ^ M ) ) = ( ( ( 2 x. N ) + 1 ) x. F )
Assertion log2ublem2 
|- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. sum_ n e. ( 0 ... N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) <_ ( 2 x. G )

Proof

Step Hyp Ref Expression
1 log2ublem2.1 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. sum_ n e. ( 0 ... K ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) <_ ( 2 x. B )
2 log2ublem2.2 
 |-  B e. NN0
3 log2ublem2.3 
 |-  F e. NN0
4 log2ublem2.4 
 |-  N e. NN0
5 log2ublem2.5 
 |-  ( N - 1 ) = K
6 log2ublem2.6 
 |-  ( B + F ) = G
7 log2ublem2.7 
 |-  M e. NN0
8 log2ublem2.8 
 |-  ( M + N ) = 3
9 log2ublem2.9 
 |-  ( ( 5 x. 7 ) x. ( 9 ^ M ) ) = ( ( ( 2 x. N ) + 1 ) x. F )
10 fzfid 
 |-  ( T. -> ( 0 ... K ) e. Fin )
11 elfznn0 
 |-  ( n e. ( 0 ... K ) -> n e. NN0 )
12 11 adantl 
 |-  ( ( T. /\ n e. ( 0 ... K ) ) -> n e. NN0 )
13 2re 
 |-  2 e. RR
14 3nn 
 |-  3 e. NN
15 2nn0 
 |-  2 e. NN0
16 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 )
17 15 16 mpan 
 |-  ( n e. NN0 -> ( 2 x. n ) e. NN0 )
18 nn0p1nn 
 |-  ( ( 2 x. n ) e. NN0 -> ( ( 2 x. n ) + 1 ) e. NN )
19 17 18 syl 
 |-  ( n e. NN0 -> ( ( 2 x. n ) + 1 ) e. NN )
20 nnmulcl 
 |-  ( ( 3 e. NN /\ ( ( 2 x. n ) + 1 ) e. NN ) -> ( 3 x. ( ( 2 x. n ) + 1 ) ) e. NN )
21 14 19 20 sylancr 
 |-  ( n e. NN0 -> ( 3 x. ( ( 2 x. n ) + 1 ) ) e. NN )
22 9nn 
 |-  9 e. NN
23 nnexpcl 
 |-  ( ( 9 e. NN /\ n e. NN0 ) -> ( 9 ^ n ) e. NN )
24 22 23 mpan 
 |-  ( n e. NN0 -> ( 9 ^ n ) e. NN )
25 21 24 nnmulcld 
 |-  ( n e. NN0 -> ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) e. NN )
26 nndivre 
 |-  ( ( 2 e. RR /\ ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) e. NN ) -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR )
27 13 25 26 sylancr 
 |-  ( n e. NN0 -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR )
28 12 27 syl 
 |-  ( ( T. /\ n e. ( 0 ... K ) ) -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR )
29 10 28 fsumrecl 
 |-  ( T. -> sum_ n e. ( 0 ... K ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR )
30 29 mptru 
 |-  sum_ n e. ( 0 ... K ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR
31 15 4 nn0mulcli 
 |-  ( 2 x. N ) e. NN0
32 nn0p1nn 
 |-  ( ( 2 x. N ) e. NN0 -> ( ( 2 x. N ) + 1 ) e. NN )
33 31 32 ax-mp 
 |-  ( ( 2 x. N ) + 1 ) e. NN
34 14 33 nnmulcli 
 |-  ( 3 x. ( ( 2 x. N ) + 1 ) ) e. NN
35 nnexpcl 
 |-  ( ( 9 e. NN /\ N e. NN0 ) -> ( 9 ^ N ) e. NN )
36 22 4 35 mp2an 
 |-  ( 9 ^ N ) e. NN
37 34 36 nnmulcli 
 |-  ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) e. NN
38 15 2 nn0mulcli 
 |-  ( 2 x. B ) e. NN0
39 15 3 nn0mulcli 
 |-  ( 2 x. F ) e. NN0
40 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
41 4 40 eleqtri 
 |-  N e. ( ZZ>= ` 0 )
42 41 a1i 
 |-  ( T. -> N e. ( ZZ>= ` 0 ) )
43 elfznn0 
 |-  ( n e. ( 0 ... N ) -> n e. NN0 )
44 43 adantl 
 |-  ( ( T. /\ n e. ( 0 ... N ) ) -> n e. NN0 )
45 27 recnd 
 |-  ( n e. NN0 -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. CC )
46 44 45 syl 
 |-  ( ( T. /\ n e. ( 0 ... N ) ) -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. CC )
47 oveq2 
 |-  ( n = N -> ( 2 x. n ) = ( 2 x. N ) )
48 47 oveq1d 
 |-  ( n = N -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. N ) + 1 ) )
49 48 oveq2d 
 |-  ( n = N -> ( 3 x. ( ( 2 x. n ) + 1 ) ) = ( 3 x. ( ( 2 x. N ) + 1 ) ) )
50 oveq2 
 |-  ( n = N -> ( 9 ^ n ) = ( 9 ^ N ) )
51 49 50 oveq12d 
 |-  ( n = N -> ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) = ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) )
52 51 oveq2d 
 |-  ( n = N -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) = ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) )
53 42 46 52 fsumm1 
 |-  ( T. -> sum_ n e. ( 0 ... N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) = ( sum_ n e. ( 0 ... ( N - 1 ) ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) + ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) ) )
54 53 mptru 
 |-  sum_ n e. ( 0 ... N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) = ( sum_ n e. ( 0 ... ( N - 1 ) ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) + ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) )
55 5 oveq2i 
 |-  ( 0 ... ( N - 1 ) ) = ( 0 ... K )
56 55 sumeq1i 
 |-  sum_ n e. ( 0 ... ( N - 1 ) ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) = sum_ n e. ( 0 ... K ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) )
57 56 oveq1i 
 |-  ( sum_ n e. ( 0 ... ( N - 1 ) ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) + ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) ) = ( sum_ n e. ( 0 ... K ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) + ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) )
58 54 57 eqtri 
 |-  sum_ n e. ( 0 ... N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) = ( sum_ n e. ( 0 ... K ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) + ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) )
59 2cn 
 |-  2 e. CC
60 2 nn0cni 
 |-  B e. CC
61 3 nn0cni 
 |-  F e. CC
62 59 60 61 adddii 
 |-  ( 2 x. ( B + F ) ) = ( ( 2 x. B ) + ( 2 x. F ) )
63 6 oveq2i 
 |-  ( 2 x. ( B + F ) ) = ( 2 x. G )
64 62 63 eqtr3i 
 |-  ( ( 2 x. B ) + ( 2 x. F ) ) = ( 2 x. G )
65 7nn 
 |-  7 e. NN
66 65 nnnn0i 
 |-  7 e. NN0
67 nnexpcl 
 |-  ( ( 3 e. NN /\ 7 e. NN0 ) -> ( 3 ^ 7 ) e. NN )
68 14 66 67 mp2an 
 |-  ( 3 ^ 7 ) e. NN
69 5nn 
 |-  5 e. NN
70 69 65 nnmulcli 
 |-  ( 5 x. 7 ) e. NN
71 68 70 nnmulcli 
 |-  ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. NN
72 71 nnrei 
 |-  ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. RR
73 72 13 remulcli 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. 2 ) e. RR
74 73 leidi 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. 2 ) <_ ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. 2 )
75 14 nnnn0i 
 |-  3 e. NN0
76 nnexpcl 
 |-  ( ( 9 e. NN /\ 3 e. NN0 ) -> ( 9 ^ 3 ) e. NN )
77 22 75 76 mp2an 
 |-  ( 9 ^ 3 ) e. NN
78 77 nncni 
 |-  ( 9 ^ 3 ) e. CC
79 70 nncni 
 |-  ( 5 x. 7 ) e. CC
80 78 79 mulcomi 
 |-  ( ( 9 ^ 3 ) x. ( 5 x. 7 ) ) = ( ( 5 x. 7 ) x. ( 9 ^ 3 ) )
81 7 nn0cni 
 |-  M e. CC
82 4 nn0cni 
 |-  N e. CC
83 81 82 addcomi 
 |-  ( M + N ) = ( N + M )
84 8 83 eqtr3i 
 |-  3 = ( N + M )
85 84 oveq2i 
 |-  ( 9 ^ 3 ) = ( 9 ^ ( N + M ) )
86 22 nncni 
 |-  9 e. CC
87 expadd 
 |-  ( ( 9 e. CC /\ N e. NN0 /\ M e. NN0 ) -> ( 9 ^ ( N + M ) ) = ( ( 9 ^ N ) x. ( 9 ^ M ) ) )
88 86 4 7 87 mp3an 
 |-  ( 9 ^ ( N + M ) ) = ( ( 9 ^ N ) x. ( 9 ^ M ) )
89 85 88 eqtri 
 |-  ( 9 ^ 3 ) = ( ( 9 ^ N ) x. ( 9 ^ M ) )
90 89 oveq2i 
 |-  ( ( 5 x. 7 ) x. ( 9 ^ 3 ) ) = ( ( 5 x. 7 ) x. ( ( 9 ^ N ) x. ( 9 ^ M ) ) )
91 36 nncni 
 |-  ( 9 ^ N ) e. CC
92 nnexpcl 
 |-  ( ( 9 e. NN /\ M e. NN0 ) -> ( 9 ^ M ) e. NN )
93 22 7 92 mp2an 
 |-  ( 9 ^ M ) e. NN
94 93 nncni 
 |-  ( 9 ^ M ) e. CC
95 79 91 94 mul12i 
 |-  ( ( 5 x. 7 ) x. ( ( 9 ^ N ) x. ( 9 ^ M ) ) ) = ( ( 9 ^ N ) x. ( ( 5 x. 7 ) x. ( 9 ^ M ) ) )
96 80 90 95 3eqtri 
 |-  ( ( 9 ^ 3 ) x. ( 5 x. 7 ) ) = ( ( 9 ^ N ) x. ( ( 5 x. 7 ) x. ( 9 ^ M ) ) )
97 9 oveq2i 
 |-  ( ( 9 ^ N ) x. ( ( 5 x. 7 ) x. ( 9 ^ M ) ) ) = ( ( 9 ^ N ) x. ( ( ( 2 x. N ) + 1 ) x. F ) )
98 96 97 eqtri 
 |-  ( ( 9 ^ 3 ) x. ( 5 x. 7 ) ) = ( ( 9 ^ N ) x. ( ( ( 2 x. N ) + 1 ) x. F ) )
99 98 oveq2i 
 |-  ( 3 x. ( ( 9 ^ 3 ) x. ( 5 x. 7 ) ) ) = ( 3 x. ( ( 9 ^ N ) x. ( ( ( 2 x. N ) + 1 ) x. F ) ) )
100 df-7 
 |-  7 = ( 6 + 1 )
101 100 oveq2i 
 |-  ( 3 ^ 7 ) = ( 3 ^ ( 6 + 1 ) )
102 3cn 
 |-  3 e. CC
103 6nn0 
 |-  6 e. NN0
104 expp1 
 |-  ( ( 3 e. CC /\ 6 e. NN0 ) -> ( 3 ^ ( 6 + 1 ) ) = ( ( 3 ^ 6 ) x. 3 ) )
105 102 103 104 mp2an 
 |-  ( 3 ^ ( 6 + 1 ) ) = ( ( 3 ^ 6 ) x. 3 )
106 expmul 
 |-  ( ( 3 e. CC /\ 2 e. NN0 /\ 3 e. NN0 ) -> ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 ) )
107 102 15 75 106 mp3an 
 |-  ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 )
108 59 102 mulcomi 
 |-  ( 2 x. 3 ) = ( 3 x. 2 )
109 3t2e6 
 |-  ( 3 x. 2 ) = 6
110 108 109 eqtri 
 |-  ( 2 x. 3 ) = 6
111 110 oveq2i 
 |-  ( 3 ^ ( 2 x. 3 ) ) = ( 3 ^ 6 )
112 sq3 
 |-  ( 3 ^ 2 ) = 9
113 112 oveq1i 
 |-  ( ( 3 ^ 2 ) ^ 3 ) = ( 9 ^ 3 )
114 107 111 113 3eqtr3i 
 |-  ( 3 ^ 6 ) = ( 9 ^ 3 )
115 114 oveq1i 
 |-  ( ( 3 ^ 6 ) x. 3 ) = ( ( 9 ^ 3 ) x. 3 )
116 105 115 eqtri 
 |-  ( 3 ^ ( 6 + 1 ) ) = ( ( 9 ^ 3 ) x. 3 )
117 78 102 mulcomi 
 |-  ( ( 9 ^ 3 ) x. 3 ) = ( 3 x. ( 9 ^ 3 ) )
118 101 116 117 3eqtri 
 |-  ( 3 ^ 7 ) = ( 3 x. ( 9 ^ 3 ) )
119 118 oveq1i 
 |-  ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) = ( ( 3 x. ( 9 ^ 3 ) ) x. ( 5 x. 7 ) )
120 102 78 79 mulassi 
 |-  ( ( 3 x. ( 9 ^ 3 ) ) x. ( 5 x. 7 ) ) = ( 3 x. ( ( 9 ^ 3 ) x. ( 5 x. 7 ) ) )
121 119 120 eqtri 
 |-  ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) = ( 3 x. ( ( 9 ^ 3 ) x. ( 5 x. 7 ) ) )
122 33 nncni 
 |-  ( ( 2 x. N ) + 1 ) e. CC
123 102 122 91 mul32i 
 |-  ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) = ( ( 3 x. ( 9 ^ N ) ) x. ( ( 2 x. N ) + 1 ) )
124 123 oveq1i 
 |-  ( ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) x. F ) = ( ( ( 3 x. ( 9 ^ N ) ) x. ( ( 2 x. N ) + 1 ) ) x. F )
125 102 91 mulcli 
 |-  ( 3 x. ( 9 ^ N ) ) e. CC
126 125 122 61 mulassi 
 |-  ( ( ( 3 x. ( 9 ^ N ) ) x. ( ( 2 x. N ) + 1 ) ) x. F ) = ( ( 3 x. ( 9 ^ N ) ) x. ( ( ( 2 x. N ) + 1 ) x. F ) )
127 122 61 mulcli 
 |-  ( ( ( 2 x. N ) + 1 ) x. F ) e. CC
128 102 91 127 mulassi 
 |-  ( ( 3 x. ( 9 ^ N ) ) x. ( ( ( 2 x. N ) + 1 ) x. F ) ) = ( 3 x. ( ( 9 ^ N ) x. ( ( ( 2 x. N ) + 1 ) x. F ) ) )
129 124 126 128 3eqtri 
 |-  ( ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) x. F ) = ( 3 x. ( ( 9 ^ N ) x. ( ( ( 2 x. N ) + 1 ) x. F ) ) )
130 99 121 129 3eqtr4i 
 |-  ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) = ( ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) x. F )
131 130 oveq2i 
 |-  ( 2 x. ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) ) = ( 2 x. ( ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) x. F ) )
132 68 nncni 
 |-  ( 3 ^ 7 ) e. CC
133 132 79 mulcli 
 |-  ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. CC
134 133 59 mulcomi 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. 2 ) = ( 2 x. ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) )
135 37 nncni 
 |-  ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) e. CC
136 135 59 61 mul12i 
 |-  ( ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) x. ( 2 x. F ) ) = ( 2 x. ( ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) x. F ) )
137 131 134 136 3eqtr4i 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. 2 ) = ( ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) x. ( 2 x. F ) )
138 74 137 breqtri 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. 2 ) <_ ( ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) x. ( 2 x. F ) )
139 1 30 15 37 38 39 58 64 138 log2ublem1 
 |-  ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. sum_ n e. ( 0 ... N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) <_ ( 2 x. G )