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 
|- ( ph -> A e. RR )
2itscp.b 
|- ( ph -> B e. RR )
2itscp.x 
|- ( ph -> X e. RR )
2itscp.y 
|- ( ph -> Y e. RR )
2itscp.d 
|- D = ( X - A )
2itscp.e 
|- E = ( B - Y )
2itscp.c 
|- C = ( ( D x. B ) + ( E x. A ) )
2itscp.r 
|- ( ph -> R e. RR )
2itscp.l 
|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) )
2itscp.n 
|- ( ph -> ( B =/= Y \/ A =/= X ) )
2itscp.q 
|- Q = ( ( E ^ 2 ) + ( D ^ 2 ) )
2itscp.s 
|- S = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
Assertion 2itscp 
|- ( ph -> 0 < S )

Proof

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