Metamath Proof Explorer

Theorem itscnhlinecirc02plem1

Description: Lemma 1 for itscnhlinecirc02p . (Contributed by AV, 6-Mar-2023)

Ref Expression
Hypotheses 2itscp.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2itscp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
2itscp.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2itscp.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
2itscp.d ⊢ 𝐷 = ( 𝑋 − 𝐴 )
2itscp.e ⊢ 𝐸 = ( 𝐵 − 𝑌 )
2itscp.c ⊢ 𝐶 = ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) )
2itscp.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
2itscp.l ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) )
itscnhlinecirc02plem1.n ⊢ ( 𝜑 → 𝐵 ≠ 𝑌 )
Assertion itscnhlinecirc02plem1 ( 𝜑 → 0 < ( ( - ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 2itscp.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 2itscp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 2itscp.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
4 2itscp.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
5 2itscp.d ⊢ 𝐷 = ( 𝑋 − 𝐴 )
6 2itscp.e ⊢ 𝐸 = ( 𝐵 − 𝑌 )
7 2itscp.c ⊢ 𝐶 = ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) )
8 2itscp.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
9 2itscp.l ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) )
10 itscnhlinecirc02plem1.n ⊢ ( 𝜑 → 𝐵 ≠ 𝑌 )
11 4re ⊢ 4 ∈ ℝ
12 11 a1i ⊢ ( 𝜑 → 4 ∈ ℝ )
13 3 1 resubcld ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ∈ ℝ )
14 5 13 eqeltrid ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
15 14 resqcld ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℝ )
16 14 2 remulcld ⊢ ( 𝜑 → ( 𝐷 · 𝐵 ) ∈ ℝ )
17 2 4 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) ∈ ℝ )
18 6 17 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
19 18 1 remulcld ⊢ ( 𝜑 → ( 𝐸 · 𝐴 ) ∈ ℝ )
20 16 19 readdcld ⊢ ( 𝜑 → ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ∈ ℝ )
21 7 20 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
22 21 resqcld ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℝ )
23 15 22 remulcld ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ∈ ℝ )
24 18 resqcld ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ )
25 24 15 readdcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℝ )
26 8 resqcld ⊢ ( 𝜑 → ( 𝑅 ↑ 2 ) ∈ ℝ )
27 24 26 remulcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℝ )
28 22 27 resubcld ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℝ )
29 25 28 remulcld ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ∈ ℝ )
30 23 29 resubcld ⊢ ( 𝜑 → ( ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ∈ ℝ )
31 4pos ⊢ 0 < 4
32 31 a1i ⊢ ( 𝜑 → 0 < 4 )
33 15 26 remulcld ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℝ )
34 27 33 readdcld ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℝ )
35 34 22 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( 𝐶 ↑ 2 ) ) ∈ ℝ )
36 6 a1i ⊢ ( 𝜑 → 𝐸 = ( 𝐵 − 𝑌 ) )
37 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
38 4 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
39 37 38 10 subne0d ⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) ≠ 0 )
40 36 39 eqnetrd ⊢ ( 𝜑 → 𝐸 ≠ 0 )
41 18 40 sqgt0d ⊢ ( 𝜑 → 0 < ( 𝐸 ↑ 2 ) )
42 10 orcd ⊢ ( 𝜑 → ( 𝐵 ≠ 𝑌 ∨ 𝐴 ≠ 𝑋 ) )
43 eqid ⊢ ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) )
44 eqid ⊢ ( ( ( 𝑅 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝐶 ↑ 2 ) ) = ( ( ( 𝑅 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝐶 ↑ 2 ) )
45 1 2 3 4 5 6 7 8 9 42 43 44 2itscp ⊢ ( 𝜑 → 0 < ( ( ( 𝑅 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝐶 ↑ 2 ) ) )
46 24 recnd ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
47 15 recnd ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℂ )
48 26 recnd ⊢ ( 𝜑 → ( 𝑅 ↑ 2 ) ∈ ℂ )
49 46 47 48 adddird ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) = ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) )
50 46 47 addcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℂ )
51 50 48 mulcomd ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) = ( ( 𝑅 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
52 49 51 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) = ( ( 𝑅 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
53 52 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( 𝐶 ↑ 2 ) ) = ( ( ( 𝑅 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝐶 ↑ 2 ) ) )
54 45 53 breqtrrd ⊢ ( 𝜑 → 0 < ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( 𝐶 ↑ 2 ) ) )
55 24 35 41 54 mulgt0d ⊢ ( 𝜑 → 0 < ( ( 𝐸 ↑ 2 ) · ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( 𝐶 ↑ 2 ) ) ) )
56 47 46 48 mul12d ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) = ( ( 𝐸 ↑ 2 ) · ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) )
57 56 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( ( 𝐸 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐸 ↑ 2 ) · ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
58 46 48 mulcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ )
59 47 48 mulcld ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ )
60 46 58 59 adddid ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( ( 𝐸 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐸 ↑ 2 ) · ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
61 57 60 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( 𝐸 ↑ 2 ) · ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
62 61 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) = ( ( ( 𝐸 ↑ 2 ) · ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
63 58 59 addcld ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℂ )
64 22 recnd ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
65 46 63 64 subdid ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( 𝐶 ↑ 2 ) ) ) = ( ( ( 𝐸 ↑ 2 ) · ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
66 62 65 eqtr4d ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) = ( ( 𝐸 ↑ 2 ) · ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( 𝐶 ↑ 2 ) ) ) )
67 55 66 breqtrrd ⊢ ( 𝜑 → 0 < ( ( ( ( 𝐸 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
68 18 recnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
69 68 sqcld ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
70 14 recnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
71 70 sqcld ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℂ )
72 27 recnd ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ )
73 mulsubaddmulsub ⊢ ( ( ( ( 𝐸 ↑ 2 ) ∈ ℂ ∧ ( 𝐷 ↑ 2 ) ∈ ℂ ) ∧ ( ( 𝐶 ↑ 2 ) ∈ ℂ ∧ ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ ) ) → ( ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = ( ( ( ( 𝐸 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
74 69 71 64 72 73 syl22anc ⊢ ( 𝜑 → ( ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = ( ( ( ( 𝐸 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
75 67 74 breqtrrd ⊢ ( 𝜑 → 0 < ( ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) )
76 12 30 32 75 mulgt0d ⊢ ( 𝜑 → 0 < ( 4 · ( ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
77 4cn ⊢ 4 ∈ ℂ
78 77 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
79 21 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
80 79 sqcld ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
81 71 80 mulcld ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ∈ ℂ )
82 69 71 addcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℂ )
83 8 recnd ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
84 83 sqcld ⊢ ( 𝜑 → ( 𝑅 ↑ 2 ) ∈ ℂ )
85 69 84 mulcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ )
86 80 85 subcld ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℂ )
87 82 86 mulcld ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ∈ ℂ )
88 78 81 87 subdid ⊢ ( 𝜑 → ( 4 · ( ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) = ( ( 4 · ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
89 76 88 breqtrd ⊢ ( 𝜑 → 0 < ( ( 4 · ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
90 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
91 70 79 mulcld ⊢ ( 𝜑 → ( 𝐷 · 𝐶 ) ∈ ℂ )
92 90 91 mulcld ⊢ ( 𝜑 → ( 2 · ( 𝐷 · 𝐶 ) ) ∈ ℂ )
93 sqneg ⊢ ( ( 2 · ( 𝐷 · 𝐶 ) ) ∈ ℂ → ( - ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) = ( ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) )
94 92 93 syl ⊢ ( 𝜑 → ( - ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) = ( ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) )
95 90 91 sqmuld ⊢ ( 𝜑 → ( ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( ( 𝐷 · 𝐶 ) ↑ 2 ) ) )
96 sq2 ⊢ ( 2 ↑ 2 ) = 4
97 96 a1i ⊢ ( 𝜑 → ( 2 ↑ 2 ) = 4 )
98 70 79 sqmuld ⊢ ( 𝜑 → ( ( 𝐷 · 𝐶 ) ↑ 2 ) = ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) )
99 97 98 oveq12d ⊢ ( 𝜑 → ( ( 2 ↑ 2 ) · ( ( 𝐷 · 𝐶 ) ↑ 2 ) ) = ( 4 · ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
100 94 95 99 3eqtrd ⊢ ( 𝜑 → ( - ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) = ( 4 · ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
101 100 oveq1d ⊢ ( 𝜑 → ( ( - ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) = ( ( 4 · ( ( 𝐷 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
102 89 101 breqtrrd ⊢ ( 𝜑 → 0 < ( ( - ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )