Metamath Proof Explorer

Theorem inlinecirc02p

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. (Contributed by AV, 9-May-2023) (Revised 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 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 ) )

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 3 ovexi 
 |-  P e. _V
9 8 a1i 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> P e. _V )
10 simpl 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( X e. P /\ Y e. P /\ X =/= Y ) )
11 simpl 
 |-  ( ( R e. RR+ /\ ( X D .0. ) < R ) -> R e. RR+ )
12 11 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> R e. RR+ )
13 1 3 rrx2pxel 
 |-  ( X e. P -> ( X ` 1 ) e. RR )
14 13 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X ` 1 ) e. RR )
15 14 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( X ` 1 ) e. RR )
16 1 3 rrx2pyel 
 |-  ( X e. P -> ( X ` 2 ) e. RR )
17 16 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X ` 2 ) e. RR )
18 17 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( X ` 2 ) e. RR )
19 1 3 rrx2pxel 
 |-  ( Y e. P -> ( Y ` 1 ) e. RR )
20 19 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( Y ` 1 ) e. RR )
21 20 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( Y ` 1 ) e. RR )
22 1 3 rrx2pyel 
 |-  ( Y e. P -> ( Y ` 2 ) e. RR )
23 22 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( Y ` 2 ) e. RR )
24 23 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( Y ` 2 ) e. RR )
25 eqid 
 |-  ( ( Y ` 1 ) - ( X ` 1 ) ) = ( ( Y ` 1 ) - ( X ` 1 ) )
26 eqid 
 |-  ( ( X ` 2 ) - ( Y ` 2 ) ) = ( ( X ` 2 ) - ( Y ` 2 ) )
27 eqid 
 |-  ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) )
28 rpre 
 |-  ( R e. RR+ -> R e. RR )
29 28 adantr 
 |-  ( ( R e. RR+ /\ ( X D .0. ) < R ) -> R e. RR )
30 29 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> R e. RR )
31 2nn0 
 |-  2 e. NN0
32 eqid 
 |-  ( EEhil ` 2 ) = ( EEhil ` 2 )
33 32 ehlval 
 |-  ( 2 e. NN0 -> ( EEhil ` 2 ) = ( RR^ ` ( 1 ... 2 ) ) )
34 31 33 ax-mp 
 |-  ( EEhil ` 2 ) = ( RR^ ` ( 1 ... 2 ) )
35 fz12pr 
 |-  ( 1 ... 2 ) = { 1 , 2 }
36 35 1 eqtr4i 
 |-  ( 1 ... 2 ) = I
37 36 fveq2i 
 |-  ( RR^ ` ( 1 ... 2 ) ) = ( RR^ ` I )
38 34 37 eqtri 
 |-  ( EEhil ` 2 ) = ( RR^ ` I )
39 2 38 eqtr4i 
 |-  E = ( EEhil ` 2 )
40 1 oveq2i 
 |-  ( RR ^m I ) = ( RR ^m { 1 , 2 } )
41 3 40 eqtri 
 |-  P = ( RR ^m { 1 , 2 } )
42 1 xpeq1i 
 |-  ( I X. { 0 } ) = ( { 1 , 2 } X. { 0 } )
43 5 42 eqtri 
 |-  .0. = ( { 1 , 2 } X. { 0 } )
44 39 41 7 43 ehl2eudis0lt 
 |-  ( ( X e. P /\ R e. RR+ ) -> ( ( X D .0. ) < R <-> ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) < ( R ^ 2 ) ) )
45 44 3ad2antl1 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ R e. RR+ ) -> ( ( X D .0. ) < R <-> ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) < ( R ^ 2 ) ) )
46 45 biimpd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ R e. RR+ ) -> ( ( X D .0. ) < R -> ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) < ( R ^ 2 ) ) )
47 46 impr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) < ( R ^ 2 ) )
48 1 3 rrx2pnecoorneor 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( X ` 1 ) =/= ( Y ` 1 ) \/ ( X ` 2 ) =/= ( Y ` 2 ) ) )
49 48 orcomd 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( X ` 2 ) =/= ( Y ` 2 ) \/ ( X ` 1 ) =/= ( Y ` 1 ) ) )
50 49 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( X ` 2 ) =/= ( Y ` 2 ) \/ ( X ` 1 ) =/= ( Y ` 1 ) ) )
51 eqid 
 |-  ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) = ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) )
52 eqid 
 |-  ( ( ( R ^ 2 ) x. ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) ) - ( ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) ) ^ 2 ) ) = ( ( ( R ^ 2 ) x. ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) ) - ( ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) ) ^ 2 ) )
53 15 18 21 24 25 26 27 30 47 50 51 52 2itscp 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> 0 < ( ( ( R ^ 2 ) x. ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) ) - ( ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) ) ^ 2 ) ) )
54 19 recnd 
 |-  ( Y e. P -> ( Y ` 1 ) e. CC )
55 54 adantl 
 |-  ( ( X e. P /\ Y e. P ) -> ( Y ` 1 ) e. CC )
56 13 recnd 
 |-  ( X e. P -> ( X ` 1 ) e. CC )
