Metamath Proof Explorer

Theorem 2itscp

Description: A condition for a quadratic equation with real coefficients (for the intersection points of a line with a circle) to have (exactly) two different real solutions. (Contributed by AV, 5-Mar-2023) (Revised by AV, 16-May-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 ) )
2itscp.n ⊢ ( 𝜑 → ( 𝐵 ≠ 𝑌 ∨ 𝐴 ≠ 𝑋 ) )
2itscp.q ⊢ 𝑄 = ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) )
2itscp.s ⊢ 𝑆 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
Assertion 2itscp ( 𝜑 → 0 < 𝑆 )

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 2itscp.n ⊢ ( 𝜑 → ( 𝐵 ≠ 𝑌 ∨ 𝐴 ≠ 𝑋 ) )
11 2itscp.q ⊢ 𝑄 = ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) )
12 2itscp.s ⊢ 𝑆 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
13 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝑌 ) → 𝐵 ∈ ℂ )
15 4 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝑌 ) → 𝑌 ∈ ℂ )
17 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝑌 ) → 𝐵 ≠ 𝑌 )
18 14 16 17 subne0d ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝑌 ) → ( 𝐵 − 𝑌 ) ≠ 0 )
19 18 ex ⊢ ( 𝜑 → ( 𝐵 ≠ 𝑌 → ( 𝐵 − 𝑌 ) ≠ 0 ) )
20 3 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑋 ) → 𝑋 ∈ ℂ )
22 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑋 ) → 𝐴 ∈ ℂ )
24 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑋 ) → 𝐴 ≠ 𝑋 )
25 24 necomd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑋 ) → 𝑋 ≠ 𝐴 )
26 21 23 25 subne0d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑋 ) → ( 𝑋 − 𝐴 ) ≠ 0 )
27 26 ex ⊢ ( 𝜑 → ( 𝐴 ≠ 𝑋 → ( 𝑋 − 𝐴 ) ≠ 0 ) )
28 6 neeq1i ⊢ ( 𝐸 ≠ 0 ↔ ( 𝐵 − 𝑌 ) ≠ 0 )
29 5 neeq1i ⊢ ( 𝐷 ≠ 0 ↔ ( 𝑋 − 𝐴 ) ≠ 0 )
30 28 29 anbi12i ⊢ ( ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ↔ ( ( 𝐵 − 𝑌 ) ≠ 0 ∧ ( 𝑋 − 𝐴 ) ≠ 0 ) )
31 2re ⊢ 2 ∈ ℝ
32 31 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
33 3 1 resubcld ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ∈ ℝ )
34 5 33 eqeltrid ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
35 34 1 remulcld ⊢ ( 𝜑 → ( 𝐷 · 𝐴 ) ∈ ℝ )
36 2 4 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) ∈ ℝ )
37 6 36 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
38 37 2 remulcld ⊢ ( 𝜑 → ( 𝐸 · 𝐵 ) ∈ ℝ )
39 35 38 remulcld ⊢ ( 𝜑 → ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ∈ ℝ )
40 32 39 remulcld ⊢ ( 𝜑 → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ∈ ℝ )
41 40 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ∈ ℝ )
42 37 resqcld ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ )
43 2 resqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℝ )
44 42 43 remulcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ∈ ℝ )
45 34 resqcld ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℝ )
46 1 resqcld ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℝ )
47 45 46 remulcld ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ∈ ℝ )
48 44 47 readdcld ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) ∈ ℝ )
49 48 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) ∈ ℝ )
50 8 resqcld ⊢ ( 𝜑 → ( 𝑅 ↑ 2 ) ∈ ℝ )
51 50 46 resubcld ⊢ ( 𝜑 → ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ∈ ℝ )
52 42 51 remulcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) ∈ ℝ )
53 50 43 resubcld ⊢ ( 𝜑 → ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℝ )
54 45 53 remulcld ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ∈ ℝ )
55 52 54 readdcld ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ∈ ℝ )
56 55 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ∈ ℝ )
57 35 38 resubcld ⊢ ( 𝜑 → ( ( 𝐷 · 𝐴 ) − ( 𝐸 · 𝐵 ) ) ∈ ℝ )
58 57 sqge0d ⊢ ( 𝜑 → 0 ≤ ( ( ( 𝐷 · 𝐴 ) − ( 𝐸 · 𝐵 ) ) ↑ 2 ) )
59 1 2 3 4 5 6 2itscplem1 ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) = ( ( ( 𝐷 · 𝐴 ) − ( 𝐸 · 𝐵 ) ) ↑ 2 ) )
60 58 59 breqtrrd ⊢ ( 𝜑 → 0 ≤ ( ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) )
61 48 40 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) ↔ ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ≤ ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) ) )
62 60 61 mpbid ⊢ ( 𝜑 → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ≤ ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )
63 62 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ≤ ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )
64 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ∈ ℝ )
65 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ∈ ℝ )
66 52 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) ∈ ℝ )
67 54 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ∈ ℝ )
68 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
69 51 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ∈ ℝ )
70 simpl ⊢ ( ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) → 𝐸 ≠ 0 )
71 sqn0rp ⊢ ( ( 𝐸 ∈ ℝ ∧ 𝐸 ≠ 0 ) → ( 𝐸 ↑ 2 ) ∈ ℝ+ )
72 37 70 71 syl2an ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( 𝐸 ↑ 2 ) ∈ ℝ+ )
73 46 43 50 ltaddsub2d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ↔ ( 𝐵 ↑ 2 ) < ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) )
74 9 73 mpbid ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) < ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( 𝐵 ↑ 2 ) < ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) )
76 68 69 72 75 ltmul2dd ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) < ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) )
77 46 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
78 53 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℝ )
79 simpr ⊢ ( ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) → 𝐷 ≠ 0 )
80 sqn0rp ⊢ ( ( 𝐷 ∈ ℝ ∧ 𝐷 ≠ 0 ) → ( 𝐷 ↑ 2 ) ∈ ℝ+ )
81 34 79 80 syl2an ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( 𝐷 ↑ 2 ) ∈ ℝ+ )
82 46 43 50 ltaddsubd ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ↔ ( 𝐴 ↑ 2 ) < ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
83 9 82 mpbid ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) < ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
84 83 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( 𝐴 ↑ 2 ) < ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
85 77 78 81 84 ltmul2dd ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) < ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
86 64 65 66 67 76 85 lt2addd ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
87 41 49 56 63 86 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
88 87 ex ⊢ ( 𝜑 → ( ( 𝐸 ≠ 0 ∧ 𝐷 ≠ 0 ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ) )
89 30 88 biimtrrid ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑌 ) ≠ 0 ∧ ( 𝑋 − 𝐴 ) ≠ 0 ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ) )
90 19 27 89 syl2and ⊢ ( 𝜑 → ( ( 𝐵 ≠ 𝑌 ∧ 𝐴 ≠ 𝑋 ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ) )
91 90 imp ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝑌 ∧ 𝐴 ≠ 𝑋 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
92 nne ⊢ ( ¬ 𝐴 ≠ 𝑋 ↔ 𝐴 = 𝑋 )
93 eqcom ⊢ ( 𝐴 = 𝑋 ↔ 𝑋 = 𝐴 )
94 20 22 subeq0ad ⊢ ( 𝜑 → ( ( 𝑋 − 𝐴 ) = 0 ↔ 𝑋 = 𝐴 ) )
95 94 biimprd ⊢ ( 𝜑 → ( 𝑋 = 𝐴 → ( 𝑋 − 𝐴 ) = 0 ) )
96 93 95 biimtrid ⊢ ( 𝜑 → ( 𝐴 = 𝑋 → ( 𝑋 − 𝐴 ) = 0 ) )
97 92 96 biimtrid ⊢ ( 𝜑 → ( ¬ 𝐴 ≠ 𝑋 → ( 𝑋 − 𝐴 ) = 0 ) )
98 5 eqeq1i ⊢ ( 𝐷 = 0 ↔ ( 𝑋 − 𝐴 ) = 0 )
99 28 98 anbi12i ⊢ ( ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ↔ ( ( 𝐵 − 𝑌 ) ≠ 0 ∧ ( 𝑋 − 𝐴 ) = 0 ) )
100 0red ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → 0 ∈ ℝ )
101 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ∈ ℝ )
102 52 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) ∈ ℝ )
103 37 sqge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐸 ↑ 2 ) )
104 2 sqge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐵 ↑ 2 ) )
105 42 43 103 104 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
106 105 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → 0 ≤ ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
107 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
108 51 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ∈ ℝ )
109 simprl ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → 𝐸 ≠ 0 )
110 37 109 71 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( 𝐸 ↑ 2 ) ∈ ℝ+ )
111 74 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( 𝐵 ↑ 2 ) < ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) )
112 107 108 110 111 ltmul2dd ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) < ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) )
113 100 101 102 106 112 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → 0 < ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) )
114 oveq1 ⊢ ( 𝐷 = 0 → ( 𝐷 · 𝐴 ) = ( 0 · 𝐴 ) )
115 114 adantl ⊢ ( ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) → ( 𝐷 · 𝐴 ) = ( 0 · 𝐴 ) )
116 22 mul02d ⊢ ( 𝜑 → ( 0 · 𝐴 ) = 0 )
117 115 116 sylan9eqr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( 𝐷 · 𝐴 ) = 0 )
118 117 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) = ( 0 · ( 𝐸 · 𝐵 ) ) )
119 38 recnd ⊢ ( 𝜑 → ( 𝐸 · 𝐵 ) ∈ ℂ )
120 119 mul02d ⊢ ( 𝜑 → ( 0 · ( 𝐸 · 𝐵 ) ) = 0 )
121 120 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( 0 · ( 𝐸 · 𝐵 ) ) = 0 )
122 118 121 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) = 0 )
123 122 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) = ( 2 · 0 ) )
124 2t0e0 ⊢ ( 2 · 0 ) = 0
125 123 124 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) = 0 )
126 sq0i ⊢ ( 𝐷 = 0 → ( 𝐷 ↑ 2 ) = 0 )
127 126 adantl ⊢ ( ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) → ( 𝐷 ↑ 2 ) = 0 )
128 127 adantl ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( 𝐷 ↑ 2 ) = 0 )
129 128 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = ( 0 · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
130 53 recnd ⊢ ( 𝜑 → ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℂ )
131 130 mul02d ⊢ ( 𝜑 → ( 0 · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = 0 )
132 131 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( 0 · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = 0 )
133 129 132 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = 0 )
134 133 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) = ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + 0 ) )
135 52 recnd ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
136 135 addridd ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + 0 ) = ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) )
137 136 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + 0 ) = ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) )
138 134 137 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) = ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) )
139 113 125 138 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
140 139 ex ⊢ ( 𝜑 → ( ( 𝐸 ≠ 0 ∧ 𝐷 = 0 ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ) )
141 99 140 biimtrrid ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑌 ) ≠ 0 ∧ ( 𝑋 − 𝐴 ) = 0 ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ) )
142 19 97 141 syl2and ⊢ ( 𝜑 → ( ( 𝐵 ≠ 𝑌 ∧ ¬ 𝐴 ≠ 𝑋 ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ) )
143 142 imp ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝑌 ∧ ¬ 𝐴 ≠ 𝑋 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
144 nne ⊢ ( ¬ 𝐵 ≠ 𝑌 ↔ 𝐵 = 𝑌 )
145 13 15 subeq0ad ⊢ ( 𝜑 → ( ( 𝐵 − 𝑌 ) = 0 ↔ 𝐵 = 𝑌 ) )
146 145 biimprd ⊢ ( 𝜑 → ( 𝐵 = 𝑌 → ( 𝐵 − 𝑌 ) = 0 ) )
147 144 146 biimtrid ⊢ ( 𝜑 → ( ¬ 𝐵 ≠ 𝑌 → ( 𝐵 − 𝑌 ) = 0 ) )
148 6 eqeq1i ⊢ ( 𝐸 = 0 ↔ ( 𝐵 − 𝑌 ) = 0 )
149 148 29 anbi12i ⊢ ( ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ↔ ( ( 𝐵 − 𝑌 ) = 0 ∧ ( 𝑋 − 𝐴 ) ≠ 0 ) )
150 0red ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → 0 ∈ ℝ )
151 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ∈ ℝ )
152 54 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ∈ ℝ )
153 34 sqge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐷 ↑ 2 ) )
154 1 sqge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐴 ↑ 2 ) )
155 45 46 153 154 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
156 155 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → 0 ≤ ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
157 46 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
158 53 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℝ )
159 simprr ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → 𝐷 ≠ 0 )
160 34 159 80 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( 𝐷 ↑ 2 ) ∈ ℝ+ )
161 43 recnd ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
162 46 recnd ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
163 161 162 addcomd ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
164 163 9 eqbrtrd ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) )
165 43 46 50 ltaddsub2d ⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ↔ ( 𝐴 ↑ 2 ) < ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
166 164 165 mpbid ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) < ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
167 166 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( 𝐴 ↑ 2 ) < ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
168 157 158 160 167 ltmul2dd ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) < ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
169 150 151 152 156 168 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → 0 < ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
170 oveq1 ⊢ ( 𝐸 = 0 → ( 𝐸 · 𝐵 ) = ( 0 · 𝐵 ) )
171 170 adantr ⊢ ( ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) → ( 𝐸 · 𝐵 ) = ( 0 · 𝐵 ) )
172 13 mul02d ⊢ ( 𝜑 → ( 0 · 𝐵 ) = 0 )
173 171 172 sylan9eqr ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( 𝐸 · 𝐵 ) = 0 )
174 173 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) = ( ( 𝐷 · 𝐴 ) · 0 ) )
175 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → 𝐷 ∈ ℝ )
176 175 recnd ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → 𝐷 ∈ ℂ )
177 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → 𝐴 ∈ ℂ )
178 176 177 mulcld ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( 𝐷 · 𝐴 ) ∈ ℂ )
179 178 mul01d ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐷 · 𝐴 ) · 0 ) = 0 )
180 174 179 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) = 0 )
181 180 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) = ( 2 · 0 ) )
182 181 124 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) = 0 )
183 sq0i ⊢ ( 𝐸 = 0 → ( 𝐸 ↑ 2 ) = 0 )
184 183 adantr ⊢ ( ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) → ( 𝐸 ↑ 2 ) = 0 )
185 184 adantl ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( 𝐸 ↑ 2 ) = 0 )
186 185 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) = ( 0 · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) )
187 51 recnd ⊢ ( 𝜑 → ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
188 187 mul02d ⊢ ( 𝜑 → ( 0 · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) = 0 )
189 188 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( 0 · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) = 0 )
190 186 189 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) = 0 )
191 190 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) = ( 0 + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
192 54 recnd ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ∈ ℂ )
193 192 addlidd ⊢ ( 𝜑 → ( 0 + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) = ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
194 193 adantr ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( 0 + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) = ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
195 191 194 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) = ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
196 169 182 195 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
197 196 ex ⊢ ( 𝜑 → ( ( 𝐸 = 0 ∧ 𝐷 ≠ 0 ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ) )
198 149 197 biimtrrid ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑌 ) = 0 ∧ ( 𝑋 − 𝐴 ) ≠ 0 ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ) )
199 147 27 198 syl2and ⊢ ( 𝜑 → ( ( ¬ 𝐵 ≠ 𝑌 ∧ 𝐴 ≠ 𝑋 ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ) )
200 199 imp ⊢ ( ( 𝜑 ∧ ( ¬ 𝐵 ≠ 𝑌 ∧ 𝐴 ≠ 𝑋 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
201 ioran ⊢ ( ¬ ( 𝐵 ≠ 𝑌 ∨ 𝐴 ≠ 𝑋 ) ↔ ( ¬ 𝐵 ≠ 𝑌 ∧ ¬ 𝐴 ≠ 𝑋 ) )
202 10 pm2.24d ⊢ ( 𝜑 → ( ¬ ( 𝐵 ≠ 𝑌 ∨ 𝐴 ≠ 𝑋 ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ) )
203 201 202 biimtrrid ⊢ ( 𝜑 → ( ( ¬ 𝐵 ≠ 𝑌 ∧ ¬ 𝐴 ≠ 𝑋 ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ) )
204 203 imp ⊢ ( ( 𝜑 ∧ ( ¬ 𝐵 ≠ 𝑌 ∧ ¬ 𝐴 ≠ 𝑋 ) ) → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
205 91 143 200 204 4casesdan ⊢ ( 𝜑 → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
206 40 55 posdifd ⊢ ( 𝜑 → ( ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) < ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) ↔ 0 < ( ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) ) )
207 205 206 mpbid ⊢ ( 𝜑 → 0 < ( ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) )
208 1 2 3 4 5 6 7 8 11 12 2itscplem3 ⊢ ( 𝜑 → 𝑆 = ( ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) )
209 207 208 breqtrrd ⊢ ( 𝜑 → 0 < 𝑆 )