Metamath Proof Explorer

Theorem itscnhlinecirc02p

Description: Intersection of a nonhorizontal line with a circle: A nonhorizontal line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 28-Jan-2023)

Ref Expression
Hypotheses itscnhlinecirc02p.i 
|- I = { 1 , 2 }
itscnhlinecirc02p.e 
|- E = ( RR^ ` I )
itscnhlinecirc02p.p 
|- P = ( RR ^m I )
itscnhlinecirc02p.s 
|- S = ( Sphere ` E )
itscnhlinecirc02p.0 
|- .0. = ( I X. { 0 } )
itscnhlinecirc02p.l 
|- L = ( LineM ` E )
itscnhlinecirc02p.d 
|- D = ( dist ` E )
itscnhlinecirc02p.z 
|- Z = { <. 1 , x >. , <. 2 , y >. }
Assertion itscnhlinecirc02p 
|- ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> E! s e. ~P RR ( ( # ` s ) = 2 /\ A. y e. s E! x e. RR ( Z e. ( .0. S R ) /\ Z e. ( X L Y ) ) ) )

Proof

Step Hyp Ref Expression
1 itscnhlinecirc02p.i 
 |-  I = { 1 , 2 }
2 itscnhlinecirc02p.e 
 |-  E = ( RR^ ` I )
3 itscnhlinecirc02p.p 
 |-  P = ( RR ^m I )
4 itscnhlinecirc02p.s 
 |-  S = ( Sphere ` E )
5 itscnhlinecirc02p.0 
 |-  .0. = ( I X. { 0 } )
6 itscnhlinecirc02p.l 
 |-  L = ( LineM ` E )
7 itscnhlinecirc02p.d 
 |-  D = ( dist ` E )
8 itscnhlinecirc02p.z 
 |-  Z = { <. 1 , x >. , <. 2 , y >. }
9 1 2 3 4 5 6 7 itscnhlinecirc02plem3 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> 0 < ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
10 1 3 rrx2pyel 
 |-  ( X e. P -> ( X ` 2 ) e. RR )
11 10 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( X ` 2 ) e. RR )
12 11 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( X ` 2 ) e. RR )
13 1 3 rrx2pyel 
 |-  ( Y e. P -> ( Y ` 2 ) e. RR )
14 13 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( Y ` 2 ) e. RR )
15 14 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( Y ` 2 ) e. RR )
16 12 15 resubcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( X ` 2 ) - ( Y ` 2 ) ) e. RR )
17 16 resqcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) e. RR )
18 1 3 rrx2pxel 
 |-  ( Y e. P -> ( Y ` 1 ) e. RR )
19 18 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( Y ` 1 ) e. RR )
20 19 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( Y ` 1 ) e. RR )
21 1 3 rrx2pxel 
 |-  ( X e. P -> ( X ` 1 ) e. RR )
22 21 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( X ` 1 ) e. RR )
23 22 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( X ` 1 ) e. RR )
24 20 23 resubcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( Y ` 1 ) - ( X ` 1 ) ) e. RR )
25 24 resqcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) e. RR )
26 17 25 readdcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) e. RR )
27 11 14 resubcld 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( ( X ` 2 ) - ( Y ` 2 ) ) e. RR )
28 27 resqcld 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) e. RR )
29 19 22 resubcld 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( ( Y ` 1 ) - ( X ` 1 ) ) e. RR )
30 29 resqcld 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) e. RR )
31 11 recnd 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( X ` 2 ) e. CC )
32 14 recnd 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( Y ` 2 ) e. CC )
33 simp3 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( X ` 2 ) =/= ( Y ` 2 ) )
34 31 32 33 subne0d 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( ( X ` 2 ) - ( Y ` 2 ) ) =/= 0 )
35 27 34 sqgt0d 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> 0 < ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) )
36 29 sqge0d 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> 0 <_ ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) )
37 28 30 35 36 addgtge0d 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> 0 < ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) )
38 37 gt0ne0d 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) =/= 0 )
39 38 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) =/= 0 )
40 2re 
 |-  2 e. RR
