Proof of Theorem 2503lem3
Step | Hyp | Ref
| Expression |
1 | | 2nn 10767 |
. . . 4
 |
2 | | 1nn0 10885 |
. . . . 5
 |
3 | | 8nn0 10892 |
. . . . 5
 |
4 | 2, 3 | deccl 11065 |
. . . 4
;  |
5 | | nnexpcl 12285 |
. . . 4
  ;    ;    |
6 | 1, 4, 5 | mp2an 678 |
. . 3
  ;   |
7 | | nnm1nn0 10911 |
. . 3
   ; 
   ;     |
8 | 6, 7 | ax-mp 5 |
. 2
   ;    |
9 | | 3nn0 10887 |
. . . 4
 |
10 | 4, 9 | deccl 11065 |
. . 3
;;   |
11 | 10, 2 | deccl 11065 |
. 2
;;;    |
12 | | 2503prm.1 |
. . 3
;;;    |
13 | | 2nn0 10886 |
. . . . . 6
 |
14 | | 5nn0 10889 |
. . . . . 6
 |
15 | 13, 14 | deccl 11065 |
. . . . 5
;  |
16 | | 0nn0 10884 |
. . . . 5
 |
17 | 15, 16 | deccl 11065 |
. . . 4
;;   |
18 | | 3nn 10768 |
. . . 4
 |
19 | 17, 18 | decnncl 11064 |
. . 3
;;;    |
20 | 12, 19 | eqeltri 2525 |
. 2
 |
21 | 12 | 2503lem1 15108 |
. . 3
   ;   ;;;     |
22 | | 1p1e2 10723 |
. . . 4
   |
23 | | eqid 2451 |
. . . 4
;;;   ;;;    |
24 | 10, 2, 22, 23 | decsuc 11074 |
. . 3
;;;    ;;;    |
25 | 20, 6, 2, 11, 21, 24 | modsubi 15044 |
. 2
    ;    ;;;     |
26 | | 6nn0 10890 |
. . . . 5
 |
27 | | 7nn0 10891 |
. . . . 5
 |
28 | 26, 27 | deccl 11065 |
. . . 4
;  |
29 | 28, 13 | deccl 11065 |
. . 3
;;   |
30 | | 4nn0 10888 |
. . . . . 6
 |
31 | 30, 3 | deccl 11065 |
. . . . 5
;  |
32 | 31, 27 | deccl 11065 |
. . . 4
;;   |
33 | 4, 14 | deccl 11065 |
. . . . 5
;;   |
34 | 2, 2 | deccl 11065 |
. . . . . . 7
;  |
35 | 34, 27 | deccl 11065 |
. . . . . 6
;;   |
36 | 26, 3 | deccl 11065 |
. . . . . . 7
;  |
37 | | 9nn0 10893 |
. . . . . . . . 9
 |
38 | 30, 37 | deccl 11065 |
. . . . . . . 8
;  |
39 | 2, 37 | deccl 11065 |
. . . . . . . . 9
;  |
40 | 38 | nn0zi 10962 |
. . . . . . . . . . 11
;  |
41 | 39 | nn0zi 10962 |
. . . . . . . . . . 11
;  |
42 | | gcdcom 14484 |
. . . . . . . . . . 11
 ; ;  ; ;  ; ;    |
43 | 40, 41, 42 | mp2an 678 |
. . . . . . . . . 10
; ;  ; ;   |
44 | | 9nn 10774 |
. . . . . . . . . . . . 13
 |
45 | 2, 44 | decnncl 11064 |
. . . . . . . . . . . 12
;  |
46 | | 1nn 10620 |
. . . . . . . . . . . . 13
 |
47 | 2, 46 | decnncl 11064 |
. . . . . . . . . . . 12
;  |
48 | | eqid 2451 |
. . . . . . . . . . . . 13
; ;  |
49 | | eqid 2451 |
. . . . . . . . . . . . 13
; ;  |
50 | | 2cn 10680 |
. . . . . . . . . . . . . . . 16
 |
51 | 50 | mulid2i 9646 |
. . . . . . . . . . . . . . 15
   |
52 | 51, 22 | oveq12i 6302 |
. . . . . . . . . . . . . 14
         |
53 | | 2p2e4 10727 |
. . . . . . . . . . . . . 14
   |
54 | 52, 53 | eqtri 2473 |
. . . . . . . . . . . . 13
       |
55 | | 8p1e9 10740 |
. . . . . . . . . . . . . 14
   |
