Theorem ine1

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

	Ref	Expression
Assertion	ine1	⊢ i ≠ 1

Proof

Step	Hyp	Ref	Expression
1		1re	⊢ 1 ∈ ℝ
2		inelr	⊢ ¬ i ∈ ℝ
3		nelne2	⊢ ( ( 1 ∈ ℝ ∧ ¬ i ∈ ℝ ) → 1 ≠ i )
4	1 2 3	mp2an	⊢ 1 ≠ i
5	4	necomi	⊢ i ≠ 1