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 \in ℤ_{\geq 2} \to B \in (ℂ ∖ \{0, 1\})$

Step	Hyp	Ref	Expression
1		nncn	$⊢ B \in ℕ \to B \in ℂ$
2	1	adantr	$⊢ (B \in ℕ \land B \neq 1) \to B \in ℂ$
3		nnne0	$⊢ B \in ℕ \to B \neq 0$
4	3	adantr	$⊢ (B \in ℕ \land B \neq 1) \to B \neq 0$
5		simpr	$⊢ (B \in ℕ \land B \neq 1) \to B \neq 1$
6	2 4 5	3jca	$⊢ (B \in ℕ \land B \neq 1) \to (B \in ℂ \land B \neq 0 \land B \neq 1)$
7		eluz2b3	$⊢ B \in ℤ_{\geq 2} \leftrightarrow (B \in ℕ \land B \neq 1)$
8		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
9	6 7 8	3imtr4i	$⊢ B \in ℤ_{\geq 2} \to B \in (ℂ ∖ \{0, 1\})$

Metamath Proof Explorer