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 e. NN0
2 8nn0 
 |-  8 e. NN0
3 8cn 
 |-  8 e. CC
4 2cn 
 |-  2 e. CC
5 8t2e16 
 |-  ( 8 x. 2 ) = ; 1 6
6 3 4 5 mulcomli 
 |-  ( 2 x. 8 ) = ; 1 6
7 2exp8 
 |-  ( 2 ^ 8 ) = ; ; 2 5 6
8 5nn0 
 |-  5 e. NN0
9 1 8 deccl 
 |-  ; 2 5 e. NN0
10 6nn0 
 |-  6 e. NN0
11 9 10 deccl 
 |-  ; ; 2 5 6 e. NN0
12 eqid 
 |-  ; ; 2 5 6 = ; ; 2 5 6
13 1nn0 
 |-  1 e. NN0
14 13 8 deccl 
 |-  ; 1 5 e. NN0
15 3nn0 
 |-  3 e. NN0
16 14 15 deccl 
 |-  ; ; 1 5 3 e. NN0
17 eqid 
 |-  ; 2 5 = ; 2 5
18 eqid 
 |-  ; ; 1 5 3 = ; ; 1 5 3
19 13 1 deccl 
 |-  ; 1 2 e. NN0
20 19 2 deccl 
 |-  ; ; 1 2 8 e. NN0
21 4nn0 
 |-  4 e. NN0
22 13 21 deccl 
 |-  ; 1 4 e. NN0
23 eqid 
 |-  ; 1 5 = ; 1 5
24 eqid 
 |-  ; ; 1 2 8 = ; ; 1 2 8
25 0nn0 
 |-  0 e. NN0
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 e. CC
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 x. 2 ) = 4
41 1p1e2 
 |-  ( 1 + 1 ) = 2
42 40 41 oveq12i 
 |-  ( ( 2 x. 2 ) + ( 1 + 1 ) ) = ( 4 + 2 )
43 4p2e6 
 |-  ( 4 + 2 ) = 6
44 42 43 eqtri 
 |-  ( ( 2 x. 2 ) + ( 1 + 1 ) ) = 6
45 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
46 33 addlidi 
 |-  ( 0 + 5 ) = 5
47 13 25 8 45 46 decaddi 
 |-  ( ( 5 x. 2 ) + 5 ) = ; 1 5
48 1 8 13 8 17 39 1 8 13 44 47 decmac 
 |-  ( ( ; 2 5 x. 2 ) + ( ; 1 4 + 1 ) ) = ; 6 5
49 6t2e12 
 |-  ( 6 x. 2 ) = ; 1 2
50 3cn 
 |-  3 e. CC
51 3p2e5 
 |-  ( 3 + 2 ) = 5
52 50 4 51 addcomli 
 |-  ( 2 + 3 ) = 5
53 13 1 15 49 52 decaddi 
 |-  ( ( 6 x. 2 ) + 3 ) = ; 1 5
54 9 10 22 15 12 36 1 8 13 48 53 decmac 
 |-  ( ( ; ; 2 5 6 x. 2 ) + ( ; 1 5 + ; ; 1 2 8 ) ) = ; ; 6 5 5
55 15 dec0h 
 |-  3 = ; 0 3
56 50 addlidi 
 |-  ( 0 + 3 ) = 3
57 56 55 eqtri 
 |-  ( 0 + 3 ) = ; 0 3
58 4 addlidi 
 |-  ( 0 + 2 ) = 2
59 58 oveq2i 
 |-  ( ( 2 x. 5 ) + ( 0 + 2 ) ) = ( ( 2 x. 5 ) + 2 )
60 33 4 45 mulcomli 
 |-  ( 2 x. 5 ) = ; 1 0
61 13 25 1 60 58 decaddi 
 |-  ( ( 2 x. 5 ) + 2 ) = ; 1 2
62 59 61 eqtri 
 |-  ( ( 2 x. 5 ) + ( 0 + 2 ) ) = ; 1 2
63 5t5e25 
 |-  ( 5 x. 5 ) = ; 2 5
64 5p3e8 
 |-  ( 5 + 3 ) = 8
65 1 8 15 63 64 decaddi 
 |-  ( ( 5 x. 5 ) + 3 ) = ; 2 8
66 1 8 25 15 17 57 8 2 1 62 65 decmac 
 |-  ( ( ; 2 5 x. 5 ) + ( 0 + 3 ) ) = ; ; 1 2 8
67 6t5e30 
 |-  ( 6 x. 5 ) = ; 3 0
68 15 25 15 67 56 decaddi 
 |-  ( ( 6 x. 5 ) + 3 ) = ; 3 3
69 9 10 25 15 12 55 8 15 15 66 68 decmac 
 |-  ( ( ; ; 2 5 6 x. 5 ) + 3 ) = ; ; ; 1 2 8 3
70 1 8 14 15 17 18 11 15 20 54 69 decma2c 
 |-  ( ( ; ; 2 5 6 x. ; 2 5 ) + ; ; 1 5 3 ) = ; ; ; 6 5 5 3
71 6cn 
 |-  6 e. CC
72 71 4 49 mulcomli 
 |-  ( 2 x. 6 ) = ; 1 2
73 13 1 15 72 52 decaddi 
 |-  ( ( 2 x. 6 ) + 3 ) = ; 1 5
74 71 33 67 mulcomli 
 |-  ( 5 x. 6 ) = ; 3 0
75 15 25 15 74 56 decaddi 
 |-  ( ( 5 x. 6 ) + 3 ) = ; 3 3
76 1 8 15 17 10 15 15 73 75 decrmac 
 |-  ( ( ; 2 5 x. 6 ) + 3 ) = ; ; 1 5 3
77 6t6e36 
 |-  ( 6 x. 6 ) = ; 3 6
78 10 9 10 12 10 15 76 77 decmul1c 
 |-  ( ; ; 2 5 6 x. 6 ) = ; ; ; 1 5 3 6
79 11 9 10 12 10 16 70 78 decmul2c 
 |-  ( ; ; 2 5 6 x. ; ; 2 5 6 ) = ; ; ; ; 6 5 5 3 6
80 1 2 6 7 79 numexp2x 
 |-  ( 2 ^ ; 1 6 ) = ; ; ; ; 6 5 5 3 6