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

Metamath Proof Explorer

Theorem recextlem2

Description: Lemma for recex . (Contributed by Eric Schmidt, 23-May-2007)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( B = 0 -> ( _i x. B ) = ( _i x. 0 ) )
2 ax-icn 
 |-  _i e. CC
3 2 mul01i 
 |-  ( _i x. 0 ) = 0
4 1 3 eqtrdi 
 |-  ( B = 0 -> ( _i x. B ) = 0 )
5 oveq12 
 |-  ( ( A = 0 /\ ( _i x. B ) = 0 ) -> ( A + ( _i x. B ) ) = ( 0 + 0 ) )
6 4 5 sylan2 
 |-  ( ( A = 0 /\ B = 0 ) -> ( A + ( _i x. B ) ) = ( 0 + 0 ) )
7 00id 
 |-  ( 0 + 0 ) = 0
8 6 7 eqtrdi 
 |-  ( ( A = 0 /\ B = 0 ) -> ( A + ( _i x. B ) ) = 0 )
9 8 necon3ai 
 |-  ( ( A + ( _i x. B ) ) =/= 0 -> -. ( A = 0 /\ B = 0 ) )
10 neorian 
 |-  ( ( A =/= 0 \/ B =/= 0 ) <-> -. ( A = 0 /\ B = 0 ) )
11 9 10 sylibr 
 |-  ( ( A + ( _i x. B ) ) =/= 0 -> ( A =/= 0 \/ B =/= 0 ) )
12 remulcl 
 |-  ( ( A e. RR /\ A e. RR ) -> ( A x. A ) e. RR )
13 12 anidms 
 |-  ( A e. RR -> ( A x. A ) e. RR )
14 remulcl 
 |-  ( ( B e. RR /\ B e. RR ) -> ( B x. B ) e. RR )
15 14 anidms 
 |-  ( B e. RR -> ( B x. B ) e. RR )
16 13 15 anim12i 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A x. A ) e. RR /\ ( B x. B ) e. RR ) )
17 msqgt0 
 |-  ( ( A e. RR /\ A =/= 0 ) -> 0 < ( A x. A ) )
18 msqge0 
 |-  ( B e. RR -> 0 <_ ( B x. B ) )
19 17 18 anim12i 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR ) -> ( 0 < ( A x. A ) /\ 0 <_ ( B x. B ) ) )
20 19 an32s 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A =/= 0 ) -> ( 0 < ( A x. A ) /\ 0 <_ ( B x. B ) ) )
21 addgtge0 
 |-  ( ( ( ( A x. A ) e. RR /\ ( B x. B ) e. RR ) /\ ( 0 < ( A x. A ) /\ 0 <_ ( B x. B ) ) ) -> 0 < ( ( A x. A ) + ( B x. B ) ) )
22 16 20 21 syl2an2r 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A =/= 0 ) -> 0 < ( ( A x. A ) + ( B x. B ) ) )
23 msqge0 
 |-  ( A e. RR -> 0 <_ ( A x. A ) )
24 msqgt0 
 |-  ( ( B e. RR /\ B =/= 0 ) -> 0 < ( B x. B ) )
25 23 24 anim12i 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) ) -> ( 0 <_ ( A x. A ) /\ 0 < ( B x. B ) ) )
26 25 anassrs 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B =/= 0 ) -> ( 0 <_ ( A x. A ) /\ 0 < ( B x. B ) ) )
27 addgegt0 
 |-  ( ( ( ( A x. A ) e. RR /\ ( B x. B ) e. RR ) /\ ( 0 <_ ( A x. A ) /\ 0 < ( B x. B ) ) ) -> 0 < ( ( A x. A ) + ( B x. B ) ) )
28 16 26 27 syl2an2r 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B =/= 0 ) -> 0 < ( ( A x. A ) + ( B x. B ) ) )
29 22 28 jaodan 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> 0 < ( ( A x. A ) + ( B x. B ) ) )
30 11 29 sylan2 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A + ( _i x. B ) ) =/= 0 ) -> 0 < ( ( A x. A ) + ( B x. B ) ) )
31 30 3impa 
 |-  ( ( A e. RR /\ B e. RR /\ ( A + ( _i x. B ) ) =/= 0 ) -> 0 < ( ( A x. A ) + ( B x. B ) ) )
32 31 gt0ne0d 
 |-  ( ( A e. RR /\ B e. RR /\ ( A + ( _i x. B ) ) =/= 0 ) -> ( ( A x. A ) + ( B x. B ) ) =/= 0 )