Metamath Proof Explorer


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