Theorem ine1

Description: _i is not 1. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Assertion	ine1	$$⊢\mathrm{i}\ne 1$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		inelr	$$⊢\neg \mathrm{i}\in ℝ$$
3		nelne2	$$⊢\left(1\in ℝ\wedge \neg \mathrm{i}\in ℝ\right)\to 1\ne \mathrm{i}$$
4	1 2 3	mp2an	$$⊢1\ne \mathrm{i}$$
5	4	necomi	$$⊢\mathrm{i}\ne 1$$