41 40 a1i 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> 2 e. RR )
42 12 20 remulcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( X ` 2 ) x. ( Y ` 1 ) ) e. RR )
43 23 15 remulcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( X ` 1 ) x. ( Y ` 2 ) ) e. RR )
44 42 43 resubcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) e. RR )
45 24 44 remulcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) e. RR )
46 41 45 remulcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) e. RR )
47 46 renegcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) e. RR )
48 44 resqcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) e. RR )
49 rpre 
 |-  ( R e. RR+ -> R e. RR )
50 49 adantr 
 |-  ( ( R e. RR+ /\ ( X D .0. ) < R ) -> R e. RR )
51 50 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> R e. RR )
52 51 resqcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( R ^ 2 ) e. RR )
53 17 52 remulcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) e. RR )
54 48 53 resubcld 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) e. RR )
55 eqidd 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) = ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
56 26 39 47 54 55 requad2 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( E! s e. ~P RR ( ( # ` s ) = 2 /\ A. y e. s ( ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( y ^ 2 ) ) + ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) x. y ) + ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 ) <-> 0 < ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) )
57 9 56 mpbird 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> E! s e. ~P RR ( ( # ` s ) = 2 /\ A. y e. s ( ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( y ^ 2 ) ) + ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) x. y ) + ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 ) )
58 0xr 
 |-  0 e. RR*
59 58 a1i 
 |-  ( R e. RR+ -> 0 e. RR* )
60 pnfxr 
 |-  +oo e. RR*
61 60 a1i 
 |-  ( R e. RR+ -> +oo e. RR* )
62 rpxr 
 |-  ( R e. RR+ -> R e. RR* )
63 rpge0 
 |-  ( R e. RR+ -> 0 <_ R )
64 ltpnf 
 |-  ( R e. RR -> R < +oo )
65 49 64 syl 
 |-  ( R e. RR+ -> R < +oo )
66 59 61 62 63 65 elicod 
 |-  ( R e. RR+ -> R e. ( 0 [,) +oo ) )
67 eqid 
 |-  { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) }
68 1 2 3 4 5 67 2sphere0 
 |-  ( R e. ( 0 [,) +oo ) -> ( .0. S R ) = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } )
69 66 68 syl 
 |-  ( R e. RR+ -> ( .0. S R ) = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } )
70 69 adantr 
 |-  ( ( R e. RR+ /\ ( X D .0. ) < R ) -> ( .0. S R ) = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } )
71 70 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( .0. S R ) = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } )
72 71 adantr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) -> ( .0. S R ) = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } )
73 72 adantr 
 |-  ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) -> ( .0. S R ) = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } )
74 73 adantr 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( .0. S R ) = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } )
75 74 adantr 
 |-  ( ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) /\ x e. RR ) -> ( .0. S R ) = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } )
76 75 eleq2d 
 |-  ( ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) /\ x e. RR ) -> ( Z e. ( .0. S R ) <-> Z e. { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } ) )
77 fveq1 
 |-  ( p = Z -> ( p ` 1 ) = ( Z ` 1 ) )
78 8 fveq1i 
 |-  ( Z ` 1 ) = ( { <. 1 , x >. , <. 2 , y >. } ` 1 )
79 1ne2 
 |-  1 =/= 2
80 1ex 
 |-  1 e. _V
81 vex 
 |-  x e. _V
82 80 81 fvpr1 
 |-  ( 1 =/= 2 -> ( { <. 1 , x >. , <. 2 , y >. } ` 1 ) = x )
83 79 82 ax-mp 
 |-  ( { <. 1 , x >. , <. 2 , y >. } ` 1 ) = x
84 78 83 eqtri 
 |-  ( Z ` 1 ) = x
85 84 a1i 
 |-  ( p = Z -> ( Z ` 1 ) = x )
86 77 85 eqtrd 
 |-  ( p = Z -> ( p ` 1 ) = x )
87 86 oveq1d 
 |-  ( p = Z -> ( ( p ` 1 ) ^ 2 ) = ( x ^ 2 ) )
