Metamath Proof Explorer

Theorem mul4sqlem

Description: Lemma for mul4sq : algebraic manipulations. The extra assumptions involving M are for a part of 4sqlem17 which needs to know not just that the product is a sum of squares, but also that it preserves divisibility by M . (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Hypotheses 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
mul4sq.1 ⊢ ( 𝜑 → 𝐴 ∈ ℤ[i] )
mul4sq.2 ⊢ ( 𝜑 → 𝐵 ∈ ℤ[i] )
mul4sq.3 ⊢ ( 𝜑 → 𝐶 ∈ ℤ[i] )
mul4sq.4 ⊢ ( 𝜑 → 𝐷 ∈ ℤ[i] )
mul4sq.5 ⊢ 𝑋 = ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) )
mul4sq.6 ⊢ 𝑌 = ( ( ( abs ‘ 𝐶 ) ↑ 2 ) + ( ( abs ‘ 𝐷 ) ↑ 2 ) )
mul4sq.7 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
mul4sq.8 ⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) / 𝑀 ) ∈ ℤ[i] )
mul4sq.9 ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) / 𝑀 ) ∈ ℤ[i] )
mul4sq.10 ⊢ ( 𝜑 → ( 𝑋 / 𝑀 ) ∈ ℕ0 )
Assertion mul4sqlem ( 𝜑 → ( ( 𝑋 / 𝑀 ) · ( 𝑌 / 𝑀 ) ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
2 mul4sq.1 ⊢ ( 𝜑 → 𝐴 ∈ ℤ[i] )
3 mul4sq.2 ⊢ ( 𝜑 → 𝐵 ∈ ℤ[i] )
4 mul4sq.3 ⊢ ( 𝜑 → 𝐶 ∈ ℤ[i] )
5 mul4sq.4 ⊢ ( 𝜑 → 𝐷 ∈ ℤ[i] )
6 mul4sq.5 ⊢ 𝑋 = ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) )
7 mul4sq.6 ⊢ 𝑌 = ( ( ( abs ‘ 𝐶 ) ↑ 2 ) + ( ( abs ‘ 𝐷 ) ↑ 2 ) )
8 mul4sq.7 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
9 mul4sq.8 ⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) / 𝑀 ) ∈ ℤ[i] )
10 mul4sq.9 ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) / 𝑀 ) ∈ ℤ[i] )
11 mul4sq.10 ⊢ ( 𝜑 → ( 𝑋 / 𝑀 ) ∈ ℕ0 )
12 gzcn ⊢ ( 𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ )
13 2 12 syl ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
14 gzcn ⊢ ( 𝐶 ∈ ℤ[i] → 𝐶 ∈ ℂ )
15 4 14 syl ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
16 13 15 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℂ )
17 16 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) = ( ( 𝐴 · 𝐶 ) · ( ∗ ‘ ( 𝐴 · 𝐶 ) ) ) )
18 16 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 · 𝐶 ) ) ∈ ℂ )
19 16 18 mulcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) · ( ∗ ‘ ( 𝐴 · 𝐶 ) ) ) ∈ ℂ )
20 17 19 eqeltrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) ∈ ℂ )
21 gzcn ⊢ ( 𝐵 ∈ ℤ[i] → 𝐵 ∈ ℂ )
22 3 21 syl ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
23 gzcn ⊢ ( 𝐷 ∈ ℤ[i] → 𝐷 ∈ ℂ )
24 5 23 syl ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
25 22 24 mulcld ⊢ ( 𝜑 → ( 𝐵 · 𝐷 ) ∈ ℂ )
26 25 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) = ( ( 𝐵 · 𝐷 ) · ( ∗ ‘ ( 𝐵 · 𝐷 ) ) ) )
27 25 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 · 𝐷 ) ) ∈ ℂ )
28 25 27 mulcld ⊢ ( 𝜑 → ( ( 𝐵 · 𝐷 ) · ( ∗ ‘ ( 𝐵 · 𝐷 ) ) ) ∈ ℂ )
29 26 28 eqeltrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ∈ ℂ )
30 20 29 addcld ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) ∈ ℂ )
31 13 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝐴 ) ∈ ℂ )
32 31 15 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · 𝐶 ) ∈ ℂ )
33 22 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝐵 ) ∈ ℂ )
34 33 24 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ∈ ℂ )
35 32 34 mulcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ∈ ℂ )
36 15 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝐶 ) ∈ ℂ )
37 22 36 mulcld ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ∈ ℂ )
38 24 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝐷 ) ∈ ℂ )
39 13 38 mulcld ⊢ ( 𝜑 → ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ∈ ℂ )
40 37 39 mulcld ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ∈ ℂ )
41 35 40 addcld ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ∈ ℂ )
42 13 24 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℂ )
43 42 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) = ( ( 𝐴 · 𝐷 ) · ( ∗ ‘ ( 𝐴 · 𝐷 ) ) ) )
44 42 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 · 𝐷 ) ) ∈ ℂ )
45 42 44 mulcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) · ( ∗ ‘ ( 𝐴 · 𝐷 ) ) ) ∈ ℂ )
46 43 45 eqeltrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) ∈ ℂ )
47 22 15 mulcld ⊢ ( 𝜑 → ( 𝐵 · 𝐶 ) ∈ ℂ )
48 47 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( ( 𝐵 · 𝐶 ) · ( ∗ ‘ ( 𝐵 · 𝐶 ) ) ) )
49 47 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 · 𝐶 ) ) ∈ ℂ )
50 47 49 mulcld ⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) · ( ∗ ‘ ( 𝐵 · 𝐶 ) ) ) ∈ ℂ )
51 48 50 eqeltrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ∈ ℂ )
52 46 51 addcld ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) ∈ ℂ )
53 30 41 52 ppncand ⊢ ( 𝜑 → ( ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) + ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ) + ( ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) − ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ) ) = ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) + ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) ) )
54 22 38 mulcld ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ∈ ℂ )
55 32 54 addcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ∈ ℂ )
56 55 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ↑ 2 ) = ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) · ( ∗ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ) )
57 32 54 cjaddd ⊢ ( 𝜑 → ( ∗ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) = ( ( ∗ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐶 ) ) + ( ∗ ‘ ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) )
58 31 15 cjmuld ⊢ ( 𝜑 → ( ∗ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐶 ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) · ( ∗ ‘ 𝐶 ) ) )
59 13 cjcjd ⊢ ( 𝜑 → ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) = 𝐴 )
60 59 oveq1d ⊢ ( 𝜑 → ( ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) · ( ∗ ‘ 𝐶 ) ) = ( 𝐴 · ( ∗ ‘ 𝐶 ) ) )
61 58 60 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐶 ) ) = ( 𝐴 · ( ∗ ‘ 𝐶 ) ) )
62 22 38 cjmuld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) = ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ ( ∗ ‘ 𝐷 ) ) ) )
63 24 cjcjd ⊢ ( 𝜑 → ( ∗ ‘ ( ∗ ‘ 𝐷 ) ) = 𝐷 )
64 63 oveq2d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ ( ∗ ‘ 𝐷 ) ) ) = ( ( ∗ ‘ 𝐵 ) · 𝐷 ) )
65 62 64 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) = ( ( ∗ ‘ 𝐵 ) · 𝐷 ) )
66 61 65 oveq12d ⊢ ( 𝜑 → ( ( ∗ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐶 ) ) + ( ∗ ‘ ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) )
67 57 66 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) )
68 67 oveq2d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) · ( ∗ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) )
69 13 36 mulcld ⊢ ( 𝜑 → ( 𝐴 · ( ∗ ‘ 𝐶 ) ) ∈ ℂ )
70 32 69 34 adddid ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( 𝐴 · ( ∗ ‘ 𝐶 ) ) ) + ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) )
71 15 31 13 36 mul4d ⊢ ( 𝜑 → ( ( 𝐶 · ( ∗ ‘ 𝐴 ) ) · ( 𝐴 · ( ∗ ‘ 𝐶 ) ) ) = ( ( 𝐶 · 𝐴 ) · ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐶 ) ) ) )
72 31 15 mulcomd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · 𝐶 ) = ( 𝐶 · ( ∗ ‘ 𝐴 ) ) )
73 72 oveq1d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( 𝐴 · ( ∗ ‘ 𝐶 ) ) ) = ( ( 𝐶 · ( ∗ ‘ 𝐴 ) ) · ( 𝐴 · ( ∗ ‘ 𝐶 ) ) ) )
74 13 15 mulcomd ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
75 13 15 cjmuld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 · 𝐶 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐶 ) ) )
76 74 75 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) · ( ∗ ‘ ( 𝐴 · 𝐶 ) ) ) = ( ( 𝐶 · 𝐴 ) · ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐶 ) ) ) )
77 71 73 76 3eqtr4d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( 𝐴 · ( ∗ ‘ 𝐶 ) ) ) = ( ( 𝐴 · 𝐶 ) · ( ∗ ‘ ( 𝐴 · 𝐶 ) ) ) )
78 77 17 eqtr4d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( 𝐴 · ( ∗ ‘ 𝐶 ) ) ) = ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) )
79 78 oveq1d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( 𝐴 · ( ∗ ‘ 𝐶 ) ) ) + ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) = ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) )
80 70 79 eqtrd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) = ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) )
81 54 69 34 adddid ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) = ( ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( 𝐴 · ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) )
82 13 36 mulcomd ⊢ ( 𝜑 → ( 𝐴 · ( ∗ ‘ 𝐶 ) ) = ( ( ∗ ‘ 𝐶 ) · 𝐴 ) )
83 82 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( 𝐴 · ( ∗ ‘ 𝐶 ) ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( ( ∗ ‘ 𝐶 ) · 𝐴 ) ) )
84 22 38 36 13 mul4d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( ( ∗ ‘ 𝐶 ) · 𝐴 ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( ( ∗ ‘ 𝐷 ) · 𝐴 ) ) )
85 38 13 mulcomd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · 𝐴 ) = ( 𝐴 · ( ∗ ‘ 𝐷 ) ) )
86 85 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( ( ∗ ‘ 𝐷 ) · 𝐴 ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) )
87 83 84 86 3eqtrd ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( 𝐴 · ( ∗ ‘ 𝐶 ) ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) )
88 22 38 24 33 mul4d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( 𝐷 · ( ∗ ‘ 𝐵 ) ) ) = ( ( 𝐵 · 𝐷 ) · ( ( ∗ ‘ 𝐷 ) · ( ∗ ‘ 𝐵 ) ) ) )
89 33 24 mulcomd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐵 ) · 𝐷 ) = ( 𝐷 · ( ∗ ‘ 𝐵 ) ) )
90 89 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( 𝐷 · ( ∗ ‘ 𝐵 ) ) ) )
91 22 24 cjmuld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 · 𝐷 ) ) = ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ 𝐷 ) ) )
92 33 38 mulcomd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ 𝐷 ) ) = ( ( ∗ ‘ 𝐷 ) · ( ∗ ‘ 𝐵 ) ) )
93 91 92 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 · 𝐷 ) ) = ( ( ∗ ‘ 𝐷 ) · ( ∗ ‘ 𝐵 ) ) )
94 93 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 · 𝐷 ) · ( ∗ ‘ ( 𝐵 · 𝐷 ) ) ) = ( ( 𝐵 · 𝐷 ) · ( ( ∗ ‘ 𝐷 ) · ( ∗ ‘ 𝐵 ) ) ) )
95 88 90 94 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) = ( ( 𝐵 · 𝐷 ) · ( ∗ ‘ ( 𝐵 · 𝐷 ) ) ) )
96 95 26 eqtr4d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) = ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) )
97 87 96 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( 𝐴 · ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) = ( ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) )
98 81 97 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) = ( ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) )
99 80 98 oveq12d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) ) = ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) + ( ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) ) )
100 69 34 addcld ⊢ ( 𝜑 → ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ∈ ℂ )
101 32 54 100 adddird ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐷 ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) ) )
102 20 29 35 40 add42d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) + ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ) = ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) + ( ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) ) )
103 99 101 102 3eqtr4d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐶 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) = ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) + ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ) )
104 56 68 103 3eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ↑ 2 ) = ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) + ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ) )
105 31 24 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ∈ ℂ )
106 105 37 subcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ∈ ℂ )
107 106 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ↑ 2 ) = ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) · ( ∗ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ) )
108 cjsub ⊢ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ∈ ℂ ∧ ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ∈ ℂ ) → ( ∗ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) = ( ( ∗ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ) − ( ∗ ‘ ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) )
109 105 37 108 syl2anc ⊢ ( 𝜑 → ( ∗ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) = ( ( ∗ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ) − ( ∗ ‘ ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) )
110 31 24 cjmuld ⊢ ( 𝜑 → ( ∗ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) · ( ∗ ‘ 𝐷 ) ) )
111 59 oveq1d ⊢ ( 𝜑 → ( ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) · ( ∗ ‘ 𝐷 ) ) = ( 𝐴 · ( ∗ ‘ 𝐷 ) ) )
112 110 111 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ) = ( 𝐴 · ( ∗ ‘ 𝐷 ) ) )
113 22 36 cjmuld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) = ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ ( ∗ ‘ 𝐶 ) ) ) )
114 15 cjcjd ⊢ ( 𝜑 → ( ∗ ‘ ( ∗ ‘ 𝐶 ) ) = 𝐶 )
115 114 oveq2d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ ( ∗ ‘ 𝐶 ) ) ) = ( ( ∗ ‘ 𝐵 ) · 𝐶 ) )
116 113 115 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) = ( ( ∗ ‘ 𝐵 ) · 𝐶 ) )
117 112 116 oveq12d ⊢ ( 𝜑 → ( ( ∗ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ) − ( ∗ ‘ ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) )
118 109 117 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) )
119 118 oveq2d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) · ( ∗ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) )
120 33 15 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ∈ ℂ )
121 39 120 subcld ⊢ ( 𝜑 → ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ∈ ℂ )
122 105 37 121 subdird ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) − ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) ) )
123 105 39 120 subdid ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) )
124 24 31 13 38 mul4d ⊢ ( 𝜑 → ( ( 𝐷 · ( ∗ ‘ 𝐴 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) = ( ( 𝐷 · 𝐴 ) · ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐷 ) ) ) )
125 31 24 mulcomd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · 𝐷 ) = ( 𝐷 · ( ∗ ‘ 𝐴 ) ) )
126 125 oveq1d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) = ( ( 𝐷 · ( ∗ ‘ 𝐴 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) )
127 13 24 mulcomd ⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) = ( 𝐷 · 𝐴 ) )
128 13 24 cjmuld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 · 𝐷 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐷 ) ) )
129 127 128 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) · ( ∗ ‘ ( 𝐴 · 𝐷 ) ) ) = ( ( 𝐷 · 𝐴 ) · ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐷 ) ) ) )
130 124 126 129 3eqtr4d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) = ( ( 𝐴 · 𝐷 ) · ( ∗ ‘ ( 𝐴 · 𝐷 ) ) ) )
131 130 43 eqtr4d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) = ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) )
132 33 15 mulcomd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐵 ) · 𝐶 ) = ( 𝐶 · ( ∗ ‘ 𝐵 ) ) )
133 132 oveq2d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( 𝐶 · ( ∗ ‘ 𝐵 ) ) ) )
134 31 24 15 33 mul4d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( 𝐶 · ( ∗ ‘ 𝐵 ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( 𝐷 · ( ∗ ‘ 𝐵 ) ) ) )
135 24 33 mulcomd ⊢ ( 𝜑 → ( 𝐷 · ( ∗ ‘ 𝐵 ) ) = ( ( ∗ ‘ 𝐵 ) · 𝐷 ) )
136 135 oveq2d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( 𝐷 · ( ∗ ‘ 𝐵 ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) )
137 133 134 136 3eqtrd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) )
138 131 137 oveq12d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) = ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) − ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) )
139 123 138 eqtrd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) = ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) − ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) )
140 37 39 120 subdid ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) = ( ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) − ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) )
141 132 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐶 · ( ∗ ‘ 𝐵 ) ) ) )
142 22 36 15 33 mul4d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐶 · ( ∗ ‘ 𝐵 ) ) ) = ( ( 𝐵 · 𝐶 ) · ( ( ∗ ‘ 𝐶 ) · ( ∗ ‘ 𝐵 ) ) ) )
143 36 33 mulcomd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐶 ) · ( ∗ ‘ 𝐵 ) ) = ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ 𝐶 ) ) )
144 22 15 cjmuld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 · 𝐶 ) ) = ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ 𝐶 ) ) )
145 143 144 eqtr4d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐶 ) · ( ∗ ‘ 𝐵 ) ) = ( ∗ ‘ ( 𝐵 · 𝐶 ) ) )
146 145 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) · ( ( ∗ ‘ 𝐶 ) · ( ∗ ‘ 𝐵 ) ) ) = ( ( 𝐵 · 𝐶 ) · ( ∗ ‘ ( 𝐵 · 𝐶 ) ) ) )
147 141 142 146 3eqtrd ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) = ( ( 𝐵 · 𝐶 ) · ( ∗ ‘ ( 𝐵 · 𝐶 ) ) ) )
148 147 48 eqtr4d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) = ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) )
149 148 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) − ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) = ( ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) − ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
150 140 149 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) = ( ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) − ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
151 139 150 oveq12d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) · ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) − ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) ) = ( ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) − ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) − ( ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) − ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) ) )
152 46 35 40 51 subadd4d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) − ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) ) − ( ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) − ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) ) = ( ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) − ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ) )
153 122 151 152 3eqtrd ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) · ( ( 𝐴 · ( ∗ ‘ 𝐷 ) ) − ( ( ∗ ‘ 𝐵 ) · 𝐶 ) ) ) = ( ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) − ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ) )
154 107 119 153 3eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ↑ 2 ) = ( ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) − ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ) )
155 104 154 oveq12d ⊢ ( 𝜑 → ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ↑ 2 ) + ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ↑ 2 ) ) = ( ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) + ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ) + ( ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) − ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ) ) )
156 13 31 mulcld ⊢ ( 𝜑 → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
157 22 33 mulcld ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ∈ ℂ )
158 15 36 mulcld ⊢ ( 𝜑 → ( 𝐶 · ( ∗ ‘ 𝐶 ) ) ∈ ℂ )
159 24 38 mulcld ⊢ ( 𝜑 → ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ∈ ℂ )
160 158 159 addcld ⊢ ( 𝜑 → ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ∈ ℂ )
161 156 157 160 adddird ⊢ ( 𝜑 → ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) · ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) · ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) ) )
162 75 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) · ( ∗ ‘ ( 𝐴 · 𝐶 ) ) ) = ( ( 𝐴 · 𝐶 ) · ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐶 ) ) ) )
163 13 15 31 36 mul4d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) · ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐶 ) ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐶 · ( ∗ ‘ 𝐶 ) ) ) )
164 17 162 163 3eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐶 · ( ∗ ‘ 𝐶 ) ) ) )
165 128 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) · ( ∗ ‘ ( 𝐴 · 𝐷 ) ) ) = ( ( 𝐴 · 𝐷 ) · ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐷 ) ) ) )
166 13 24 31 38 mul4d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) · ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐷 ) ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) )
167 43 165 166 3eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) )
168 164 167 oveq12d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐶 · ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) )
169 156 158 159 adddid ⊢ ( 𝜑 → ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐶 · ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) )
170 168 169 eqtr4d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) )
171 144 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) · ( ∗ ‘ ( 𝐵 · 𝐶 ) ) ) = ( ( 𝐵 · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ 𝐶 ) ) ) )
172 22 15 33 36 mul4d ⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ 𝐶 ) ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) · ( 𝐶 · ( ∗ ‘ 𝐶 ) ) ) )
173 48 171 172 3eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) · ( 𝐶 · ( ∗ ‘ 𝐶 ) ) ) )
174 91 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 · 𝐷 ) · ( ∗ ‘ ( 𝐵 · 𝐷 ) ) ) = ( ( 𝐵 · 𝐷 ) · ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ 𝐷 ) ) ) )
175 22 24 33 38 mul4d ⊢ ( 𝜑 → ( ( 𝐵 · 𝐷 ) · ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ 𝐷 ) ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) · ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) )
176 26 174 175 3eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) = ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) · ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) )
177 173 176 oveq12d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) = ( ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) · ( 𝐶 · ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) · ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) )
178 157 158 159 adddid ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) · ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) · ( 𝐶 · ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) · ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) )
179 177 178 eqtr4d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) · ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) )
180 170 179 oveq12d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) ) + ( ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) · ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) ) )
181 161 180 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) · ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) = ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) ) + ( ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) ) )
182 13 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
183 22 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ 𝐵 ) ↑ 2 ) = ( 𝐵 · ( ∗ ‘ 𝐵 ) ) )
184 182 183 oveq12d ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) )
185 6 184 syl5eq ⊢ ( 𝜑 → 𝑋 = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) )
186 15 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) ↑ 2 ) = ( 𝐶 · ( ∗ ‘ 𝐶 ) ) )
187 24 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ 𝐷 ) ↑ 2 ) = ( 𝐷 · ( ∗ ‘ 𝐷 ) ) )
188 186 187 oveq12d ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 2 ) + ( ( abs ‘ 𝐷 ) ↑ 2 ) ) = ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) )
189 7 188 syl5eq ⊢ ( 𝜑 → 𝑌 = ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) )
190 185 189 oveq12d ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) · ( ( 𝐶 · ( ∗ ‘ 𝐶 ) ) + ( 𝐷 · ( ∗ ‘ 𝐷 ) ) ) ) )
191 20 29 46 51 add42d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) + ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) ) = ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) ) + ( ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) ) )
192 181 190 191 3eqtr4d ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) = ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) + ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) ) )
193 53 155 192 3eqtr4d ⊢ ( 𝜑 → ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ↑ 2 ) + ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ↑ 2 ) ) = ( 𝑋 · 𝑌 ) )
194 193 oveq1d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ↑ 2 ) + ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ↑ 2 ) ) / ( 𝑀 ↑ 2 ) ) = ( ( 𝑋 · 𝑌 ) / ( 𝑀 ↑ 2 ) ) )
195 8 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
196 8 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
197 55 195 196 absdivd ⊢ ( 𝜑 → ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) ) = ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) / ( abs ‘ 𝑀 ) ) )
198 8 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
199 8 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
200 199 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑀 )
201 198 200 absidd ⊢ ( 𝜑 → ( abs ‘ 𝑀 ) = 𝑀 )
202 201 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) / ( abs ‘ 𝑀 ) ) = ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) / 𝑀 ) )
203 197 202 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) ) = ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) / 𝑀 ) )
204 203 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) ) ↑ 2 ) = ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) / 𝑀 ) ↑ 2 ) )
205 55 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ∈ ℝ )
206 205 recnd ⊢ ( 𝜑 → ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ∈ ℂ )
207 206 195 196 sqdivd ⊢ ( 𝜑 → ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) / 𝑀 ) ↑ 2 ) = ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ↑ 2 ) / ( 𝑀 ↑ 2 ) ) )
208 204 207 eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) ) ↑ 2 ) = ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ↑ 2 ) / ( 𝑀 ↑ 2 ) ) )
209 106 195 196 absdivd ⊢ ( 𝜑 → ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) ) = ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) / ( abs ‘ 𝑀 ) ) )
210 201 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) / ( abs ‘ 𝑀 ) ) = ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) / 𝑀 ) )
211 209 210 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) ) = ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) / 𝑀 ) )
212 211 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) ) ↑ 2 ) = ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) / 𝑀 ) ↑ 2 ) )
213 106 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ∈ ℝ )
214 213 recnd ⊢ ( 𝜑 → ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ∈ ℂ )
215 214 195 196 sqdivd ⊢ ( 𝜑 → ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) / 𝑀 ) ↑ 2 ) = ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ↑ 2 ) / ( 𝑀 ↑ 2 ) ) )
216 212 215 eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) ) ↑ 2 ) = ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ↑ 2 ) / ( 𝑀 ↑ 2 ) ) )
217 208 216 oveq12d ⊢ ( 𝜑 → ( ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) ) ↑ 2 ) ) = ( ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ↑ 2 ) / ( 𝑀 ↑ 2 ) ) + ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ↑ 2 ) / ( 𝑀 ↑ 2 ) ) ) )
218 30 41 addcld ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 · 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) + ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ) ∈ ℂ )
219 104 218 eqeltrd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ↑ 2 ) ∈ ℂ )
220 52 41 subcld ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 · 𝐷 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) − ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) · ( ( ∗ ‘ 𝐵 ) · 𝐷 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐶 ) ) · ( 𝐴 · ( ∗ ‘ 𝐷 ) ) ) ) ) ∈ ℂ )
221 154 220 eqeltrd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ↑ 2 ) ∈ ℂ )
222 8 nnsqcld ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℕ )
223 222 nncnd ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℂ )
224 222 nnne0d ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ≠ 0 )
225 219 221 223 224 divdird ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ↑ 2 ) + ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ↑ 2 ) ) / ( 𝑀 ↑ 2 ) ) = ( ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ↑ 2 ) / ( 𝑀 ↑ 2 ) ) + ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ↑ 2 ) / ( 𝑀 ↑ 2 ) ) ) )
226 217 225 eqtr4d ⊢ ( 𝜑 → ( ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) ) ↑ 2 ) ) = ( ( ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ↑ 2 ) + ( ( abs ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) ) ↑ 2 ) ) / ( 𝑀 ↑ 2 ) ) )
227 182 156 eqeltrd ⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
228 183 157 eqeltrd ⊢ ( 𝜑 → ( ( abs ‘ 𝐵 ) ↑ 2 ) ∈ ℂ )
229 227 228 addcld ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) ∈ ℂ )
230 6 229 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
231 189 160 eqeltrd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
232 230 195 231 195 196 196 divmuldivd ⊢ ( 𝜑 → ( ( 𝑋 / 𝑀 ) · ( 𝑌 / 𝑀 ) ) = ( ( 𝑋 · 𝑌 ) / ( 𝑀 · 𝑀 ) ) )
233 195 sqvald ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) = ( 𝑀 · 𝑀 ) )
234 233 oveq2d ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) / ( 𝑀 ↑ 2 ) ) = ( ( 𝑋 · 𝑌 ) / ( 𝑀 · 𝑀 ) ) )
235 232 234 eqtr4d ⊢ ( 𝜑 → ( ( 𝑋 / 𝑀 ) · ( 𝑌 / 𝑀 ) ) = ( ( 𝑋 · 𝑌 ) / ( 𝑀 ↑ 2 ) ) )
236 194 226 235 3eqtr4d ⊢ ( 𝜑 → ( ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) ) ↑ 2 ) ) = ( ( 𝑋 / 𝑀 ) · ( 𝑌 / 𝑀 ) ) )
237 230 55 nncand ⊢ ( 𝜑 → ( 𝑋 − ( 𝑋 − ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) )
238 156 157 32 54 addsub4d ⊢ ( 𝜑 → ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · 𝐶 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) − ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) )
239 185 oveq1d ⊢ ( 𝜑 → ( 𝑋 − ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) )
240 31 13 15 subdid ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐴 ) − ( ( ∗ ‘ 𝐴 ) · 𝐶 ) ) )
241 31 13 mulcomd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · 𝐴 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
242 241 oveq1d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐴 ) − ( ( ∗ ‘ 𝐴 ) · 𝐶 ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · 𝐶 ) ) )
243 240 242 eqtrd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · 𝐶 ) ) )
244 cjsub ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ∗ ‘ ( 𝐵 − 𝐷 ) ) = ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐷 ) ) )
245 22 24 244 syl2anc ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 − 𝐷 ) ) = ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐷 ) ) )
246 245 oveq2d ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) = ( 𝐵 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐷 ) ) ) )
247 22 33 38 subdid ⊢ ( 𝜑 → ( 𝐵 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐷 ) ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) − ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) )
248 246 247 eqtrd ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) − ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) )
249 243 248 oveq12d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) + ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · 𝐶 ) ) + ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) − ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) )
250 238 239 249 3eqtr4d ⊢ ( 𝜑 → ( 𝑋 − ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) + ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) ) )
251 250 oveq2d ⊢ ( 𝜑 → ( 𝑋 − ( 𝑋 − ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) ) ) = ( 𝑋 − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) + ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) ) ) )
252 237 251 eqtr3d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) = ( 𝑋 − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) + ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) ) ) )
253 252 oveq1d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) = ( ( 𝑋 − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) + ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) ) ) / 𝑀 ) )
254 13 15 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ∈ ℂ )
255 31 254 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) ∈ ℂ )
256 22 24 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) ∈ ℂ )
257 256 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ∈ ℂ )
258 22 257 mulcld ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) ∈ ℂ )
259 255 258 addcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) + ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) ) ∈ ℂ )
260 230 259 195 196 divsubdird ⊢ ( 𝜑 → ( ( 𝑋 − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) + ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) ) ) / 𝑀 ) = ( ( 𝑋 / 𝑀 ) − ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) + ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) ) / 𝑀 ) ) )
261 255 258 195 196 divdird ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) + ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) ) / 𝑀 ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) / 𝑀 ) + ( ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) / 𝑀 ) ) )
262 31 254 195 196 divassd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) / 𝑀 ) = ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) )
263 22 257 195 196 divassd ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) / 𝑀 ) = ( 𝐵 · ( ( ∗ ‘ ( 𝐵 − 𝐷 ) ) / 𝑀 ) ) )
264 256 195 196 cjdivd ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) = ( ( ∗ ‘ ( 𝐵 − 𝐷 ) ) / ( ∗ ‘ 𝑀 ) ) )
265 198 cjred ⊢ ( 𝜑 → ( ∗ ‘ 𝑀 ) = 𝑀 )
266 265 oveq2d ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐵 − 𝐷 ) ) / ( ∗ ‘ 𝑀 ) ) = ( ( ∗ ‘ ( 𝐵 − 𝐷 ) ) / 𝑀 ) )
267 264 266 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) = ( ( ∗ ‘ ( 𝐵 − 𝐷 ) ) / 𝑀 ) )
268 267 oveq2d ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) = ( 𝐵 · ( ( ∗ ‘ ( 𝐵 − 𝐷 ) ) / 𝑀 ) ) )
269 263 268 eqtr4d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) / 𝑀 ) = ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) )
270 262 269 oveq12d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) / 𝑀 ) + ( ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) / 𝑀 ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) + ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ) )
271 261 270 eqtrd ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) + ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) ) / 𝑀 ) = ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) + ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ) )
272 271 oveq2d ⊢ ( 𝜑 → ( ( 𝑋 / 𝑀 ) − ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐴 − 𝐶 ) ) + ( 𝐵 · ( ∗ ‘ ( 𝐵 − 𝐷 ) ) ) ) / 𝑀 ) ) = ( ( 𝑋 / 𝑀 ) − ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) + ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ) ) )
273 253 260 272 3eqtrd ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) = ( ( 𝑋 / 𝑀 ) − ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) + ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ) ) )
274 11 nn0zd ⊢ ( 𝜑 → ( 𝑋 / 𝑀 ) ∈ ℤ )
275 zgz ⊢ ( ( 𝑋 / 𝑀 ) ∈ ℤ → ( 𝑋 / 𝑀 ) ∈ ℤ[i] )
276 274 275 syl ⊢ ( 𝜑 → ( 𝑋 / 𝑀 ) ∈ ℤ[i] )
277 gzcjcl ⊢ ( 𝐴 ∈ ℤ[i] → ( ∗ ‘ 𝐴 ) ∈ ℤ[i] )
278 2 277 syl ⊢ ( 𝜑 → ( ∗ ‘ 𝐴 ) ∈ ℤ[i] )
279 gzmulcl ⊢ ( ( ( ∗ ‘ 𝐴 ) ∈ ℤ[i] ∧ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ∈ ℤ[i] ) → ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ∈ ℤ[i] )
280 278 9 279 syl2anc ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ∈ ℤ[i] )
281 gzcjcl ⊢ ( ( ( 𝐵 − 𝐷 ) / 𝑀 ) ∈ ℤ[i] → ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ∈ ℤ[i] )
282 10 281 syl ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ∈ ℤ[i] )
283 gzmulcl ⊢ ( ( 𝐵 ∈ ℤ[i] ∧ ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ∈ ℤ[i] ) → ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ∈ ℤ[i] )
284 3 282 283 syl2anc ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ∈ ℤ[i] )
285 gzaddcl ⊢ ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ∈ ℤ[i] ∧ ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ∈ ℤ[i] ) → ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) + ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ) ∈ ℤ[i] )
286 280 284 285 syl2anc ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) + ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ) ∈ ℤ[i] )
287 gzsubcl ⊢ ( ( ( 𝑋 / 𝑀 ) ∈ ℤ[i] ∧ ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) + ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ) ∈ ℤ[i] ) → ( ( 𝑋 / 𝑀 ) − ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) + ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ) ) ∈ ℤ[i] )
288 276 286 287 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 / 𝑀 ) − ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) + ( 𝐵 · ( ∗ ‘ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ) ) ∈ ℤ[i] )
289 273 288 eqeltrd ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) ∈ ℤ[i] )
290 254 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ∈ ℂ )
291 22 290 mulcld ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ) ∈ ℂ )
292 31 256 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( 𝐵 − 𝐷 ) ) ∈ ℂ )
293 291 292 195 196 divsubdird ⊢ ( 𝜑 → ( ( ( 𝐵 · ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐵 − 𝐷 ) ) ) / 𝑀 ) = ( ( ( 𝐵 · ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ) / 𝑀 ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐵 − 𝐷 ) ) / 𝑀 ) ) )
294 cjsub ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 − 𝐶 ) ) = ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) )
295 13 15 294 syl2anc ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 − 𝐶 ) ) = ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) )
296 295 oveq2d ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ) = ( 𝐵 · ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) ) )
297 22 31 36 subdid ⊢ ( 𝜑 → ( 𝐵 · ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐴 ) ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) )
298 296 297 eqtrd ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐴 ) ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) )
299 31 22 24 subdid ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( 𝐵 − 𝐷 ) ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) − ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ) )
300 31 22 mulcomd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · 𝐵 ) = ( 𝐵 · ( ∗ ‘ 𝐴 ) ) )
301 300 oveq1d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) − ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ) )
302 299 301 eqtrd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( 𝐵 − 𝐷 ) ) = ( ( 𝐵 · ( ∗ ‘ 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ) )
303 298 302 oveq12d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐵 − 𝐷 ) ) ) = ( ( ( 𝐵 · ( ∗ ‘ 𝐴 ) ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) − ( ( 𝐵 · ( ∗ ‘ 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ) ) )
304 22 31 mulcld ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
305 304 37 105 nnncan1d ⊢ ( 𝜑 → ( ( ( 𝐵 · ( ∗ ‘ 𝐴 ) ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) − ( ( 𝐵 · ( ∗ ‘ 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · 𝐷 ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) )
306 303 305 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐵 − 𝐷 ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) )
307 306 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐵 · ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐵 − 𝐷 ) ) ) / 𝑀 ) = ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) )
308 293 307 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐵 · ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ) / 𝑀 ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐵 − 𝐷 ) ) / 𝑀 ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) )
309 22 290 195 196 divassd ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ) / 𝑀 ) = ( 𝐵 · ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) / 𝑀 ) ) )
310 254 195 196 cjdivd ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) = ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) / ( ∗ ‘ 𝑀 ) ) )
311 265 oveq2d ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) / ( ∗ ‘ 𝑀 ) ) = ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) / 𝑀 ) )
312 310 311 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) = ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) / 𝑀 ) )
313 312 oveq2d ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ) = ( 𝐵 · ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) / 𝑀 ) ) )
314 309 313 eqtr4d ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ) / 𝑀 ) = ( 𝐵 · ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ) )
315 31 256 195 196 divassd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐵 − 𝐷 ) ) / 𝑀 ) = ( ( ∗ ‘ 𝐴 ) · ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) )
316 314 315 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐵 · ( ∗ ‘ ( 𝐴 − 𝐶 ) ) ) / 𝑀 ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐵 − 𝐷 ) ) / 𝑀 ) ) = ( ( 𝐵 · ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ) − ( ( ∗ ‘ 𝐴 ) · ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) )
317 308 316 eqtr3d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) = ( ( 𝐵 · ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ) − ( ( ∗ ‘ 𝐴 ) · ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) )
318 gzcjcl ⊢ ( ( ( 𝐴 − 𝐶 ) / 𝑀 ) ∈ ℤ[i] → ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ∈ ℤ[i] )
319 9 318 syl ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ∈ ℤ[i] )
320 gzmulcl ⊢ ( ( 𝐵 ∈ ℤ[i] ∧ ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ∈ ℤ[i] ) → ( 𝐵 · ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ) ∈ ℤ[i] )
321 3 319 320 syl2anc ⊢ ( 𝜑 → ( 𝐵 · ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ) ∈ ℤ[i] )
322 gzmulcl ⊢ ( ( ( ∗ ‘ 𝐴 ) ∈ ℤ[i] ∧ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ∈ ℤ[i] ) → ( ( ∗ ‘ 𝐴 ) · ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ∈ ℤ[i] )
323 278 10 322 syl2anc ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ∈ ℤ[i] )
324 gzsubcl ⊢ ( ( ( 𝐵 · ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ) ∈ ℤ[i] ∧ ( ( ∗ ‘ 𝐴 ) · ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ∈ ℤ[i] ) → ( ( 𝐵 · ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ) − ( ( ∗ ‘ 𝐴 ) · ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ∈ ℤ[i] )
325 321 323 324 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 · ( ∗ ‘ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ) ) − ( ( ∗ ‘ 𝐴 ) · ( ( 𝐵 − 𝐷 ) / 𝑀 ) ) ) ∈ ℤ[i] )
326 317 325 eqeltrd ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) ∈ ℤ[i] )
327 1 4sqlem4a ⊢ ( ( ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) ∈ ℤ[i] ∧ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) ∈ ℤ[i] ) → ( ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) ) ↑ 2 ) ) ∈ 𝑆 )
328 289 326 327 syl2anc ⊢ ( 𝜑 → ( ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐶 ) + ( 𝐵 · ( ∗ ‘ 𝐷 ) ) ) / 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( ( ( ( ∗ ‘ 𝐴 ) · 𝐷 ) − ( 𝐵 · ( ∗ ‘ 𝐶 ) ) ) / 𝑀 ) ) ↑ 2 ) ) ∈ 𝑆 )
329 236 328 eqeltrrd ⊢ ( 𝜑 → ( ( 𝑋 / 𝑀 ) · ( 𝑌 / 𝑀 ) ) ∈ 𝑆 )