Metamath Proof Explorer

Theorem 1nprm

Description: 1 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by Fan Zheng, 3-Jul-2016)

Ref Expression
Assertion 1nprm ⊢ ¬ 1 ∈ ℙ

Proof

Step Hyp Ref Expression
1 1nn ⊢ 1 ∈ ℕ
2 eleq1 ⊢ z = 1 → z ∈ ℕ ↔ 1 ∈ ℕ
3 1 2 mpbiri ⊢ z = 1 → z ∈ ℕ
4 nnnn0 ⊢ z ∈ ℕ → z ∈ ℕ 0
5 dvds1 ⊢ z ∈ ℕ 0 → z ∥ 1 ↔ z = 1
6 4 5 syl ⊢ z ∈ ℕ → z ∥ 1 ↔ z = 1
7 6 bicomd ⊢ z ∈ ℕ → z = 1 ↔ z ∥ 1
8 3 7 biadanii ⊢ z = 1 ↔ z ∈ ℕ ∧ z ∥ 1
9 velsn ⊢ z ∈ 1 ↔ z = 1
10 breq1 ⊢ n = z → n ∥ 1 ↔ z ∥ 1
11 10 elrab ⊢ z ∈ n ∈ ℕ | n ∥ 1 ↔ z ∈ ℕ ∧ z ∥ 1
12 8 9 11 3bitr4ri ⊢ z ∈ n ∈ ℕ | n ∥ 1 ↔ z ∈ 1
13 12 eqriv ⊢ n ∈ ℕ | n ∥ 1 = 1
14 1ex ⊢ 1 ∈ V
15 14 ensn1 ⊢ 1 ≈ 1 𝑜
16 13 15 eqbrtri ⊢ n ∈ ℕ | n ∥ 1 ≈ 1 𝑜
17 1sdom2 ⊢ 1 𝑜 ≺ 2 𝑜
18 ensdomtr ⊢ n ∈ ℕ | n ∥ 1 ≈ 1 𝑜 ∧ 1 𝑜 ≺ 2 𝑜 → n ∈ ℕ | n ∥ 1 ≺ 2 𝑜
19 16 17 18 mp2an ⊢ n ∈ ℕ | n ∥ 1 ≺ 2 𝑜
20 sdomnen ⊢ n ∈ ℕ | n ∥ 1 ≺ 2 𝑜 → ¬ n ∈ ℕ | n ∥ 1 ≈ 2 𝑜
21 19 20 ax-mp ⊢ ¬ n ∈ ℕ | n ∥ 1 ≈ 2 𝑜
22 isprm ⊢ 1 ∈ ℙ ↔ 1 ∈ ℕ ∧ n ∈ ℕ | n ∥ 1 ≈ 2 𝑜
23 1 22 mpbiran ⊢ 1 ∈ ℙ ↔ n ∈ ℕ | n ∥ 1 ≈ 2 𝑜
24 21 23 mtbir ⊢ ¬ 1 ∈ ℙ