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 = ( 0 ..^ 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 )
Assertion itscnhlinecirc02p 
|- ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> E! s e. ~P RR ( ( # ` s ) = 2 /\ A. y e. s E! x e. RR ( <" x y "> e. ( .0. S R ) /\ <" x y "> e. ( X L Y ) ) ) )

Proof

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