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