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 1 2 7 ∈ ℙ

Proof

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