Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
ine1
Next ⟩
0tie0
Metamath Proof Explorer
Ascii
Unicode
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