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 x. 0 ) = 0

Proof

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