Metamath Proof Explorer

Theorem recextlem1

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

Ref Expression
Assertion recextlem1 
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) = ( ( A x. A ) + ( B x. B ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
2 ax-icn 
 |-  _i e. CC
3 mulcl 
 |-  ( ( _i e. CC /\ B e. CC ) -> ( _i x. B ) e. CC )
4 2 3 mpan 
 |-  ( B e. CC -> ( _i x. B ) e. CC )
5 4 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. B ) e. CC )
6 subcl 
 |-  ( ( A e. CC /\ ( _i x. B ) e. CC ) -> ( A - ( _i x. B ) ) e. CC )
7 4 6 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - ( _i x. B ) ) e. CC )
8 1 5 7 adddird 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) = ( ( A x. ( A - ( _i x. B ) ) ) + ( ( _i x. B ) x. ( A - ( _i x. B ) ) ) ) )
9 1 1 5 subdid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. ( A - ( _i x. B ) ) ) = ( ( A x. A ) - ( A x. ( _i x. B ) ) ) )
10 5 1 5 subdid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. B ) x. ( A - ( _i x. B ) ) ) = ( ( ( _i x. B ) x. A ) - ( ( _i x. B ) x. ( _i x. B ) ) ) )
11 mulcom 
 |-  ( ( A e. CC /\ ( _i x. B ) e. CC ) -> ( A x. ( _i x. B ) ) = ( ( _i x. B ) x. A ) )
12 4 11 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. ( _i x. B ) ) = ( ( _i x. B ) x. A ) )
13 ixi 
 |-  ( _i x. _i ) = -u 1
14 13 oveq1i 
 |-  ( ( _i x. _i ) x. ( B x. B ) ) = ( -u 1 x. ( B x. B ) )
15 mulcl 
 |-  ( ( B e. CC /\ B e. CC ) -> ( B x. B ) e. CC )
16 15 mulm1d 
 |-  ( ( B e. CC /\ B e. CC ) -> ( -u 1 x. ( B x. B ) ) = -u ( B x. B ) )
17 14 16 syl5req 
 |-  ( ( B e. CC /\ B e. CC ) -> -u ( B x. B ) = ( ( _i x. _i ) x. ( B x. B ) ) )
18 mul4 
 |-  ( ( ( _i e. CC /\ _i e. CC ) /\ ( B e. CC /\ B e. CC ) ) -> ( ( _i x. _i ) x. ( B x. B ) ) = ( ( _i x. B ) x. ( _i x. B ) ) )
19 2 2 18 mpanl12 
 |-  ( ( B e. CC /\ B e. CC ) -> ( ( _i x. _i ) x. ( B x. B ) ) = ( ( _i x. B ) x. ( _i x. B ) ) )
20 17 19 eqtrd 
 |-  ( ( B e. CC /\ B e. CC ) -> -u ( B x. B ) = ( ( _i x. B ) x. ( _i x. B ) ) )
21 20 anidms 
 |-  ( B e. CC -> -u ( B x. B ) = ( ( _i x. B ) x. ( _i x. B ) ) )
22 21 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> -u ( B x. B ) = ( ( _i x. B ) x. ( _i x. B ) ) )
23 12 22 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. ( _i x. B ) ) - -u ( B x. B ) ) = ( ( ( _i x. B ) x. A ) - ( ( _i x. B ) x. ( _i x. B ) ) ) )
24 10 23 eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. B ) x. ( A - ( _i x. B ) ) ) = ( ( A x. ( _i x. B ) ) - -u ( B x. B ) ) )
25 9 24 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. ( A - ( _i x. B ) ) ) + ( ( _i x. B ) x. ( A - ( _i x. B ) ) ) ) = ( ( ( A x. A ) - ( A x. ( _i x. B ) ) ) + ( ( A x. ( _i x. B ) ) - -u ( B x. B ) ) ) )
26 mulcl 
 |-  ( ( A e. CC /\ A e. CC ) -> ( A x. A ) e. CC )
27 26 anidms 
 |-  ( A e. CC -> ( A x. A ) e. CC )
28 27 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. A ) e. CC )
29 mulcl 
 |-  ( ( A e. CC /\ ( _i x. B ) e. CC ) -> ( A x. ( _i x. B ) ) e. CC )
30 4 29 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. ( _i x. B ) ) e. CC )
31 15 negcld 
 |-  ( ( B e. CC /\ B e. CC ) -> -u ( B x. B ) e. CC )
32 31 anidms 
 |-  ( B e. CC -> -u ( B x. B ) e. CC )
33 32 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> -u ( B x. B ) e. CC )
34 28 30 33 npncand 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A x. A ) - ( A x. ( _i x. B ) ) ) + ( ( A x. ( _i x. B ) ) - -u ( B x. B ) ) ) = ( ( A x. A ) - -u ( B x. B ) ) )
35 15 anidms 
 |-  ( B e. CC -> ( B x. B ) e. CC )
36 subneg 
 |-  ( ( ( A x. A ) e. CC /\ ( B x. B ) e. CC ) -> ( ( A x. A ) - -u ( B x. B ) ) = ( ( A x. A ) + ( B x. B ) ) )
37 27 35 36 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. A ) - -u ( B x. B ) ) = ( ( A x. A ) + ( B x. B ) ) )
38 34 37 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A x. A ) - ( A x. ( _i x. B ) ) ) + ( ( A x. ( _i x. B ) ) - -u ( B x. B ) ) ) = ( ( A x. A ) + ( B x. B ) ) )
39 8 25 38 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) = ( ( A x. A ) + ( B x. B ) ) )