Proof of Theorem 257prm
Step | Hyp | Ref
| Expression |
1 | | 2nn0 11309 |
. . . 4
|
2 | | 5nn0 11312 |
. . . 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 | | 1nn0 11308 |
. . 3
|
10 | | 2lt8 11220 |
. . 3
|
11 | | 5lt10 11677 |
. . 3
; |
12 | | 7lt10 11675 |
. . 3
; |
13 | 1, 6, 2, 7, 8, 9, 10, 11, 12 | 3decltc 11538 |
. 2
;; ;; |
14 | | 5nn 11188 |
. . . 4
|
15 | 1, 14 | decnncl 11518 |
. . 3
; |
16 | | 1lt10 11681 |
. . 3
; |
17 | 15, 8, 9, 16 | declti 11546 |
. 2
;; |
18 | | 3nn0 11310 |
. . 3
|
19 | | 3t2e6 11179 |
. . 3
|
20 | | df-7 11084 |
. . 3
|
21 | 3, 18, 19, 20 | dec2dvds 15767 |
. 2
;; |
22 | | 3nn 11186 |
. . . 4
|
23 | | 2nn 11185 |
. . . 4
|
24 | | 3cn 11095 |
. . . . . . 7
|
25 | 24 | mulid1i 10042 |
. . . . . 6
|
26 | 25 | oveq1i 6660 |
. . . . 5
|
27 | | 3p2e5 11160 |
. . . . 5
|
28 | 26, 27 | eqtri 2644 |
. . . 4
|
29 | | 2lt3 11195 |
. . . 4
|
30 | 22, 9, 23, 28, 29 | ndvdsi 15136 |
. . 3
|
31 | 1, 2, 8 | 3dvds2dec 15056 |
. . . 4
;; |
32 | | 5cn 11100 |
. . . . . . . 8
|
33 | | 2cn 11091 |
. . . . . . . 8
|
34 | | 5p2e7 11165 |
. . . . . . . 8
|
35 | 32, 33, 34 | addcomli 10228 |
. . . . . . 7
|
36 | 35 | oveq1i 6660 |
. . . . . 6
|
37 | | 7p7e14 11609 |
. . . . . 6
; |
38 | 36, 37 | eqtri 2644 |
. . . . 5
; |
39 | 38 | breq2i 4661 |
. . . 4
; |
40 | 9, 7 | 3dvdsdec 15054 |
. . . . 5
; |
41 | | 4cn 11098 |
. . . . . . 7
|
42 | | ax-1cn 9994 |
. . . . . . 7
|
43 | | 4p1e5 11154 |
. . . . . . 7
|
44 | 41, 42, 43 | addcomli 10228 |
. . . . . 6
|
45 | 44 | breq2i 4661 |
. . . . 5
|
46 | 40, 45 | bitri 264 |
. . . 4
; |
47 | 31, 39, 46 | 3bitri 286 |
. . 3
;; |
48 | 30, 47 | mtbir 313 |
. 2
;; |
49 | | 2lt5 11202 |
. . 3
|
50 | 3, 23, 49, 34 | dec5dvds2 15769 |
. 2
;; |
51 | | 6nn0 11313 |
. . . 4
|
52 | 18, 51 | deccl 11512 |
. . 3
; |
53 | | eqid 2622 |
. . . . 5
; ; |
54 | | 7t3e21 11649 |
. . . . . 6
; |
55 | 1, 9, 7, 54, 44 | decaddi 11579 |
. . . . 5
; |
56 | | 7t6e42 11652 |
. . . . 5
; |
57 | 8, 18, 51, 53, 1, 7, 55, 56 | decmul2c 11589 |
. . . 4
; ;; |
58 | 3, 1, 2, 57, 35 | decaddi 11579 |
. . 3
; ;; |
59 | | 5lt7 11210 |
. . 3
|
60 | 4, 52, 14, 58, 59 | ndvdsi 15136 |
. 2
;; |
61 | | 1nn 11031 |
. . . 4
|
62 | 9, 61 | decnncl 11518 |
. . 3
; |
63 | 1, 18 | deccl 11512 |
. . 3
; |
64 | | 4nn 11187 |
. . 3
|
65 | 9, 9 | deccl 11512 |
. . . . 5
; |
66 | | eqid 2622 |
. . . . 5
; ; |
67 | 65 | nn0cni 11304 |
. . . . . . . 8
; |
68 | 67, 33 | mulcomi 10046 |
. . . . . . 7
; ; |
69 | 68 | oveq1i 6660 |
. . . . . 6
; ; |
70 | 1 | 11multnc 11592 |
. . . . . . 7
; ; |
71 | 24, 33, 27 | addcomli 10228 |
. . . . . . 7
|
72 | 1, 1, 18, 70, 71 | decaddi 11579 |
. . . . . 6
; ; |
73 | 69, 72 | eqtri 2644 |
. . . . 5
; ; |
74 | 18 | 11multnc 11592 |
. . . . . 6
; ; |
75 | 24, 67, 74 | mulcomli 10047 |
. . . . 5
; ; |
76 | 65, 1, 18, 66, 18, 18, 73, 75 | decmul2c 11589 |
. . . 4
; ; ;; |
77 | | 4p3e7 11163 |
. . . . 5
|
78 | 41, 24, 77 | addcomli 10228 |
. . . 4
|
79 | 3, 18, 7, 76, 78 | decaddi 11579 |
. . 3
; ; ;; |
80 | | 4lt10 11678 |
. . . 4
; |
81 | 61, 9, 7, 80 | declti 11546 |
. . 3
; |
82 | 62, 63, 64, 79, 81 | ndvdsi 15136 |
. 2
; ;; |
83 | 9, 22 | decnncl 11518 |
. . 3
; |
84 | | 9nn0 11316 |
. . . 4
|
85 | 9, 84 | deccl 11512 |
. . 3
; |
86 | | 10nn 11514 |
. . 3
; |
87 | 9, 18 | deccl 11512 |
. . . . . . 7
; |
88 | 87 | nn0cni 11304 |
. . . . . 6
; |
89 | 85 | nn0cni 11304 |
. . . . . 6
; |
90 | 88, 89 | mulcomi 10046 |
. . . . 5
; ; ; ; |
91 | 90 | oveq1i 6660 |
. . . 4
; ; ; ; ; ; |
92 | | 0nn0 11307 |
. . . . 5
|
93 | | eqid 2622 |
. . . . 5
; ; |
94 | | eqid 2622 |
. . . . 5
; ; |
95 | 88 | mulid2i 10043 |
. . . . . 6
; ; |
96 | | 1p1e2 11134 |
. . . . . . . 8
|
97 | | eqid 2622 |
. . . . . . . 8
; ; |
98 | 9, 9, 96, 97 | decsuc 11535 |
. . . . . . 7
; ; |
99 | 67, 42, 98 | addcomli 10228 |
. . . . . 6
; ; |
100 | 9, 18, 9, 1, 95, 99, 96, 27 | decadd 11570 |
. . . . 5
; ; ; |
101 | | eqid 2622 |
. . . . . . . 8
; ; |
102 | | 9cn 11108 |
. . . . . . . . . . 11
|
103 | 102 | mulid1i 10042 |
. . . . . . . . . 10
|
104 | 103 | oveq1i 6660 |
. . . . . . . . 9
|
105 | | 9p2e11 11619 |
. . . . . . . . 9
; |
106 | 104, 105 | eqtri 2644 |
. . . . . . . 8
; |
107 | | 9t3e27 11664 |
. . . . . . . 8
; |
108 | 84, 9, 18, 101, 8, 1, 106, 107 | decmul2c 11589 |
. . . . . . 7
; ;; |
109 | 108 | oveq1i 6660 |
. . . . . 6
; ;; |
110 | 65, 8 | deccl 11512 |
. . . . . . . 8
;; |
111 | 110 | nn0cni 11304 |
. . . . . . 7
;; |
112 | 111 | addid1i 10223 |
. . . . . 6
;; ;; |
113 | 109, 112 | eqtri 2644 |
. . . . 5
; ;; |
114 | 9, 84, 9, 92, 93, 94, 87, 8, 65, 100, 113 | decmac 11566 |
. . . 4
; ; ; ;; |
115 | 91, 114 | eqtri 2644 |
. . 3
; ; ; ;; |
116 | | 3pos 11114 |
. . . 4
|
117 | 9, 92, 22, 116 | declt 11530 |
. . 3
; ; |
118 | 83, 85, 86, 115, 117 | ndvdsi 15136 |
. 2
; ;; |
119 | 9, 4 | decnncl 11518 |
. . 3
; |
120 | 9, 2 | deccl 11512 |
. . 3
; |
121 | 9, 8 | deccl 11512 |
. . . . 5
; |
122 | | eqid 2622 |
. . . . 5
; ; |
123 | 121 | nn0cni 11304 |
. . . . . . 7
; |
124 | 123 | mulid1i 10042 |
. . . . . 6
; ; |
125 | | 8cn 11106 |
. . . . . . 7
|
126 | | 7cn 11104 |
. . . . . . 7
|
127 | | 8p7e15 11617 |
. . . . . . 7
; |
128 | 125, 126,
127 | addcomli 10228 |
. . . . . 6
; |
129 | 9, 8, 6, 124, 96, 2, 128 | decaddci 11580 |
. . . . 5
; ; |
130 | | eqid 2622 |
. . . . . 6
; ; |
131 | 32 | mulid2i 10043 |
. . . . . . . 8
|
132 | 131 | oveq1i 6660 |
. . . . . . 7
|
133 | | 5p3e8 11166 |
. . . . . . 7
|
134 | 132, 133 | eqtri 2644 |
. . . . . 6
|
135 | | 7t5e35 11651 |
. . . . . 6
; |
136 | 2, 9, 8, 130, 2, 18, 134, 135 | decmul1c 11587 |
. . . . 5
; ; |
137 | 121, 9, 2, 122, 2, 6, 129, 136 | decmul2c 11589 |
. . . 4
; ; ;; |
138 | 3, 2, 1, 137, 34 | decaddi 11579 |
. . 3
; ; ;; |
139 | | 2lt10 11680 |
. . . 4
; |
140 | 61, 8, 1, 139 | declti 11546 |
. . 3
; |
141 | 119, 120,
23, 138, 140 | ndvdsi 15136 |
. 2
; ;; |
142 | | 9nn 11192 |
. . . 4
|
143 | 9, 142 | decnncl 11518 |
. . 3
; |
144 | | 9pos 11122 |
. . . 4
|
145 | 9, 92, 142, 144 | declt 11530 |
. . 3
; ; |
146 | 143, 87, 86, 114, 145 | ndvdsi 15136 |
. 2
; ;; |
147 | 1, 22 | decnncl 11518 |
. . 3
; |
148 | 65, 1, 18, 66, 18, 18, 72, 74 | decmul1c 11587 |
. . . 4
; ; ;; |
149 | 3, 18, 7, 148, 78 | decaddi 11579 |
. . 3
; ; ;; |
150 | 23, 18, 7, 80 | declti 11546 |
. . 3
; |
151 | 147, 65, 64, 149, 150 | ndvdsi 15136 |
. 2
; ;; |
152 | 5, 13, 17, 21, 48, 50, 60, 82, 118, 141, 146, 151 | prmlem2 15827 |
1
;; |