MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  log2ublem3 Structured version   Unicode version

Theorem log2ublem3 20789
Description: Lemma for log2ub 20790. In decimal, this is a proof that the first four terms of the series for 
log 2 is less than  5 3
0 5 6  / 
7 6 5 4 5. (Contributed by Mario Carneiro, 17-Apr-2015.)
Assertion
Ref Expression
log2ublem3  |-  ( ( ( 3 ^ 7 )  x.  ( 5  x.  7 ) )  x.  sum_ n  e.  ( 0 ... 3 ) ( 2  /  (
( 3  x.  (
( 2  x.  n
)  +  1 ) )  x.  ( 9 ^ n ) ) ) )  <_ ;;;; 5 3 0 5 6

Proof of Theorem log2ublem3
StepHypRef Expression
1 0le0 10082 . . . . . . 7  |-  0  <_  0
2 0re 9092 . . . . . . . . . . . . 13  |-  0  e.  RR
3 ltm1 9851 . . . . . . . . . . . . 13  |-  ( 0  e.  RR  ->  (
0  -  1 )  <  0 )
42, 3ax-mp 8 . . . . . . . . . . . 12  |-  ( 0  -  1 )  <  0
5 0z 10294 . . . . . . . . . . . . 13  |-  0  e.  ZZ
6 peano2zm 10321 . . . . . . . . . . . . . 14  |-  ( 0  e.  ZZ  ->  (
0  -  1 )  e.  ZZ )
75, 6ax-mp 8 . . . . . . . . . . . . 13  |-  ( 0  -  1 )  e.  ZZ
8 fzn 11072 . . . . . . . . . . . . 13  |-  ( ( 0  e.  ZZ  /\  ( 0  -  1 )  e.  ZZ )  ->  ( ( 0  -  1 )  <  0  <->  ( 0 ... ( 0  -  1 ) )  =  (/) ) )
95, 7, 8mp2an 655 . . . . . . . . . . . 12  |-  ( ( 0  -  1 )  <  0  <->  ( 0 ... ( 0  -  1 ) )  =  (/) )
104, 9mpbi 201 . . . . . . . . . . 11  |-  ( 0 ... ( 0  -  1 ) )  =  (/)
1110sumeq1i 12493 . . . . . . . . . 10  |-  sum_ n  e.  ( 0 ... (
0  -  1 ) ) ( 2  / 
( ( 3  x.  ( ( 2  x.  n )  +  1 ) )  x.  (
9 ^ n ) ) )  =  sum_ n  e.  (/)  ( 2  / 
( ( 3  x.  ( ( 2  x.  n )  +  1 ) )  x.  (
9 ^ n ) ) )
12 sum0 12516 . . . . . . . . . 10  |-  sum_ n  e.  (/)  ( 2  / 
( ( 3  x.  ( ( 2  x.  n )  +  1 ) )  x.  (
9 ^ n ) ) )  =  0
1311, 12eqtri 2457 . . . . . . . . 9  |-  sum_ n  e.  ( 0 ... (
0  -  1 ) ) ( 2  / 
( ( 3  x.  ( ( 2  x.  n )  +  1 ) )  x.  (
9 ^ n ) ) )  =  0
1413oveq2i 6093 . . . . . . . 8  |-  ( ( ( 3 ^ 7 )  x.  ( 5  x.  7 ) )  x.  sum_ n  e.  ( 0 ... ( 0  -  1 ) ) ( 2  /  (
( 3  x.  (
( 2  x.  n
)  +  1 ) )  x.  ( 9 ^ n ) ) ) )  =  ( ( ( 3 ^ 7 )  x.  (
5  x.  7 ) )  x.  0 )
15 3cn 10073 . . . . . . . . . . 11  |-  3  e.  CC
16 7nn0 10244 . . . . . . . . . . 11  |-  7  e.  NN0
17 expcl 11400 . . . . . . . . . . 11  |-  ( ( 3  e.  CC  /\  7  e.  NN0 )  -> 
( 3 ^ 7 )  e.  CC )
1815, 16, 17mp2an 655 . . . . . . . . . 10  |-  ( 3 ^ 7 )  e.  CC
19 5nn 10137 . . . . . . . . . . . 12  |-  5  e.  NN
2019nncni 10011 . . . . . . . . . . 11  |-  5  e.  CC
21 7nn 10139 . . . . . . . . . . . 12  |-  7  e.  NN
2221nncni 10011 . . . . . . . . . . 11  |-  7  e.  CC
2320, 22mulcli 9096 . . . . . . . . . 10  |-  ( 5  x.  7 )  e.  CC
2418, 23mulcli 9096 . . . . . . . . 9  |-  ( ( 3 ^ 7 )  x.  ( 5  x.  7 ) )  e.  CC
2524mul01i 9257 . . . . . . . 8  |-  ( ( ( 3 ^ 7 )  x.  ( 5  x.  7 ) )  x.  0 )  =  0
2614, 25eqtri 2457 . . . . . . 7  |-  ( ( ( 3 ^ 7 )  x.  ( 5  x.  7 ) )  x.  sum_ n  e.  ( 0 ... ( 0  -  1 ) ) ( 2  /  (
( 3  x.  (
( 2  x.  n
)  +  1 ) )  x.  ( 9 ^ n ) ) ) )  =  0
27 2cn 10071 . . . . . . . 8  |-  2  e.  CC
2827mul01i 9257 . . . . . . 7  |-  ( 2  x.  0 )  =  0
291, 26, 283brtr4i 4241 . . . . . 6  |-  ( ( ( 3 ^ 7 )  x.  ( 5  x.  7 ) )  x.  sum_ n  e.  ( 0 ... ( 0  -  1 ) ) ( 2  /  (
( 3  x.  (
( 2  x.  n
)  +  1 ) )  x.  ( 9 ^ n ) ) ) )  <_  (
2  x.  0 )
30 0nn0 10237 . . . . . 6  |-  0  e.  NN0
31 2nn0 10239 . . . . . . . . . 10  |-  2  e.  NN0
32 5nn0 10242 . . . . . . . . . 10  |-  5  e.  NN0
3331, 32deccl 10397 . . . . . . . . 9  |- ; 2 5  e.  NN0
3433, 32deccl 10397 . . . . . . . 8  |- ;; 2 5 5  e.  NN0
35 1nn0 10238 . . . . . . . 8  |-  1  e.  NN0
3634, 35deccl 10397 . . . . . . 7  |- ;;; 2 5 5 1  e.  NN0
3736, 32deccl 10397 . . . . . 6  |- ;;;; 2 5 5 1 5  e.  NN0
38 eqid 2437 . . . . . 6  |-  ( 0  -  1 )  =  ( 0  -  1 )
3937nn0cni 10234 . . . . . . 7  |- ;;;; 2 5 5 1 5  e.  CC
4039addid2i 9255 . . . . . 6  |-  ( 0  + ;;;; 2 5 5 1 5 )  = ;;;; 2 5 5 1 5
41 3nn0 10240 . . . . . 6  |-  3  e.  NN0
4215addid1i 9254 . . . . . 6  |-  ( 3  +  0 )  =  3
4339mulid2i 9094 . . . . . . 7  |-  ( 1  x. ;;;; 2 5 5 1 5 )  = ;;;; 2 5 5 1 5
4428oveq1i 6092 . . . . . . . . 9  |-  ( ( 2  x.  0 )  +  1 )  =  ( 0  +  1 )
45 0p1e1 10094 . . . . . . . . 9  |-  ( 0  +  1 )  =  1
4644, 45eqtri 2457 . . . . . . . 8  |-  ( ( 2  x.  0 )  +  1 )  =  1
4746oveq1i 6092 . . . . . . 7  |-  ( ( ( 2  x.  0 )  +  1 )  x. ;;;; 2 5 5 1 5 )  =  ( 1  x. ;;;; 2 5 5 1 5 )
4832, 16nn0mulcli 10259 . . . . . . . 8  |-  ( 5  x.  7 )  e. 
NN0
4916, 31deccl 10397 . . . . . . . 8  |- ; 7 2  e.  NN0
50 9nn0 10246 . . . . . . . 8  |-  9  e.  NN0
51 2p1e3 10104 . . . . . . . . 9  |-  ( 2  +  1 )  =  3
52 8nn0 10245 . . . . . . . . . 10  |-  8  e.  NN0
53 1p1e2 10095 . . . . . . . . . . 11  |-  ( 1  +  1 )  =  2
54 9nn 10141 . . . . . . . . . . . . . . 15  |-  9  e.  NN
5554nncni 10011 . . . . . . . . . . . . . 14  |-  9  e.  CC
56 exp1 11388 . . . . . . . . . . . . . 14  |-  ( 9  e.  CC  ->  (
9 ^ 1 )  =  9 )
5755, 56ax-mp 8 . . . . . . . . . . . . 13  |-  ( 9 ^ 1 )  =  9
5857oveq1i 6092 . . . . . . . . . . . 12  |-  ( ( 9 ^ 1 )  x.  9 )  =  ( 9  x.  9 )
59 9t9e81 10485 . . . . . . . . . . . 12  |-  ( 9  x.  9 )  = ; 8
1
6058, 59eqtri 2457 . . . . . . . . . . 11  |-  ( ( 9 ^ 1 )  x.  9 )  = ; 8
1
6150, 35, 53, 60numexpp1 13415 . . . . . . . . . 10  |-  ( 9 ^ 2 )  = ; 8
1
62 8nn 10140 . . . . . . . . . . . . . 14  |-  8  e.  NN
6362nncni 10011 . . . . . . . . . . . . 13  |-  8  e.  CC
64 9t8e72 10484 . . . . . . . . . . . . 13  |-  ( 9  x.  8 )  = ; 7
2
6555, 63, 64mulcomli 9098 . . . . . . . . . . . 12  |-  ( 8  x.  9 )  = ; 7
2
6665oveq1i 6092 . . . . . . . . . . 11  |-  ( ( 8  x.  9 )  +  0 )  =  (; 7 2  +  0 )
6749nn0cni 10234 . . . . . . . . . . . 12  |- ; 7 2  e.  CC
6867addid1i 9254 . . . . . . . . . . 11  |-  (; 7 2  +  0 )  = ; 7 2
6966, 68eqtri 2457 . . . . . . . . . 10  |-  ( ( 8  x.  9 )  +  0 )  = ; 7
2
7055mulid2i 9094 . . . . . . . . . . 11  |-  ( 1  x.  9 )  =  9
7150dec0h 10399 . . . . . . . . . . 11  |-  9  = ; 0 9
7270, 71eqtri 2457 . . . . . . . . . 10  |-  ( 1  x.  9 )  = ; 0
9
7350, 52, 35, 61, 50, 30, 69, 72decmul1c 10430 . . . . . . . . 9  |-  ( ( 9 ^ 2 )  x.  9 )  = ;; 7 2 9
7450, 31, 51, 73numexpp1 13415 . . . . . . . 8  |-  ( 9 ^ 3 )  = ;; 7 2 9
7541, 35deccl 10397 . . . . . . . 8  |- ; 3 1  e.  NN0
76 eqid 2437 . . . . . . . . 9  |- ; 7 2  = ; 7 2
77 eqid 2437 . . . . . . . . 9  |- ; 3 1  = ; 3 1
78 7t5e35 10468 . . . . . . . . . . 11  |-  ( 7  x.  5 )  = ; 3
5
7922, 20, 78mulcomli 9098 . . . . . . . . . 10  |-  ( 5  x.  7 )  = ; 3
5
80 7p3e10 10125 . . . . . . . . . . . 12  |-  ( 7  +  3 )  =  10
8122, 15, 80addcomli 9259 . . . . . . . . . . 11  |-  ( 3  +  7 )  =  10
82 dec10 10413 . . . . . . . . . . 11  |-  10  = ; 1 0
8381, 82eqtri 2457 . . . . . . . . . 10  |-  ( 3  +  7 )  = ; 1
0
84 ax-1cn 9049 . . . . . . . . . . . . 13  |-  1  e.  CC
85 3p1e4 10105 . . . . . . . . . . . . 13  |-  ( 3  +  1 )  =  4
8615, 84, 85addcomli 9259 . . . . . . . . . . . 12  |-  ( 1  +  3 )  =  4
8786oveq2i 6093 . . . . . . . . . . 11  |-  ( ( 3  x.  7 )  +  ( 1  +  3 ) )  =  ( ( 3  x.  7 )  +  4 )
88 4nn0 10241 . . . . . . . . . . . 12  |-  4  e.  NN0
89 7t3e21 10466 . . . . . . . . . . . . 13  |-  ( 7  x.  3 )  = ; 2
1
9022, 15, 89mulcomli 9098 . . . . . . . . . . . 12  |-  ( 3  x.  7 )  = ; 2
1
91 4cn 10075 . . . . . . . . . . . . 13  |-  4  e.  CC
92 4p1e5 10106 . . . . . . . . . . . . 13  |-  ( 4  +  1 )  =  5
9391, 84, 92addcomli 9259 . . . . . . . . . . . 12  |-  ( 1  +  4 )  =  5
9431, 35, 88, 90, 93decaddi 10427 . . . . . . . . . . 11  |-  ( ( 3  x.  7 )  +  4 )  = ; 2
5
9587, 94eqtri 2457 . . . . . . . . . 10  |-  ( ( 3  x.  7 )  +  ( 1  +  3 ) )  = ; 2
5
9679oveq1i 6092 . . . . . . . . . . 11  |-  ( ( 5  x.  7 )  +  0 )  =  (; 3 5  +  0 )
9741, 32deccl 10397 . . . . . . . . . . . . 13  |- ; 3 5  e.  NN0
9897nn0cni 10234 . . . . . . . . . . . 12  |- ; 3 5  e.  CC
9998addid1i 9254 . . . . . . . . . . 11  |-  (; 3 5  +  0 )  = ; 3 5
10096, 99eqtri 2457 . . . . . . . . . 10  |-  ( ( 5  x.  7 )  +  0 )  = ; 3
5
10141, 32, 35, 30, 79, 83, 16, 32, 41, 95, 100decmac 10422 . . . . . . . . 9  |-  ( ( ( 5  x.  7 )  x.  7 )  +  ( 3  +  7 ) )  = ;; 2 5 5
10235dec0h 10399 . . . . . . . . . 10  |-  1  = ; 0 1
103 3t2e6 10129 . . . . . . . . . . . 12  |-  ( 3  x.  2 )  =  6
104103, 45oveq12i 6094 . . . . . . . . . . 11  |-  ( ( 3  x.  2 )  +  ( 0  +  1 ) )  =  ( 6  +  1 )
105 6p1e7 10108 . . . . . . . . . . 11  |-  ( 6  +  1 )  =  7
106104, 105eqtri 2457 . . . . . . . . . 10  |-  ( ( 3  x.  2 )  +  ( 0  +  1 ) )  =  7
107 5t2e10 10132 . . . . . . . . . . . 12  |-  ( 5  x.  2 )  =  10
108107, 82eqtri 2457 . . . . . . . . . . 11  |-  ( 5  x.  2 )  = ; 1
0
10935, 30, 45, 108decsuc 10406 . . . . . . . . . 10  |-  ( ( 5  x.  2 )  +  1 )  = ; 1
1
11041, 32, 30, 35, 79, 102, 31, 35, 35, 106, 109decmac 10422 . . . . . . . . 9  |-  ( ( ( 5  x.  7 )  x.  2 )  +  1 )  = ; 7
1
11116, 31, 41, 35, 76, 77, 48, 35, 16, 101, 110decma2c 10423 . . . . . . . 8  |-  ( ( ( 5  x.  7 )  x. ; 7 2 )  + ; 3
1 )  = ;;; 2 5 5 1
112 9t3e27 10479 . . . . . . . . . . 11  |-  ( 9  x.  3 )  = ; 2
7
11355, 15, 112mulcomli 9098 . . . . . . . . . 10  |-  ( 3  x.  9 )  = ; 2
7
114 7p4e11 10435 . . . . . . . . . 10  |-  ( 7  +  4 )  = ; 1
1
11531, 16, 88, 113, 51, 35, 114decaddci 10428 . . . . . . . . 9  |-  ( ( 3  x.  9 )  +  4 )  = ; 3
1
116 9t5e45 10481 . . . . . . . . . 10  |-  ( 9  x.  5 )  = ; 4
5
11755, 20, 116mulcomli 9098 . . . . . . . . 9  |-  ( 5  x.  9 )  = ; 4
5
11850, 41, 32, 79, 32, 88, 115, 117decmul1c 10430 . . . . . . . 8  |-  ( ( 5  x.  7 )  x.  9 )  = ;; 3 1 5
11948, 49, 50, 74, 32, 75, 111, 118decmul2c 10431 . . . . . . 7  |-  ( ( 5  x.  7 )  x.  ( 9 ^ 3 ) )  = ;;;; 2 5 5 1 5
12043, 47, 1193eqtr4ri 2468 . . . . . 6  |-  ( ( 5  x.  7 )  x.  ( 9 ^ 3 ) )  =  ( ( ( 2  x.  0 )  +  1 )  x. ;;;; 2 5 5 1 5 )
12129, 30, 37, 30, 38, 40, 41, 42, 120log2ublem2 20788 . . . . 5  |-  ( ( ( 3 ^ 7 )  x.  ( 5  x.  7 ) )  x.  sum_ n  e.  ( 0 ... 0 ) ( 2  /  (
( 3  x.  (
( 2  x.  n
)  +  1 ) )  x.  ( 9 ^ n ) ) ) )  <_  (
2  x. ;;;; 2 5 5 1 5 )
12250, 88deccl 10397 . . . . . 6  |- ; 9 4  e.  NN0
123122, 32deccl 10397 . . . . 5  |- ;; 9 4 5  e.  NN0
124 1m1e0 10069 . . . . 5  |-  ( 1  -  1 )  =  0
125 eqid 2437 . . . . . 6  |- ;;;; 2 5 5 1 5  = ;;;; 2 5 5 1 5
126 eqid 2437 . . . . . 6  |- ;; 9 4 5  = ;; 9 4 5
127 6nn0 10243 . . . . . . . . 9  |-  6  e.  NN0
12831, 127deccl 10397 . . . . . . . 8  |- ; 2 6  e.  NN0
129128, 88deccl 10397 . . . . . . 7  |- ;; 2 6 4  e.  NN0
130 5p1e6 10107 . . . . . . 7  |-  ( 5  +  1 )  =  6
131 eqid 2437 . . . . . . . 8  |- ;;; 2 5 5 1  = ;;; 2 5 5 1
132 eqid 2437 . . . . . . . 8  |- ; 9 4  = ; 9 4
133 eqid 2437 . . . . . . . . 9  |- ;; 2 5 5  = ;; 2 5 5
134 eqid 2437 . . . . . . . . . 10  |- ; 2 5  = ; 2 5
13531, 32, 130, 134decsuc 10406 . . . . . . . . 9  |-  (; 2 5  +  1 )  = ; 2 6
136 9p5e14 10448 . . . . . . . . . 10  |-  ( 9  +  5 )  = ; 1
4
13755, 20, 136addcomli 9259 . . . . . . . . 9  |-  ( 5  +  9 )  = ; 1
4
13833, 32, 50, 133, 135, 88, 137decaddci 10428 . . . . . . . 8  |-  (;; 2 5 5  +  9 )  = ;; 2 6 4
13934, 35, 50, 88, 131, 132, 138, 93decadd 10424 . . . . . . 7  |-  (;;; 2 5 5 1  + ; 9 4 )  = ;;; 2 6 4 5
140129, 32, 130, 139decsuc 10406 . . . . . 6  |-  ( (;;; 2 5 5 1  + ; 9
4 )  +  1 )  = ;;; 2 6 4 6
141 5p5e10 10120 . . . . . 6  |-  ( 5  +  5 )  =  10
14236, 32, 122, 32, 125, 126, 140, 141decaddc2 10426 . . . . 5  |-  (;;;; 2 5 5 1 5  + ;; 9 4 5 )  = ;;;; 2 6 4 6 0
14355sqvali 11462 . . . . . . . . 9  |-  ( 9 ^ 2 )  =  ( 9  x.  9 )
144 3t3e9 10130 . . . . . . . . . 10  |-  ( 3  x.  3 )  =  9
145144oveq1i 6092 . . . . . . . . 9  |-  ( ( 3  x.  3 )  x.  9 )  =  ( 9  x.  9 )
146143, 145eqtr4i 2460 . . . . . . . 8  |-  ( 9 ^ 2 )  =  ( ( 3  x.  3 )  x.  9 )
14715, 15, 55mulassi 9100 . . . . . . . 8  |-  ( ( 3  x.  3 )  x.  9 )  =  ( 3  x.  (
3  x.  9 ) )
148146, 147eqtri 2457 . . . . . . 7  |-  ( 9 ^ 2 )  =  ( 3  x.  (
3  x.  9 ) )
149148oveq2i 6093 . . . . . 6  |-  ( ( 5  x.  7 )  x.  ( 9 ^ 2 ) )  =  ( ( 5  x.  7 )  x.  (
3  x.  ( 3  x.  9 ) ) )
15015, 55mulcli 9096 . . . . . . . 8  |-  ( 3  x.  9 )  e.  CC
15123, 15, 150mul12i 9262 . . . . . . 7  |-  ( ( 5  x.  7 )  x.  ( 3  x.  ( 3  x.  9 ) ) )  =  ( 3  x.  (
( 5  x.  7 )  x.  ( 3  x.  9 ) ) )
15231, 88deccl 10397 . . . . . . . . 9  |- ; 2 4  e.  NN0
153 eqid 2437 . . . . . . . . . 10  |- ; 2 4  = ; 2 4
154103, 51oveq12i 6094 . . . . . . . . . . 11  |-  ( ( 3  x.  2 )  +  ( 2  +  1 ) )  =  ( 6  +  3 )
155 6p3e9 10122 . . . . . . . . . . 11  |-  ( 6  +  3 )  =  9
156154, 155eqtri 2457 . . . . . . . . . 10  |-  ( ( 3  x.  2 )  +  ( 2  +  1 ) )  =  9
15791addid2i 9255 . . . . . . . . . . 11  |-  ( 0  +  4 )  =  4
15835, 30, 88, 108, 157decaddi 10427 . . . . . . . . . 10  |-  ( ( 5  x.  2 )  +  4 )  = ; 1
4
15941, 32, 31, 88, 79, 153, 31, 88, 35, 156, 158decmac 10422 . . . . . . . . 9  |-  ( ( ( 5  x.  7 )  x.  2 )  + ; 2 4 )  = ; 9
4
16031, 35, 41, 90, 86decaddi 10427 . . . . . . . . . 10  |-  ( ( 3  x.  7 )  +  3 )  = ; 2
4
16116, 41, 32, 79, 32, 41, 160, 79decmul1c 10430 . . . . . . . . 9  |-  ( ( 5  x.  7 )  x.  7 )  = ;; 2 4 5
16248, 31, 16, 113, 32, 152, 159, 161decmul2c 10431 . . . . . . . 8  |-  ( ( 5  x.  7 )  x.  ( 3  x.  9 ) )  = ;; 9 4 5
163162oveq2i 6093 . . . . . . 7  |-  ( 3  x.  ( ( 5  x.  7 )  x.  ( 3  x.  9 ) ) )  =  ( 3  x. ;; 9 4 5 )
164151, 163eqtri 2457 . . . . . 6  |-  ( ( 5  x.  7 )  x.  ( 3  x.  ( 3  x.  9 ) ) )  =  ( 3  x. ;; 9 4 5 )
165 df-3 10060 . . . . . . . 8  |-  3  =  ( 2  +  1 )
16627mulid1i 9093 . . . . . . . . 9  |-  ( 2  x.  1 )  =  2
167166oveq1i 6092 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  1 )  =  ( 2  +  1 )
168165, 167eqtr4i 2460 . . . . . . 7  |-  3  =  ( ( 2  x.  1 )  +  1 )
169168oveq1i 6092 . . . . . 6  |-  ( 3  x. ;; 9 4 5 )  =  ( ( ( 2  x.  1 )  +  1 )  x. ;; 9 4 5 )
170149, 164, 1693eqtri 2461 . . . . 5  |-  ( ( 5  x.  7 )  x.  ( 9 ^ 2 ) )  =  ( ( ( 2  x.  1 )  +  1 )  x. ;; 9 4 5 )
171121, 37, 123, 35, 124, 142, 31, 51, 170log2ublem2 20788 . . . 4  |-  ( ( ( 3 ^ 7 )  x.  ( 5  x.  7 ) )  x.  sum_ n  e.  ( 0 ... 1 ) ( 2  /  (
( 3  x.  (
( 2  x.  n
)  +  1 ) )  x.  ( 9 ^ n ) ) ) )  <_  (
2  x. ;;;; 2 6 4 6 0 )
172129, 127deccl 10397 . . . . 5  |- ;;; 2 6 4 6  e.  NN0
173172, 30deccl 10397 . . . 4  |- ;;;; 2 6 4 6 0  e.  NN0
174127, 41deccl 10397 . . . 4  |- ; 6 3  e.  NN0
175 2m1e1 10096 . . . 4  |-  ( 2  -  1 )  =  1
176 eqid 2437 . . . . 5  |- ;;;; 2 6 4 6 0  = ;;;; 2 6 4 6 0
177 eqid 2437 . . . . 5  |- ; 6 3  = ; 6 3
178 eqid 2437 . . . . . 6  |- ;;; 2 6 4 6  = ;;; 2 6 4 6
179 eqid 2437 . . . . . . 7  |- ;; 2 6 4  = ;; 2 6 4
180128, 88, 92, 179decsuc 10406 . . . . . 6  |-  (;; 2 6 4  +  1 )  = ;; 2 6 5
181 6p6e12 10434 . . . . . 6  |-  ( 6  +  6 )  = ; 1
2
182129, 127, 127, 178, 180, 31, 181decaddci 10428 . . . . 5  |-  (;;; 2 6 4 6  +  6 )  = ;;; 2 6 5 2
18315addid2i 9255 . . . . 5  |-  ( 0  +  3 )  =  3
184172, 30, 127, 41, 176, 177, 182, 183decadd 10424 . . . 4  |-  (;;;; 2 6 4 6 0  + ; 6 3 )  = ;;;; 2 6 5 2 3
18584, 27addcomi 9258 . . . . 5  |-  ( 1  +  2 )  =  ( 2  +  1 )
186185, 165eqtr4i 2460 . . . 4  |-  ( 1  +  2 )  =  3
18757oveq2i 6093 . . . . 5  |-  ( ( 5  x.  7 )  x.  ( 9 ^ 1 ) )  =  ( ( 5  x.  7 )  x.  9 )
18820, 22, 55mulassi 9100 . . . . . 6  |-  ( ( 5  x.  7 )  x.  9 )  =  ( 5  x.  (
7  x.  9 ) )
189 9t7e63 10483 . . . . . . . 8  |-  ( 9  x.  7 )  = ; 6
3
19055, 22, 189mulcomli 9098 . . . . . . 7  |-  ( 7  x.  9 )  = ; 6
3
191190oveq2i 6093 . . . . . 6  |-  ( 5  x.  ( 7  x.  9 ) )  =  ( 5  x. ; 6 3 )
192188, 191eqtri 2457 . . . . 5  |-  ( ( 5  x.  7 )  x.  9 )  =  ( 5  x. ; 6 3 )
193 df-5 10062 . . . . . . 7  |-  5  =  ( 4  +  1 )
194 2t2e4 10128 . . . . . . . 8  |-  ( 2  x.  2 )  =  4
195194oveq1i 6092 . . . . . . 7  |-  ( ( 2  x.  2 )  +  1 )  =  ( 4  +  1 )
196193, 195eqtr4i 2460 . . . . . 6  |-  5  =  ( ( 2  x.  2 )  +  1 )
197196oveq1i 6092 . . . . 5  |-  ( 5  x. ; 6 3 )  =  ( ( ( 2  x.  2 )  +  1 )  x. ; 6 3 )
198187, 192, 1973eqtri 2461 . . . 4  |-  ( ( 5  x.  7 )  x.  ( 9 ^ 1 ) )  =  ( ( ( 2  x.  2 )  +  1 )  x. ; 6 3 )
199171, 173, 174, 31, 175, 184, 35, 186, 198log2ublem2 20788 . . 3  |-  ( ( ( 3 ^ 7 )  x.  ( 5  x.  7 ) )  x.  sum_ n  e.  ( 0 ... 2 ) ( 2  /  (
( 3  x.  (
( 2  x.  n
)  +  1 ) )  x.  ( 9 ^ n ) ) ) )  <_  (
2  x. ;;;; 2 6 5 2 3 )
200128, 32deccl 10397 . . . . 5  |- ;; 2 6 5  e.  NN0
201200, 31deccl 10397 . . . 4  |- ;;; 2 6 5 2  e.  NN0
202201, 41deccl 10397 . . 3  |- ;;;; 2 6 5 2 3  e.  NN0
203 3m1e2 10097 . . 3  |-  ( 3  -  1 )  =  2
204 eqid 2437 . . . 4  |- ;;;; 2 6 5 2 3  = ;;;; 2 6 5 2 3
205 5p3e8 10118 . . . . 5  |-  ( 5  +  3 )  =  8
20620, 15, 205addcomli 9259 . . . 4  |-  ( 3  +  5 )  =  8
207201, 41, 32, 204, 206decaddi 10427 . . 3  |-  (;;;; 2 6 5 2 3  +  5 )  = ;;;; 2 6 5 2 8
20822, 20mulcli 9096 . . . . 5  |-  ( 7  x.  5 )  e.  CC
209208mulid1i 9093 . . . 4  |-  ( ( 7  x.  5 )  x.  1 )  =  ( 7  x.  5 )
21020, 22mulcomi 9097 . . . . 5  |-  ( 5  x.  7 )  =  ( 7  x.  5 )
211 exp0 11387 . . . . . 6  |-  ( 9  e.  CC  ->  (
9 ^ 0 )  =  1 )
21255, 211ax-mp 8 . . . . 5  |-  ( 9 ^ 0 )  =  1
213210, 212oveq12i 6094 . . . 4  |-  ( ( 5  x.  7 )  x.  ( 9 ^ 0 ) )  =  ( ( 7  x.  5 )  x.  1 )
21415, 27, 103mulcomli 9098 . . . . . . 7  |-  ( 2  x.  3 )  =  6
215214oveq1i 6092 . . . . . 6  |-  ( ( 2  x.  3 )  +  1 )  =  ( 6  +  1 )
216 df-7 10064 . . . . . 6  |-  7  =  ( 6  +  1 )
217215, 216eqtr4i 2460 . . . . 5  |-  ( ( 2  x.  3 )  +  1 )  =  7
218217oveq1i 6092 . . . 4  |-  ( ( ( 2  x.  3 )  +  1 )  x.  5 )  =  ( 7  x.  5 )
219209, 213, 2183eqtr4i 2467 . . 3  |-  ( ( 5  x.  7 )  x.  ( 9 ^ 0 ) )  =  ( ( ( 2  x.  3 )  +  1 )  x.  5 )
220199, 202, 32, 41, 203, 207, 30, 183, 219log2ublem2 20788 . 2  |-  ( ( ( 3 ^ 7 )  x.  ( 5  x.  7 ) )  x.  sum_ n  e.  ( 0 ... 3 ) ( 2  /  (
( 3  x.  (
( 2  x.  n
)  +  1 ) )  x.  ( 9 ^ n ) ) ) )  <_  (
2  x. ;;;; 2 6 5 2 8 )
221 eqid 2437 . . 3  |- ;;;; 2 6 5 2 8  = ;;;; 2 6 5 2 8
222 eqid 2437 . . . 4  |- ;;; 2 6 5 2  = ;;; 2 6 5 2
223 eqid 2437 . . . . 5  |- ;; 2 6 5  = ;; 2 6 5
224 00id 9242 . . . . . 6  |-  ( 0  +  0 )  =  0
22530dec0h 10399 . . . . . 6  |-  0  = ; 0 0
226224, 225eqtri 2457 . . . . 5  |-  ( 0  +  0 )  = ; 0
0
227 eqid 2437 . . . . . 6  |- ; 2 6  = ; 2 6
22845, 102eqtri 2457 . . . . . 6  |-  ( 0  +  1 )  = ; 0
1
229194, 45oveq12i 6094 . . . . . . 7  |-  ( ( 2  x.  2 )  +  ( 0  +  1 ) )  =  ( 4  +  1 )
230229, 92eqtri 2457 . . . . . 6  |-  ( ( 2  x.  2 )  +  ( 0  +  1 ) )  =  5
231 6nn 10138 . . . . . . . . 9  |-  6  e.  NN
232231nncni 10011 . . . . . . . 8  |-  6  e.  CC
233 6t2e12 10460 . . . . . . . 8  |-  ( 6  x.  2 )  = ; 1
2
234232, 27, 233mulcomli 9098 . . . . . . 7  |-  ( 2  x.  6 )  = ; 1
2
23535, 31, 51, 234decsuc 10406 . . . . . 6  |-  ( ( 2  x.  6 )  +  1 )  = ; 1
3
23631, 127, 30, 35, 227, 228, 31, 41, 35, 230, 235decma2c 10423 . . . . 5  |-  ( ( 2  x. ; 2 6 )  +  ( 0  +  1 ) )  = ; 5 3
23720, 27, 107mulcomli 9098 . . . . . . 7  |-  ( 2  x.  5 )  =  10
238237oveq1i 6092 . . . . . 6  |-  ( ( 2  x.  5 )  +  0 )  =  ( 10  +  0 )
239 dec10p 10412 . . . . . 6  |-  ( 10  +  0 )  = ; 1
0
240238, 239eqtri 2457 . . . . 5  |-  ( ( 2  x.  5 )  +  0 )  = ; 1
0
241128, 32, 30, 30, 223, 226, 31, 30, 35, 236, 240decma2c 10423 . . . 4  |-  ( ( 2  x. ;; 2 6 5 )  +  ( 0  +  0 ) )  = ;; 5 3 0
24232dec0h 10399 . . . . 5  |-  5  = ; 0 5
243195, 92, 2423eqtri 2461 . . . 4  |-  ( ( 2  x.  2 )  +  1 )  = ; 0
5
244200, 31, 30, 35, 222, 102, 31, 32, 30, 241, 243decma2c 10423 . . 3  |-  ( ( 2  x. ;;; 2 6 5 2 )  +  1 )  = ;;; 5 3 0 5
245 8t2e16 10471 . . . 4  |-  ( 8  x.  2 )  = ; 1
6
24663, 27, 245mulcomli 9098 . . 3  |-  ( 2  x.  8 )  = ; 1
6
24731, 201, 52, 221, 127, 35, 244, 246decmul2c 10431 . 2  |-  ( 2  x. ;;;; 2 6 5 2 8 )  = ;;;; 5 3 0 5 6
248220, 247breqtri 4236 1  |-  ( ( ( 3 ^ 7 )  x.  ( 5  x.  7 ) )  x.  sum_ n  e.  ( 0 ... 3 ) ( 2  /  (
( 3  x.  (
( 2  x.  n
)  +  1 ) )  x.  ( 9 ^ n ) ) ) )  <_ ;;;; 5 3 0 5 6
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1653    e. wcel 1726   (/)c0 3629   class class class wbr 4213  (class class class)co 6082   CCcc 8989   RRcr 8990   0cc0 8991   1c1 8992    + caddc 8994    x. cmul 8996    < clt 9121    <_ cle 9122    - cmin 9292    / cdiv 9678   2c2 10050   3c3 10051   4c4 10052   5c5 10053   6c6 10054   7c7 10055   8c8 10056   9c9 10057   10c10 10058   NN0cn0 10222   ZZcz 10283  ;cdc 10383   ...cfz 11044   ^cexp 11383   sum_csu 12480
This theorem is referenced by:  log2ub  20790
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-rep 4321  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-inf2 7597  ax-cnex 9047  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060  ax-1rid 9061  ax-rnegex 9062  ax-rrecex 9063  ax-cnre 9064  ax-pre-lttri 9065  ax-pre-lttrn 9066  ax-pre-ltadd 9067  ax-pre-mulgt0 9068  ax-pre-sup 9069
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-reu 2713  df-rmo 2714  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-int 4052  df-iun 4096  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-se 4543  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-isom 5464  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-1st 6350  df-2nd 6351  df-riota 6550  df-recs 6634  df-rdg 6669  df-1o 6725  df-oadd 6729  df-er 6906  df-en 7111  df-dom 7112  df-sdom 7113  df-fin 7114  df-sup 7447  df-oi 7480  df-card 7827  df-pnf 9123  df-mnf 9124  df-xr 9125  df-ltxr 9126  df-le 9127  df-sub 9294  df-neg 9295  df-div 9679  df-nn 10002  df-2 10059  df-3 10060  df-4 10061  df-5 10062  df-6 10063  df-7 10064  df-8 10065  df-9 10066  df-10 10067  df-n0 10223  df-z 10284  df-dec 10384  df-uz 10490  df-rp 10614  df-fz 11045  df-fzo 11137  df-seq 11325  df-exp 11384  df-hash 11620  df-cj 11905  df-re 11906  df-im 11907  df-sqr 12041  df-abs 12042  df-clim 12283  df-sum 12481
  Copyright terms: Public domain W3C validator