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