Proof of Theorem 1259lem1
Step | Hyp | Ref
| Expression |
1 | | 1259prm.1 |
. . 3
;;; |
2 | | 1nn0 11308 |
. . . . . 6
|
3 | | 2nn0 11309 |
. . . . . 6
|
4 | 2, 3 | deccl 11512 |
. . . . 5
; |
5 | | 5nn0 11312 |
. . . . 5
|
6 | 4, 5 | deccl 11512 |
. . . 4
;; |
7 | | 9nn 11192 |
. . . 4
|
8 | 6, 7 | decnncl 11518 |
. . 3
;;; |
9 | 1, 8 | eqeltri 2697 |
. 2
|
10 | | 2nn 11185 |
. 2
|
11 | | 6nn0 11313 |
. . 3
|
12 | 2, 11 | deccl 11512 |
. 2
; |
13 | | 0z 11388 |
. 2
|
14 | | 8nn0 11315 |
. . 3
|
15 | 11, 14 | deccl 11512 |
. 2
; |
16 | | 3nn0 11310 |
. . . 4
|
17 | 2, 16 | deccl 11512 |
. . 3
; |
18 | 17, 11 | deccl 11512 |
. 2
;; |
19 | 5, 3 | deccl 11512 |
. . . 4
; |
20 | 19 | nn0zi 11402 |
. . 3
; |
21 | 3, 14 | nn0expcli 12886 |
. . 3
|
22 | | eqid 2622 |
. . 3
|
23 | 14 | nn0cni 11304 |
. . . 4
|
24 | | 2cn 11091 |
. . . 4
|
25 | | 8t2e16 11654 |
. . . 4
; |
26 | 23, 24, 25 | mulcomli 10047 |
. . 3
; |
27 | | 9nn0 11316 |
. . . . 5
|
28 | | eqid 2622 |
. . . . 5
; ; |
29 | | 4nn0 11311 |
. . . . . 6
|
30 | | 7nn0 11314 |
. . . . . 6
|
31 | 29, 30 | deccl 11512 |
. . . . 5
; |
32 | | eqid 2622 |
. . . . . 6
;; ;; |
33 | | 0nn0 11307 |
. . . . . . 7
|
34 | 11 | dec0h 11522 |
. . . . . . 7
; |
35 | | eqid 2622 |
. . . . . . 7
; ; |
36 | | 4cn 11098 |
. . . . . . . . . 10
|
37 | 36 | addid2i 10224 |
. . . . . . . . 9
|
38 | 37 | oveq1i 6660 |
. . . . . . . 8
|
39 | | 4p1e5 11154 |
. . . . . . . 8
|
40 | 38, 39 | eqtri 2644 |
. . . . . . 7
|
41 | | 7cn 11104 |
. . . . . . . 8
|
42 | | 6cn 11102 |
. . . . . . . 8
|
43 | | 7p6e13 11608 |
. . . . . . . 8
; |
44 | 41, 42, 43 | addcomli 10228 |
. . . . . . 7
; |
45 | 33, 11, 29, 30, 34, 35, 40, 16, 44 | decaddc 11572 |
. . . . . 6
; ; |
46 | 3, 11 | deccl 11512 |
. . . . . 6
; |
47 | | eqid 2622 |
. . . . . . 7
; ; |
48 | 5 | dec0h 11522 |
. . . . . . . 8
; |
49 | | eqid 2622 |
. . . . . . . 8
; ; |
50 | 24 | addid2i 10224 |
. . . . . . . . . 10
|
51 | 50 | oveq1i 6660 |
. . . . . . . . 9
|
52 | | 2p1e3 11151 |
. . . . . . . . 9
|
53 | 51, 52 | eqtri 2644 |
. . . . . . . 8
|
54 | | 5cn 11100 |
. . . . . . . . 9
|
55 | | 6p5e11 11600 |
. . . . . . . . 9
; |
56 | 42, 54, 55 | addcomli 10228 |
. . . . . . . 8
; |
57 | 33, 5, 3, 11, 48, 49, 53, 2, 56 | decaddc 11572 |
. . . . . . 7
; ; |
58 | | 10nn0 11516 |
. . . . . . 7
; |
59 | | eqid 2622 |
. . . . . . . 8
; ; |
60 | 58 | nn0cni 11304 |
. . . . . . . . 9
; |
61 | | 3cn 11095 |
. . . . . . . . 9
|
62 | | dec10p 11553 |
. . . . . . . . 9
; ; |
63 | 60, 61, 62 | addcomli 10228 |
. . . . . . . 8
; ; |
64 | 54 | mulid1i 10042 |
. . . . . . . . . 10
|
65 | | 1p0e1 11133 |
. . . . . . . . . 10
|
66 | 64, 65 | oveq12i 6662 |
. . . . . . . . 9
|
67 | | 5p1e6 11155 |
. . . . . . . . 9
|
68 | 66, 67 | eqtri 2644 |
. . . . . . . 8
|
69 | 24 | mulid1i 10042 |
. . . . . . . . . 10
|
70 | 69 | oveq1i 6660 |
. . . . . . . . 9
|
71 | | 3p2e5 11160 |
. . . . . . . . . 10
|
72 | 61, 24, 71 | addcomli 10228 |
. . . . . . . . 9
|
73 | 70, 72, 48 | 3eqtri 2648 |
. . . . . . . 8
; |
74 | 5, 3, 2, 16, 59, 63, 2, 5, 33, 68, 73 | decmac 11566 |
. . . . . . 7
; ; ; |
75 | 2 | dec0h 11522 |
. . . . . . . 8
; |
76 | | 5t2e10 11634 |
. . . . . . . . . 10
; |
77 | | 00id 10211 |
. . . . . . . . . 10
|
78 | 76, 77 | oveq12i 6662 |
. . . . . . . . 9
; |
79 | | dec10p 11553 |
. . . . . . . . 9
; ; |
80 | 78, 79 | eqtri 2644 |
. . . . . . . 8
; |
81 | | 2t2e4 11177 |
. . . . . . . . . 10
|
82 | 81 | oveq1i 6660 |
. . . . . . . . 9
|
83 | 82, 39, 48 | 3eqtri 2648 |
. . . . . . . 8
; |
84 | 5, 3, 33, 2, 59, 75, 3, 5, 33, 80, 83 | decmac 11566 |
. . . . . . 7
; ;; |
85 | 2, 3, 16, 2, 47, 57, 19, 5, 58, 74, 84 | decma2c 11568 |
. . . . . 6
; ; ; ;; |
86 | | 5t5e25 11639 |
. . . . . . . 8
; |
87 | 3, 5, 67, 86 | decsuc 11535 |
. . . . . . 7
; |
88 | 54, 24, 76 | mulcomli 10047 |
. . . . . . . 8
; |
89 | 61 | addid2i 10224 |
. . . . . . . 8
|
90 | 2, 33, 16, 88, 89 | decaddi 11579 |
. . . . . . 7
; |
91 | 5, 3, 16, 59, 5, 16, 2, 87, 90 | decrmac 11577 |
. . . . . 6
; ;; |
92 | 4, 5, 5, 16, 32, 45, 19, 16, 46, 85, 91 | decma2c 11568 |
. . . . 5
; ;; ; ;;; |
93 | | 9cn 11108 |
. . . . . . . 8
|
94 | | 9t5e45 11666 |
. . . . . . . 8
; |
95 | 93, 54, 94 | mulcomli 10047 |
. . . . . . 7
; |
96 | | 5p2e7 11165 |
. . . . . . 7
|
97 | 29, 5, 3, 95, 96 | decaddi 11579 |
. . . . . 6
; |
98 | | 9t2e18 11663 |
. . . . . . . 8
; |
99 | 93, 24, 98 | mulcomli 10047 |
. . . . . . 7
; |
100 | | 1p1e2 11134 |
. . . . . . 7
|
101 | | 8p8e16 11618 |
. . . . . . 7
; |
102 | 2, 14, 14, 99, 100, 11, 101 | decaddci 11580 |
. . . . . 6
; |
103 | 5, 3, 14, 59, 27, 11, 3, 97, 102 | decrmac 11577 |
. . . . 5
; ;; |
104 | 6, 27, 11, 14, 1, 28, 19, 11, 31, 92, 103 | decma2c 11568 |
. . . 4
; ; ;;;; |
105 | | 2exp16 15797 |
. . . 4
; ;;;; |
106 | | eqid 2622 |
. . . . 5
|
107 | | eqid 2622 |
. . . . 5
|
108 | 3, 14, 26, 106, 107 | numexp2x 15783 |
. . . 4
; |
109 | 104, 105,
108 | 3eqtr2i 2650 |
. . 3
; ; |
110 | 9, 10, 14, 20, 21, 15, 22, 26, 109 | mod2xi 15773 |
. 2
; ;
|
111 | | 6p1e7 11156 |
. . 3
|
112 | | eqid 2622 |
. . 3
; ; |
113 | 2, 11, 111, 112 | decsuc 11535 |
. 2
; ; |
114 | 18 | nn0cni 11304 |
. . . 4
;; |
115 | 114 | addid2i 10224 |
. . 3
;; ;; |
116 | 9 | nncni 11030 |
. . . . 5
|
117 | 116 | mul02i 10225 |
. . . 4
|
118 | 117 | oveq1i 6660 |
. . 3
;; ;; |
119 | | 6t2e12 11641 |
. . . . 5
; |
120 | 2, 3, 52, 119 | decsuc 11535 |
. . . 4
; |
121 | 3, 11, 14, 28, 11, 2, 120, 25 | decmul1c 11587 |
. . 3
; ;; |
122 | 115, 118,
121 | 3eqtr4i 2654 |
. 2
;; ; |
123 | 9, 10, 12, 13, 15, 18, 110, 113, 122 | modxp1i 15774 |
1
; ;; |