88 fveq1 
 |-  ( p = Z -> ( p ` 2 ) = ( Z ` 2 ) )
89 8 fveq1i 
 |-  ( Z ` 2 ) = ( { <. 1 , x >. , <. 2 , y >. } ` 2 )
90 2ex 
 |-  2 e. _V
91 vex 
 |-  y e. _V
92 90 91 fvpr2 
 |-  ( 1 =/= 2 -> ( { <. 1 , x >. , <. 2 , y >. } ` 2 ) = y )
93 79 92 ax-mp 
 |-  ( { <. 1 , x >. , <. 2 , y >. } ` 2 ) = y
94 89 93 eqtri 
 |-  ( Z ` 2 ) = y
95 94 a1i 
 |-  ( p = Z -> ( Z ` 2 ) = y )
96 88 95 eqtrd 
 |-  ( p = Z -> ( p ` 2 ) = y )
97 96 oveq1d 
 |-  ( p = Z -> ( ( p ` 2 ) ^ 2 ) = ( y ^ 2 ) )
98 87 97 oveq12d 
 |-  ( p = Z -> ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
99 98 eqeq1d 
 |-  ( p = Z -> ( ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) <-> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) )
100 99 elrab 
 |-  ( Z e. { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } <-> ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) )
101 100 a1i 
 |-  ( ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) /\ x e. RR ) -> ( Z e. { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } <-> ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) ) )
102 76 101 bitrd 
 |-  ( ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) /\ x e. RR ) -> ( Z e. ( .0. S R ) <-> ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) ) )
103 simp1 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> X e. P )
104 simp2 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> Y e. P )
105 fveq1 
 |-  ( X = Y -> ( X ` 2 ) = ( Y ` 2 ) )
106 105 a1i 
 |-  ( ( X e. P /\ Y e. P ) -> ( X = Y -> ( X ` 2 ) = ( Y ` 2 ) ) )
107 106 necon3d 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 2 ) =/= ( Y ` 2 ) -> X =/= Y ) )
108 107 ex 
 |-  ( X e. P -> ( Y e. P -> ( ( X ` 2 ) =/= ( Y ` 2 ) -> X =/= Y ) ) )
109 108 3imp 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> X =/= Y )
110 103 104 109 3jca 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( X e. P /\ Y e. P /\ X =/= Y ) )
111 110 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( X e. P /\ Y e. P /\ X =/= Y ) )
112 111 adantr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) -> ( X e. P /\ Y e. P /\ X =/= Y ) )
113 112 adantr 
 |-  ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) -> ( X e. P /\ Y e. P /\ X =/= Y ) )
114 113 adantr 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( X e. P /\ Y e. P /\ X =/= Y ) )
115 114 adantr 
 |-  ( ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) /\ x e. RR ) -> ( X e. P /\ Y e. P /\ X =/= Y ) )
116 eqid 
 |-  ( ( X ` 2 ) - ( Y ` 2 ) ) = ( ( X ` 2 ) - ( Y ` 2 ) )
117 eqid 
 |-  ( ( Y ` 1 ) - ( X ` 1 ) ) = ( ( Y ` 1 ) - ( X ` 1 ) )
118 eqid 
 |-  ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) )
119 1 2 3 6 116 117 118 rrx2linest2 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) } )
120 115 119 syl 
 |-  ( ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) /\ x e. RR ) -> ( X L Y ) = { p e. P | ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) } )
121 120 eleq2d 
 |-  ( ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) /\ x e. RR ) -> ( Z e. ( X L Y ) <-> Z e. { p e. P | ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) } ) )
122 86 oveq2d 
 |-  ( p = Z -> ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( p ` 1 ) ) = ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) )
123 96 oveq2d 
 |-  ( p = Z -> ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) = ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) )
124 122 123 oveq12d 
 |-  ( p = Z -> ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) ) = ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) )
