Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
retire
Next ⟩
Exponents and divisibility
Metamath Proof Explorer
Ascii
Unicode
Theorem
retire
Description:
A real times
_i
is real iff the real is zero.
(Contributed by
SN
, 25-Apr-2025)
Ref
Expression
Assertion
retire
⊢
R
∈
ℝ
→
R
⁢
i
∈
ℝ
↔
R
=
0
Proof
Step
Hyp
Ref
Expression
1
recn
⊢
R
∈
ℝ
→
R
∈
ℂ
2
ax-icn
⊢
i
∈
ℂ
3
2
a1i
⊢
R
∈
ℝ
→
i
∈
ℂ
4
1
3
mulcomd
⊢
R
∈
ℝ
→
R
⁢
i
=
i
⁢
R
5
4
eleq1d
⊢
R
∈
ℝ
→
R
⁢
i
∈
ℝ
↔
i
⁢
R
∈
ℝ
6
itrere
⊢
R
∈
ℝ
→
i
⁢
R
∈
ℝ
↔
R
=
0
7
5
6
bitrd
⊢
R
∈
ℝ
→
R
⁢
i
∈
ℝ
↔
R
=
0