Proof of Theorem 631prm
Step | Hyp | Ref
| Expression |
1 | | 6nn0 10890 |
. . . 4
 |
2 | | 3nn0 10887 |
. . . 4
 |
3 | 1, 2 | deccl 11065 |
. . 3
;  |
4 | | 1nn 10620 |
. . 3
 |
5 | 3, 4 | decnncl 11064 |
. 2
;;   |
6 | | 8nn0 10892 |
. . . 4
 |
7 | | 4nn0 10888 |
. . . 4
 |
8 | 6, 7 | deccl 11065 |
. . 3
;  |
9 | | 1nn0 10885 |
. . 3
 |
10 | | 1lt10 10820 |
. . 3
 |
11 | | 3lt10 10818 |
. . . 4
 |
12 | | 6lt8 10798 |
. . . 4
 |
13 | 1, 6, 2, 7, 11, 12 | decltc 11073 |
. . 3
; ;  |
14 | 3, 8, 9, 9, 10, 13 | decltc 11073 |
. 2
;;  ;;   |
15 | | 3nn 10768 |
. . . 4
 |
16 | 1, 15 | decnncl 11064 |
. . 3
;  |
17 | 16, 9, 9, 10 | declti 11076 |
. 2
;;   |
18 | | 0nn0 10884 |
. . 3
 |
19 | | 2cn 10680 |
. . . 4
 |
20 | 19 | mul02i 9822 |
. . 3
   |
21 | | 1e0p1 11079 |
. . 3
   |
22 | 3, 18, 20, 21 | dec2dvds 15035 |
. 2
;;   |
23 | | 2nn0 10886 |
. . . . 5
 |
24 | 23, 9 | deccl 11065 |
. . . 4
;  |
25 | 24, 18 | deccl 11065 |
. . 3
;;   |
26 | | eqid 2451 |
. . . 4
;;  ;;   |
27 | 9 | dec0h 11067 |
. . . 4
;  |
28 | | eqid 2451 |
. . . . 5
; ;  |
29 | | 00id 9808 |
. . . . . 6
   |
30 | 18 | dec0h 11067 |
. . . . . 6
;  |
31 | 29, 30 | eqtri 2473 |
. . . . 5
  ;  |
32 | | 3t2e6 10761 |
. . . . . . 7
   |
33 | 32, 29 | oveq12i 6302 |
. . . . . 6
         |
34 | | 6cn 10691 |
. . . . . . 7
 |
35 | 34 | addid1i 9820 |
. . . . . 6
   |
36 | 33, 35 | eqtri 2473 |
. . . . 5
       |
37 | | 3t1e3 10760 |
. . . . . . 7
   |
38 | 37 | oveq1i 6300 |
. . . . . 6
       |
39 | | 3cn 10684 |
. . . . . . 7
 |
40 | 39 | addid1i 9820 |
. . . . . 6
   |
41 | 2 | dec0h 11067 |
. . . . . 6
;  |
42 | 38, 40, 41 | 3eqtri 2477 |
. . . . 5
    ;  |
43 | 23, 9, 18, 18, 28, 31, 2, 2, 18, 36, 42 | decma2c 11091 |
. . . 4
  ;     ;  |
44 | 39 | mul01i 9823 |
. . . . . 6
   |
45 | 44 | oveq1i 6300 |
. . . . 5
       |
46 | | 0p1e1 10721 |
. . . . 5
   |
47 | 45, 46, 27 | 3eqtri 2477 |
. . . 4
    ;  |
48 | 24, 18, 18, 9, 26, 27, 2, 9, 18, 43, 47 | decma2c 11091 |
. . 3
  ;;    ;;   |
49 | | 1lt3 10778 |
. . 3
 |
50 | 15, 25, 4, 48, 49 | ndvdsi 14391 |
. 2
;;   |
51 | | 1lt5 10785 |
. . 3
 |
52 | 3, 4, 51 | dec5dvds 15036 |
. 2
;;   |
53 | | 7nn 10772 |
. . 3
 |
54 | | 9nn0 10893 |
. . . 4
 |
55 | 54, 18 | deccl 11065 |
. . 3
;  |
56 | | eqid 2451 |
. . . 4
; ;  |
57 | | 7nn0 10891 |
. . . 4
 |
58 | 29 | oveq2i 6301 |
. . . . 5
           |
59 | | 9cn 10697 |
. . . . . . 7
 |
60 | | 7cn 10693 |
. . . . . . 7
 |
61 | | 9t7e63 11151 |
. . . . . . 7
  ;  |
62 | 59, 60, 61 | mulcomli 9650 |
. . . . . 6
  ;  |
63 | 62 | oveq1i 6300 |
. . . . 5
    ;   |
