Description: 139 is a prime number. In contrast to 139prm , the proof of this theorem uses 3dvds2dec for checking the divisibility by 3. Although the proof using 3dvds2dec is longer (regarding size: 1849 characters compared with 1809 for 139prm ), the number of essential steps is smaller (301 compared with 327 for 139prm ). (Contributed by Mario Carneiro, 19-Feb-2014) (Revised by AV, 18-Aug-2021) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | 139prmALT | ⊢ ; ; 1 3 9 ∈ ℙ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nn0 | ⊢ 1 ∈ ℕ0 | |
2 | 3nn0 | ⊢ 3 ∈ ℕ0 | |
3 | 1 2 | deccl | ⊢ ; 1 3 ∈ ℕ0 |
4 | 9nn | ⊢ 9 ∈ ℕ | |
5 | 3 4 | decnncl | ⊢ ; ; 1 3 9 ∈ ℕ |
6 | 8nn0 | ⊢ 8 ∈ ℕ0 | |
7 | 4nn0 | ⊢ 4 ∈ ℕ0 | |
8 | 9nn0 | ⊢ 9 ∈ ℕ0 | |
9 | 1lt8 | ⊢ 1 < 8 | |
10 | 3lt10 | ⊢ 3 < ; 1 0 | |
11 | 9lt10 | ⊢ 9 < ; 1 0 | |
12 | 1 6 2 7 8 1 9 10 11 | 3decltc | ⊢ ; ; 1 3 9 < ; ; 8 4 1 |
13 | 3nn | ⊢ 3 ∈ ℕ | |
14 | 1 13 | decnncl | ⊢ ; 1 3 ∈ ℕ |
15 | 1lt10 | ⊢ 1 < ; 1 0 | |
16 | 14 8 1 15 | declti | ⊢ 1 < ; ; 1 3 9 |
17 | 4t2e8 | ⊢ ( 4 · 2 ) = 8 | |
18 | df-9 | ⊢ 9 = ( 8 + 1 ) | |
19 | 3 7 17 18 | dec2dvds | ⊢ ¬ 2 ∥ ; ; 1 3 9 |
20 | 3ndvds4 | ⊢ ¬ 3 ∥ 4 | |
21 | 1 2 | 3dvdsdec | ⊢ ( 3 ∥ ; 1 3 ↔ 3 ∥ ( 1 + 3 ) ) |
22 | 3cn | ⊢ 3 ∈ ℂ | |
23 | ax-1cn | ⊢ 1 ∈ ℂ | |
24 | 3p1e4 | ⊢ ( 3 + 1 ) = 4 | |
25 | 22 23 24 | addcomli | ⊢ ( 1 + 3 ) = 4 |
26 | 25 | breq2i | ⊢ ( 3 ∥ ( 1 + 3 ) ↔ 3 ∥ 4 ) |
27 | 21 26 | bitri | ⊢ ( 3 ∥ ; 1 3 ↔ 3 ∥ 4 ) |
28 | 20 27 | mtbir | ⊢ ¬ 3 ∥ ; 1 3 |
29 | 1 2 8 | 3dvds2dec | ⊢ ( 3 ∥ ; ; 1 3 9 ↔ 3 ∥ ( ( 1 + 3 ) + 9 ) ) |
30 | 25 | oveq1i | ⊢ ( ( 1 + 3 ) + 9 ) = ( 4 + 9 ) |
31 | 9cn | ⊢ 9 ∈ ℂ | |
32 | 4cn | ⊢ 4 ∈ ℂ | |
33 | 9p4e13 | ⊢ ( 9 + 4 ) = ; 1 3 | |
34 | 31 32 33 | addcomli | ⊢ ( 4 + 9 ) = ; 1 3 |
35 | 30 34 | eqtri | ⊢ ( ( 1 + 3 ) + 9 ) = ; 1 3 |
36 | 35 | breq2i | ⊢ ( 3 ∥ ( ( 1 + 3 ) + 9 ) ↔ 3 ∥ ; 1 3 ) |
37 | 29 36 | bitri | ⊢ ( 3 ∥ ; ; 1 3 9 ↔ 3 ∥ ; 1 3 ) |
38 | 28 37 | mtbir | ⊢ ¬ 3 ∥ ; ; 1 3 9 |
39 | 4nn | ⊢ 4 ∈ ℕ | |
40 | 4lt5 | ⊢ 4 < 5 | |
41 | 5p4e9 | ⊢ ( 5 + 4 ) = 9 | |
42 | 3 39 40 41 | dec5dvds2 | ⊢ ¬ 5 ∥ ; ; 1 3 9 |
43 | 7nn | ⊢ 7 ∈ ℕ | |
44 | 1 8 | deccl | ⊢ ; 1 9 ∈ ℕ0 |
45 | 6nn | ⊢ 6 ∈ ℕ | |
46 | 0nn0 | ⊢ 0 ∈ ℕ0 | |
47 | 6nn0 | ⊢ 6 ∈ ℕ0 | |
48 | eqid | ⊢ ; 1 9 = ; 1 9 | |
49 | 47 | dec0h | ⊢ 6 = ; 0 6 |
50 | 7nn0 | ⊢ 7 ∈ ℕ0 | |
51 | 7cn | ⊢ 7 ∈ ℂ | |
52 | 51 | mulid1i | ⊢ ( 7 · 1 ) = 7 |
53 | 6cn | ⊢ 6 ∈ ℂ | |
54 | 53 | addid2i | ⊢ ( 0 + 6 ) = 6 |
55 | 52 54 | oveq12i | ⊢ ( ( 7 · 1 ) + ( 0 + 6 ) ) = ( 7 + 6 ) |
56 | 7p6e13 | ⊢ ( 7 + 6 ) = ; 1 3 | |
57 | 55 56 | eqtri | ⊢ ( ( 7 · 1 ) + ( 0 + 6 ) ) = ; 1 3 |
58 | 9t7e63 | ⊢ ( 9 · 7 ) = ; 6 3 | |
59 | 31 51 58 | mulcomli | ⊢ ( 7 · 9 ) = ; 6 3 |
60 | 6p3e9 | ⊢ ( 6 + 3 ) = 9 | |
61 | 53 22 60 | addcomli | ⊢ ( 3 + 6 ) = 9 |
62 | 47 2 47 59 61 | decaddi | ⊢ ( ( 7 · 9 ) + 6 ) = ; 6 9 |
63 | 1 8 46 47 48 49 50 8 47 57 62 | decma2c | ⊢ ( ( 7 · ; 1 9 ) + 6 ) = ; ; 1 3 9 |
64 | 6lt7 | ⊢ 6 < 7 | |
65 | 43 44 45 63 64 | ndvdsi | ⊢ ¬ 7 ∥ ; ; 1 3 9 |
66 | 1nn | ⊢ 1 ∈ ℕ | |
67 | 1 66 | decnncl | ⊢ ; 1 1 ∈ ℕ |
68 | 2nn0 | ⊢ 2 ∈ ℕ0 | |
69 | 1 68 | deccl | ⊢ ; 1 2 ∈ ℕ0 |
70 | eqid | ⊢ ; 1 2 = ; 1 2 | |
71 | 50 | dec0h | ⊢ 7 = ; 0 7 |
72 | 1 1 | deccl | ⊢ ; 1 1 ∈ ℕ0 |
73 | 2cn | ⊢ 2 ∈ ℂ | |
74 | 73 | addid2i | ⊢ ( 0 + 2 ) = 2 |
75 | 74 | oveq2i | ⊢ ( ( ; 1 1 · 1 ) + ( 0 + 2 ) ) = ( ( ; 1 1 · 1 ) + 2 ) |
76 | 67 | nncni | ⊢ ; 1 1 ∈ ℂ |
77 | 76 | mulid1i | ⊢ ( ; 1 1 · 1 ) = ; 1 1 |
78 | 1p2e3 | ⊢ ( 1 + 2 ) = 3 | |
79 | 1 1 68 77 78 | decaddi | ⊢ ( ( ; 1 1 · 1 ) + 2 ) = ; 1 3 |
80 | 75 79 | eqtri | ⊢ ( ( ; 1 1 · 1 ) + ( 0 + 2 ) ) = ; 1 3 |
81 | eqid | ⊢ ; 1 1 = ; 1 1 | |
82 | 73 | mulid2i | ⊢ ( 1 · 2 ) = 2 |
83 | 00id | ⊢ ( 0 + 0 ) = 0 | |
84 | 82 83 | oveq12i | ⊢ ( ( 1 · 2 ) + ( 0 + 0 ) ) = ( 2 + 0 ) |
85 | 73 | addid1i | ⊢ ( 2 + 0 ) = 2 |
86 | 84 85 | eqtri | ⊢ ( ( 1 · 2 ) + ( 0 + 0 ) ) = 2 |
87 | 82 | oveq1i | ⊢ ( ( 1 · 2 ) + 7 ) = ( 2 + 7 ) |
88 | 7p2e9 | ⊢ ( 7 + 2 ) = 9 | |
89 | 51 73 88 | addcomli | ⊢ ( 2 + 7 ) = 9 |
90 | 8 | dec0h | ⊢ 9 = ; 0 9 |
91 | 87 89 90 | 3eqtri | ⊢ ( ( 1 · 2 ) + 7 ) = ; 0 9 |
92 | 1 1 46 50 81 71 68 8 46 86 91 | decmac | ⊢ ( ( ; 1 1 · 2 ) + 7 ) = ; 2 9 |
93 | 1 68 46 50 70 71 72 8 68 80 92 | decma2c | ⊢ ( ( ; 1 1 · ; 1 2 ) + 7 ) = ; ; 1 3 9 |
94 | 7lt10 | ⊢ 7 < ; 1 0 | |
95 | 66 1 50 94 | declti | ⊢ 7 < ; 1 1 |
96 | 67 69 43 93 95 | ndvdsi | ⊢ ¬ ; 1 1 ∥ ; ; 1 3 9 |
97 | 1 46 | deccl | ⊢ ; 1 0 ∈ ℕ0 |
98 | eqid | ⊢ ; 1 0 = ; 1 0 | |
99 | 3 | nn0cni | ⊢ ; 1 3 ∈ ℂ |
100 | 99 | mulid1i | ⊢ ( ; 1 3 · 1 ) = ; 1 3 |
101 | 100 83 | oveq12i | ⊢ ( ( ; 1 3 · 1 ) + ( 0 + 0 ) ) = ( ; 1 3 + 0 ) |
102 | 99 | addid1i | ⊢ ( ; 1 3 + 0 ) = ; 1 3 |
103 | 101 102 | eqtri | ⊢ ( ( ; 1 3 · 1 ) + ( 0 + 0 ) ) = ; 1 3 |
104 | 99 | mul01i | ⊢ ( ; 1 3 · 0 ) = 0 |
105 | 104 | oveq1i | ⊢ ( ( ; 1 3 · 0 ) + 9 ) = ( 0 + 9 ) |
106 | 31 | addid2i | ⊢ ( 0 + 9 ) = 9 |
107 | 105 106 90 | 3eqtri | ⊢ ( ( ; 1 3 · 0 ) + 9 ) = ; 0 9 |
108 | 1 46 46 8 98 90 3 8 46 103 107 | decma2c | ⊢ ( ( ; 1 3 · ; 1 0 ) + 9 ) = ; ; 1 3 9 |
109 | 66 2 8 11 | declti | ⊢ 9 < ; 1 3 |
110 | 14 97 4 108 109 | ndvdsi | ⊢ ¬ ; 1 3 ∥ ; ; 1 3 9 |
111 | 1 43 | decnncl | ⊢ ; 1 7 ∈ ℕ |
112 | eqid | ⊢ ; 1 7 = ; 1 7 | |
113 | 2 | dec0h | ⊢ 3 = ; 0 3 |
114 | 5nn0 | ⊢ 5 ∈ ℕ0 | |
115 | 8cn | ⊢ 8 ∈ ℂ | |
116 | 115 | mulid2i | ⊢ ( 1 · 8 ) = 8 |
117 | 5cn | ⊢ 5 ∈ ℂ | |
118 | 117 | addid2i | ⊢ ( 0 + 5 ) = 5 |
119 | 116 118 | oveq12i | ⊢ ( ( 1 · 8 ) + ( 0 + 5 ) ) = ( 8 + 5 ) |
120 | 8p5e13 | ⊢ ( 8 + 5 ) = ; 1 3 | |
121 | 119 120 | eqtri | ⊢ ( ( 1 · 8 ) + ( 0 + 5 ) ) = ; 1 3 |
122 | 8t7e56 | ⊢ ( 8 · 7 ) = ; 5 6 | |
123 | 115 51 122 | mulcomli | ⊢ ( 7 · 8 ) = ; 5 6 |
124 | 114 47 2 123 60 | decaddi | ⊢ ( ( 7 · 8 ) + 3 ) = ; 5 9 |
125 | 1 50 46 2 112 113 6 8 114 121 124 | decmac | ⊢ ( ( ; 1 7 · 8 ) + 3 ) = ; ; 1 3 9 |
126 | 66 50 2 10 | declti | ⊢ 3 < ; 1 7 |
127 | 111 6 13 125 126 | ndvdsi | ⊢ ¬ ; 1 7 ∥ ; ; 1 3 9 |
128 | 1 4 | decnncl | ⊢ ; 1 9 ∈ ℕ |
129 | 51 | mulid2i | ⊢ ( 1 · 7 ) = 7 |
130 | 129 54 | oveq12i | ⊢ ( ( 1 · 7 ) + ( 0 + 6 ) ) = ( 7 + 6 ) |
131 | 130 56 | eqtri | ⊢ ( ( 1 · 7 ) + ( 0 + 6 ) ) = ; 1 3 |
132 | 47 2 47 58 61 | decaddi | ⊢ ( ( 9 · 7 ) + 6 ) = ; 6 9 |
133 | 1 8 46 47 48 49 50 8 47 131 132 | decmac | ⊢ ( ( ; 1 9 · 7 ) + 6 ) = ; ; 1 3 9 |
134 | 6lt10 | ⊢ 6 < ; 1 0 | |
135 | 66 8 47 134 | declti | ⊢ 6 < ; 1 9 |
136 | 128 50 45 133 135 | ndvdsi | ⊢ ¬ ; 1 9 ∥ ; ; 1 3 9 |
137 | 68 13 | decnncl | ⊢ ; 2 3 ∈ ℕ |
138 | eqid | ⊢ ; 2 3 = ; 2 3 | |
139 | 2p1e3 | ⊢ ( 2 + 1 ) = 3 | |
140 | 6t2e12 | ⊢ ( 6 · 2 ) = ; 1 2 | |
141 | 53 73 140 | mulcomli | ⊢ ( 2 · 6 ) = ; 1 2 |
142 | 1 68 139 141 | decsuc | ⊢ ( ( 2 · 6 ) + 1 ) = ; 1 3 |
143 | 8p1e9 | ⊢ ( 8 + 1 ) = 9 | |
144 | 6t3e18 | ⊢ ( 6 · 3 ) = ; 1 8 | |
145 | 53 22 144 | mulcomli | ⊢ ( 3 · 6 ) = ; 1 8 |
146 | 1 6 143 145 | decsuc | ⊢ ( ( 3 · 6 ) + 1 ) = ; 1 9 |
147 | 68 2 1 138 47 8 1 142 146 | decrmac | ⊢ ( ( ; 2 3 · 6 ) + 1 ) = ; ; 1 3 9 |
148 | 2nn | ⊢ 2 ∈ ℕ | |
149 | 148 2 1 15 | declti | ⊢ 1 < ; 2 3 |
150 | 137 47 66 147 149 | ndvdsi | ⊢ ¬ ; 2 3 ∥ ; ; 1 3 9 |
151 | 5 12 16 19 38 42 65 96 110 127 136 150 | prmlem2 | ⊢ ; ; 1 3 9 ∈ ℙ |