Metamath Proof Explorer

Theorem itscnhlinecirc02plem2

Description: Lemma 2 for itscnhlinecirc02p . (Contributed by AV, 10-Mar-2023)

Ref Expression
Hypotheses itscnhlinecirc02plem2.d 
|- D = ( X - A )
itscnhlinecirc02plem2.e 
|- E = ( B - Y )
itscnhlinecirc02plem2.c 
|- C = ( ( B x. X ) - ( A x. Y ) )
Assertion itscnhlinecirc02plem2 
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) /\ B =/= Y ) /\ ( R e. RR /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) ) ) -> 0 < ( ( -u ( 2 x. ( D x. C ) ) ^ 2 ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 itscnhlinecirc02plem2.d 
 |-  D = ( X - A )
2 itscnhlinecirc02plem2.e 
 |-  E = ( B - Y )
3 itscnhlinecirc02plem2.c 
 |-  C = ( ( B x. X ) - ( A x. Y ) )
4 simpl1l 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) /\ B =/= Y ) /\ ( R e. RR /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) ) ) -> A e. RR )
5 simpl1r 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) /\ B =/= Y ) /\ ( R e. RR /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) ) ) -> B e. RR )
6 simpl2l 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) /\ B =/= Y ) /\ ( R e. RR /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) ) ) -> X e. RR )
7 simpl2r 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) /\ B =/= Y ) /\ ( R e. RR /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) ) ) -> Y e. RR )
8 eqid 
 |-  ( ( D x. B ) + ( E x. A ) ) = ( ( D x. B ) + ( E x. A ) )
9 simprl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) /\ B =/= Y ) /\ ( R e. RR /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) ) ) -> R e. RR )
10 simprr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) /\ B =/= Y ) /\ ( R e. RR /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) )
11 simpl3 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) /\ B =/= Y ) /\ ( R e. RR /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) ) ) -> B =/= Y )
12 4 5 6 7 1 2 8 9 10 11 itscnhlinecirc02plem1 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) /\ B =/= Y ) /\ ( R e. RR /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) ) ) -> 0 < ( ( -u ( 2 x. ( D x. ( ( D x. B ) + ( E x. A ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( ( ( D x. B ) + ( E x. A ) ) ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
13 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> B e. RR )
14 13 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> B e. CC )
15 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> X e. RR )
16 15 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> X e. CC )
17 14 16 mulcomd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( B x. X ) = ( X x. B ) )
18 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> A e. RR )
19 18 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> A e. CC )
20 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> Y e. RR )
21 20 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> Y e. CC )
22 19 21 mulcomd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( A x. Y ) = ( Y x. A ) )
23 17 22 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. X ) - ( A x. Y ) ) = ( ( X x. B ) - ( Y x. A ) ) )
24 16 19 14 subdird 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( X - A ) x. B ) = ( ( X x. B ) - ( A x. B ) ) )
25 14 21 19 subdird 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B - Y ) x. A ) = ( ( B x. A ) - ( Y x. A ) ) )
26 24 25 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( X - A ) x. B ) + ( ( B - Y ) x. A ) ) = ( ( ( X x. B ) - ( A x. B ) ) + ( ( B x. A ) - ( Y x. A ) ) ) )
27 14 19 mulcomd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( B x. A ) = ( A x. B ) )
28 27 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. A ) - ( Y x. A ) ) = ( ( A x. B ) - ( Y x. A ) ) )
29 28 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( X x. B ) - ( A x. B ) ) + ( ( B x. A ) - ( Y x. A ) ) ) = ( ( ( X x. B ) - ( A x. B ) ) + ( ( A x. B ) - ( Y x. A ) ) ) )
30 16 14 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( X x. B ) e. CC )
31 19 14 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( A x. B ) e. CC )
32 21 19 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Y x. A ) e. CC )
33 30 31 32 npncand 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( X x. B ) - ( A x. B ) ) + ( ( A x. B ) - ( Y x. A ) ) ) = ( ( X x. B ) - ( Y x. A ) ) )
34 26 29 33 3eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( X - A ) x. B ) + ( ( B - Y ) x. A ) ) = ( ( X x. B ) - ( Y x. A ) ) )
35 23 34 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. X ) - ( A x. Y ) ) = ( ( ( X - A ) x. B ) + ( ( B - Y ) x. A ) ) )
36 1 oveq1i 
 |-  ( D x. B ) = ( ( X - A ) x. B )
37 2 oveq1i 
 |-  ( E x. A ) = ( ( B - Y ) x. A )
38 36 37 oveq12i 
 |-  ( ( D x. B ) + ( E x. A ) ) = ( ( ( X - A ) x. B ) + ( ( B - Y ) x. A ) )
39 35 3 38 3eqtr4g 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> C = ( ( D x. B ) + ( E x. A ) ) )
40 39 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( D x. C ) = ( D x. ( ( D x. B ) + ( E x. A ) ) ) )
41 40 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( 2 x. ( D x. C ) ) = ( 2 x. ( D x. ( ( D x. B ) + ( E x. A ) ) ) ) )
42 41 negeqd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> -u ( 2 x. ( D x. C ) ) = -u ( 2 x. ( D x. ( ( D x. B ) + ( E x. A ) ) ) ) )
43 42 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( -u ( 2 x. ( D x. C ) ) ^ 2 ) = ( -u ( 2 x. ( D x. ( ( D x. B ) + ( E x. A ) ) ) ) ^ 2 ) )
44 39 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( C ^ 2 ) = ( ( ( D x. B ) + ( E x. A ) ) ^ 2 ) )
45 44 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) = ( ( ( ( D x. B ) + ( E x. A ) ) ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) )
46 45 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( ( ( D x. B ) + ( E x. A ) ) ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) )
47 46 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( ( ( D x. B ) + ( E x. A ) ) ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) )
48 43 47 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( -u ( 2 x. ( D x. C ) ) ^ 2 ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) = ( ( -u ( 2 x. ( D x. ( ( D x. B ) + ( E x. A ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( ( ( D x. B ) + ( E x. A ) ) ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
49 48 3adant3 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) /\ B =/= Y ) -> ( ( -u ( 2 x. ( D x. C ) ) ^ 2 ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) = ( ( -u ( 2 x. ( D x. ( ( D x. B ) + ( E x. A ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( ( ( D x. B ) + ( E x. A ) ) ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
50 49 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) /\ B =/= Y ) /\ ( R e. RR /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) ) ) -> ( ( -u ( 2 x. ( D x. C ) ) ^ 2 ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) = ( ( -u ( 2 x. ( D x. ( ( D x. B ) + ( E x. A ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( ( ( D x. B ) + ( E x. A ) ) ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
51 12 50 breqtrrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) /\ B =/= Y ) /\ ( R e. RR /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) ) ) -> 0 < ( ( -u ( 2 x. ( D x. C ) ) ^ 2 ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )