Proof of Theorem 1259lem5
Step | Hyp | Ref
| Expression |
1 | | 2nn 10767 |
. . . 4
 |
2 | | 3nn0 10887 |
. . . . 5
 |
3 | | 4nn0 10888 |
. . . . 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 | | 8nn0 10892 |
. . . 4
 |
10 | | 6nn0 10890 |
. . . 4
 |
11 | 9, 10 | deccl 11065 |
. . 3
;  |
12 | | 9nn0 10893 |
. . 3
 |
13 | 11, 12 | deccl 11065 |
. 2
;;   |
14 | | 1259prm.1 |
. . 3
;;;    |
15 | | 1nn0 10885 |
. . . . . 6
 |
16 | | 2nn0 10886 |
. . . . . 6
 |
17 | 15, 16 | deccl 11065 |
. . . . 5
;  |
18 | | 5nn0 10889 |
. . . . 5
 |
19 | 17, 18 | deccl 11065 |
. . . 4
;;   |
20 | | 9nn 10774 |
. . . 4
 |
21 | 19, 20 | decnncl 11064 |
. . 3
;;;    |
22 | 14, 21 | eqeltri 2525 |
. 2
 |
23 | 14 | 1259lem2 15103 |
. . 3
   ;   ;;    |
24 | | 6p1e7 10738 |
. . . . 5
   |
25 | | eqid 2451 |
. . . . 5
; ;  |
26 | 9, 10, 24, 25 | decsuc 11074 |
. . . 4
;  ;  |
27 | | eqid 2451 |
. . . 4
;;  ;;   |
28 | 11, 26, 27 | decsucc 11078 |
. . 3
;;   ;;   |
29 | 22, 6, 15, 13, 23, 28 | modsubi 15044 |
. 2
    ;    ;;    |
30 | 2, 12 | deccl 11065 |
. . . 4
;  |
31 | | 0nn0 10884 |
. . . 4
 |
32 | 30, 31 | deccl 11065 |
. . 3
;;   |
33 | 9, 12 | deccl 11065 |
. . . 4
;  |
34 | 16, 15 | deccl 11065 |
. . . . . 6
;  |
35 | 15, 2 | deccl 11065 |
. . . . . . 7
;  |
36 | 34 | nn0zi 10962 |
. . . . . . . . 9
;  |
37 | 35 | nn0zi 10962 |
. . . . . . . . 9
;  |
38 | | gcdcom 14484 |
. . . . . . . . 9
 ; ;  ; ;  ; ;    |
39 | 36, 37, 38 | mp2an 678 |
. . . . . . . 8
; ;  ; ;   |
40 | | 3nn 10768 |
. . . . . . . . . . 11
 |
41 | 15, 40 | decnncl 11064 |
. . . . . . . . . 10
;  |
42 | | 8nn 10773 |
. . . . . . . . . 10
 |
43 | | eqid 2451 |
. . . . . . . . . . 11
; ;  |
44 | 9 | dec0h 11067 |
. . . . . . . . . . 11
;  |
45 | | ax-1cn 9597 |
. . . . . . . . . . . . . 14
 |
46 | 45 | mulid1i 9645 |
. . . . . . . . . . . . 13
   |
47 | 45 | addid2i 9821 |
. . . . . . . . . . . . 13
   |
48 | 46, 47 | oveq12i 6302 |
. . . . . . . . . . . 12
         |
49 | | 1p1e2 10723 |
. . . . . . . . . . . 12
   |
50 | 48, 49 | eqtri 2473 |
. . . . . . . . . . 11
       |
51 | | 3cn 10684 |
. . . . . . . . . . . . . 14
 |
52 | 51 | mulid1i 9645 |
. . . . . . . . . . . . 13
   |
53 | 52 | oveq1i 6300 |
. . . . . . . . . . . 12
       |
54 | | 8cn 10695 |
. . . . . . . . . . . . 13
 |
55 | | 8p3e11 11107 |
. . . . . . . . . . . . 13
  ;  |
56 | 54, 51, 55 | addcomli 9825 |
. . . . . . . . . . . 12
  ;  |
57 | 53, 56 | eqtri 2473 |
. . . . . . . . . . 11
    ;  |
58 | 15, 2, 31, 9, 43, 44, 15, 15, 15, 50, 57 | decmac 11090 |
. . . . . . . . . 10
 ;   ;  |
