This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑧 = 1 → ( 𝑧 ∈ ℕ ↔ 1 ∈ ℕ ) )
3 1 2 mpbiri ⊢ ( 𝑧 = 1 → 𝑧 ∈ ℕ )
4 nnnn0 ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℕ0 )
5 dvds1 ⊢ ( 𝑧 ∈ ℕ0 → ( 𝑧 ∥ 1 ↔ 𝑧 = 1 ) )
6 4 5 syl ⊢ ( 𝑧 ∈ ℕ → ( 𝑧 ∥ 1 ↔ 𝑧 = 1 ) )
7 6 bicomd ⊢ ( 𝑧 ∈ ℕ → ( 𝑧 = 1 ↔ 𝑧 ∥ 1 ) )
8 3 7 biadanii ⊢ ( 𝑧 = 1 ↔ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 1 ) )
9 velsn ⊢ ( 𝑧 ∈ { 1 } ↔ 𝑧 = 1 )
10 breq1 ⊢ ( 𝑛 = 𝑧 → ( 𝑛 ∥ 1 ↔ 𝑧 ∥ 1 ) )
11 10 elrab ⊢ ( 𝑧 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 1 } ↔ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 1 ) )
12 8 9 11 3bitr4ri ⊢ ( 𝑧 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 1 } ↔ 𝑧 ∈ { 1 } )
13 12 eqriv ⊢ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 1 } = { 1 }
14 1ex ⊢ 1 ∈ V
15 14 ensn1 ⊢ { 1 } ≈ 1o
16 13 15 eqbrtri ⊢ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 1 } ≈ 1o
17 1sdom2 ⊢ 1o ≺ 2o
18 ensdomtr ⊢ ( ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 1 } ≈ 1o ∧ 1o ≺ 2o ) → { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 1 } ≺ 2o )
19 16 17 18 mp2an ⊢ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 1 } ≺ 2o
20 sdomnen ⊢ ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 1 } ≺ 2o → ¬ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 1 } ≈ 2o )
21 19 20 ax-mp ⊢ ¬ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 1 } ≈ 2o
22 isprm ⊢ ( 1 ∈ ℙ ↔ ( 1 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 1 } ≈ 2o ) )
23 1 22 mpbiran ⊢ ( 1 ∈ ℙ ↔ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 1 } ≈ 2o )
24 21 23 mtbir ⊢ ¬ 1 ∈ ℙ