Proof of Theorem 163prm
Step | Hyp | Ref
| Expression |
1 | | 1nn0 11308 |
. . . 4
|
2 | | 6nn0 11313 |
. . . 4
|
3 | 1, 2 | deccl 11512 |
. . 3
; |
4 | | 3nn 11186 |
. . 3
|
5 | 3, 4 | decnncl 11518 |
. 2
;; |
6 | | 8nn0 11315 |
. . 3
|
7 | | 4nn0 11311 |
. . 3
|
8 | | 3nn0 11310 |
. . 3
|
9 | | 1lt8 11221 |
. . 3
|
10 | | 6lt10 11676 |
. . 3
; |
11 | | 3lt10 11679 |
. . 3
; |
12 | 1, 6, 2, 7, 8, 1, 9, 10, 11 | 3decltc 11538 |
. 2
;; ;; |
13 | | 6nn 11189 |
. . . 4
|
14 | 1, 13 | decnncl 11518 |
. . 3
; |
15 | | 1lt10 11681 |
. . 3
; |
16 | 14, 8, 1, 15 | declti 11546 |
. 2
;; |
17 | | 2cn 11091 |
. . . 4
|
18 | 17 | mulid2i 10043 |
. . 3
|
19 | | df-3 11080 |
. . 3
|
20 | 3, 1, 18, 19 | dec2dvds 15767 |
. 2
;; |
21 | | 5nn0 11312 |
. . . 4
|
22 | 21, 7 | deccl 11512 |
. . 3
; |
23 | | 1nn 11031 |
. . 3
|
24 | | 0nn0 11307 |
. . . 4
|
25 | | eqid 2622 |
. . . 4
; ; |
26 | 1 | dec0h 11522 |
. . . 4
; |
27 | | ax-1cn 9994 |
. . . . . . 7
|
28 | 27 | addid2i 10224 |
. . . . . 6
|
29 | 28 | oveq2i 6661 |
. . . . 5
|
30 | | 5p1e6 11155 |
. . . . . 6
|
31 | | 5cn 11100 |
. . . . . . 7
|
32 | | 3cn 11095 |
. . . . . . 7
|
33 | | 5t3e15 11635 |
. . . . . . 7
; |
34 | 31, 32, 33 | mulcomli 10047 |
. . . . . 6
; |
35 | 1, 21, 30, 34 | decsuc 11535 |
. . . . 5
; |
36 | 29, 35 | eqtri 2644 |
. . . 4
; |
37 | | 2nn0 11309 |
. . . . 5
|
38 | | 2p1e3 11151 |
. . . . 5
|
39 | | 4cn 11098 |
. . . . . 6
|
40 | | 4t3e12 11632 |
. . . . . 6
; |
41 | 39, 32, 40 | mulcomli 10047 |
. . . . 5
; |
42 | 1, 37, 38, 41 | decsuc 11535 |
. . . 4
; |
43 | 21, 7, 24, 1, 25, 26, 8, 8, 1,
36, 42 | decma2c 11568 |
. . 3
; ;; |
44 | | 1lt3 11196 |
. . 3
|
45 | 4, 22, 23, 43, 44 | ndvdsi 15136 |
. 2
;; |
46 | | 3lt5 11201 |
. . 3
|
47 | 3, 4, 46 | dec5dvds 15768 |
. 2
;; |
48 | | 7nn 11190 |
. . 3
|
49 | 37, 8 | deccl 11512 |
. . 3
; |
50 | | 2nn 11185 |
. . 3
|
51 | | eqid 2622 |
. . . 4
; ; |
52 | 37 | dec0h 11522 |
. . . 4
; |
53 | | 7nn0 11314 |
. . . 4
|
54 | 17 | addid2i 10224 |
. . . . . 6
|
55 | 54 | oveq2i 6661 |
. . . . 5
|
56 | | 7t2e14 11648 |
. . . . . 6
; |
57 | | 4p2e6 11162 |
. . . . . 6
|
58 | 1, 7, 37, 56, 57 | decaddi 11579 |
. . . . 5
; |
59 | 55, 58 | eqtri 2644 |
. . . 4
; |
60 | | 7t3e21 11649 |
. . . . 5
; |
61 | | 1p2e3 11152 |
. . . . 5
|
62 | 37, 1, 37, 60, 61 | decaddi 11579 |
. . . 4
; |
63 | 37, 8, 24, 37, 51, 52, 53, 8, 37, 59, 62 | decma2c 11568 |
. . 3
; ;; |
64 | | 2lt7 11213 |
. . 3
|
65 | 48, 49, 50, 63, 64 | ndvdsi 15136 |
. 2
;; |
66 | 1, 23 | decnncl 11518 |
. . 3
; |
67 | 1, 7 | deccl 11512 |
. . 3
; |
68 | | 9nn 11192 |
. . 3
|
69 | | 9nn0 11316 |
. . . 4
|
70 | | eqid 2622 |
. . . 4
; ; |
71 | 69 | dec0h 11522 |
. . . 4
; |
72 | 1, 1 | deccl 11512 |
. . . 4
; |
73 | 31 | addid2i 10224 |
. . . . . 6
|
74 | 73 | oveq2i 6661 |
. . . . 5
; ; |
75 | 66 | nncni 11030 |
. . . . . . 7
; |
76 | 75 | mulid1i 10042 |
. . . . . 6
; ; |
77 | 31, 27, 30 | addcomli 10228 |
. . . . . 6
|
78 | 1, 1, 21, 76, 77 | decaddi 11579 |
. . . . 5
; ; |
79 | 74, 78 | eqtri 2644 |
. . . 4
; ; |
80 | | eqid 2622 |
. . . . 5
; ; |
81 | 39 | mulid2i 10043 |
. . . . . . 7
|
82 | 81, 28 | oveq12i 6662 |
. . . . . 6
|
83 | | 4p1e5 11154 |
. . . . . 6
|
84 | 82, 83 | eqtri 2644 |
. . . . 5
|
85 | 81 | oveq1i 6660 |
. . . . . 6
|
86 | | 9cn 11108 |
. . . . . . 7
|
87 | | 9p4e13 11622 |
. . . . . . 7
; |
88 | 86, 39, 87 | addcomli 10228 |
. . . . . 6
; |
89 | 85, 88 | eqtri 2644 |
. . . . 5
; |
90 | 1, 1, 24, 69, 80, 71, 7, 8, 1,
84, 89 | decmac 11566 |
. . . 4
; ; |
91 | 1, 7, 24, 69, 70, 71, 72, 8, 21, 79, 90 | decma2c 11568 |
. . 3
; ; ;; |
92 | | 9lt10 11673 |
. . . 4
; |
93 | 23, 1, 69, 92 | declti 11546 |
. . 3
; |
94 | 66, 67, 68, 91, 93 | ndvdsi 15136 |
. 2
; ;; |
95 | 1, 4 | decnncl 11518 |
. . 3
; |
96 | 1, 37 | deccl 11512 |
. . 3
; |
97 | | eqid 2622 |
. . . 4
; ; |
98 | 53 | dec0h 11522 |
. . . 4
; |
99 | 1, 8 | deccl 11512 |
. . . 4
; |
100 | | eqid 2622 |
. . . . 5
; ; |
101 | 32 | addid2i 10224 |
. . . . . 6
|
102 | 8 | dec0h 11522 |
. . . . . 6
; |
103 | 101, 102 | eqtri 2644 |
. . . . 5
; |
104 | 27 | mulid1i 10042 |
. . . . . . 7
|
105 | | 00id 10211 |
. . . . . . 7
|
106 | 104, 105 | oveq12i 6662 |
. . . . . 6
|
107 | 27 | addid1i 10223 |
. . . . . 6
|
108 | 106, 107 | eqtri 2644 |
. . . . 5
|
109 | 32 | mulid1i 10042 |
. . . . . . . 8
|
110 | 109 | oveq1i 6660 |
. . . . . . 7
|
111 | | 3p3e6 11161 |
. . . . . . 7
|
112 | 110, 111 | eqtri 2644 |
. . . . . 6
|
113 | 2 | dec0h 11522 |
. . . . . 6
; |
114 | 112, 113 | eqtri 2644 |
. . . . 5
; |
115 | 1, 8, 24, 8, 100, 103, 1, 2, 24, 108, 114 | decmac 11566 |
. . . 4
; ; |
116 | 18, 28 | oveq12i 6662 |
. . . . . 6
|
117 | 116, 38 | eqtri 2644 |
. . . . 5
|
118 | | 3t2e6 11179 |
. . . . . . 7
|
119 | 118 | oveq1i 6660 |
. . . . . 6
|
120 | | 7cn 11104 |
. . . . . . 7
|
121 | | 6cn 11102 |
. . . . . . 7
|
122 | | 7p6e13 11608 |
. . . . . . 7
; |
123 | 120, 121,
122 | addcomli 10228 |
. . . . . 6
; |
124 | 119, 123 | eqtri 2644 |
. . . . 5
; |
125 | 1, 8, 24, 53, 100, 98, 37, 8, 1, 117, 124 | decmac 11566 |
. . . 4
; ; |
126 | 1, 37, 24, 53, 97, 98, 99, 8, 8, 115, 125 | decma2c 11568 |
. . 3
; ; ;; |
127 | | 7lt10 11675 |
. . . 4
; |
128 | 23, 8, 53, 127 | declti 11546 |
. . 3
; |
129 | 95, 96, 48, 126, 128 | ndvdsi 15136 |
. 2
; ;; |
130 | 1, 48 | decnncl 11518 |
. . 3
; |
131 | | 10nn 11514 |
. . 3
; |
132 | | eqid 2622 |
. . . 4
; ; |
133 | | eqid 2622 |
. . . 4
; ; |
134 | 86 | mulid2i 10043 |
. . . . . 6
|
135 | | 6p1e7 11156 |
. . . . . . 7
|
136 | 121, 27, 135 | addcomli 10228 |
. . . . . 6
|
137 | 134, 136 | oveq12i 6662 |
. . . . 5
|
138 | | 9p7e16 11625 |
. . . . 5
; |
139 | 137, 138 | eqtri 2644 |
. . . 4
; |
140 | | 9t7e63 11668 |
. . . . . . 7
; |
141 | 86, 120, 140 | mulcomli 10047 |
. . . . . 6
; |
142 | 141 | oveq1i 6660 |
. . . . 5
; |
143 | 2, 8 | deccl 11512 |
. . . . . . 7
; |
144 | 143 | nn0cni 11304 |
. . . . . 6
; |
145 | 144 | addid1i 10223 |
. . . . 5
; ; |
146 | 142, 145 | eqtri 2644 |
. . . 4
; |
147 | 1, 53, 1, 24, 132, 133, 69, 8, 2, 139, 146 | decmac 11566 |
. . 3
; ; ;; |
148 | | 7pos 11120 |
. . . 4
|
149 | 1, 24, 48, 148 | declt 11530 |
. . 3
; ; |
150 | 130, 69, 131, 147, 149 | ndvdsi 15136 |
. 2
; ;; |
151 | 1, 68 | decnncl 11518 |
. . 3
; |
152 | | eqid 2622 |
. . . 4
; ; |
153 | | 8cn 11106 |
. . . . . . 7
|
154 | 153 | mulid2i 10043 |
. . . . . 6
|
155 | | 7p1e8 11157 |
. . . . . . 7
|
156 | 120, 27, 155 | addcomli 10228 |
. . . . . 6
|
157 | 154, 156 | oveq12i 6662 |
. . . . 5
|
158 | | 8p8e16 11618 |
. . . . 5
; |
159 | 157, 158 | eqtri 2644 |
. . . 4
; |
160 | | 9t8e72 11669 |
. . . . 5
; |
161 | 53, 37, 38, 160 | decsuc 11535 |
. . . 4
; |
162 | 1, 69, 1, 1, 152, 80, 6, 8, 53, 159, 161 | decmac 11566 |
. . 3
; ; ;; |
163 | | 1lt9 11229 |
. . . 4
|
164 | 1, 1, 68, 163 | declt 11530 |
. . 3
; ; |
165 | 151, 6, 66, 162, 164 | ndvdsi 15136 |
. 2
; ;; |
166 | 37, 4 | decnncl 11518 |
. . 3
; |
167 | 120, 17, 56 | mulcomli 10047 |
. . . . 5
; |
168 | 1, 7, 37, 167, 57 | decaddi 11579 |
. . . 4
; |
169 | 120, 32, 60 | mulcomli 10047 |
. . . . 5
; |
170 | 37, 1, 37, 169, 61 | decaddi 11579 |
. . . 4
; |
171 | 37, 8, 37, 51, 53, 8, 37, 168, 170 | decrmac 11577 |
. . 3
; ;; |
172 | | 2lt10 11680 |
. . . 4
; |
173 | 50, 8, 37, 172 | declti 11546 |
. . 3
; |
174 | 166, 53, 50, 171, 173 | ndvdsi 15136 |
. 2
; ;; |
175 | 5, 12, 16, 20, 45, 47, 65, 94, 129, 150, 165, 174 | prmlem2 15827 |
1
;; |