Proof of Theorem 139prm
Step | Hyp | Ref
| Expression |
1 | | 1nn0 11308 |
. . . 4
|
2 | | 3nn0 11310 |
. . . 4
|
3 | 1, 2 | deccl 11512 |
. . 3
; |
4 | | 9nn 11192 |
. . 3
|
5 | 3, 4 | decnncl 11518 |
. 2
;; |
6 | | 8nn0 11315 |
. . 3
|
7 | | 4nn0 11311 |
. . 3
|
8 | | 9nn0 11316 |
. . 3
|
9 | | 1lt8 11221 |
. . 3
|
10 | | 3lt10 11679 |
. . 3
; |
11 | | 9lt10 11673 |
. . 3
; |
12 | 1, 6, 2, 7, 8, 1, 9, 10, 11 | 3decltc 11538 |
. 2
;; ;; |
13 | | 3nn 11186 |
. . . 4
|
14 | 1, 13 | decnncl 11518 |
. . 3
; |
15 | | 1lt10 11681 |
. . 3
; |
16 | 14, 8, 1, 15 | declti 11546 |
. 2
;; |
17 | | 4t2e8 11181 |
. . 3
|
18 | | df-9 11086 |
. . 3
|
19 | 3, 7, 17, 18 | dec2dvds 15767 |
. 2
;; |
20 | | 6nn0 11313 |
. . . 4
|
21 | 7, 20 | deccl 11512 |
. . 3
; |
22 | | 1nn 11031 |
. . 3
|
23 | | 0nn0 11307 |
. . . 4
|
24 | | eqid 2622 |
. . . 4
; ; |
25 | 1 | dec0h 11522 |
. . . 4
; |
26 | | ax-1cn 9994 |
. . . . . . 7
|
27 | 26 | addid2i 10224 |
. . . . . 6
|
28 | 27 | oveq2i 6661 |
. . . . 5
|
29 | | 2nn0 11309 |
. . . . . 6
|
30 | | 2p1e3 11151 |
. . . . . 6
|
31 | 7 | nn0cni 11304 |
. . . . . . 7
|
32 | | 3cn 11095 |
. . . . . . 7
|
33 | | 4t3e12 11632 |
. . . . . . 7
; |
34 | 31, 32, 33 | mulcomli 10047 |
. . . . . 6
; |
35 | 1, 29, 30, 34 | decsuc 11535 |
. . . . 5
; |
36 | 28, 35 | eqtri 2644 |
. . . 4
; |
37 | | 8p1e9 11158 |
. . . . 5
|
38 | 20 | nn0cni 11304 |
. . . . . 6
|
39 | | 6t3e18 11642 |
. . . . . 6
; |
40 | 38, 32, 39 | mulcomli 10047 |
. . . . 5
; |
41 | 1, 6, 37, 40 | decsuc 11535 |
. . . 4
; |
42 | 7, 20, 23, 1, 24, 25, 2, 8, 1,
36, 41 | decma2c 11568 |
. . 3
; ;; |
43 | | 1lt3 11196 |
. . 3
|
44 | 13, 21, 22, 42, 43 | ndvdsi 15136 |
. 2
;; |
45 | | 4nn 11187 |
. . 3
|
46 | | 4lt5 11200 |
. . 3
|
47 | | 5p4e9 11167 |
. . 3
|
48 | 3, 45, 46, 47 | dec5dvds2 15769 |
. 2
;; |
49 | | 7nn 11190 |
. . 3
|
50 | 1, 8 | deccl 11512 |
. . 3
; |
51 | | 6nn 11189 |
. . 3
|
52 | | eqid 2622 |
. . . 4
; ; |
53 | 20 | dec0h 11522 |
. . . 4
; |
54 | | 7nn0 11314 |
. . . 4
|
55 | | 7cn 11104 |
. . . . . . 7
|
56 | 55 | mulid1i 10042 |
. . . . . 6
|
57 | 38 | addid2i 10224 |
. . . . . 6
|
58 | 56, 57 | oveq12i 6662 |
. . . . 5
|
59 | | 7p6e13 11608 |
. . . . 5
; |
60 | 58, 59 | eqtri 2644 |
. . . 4
; |
61 | | 9cn 11108 |
. . . . . 6
|
62 | | 9t7e63 11668 |
. . . . . 6
; |
63 | 61, 55, 62 | mulcomli 10047 |
. . . . 5
; |
64 | | 6p3e9 11170 |
. . . . . 6
|
65 | 38, 32, 64 | addcomli 10228 |
. . . . 5
|
66 | 20, 2, 20, 63, 65 | decaddi 11579 |
. . . 4
; |
67 | 1, 8, 23, 20, 52, 53, 54, 8, 20, 60, 66 | decma2c 11568 |
. . 3
; ;; |
68 | | 6lt7 11209 |
. . 3
|
69 | 49, 50, 51, 67, 68 | ndvdsi 15136 |
. 2
;; |
70 | 1, 22 | decnncl 11518 |
. . 3
; |
71 | 1, 29 | deccl 11512 |
. . 3
; |
72 | | eqid 2622 |
. . . 4
; ; |
73 | 54 | dec0h 11522 |
. . . 4
; |
74 | 1, 1 | deccl 11512 |
. . . 4
; |
75 | | 2cn 11091 |
. . . . . . 7
|
76 | 75 | addid2i 10224 |
. . . . . 6
|
77 | 76 | oveq2i 6661 |
. . . . 5
; ; |
78 | 70 | nncni 11030 |
. . . . . . 7
; |
79 | 78 | mulid1i 10042 |
. . . . . 6
; ; |
80 | | 1p2e3 11152 |
. . . . . 6
|
81 | 1, 1, 29, 79, 80 | decaddi 11579 |
. . . . 5
; ; |
82 | 77, 81 | eqtri 2644 |
. . . 4
; ; |
83 | | eqid 2622 |
. . . . 5
; ; |
84 | 75 | mulid2i 10043 |
. . . . . . 7
|
85 | | 00id 10211 |
. . . . . . 7
|
86 | 84, 85 | oveq12i 6662 |
. . . . . 6
|
87 | 75 | addid1i 10223 |
. . . . . 6
|
88 | 86, 87 | eqtri 2644 |
. . . . 5
|
89 | 84 | oveq1i 6660 |
. . . . . 6
|
90 | | 7p2e9 11172 |
. . . . . . 7
|
91 | 55, 75, 90 | addcomli 10228 |
. . . . . 6
|
92 | 8 | dec0h 11522 |
. . . . . 6
; |
93 | 89, 91, 92 | 3eqtri 2648 |
. . . . 5
; |
94 | 1, 1, 23, 54, 83, 73, 29, 8, 23, 88, 93 | decmac 11566 |
. . . 4
; ; |
95 | 1, 29, 23, 54, 72, 73, 74, 8, 29, 82, 94 | decma2c 11568 |
. . 3
; ; ;; |
96 | | 7lt10 11675 |
. . . 4
; |
97 | 22, 1, 54, 96 | declti 11546 |
. . 3
; |
98 | 70, 71, 49, 95, 97 | ndvdsi 15136 |
. 2
; ;; |
99 | | 10nn0 11516 |
. . 3
; |
100 | | eqid 2622 |
. . . 4
; ; |
101 | | eqid 2622 |
. . . . 5
; ; |
102 | 23 | dec0h 11522 |
. . . . . 6
; |
103 | 85, 102 | eqtri 2644 |
. . . . 5
; |
104 | 26 | mulid1i 10042 |
. . . . . . 7
|
105 | 104, 85 | oveq12i 6662 |
. . . . . 6
|
106 | 26 | addid1i 10223 |
. . . . . 6
|
107 | 105, 106 | eqtri 2644 |
. . . . 5
|
108 | 32 | mulid1i 10042 |
. . . . . . 7
|
109 | 108 | oveq1i 6660 |
. . . . . 6
|
110 | 32 | addid1i 10223 |
. . . . . 6
|
111 | 2 | dec0h 11522 |
. . . . . 6
; |
112 | 109, 110,
111 | 3eqtri 2648 |
. . . . 5
; |
113 | 1, 2, 23, 23, 101, 103, 1, 2, 23, 107, 112 | decmac 11566 |
. . . 4
; ; |
114 | 3 | nn0cni 11304 |
. . . . . . 7
; |
115 | 114 | mul01i 10226 |
. . . . . 6
; |
116 | 115 | oveq1i 6660 |
. . . . 5
; |
117 | 61 | addid2i 10224 |
. . . . 5
|
118 | 116, 117,
92 | 3eqtri 2648 |
. . . 4
; ; |
119 | 1, 23, 23, 8, 100, 92, 3, 8, 23, 113, 118 | decma2c 11568 |
. . 3
; ; ;; |
120 | 22, 2, 8, 11 | declti 11546 |
. . 3
; |
121 | 14, 99, 4, 119, 120 | ndvdsi 15136 |
. 2
; ;; |
122 | 1, 49 | decnncl 11518 |
. . 3
; |
123 | | eqid 2622 |
. . . 4
; ; |
124 | | 5nn0 11312 |
. . . 4
|
125 | | 8cn 11106 |
. . . . . . 7
|
126 | 125 | mulid2i 10043 |
. . . . . 6
|
127 | | 5cn 11100 |
. . . . . . 7
|
128 | 127 | addid2i 10224 |
. . . . . 6
|
129 | 126, 128 | oveq12i 6662 |
. . . . 5
|
130 | | 8p5e13 11615 |
. . . . 5
; |
131 | 129, 130 | eqtri 2644 |
. . . 4
; |
132 | | 8t7e56 11661 |
. . . . . 6
; |
133 | 125, 55, 132 | mulcomli 10047 |
. . . . 5
; |
134 | 124, 20, 2, 133, 64 | decaddi 11579 |
. . . 4
; |
135 | 1, 54, 23, 2, 123, 111, 6, 8, 124, 131, 134 | decmac 11566 |
. . 3
; ;; |
136 | 22, 54, 2, 10 | declti 11546 |
. . 3
; |
137 | 122, 6, 13, 135, 136 | ndvdsi 15136 |
. 2
; ;; |
138 | 1, 4 | decnncl 11518 |
. . 3
; |
139 | 55 | mulid2i 10043 |
. . . . . 6
|
140 | 139, 57 | oveq12i 6662 |
. . . . 5
|
141 | 140, 59 | eqtri 2644 |
. . . 4
; |
142 | 20, 2, 20, 62, 65 | decaddi 11579 |
. . . 4
; |
143 | 1, 8, 23, 20, 52, 53, 54, 8, 20, 141, 142 | decmac 11566 |
. . 3
; ;; |
144 | | 6lt10 11676 |
. . . 4
; |
145 | 22, 8, 20, 144 | declti 11546 |
. . 3
; |
146 | 138, 54, 51, 143, 145 | ndvdsi 15136 |
. 2
; ;; |
147 | 29, 13 | decnncl 11518 |
. . 3
; |
148 | | eqid 2622 |
. . . 4
; ; |
149 | | 6t2e12 11641 |
. . . . . 6
; |
150 | 38, 75, 149 | mulcomli 10047 |
. . . . 5
; |
151 | 1, 29, 30, 150 | decsuc 11535 |
. . . 4
; |
152 | 29, 2, 1, 148, 20, 8, 1, 151, 41 | decrmac 11577 |
. . 3
; ;; |
153 | | 2nn 11185 |
. . . 4
|
154 | 153, 2, 1, 15 | declti 11546 |
. . 3
; |
155 | 147, 20, 22, 152, 154 | ndvdsi 15136 |
. 2
; ;; |
156 | 5, 12, 16, 19, 44, 48, 69, 98, 121, 137, 146, 155 | prmlem2 15827 |
1
;; |