Description: Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | 2exp11 | |- ( 2 ^ ; 1 1 ) = ; ; ; 2 0 4 8 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 8p3e11 | |- ( 8 + 3 ) = ; 1 1 |
|
2 | 1 | eqcomi | |- ; 1 1 = ( 8 + 3 ) |
3 | 2 | oveq2i | |- ( 2 ^ ; 1 1 ) = ( 2 ^ ( 8 + 3 ) ) |
4 | 2cn | |- 2 e. CC |
|
5 | 8nn0 | |- 8 e. NN0 |
|
6 | 3nn0 | |- 3 e. NN0 |
|
7 | expadd | |- ( ( 2 e. CC /\ 8 e. NN0 /\ 3 e. NN0 ) -> ( 2 ^ ( 8 + 3 ) ) = ( ( 2 ^ 8 ) x. ( 2 ^ 3 ) ) ) |
|
8 | 4 5 6 7 | mp3an | |- ( 2 ^ ( 8 + 3 ) ) = ( ( 2 ^ 8 ) x. ( 2 ^ 3 ) ) |
9 | 3 8 | eqtri | |- ( 2 ^ ; 1 1 ) = ( ( 2 ^ 8 ) x. ( 2 ^ 3 ) ) |
10 | 2exp8 | |- ( 2 ^ 8 ) = ; ; 2 5 6 |
|
11 | cu2 | |- ( 2 ^ 3 ) = 8 |
|
12 | 10 11 | oveq12i | |- ( ( 2 ^ 8 ) x. ( 2 ^ 3 ) ) = ( ; ; 2 5 6 x. 8 ) |
13 | 2nn0 | |- 2 e. NN0 |
|
14 | 5nn0 | |- 5 e. NN0 |
|
15 | 13 14 | deccl | |- ; 2 5 e. NN0 |
16 | 6nn0 | |- 6 e. NN0 |
|
17 | eqid | |- ; ; 2 5 6 = ; ; 2 5 6 |
|
18 | 4nn0 | |- 4 e. NN0 |
|
19 | 0nn0 | |- 0 e. NN0 |
|
20 | 13 19 | deccl | |- ; 2 0 e. NN0 |
21 | eqid | |- ; 2 5 = ; 2 5 |
|
22 | 1nn0 | |- 1 e. NN0 |
|
23 | 8cn | |- 8 e. CC |
|
24 | 8t2e16 | |- ( 8 x. 2 ) = ; 1 6 |
|
25 | 23 4 24 | mulcomli | |- ( 2 x. 8 ) = ; 1 6 |
26 | 1p1e2 | |- ( 1 + 1 ) = 2 |
|
27 | 6p4e10 | |- ( 6 + 4 ) = ; 1 0 |
|
28 | 22 16 18 25 26 19 27 | decaddci | |- ( ( 2 x. 8 ) + 4 ) = ; 2 0 |
29 | 5cn | |- 5 e. CC |
|
30 | 8t5e40 | |- ( 8 x. 5 ) = ; 4 0 |
|
31 | 23 29 30 | mulcomli | |- ( 5 x. 8 ) = ; 4 0 |
32 | 5 13 14 21 19 18 28 31 | decmul1c | |- ( ; 2 5 x. 8 ) = ; ; 2 0 0 |
33 | 4cn | |- 4 e. CC |
|
34 | 33 | addid2i | |- ( 0 + 4 ) = 4 |
35 | 20 19 18 32 34 | decaddi | |- ( ( ; 2 5 x. 8 ) + 4 ) = ; ; 2 0 4 |
36 | 6cn | |- 6 e. CC |
|
37 | 8t6e48 | |- ( 8 x. 6 ) = ; 4 8 |
|
38 | 23 36 37 | mulcomli | |- ( 6 x. 8 ) = ; 4 8 |
39 | 5 15 16 17 5 18 35 38 | decmul1c | |- ( ; ; 2 5 6 x. 8 ) = ; ; ; 2 0 4 8 |
40 | 12 39 | eqtri | |- ( ( 2 ^ 8 ) x. ( 2 ^ 3 ) ) = ; ; ; 2 0 4 8 |
41 | 9 40 | eqtri | |- ( 2 ^ ; 1 1 ) = ; ; ; 2 0 4 8 |