Metamath Proof Explorer


Theorem recextlem1

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

Ref Expression
Assertion recextlem1 A B A + i B A i B = A A + B B

Proof

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