56 | | 9t2e18 11146 |
. . . . . . . . . . . . . 14
  ;  |
57 | 2, 3, 55, 56 | decsuc 11074 |
. . . . . . . . . . . . 13
    ;  |
58 | 2, 37, 2, 2, 48, 49, 13, 37, 2, 54, 57 | decmac 11090 |
. . . . . . . . . . . 12
 ;  ;  ;  |
59 | | 1lt9 10811 |
. . . . . . . . . . . . 13
 |
60 | 2, 2, 44, 59 | declt 11072 |
. . . . . . . . . . . 12
; ;  |
61 | 45, 13, 47, 58, 60 | ndvdsi 14391 |
. . . . . . . . . . 11
; ;  |
62 | | 19prm 15089 |
. . . . . . . . . . . 12
;  |
63 | | coprm 14657 |
. . . . . . . . . . . 12
 ; ;   ; ;
; ;     |
64 | 62, 40, 63 | mp2an 678 |
. . . . . . . . . . 11
 ;
;
; ;    |
65 | 61, 64 | mpbi 212 |
. . . . . . . . . 10
; ;   |
66 | 43, 65 | eqtri 2473 |
. . . . . . . . 9
; ;   |
67 | | eqid 2451 |
. . . . . . . . . 10
; ;  |
68 | | 4cn 10687 |
. . . . . . . . . . . . 13
 |
69 | 68 | mulid2i 9646 |
. . . . . . . . . . . 12
   |
70 | 69, 22 | oveq12i 6302 |
. . . . . . . . . . 11
         |
71 | | 4p2e6 10744 |
. . . . . . . . . . 11
   |
72 | 70, 71 | eqtri 2473 |
. . . . . . . . . 10
       |
73 | | 9cn 10697 |
. . . . . . . . . . . . 13
 |
74 | 73 | mulid2i 9646 |
. . . . . . . . . . . 12
   |
75 | 74 | oveq1i 6300 |
. . . . . . . . . . 11
       |
76 | | 9p9e18 11120 |
. . . . . . . . . . 11
  ;  |
77 | 75, 76 | eqtri 2473 |
. . . . . . . . . 10
    ;  |
78 | 30, 37, 2, 37, 67, 48, 2, 3, 2,
72, 77 | decma2c 11091 |
. . . . . . . . 9
  ;  ;  ;  |
79 | 2, 39, 38, 66, 78 | gcdi 15045 |
. . . . . . . 8
; ;   |
80 | | eqid 2451 |
. . . . . . . . 9
; ;  |
81 | | 6cn 10691 |
. . . . . . . . . . . 12
 |
82 | 81 | mulid2i 9646 |
. . . . . . . . . . 11
   |
83 | | 4p1e5 10736 |
. . . . . . . . . . 11
   |
84 | 82, 83 | oveq12i 6302 |
. . . . . . . . . 10
         |
85 | | 6p5e11 11101 |
. . . . . . . . . 10
  ;  |
86 | 84, 85 | eqtri 2473 |
. . . . . . . . 9
      ;  |
87 | | 8cn 10695 |
. . . . . . . . . . . 12
 |
88 | 87 | mulid2i 9646 |
. . . . . . . . . . 11
   |
89 | 88 | oveq1i 6300 |
. . . . . . . . . 10
       |
90 | | 9p8e17 11119 |
. . . . . . . . . . 11
  ;  |
91 | 73, 87, 90 | addcomli 9825 |
. . . . . . . . . 10
  ;  |
92 | 89, 91 | eqtri 2473 |
. . . . . . . . 9
    ;  |
93 | 26, 3, 30, 37, 80, 67, 2, 27, 2, 86, 92 | decma2c 11091 |
. . . . . . . 8
  ;  ;  ;;   |
94 | 2, 38, 36, 79, 93 | gcdi 15045 |
. . . . . . 7
;;  ;   |
95 | | eqid 2451 |
. . . . . . . 8
;;  ;;   |
96 | | 6p1e7 10738 |
. . . . . . . . . 10
   |
97 | 27 | dec0h 11067 |
. . . . . . . . . 10
;  |
98 | 96, 97 | eqtri 2473 |
. . . . . . . . 9
  ;  |
99 | | ax-1cn 9597 |
. . . . . . . . . . . 12
 |
100 | 99 | mulid1i 9645 |
. . . . . . . . . . 11
   |
101 | | 00id 9808 |
. . . . . . . . . . 11
   |
