Proof of Theorem 2503lem3
Step | Hyp | Ref
| Expression |
1 | | 2nn 11185 |
. . . 4
|
2 | | 1nn0 11308 |
. . . . 5
|
3 | | 8nn0 11315 |
. . . . 5
|
4 | 2, 3 | deccl 11512 |
. . . 4
; |
5 | | nnexpcl 12873 |
. . . 4
; ; |
6 | 1, 4, 5 | mp2an 708 |
. . 3
; |
7 | | nnm1nn0 11334 |
. . 3
;
; |
8 | 6, 7 | ax-mp 5 |
. 2
; |
9 | | 3nn0 11310 |
. . . 4
|
10 | 4, 9 | deccl 11512 |
. . 3
;; |
11 | 10, 2 | deccl 11512 |
. 2
;;; |
12 | | 2503prm.1 |
. . 3
;;; |
13 | | 2nn0 11309 |
. . . . . 6
|
14 | | 5nn0 11312 |
. . . . . 6
|
15 | 13, 14 | deccl 11512 |
. . . . 5
; |
16 | | 0nn0 11307 |
. . . . 5
|
17 | 15, 16 | deccl 11512 |
. . . 4
;; |
18 | | 3nn 11186 |
. . . 4
|
19 | 17, 18 | decnncl 11518 |
. . 3
;;; |
20 | 12, 19 | eqeltri 2697 |
. 2
|
21 | 12 | 2503lem1 15844 |
. . 3
; ;;; |
22 | | 1p1e2 11134 |
. . . 4
|
23 | | eqid 2622 |
. . . 4
;;; ;;; |
24 | 10, 2, 22, 23 | decsuc 11535 |
. . 3
;;; ;;; |
25 | 20, 6, 2, 11, 21, 24 | modsubi 15776 |
. 2
; ;;; |
26 | | 6nn0 11313 |
. . . . 5
|
27 | | 7nn0 11314 |
. . . . 5
|
28 | 26, 27 | deccl 11512 |
. . . 4
; |
29 | 28, 13 | deccl 11512 |
. . 3
;; |
30 | | 4nn0 11311 |
. . . . . 6
|
31 | 30, 3 | deccl 11512 |
. . . . 5
; |
32 | 31, 27 | deccl 11512 |
. . . 4
;; |
33 | 4, 14 | deccl 11512 |
. . . . 5
;; |
34 | 2, 2 | deccl 11512 |
. . . . . . 7
; |
35 | 34, 27 | deccl 11512 |
. . . . . 6
;; |
36 | 26, 3 | deccl 11512 |
. . . . . . 7
; |
37 | | 9nn0 11316 |
. . . . . . . . 9
|
38 | 30, 37 | deccl 11512 |
. . . . . . . 8
; |
39 | 2, 37 | deccl 11512 |
. . . . . . . . 9
; |
40 | 38 | nn0zi 11402 |
. . . . . . . . . . 11
; |
41 | 39 | nn0zi 11402 |
. . . . . . . . . . 11
; |
42 | | gcdcom 15235 |
. . . . . . . . . . 11
; ; ; ; ; ; |
43 | 40, 41, 42 | mp2an 708 |
. . . . . . . . . 10
; ; ; ; |
44 | | 9nn 11192 |
. . . . . . . . . . . . 13
|
45 | 2, 44 | decnncl 11518 |
. . . . . . . . . . . 12
; |
46 | | 1nn 11031 |
. . . . . . . . . . . . 13
|
47 | 2, 46 | decnncl 11518 |
. . . . . . . . . . . 12
; |
48 | | eqid 2622 |
. . . . . . . . . . . . 13
; ; |
49 | | eqid 2622 |
. . . . . . . . . . . . 13
; ; |
50 | | 2cn 11091 |
. . . . . . . . . . . . . . . 16
|
51 | 50 | mulid2i 10043 |
. . . . . . . . . . . . . . 15
|
52 | 51, 22 | oveq12i 6662 |
. . . . . . . . . . . . . 14
|
53 | | 2p2e4 11144 |
. . . . . . . . . . . . . 14
|
54 | 52, 53 | eqtri 2644 |
. . . . . . . . . . . . 13
|
55 | | 8p1e9 11158 |
. . . . . . . . . . . . . 14
|
56 | | 9t2e18 11663 |
. . . . . . . . . . . . . 14
; |
57 | 2, 3, 55, 56 | decsuc 11535 |
. . . . . . . . . . . . 13
; |
58 | 2, 37, 2, 2, 48, 49, 13, 37, 2, 54, 57 | decmac 11566 |
. . . . . . . . . . . 12
; ; ; |
59 | | 1lt9 11229 |
. . . . . . . . . . . . 13
|
60 | 2, 2, 44, 59 | declt 11530 |
. . . . . . . . . . . 12
; ; |
61 | 45, 13, 47, 58, 60 | ndvdsi 15136 |
. . . . . . . . . . 11
; ; |
62 | | 19prm 15825 |
. . . . . . . . . . . 12
; |
63 | | coprm 15423 |
. . . . . . . . . . . 12
; ; ; ;
; ; |
64 | 62, 40, 63 | mp2an 708 |
. . . . . . . . . . 11
;
;
; ; |
65 | 61, 64 | mpbi 220 |
. . . . . . . . . 10
; ; |
66 | 43, 65 | eqtri 2644 |
. . . . . . . . 9
; ; |
67 | | eqid 2622 |
. . . . . . . . . 10
; ; |
68 | | 4cn 11098 |
. . . . . . . . . . . . 13
|
69 | 68 | mulid2i 10043 |
. . . . . . . . . . . 12
|
70 | 69, 22 | oveq12i 6662 |
. . . . . . . . . . 11
|
71 | | 4p2e6 11162 |
. . . . . . . . . . 11
|
72 | 70, 71 | eqtri 2644 |
. . . . . . . . . 10
|
73 | | 9cn 11108 |
. . . . . . . . . . . . 13
|
74 | 73 | mulid2i 10043 |
. . . . . . . . . . . 12
|
75 | 74 | oveq1i 6660 |
. . . . . . . . . . 11
|
76 | | 9p9e18 11627 |
. . . . . . . . . . 11
; |
77 | 75, 76 | eqtri 2644 |
. . . . . . . . . 10
; |
78 | 30, 37, 2, 37, 67, 48, 2, 3, 2,
72, 77 | decma2c 11568 |
. . . . . . . . 9
; ; ; |
79 | 2, 39, 38, 66, 78 | gcdi 15777 |
. . . . . . . 8
; ; |
80 | | eqid 2622 |
. . . . . . . . 9
; ; |
81 | | 6cn 11102 |
. . . . . . . . . . . 12
|
82 | 81 | mulid2i 10043 |
. . . . . . . . . . 11
|
83 | | 4p1e5 11154 |
. . . . . . . . . . 11
|
84 | 82, 83 | oveq12i 6662 |
. . . . . . . . . 10
|
85 | | 6p5e11 11600 |
. . . . . . . . . 10
; |
86 | 84, 85 | eqtri 2644 |
. . . . . . . . 9
; |
87 | | 8cn 11106 |
. . . . . . . . . . . 12
|
88 | 87 | mulid2i 10043 |
. . . . . . . . . . 11
|
89 | 88 | oveq1i 6660 |
. . . . . . . . . 10
|
90 | | 9p8e17 11626 |
. . . . . . . . . . 11
; |
91 | 73, 87, 90 | addcomli 10228 |
. . . . . . . . . 10
; |
92 | 89, 91 | eqtri 2644 |
. . . . . . . . 9
; |
93 | 26, 3, 30, 37, 80, 67, 2, 27, 2, 86, 92 | decma2c 11568 |
. . . . . . . 8
; ; ;; |
94 | 2, 38, 36, 79, 93 | gcdi 15777 |
. . . . . . 7
;; ; |
95 | | eqid 2622 |
. . . . . . . 8
;; ;; |
96 | | 6p1e7 11156 |
. . . . . . . . . 10
|
97 | 27 | dec0h 11522 |
. . . . . . . . . 10
; |
98 | 96, 97 | eqtri 2644 |
. . . . . . . . 9
; |
99 | | 1t1e1 11175 |
. . . . . . . . . . 11
|
100 | | 00id 10211 |
. . . . . . . . . . 11
|
101 | 99, 100 | oveq12i 6662 |
. . . . . . . . . 10
|
102 | | ax-1cn 9994 |
. . . . . . . . . . 11
|
103 | 102 | addid1i 10223 |
. . . . . . . . . 10
|
104 | 101, 103 | eqtri 2644 |
. . . . . . . . 9
|
105 | 99 | oveq1i 6660 |
. . . . . . . . . 10
|
106 | | 7cn 11104 |
. . . . . . . . . . 11
|
107 | | 7p1e8 11157 |
. . . . . . . . . . 11
|
108 | 106, 102,
107 | addcomli 10228 |
. . . . . . . . . 10
|
109 | 3 | dec0h 11522 |
. . . . . . . . . 10
; |
110 | 105, 108,
109 | 3eqtri 2648 |
. . . . . . . . 9
; |
111 | 2, 2, 16, 27, 49, 98, 2, 3, 16, 104, 110 | decma2c 11568 |
. . . . . . . 8
; ; |
112 | 106 | mulid2i 10043 |
. . . . . . . . . 10
|
113 | 112 | oveq1i 6660 |
. . . . . . . . 9
|
114 | | 8p7e15 11617 |
. . . . . . . . . 10
; |
115 | 87, 106, 114 | addcomli 10228 |
. . . . . . . . 9
; |
116 | 113, 115 | eqtri 2644 |
. . . . . . . 8
; |
117 | 34, 27, 26, 3, 95, 80, 2, 14, 2, 111, 116 | decma2c 11568 |
. . . . . . 7
;; ; ;; |
118 | 2, 36, 35, 94, 117 | gcdi 15777 |
. . . . . 6
;; ;; |
119 | | eqid 2622 |
. . . . . . 7
;; ;; |
120 | | eqid 2622 |
. . . . . . . 8
; ; |
121 | 2, 2, 22, 49 | decsuc 11535 |
. . . . . . . 8
; ; |
122 | | 2t1e2 11176 |
. . . . . . . . . 10
|
123 | 122, 22 | oveq12i 6662 |
. . . . . . . . 9
|
124 | 123, 53 | eqtri 2644 |
. . . . . . . 8
|
125 | | 8t2e16 11654 |
. . . . . . . . . 10
; |
126 | 87, 50, 125 | mulcomli 10047 |
. . . . . . . . 9
; |
127 | | 6p2e8 11169 |
. . . . . . . . 9
|
128 | 2, 26, 13, 126, 127 | decaddi 11579 |
. . . . . . . 8
; |
129 | 2, 3, 2, 13, 120, 121, 13, 3, 2, 124, 128 | decma2c 11568 |
. . . . . . 7
; ; ; |
130 | | 5cn 11100 |
. . . . . . . . 9
|
131 | | 5t2e10 11634 |
. . . . . . . . 9
; |
132 | 130, 50, 131 | mulcomli 10047 |
. . . . . . . 8
; |
133 | 106 | addid2i 10224 |
. . . . . . . 8
|
134 | 2, 16, 27, 132, 133 | decaddi 11579 |
. . . . . . 7
; |
135 | 4, 14, 34, 27, 119, 95, 13, 27, 2, 129, 134 | decma2c 11568 |
. . . . . 6
;; ;; ;; |
136 | 13, 35, 33, 118, 135 | gcdi 15777 |
. . . . 5
;; ;; |
137 | | eqid 2622 |
. . . . . 6
;; ;; |
138 | | eqid 2622 |
. . . . . . 7
; ; |
139 | 2, 3, 55, 120 | decsuc 11535 |
. . . . . . 7
; ; |
140 | 30, 3, 2, 37, 138, 139, 2, 27, 2, 72, 92 | decma2c 11568 |
. . . . . 6
; ; ; |
141 | 112 | oveq1i 6660 |
. . . . . . 7
|
142 | | 7p5e12 11607 |
. . . . . . 7
; |
143 | 141, 142 | eqtri 2644 |
. . . . . 6
; |
144 | 31, 27, 4, 14, 137, 119, 2, 13, 2, 140, 143 | decma2c 11568 |
. . . . 5
;; ;; ;; |
145 | 2, 33, 32, 136, 144 | gcdi 15777 |
. . . 4
;; ;; |
146 | | eqid 2622 |
. . . . 5
;; ;; |
147 | | eqid 2622 |
. . . . . 6
; ; |
148 | 30, 3, 55, 138 | decsuc 11535 |
. . . . . 6
; ; |
149 | 71 | oveq2i 6661 |
. . . . . . 7
|
150 | | 6t2e12 11641 |
. . . . . . . . 9
; |
151 | 81, 50, 150 | mulcomli 10047 |
. . . . . . . 8
; |
152 | 81, 50, 127 | addcomli 10228 |
. . . . . . . 8
|
153 | 2, 13, 26, 151, 152 | decaddi 11579 |
. . . . . . 7
; |
154 | 149, 153 | eqtri 2644 |
. . . . . 6
; |
155 | | 7t2e14 11648 |
. . . . . . . 8
; |
156 | 106, 50, 155 | mulcomli 10047 |
. . . . . . 7
; |
157 | | 9p4e13 11622 |
. . . . . . . 8
; |
158 | 73, 68, 157 | addcomli 10228 |
. . . . . . 7
; |
159 | 2, 30, 37, 156, 22, 9, 158 | decaddci 11580 |
. . . . . 6
; |
160 | 26, 27, 30, 37, 147, 148, 13, 9, 13, 154, 159 | decma2c 11568 |
. . . . 5
; ; ;; |
161 | | 2t2e4 11177 |
. . . . . . 7
|
162 | 161 | oveq1i 6660 |
. . . . . 6
|
163 | | 7p4e11 11605 |
. . . . . . 7
; |
164 | 106, 68, 163 | addcomli 10228 |
. . . . . 6
; |
165 | 162, 164 | eqtri 2644 |
. . . . 5
; |
166 | 28, 13, 31, 27, 146, 137, 13, 2, 2, 160, 165 | decma2c 11568 |
. . . 4
;; ;; ;;; |
167 | 13, 32, 29, 145, 166 | gcdi 15777 |
. . 3
;;; ;; |
168 | | eqid 2622 |
. . . . . 6
;; ;; |
169 | 28 | nn0cni 11304 |
. . . . . . 7
; |
170 | 169 | addid1i 10223 |
. . . . . 6
; ; |
171 | 102 | addid2i 10224 |
. . . . . . . . 9
|
172 | 99, 171 | oveq12i 6662 |
. . . . . . . 8
|
173 | 172, 22 | eqtri 2644 |
. . . . . . 7
|
174 | 88 | oveq1i 6660 |
. . . . . . . 8
|
175 | 174, 114 | eqtri 2644 |
. . . . . . 7
; |
176 | 2, 3, 16, 27, 120, 98, 2, 14, 2, 173, 175 | decma2c 11568 |
. . . . . 6
; ; |
177 | | 3cn 11095 |
. . . . . . . . 9
|
178 | 177 | mulid2i 10043 |
. . . . . . . 8
|
179 | 178 | oveq1i 6660 |
. . . . . . 7
|
180 | | 7p3e10 11603 |
. . . . . . . 8
; |
181 | 106, 177,
180 | addcomli 10228 |
. . . . . . 7
; |
182 | 179, 181 | eqtri 2644 |
. . . . . 6
; |
183 | 4, 9, 26, 27, 168, 170, 2, 16, 2, 176, 182 | decma2c 11568 |
. . . . 5
;; ; ;; |
184 | 99 | oveq1i 6660 |
. . . . . 6
|
185 | | 1p2e3 11152 |
. . . . . 6
|
186 | 9 | dec0h 11522 |
. . . . . 6
; |
187 | 184, 185,
186 | 3eqtri 2648 |
. . . . 5
; |
188 | 10, 2, 28, 13, 23, 146, 2, 9, 16, 183, 187 | decma2c 11568 |
. . . 4
;;; ;; ;;; |
189 | 188, 12 | eqtr4i 2647 |
. . 3
;;; ;; |
190 | 2, 29, 11, 167, 189 | gcdi 15777 |
. 2
;;; |
191 | 8, 11, 20, 25, 190 | gcdmodi 15778 |
1
; |