125 124 eqeq1d 
 |-  ( p = Z -> ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) <-> ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) )
126 125 elrab 
 |-  ( Z e. { p e. P | ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) } <-> ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) )
127 126 a1i 
 |-  ( ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) /\ x e. RR ) -> ( Z e. { p e. P | ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) } <-> ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) )
128 121 127 bitrd 
 |-  ( ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) /\ x e. RR ) -> ( Z e. ( X L Y ) <-> ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) )
129 102 128 anbi12d 
 |-  ( ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) /\ x e. RR ) -> ( ( Z e. ( .0. S R ) /\ Z e. ( X L Y ) ) <-> ( ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) /\ ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) ) )
130 129 reubidva 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( E! x e. RR ( Z e. ( .0. S R ) /\ Z e. ( X L Y ) ) <-> E! x e. RR ( ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) /\ ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) ) )
131 elelpwi 
 |-  ( ( y e. s /\ s e. ~P RR ) -> y e. RR )
132 1 3 prelrrx2 
 |-  ( ( x e. RR /\ y e. RR ) -> { <. 1 , x >. , <. 2 , y >. } e. P )
133 132 ancoms 
 |-  ( ( y e. RR /\ x e. RR ) -> { <. 1 , x >. , <. 2 , y >. } e. P )
134 8 eleq1i 
 |-  ( Z e. P <-> { <. 1 , x >. , <. 2 , y >. } e. P )
135 133 134 sylibr 
 |-  ( ( y e. RR /\ x e. RR ) -> Z e. P )
136 135 biantrurd 
 |-  ( ( y e. RR /\ x e. RR ) -> ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) <-> ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) ) )
137 136 bicomd 
 |-  ( ( y e. RR /\ x e. RR ) -> ( ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) <-> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) )
138 135 biantrurd 
 |-  ( ( y e. RR /\ x e. RR ) -> ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) <-> ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) )
139 138 bicomd 
 |-  ( ( y e. RR /\ x e. RR ) -> ( ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) <-> ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) )
140 137 139 anbi12d 
 |-  ( ( y e. RR /\ x e. RR ) -> ( ( ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) /\ ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) <-> ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) )
141 140 reubidva 
 |-  ( y e. RR -> ( E! x e. RR ( ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) /\ ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) <-> E! x e. RR ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) )
142 131 141 syl 
 |-  ( ( y e. s /\ s e. ~P RR ) -> ( E! x e. RR ( ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) /\ ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) <-> E! x e. RR ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) )
143 142 expcom 
 |-  ( s e. ~P RR -> ( y e. s -> ( E! x e. RR ( ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) /\ ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) <-> E! x e. RR ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) ) )
144 143 adantl 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) -> ( y e. s -> ( E! x e. RR ( ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) /\ ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) <-> E! x e. RR ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) ) )
145 144 adantr 
 |-  ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) -> ( y e. s -> ( E! x e. RR ( ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) /\ ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) <-> E! x e. RR ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) ) )
146 145 imp 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( E! x e. RR ( ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) /\ ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) <-> E! x e. RR ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) )
147 27 34 jca 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( ( ( X ` 2 ) - ( Y ` 2 ) ) e. RR /\ ( ( X ` 2 ) - ( Y ` 2 ) ) =/= 0 ) )
148 147 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( X ` 2 ) - ( Y ` 2 ) ) e. RR /\ ( ( X ` 2 ) - ( Y ` 2 ) ) =/= 0 ) )
149 148 ad3antrrr 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( ( ( X ` 2 ) - ( Y ` 2 ) ) e. RR /\ ( ( X ` 2 ) - ( Y ` 2 ) ) =/= 0 ) )
150 20 ad3antrrr 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( Y ` 1 ) e. RR )
151 23 ad3antrrr 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( X ` 1 ) e. RR )
152 150 151 resubcld 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( ( Y ` 1 ) - ( X ` 1 ) ) e. RR )
153 12 ad3antrrr 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( X ` 2 ) e. RR )
154 153 150 remulcld 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( ( X ` 2 ) x. ( Y ` 1 ) ) e. RR )
155 15 ad3antrrr 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( Y ` 2 ) e. RR )
156 151 155 remulcld 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( ( X ` 1 ) x. ( Y ` 2 ) ) e. RR )
157 154 156 resubcld 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) e. RR )
158 149 152 157 3jca 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) e. RR /\ ( ( X ` 2 ) - ( Y ` 2 ) ) =/= 0 ) /\ ( ( Y ` 1 ) - ( X ` 1 ) ) e. RR /\ ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) e. RR ) )
159 simplrl 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) -> R e. RR+ )
160 159 adantr 
 |-  ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) -> R e. RR+ )
