Proof of Theorem 2exp16
Step | Hyp | Ref
| Expression |
1 | | 2nn0 11309 |
. 2
|
2 | | 8nn0 11315 |
. 2
|
3 | | 8cn 11106 |
. . 3
|
4 | | 2cn 11091 |
. . 3
|
5 | | 8t2e16 11654 |
. . 3
; |
6 | 3, 4, 5 | mulcomli 10047 |
. 2
; |
7 | | 2exp8 15796 |
. 2
;; |
8 | | 5nn0 11312 |
. . . . 5
|
9 | 1, 8 | deccl 11512 |
. . . 4
; |
10 | | 6nn0 11313 |
. . . 4
|
11 | 9, 10 | deccl 11512 |
. . 3
;; |
12 | | eqid 2622 |
. . 3
;; ;; |
13 | | 1nn0 11308 |
. . . . 5
|
14 | 13, 8 | deccl 11512 |
. . . 4
; |
15 | | 3nn0 11310 |
. . . 4
|
16 | 14, 15 | deccl 11512 |
. . 3
;; |
17 | | eqid 2622 |
. . . 4
; ; |
18 | | eqid 2622 |
. . . 4
;; ;; |
19 | 13, 1 | deccl 11512 |
. . . . 5
; |
20 | 19, 2 | deccl 11512 |
. . . 4
;; |
21 | | 4nn0 11311 |
. . . . . 6
|
22 | 13, 21 | deccl 11512 |
. . . . 5
; |
23 | | eqid 2622 |
. . . . . 6
; ; |
24 | | eqid 2622 |
. . . . . 6
;; ;; |
25 | | 0nn0 11307 |
. . . . . . . 8
|
26 | 13 | dec0h 11522 |
. . . . . . . 8
; |
27 | | eqid 2622 |
. . . . . . . 8
; ; |
28 | | 0p1e1 11132 |
. . . . . . . 8
|
29 | | 1p2e3 11152 |
. . . . . . . 8
|
30 | 25, 13, 13, 1, 26, 27, 28, 29 | decadd 11570 |
. . . . . . 7
; ; |
31 | | 3p1e4 11153 |
. . . . . . 7
|
32 | 13, 15, 13, 30, 31 | decaddi 11579 |
. . . . . 6
; ; |
33 | | 5cn 11100 |
. . . . . . 7
|
34 | | 8p5e13 11615 |
. . . . . . 7
; |
35 | 3, 33, 34 | addcomli 10228 |
. . . . . 6
; |
36 | 13, 8, 19, 2, 23, 24, 32, 15, 35 | decaddc 11572 |
. . . . 5
; ;; ;; |
37 | | eqid 2622 |
. . . . . . 7
; ; |
38 | | 4p1e5 11154 |
. . . . . . 7
|
39 | 13, 21, 13, 37, 38 | decaddi 11579 |
. . . . . 6
; ; |
40 | | 2t2e4 11177 |
. . . . . . . 8
|
41 | | 1p1e2 11134 |
. . . . . . . 8
|
42 | 40, 41 | oveq12i 6662 |
. . . . . . 7
|
43 | | 4p2e6 11162 |
. . . . . . 7
|
44 | 42, 43 | eqtri 2644 |
. . . . . 6
|
45 | | 5t2e10 11634 |
. . . . . . 7
; |
46 | 33 | addid2i 10224 |
. . . . . . 7
|
47 | 13, 25, 8, 45, 46 | decaddi 11579 |
. . . . . 6
; |
48 | 1, 8, 13, 8, 17, 39, 1, 8, 13, 44, 47 | decmac 11566 |
. . . . 5
; ; ; |
49 | | 6t2e12 11641 |
. . . . . 6
; |
50 | | 3cn 11095 |
. . . . . . 7
|
51 | | 3p2e5 11160 |
. . . . . . 7
|
52 | 50, 4, 51 | addcomli 10228 |
. . . . . 6
|
53 | 13, 1, 15, 49, 52 | decaddi 11579 |
. . . . 5
; |
54 | 9, 10, 22, 15, 12, 36, 1, 8, 13, 48, 53 | decmac 11566 |
. . . 4
;; ; ;; ;; |
55 | 15 | dec0h 11522 |
. . . . 5
; |
56 | 50 | addid2i 10224 |
. . . . . . 7
|
57 | 56, 55 | eqtri 2644 |
. . . . . 6
; |
58 | 4 | addid2i 10224 |
. . . . . . . 8
|
59 | 58 | oveq2i 6661 |
. . . . . . 7
|
60 | 33, 4, 45 | mulcomli 10047 |
. . . . . . . 8
; |
61 | 13, 25, 1, 60, 58 | decaddi 11579 |
. . . . . . 7
; |
62 | 59, 61 | eqtri 2644 |
. . . . . 6
; |
63 | | 5t5e25 11639 |
. . . . . . 7
; |
64 | | 5p3e8 11166 |
. . . . . . 7
|
65 | 1, 8, 15, 63, 64 | decaddi 11579 |
. . . . . 6
; |
66 | 1, 8, 25, 15, 17, 57, 8, 2, 1,
62, 65 | decmac 11566 |
. . . . 5
; ;; |
67 | | 6t5e30 11644 |
. . . . . 6
; |
68 | 15, 25, 15, 67, 56 | decaddi 11579 |
. . . . 5
; |
69 | 9, 10, 25, 15, 12, 55, 8, 15, 15, 66, 68 | decmac 11566 |
. . . 4
;; ;;; |
70 | 1, 8, 14, 15, 17, 18, 11, 15, 20, 54, 69 | decma2c 11568 |
. . 3
;; ; ;; ;;; |
71 | | 6cn 11102 |
. . . . . . 7
|
72 | 71, 4, 49 | mulcomli 10047 |
. . . . . 6
; |
73 | 13, 1, 15, 72, 52 | decaddi 11579 |
. . . . 5
; |
74 | 71, 33, 67 | mulcomli 10047 |
. . . . . 6
; |
75 | 15, 25, 15, 74, 56 | decaddi 11579 |
. . . . 5
; |
76 | 1, 8, 15, 17, 10, 15, 15, 73, 75 | decrmac 11577 |
. . . 4
; ;; |
77 | | 6t6e36 11646 |
. . . 4
; |
78 | 10, 9, 10, 12, 10, 15, 76, 77 | decmul1c 11587 |
. . 3
;; ;;; |
79 | 11, 9, 10, 12, 10, 16, 70, 78 | decmul2c 11589 |
. 2
;; ;; ;;;; |
80 | 1, 2, 6, 7, 79 | numexp2x 15783 |
1
; ;;;; |