This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mul02lem1

Description: Lemma for mul02 . If any real does not produce 0 when multiplied by 0 , then any complex is equal to double itself. (Contributed by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion mul02lem1 
|- ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) -> B = ( B + B ) )

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 remulcl 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 x. A ) e. RR )
3 1 2 mpan 
 |-  ( A e. RR -> ( 0 x. A ) e. RR )
4 ax-rrecex 
 |-  ( ( ( 0 x. A ) e. RR /\ ( 0 x. A ) =/= 0 ) -> E. y e. RR ( ( 0 x. A ) x. y ) = 1 )
5 3 4 sylan 
 |-  ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) -> E. y e. RR ( ( 0 x. A ) x. y ) = 1 )
6 5 adantr 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) -> E. y e. RR ( ( 0 x. A ) x. y ) = 1 )
7 00id 
 |-  ( 0 + 0 ) = 0
8 7 oveq2i 
 |-  ( ( ( y x. A ) x. B ) x. ( 0 + 0 ) ) = ( ( ( y x. A ) x. B ) x. 0 )
9 8 eqcomi 
 |-  ( ( ( y x. A ) x. B ) x. 0 ) = ( ( ( y x. A ) x. B ) x. ( 0 + 0 ) )
10 simprl 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> y e. RR )
11 10 recnd 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> y e. CC )
12 simplll 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> A e. RR )
13 12 recnd 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> A e. CC )
14 11 13 mulcld 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( y x. A ) e. CC )
15 simplr 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> B e. CC )
16 0cn 
 |-  0 e. CC
17 mul32 
 |-  ( ( ( y x. A ) e. CC /\ B e. CC /\ 0 e. CC ) -> ( ( ( y x. A ) x. B ) x. 0 ) = ( ( ( y x. A ) x. 0 ) x. B ) )
18 16 17 mp3an3 
 |-  ( ( ( y x. A ) e. CC /\ B e. CC ) -> ( ( ( y x. A ) x. B ) x. 0 ) = ( ( ( y x. A ) x. 0 ) x. B ) )
19 14 15 18 syl2anc 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( ( ( y x. A ) x. B ) x. 0 ) = ( ( ( y x. A ) x. 0 ) x. B ) )
20 mul31 
 |-  ( ( y e. CC /\ A e. CC /\ 0 e. CC ) -> ( ( y x. A ) x. 0 ) = ( ( 0 x. A ) x. y ) )
21 16 20 mp3an3 
 |-  ( ( y e. CC /\ A e. CC ) -> ( ( y x. A ) x. 0 ) = ( ( 0 x. A ) x. y ) )
22 11 13 21 syl2anc 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( ( y x. A ) x. 0 ) = ( ( 0 x. A ) x. y ) )
23 simprr 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( ( 0 x. A ) x. y ) = 1 )
24 22 23 eqtrd 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( ( y x. A ) x. 0 ) = 1 )
25 24 oveq1d 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( ( ( y x. A ) x. 0 ) x. B ) = ( 1 x. B ) )
26 mullid 
 |-  ( B e. CC -> ( 1 x. B ) = B )
27 26 ad2antlr 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( 1 x. B ) = B )
28 25 27 eqtrd 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( ( ( y x. A ) x. 0 ) x. B ) = B )
29 19 28 eqtrd 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( ( ( y x. A ) x. B ) x. 0 ) = B )
30 14 15 mulcld 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( ( y x. A ) x. B ) e. CC )
31 adddi 
 |-  ( ( ( ( y x. A ) x. B ) e. CC /\ 0 e. CC /\ 0 e. CC ) -> ( ( ( y x. A ) x. B ) x. ( 0 + 0 ) ) = ( ( ( ( y x. A ) x. B ) x. 0 ) + ( ( ( y x. A ) x. B ) x. 0 ) ) )
32 16 16 31 mp3an23 
 |-  ( ( ( y x. A ) x. B ) e. CC -> ( ( ( y x. A ) x. B ) x. ( 0 + 0 ) ) = ( ( ( ( y x. A ) x. B ) x. 0 ) + ( ( ( y x. A ) x. B ) x. 0 ) ) )
33 30 32 syl 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( ( ( y x. A ) x. B ) x. ( 0 + 0 ) ) = ( ( ( ( y x. A ) x. B ) x. 0 ) + ( ( ( y x. A ) x. B ) x. 0 ) ) )
34 29 29 oveq12d 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( ( ( ( y x. A ) x. B ) x. 0 ) + ( ( ( y x. A ) x. B ) x. 0 ) ) = ( B + B ) )
35 33 34 eqtrd 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> ( ( ( y x. A ) x. B ) x. ( 0 + 0 ) ) = ( B + B ) )
36 9 29 35 3eqtr3a 
 |-  ( ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) /\ ( y e. RR /\ ( ( 0 x. A ) x. y ) = 1 ) ) -> B = ( B + B ) )
37 6 36 rexlimddv 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) -> B = ( B + B ) )