Metamath Proof Explorer

Theorem 2exp11

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

Proof

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 addlidi 
 |-  ( 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