102 | 100, 101 | oveq12i 6302 |
. . . . . . . . . 10
         |
103 | 99 | addid1i 9820 |
. . . . . . . . . 10
   |
104 | 102, 103 | eqtri 2473 |
. . . . . . . . 9
       |
105 | 100 | oveq1i 6300 |
. . . . . . . . . 10
       |
106 | | 7cn 10693 |
. . . . . . . . . . 11
 |
107 | | 7p1e8 10739 |
. . . . . . . . . . 11
   |
108 | 106, 99, 107 | addcomli 9825 |
. . . . . . . . . 10
   |
109 | 3 | dec0h 11067 |
. . . . . . . . . 10
;  |
110 | 105, 108,
109 | 3eqtri 2477 |
. . . . . . . . 9
    ;  |
111 | 2, 2, 16, 27, 49, 98, 2, 3, 16, 104, 110 | decma2c 11091 |
. . . . . . . 8
  ;     ;  |
112 | 106 | mulid2i 9646 |
. . . . . . . . . 10
   |
113 | 112 | oveq1i 6300 |
. . . . . . . . 9
       |
114 | | 8p7e15 11111 |
. . . . . . . . . 10
  ;  |
115 | 87, 106, 114 | addcomli 9825 |
. . . . . . . . 9
  ;  |
116 | 113, 115 | eqtri 2473 |
. . . . . . . 8
    ;  |
117 | 34, 27, 26, 3, 95, 80, 2, 14, 2, 111, 116 | decma2c 11091 |
. . . . . . 7
  ;;   ;  ;;   |
118 | 2, 36, 35, 94, 117 | gcdi 15045 |
. . . . . 6
;;  ;;    |
119 | | eqid 2451 |
. . . . . . 7
;;  ;;   |
120 | | eqid 2451 |
. . . . . . . 8
; ;  |
121 | 2, 2, 22, 49 | decsuc 11074 |
. . . . . . . 8
;  ;  |
122 | 50 | mulid1i 9645 |
. . . . . . . . . 10
   |
123 | 122, 22 | oveq12i 6302 |
. . . . . . . . 9
         |
124 | 123, 53 | eqtri 2473 |
. . . . . . . 8
       |
125 | | 8t2e16 11139 |
. . . . . . . . . 10
  ;  |
126 | 87, 50, 125 | mulcomli 9650 |
. . . . . . . . 9
  ;  |
127 | | 6p2e8 10751 |
. . . . . . . . 9
   |
128 | 2, 26, 13, 126, 127 | decaddi 11095 |
. . . . . . . 8
    ;  |
129 | 2, 3, 2, 13, 120, 121, 13, 3, 2, 124, 128 | decma2c 11091 |
. . . . . . 7
  ;  ;   ;  |
130 | | 5cn 10689 |
. . . . . . . . . 10
 |
131 | | 5t2e10 10764 |
. . . . . . . . . 10
   |
132 | 130, 50, 131 | mulcomli 9650 |
. . . . . . . . 9
   |
133 | | dec10 11081 |
. . . . . . . . 9
;  |
134 | 132, 133 | eqtri 2473 |
. . . . . . . 8
  ;  |
135 | 106 | addid2i 9821 |
. . . . . . . 8
   |
136 | 2, 16, 27, 134, 135 | decaddi 11095 |
. . . . . . 7
    ;  |
137 | 4, 14, 34, 27, 119, 95, 13, 27, 2, 129, 136 | decma2c 11091 |
. . . . . 6
  ;;   ;;   ;;   |
138 | 13, 35, 33, 118, 137 | gcdi 15045 |
. . . . 5
;;  ;;    |
139 | | eqid 2451 |
. . . . . 6
;;  ;;   |
140 | | eqid 2451 |
. . . . . . 7
; ;  |
141 | 2, 3, 55, 120 | decsuc 11074 |
. . . . . . 7
;  ;  |
142 | 30, 3, 2, 37, 140, 141, 2, 27, 2, 72, 92 | decma2c 11091 |
. . . . . 6
  ;  ;   ;  |
143 | 112 | oveq1i 6300 |
. . . . . . 7
       |
144 | | 7p5e12 11104 |
. . . . . . 7
  ;  |
145 | 143, 144 | eqtri 2473 |
. . . . . 6
    ;  |
146 | 31, 27, 4, 14, 139, 119, 2, 13, 2, 142, 145 | decma2c 11091 |
. . . . 5
  ;;   ;;   ;;   |