59 | | 1nn 10620 |
. . . . . . . . . . 11
 |
60 | | 8lt10 10813 |
. . . . . . . . . . 11
 |
61 | 59, 2, 9, 60 | declti 11076 |
. . . . . . . . . 10
;  |
62 | 41, 15, 42, 58, 61 | ndvdsi 14391 |
. . . . . . . . 9
; ;  |
63 | | 13prm 15087 |
. . . . . . . . . 10
;  |
64 | | coprm 14657 |
. . . . . . . . . 10
 ; ;   ; ;
; ;     |
65 | 63, 36, 64 | mp2an 678 |
. . . . . . . . 9
 ;
;
; ;    |
66 | 62, 65 | mpbi 212 |
. . . . . . . 8
; ;   |
67 | 39, 66 | eqtri 2473 |
. . . . . . 7
; ;   |
68 | | eqid 2451 |
. . . . . . . 8
; ;  |
69 | | 2cn 10680 |
. . . . . . . . . . 11
 |
70 | 69 | mulid2i 9646 |
. . . . . . . . . 10
   |
71 | 45 | addid1i 9820 |
. . . . . . . . . 10
   |
72 | 70, 71 | oveq12i 6302 |
. . . . . . . . 9
         |
73 | | 2p1e3 10733 |
. . . . . . . . 9
   |
74 | 72, 73 | eqtri 2473 |
. . . . . . . 8
       |
75 | 46 | oveq1i 6300 |
. . . . . . . . 9
       |
76 | | 3p1e4 10735 |
. . . . . . . . . 10
   |
77 | 51, 45, 76 | addcomli 9825 |
. . . . . . . . 9
   |
78 | 3 | dec0h 11067 |
. . . . . . . . 9
;  |
79 | 75, 77, 78 | 3eqtri 2477 |
. . . . . . . 8
    ;  |
80 | 16, 15, 15, 2, 68, 43, 15, 3, 31, 74, 79 | decma2c 11091 |
. . . . . . 7
  ;  ;  ;  |
81 | 15, 35, 34, 67, 80 | gcdi 15045 |
. . . . . 6
; ;   |
82 | | eqid 2451 |
. . . . . . 7
; ;  |
83 | | 3t2e6 10761 |
. . . . . . . . . 10
   |
84 | 51, 69, 83 | mulcomli 9650 |
. . . . . . . . 9
   |
85 | 69 | addid1i 9820 |
. . . . . . . . 9
   |
86 | 84, 85 | oveq12i 6302 |
. . . . . . . 8
         |
87 | | 6p2e8 10751 |
. . . . . . . 8
   |
88 | 86, 87 | eqtri 2473 |
. . . . . . 7
       |
89 | | 4cn 10687 |
. . . . . . . . . 10
 |
90 | | 4t2e8 10763 |
. . . . . . . . . 10
   |
91 | 89, 69, 90 | mulcomli 9650 |
. . . . . . . . 9
   |
92 | 91 | oveq1i 6300 |
. . . . . . . 8
       |
93 | | 8p1e9 10740 |
. . . . . . . 8
   |
94 | 12 | dec0h 11067 |
. . . . . . . 8
;  |
95 | 92, 93, 94 | 3eqtri 2477 |
. . . . . . 7
    ;  |
96 | 2, 3, 16, 15, 82, 68, 16, 12, 31, 88, 95 | decma2c 11091 |
. . . . . 6
  ;  ;  ;  |
97 | 16, 34, 4, 81, 96 | gcdi 15045 |
. . . . 5
; ;   |
98 | | eqid 2451 |
. . . . . 6
; ;  |
99 | | 4p3e7 10745 |
. . . . . . . . 9
   |
100 | 89, 51, 99 | addcomli 9825 |
. . . . . . . 8
   |
101 | 100 | oveq2i 6301 |
. . . . . . 7
           |
102 | | 7nn0 10891 |
. . . . . . . 8
 |
103 | | 8t4e32 11141 |
. . . . . . . . 9
  ;  |
104 | 54, 89, 103 | mulcomli 9650 |
. . . . . . . 8
  ;  |
105 | | 7cn 10693 |
. . . . . . . . 9
 |
106 | | 7p2e9 10754 |
. . . . . . . . 9
   |
107 | 105, 69, 106 | addcomli 9825 |
. . . . . . . 8
   |
108 | 2, 16, 102, 104, 107 | decaddi 11095 |
. . . . . . 7
    ;  |
