Metamath Proof Explorer

Theorem mul02lem2

Description: Lemma for mul02 . Zero times a real is zero. (Contributed by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion mul02lem2 
|- ( A e. RR -> ( 0 x. A ) = 0 )

Proof

Step Hyp Ref Expression
1 ax-1ne0 
 |-  1 =/= 0
2 ax-1cn 
 |-  1 e. CC
3 mul02lem1 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ 1 e. CC ) -> 1 = ( 1 + 1 ) )
4 2 3 mpan2 
 |-  ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) -> 1 = ( 1 + 1 ) )
5 4 eqcomd 
 |-  ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) -> ( 1 + 1 ) = 1 )
6 5 oveq2d 
 |-  ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) -> ( ( _i x. _i ) + ( 1 + 1 ) ) = ( ( _i x. _i ) + 1 ) )
7 ax-icn 
 |-  _i e. CC
8 7 7 mulcli 
 |-  ( _i x. _i ) e. CC
9 8 2 2 addassi 
 |-  ( ( ( _i x. _i ) + 1 ) + 1 ) = ( ( _i x. _i ) + ( 1 + 1 ) )
10 ax-i2m1 
 |-  ( ( _i x. _i ) + 1 ) = 0
11 10 oveq1i 
 |-  ( ( ( _i x. _i ) + 1 ) + 1 ) = ( 0 + 1 )
12 9 11 eqtr3i 
 |-  ( ( _i x. _i ) + ( 1 + 1 ) ) = ( 0 + 1 )
13 00id 
 |-  ( 0 + 0 ) = 0
14 10 13 eqtr4i 
 |-  ( ( _i x. _i ) + 1 ) = ( 0 + 0 )
15 6 12 14 3eqtr3g 
 |-  ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) -> ( 0 + 1 ) = ( 0 + 0 ) )
16 1re 
 |-  1 e. RR
17 0re 
 |-  0 e. RR
18 readdcan 
 |-  ( ( 1 e. RR /\ 0 e. RR /\ 0 e. RR ) -> ( ( 0 + 1 ) = ( 0 + 0 ) <-> 1 = 0 ) )
19 16 17 17 18 mp3an 
 |-  ( ( 0 + 1 ) = ( 0 + 0 ) <-> 1 = 0 )
20 15 19 sylib 
 |-  ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) -> 1 = 0 )
21 20 ex 
 |-  ( A e. RR -> ( ( 0 x. A ) =/= 0 -> 1 = 0 ) )
22 21 necon1d 
 |-  ( A e. RR -> ( 1 =/= 0 -> ( 0 x. A ) = 0 ) )
23 1 22 mpi 
 |-  ( A e. RR -> ( 0 x. A ) = 0 )