Metamath Proof Explorer

Theorem eluz2cnn0n1

Description: An integer greater than 1 is a complex number not equal to 0 or 1. (Contributed by AV, 23-May-2020)

Ref Expression
Assertion eluz2cnn0n1 ⊢ B ∈ ℤ ≥ 2 → B ∈ ℂ ∖ 0 1

Proof

Step Hyp Ref Expression
1 nncn ⊢ B ∈ ℕ → B ∈ ℂ
2 1 adantr ⊢ B ∈ ℕ ∧ B ≠ 1 → B ∈ ℂ
3 nnne0 ⊢ B ∈ ℕ → B ≠ 0
4 3 adantr ⊢ B ∈ ℕ ∧ B ≠ 1 → B ≠ 0
5 simpr ⊢ B ∈ ℕ ∧ B ≠ 1 → B ≠ 1
6 2 4 5 3jca ⊢ B ∈ ℕ ∧ B ≠ 1 → B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1
7 eluz2b3 ⊢ B ∈ ℤ ≥ 2 ↔ B ∈ ℕ ∧ B ≠ 1
8 eldifpr ⊢ B ∈ ℂ ∖ 0 1 ↔ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1
9 6 7 8 3imtr4i ⊢ B ∈ ℤ ≥ 2 → B ∈ ℂ ∖ 0 1