Metamath Proof Explorer


Theorem itrere

Description: _i times a real is real iff the real is zero. (Contributed by SN, 25-Apr-2025)

Ref Expression
Assertion itrere R i R R = 0

Proof

Step Hyp Ref Expression
1 inelr ¬ i
2 ax-icn i
3 2 a1i R R 0 i R i
4 simpll R R 0 i R R
5 4 recnd R R 0 i R R
6 simplr R R 0 i R R 0
7 3 5 6 divcan4d R R 0 i R i R R = i
8 simpr R R 0 i R i R
9 8 4 6 redivcld R R 0 i R i R R
10 7 9 eqeltrrd R R 0 i R i
11 10 ex R R 0 i R i
12 1 11 mtoi R R 0 ¬ i R
13 12 ex R R 0 ¬ i R
14 13 necon4ad R i R R = 0
15 oveq2 R = 0 i R = i 0
16 it0e0 i 0 = 0
17 0re 0
18 16 17 eqeltri i 0
19 15 18 eqeltrdi R = 0 i R
20 14 19 impbid1 R i R R = 0