Proof of Theorem 37prm
Step | Hyp | Ref
| Expression |
1 | | 3nn0 11310 |
. . 3
|
2 | | 7nn 11190 |
. . 3
|
3 | 1, 2 | decnncl 11518 |
. 2
; |
4 | | 8nn0 11315 |
. . . 4
|
5 | | 4nn0 11311 |
. . . 4
|
6 | 4, 5 | deccl 11512 |
. . 3
; |
7 | | 7nn0 11314 |
. . 3
|
8 | | 1nn0 11308 |
. . 3
|
9 | | 7lt10 11675 |
. . 3
; |
10 | | 8nn 11191 |
. . . 4
|
11 | | 3lt10 11679 |
. . . 4
; |
12 | 10, 5, 1, 11 | declti 11546 |
. . 3
; |
13 | 1, 6, 7, 8, 9, 12 | decltc 11532 |
. 2
; ;; |
14 | | 3nn 11186 |
. . 3
|
15 | | 1lt10 11681 |
. . 3
; |
16 | 14, 7, 8, 15 | declti 11546 |
. 2
; |
17 | | 3t2e6 11179 |
. . 3
|
18 | | df-7 11084 |
. . 3
|
19 | 1, 1, 17, 18 | dec2dvds 15767 |
. 2
; |
20 | | 2nn0 11309 |
. . . 4
|
21 | 8, 20 | deccl 11512 |
. . 3
; |
22 | | 1nn 11031 |
. . 3
|
23 | | 6nn0 11313 |
. . . 4
|
24 | | 6p1e7 11156 |
. . . 4
|
25 | | eqid 2622 |
. . . . 5
; ; |
26 | | 0nn0 11307 |
. . . . 5
|
27 | | 3cn 11095 |
. . . . . . . 8
|
28 | 27 | mulid1i 10042 |
. . . . . . 7
|
29 | 28 | oveq1i 6660 |
. . . . . 6
|
30 | 27 | addid1i 10223 |
. . . . . 6
|
31 | 29, 30 | eqtri 2644 |
. . . . 5
|
32 | 23 | dec0h 11522 |
. . . . . 6
; |
33 | 17, 32 | eqtri 2644 |
. . . . 5
; |
34 | 1, 8, 20, 25, 23, 26, 31, 33 | decmul2c 11589 |
. . . 4
; ; |
35 | 1, 23, 24, 34 | decsuc 11535 |
. . 3
; ; |
36 | | 1lt3 11196 |
. . 3
|
37 | 14, 21, 22, 35, 36 | ndvdsi 15136 |
. 2
; |
38 | | 2nn 11185 |
. . 3
|
39 | | 2lt5 11202 |
. . 3
|
40 | | 5p2e7 11165 |
. . 3
|
41 | 1, 38, 39, 40 | dec5dvds2 15769 |
. 2
; |
42 | | 5nn0 11312 |
. . 3
|
43 | | 7t5e35 11651 |
. . . 4
; |
44 | 1, 42, 20, 43, 40 | decaddi 11579 |
. . 3
; |
45 | | 2lt7 11213 |
. . 3
|
46 | 2, 42, 38, 44, 45 | ndvdsi 15136 |
. 2
; |
47 | 8, 22 | decnncl 11518 |
. . 3
; |
48 | | 4nn 11187 |
. . 3
|
49 | | eqid 2622 |
. . . 4
; ; |
50 | 27 | mulid2i 10043 |
. . . 4
|
51 | 50 | oveq1i 6660 |
. . . . 5
|
52 | 48 | nncni 11030 |
. . . . . 6
|
53 | | 4p3e7 11163 |
. . . . . 6
|
54 | 52, 27, 53 | addcomli 10228 |
. . . . 5
|
55 | 51, 54 | eqtri 2644 |
. . . 4
|
56 | 8, 8, 5, 49, 1, 50, 55 | decrmanc 11576 |
. . 3
; ; |
57 | | 4lt10 11678 |
. . . 4
; |
58 | 22, 8, 5, 57 | declti 11546 |
. . 3
; |
59 | 47, 1, 48, 56, 58 | ndvdsi 15136 |
. 2
; ; |
60 | 8, 14 | decnncl 11518 |
. . 3
; |
61 | | eqid 2622 |
. . . . 5
; ; |
62 | | 2cn 11091 |
. . . . . 6
|
63 | 62 | mulid2i 10043 |
. . . . 5
|
64 | 20, 8, 1, 61, 23, 63, 17 | decmul1 11585 |
. . . 4
; ; |
65 | | 2p1e3 11151 |
. . . 4
|
66 | 20, 23, 8, 8, 64, 49, 65, 24 | decadd 11570 |
. . 3
; ; ; |
67 | 8, 8, 14, 36 | declt 11530 |
. . 3
; ; |
68 | 60, 20, 47, 66, 67 | ndvdsi 15136 |
. 2
; ; |
69 | 8, 2 | decnncl 11518 |
. . 3
; |
70 | | eqid 2622 |
. . . 4
; ; |
71 | 1 | dec0h 11522 |
. . . 4
; |
72 | | 0p1e1 11132 |
. . . . . 6
|
73 | 63, 72 | oveq12i 6662 |
. . . . 5
|
74 | 73, 65 | eqtri 2644 |
. . . 4
|
75 | | 7t2e14 11648 |
. . . . 5
; |
76 | 8, 5, 1, 75, 53 | decaddi 11579 |
. . . 4
; |
77 | 8, 7, 26, 1, 70, 71, 20, 7, 8, 74, 76 | decmac 11566 |
. . 3
; ; |
78 | 22, 7, 1, 11 | declti 11546 |
. . 3
; |
79 | 69, 20, 14, 77, 78 | ndvdsi 15136 |
. 2
; ; |
80 | | 9nn 11192 |
. . . 4
|
81 | 8, 80 | decnncl 11518 |
. . 3
; |
82 | 8, 10 | decnncl 11518 |
. . 3
; |
83 | | 9nn0 11316 |
. . . 4
|
84 | 81 | nncni 11030 |
. . . . 5
; |
85 | 84 | mulid1i 10042 |
. . . 4
; ; |
86 | | eqid 2622 |
. . . 4
; ; |
87 | | 1p1e2 11134 |
. . . . . 6
|
88 | 87 | oveq1i 6660 |
. . . . 5
|
89 | 88, 65 | eqtri 2644 |
. . . 4
|
90 | | 9p8e17 11626 |
. . . 4
; |
91 | 8, 83, 8, 4, 85, 86, 89, 7, 90 | decaddc 11572 |
. . 3
; ; ; |
92 | | 8lt9 11222 |
. . . 4
|
93 | 8, 4, 80, 92 | declt 11530 |
. . 3
; ; |
94 | 81, 8, 82, 91, 93 | ndvdsi 15136 |
. 2
; ; |
95 | 20, 14 | decnncl 11518 |
. . 3
; |
96 | 8, 48 | decnncl 11518 |
. . 3
; |
97 | 95 | nncni 11030 |
. . . . 5
; |
98 | 97 | mulid1i 10042 |
. . . 4
; ; |
99 | | eqid 2622 |
. . . 4
; ; |
100 | 20, 1, 8, 5, 98, 99, 65, 54 | decadd 11570 |
. . 3
; ; ; |
101 | | 1lt2 11194 |
. . . 4
|
102 | 8, 20, 5, 1, 57, 101 | decltc 11532 |
. . 3
; ; |
103 | 95, 8, 96, 100, 102 | ndvdsi 15136 |
. 2
; ; |
104 | 3, 13, 16, 19, 37, 41, 46, 59, 68, 79, 94, 103 | prmlem2 15827 |
1
; |