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 mulid1i ( 7 · 1 ) = 7
49 5cn 5 ∈ ℂ
50 49 addid2i ( 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 mulid1i ( 1 1 · 1 ) = 1 1
70 ax-1cn 1 ∈ ℂ
71 70 addid2i ( 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 mulid2i ( 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 addid1i ( 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 mulid2i ( 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 mulid2i ( 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 ∈ ℙ