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	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )

Proof

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