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