Metamath Proof Explorer


Theorem sn-it0e0

Description: Proof of it0e0 without ax-mulcom . Informally, a real number times 0 is 0, and E. r e. RR r = _i x. s by ax-cnre and renegid2 . (Contributed by SN, 30-Apr-2024)

Ref Expression
Assertion sn-it0e0 i 0 = 0

Proof

Step Hyp Ref Expression
1 0cn 0
2 cnre 0 a b 0 = a + i b
3 oveq2 0 = a + i b 0 - a + 0 = 0 - a + a + i b
4 ax-icn i
5 4 a1i b i
6 recn b b
7 0cnd b 0
8 5 6 7 mulassd b i b 0 = i b 0
9 remul01 b b 0 = 0
10 9 oveq2d b i b 0 = i 0
11 8 10 eqtrd b i b 0 = i 0
12 11 ad2antlr a b 0 - a + 0 = 0 - a + a + i b i b 0 = i 0
13 rernegcl a 0 - a
14 13 recnd a 0 - a
15 14 adantr a b 0 - a
16 recn a a
17 16 adantr a b a
18 5 6 mulcld b i b
19 18 adantl a b i b
20 15 17 19 addassd a b 0 - a + a + i b = 0 - a + a + i b
21 renegid2 a 0 - a + a = 0
22 21 oveq1d a 0 - a + a + i b = 0 + i b
23 sn-addid2 i b 0 + i b = i b
24 18 23 syl b 0 + i b = i b
25 22 24 sylan9eq a b 0 - a + a + i b = i b
26 20 25 eqtr3d a b 0 - a + a + i b = i b
27 26 eqeq2d a b 0 - a + 0 = 0 - a + a + i b 0 - a + 0 = i b
28 27 biimpa a b 0 - a + 0 = 0 - a + a + i b 0 - a + 0 = i b
29 28 oveq1d a b 0 - a + 0 = 0 - a + a + i b 0 - a + 0 0 = i b 0
30 elre0re a 0
31 13 30 readdcld a 0 - a + 0
32 31 ad2antrr a b 0 - a + 0 = 0 - a + a + i b 0 - a + 0
33 remul01 0 - a + 0 0 - a + 0 0 = 0
34 32 33 syl a b 0 - a + 0 = 0 - a + a + i b 0 - a + 0 0 = 0
35 29 34 eqtr3d a b 0 - a + 0 = 0 - a + a + i b i b 0 = 0
36 12 35 eqtr3d a b 0 - a + 0 = 0 - a + a + i b i 0 = 0
37 36 ex a b 0 - a + 0 = 0 - a + a + i b i 0 = 0
38 3 37 syl5 a b 0 = a + i b i 0 = 0
39 38 rexlimivv a b 0 = a + i b i 0 = 0
40 1 2 39 mp2b i 0 = 0