Metamath Proof Explorer


Theorem 127prm

Description: 127 is a prime number. (Contributed by AV, 16-Aug-2021) (Proof shortened by AV, 16-Sep-2021)

Ref Expression
Assertion 127prm 127

Proof

Step Hyp Ref Expression
1 1nn0 10
2 2nn0 20
3 1 2 deccl 120
4 7nn 7
5 3 4 decnncl 127
6 8nn0 80
7 4nn0 40
8 7nn0 70
9 1lt8 1<8
10 2lt10 2<10
11 7lt10 7<10
12 1 6 2 7 8 1 9 10 11 3decltc 127<841
13 2nn 2
14 1 13 decnncl 12
15 1lt10 1<10
16 14 8 1 15 declti 1<127
17 3nn0 30
18 3t2e6 32=6
19 df-7 7=6+1
20 3 17 18 19 dec2dvds ¬2127
21 3nn 3
22 1nn 1
23 3t3e9 33=9
24 23 oveq1i 33+1=9+1
25 9p1e10 9+1=10
26 24 25 eqtri 33+1=10
27 1lt3 1<3
28 21 17 22 26 27 ndvdsi ¬310
29 1 2 8 3dvds2dec 312731+2+7
30 1p2e3 1+2=3
31 30 oveq1i 1+2+7=3+7
32 7cn 7
33 3cn 3
34 7p3e10 7+3=10
35 32 33 34 addcomli 3+7=10
36 31 35 eqtri 1+2+7=10
37 36 breq2i 31+2+7310
38 29 37 bitri 3127310
39 28 38 mtbir ¬3127
40 2lt5 2<5
41 5p2e7 5+2=7
42 3 13 40 41 dec5dvds2 ¬5127
43 1 6 deccl 180
44 0nn0 00
45 eqid 18=18
46 1 dec0h 1=01
47 5nn0 50
48 32 mulid1i 71=7
49 5cn 5
50 49 addid2i 0+5=5
51 48 50 oveq12i 71+0+5=7+5
52 7p5e12 7+5=12
53 51 52 eqtri 71+0+5=12
54 6nn0 60
55 8cn 8
56 8t7e56 87=56
57 55 32 56 mulcomli 78=56
58 6p1e7 6+1=7
59 47 54 1 57 58 decaddi 78+1=57
60 1 6 44 1 45 46 8 8 47 53 59 decma2c 718+1=127
61 1lt7 1<7
62 4 43 22 60 61 ndvdsi ¬7127
63 1 22 decnncl 11
64 1 1 deccl 110
65 6nn 6
66 eqid 11=11
67 54 dec0h 6=06
68 64 nn0cni 11
69 68 mulid1i 111=11
70 ax-1cn 1
71 70 addid2i 0+1=1
72 69 71 oveq12i 111+0+1=11+1
73 1p1e2 1+1=2
74 1 1 1 66 73 decaddi 11+1=12
75 72 74 eqtri 111+0+1=12
76 6cn 6
77 76 70 58 addcomli 1+6=7
78 1 1 54 69 77 decaddi 111+6=17
79 1 1 44 54 66 67 64 8 1 75 78 decma2c 1111+6=127
80 6lt10 6<10
81 22 1 54 80 declti 6<11
82 63 64 65 79 81 ndvdsi ¬11127
83 1 21 decnncl 13
84 9nn0 90
85 10nn 10
86 eqid 13=13
87 eqid 10=10
88 9cn 9
89 88 mulid2i 19=9
90 89 30 oveq12i 19+1+2=9+3
91 9p3e12 9+3=12
92 90 91 eqtri 19+1+2=12
93 9t3e27 93=27
94 88 33 93 mulcomli 39=27
95 32 addid1i 7+0=7
96 2 8 44 94 95 decaddi 39+0=27
97 1 17 1 44 86 87 84 8 2 92 96 decmac 139+10=127
98 3pos 0<3
99 1 44 21 98 declt 10<13
100 83 84 85 97 99 ndvdsi ¬13127
101 1 4 decnncl 17
102 8nn 8
103 eqid 17=17
104 32 mulid2i 17=7
105 104 oveq1i 17+5=7+5
106 105 52 eqtri 17+5=12
107 7t7e49 77=49
108 4p1e5 4+1=5
109 9p8e17 9+8=17
110 7 84 6 107 108 8 109 decaddci 77+8=57
111 1 8 6 103 8 8 47 106 110 decrmac 177+8=127
112 8lt10 8<10
113 22 8 6 112 declti 8<17
114 101 8 102 111 113 ndvdsi ¬17127
115 9nn 9
116 1 115 decnncl 19
117 eqid 19=19
118 76 mulid2i 16=6
119 5p1e6 5+1=6
120 49 70 119 addcomli 1+5=6
121 118 120 oveq12i 16+1+5=6+6
122 6p6e12 6+6=12
123 121 122 eqtri 16+1+5=12
124 9t6e54 96=54
125 4p3e7 4+3=7
126 47 7 17 124 125 decaddi 96+3=57
127 1 84 1 17 117 86 54 8 47 123 126 decmac 196+13=127
128 3lt9 3<9
129 1 17 115 128 declt 13<19
130 116 54 83 127 129 ndvdsi ¬19127
131 2 21 decnncl 23
132 eqid 23=23
133 eqid 12=12
134 2cn 2
135 5t2e10 52=10
136 49 134 135 mulcomli 25=10
137 136 73 oveq12i 25+1+1=10+2
138 dec10p 10+2=12
139 137 138 eqtri 25+1+1=12
140 5t3e15 53=15
141 49 33 140 mulcomli 35=15
142 1 47 2 141 41 decaddi 35+2=17
143 2 17 1 2 132 133 47 8 1 139 142 decmac 235+12=127
144 1lt2 1<2
145 1 2 2 17 10 144 decltc 12<23
146 131 47 14 143 145 ndvdsi ¬23127
147 5 12 16 20 39 42 62 82 100 114 130 146 prmlem2 127