Metamath Proof Explorer

Theorem inlinecirc02preu

Description: Intersection of a line with a circle: A line passing through a point within a circle around the origin intersects the circle at exactly two different points, expressed with restricted uniqueness (and without the definition of proper pairs). (Contributed by AV, 16-May-2023)

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

Proof

Step Hyp Ref Expression
1 inlinecirc02p.i 
 |-  I = { 1 , 2 }
2 inlinecirc02p.e 
 |-  E = ( RR^ ` I )
3 inlinecirc02p.p 
 |-  P = ( RR ^m I )
4 inlinecirc02p.s 
 |-  S = ( Sphere ` E )
5 inlinecirc02p.0 
 |-  .0. = ( I X. { 0 } )
6 inlinecirc02p.l 
 |-  L = ( LineM ` E )
7 inlinecirc02p.d 
 |-  D = ( dist ` E )
8 1 2 3 4 5 6 7 inlinecirc02p 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( .0. S R ) i^i ( X L Y ) ) e. ( PrPairs ` P ) )
9 reueq 
 |-  ( ( ( .0. S R ) i^i ( X L Y ) ) e. ( PrPairs ` P ) <-> E! p e. ( PrPairs ` P ) p = ( ( .0. S R ) i^i ( X L Y ) ) )
10 8 9 sylib 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> E! p e. ( PrPairs ` P ) p = ( ( .0. S R ) i^i ( X L Y ) ) )
11 3 ovexi 
 |-  P e. _V
12 prprreueq 
 |-  ( P e. _V -> ( E! p e. ( PrPairs ` P ) p = ( ( .0. S R ) i^i ( X L Y ) ) <-> E! p e. ~P P ( ( # ` p ) = 2 /\ p = ( ( .0. S R ) i^i ( X L Y ) ) ) ) )
13 11 12 mp1i 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( E! p e. ( PrPairs ` P ) p = ( ( .0. S R ) i^i ( X L Y ) ) <-> E! p e. ~P P ( ( # ` p ) = 2 /\ p = ( ( .0. S R ) i^i ( X L Y ) ) ) ) )
14 10 13 mpbid 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> E! p e. ~P P ( ( # ` p ) = 2 /\ p = ( ( .0. S R ) i^i ( X L Y ) ) ) )