147 | 2, 33, 32, 138, 146 | gcdi 15045 |
. . . 4
;;  ;;    |
148 | | eqid 2451 |
. . . . 5
;;  ;;   |
149 | | eqid 2451 |
. . . . . 6
; ;  |
150 | 30, 3, 55, 140 | decsuc 11074 |
. . . . . 6
;  ;  |
151 | 71 | oveq2i 6301 |
. . . . . . 7
           |
152 | | 6t2e12 11128 |
. . . . . . . . 9
  ;  |
153 | 81, 50, 152 | mulcomli 9650 |
. . . . . . . 8
  ;  |
154 | 81, 50, 127 | addcomli 9825 |
. . . . . . . 8
   |
155 | 2, 13, 26, 153, 154 | decaddi 11095 |
. . . . . . 7
    ;  |
156 | 151, 155 | eqtri 2473 |
. . . . . 6
      ;  |
157 | | 7t2e14 11133 |
. . . . . . . 8
  ;  |
158 | 106, 50, 157 | mulcomli 9650 |
. . . . . . 7
  ;  |
159 | | 9p4e13 11115 |
. . . . . . . 8
  ;  |
160 | 73, 68, 159 | addcomli 9825 |
. . . . . . 7
  ;  |
161 | 2, 30, 37, 158, 22, 9, 160 | decaddci 11096 |
. . . . . 6
    ;  |
162 | 26, 27, 30, 37, 149, 150, 13, 9, 13, 156, 161 | decma2c 11091 |
. . . . 5
  ;  ;   ;;   |
163 | | 2t2e4 10759 |
. . . . . . 7
   |
164 | 163 | oveq1i 6300 |
. . . . . 6
       |
165 | | 7p4e11 11103 |
. . . . . . 7
  ;  |
166 | 106, 68, 165 | addcomli 9825 |
. . . . . 6
  ;  |
167 | 164, 166 | eqtri 2473 |
. . . . 5
    ;  |
168 | 28, 13, 31, 27, 148, 139, 13, 2, 2, 162, 167 | decma2c 11091 |
. . . 4
  ;;   ;;   ;;;    |
169 | 13, 32, 29, 147, 168 | gcdi 15045 |
. . 3
;;;   ;;    |
170 | | eqid 2451 |
. . . . . 6
;;  ;;   |
171 | 28 | nn0cni 10881 |
. . . . . . 7
;  |
172 | 171 | addid1i 9820 |
. . . . . 6
;  ;  |
173 | 99 | addid2i 9821 |
. . . . . . . . 9
   |
174 | 100, 173 | oveq12i 6302 |
. . . . . . . 8
         |
175 | 174, 22 | eqtri 2473 |
. . . . . . 7
       |
176 | 88 | oveq1i 6300 |
. . . . . . . 8
       |
177 | 176, 114 | eqtri 2473 |
. . . . . . 7
    ;  |
178 | 2, 3, 16, 27, 120, 98, 2, 14, 2, 175, 177 | decma2c 11091 |
. . . . . 6
  ;     ;  |
179 | | 3cn 10684 |
. . . . . . . . 9
 |
180 | 179 | mulid2i 9646 |
. . . . . . . 8
   |
181 | 180 | oveq1i 6300 |
. . . . . . 7
       |
182 | | 7p3e10 10755 |
. . . . . . . 8
   |
183 | 106, 179,
182 | addcomli 9825 |
. . . . . . 7
   |
184 | 181, 183,
133 | 3eqtri 2477 |
. . . . . 6
    ;  |
185 | 4, 9, 26, 27, 170, 172, 2, 16, 2, 178, 184 | decma2c 11091 |
. . . . 5
  ;;   ;   ;;   |
186 | 100 | oveq1i 6300 |
. . . . . 6
       |
187 | | 1p2e3 10734 |
. . . . . 6
   |
188 | 9 | dec0h 11067 |
. . . . . 6
;  |
189 | 186, 187,
188 | 3eqtri 2477 |
. . . . 5
    ;  |
190 | 10, 2, 28, 13, 23, 148, 2, 9, 16, 185, 189 | decma2c 11091 |
. . . 4
  ;;;    ;;   ;;;    |
191 | 190, 12 | eqtr4i 2476 |
. . 3
  ;;;    ;;    |
192 | 2, 29, 11, 169, 191 | gcdi 15045 |
. 2
 ;;;     |
193 | 8, 11, 20, 25, 192 | gcdmodi 15046 |
1
    ;     |