# Metamath Proof Explorer

## Theorem 2exp16

Description: Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 2exp16 ${⊢}{2}^{16}=65536$

### Proof

Step Hyp Ref Expression
1 2nn0 ${⊢}2\in {ℕ}_{0}$
2 8nn0 ${⊢}8\in {ℕ}_{0}$
3 8cn ${⊢}8\in ℂ$
4 2cn ${⊢}2\in ℂ$
5 8t2e16 ${⊢}8\cdot 2=16$
6 3 4 5 mulcomli ${⊢}2\cdot 8=16$
7 2exp8 ${⊢}{2}^{8}=256$
8 5nn0 ${⊢}5\in {ℕ}_{0}$
9 1 8 deccl ${⊢}25\in {ℕ}_{0}$
10 6nn0 ${⊢}6\in {ℕ}_{0}$
11 9 10 deccl ${⊢}256\in {ℕ}_{0}$
12 eqid ${⊢}256=256$
13 1nn0 ${⊢}1\in {ℕ}_{0}$
14 13 8 deccl ${⊢}15\in {ℕ}_{0}$
15 3nn0 ${⊢}3\in {ℕ}_{0}$
16 14 15 deccl ${⊢}153\in {ℕ}_{0}$
17 eqid ${⊢}25=25$
18 eqid ${⊢}153=153$
19 13 1 deccl ${⊢}12\in {ℕ}_{0}$
20 19 2 deccl ${⊢}128\in {ℕ}_{0}$
21 4nn0 ${⊢}4\in {ℕ}_{0}$
22 13 21 deccl ${⊢}14\in {ℕ}_{0}$
23 eqid ${⊢}15=15$
24 eqid ${⊢}128=128$
25 0nn0 ${⊢}0\in {ℕ}_{0}$
26 13 dec0h ${⊢}1=01$
27 eqid ${⊢}12=12$
28 0p1e1 ${⊢}0+1=1$
29 1p2e3 ${⊢}1+2=3$
30 25 13 13 1 26 27 28 29 decadd ${⊢}1+12=13$
31 3p1e4 ${⊢}3+1=4$
32 13 15 13 30 31 decaddi ${⊢}1+12+1=14$
33 5cn ${⊢}5\in ℂ$
34 8p5e13 ${⊢}8+5=13$
35 3 33 34 addcomli ${⊢}5+8=13$
36 13 8 19 2 23 24 32 15 35 decaddc ${⊢}15+128=143$
37 eqid ${⊢}14=14$
38 4p1e5 ${⊢}4+1=5$
39 13 21 13 37 38 decaddi ${⊢}14+1=15$
40 2t2e4 ${⊢}2\cdot 2=4$
41 1p1e2 ${⊢}1+1=2$
42 40 41 oveq12i ${⊢}2\cdot 2+1+1=4+2$
43 4p2e6 ${⊢}4+2=6$
44 42 43 eqtri ${⊢}2\cdot 2+1+1=6$
45 5t2e10 ${⊢}5\cdot 2=10$
46 33 addid2i ${⊢}0+5=5$
47 13 25 8 45 46 decaddi ${⊢}5\cdot 2+5=15$
48 1 8 13 8 17 39 1 8 13 44 47 decmac ${⊢}25\cdot 2+14+1=65$
49 6t2e12 ${⊢}6\cdot 2=12$
50 3cn ${⊢}3\in ℂ$
51 3p2e5 ${⊢}3+2=5$
52 50 4 51 addcomli ${⊢}2+3=5$
53 13 1 15 49 52 decaddi ${⊢}6\cdot 2+3=15$
54 9 10 22 15 12 36 1 8 13 48 53 decmac ${⊢}256\cdot 2+15+128=655$
55 15 dec0h ${⊢}3=03$
56 50 addid2i ${⊢}0+3=3$
57 56 55 eqtri ${⊢}0+3=03$
58 4 addid2i ${⊢}0+2=2$
59 58 oveq2i ${⊢}2\cdot 5+0+2=2\cdot 5+2$
60 33 4 45 mulcomli ${⊢}2\cdot 5=10$
61 13 25 1 60 58 decaddi ${⊢}2\cdot 5+2=12$
62 59 61 eqtri ${⊢}2\cdot 5+0+2=12$
63 5t5e25 ${⊢}5\cdot 5=25$
64 5p3e8 ${⊢}5+3=8$
65 1 8 15 63 64 decaddi ${⊢}5\cdot 5+3=28$
66 1 8 25 15 17 57 8 2 1 62 65 decmac ${⊢}25\cdot 5+0+3=128$
67 6t5e30 ${⊢}6\cdot 5=30$
68 15 25 15 67 56 decaddi ${⊢}6\cdot 5+3=33$
69 9 10 25 15 12 55 8 15 15 66 68 decmac ${⊢}256\cdot 5+3=1283$
70 1 8 14 15 17 18 11 15 20 54 69 decma2c ${⊢}256\cdot 25+153=6553$
71 6cn ${⊢}6\in ℂ$
72 71 4 49 mulcomli ${⊢}2\cdot 6=12$
73 13 1 15 72 52 decaddi ${⊢}2\cdot 6+3=15$
74 71 33 67 mulcomli ${⊢}5\cdot 6=30$
75 15 25 15 74 56 decaddi ${⊢}5\cdot 6+3=33$
76 1 8 15 17 10 15 15 73 75 decrmac ${⊢}25\cdot 6+3=153$
77 6t6e36 ${⊢}6\cdot 6=36$
78 10 9 10 12 10 15 76 77 decmul1c ${⊢}256\cdot 6=1536$
79 11 9 10 12 10 16 70 78 decmul2c ${⊢}256\cdot 256=65536$
80 1 2 6 7 79 numexp2x ${⊢}{2}^{16}=65536$