Proof of Theorem 127prm
Step | Hyp | Ref
| Expression |
1 | | 1nn0 11308 |
. . . 4
|
2 | | 2nn0 11309 |
. . . 4
|
3 | 1, 2 | deccl 11512 |
. . 3
; |
4 | | 7nn 11190 |
. . 3
|
5 | 3, 4 | decnncl 11518 |
. 2
;; |
6 | | 8nn0 11315 |
. . 3
|
7 | | 4nn0 11311 |
. . 3
|
8 | | 7nn0 11314 |
. . 3
|
9 | | 1lt8 11221 |
. . 3
|
10 | | 2lt10 11680 |
. . 3
; |
11 | | 7lt10 11675 |
. . 3
; |
12 | 1, 6, 2, 7, 8, 1, 9, 10, 11 | 3decltc 11538 |
. 2
;; ;; |
13 | | 2nn 11185 |
. . . 4
|
14 | 1, 13 | decnncl 11518 |
. . 3
; |
15 | | 1lt10 11681 |
. . 3
; |
16 | 14, 8, 1, 15 | declti 11546 |
. 2
;; |
17 | | 3nn0 11310 |
. . 3
|
18 | | 3t2e6 11179 |
. . 3
|
19 | | df-7 11084 |
. . 3
|
20 | 3, 17, 18, 19 | dec2dvds 15767 |
. 2
;; |
21 | | 3nn 11186 |
. . . 4
|
22 | | 1nn 11031 |
. . . 4
|
23 | | 3t3e9 11180 |
. . . . . 6
|
24 | 23 | oveq1i 6660 |
. . . . 5
|
25 | | 9p1e10 11496 |
. . . . 5
; |
26 | 24, 25 | eqtri 2644 |
. . . 4
; |
27 | | 1lt3 11196 |
. . . 4
|
28 | 21, 17, 22, 26, 27 | ndvdsi 15136 |
. . 3
; |
29 | 1, 2, 8 | 3dvds2dec 15056 |
. . . 4
;; |
30 | | 1p2e3 11152 |
. . . . . . 7
|
31 | 30 | oveq1i 6660 |
. . . . . 6
|
32 | | 7cn 11104 |
. . . . . . 7
|
33 | | 3cn 11095 |
. . . . . . 7
|
34 | | 7p3e10 11603 |
. . . . . . 7
; |
35 | 32, 33, 34 | addcomli 10228 |
. . . . . 6
; |
36 | 31, 35 | eqtri 2644 |
. . . . 5
; |
37 | 36 | breq2i 4661 |
. . . 4
; |
38 | 29, 37 | bitri 264 |
. . 3
;; ; |
39 | 28, 38 | mtbir 313 |
. 2
;; |
40 | | 2lt5 11202 |
. . 3
|
41 | | 5p2e7 11165 |
. . 3
|
42 | 3, 13, 40, 41 | dec5dvds2 15769 |
. 2
;; |
43 | 1, 6 | deccl 11512 |
. . 3
; |
44 | | 0nn0 11307 |
. . . 4
|
45 | | eqid 2622 |
. . . 4
; ; |
46 | 1 | dec0h 11522 |
. . . 4
; |
47 | | 5nn0 11312 |
. . . 4
|
48 | 32 | mulid1i 10042 |
. . . . . 6
|
49 | | 5cn 11100 |
. . . . . . 7
|
50 | 49 | addid2i 10224 |
. . . . . 6
|
51 | 48, 50 | oveq12i 6662 |
. . . . 5
|
52 | | 7p5e12 11607 |
. . . . 5
; |
53 | 51, 52 | eqtri 2644 |
. . . 4
; |
54 | | 6nn0 11313 |
. . . . 5
|
55 | | 8cn 11106 |
. . . . . 6
|
56 | | 8t7e56 11661 |
. . . . . 6
; |
57 | 55, 32, 56 | mulcomli 10047 |
. . . . 5
; |
58 | | 6p1e7 11156 |
. . . . 5
|
59 | 47, 54, 1, 57, 58 | decaddi 11579 |
. . . 4
; |
60 | 1, 6, 44, 1, 45, 46, 8, 8, 47, 53, 59 | decma2c 11568 |
. . 3
; ;; |
61 | | 1lt7 11214 |
. . 3
|
62 | 4, 43, 22, 60, 61 | ndvdsi 15136 |
. 2
;; |
63 | 1, 22 | decnncl 11518 |
. . 3
; |
64 | 1, 1 | deccl 11512 |
. . 3
; |
65 | | 6nn 11189 |
. . 3
|
66 | | eqid 2622 |
. . . 4
; ; |
67 | 54 | dec0h 11522 |
. . . 4
; |
68 | 64 | nn0cni 11304 |
. . . . . . 7
; |
69 | 68 | mulid1i 10042 |
. . . . . 6
; ; |
70 | | ax-1cn 9994 |
. . . . . . 7
|
71 | 70 | addid2i 10224 |
. . . . . 6
|
72 | 69, 71 | oveq12i 6662 |
. . . . 5
; ; |
73 | | 1p1e2 11134 |
. . . . . 6
|
74 | 1, 1, 1, 66, 73 | decaddi 11579 |
. . . . 5
; ; |
75 | 72, 74 | eqtri 2644 |
. . . 4
; ; |
76 | | 6cn 11102 |
. . . . . 6
|
77 | 76, 70, 58 | addcomli 10228 |
. . . . 5
|
78 | 1, 1, 54, 69, 77 | decaddi 11579 |
. . . 4
; ; |
79 | 1, 1, 44, 54, 66, 67, 64, 8, 1, 75, 78 | decma2c 11568 |
. . 3
; ; ;; |
80 | | 6lt10 11676 |
. . . 4
; |
81 | 22, 1, 54, 80 | declti 11546 |
. . 3
; |
82 | 63, 64, 65, 79, 81 | ndvdsi 15136 |
. 2
; ;; |
83 | 1, 21 | decnncl 11518 |
. . 3
; |
84 | | 9nn0 11316 |
. . 3
|
85 | | 10nn 11514 |
. . 3
; |
86 | | eqid 2622 |
. . . 4
; ; |
87 | | eqid 2622 |
. . . 4
; ; |
88 | | 9cn 11108 |
. . . . . . 7
|
89 | 88 | mulid2i 10043 |
. . . . . 6
|
90 | 89, 30 | oveq12i 6662 |
. . . . 5
|
91 | | 9p3e12 11621 |
. . . . 5
; |
92 | 90, 91 | eqtri 2644 |
. . . 4
; |
93 | | 9t3e27 11664 |
. . . . . 6
; |
94 | 88, 33, 93 | mulcomli 10047 |
. . . . 5
; |
95 | 32 | addid1i 10223 |
. . . . 5
|
96 | 2, 8, 44, 94, 95 | decaddi 11579 |
. . . 4
; |
97 | 1, 17, 1, 44, 86, 87, 84, 8, 2, 92, 96 | decmac 11566 |
. . 3
; ; ;; |
98 | | 3pos 11114 |
. . . 4
|
99 | 1, 44, 21, 98 | declt 11530 |
. . 3
; ; |
100 | 83, 84, 85, 97, 99 | ndvdsi 15136 |
. 2
; ;; |
101 | 1, 4 | decnncl 11518 |
. . 3
; |
102 | | 8nn 11191 |
. . 3
|
103 | | eqid 2622 |
. . . 4
; ; |
104 | 32 | mulid2i 10043 |
. . . . . 6
|
105 | 104 | oveq1i 6660 |
. . . . 5
|
106 | 105, 52 | eqtri 2644 |
. . . 4
; |
107 | | 7t7e49 11653 |
. . . . 5
; |
108 | | 4p1e5 11154 |
. . . . 5
|
109 | | 9p8e17 11626 |
. . . . 5
; |
110 | 7, 84, 6, 107, 108, 8, 109 | decaddci 11580 |
. . . 4
; |
111 | 1, 8, 6, 103, 8, 8, 47, 106, 110 | decrmac 11577 |
. . 3
; ;; |
112 | | 8lt10 11674 |
. . . 4
; |
113 | 22, 8, 6, 112 | declti 11546 |
. . 3
; |
114 | 101, 8, 102, 111, 113 | ndvdsi 15136 |
. 2
; ;; |
115 | | 9nn 11192 |
. . . 4
|
116 | 1, 115 | decnncl 11518 |
. . 3
; |
117 | | eqid 2622 |
. . . 4
; ; |
118 | 76 | mulid2i 10043 |
. . . . . 6
|
119 | | 5p1e6 11155 |
. . . . . . 7
|
120 | 49, 70, 119 | addcomli 10228 |
. . . . . 6
|
121 | 118, 120 | oveq12i 6662 |
. . . . 5
|
122 | | 6p6e12 11602 |
. . . . 5
; |
123 | 121, 122 | eqtri 2644 |
. . . 4
; |
124 | | 9t6e54 11667 |
. . . . 5
; |
125 | | 4p3e7 11163 |
. . . . 5
|
126 | 47, 7, 17, 124, 125 | decaddi 11579 |
. . . 4
; |
127 | 1, 84, 1, 17, 117, 86, 54, 8, 47, 123, 126 | decmac 11566 |
. . 3
; ; ;; |
128 | | 3lt9 11227 |
. . . 4
|
129 | 1, 17, 115, 128 | declt 11530 |
. . 3
; ; |
130 | 116, 54, 83, 127, 129 | ndvdsi 15136 |
. 2
; ;; |
131 | 2, 21 | decnncl 11518 |
. . 3
; |
132 | | eqid 2622 |
. . . 4
; ; |
133 | | eqid 2622 |
. . . 4
; ; |
134 | | 2cn 11091 |
. . . . . . 7
|
135 | | 5t2e10 11634 |
. . . . . . 7
; |
136 | 49, 134, 135 | mulcomli 10047 |
. . . . . 6
; |
137 | 136, 73 | oveq12i 6662 |
. . . . 5
; |
138 | | dec10p 11553 |
. . . . 5
; ; |
139 | 137, 138 | eqtri 2644 |
. . . 4
; |
140 | | 5t3e15 11635 |
. . . . . 6
; |
141 | 49, 33, 140 | mulcomli 10047 |
. . . . 5
; |
142 | 1, 47, 2, 141, 41 | decaddi 11579 |
. . . 4
; |
143 | 2, 17, 1, 2, 132, 133, 47, 8, 1, 139, 142 | decmac 11566 |
. . 3
; ; ;; |
144 | | 1lt2 11194 |
. . . 4
|
145 | 1, 2, 2, 17, 10, 144 | decltc 11532 |
. . 3
; ; |
146 | 131, 47, 14, 143, 145 | ndvdsi 15136 |
. 2
; ;; |
147 | 5, 12, 16, 20, 39, 42, 62, 82, 100, 114, 130, 146 | prmlem2 15827 |
1
;; |