57 56 adantr 
 |-  ( ( X e. P /\ Y e. P ) -> ( X ` 1 ) e. CC )
58 16 recnd 
 |-  ( X e. P -> ( X ` 2 ) e. CC )
59 58 adantr 
 |-  ( ( X e. P /\ Y e. P ) -> ( X ` 2 ) e. CC )
60 55 57 59 subdird 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) = ( ( ( Y ` 1 ) x. ( X ` 2 ) ) - ( ( X ` 1 ) x. ( X ` 2 ) ) ) )
61 22 recnd 
 |-  ( Y e. P -> ( Y ` 2 ) e. CC )
62 61 adantl 
 |-  ( ( X e. P /\ Y e. P ) -> ( Y ` 2 ) e. CC )
63 59 62 57 subdird 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) = ( ( ( X ` 2 ) x. ( X ` 1 ) ) - ( ( Y ` 2 ) x. ( X ` 1 ) ) ) )
64 60 63 oveq12d 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) ) = ( ( ( ( Y ` 1 ) x. ( X ` 2 ) ) - ( ( X ` 1 ) x. ( X ` 2 ) ) ) + ( ( ( X ` 2 ) x. ( X ` 1 ) ) - ( ( Y ` 2 ) x. ( X ` 1 ) ) ) ) )
65 55 59 mulcomd 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( Y ` 1 ) x. ( X ` 2 ) ) = ( ( X ` 2 ) x. ( Y ` 1 ) ) )
66 65 oveq1d 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( Y ` 1 ) x. ( X ` 2 ) ) - ( ( X ` 1 ) x. ( X ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( X ` 2 ) ) ) )
67 59 57 mulcomd 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 2 ) x. ( X ` 1 ) ) = ( ( X ` 1 ) x. ( X ` 2 ) ) )
68 62 57 mulcomd 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( Y ` 2 ) x. ( X ` 1 ) ) = ( ( X ` 1 ) x. ( Y ` 2 ) ) )
69 67 68 oveq12d 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( X ` 2 ) x. ( X ` 1 ) ) - ( ( Y ` 2 ) x. ( X ` 1 ) ) ) = ( ( ( X ` 1 ) x. ( X ` 2 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) )
70 66 69 oveq12d 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( ( Y ` 1 ) x. ( X ` 2 ) ) - ( ( X ` 1 ) x. ( X ` 2 ) ) ) + ( ( ( X ` 2 ) x. ( X ` 1 ) ) - ( ( Y ` 2 ) x. ( X ` 1 ) ) ) ) = ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( X ` 2 ) ) ) + ( ( ( X ` 1 ) x. ( X ` 2 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) )
71 59 55 mulcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 2 ) x. ( Y ` 1 ) ) e. CC )
72 57 59 mulcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 1 ) x. ( X ` 2 ) ) e. CC )
73 57 62 mulcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 1 ) x. ( Y ` 2 ) ) e. CC )
74 71 72 73 npncand 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( X ` 2 ) ) ) + ( ( ( X ` 1 ) x. ( X ` 2 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) )
75 64 70 74 3eqtrd 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) )
76 75 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) )
77 76 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) )
78 77 eqcomd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) ) )
79 78 oveq1d 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) = ( ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) ) ^ 2 ) )
80 79 oveq2d 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( R ^ 2 ) x. ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) ) - ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) ) = ( ( ( R ^ 2 ) x. ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) ) - ( ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( X ` 2 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( X ` 1 ) ) ) ^ 2 ) ) )
81 53 80 breqtrrd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> 0 < ( ( ( R ^ 2 ) x. ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) ) - ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) ) )
82 eqid 
 |-  ( ( ( R ^ 2 ) x. ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) ) - ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) ) = ( ( ( R ^ 2 ) x. ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) ) - ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) )
83 eqid 
 |-  ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) )
84 1 2 3 4 5 6 51 82 26 25 83 inlinecirc02plem 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 < ( ( ( R ^ 2 ) x. ( ( ( ( X ` 2 ) - ( Y ` 2 ) ) ^ 2 ) + ( ( ( Y ` 1 ) - ( X ` 1 ) ) ^ 2 ) ) ) - ( ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ^ 2 ) ) ) ) -> E. a e. P E. b e. P ( ( ( .0. S R ) i^i ( X L Y ) ) = { a , b } /\ a =/= b ) )
85 10 12 81 84 syl12anc 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> E. a e. P E. b e. P ( ( ( .0. S R ) i^i ( X L Y ) ) = { a , b } /\ a =/= b ) )
86 prprelprb 
 |-  ( ( ( .0. S R ) i^i ( X L Y ) ) e. ( PrPairs ` P ) <-> ( P e. _V /\ E. a e. P E. b e. P ( ( ( .0. S R ) i^i ( X L Y ) ) = { a , b } /\ a =/= b ) ) )
87 9 85 86 sylanbrc 
 |-  ( ( ( 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 ) )