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 ↑ 1 6 ) = 6 5 5 3 6

Proof

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