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 eqtr2id
 |-  ( ( 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 ) ) )