64 | 3 | nn0cni 10881 |
. . . . . 6
;  |
65 | 64 | addid1i 9820 |
. . . . 5
;  ;  |
66 | 58, 63, 65 | 3eqtri 2477 |
. . . 4
      ;  |
67 | 60 | mul01i 9823 |
. . . . . 6
   |
68 | 67 | oveq1i 6300 |
. . . . 5
       |
69 | 68, 46, 27 | 3eqtri 2477 |
. . . 4
    ;  |
70 | 54, 18, 18, 9, 56, 27, 57, 9, 18, 66, 69 | decma2c 11091 |
. . 3
  ;   ;;   |
71 | | 1lt7 10796 |
. . 3
 |
72 | 53, 55, 4, 70, 71 | ndvdsi 14391 |
. 2
;;   |
73 | 9, 4 | decnncl 11064 |
. . 3
;  |
74 | | 5nn0 10889 |
. . . 4
 |
75 | 74, 57 | deccl 11065 |
. . 3
;  |
76 | | 4nn 10769 |
. . 3
 |
77 | | eqid 2451 |
. . . 4
; ;  |
78 | 7 | dec0h 11067 |
. . . 4
;  |
79 | 9, 9 | deccl 11065 |
. . . 4
;  |
80 | | eqid 2451 |
. . . . 5
; ;  |
81 | | 8cn 10695 |
. . . . . . 7
 |
82 | 81 | addid2i 9821 |
. . . . . 6
   |
83 | 6 | dec0h 11067 |
. . . . . 6
;  |
84 | 82, 83 | eqtri 2473 |
. . . . 5
  ;  |
85 | | 5cn 10689 |
. . . . . . . 8
 |
86 | 85 | mulid2i 9646 |
. . . . . . 7
   |
87 | 86, 46 | oveq12i 6302 |
. . . . . 6
         |
88 | | 5p1e6 10737 |
. . . . . 6
   |
89 | 87, 88 | eqtri 2473 |
. . . . 5
       |
90 | 86 | oveq1i 6300 |
. . . . . 6
       |
91 | | 8p5e13 11109 |
. . . . . . 7
  ;  |
92 | 81, 85, 91 | addcomli 9825 |
. . . . . 6
  ;  |
93 | 90, 92 | eqtri 2473 |
. . . . 5
    ;  |
94 | 9, 9, 18, 6, 80, 84, 74, 2, 9, 89, 93 | decmac 11090 |
. . . 4
 ;     ;  |
95 | 60 | mulid2i 9646 |
. . . . . . 7
   |
96 | 95, 46 | oveq12i 6302 |
. . . . . 6
         |
97 | | 7p1e8 10739 |
. . . . . 6
   |
98 | 96, 97 | eqtri 2473 |
. . . . 5
       |
99 | 95 | oveq1i 6300 |
. . . . . 6
       |
100 | | 7p4e11 11103 |
. . . . . 6
  ;  |
101 | 99, 100 | eqtri 2473 |
. . . . 5
    ;  |
102 | 9, 9, 18, 7, 80, 78, 57, 9, 9, 98, 101 | decmac 11090 |
. . . 4
 ;   ;  |
103 | 74, 57, 18, 7, 77, 78, 79, 9, 6, 94, 102 | decma2c 11091 |
. . 3
 ; ;   ;;   |
104 | | 4lt10 10817 |
. . . 4
 |
105 | 4, 9, 7, 104 | declti 11076 |
. . 3
;  |
106 | 73, 75, 76, 103, 105 | ndvdsi 14391 |
. 2
; ;;   |
107 | 9, 15 | decnncl 11064 |
. . 3
;  |
108 | 7, 6 | deccl 11065 |
. . 3
;  |
109 | | eqid 2451 |
. . . 4
; ;  |
110 | 57 | dec0h 11067 |
. . . 4
;  |
111 | 9, 2 | deccl 11065 |
. . . 4
;  |
112 | | eqid 2451 |
. . . . 5
; ;  |
113 | 79 | nn0cni 10881 |
. . . . . 6
;  |
114 | 113 | addid2i 9821 |
. . . . 5
 ;  ;  |
115 | | 4cn 10687 |
. . . . . . . 8
 |
116 | 115 | mulid2i 9646 |
. . . . . . 7
   |
117 | | 1p1e2 10723 |
. . . . . . 7
   |
118 | 116, 117 | oveq12i 6302 |
. . . . . 6
         |
119 | | 4p2e6 10744 |
. . . . . 6
   |
120 | 118, 119 | eqtri 2473 |
. . . . 5
       |
121 | | 4t3e12 11123 |
. . . . . . 7
  ;  |
122 | 115, 39, 121 | mulcomli 9650 |
. . . . . 6
  ;  |