161 160 adantr 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> R e. RR+ )
162 131 expcom 
 |-  ( s e. ~P RR -> ( y e. s -> y e. RR ) )
163 162 adantl 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) -> ( y e. s -> y e. RR ) )
164 163 adantr 
 |-  ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) -> ( y e. s -> y e. RR ) )
165 164 imp 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> y e. RR )
166 158 161 165 3jca 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) e. RR /\ ( ( X ` 2 ) - ( Y ` 2 ) ) =/= 0 ) /\ ( ( Y ` 1 ) - ( X ` 1 ) ) e. RR /\ ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) e. RR ) /\ R e. RR+ /\ y e. RR ) )
167 eqid 
 |-  ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) = ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) )
168 eqid 
 |-  -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) = -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) )
169 eqid 
 |-  ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) = ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) )
170 167 168 169 itsclquadeu 
 |-  ( ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) e. RR /\ ( ( X ` 2 ) - ( Y ` 2 ) ) =/= 0 ) /\ ( ( Y ` 1 ) - ( X ` 1 ) ) e. RR /\ ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) e. RR ) /\ R e. RR+ /\ y e. RR ) -> ( E! x e. RR ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) <-> ( ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( y ^ 2 ) ) + ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) x. y ) + ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 ) )
171 166 170 syl 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( E! x e. RR ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) <-> ( ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( y ^ 2 ) ) + ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) x. y ) + ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 ) )
172 146 171 bitrd 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( E! x e. RR ( ( Z e. P /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( R ^ 2 ) ) /\ ( Z e. P /\ ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. x ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. y ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) <-> ( ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( y ^ 2 ) ) + ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) x. y ) + ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 ) )
173 130 172 bitrd 
 |-  ( ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) /\ y e. s ) -> ( E! x e. RR ( Z e. ( .0. S R ) /\ Z e. ( X L Y ) ) <-> ( ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( y ^ 2 ) ) + ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) x. y ) + ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 ) )
174 173 ralbidva 
 |-  ( ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) /\ ( # ` s ) = 2 ) -> ( A. y e. s E! x e. RR ( Z e. ( .0. S R ) /\ Z e. ( X L Y ) ) <-> A. y e. s ( ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( y ^ 2 ) ) + ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) x. y ) + ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 ) )
175 174 pm5.32da 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) /\ s e. ~P RR ) -> ( ( ( # ` s ) = 2 /\ A. y e. s E! x e. RR ( Z e. ( .0. S R ) /\ Z e. ( X L Y ) ) ) <-> ( ( # ` s ) = 2 /\ A. y e. s ( ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( y ^ 2 ) ) + ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) x. y ) + ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 ) ) )
176 175 reubidva 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( E! s e. ~P RR ( ( # ` s ) = 2 /\ A. y e. s E! x e. RR ( Z e. ( .0. S R ) /\ Z e. ( X L Y ) ) ) <-> E! s e. ~P RR ( ( # ` s ) = 2 /\ A. y e. s ( ( ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) x. ( y ^ 2 ) ) + ( ( -u ( 2 x. ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) x. y ) + ( ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) - ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 ) ) )
177 57 176 mpbird 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> E! s e. ~P RR ( ( # ` s ) = 2 /\ A. y e. s E! x e. RR ( Z e. ( .0. S R ) /\ Z e. ( X L Y ) ) ) )