Proof of Theorem 83prm
Step | Hyp | Ref
| Expression |
1 | | 8nn0 11315 |
. . 3
|
2 | | 3nn 11186 |
. . 3
|
3 | 1, 2 | decnncl 11518 |
. 2
; |
4 | | 4nn0 11311 |
. . . 4
|
5 | 1, 4 | deccl 11512 |
. . 3
; |
6 | | 3nn0 11310 |
. . 3
|
7 | | 1nn0 11308 |
. . 3
|
8 | | 3lt10 11679 |
. . 3
; |
9 | | 8nn 11191 |
. . . 4
|
10 | | 8lt10 11674 |
. . . 4
; |
11 | 9, 4, 1, 10 | declti 11546 |
. . 3
; |
12 | 1, 5, 6, 7, 8, 11 | decltc 11532 |
. 2
; ;; |
13 | | 1lt10 11681 |
. . 3
; |
14 | 9, 6, 7, 13 | declti 11546 |
. 2
; |
15 | | 2cn 11091 |
. . . 4
|
16 | 15 | mulid2i 10043 |
. . 3
|
17 | | df-3 11080 |
. . 3
|
18 | 1, 7, 16, 17 | dec2dvds 15767 |
. 2
; |
19 | | 2nn0 11309 |
. . . 4
|
20 | | 7nn0 11314 |
. . . 4
|
21 | 19, 20 | deccl 11512 |
. . 3
; |
22 | | 2nn 11185 |
. . 3
|
23 | | 0nn0 11307 |
. . . 4
|
24 | | eqid 2622 |
. . . 4
; ; |
25 | 19 | dec0h 11522 |
. . . 4
; |
26 | | 3t2e6 11179 |
. . . . . 6
|
27 | 15 | addid2i 10224 |
. . . . . 6
|
28 | 26, 27 | oveq12i 6662 |
. . . . 5
|
29 | | 6p2e8 11169 |
. . . . 5
|
30 | 28, 29 | eqtri 2644 |
. . . 4
|
31 | 20 | nn0cni 11304 |
. . . . . 6
|
32 | | 3cn 11095 |
. . . . . 6
|
33 | | 7t3e21 11649 |
. . . . . 6
; |
34 | 31, 32, 33 | mulcomli 10047 |
. . . . 5
; |
35 | | 1p2e3 11152 |
. . . . 5
|
36 | 19, 7, 19, 34, 35 | decaddi 11579 |
. . . 4
; |
37 | 19, 20, 23, 19, 24, 25, 6, 6, 19, 30, 36 | decma2c 11568 |
. . 3
; ; |
38 | | 2lt3 11195 |
. . 3
|
39 | 2, 21, 22, 37, 38 | ndvdsi 15136 |
. 2
; |
40 | | 3lt5 11201 |
. . 3
|
41 | 1, 2, 40 | dec5dvds 15768 |
. 2
; |
42 | | 7nn 11190 |
. . 3
|
43 | 7, 7 | deccl 11512 |
. . 3
; |
44 | | 6nn 11189 |
. . 3
|
45 | 44 | nnnn0i 11300 |
. . . 4
|
46 | | eqid 2622 |
. . . 4
; ; |
47 | 45 | dec0h 11522 |
. . . 4
; |
48 | 31 | mulid1i 10042 |
. . . . . 6
|
49 | | ax-1cn 9994 |
. . . . . . 7
|
50 | 49 | addid2i 10224 |
. . . . . 6
|
51 | 48, 50 | oveq12i 6662 |
. . . . 5
|
52 | | 7p1e8 11157 |
. . . . 5
|
53 | 51, 52 | eqtri 2644 |
. . . 4
|
54 | 48 | oveq1i 6660 |
. . . . 5
|
55 | | 7p6e13 11608 |
. . . . 5
; |
56 | 54, 55 | eqtri 2644 |
. . . 4
; |
57 | 7, 7, 23, 45, 46, 47, 20, 6, 7, 53, 56 | decma2c 11568 |
. . 3
; ; |
58 | | 6lt7 11209 |
. . 3
|
59 | 42, 43, 44, 57, 58 | ndvdsi 15136 |
. 2
; |
60 | | 1nn 11031 |
. . . 4
|
61 | 7, 60 | decnncl 11518 |
. . 3
; |
62 | 61 | nncni 11030 |
. . . . . 6
; |
63 | 62, 31 | mulcomi 10046 |
. . . . 5
; ; |
64 | 63 | oveq1i 6660 |
. . . 4
; ; |
65 | 64, 57 | eqtri 2644 |
. . 3
; ; |
66 | | 6lt10 11676 |
. . . 4
; |
67 | 60, 7, 45, 66 | declti 11546 |
. . 3
; |
68 | 61, 20, 44, 65, 67 | ndvdsi 15136 |
. 2
; ; |
69 | 7, 2 | decnncl 11518 |
. . 3
; |
70 | | 5nn 11188 |
. . 3
|
71 | 70 | nnnn0i 11300 |
. . . 4
|
72 | | eqid 2622 |
. . . 4
; ; |
73 | 71 | dec0h 11522 |
. . . 4
; |
74 | | 6cn 11102 |
. . . . . . 7
|
75 | 74 | mulid2i 10043 |
. . . . . 6
|
76 | 75, 27 | oveq12i 6662 |
. . . . 5
|
77 | 76, 29 | eqtri 2644 |
. . . 4
|
78 | | 6t3e18 11642 |
. . . . . 6
; |
79 | 74, 32, 78 | mulcomli 10047 |
. . . . 5
; |
80 | | 1p1e2 11134 |
. . . . 5
|
81 | | 8p5e13 11615 |
. . . . 5
; |
82 | 7, 1, 71, 79, 80, 6, 81 | decaddci 11580 |
. . . 4
; |
83 | 7, 6, 23, 71, 72, 73, 45, 6, 19, 77, 82 | decmac 11566 |
. . 3
; ; |
84 | | 5lt10 11677 |
. . . 4
; |
85 | 60, 6, 71, 84 | declti 11546 |
. . 3
; |
86 | 69, 45, 70, 83, 85 | ndvdsi 15136 |
. 2
; ; |
87 | 7, 42 | decnncl 11518 |
. . 3
; |
88 | 7, 70 | decnncl 11518 |
. . 3
; |
89 | | eqid 2622 |
. . . 4
; ; |
90 | | eqid 2622 |
. . . 4
; ; |
91 | 4 | nn0cni 11304 |
. . . . . . 7
|
92 | 91 | mulid2i 10043 |
. . . . . 6
|
93 | | 3p1e4 11153 |
. . . . . . 7
|
94 | 32, 49, 93 | addcomli 10228 |
. . . . . 6
|
95 | 92, 94 | oveq12i 6662 |
. . . . 5
|
96 | | 4p4e8 11164 |
. . . . 5
|
97 | 95, 96 | eqtri 2644 |
. . . 4
|
98 | | 7t4e28 11650 |
. . . . 5
; |
99 | | 2p1e3 11151 |
. . . . 5
|
100 | 19, 1, 71, 98, 99, 6, 81 | decaddci 11580 |
. . . 4
; |
101 | 7, 20, 7, 71, 89, 90, 4, 6, 6,
97, 100 | decmac 11566 |
. . 3
; ; ; |
102 | | 5lt7 11210 |
. . . 4
|
103 | 7, 71, 42, 102 | declt 11530 |
. . 3
; ; |
104 | 87, 4, 88, 101, 103 | ndvdsi 15136 |
. 2
; ; |
105 | | 9nn 11192 |
. . . 4
|
106 | 7, 105 | decnncl 11518 |
. . 3
; |
107 | | 9nn0 11316 |
. . . 4
|
108 | | eqid 2622 |
. . . 4
; ; |
109 | 20 | dec0h 11522 |
. . . 4
; |
110 | 91 | addid2i 10224 |
. . . . . 6
|
111 | 92, 110 | oveq12i 6662 |
. . . . 5
|
112 | 111, 96 | eqtri 2644 |
. . . 4
|
113 | | 9t4e36 11665 |
. . . . 5
; |
114 | 31, 74, 55 | addcomli 10228 |
. . . . 5
; |
115 | 6, 45, 20, 113, 93, 6, 114 | decaddci 11580 |
. . . 4
; |
116 | 7, 107, 23, 20, 108, 109, 4, 6, 4, 112, 115 | decmac 11566 |
. . 3
; ; |
117 | | 7lt10 11675 |
. . . 4
; |
118 | 60, 107, 20, 117 | declti 11546 |
. . 3
; |
119 | 106, 4, 42, 116, 118 | ndvdsi 15136 |
. 2
; ; |
120 | 19, 2 | decnncl 11518 |
. . 3
; |
121 | | 4nn 11187 |
. . . 4
|
122 | 7, 121 | decnncl 11518 |
. . 3
; |
123 | | eqid 2622 |
. . . 4
; ; |
124 | | eqid 2622 |
. . . 4
; ; |
125 | 32, 15, 26 | mulcomli 10047 |
. . . . . 6
|
126 | 125, 80 | oveq12i 6662 |
. . . . 5
|
127 | 126, 29 | eqtri 2644 |
. . . 4
|
128 | | 3t3e9 11180 |
. . . . . 6
|
129 | 128 | oveq1i 6660 |
. . . . 5
|
130 | | 9p4e13 11622 |
. . . . 5
; |
131 | 129, 130 | eqtri 2644 |
. . . 4
; |
132 | 19, 6, 7, 4, 123, 124, 6, 6, 7, 127, 131 | decmac 11566 |
. . 3
; ; ; |
133 | | 4lt10 11678 |
. . . 4
; |
134 | | 1lt2 11194 |
. . . 4
|
135 | 7, 19, 4, 6, 133, 134 | decltc 11532 |
. . 3
; ; |
136 | 120, 6, 122, 132, 135 | ndvdsi 15136 |
. 2
; ; |
137 | 3, 12, 14, 18, 39, 41, 59, 68, 86, 104, 119, 136 | prmlem2 15827 |
1
; |