Proof of Theorem 631prm
Step | Hyp | Ref
| Expression |
1 | | 6nn0 11313 |
. . . 4
|
2 | | 3nn0 11310 |
. . . 4
|
3 | 1, 2 | deccl 11512 |
. . 3
; |
4 | | 1nn 11031 |
. . 3
|
5 | 3, 4 | decnncl 11518 |
. 2
;; |
6 | | 8nn0 11315 |
. . 3
|
7 | | 4nn0 11311 |
. . 3
|
8 | | 1nn0 11308 |
. . 3
|
9 | | 6lt8 11216 |
. . 3
|
10 | | 3lt10 11679 |
. . 3
; |
11 | | 1lt10 11681 |
. . 3
; |
12 | 1, 6, 2, 7, 8, 8, 9, 10, 11 | 3decltc 11538 |
. 2
;; ;; |
13 | | 3nn 11186 |
. . . 4
|
14 | 1, 13 | decnncl 11518 |
. . 3
; |
15 | 14, 8, 8, 11 | declti 11546 |
. 2
;; |
16 | | 0nn0 11307 |
. . 3
|
17 | | 2cn 11091 |
. . . 4
|
18 | 17 | mul02i 10225 |
. . 3
|
19 | | 1e0p1 11552 |
. . 3
|
20 | 3, 16, 18, 19 | dec2dvds 15767 |
. 2
;; |
21 | | 2nn0 11309 |
. . . . 5
|
22 | 21, 8 | deccl 11512 |
. . . 4
; |
23 | 22, 16 | deccl 11512 |
. . 3
;; |
24 | | eqid 2622 |
. . . 4
;; ;; |
25 | 8 | dec0h 11522 |
. . . 4
; |
26 | | eqid 2622 |
. . . . 5
; ; |
27 | | 00id 10211 |
. . . . . 6
|
28 | 16 | dec0h 11522 |
. . . . . 6
; |
29 | 27, 28 | eqtri 2644 |
. . . . 5
; |
30 | | 3t2e6 11179 |
. . . . . . 7
|
31 | 30, 27 | oveq12i 6662 |
. . . . . 6
|
32 | | 6cn 11102 |
. . . . . . 7
|
33 | 32 | addid1i 10223 |
. . . . . 6
|
34 | 31, 33 | eqtri 2644 |
. . . . 5
|
35 | | 3t1e3 11178 |
. . . . . . 7
|
36 | 35 | oveq1i 6660 |
. . . . . 6
|
37 | | 3cn 11095 |
. . . . . . 7
|
38 | 37 | addid1i 10223 |
. . . . . 6
|
39 | 2 | dec0h 11522 |
. . . . . 6
; |
40 | 36, 38, 39 | 3eqtri 2648 |
. . . . 5
; |
41 | 21, 8, 16, 16, 26, 29, 2, 2, 16, 34, 40 | decma2c 11568 |
. . . 4
; ; |
42 | 37 | mul01i 10226 |
. . . . . 6
|
43 | 42 | oveq1i 6660 |
. . . . 5
|
44 | | 0p1e1 11132 |
. . . . 5
|
45 | 43, 44, 25 | 3eqtri 2648 |
. . . 4
; |
46 | 22, 16, 16, 8, 24, 25, 2, 8, 16, 41, 45 | decma2c 11568 |
. . 3
;; ;; |
47 | | 1lt3 11196 |
. . 3
|
48 | 13, 23, 4, 46, 47 | ndvdsi 15136 |
. 2
;; |
49 | | 1lt5 11203 |
. . 3
|
50 | 3, 4, 49 | dec5dvds 15768 |
. 2
;; |
51 | | 7nn 11190 |
. . 3
|
52 | | 9nn0 11316 |
. . . 4
|
53 | 52, 16 | deccl 11512 |
. . 3
; |
54 | | eqid 2622 |
. . . 4
; ; |
55 | | 7nn0 11314 |
. . . 4
|
56 | 27 | oveq2i 6661 |
. . . . 5
|
57 | | 9cn 11108 |
. . . . . . 7
|
58 | | 7cn 11104 |
. . . . . . 7
|
59 | | 9t7e63 11668 |
. . . . . . 7
; |
60 | 57, 58, 59 | mulcomli 10047 |
. . . . . 6
; |
61 | 60 | oveq1i 6660 |
. . . . 5
; |
62 | 3 | nn0cni 11304 |
. . . . . 6
; |
63 | 62 | addid1i 10223 |
. . . . 5
; ; |
64 | 56, 61, 63 | 3eqtri 2648 |
. . . 4
; |
65 | 58 | mul01i 10226 |
. . . . . 6
|
66 | 65 | oveq1i 6660 |
. . . . 5
|
67 | 66, 44, 25 | 3eqtri 2648 |
. . . 4
; |
68 | 52, 16, 16, 8, 54, 25, 55, 8, 16, 64, 67 | decma2c 11568 |
. . 3
; ;; |
69 | | 1lt7 11214 |
. . 3
|
70 | 51, 53, 4, 68, 69 | ndvdsi 15136 |
. 2
;; |
71 | 8, 4 | decnncl 11518 |
. . 3
; |
72 | | 5nn0 11312 |
. . . 4
|
73 | 72, 55 | deccl 11512 |
. . 3
; |
74 | | 4nn 11187 |
. . 3
|
75 | | eqid 2622 |
. . . 4
; ; |
76 | 7 | dec0h 11522 |
. . . 4
; |
77 | 8, 8 | deccl 11512 |
. . . 4
; |
78 | | eqid 2622 |
. . . . 5
; ; |
79 | | 8cn 11106 |
. . . . . . 7
|
80 | 79 | addid2i 10224 |
. . . . . 6
|
81 | 6 | dec0h 11522 |
. . . . . 6
; |
82 | 80, 81 | eqtri 2644 |
. . . . 5
; |
83 | | 5cn 11100 |
. . . . . . . 8
|
84 | 83 | mulid2i 10043 |
. . . . . . 7
|
85 | 84, 44 | oveq12i 6662 |
. . . . . 6
|
86 | | 5p1e6 11155 |
. . . . . 6
|
87 | 85, 86 | eqtri 2644 |
. . . . 5
|
88 | 84 | oveq1i 6660 |
. . . . . 6
|
89 | | 8p5e13 11615 |
. . . . . . 7
; |
90 | 79, 83, 89 | addcomli 10228 |
. . . . . 6
; |
91 | 88, 90 | eqtri 2644 |
. . . . 5
; |
92 | 8, 8, 16, 6, 78, 82, 72, 2, 8, 87, 91 | decmac 11566 |
. . . 4
; ; |
93 | 58 | mulid2i 10043 |
. . . . . . 7
|
94 | 93, 44 | oveq12i 6662 |
. . . . . 6
|
95 | | 7p1e8 11157 |
. . . . . 6
|
96 | 94, 95 | eqtri 2644 |
. . . . 5
|
97 | 93 | oveq1i 6660 |
. . . . . 6
|
98 | | 7p4e11 11605 |
. . . . . 6
; |
99 | 97, 98 | eqtri 2644 |
. . . . 5
; |
100 | 8, 8, 16, 7, 78, 76, 55, 8, 8, 96, 99 | decmac 11566 |
. . . 4
; ; |
101 | 72, 55, 16, 7, 75, 76, 77, 8, 6, 92, 100 | decma2c 11568 |
. . 3
; ; ;; |
102 | | 4lt10 11678 |
. . . 4
; |
103 | 4, 8, 7, 102 | declti 11546 |
. . 3
; |
104 | 71, 73, 74, 101, 103 | ndvdsi 15136 |
. 2
; ;; |
105 | 8, 13 | decnncl 11518 |
. . 3
; |
106 | 7, 6 | deccl 11512 |
. . 3
; |
107 | | eqid 2622 |
. . . 4
; ; |
108 | 55 | dec0h 11522 |
. . . 4
; |
109 | 8, 2 | deccl 11512 |
. . . 4
; |
110 | | eqid 2622 |
. . . . 5
; ; |
111 | 77 | nn0cni 11304 |
. . . . . 6
; |
112 | 111 | addid2i 10224 |
. . . . 5
; ; |
113 | | 4cn 11098 |
. . . . . . . 8
|
114 | 113 | mulid2i 10043 |
. . . . . . 7
|
115 | | 1p1e2 11134 |
. . . . . . 7
|
116 | 114, 115 | oveq12i 6662 |
. . . . . 6
|
117 | | 4p2e6 11162 |
. . . . . 6
|
118 | 116, 117 | eqtri 2644 |
. . . . 5
|
119 | | 4t3e12 11632 |
. . . . . . 7
; |
120 | 113, 37, 119 | mulcomli 10047 |
. . . . . 6
; |
121 | | 2p1e3 11151 |
. . . . . 6
|
122 | 8, 21, 8, 120, 121 | decaddi 11579 |
. . . . 5
; |
123 | 8, 2, 8, 8, 110, 112, 7, 2, 8, 118, 122 | decmac 11566 |
. . . 4
; ; ; |
124 | 79 | mulid2i 10043 |
. . . . . . 7
|
125 | 37 | addid2i 10224 |
. . . . . . 7
|
126 | 124, 125 | oveq12i 6662 |
. . . . . 6
|
127 | | 8p3e11 11612 |
. . . . . 6
; |
128 | 126, 127 | eqtri 2644 |
. . . . 5
; |
129 | | 8t3e24 11655 |
. . . . . . 7
; |
130 | 79, 37, 129 | mulcomli 10047 |
. . . . . 6
; |
131 | 58, 113, 98 | addcomli 10228 |
. . . . . 6
; |
132 | 21, 7, 55, 130, 121, 8, 131 | decaddci 11580 |
. . . . 5
; |
133 | 8, 2, 16, 55, 110, 108, 6, 8, 2, 128, 132 | decmac 11566 |
. . . 4
; ;; |
134 | 7, 6, 16, 55, 107, 108, 109, 8, 77, 123, 133 | decma2c 11568 |
. . 3
; ; ;; |
135 | | 7lt10 11675 |
. . . 4
; |
136 | 4, 2, 55, 135 | declti 11546 |
. . 3
; |
137 | 105, 106,
51, 134, 136 | ndvdsi 15136 |
. 2
; ;; |
138 | 8, 51 | decnncl 11518 |
. . 3
; |
139 | 2, 55 | deccl 11512 |
. . 3
; |
140 | | 2nn 11185 |
. . 3
|
141 | | eqid 2622 |
. . . 4
; ; |
142 | 21 | dec0h 11522 |
. . . 4
; |
143 | 8, 55 | deccl 11512 |
. . . 4
; |
144 | 8, 21 | deccl 11512 |
. . . 4
; |
145 | | eqid 2622 |
. . . . 5
; ; |
146 | 144 | nn0cni 11304 |
. . . . . 6
; |
147 | 146 | addid2i 10224 |
. . . . 5
; ; |
148 | 37 | mulid2i 10043 |
. . . . . . 7
|
149 | | 1p2e3 11152 |
. . . . . . 7
|
150 | 148, 149 | oveq12i 6662 |
. . . . . 6
|
151 | | 3p3e6 11161 |
. . . . . 6
|
152 | 150, 151 | eqtri 2644 |
. . . . 5
|
153 | | 7t3e21 11649 |
. . . . . 6
; |
154 | 21, 8, 21, 153, 149 | decaddi 11579 |
. . . . 5
; |
155 | 8, 55, 8, 21, 145, 147, 2, 2, 21, 152, 154 | decmac 11566 |
. . . 4
; ; ; |
156 | 83 | addid2i 10224 |
. . . . . . 7
|
157 | 93, 156 | oveq12i 6662 |
. . . . . 6
|
158 | | 7p5e12 11607 |
. . . . . 6
; |
159 | 157, 158 | eqtri 2644 |
. . . . 5
; |
160 | | 7t7e49 11653 |
. . . . . 6
; |
161 | | 4p1e5 11154 |
. . . . . 6
|
162 | | 9p2e11 11619 |
. . . . . 6
; |
163 | 7, 52, 21, 160, 161, 8, 162 | decaddci 11580 |
. . . . 5
; |
164 | 8, 55, 16, 21, 145, 142, 55, 8, 72, 159, 163 | decmac 11566 |
. . . 4
; ;; |
165 | 2, 55, 16, 21, 141, 142, 143, 8, 144, 155, 164 | decma2c 11568 |
. . 3
; ; ;; |
166 | | 2lt10 11680 |
. . . 4
; |
167 | 4, 55, 21, 166 | declti 11546 |
. . 3
; |
168 | 138, 139,
140, 165, 167 | ndvdsi 15136 |
. 2
; ;; |
169 | | 9nn 11192 |
. . . 4
|
170 | 8, 169 | decnncl 11518 |
. . 3
; |
171 | 2, 2 | deccl 11512 |
. . 3
; |
172 | | eqid 2622 |
. . . 4
; ; |
173 | 8, 52 | deccl 11512 |
. . . 4
; |
174 | | eqid 2622 |
. . . . 5
; ; |
175 | 32 | addid2i 10224 |
. . . . . 6
|
176 | 1 | dec0h 11522 |
. . . . . 6
; |
177 | 175, 176 | eqtri 2644 |
. . . . 5
; |
178 | 148, 125 | oveq12i 6662 |
. . . . . 6
|
179 | 178, 151 | eqtri 2644 |
. . . . 5
|
180 | | 9t3e27 11664 |
. . . . . 6
; |
181 | | 7p6e13 11608 |
. . . . . 6
; |
182 | 21, 55, 1, 180, 121, 2, 181 | decaddci 11580 |
. . . . 5
; |
183 | 8, 52, 16, 1, 174, 177, 2, 2, 2, 179, 182 | decmac 11566 |
. . . 4
; ; |
184 | 21, 55, 7, 180, 121, 8, 98 | decaddci 11580 |
. . . . 5
; |
185 | 8, 52, 16, 7, 174, 76, 2, 8, 2,
179, 184 | decmac 11566 |
. . . 4
; ; |
186 | 2, 2, 16, 7, 172, 76, 173, 8, 1, 183, 185 | decma2c 11568 |
. . 3
; ; ;; |
187 | 4, 52, 7, 102 | declti 11546 |
. . 3
; |
188 | 170, 171,
74, 186, 187 | ndvdsi 15136 |
. 2
; ;; |
189 | 21, 13 | decnncl 11518 |
. . 3
; |
190 | 21, 55 | deccl 11512 |
. . 3
; |
191 | | 10nn 11514 |
. . 3
; |
192 | | eqid 2622 |
. . . 4
; ; |
193 | | eqid 2622 |
. . . 4
; ; |
194 | 21, 2 | deccl 11512 |
. . . 4
; |
195 | 8, 1 | deccl 11512 |
. . . 4
; |
196 | | eqid 2622 |
. . . . 5
; ; |
197 | | eqid 2622 |
. . . . . 6
; ; |
198 | | ax-1cn 9994 |
. . . . . . 7
|
199 | | 6p1e7 11156 |
. . . . . . 7
|
200 | 32, 198, 199 | addcomli 10228 |
. . . . . 6
|
201 | 16, 8, 8, 1, 25, 197, 44, 200 | decadd 11570 |
. . . . 5
; ; |
202 | | 2t2e4 11177 |
. . . . . . 7
|
203 | 202, 115 | oveq12i 6662 |
. . . . . 6
|
204 | 203, 117 | eqtri 2644 |
. . . . 5
|
205 | 30 | oveq1i 6660 |
. . . . . 6
|
206 | 58, 32, 181 | addcomli 10228 |
. . . . . 6
; |
207 | 205, 206 | eqtri 2644 |
. . . . 5
; |
208 | 21, 2, 8, 55, 196, 201, 21, 2, 8, 204, 207 | decmac 11566 |
. . . 4
; ; ; |
209 | | 7t2e14 11648 |
. . . . . . . . 9
; |
210 | 58, 17, 209 | mulcomli 10047 |
. . . . . . . 8
; |
211 | 8, 7, 21, 210, 117 | decaddi 11579 |
. . . . . . 7
; |
212 | 58, 37, 153 | mulcomli 10047 |
. . . . . . 7
; |
213 | 55, 21, 2, 196, 8, 21, 211, 212 | decmul1c 11587 |
. . . . . 6
; ;; |
214 | 213 | oveq1i 6660 |
. . . . 5
; ;; |
215 | 195, 8 | deccl 11512 |
. . . . . . 7
;; |
216 | 215 | nn0cni 11304 |
. . . . . 6
;; |
217 | 216 | addid1i 10223 |
. . . . 5
;; ;; |
218 | 214, 217 | eqtri 2644 |
. . . 4
; ;; |
219 | 21, 55, 8, 16, 192, 193, 194, 8, 195, 208, 218 | decma2c 11568 |
. . 3
; ; ; ;; |
220 | | 10pos 11515 |
. . . 4
; |
221 | | 1lt2 11194 |
. . . 4
|
222 | 8, 21, 16, 2, 220, 221 | decltc 11532 |
. . 3
; ; |
223 | 189, 190,
191, 219, 222 | ndvdsi 15136 |
. 2
; ;; |
224 | 5, 12, 15, 20, 48, 50, 70, 104, 137, 168, 188, 223 | prmlem2 15827 |
1
;; |