Metamath Proof Explorer

Theorem 139prm

Description: 139 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 139prm 1 3 9 ∈ ℙ

Proof

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 6nn0 ⊢ 6 ∈ ℕ0
21 7 20 deccl ⊢ 4 6 ∈ ℕ0
22 1nn ⊢ 1 ∈ ℕ
23 0nn0 ⊢ 0 ∈ ℕ0
24 eqid ⊢ 4 6 = 4 6
25 1 dec0h ⊢ 1 = 0 1
26 ax-1cn ⊢ 1 ∈ ℂ
27 26 addlidi ⊢ ( 0 + 1 ) = 1
28 27 oveq2i ⊢ ( ( 3 · 4 ) + ( 0 + 1 ) ) = ( ( 3 · 4 ) + 1 )
29 2nn0 ⊢ 2 ∈ ℕ0
30 2p1e3 ⊢ ( 2 + 1 ) = 3
31 7 nn0cni ⊢ 4 ∈ ℂ
32 3cn ⊢ 3 ∈ ℂ
33 4t3e12 ⊢ ( 4 · 3 ) = 1 2
34 31 32 33 mulcomli ⊢ ( 3 · 4 ) = 1 2
35 1 29 30 34 decsuc ⊢ ( ( 3 · 4 ) + 1 ) = 1 3
36 28 35 eqtri ⊢ ( ( 3 · 4 ) + ( 0 + 1 ) ) = 1 3
37 8p1e9 ⊢ ( 8 + 1 ) = 9
38 20 nn0cni ⊢ 6 ∈ ℂ
39 6t3e18 ⊢ ( 6 · 3 ) = 1 8
40 38 32 39 mulcomli ⊢ ( 3 · 6 ) = 1 8
41 1 6 37 40 decsuc ⊢ ( ( 3 · 6 ) + 1 ) = 1 9
42 7 20 23 1 24 25 2 8 1 36 41 decma2c ⊢ ( ( 3 · 4 6 ) + 1 ) = 1 3 9
43 1lt3 ⊢ 1 < 3
44 13 21 22 42 43 ndvdsi ⊢ ¬ 3 ∥ 1 3 9
45 4nn ⊢ 4 ∈ ℕ
46 4lt5 ⊢ 4 < 5
47 5p4e9 ⊢ ( 5 + 4 ) = 9
48 3 45 46 47 dec5dvds2 ⊢ ¬ 5 ∥ 1 3 9
49 7nn ⊢ 7 ∈ ℕ
50 1 8 deccl ⊢ 1 9 ∈ ℕ0
51 6nn ⊢ 6 ∈ ℕ
52 eqid ⊢ 1 9 = 1 9
53 20 dec0h ⊢ 6 = 0 6
54 7nn0 ⊢ 7 ∈ ℕ0
55 7cn ⊢ 7 ∈ ℂ
56 55 mulridi ⊢ ( 7 · 1 ) = 7
57 38 addlidi ⊢ ( 0 + 6 ) = 6
58 56 57 oveq12i ⊢ ( ( 7 · 1 ) + ( 0 + 6 ) ) = ( 7 + 6 )
59 7p6e13 ⊢ ( 7 + 6 ) = 1 3
60 58 59 eqtri ⊢ ( ( 7 · 1 ) + ( 0 + 6 ) ) = 1 3
61 9cn ⊢ 9 ∈ ℂ
62 9t7e63 ⊢ ( 9 · 7 ) = 6 3
63 61 55 62 mulcomli ⊢ ( 7 · 9 ) = 6 3
64 6p3e9 ⊢ ( 6 + 3 ) = 9
65 38 32 64 addcomli ⊢ ( 3 + 6 ) = 9
66 20 2 20 63 65 decaddi ⊢ ( ( 7 · 9 ) + 6 ) = 6 9
67 1 8 23 20 52 53 54 8 20 60 66 decma2c ⊢ ( ( 7 · 1 9 ) + 6 ) = 1 3 9
68 6lt7 ⊢ 6 < 7
69 49 50 51 67 68 ndvdsi ⊢ ¬ 7 ∥ 1 3 9
70 1 22 decnncl ⊢ 1 1 ∈ ℕ
71 1 29 deccl ⊢ 1 2 ∈ ℕ0
72 eqid ⊢ 1 2 = 1 2
73 54 dec0h ⊢ 7 = 0 7
74 1 1 deccl ⊢ 1 1 ∈ ℕ0
75 2cn ⊢ 2 ∈ ℂ
76 75 addlidi ⊢ ( 0 + 2 ) = 2
77 76 oveq2i ⊢ ( ( 1 1 · 1 ) + ( 0 + 2 ) ) = ( ( 1 1 · 1 ) + 2 )
78 70 nncni ⊢ 1 1 ∈ ℂ
79 78 mulridi ⊢ ( 1 1 · 1 ) = 1 1
80 1p2e3 ⊢ ( 1 + 2 ) = 3
81 1 1 29 79 80 decaddi ⊢ ( ( 1 1 · 1 ) + 2 ) = 1 3
82 77 81 eqtri ⊢ ( ( 1 1 · 1 ) + ( 0 + 2 ) ) = 1 3
83 eqid ⊢ 1 1 = 1 1
84 75 mullidi ⊢ ( 1 · 2 ) = 2
85 00id ⊢ ( 0 + 0 ) = 0
86 84 85 oveq12i ⊢ ( ( 1 · 2 ) + ( 0 + 0 ) ) = ( 2 + 0 )
87 75 addridi ⊢ ( 2 + 0 ) = 2
88 86 87 eqtri ⊢ ( ( 1 · 2 ) + ( 0 + 0 ) ) = 2
89 84 oveq1i ⊢ ( ( 1 · 2 ) + 7 ) = ( 2 + 7 )
90 7p2e9 ⊢ ( 7 + 2 ) = 9
91 55 75 90 addcomli ⊢ ( 2 + 7 ) = 9
92 8 dec0h ⊢ 9 = 0 9
93 89 91 92 3eqtri ⊢ ( ( 1 · 2 ) + 7 ) = 0 9
94 1 1 23 54 83 73 29 8 23 88 93 decmac ⊢ ( ( 1 1 · 2 ) + 7 ) = 2 9
95 1 29 23 54 72 73 74 8 29 82 94 decma2c ⊢ ( ( 1 1 · 1 2 ) + 7 ) = 1 3 9
96 7lt10 ⊢ 7 < 1 0
97 22 1 54 96 declti ⊢ 7 < 1 1
98 70 71 49 95 97 ndvdsi ⊢ ¬ 1 1 ∥ 1 3 9
99 10nn0 ⊢ 1 0 ∈ ℕ0
100 eqid ⊢ 1 0 = 1 0
101 eqid ⊢ 1 3 = 1 3
102 23 dec0h ⊢ 0 = 0 0
103 85 102 eqtri ⊢ ( 0 + 0 ) = 0 0
104 26 mulridi ⊢ ( 1 · 1 ) = 1
105 104 85 oveq12i ⊢ ( ( 1 · 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
106 26 addridi ⊢ ( 1 + 0 ) = 1
107 105 106 eqtri ⊢ ( ( 1 · 1 ) + ( 0 + 0 ) ) = 1
108 32 mulridi ⊢ ( 3 · 1 ) = 3
109 108 oveq1i ⊢ ( ( 3 · 1 ) + 0 ) = ( 3 + 0 )
110 32 addridi ⊢ ( 3 + 0 ) = 3
111 2 dec0h ⊢ 3 = 0 3
112 109 110 111 3eqtri ⊢ ( ( 3 · 1 ) + 0 ) = 0 3
113 1 2 23 23 101 103 1 2 23 107 112 decmac ⊢ ( ( 1 3 · 1 ) + ( 0 + 0 ) ) = 1 3
114 3 nn0cni ⊢ 1 3 ∈ ℂ
115 114 mul01i ⊢ ( 1 3 · 0 ) = 0
116 115 oveq1i ⊢ ( ( 1 3 · 0 ) + 9 ) = ( 0 + 9 )
117 61 addlidi ⊢ ( 0 + 9 ) = 9
118 116 117 92 3eqtri ⊢ ( ( 1 3 · 0 ) + 9 ) = 0 9
119 1 23 23 8 100 92 3 8 23 113 118 decma2c ⊢ ( ( 1 3 · 1 0 ) + 9 ) = 1 3 9
120 22 2 8 11 declti ⊢ 9 < 1 3
121 14 99 4 119 120 ndvdsi ⊢ ¬ 1 3 ∥ 1 3 9
122 1 49 decnncl ⊢ 1 7 ∈ ℕ
123 eqid ⊢ 1 7 = 1 7
124 5nn0 ⊢ 5 ∈ ℕ0
125 8cn ⊢ 8 ∈ ℂ
126 125 mullidi ⊢ ( 1 · 8 ) = 8
127 5cn ⊢ 5 ∈ ℂ
128 127 addlidi ⊢ ( 0 + 5 ) = 5
129 126 128 oveq12i ⊢ ( ( 1 · 8 ) + ( 0 + 5 ) ) = ( 8 + 5 )
130 8p5e13 ⊢ ( 8 + 5 ) = 1 3
131 129 130 eqtri ⊢ ( ( 1 · 8 ) + ( 0 + 5 ) ) = 1 3
132 8t7e56 ⊢ ( 8 · 7 ) = 5 6
133 125 55 132 mulcomli ⊢ ( 7 · 8 ) = 5 6
134 124 20 2 133 64 decaddi ⊢ ( ( 7 · 8 ) + 3 ) = 5 9
135 1 54 23 2 123 111 6 8 124 131 134 decmac ⊢ ( ( 1 7 · 8 ) + 3 ) = 1 3 9
136 22 54 2 10 declti ⊢ 3 < 1 7
137 122 6 13 135 136 ndvdsi ⊢ ¬ 1 7 ∥ 1 3 9
138 1 4 decnncl ⊢ 1 9 ∈ ℕ
139 55 mullidi ⊢ ( 1 · 7 ) = 7
140 139 57 oveq12i ⊢ ( ( 1 · 7 ) + ( 0 + 6 ) ) = ( 7 + 6 )
141 140 59 eqtri ⊢ ( ( 1 · 7 ) + ( 0 + 6 ) ) = 1 3
142 20 2 20 62 65 decaddi ⊢ ( ( 9 · 7 ) + 6 ) = 6 9
143 1 8 23 20 52 53 54 8 20 141 142 decmac ⊢ ( ( 1 9 · 7 ) + 6 ) = 1 3 9
144 6lt10 ⊢ 6 < 1 0
145 22 8 20 144 declti ⊢ 6 < 1 9
146 138 54 51 143 145 ndvdsi ⊢ ¬ 1 9 ∥ 1 3 9
147 29 13 decnncl ⊢ 2 3 ∈ ℕ
148 eqid ⊢ 2 3 = 2 3
149 6t2e12 ⊢ ( 6 · 2 ) = 1 2
150 38 75 149 mulcomli ⊢ ( 2 · 6 ) = 1 2
151 1 29 30 150 decsuc ⊢ ( ( 2 · 6 ) + 1 ) = 1 3
152 29 2 1 148 20 8 1 151 41 decrmac ⊢ ( ( 2 3 · 6 ) + 1 ) = 1 3 9
153 2nn ⊢ 2 ∈ ℕ
154 153 2 1 15 declti ⊢ 1 < 2 3
155 147 20 22 152 154 ndvdsi ⊢ ¬ 2 3 ∥ 1 3 9
156 5 12 16 19 44 48 69 98 121 137 146 155 prmlem2 ⊢ 1 3 9 ∈ ℙ