123 | | 2p1e3 10733 |
. . . . . 6
   |
124 | 9, 23, 9, 122, 123 | decaddi 11095 |
. . . . 5
    ;  |
125 | 9, 2, 9, 9, 112, 114, 7, 2, 9, 120, 124 | decmac 11090 |
. . . 4
 ;   ;   ;  |
126 | 81 | mulid2i 9646 |
. . . . . . 7
   |
127 | 39 | addid2i 9821 |
. . . . . . 7
   |
128 | 126, 127 | oveq12i 6302 |
. . . . . 6
         |
129 | | 8p3e11 11107 |
. . . . . 6
  ;  |
130 | 128, 129 | eqtri 2473 |
. . . . 5
      ;  |
131 | | 8t3e24 11140 |
. . . . . . 7
  ;  |
132 | 81, 39, 131 | mulcomli 9650 |
. . . . . 6
  ;  |
133 | 60, 115, 100 | addcomli 9825 |
. . . . . 6
  ;  |
134 | 23, 7, 57, 132, 123, 9, 133 | decaddci 11096 |
. . . . 5
    ;  |
135 | 9, 2, 18, 57, 112, 110, 6, 9, 2, 130, 134 | decmac 11090 |
. . . 4
 ;   ;;   |
136 | 7, 6, 18, 57, 109, 110, 111, 9, 79, 125, 135 | decma2c 11091 |
. . 3
 ; ;   ;;   |
137 | | 7lt10 10814 |
. . . 4
 |
138 | 4, 2, 57, 137 | declti 11076 |
. . 3
;  |
139 | 107, 108,
53, 136, 138 | ndvdsi 14391 |
. 2
; ;;   |
140 | 9, 53 | decnncl 11064 |
. . 3
;  |
141 | 2, 57 | deccl 11065 |
. . 3
;  |
142 | | 2nn 10767 |
. . 3
 |
143 | | eqid 2451 |
. . . 4
; ;  |
144 | 23 | dec0h 11067 |
. . . 4
;  |
145 | 9, 57 | deccl 11065 |
. . . 4
;  |
146 | 9, 23 | deccl 11065 |
. . . 4
;  |
147 | | eqid 2451 |
. . . . 5
; ;  |
148 | 146 | nn0cni 10881 |
. . . . . 6
;  |
149 | 148 | addid2i 9821 |
. . . . 5
 ;  ;  |
150 | 39 | mulid2i 9646 |
. . . . . . 7
   |
151 | | 1p2e3 10734 |
. . . . . . 7
   |
152 | 150, 151 | oveq12i 6302 |
. . . . . 6
         |
153 | | 3p3e6 10743 |
. . . . . 6
   |
154 | 152, 153 | eqtri 2473 |
. . . . 5
       |
155 | | 7t3e21 11134 |
. . . . . 6
  ;  |
156 | 23, 9, 23, 155, 151 | decaddi 11095 |
. . . . 5
    ;  |
157 | 9, 57, 9, 23, 147, 149, 2, 2, 23, 154, 156 | decmac 11090 |
. . . 4
 ;   ;   ;  |
158 | 85 | addid2i 9821 |
. . . . . . 7
   |
159 | 95, 158 | oveq12i 6302 |
. . . . . 6
         |
160 | | 7p5e12 11104 |
. . . . . 6
  ;  |
161 | 159, 160 | eqtri 2473 |
. . . . 5
      ;  |
162 | | 7t7e49 11138 |
. . . . . 6
  ;  |
163 | | 4p1e5 10736 |
. . . . . 6
   |
164 | | 9p2e11 11113 |
. . . . . 6
  ;  |
165 | 7, 54, 23, 162, 163, 9, 164 | decaddci 11096 |
. . . . 5
    ;  |
166 | 9, 57, 18, 23, 147, 144, 57, 9, 74, 161, 165 | decmac 11090 |
. . . 4
 ;   ;;   |
167 | 2, 57, 18, 23, 143, 144, 145, 9, 146, 157, 166 | decma2c 11091 |
. . 3
 ; ;   ;;   |
168 | | 2lt10 10819 |
. . . 4
 |
169 | 4, 57, 23, 168 | declti 11076 |
. . 3
;  |
170 | 140, 141,
142, 167, 169 | ndvdsi 14391 |
. 2
; ;;   |
171 | | 9nn 10774 |
. . . 4
 |
172 | 9, 171 | decnncl 11064 |
. . 3
;  |
173 | 2, 2 | deccl 11065 |
. . 3
;  |
174 | | eqid 2451 |
. . . 4
; ;  |
175 | 9, 54 | deccl 11065 |
. . . 4
;  |
176 | | eqid 2451 |
. . . . 5
; ;  |
177 | 34 | addid2i 9821 |
. . . . . 6
   |