109 | 101, 108 | eqtri 2473 |
. . . . . 6
      ;  |
110 | | 9cn 10697 |
. . . . . . . 8
 |
111 | | 9t4e36 11148 |
. . . . . . . 8
  ;  |
112 | 110, 89, 111 | mulcomli 9650 |
. . . . . . 7
  ;  |
113 | | 6p4e10 10753 |
. . . . . . 7
   |
114 | 2, 10, 3, 112, 76, 113 | decaddci2 11097 |
. . . . . 6
    ;  |
115 | 9, 12, 2, 3, 98, 82, 3, 31, 3, 109, 114 | decma2c 11091 |
. . . . 5
  ;  ;  ;;   |
116 | 3, 4, 33, 97, 115 | gcdi 15045 |
. . . 4
;;  ;   |
117 | | eqid 2451 |
. . . . 5
;;  ;;   |
118 | | eqid 2451 |
. . . . . 6
; ;  |
119 | 54 | addid1i 9820 |
. . . . . . 7
   |
120 | 119, 44 | eqtri 2473 |
. . . . . 6
  ;  |
121 | 69 | addid2i 9821 |
. . . . . . . 8
   |
122 | 84, 121 | oveq12i 6302 |
. . . . . . 7
         |
123 | 122, 87 | eqtri 2473 |
. . . . . 6
       |
124 | | 9t2e18 11146 |
. . . . . . . 8
  ;  |
125 | 110, 69, 124 | mulcomli 9650 |
. . . . . . 7
  ;  |
126 | | 8p8e16 11112 |
. . . . . . 7
  ;  |
127 | 15, 9, 9, 125, 49, 10, 126 | decaddci 11096 |
. . . . . 6
    ;  |
128 | 2, 12, 31, 9, 118, 120, 16, 10, 16, 123, 127 | decma2c 11091 |
. . . . 5
  ;     ;  |
129 | | 2t0e0 10765 |
. . . . . . 7
   |
130 | 129 | oveq1i 6300 |
. . . . . 6
       |
131 | 110 | addid2i 9821 |
. . . . . 6
   |
132 | 130, 131,
94 | 3eqtri 2477 |
. . . . 5
    ;  |
133 | 30, 31, 9, 12, 117, 98, 16, 12, 31, 128, 132 | decma2c 11091 |
. . . 4
  ;;   ;  ;;   |
134 | 16, 33, 32, 116, 133 | gcdi 15045 |
. . 3
;;  ;;    |
135 | 30 | nn0cni 10881 |
. . . . . . 7
;  |
136 | 135 | addid1i 9820 |
. . . . . 6
;  ;  |
137 | 54 | mulid2i 9646 |
. . . . . . . 8
   |
138 | 137, 76 | oveq12i 6302 |
. . . . . . 7
         |
139 | | 8p4e12 11108 |
. . . . . . 7
  ;  |
140 | 138, 139 | eqtri 2473 |
. . . . . 6
      ;  |
141 | | 6cn 10691 |
. . . . . . . . 9
 |
142 | 141 | mulid2i 9646 |
. . . . . . . 8
   |
143 | 142 | oveq1i 6300 |
. . . . . . 7
       |
144 | | 9p6e15 11117 |
. . . . . . . 8
  ;  |
145 | 110, 141,
144 | addcomli 9825 |
. . . . . . 7
  ;  |
146 | 143, 145 | eqtri 2473 |
. . . . . 6
    ;  |
147 | 9, 10, 2, 12, 25, 136, 15, 18, 15, 140, 146 | decma2c 11091 |
. . . . 5
  ;  ;   ;;   |
148 | 110 | mulid2i 9646 |
. . . . . . 7
   |
149 | 148 | oveq1i 6300 |
. . . . . 6
       |
150 | 110 | addid1i 9820 |
. . . . . 6
   |
151 | 149, 150,
94 | 3eqtri 2477 |
. . . . 5
    ;  |
152 | 11, 12, 30, 31, 27, 117, 15, 12, 31, 147, 151 | decma2c 11091 |
. . . 4
  ;;   ;;   ;;;    |
153 | 152, 14 | eqtr4i 2476 |
. . 3
  ;;   ;;    |
154 | 15, 32, 13, 134, 153 | gcdi 15045 |
. 2
 ;;    |
155 | 8, 13, 22, 29, 154 | gcdmodi 15046 |
1
    ;     |