178 | 1 | dec0h 11067 |
. . . . . 6
;  |
179 | 177, 178 | eqtri 2473 |
. . . . 5
  ;  |
180 | 150, 127 | oveq12i 6302 |
. . . . . 6
         |
181 | 180, 153 | eqtri 2473 |
. . . . 5
       |
182 | | 9t3e27 11147 |
. . . . . 6
  ;  |
183 | | 7p6e13 11105 |
. . . . . 6
  ;  |
184 | 23, 57, 1, 182, 123, 2, 183 | decaddci 11096 |
. . . . 5
    ;  |
185 | 9, 54, 18, 1, 176, 179, 2, 2, 2, 181, 184 | decmac 11090 |
. . . 4
 ;     ;  |
186 | 23, 57, 7, 182, 123, 9, 100 | decaddci 11096 |
. . . . 5
    ;  |
187 | 9, 54, 18, 7, 176, 78, 2, 9, 2,
181, 186 | decmac 11090 |
. . . 4
 ;   ;  |
188 | 2, 2, 18, 7, 174, 78, 175, 9, 1, 185, 187 | decma2c 11091 |
. . 3
 ; ;   ;;   |
189 | 4, 54, 7, 104 | declti 11076 |
. . 3
;  |
190 | 172, 173,
76, 188, 189 | ndvdsi 14391 |
. 2
; ;;   |
191 | 23, 15 | decnncl 11064 |
. . 3
;  |
192 | 23, 57 | deccl 11065 |
. . 3
;  |
193 | | 10nn 10775 |
. . 3
 |
194 | | eqid 2451 |
. . . 4
; ;  |
195 | | dec10 11081 |
. . . 4
;  |
196 | 23, 2 | deccl 11065 |
. . . 4
;  |
197 | 9, 1 | deccl 11065 |
. . . 4
;  |
198 | | eqid 2451 |
. . . . 5
; ;  |
199 | | eqid 2451 |
. . . . . 6
; ;  |
200 | | ax-1cn 9597 |
. . . . . . 7
 |
201 | | 6p1e7 10738 |
. . . . . . 7
   |
202 | 34, 200, 201 | addcomli 9825 |
. . . . . 6
   |
203 | 18, 9, 9, 1, 27, 199, 46, 202 | decadd 11092 |
. . . . 5
 ;  ;  |
204 | | 2t2e4 10759 |
. . . . . . 7
   |
205 | 204, 117 | oveq12i 6302 |
. . . . . 6
         |
206 | 205, 119 | eqtri 2473 |
. . . . 5
       |
207 | 32 | oveq1i 6300 |
. . . . . 6
       |
208 | 60, 34, 183 | addcomli 9825 |
. . . . . 6
  ;  |
209 | 207, 208 | eqtri 2473 |
. . . . 5
    ;  |
210 | 23, 2, 9, 57, 198, 203, 23, 2, 9, 206, 209 | decmac 11090 |
. . . 4
 ;   ;   ;  |
211 | | 7t2e14 11133 |
. . . . . . . . 9
  ;  |
212 | 60, 19, 211 | mulcomli 9650 |
. . . . . . . 8
  ;  |
213 | 9, 7, 23, 212, 119 | decaddi 11095 |
. . . . . . 7
    ;  |
214 | 60, 39, 155 | mulcomli 9650 |
. . . . . . 7
  ;  |
215 | 57, 23, 2, 198, 9, 23, 213, 214 | decmul1c 11098 |
. . . . . 6
;  ;;   |
216 | 215 | oveq1i 6300 |
. . . . 5
 ;   ;;    |
217 | 197, 9 | deccl 11065 |
. . . . . . 7
;;   |
218 | 217 | nn0cni 10881 |
. . . . . 6
;;   |
219 | 218 | addid1i 9820 |
. . . . 5
;;   ;;   |
220 | 216, 219 | eqtri 2473 |
. . . 4
 ;   ;;   |
221 | 23, 57, 9, 18, 194, 195, 196, 9, 197, 210, 220 | decma2c 11091 |
. . 3
 ; ;   ;;   |
222 | | 10pos 10712 |
. . . . 5
 |
223 | | 1lt2 10776 |
. . . . 5
 |
224 | 9, 23, 18, 2, 222, 223 | decltc 11073 |
. . . 4
; ;  |
225 | 195, 224 | eqbrtri 4422 |
. . 3
;  |
226 | 191, 192,
193, 221, 225 | ndvdsi 14391 |
. 2
; ;;   |
227 | 5, 14, 17, 22, 50, 52, 72, 106, 139, 170, 190, 226 | prmlem2 15091 |
1
;;   |