Metamath Proof Explorer

Theorem itscnhlinecirc02plem3

Description: Lemma 3 for itscnhlinecirc02p . (Contributed by AV, 10-Mar-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 )
Assertion 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 ) ) ) ) ) ) )

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 1 3 rrx2pxel 
 |-  ( X e. P -> ( X ` 1 ) e. RR )
9 1 3 rrx2pyel 
 |-  ( X e. P -> ( X ` 2 ) e. RR )
10 8 9 jca 
 |-  ( X e. P -> ( ( X ` 1 ) e. RR /\ ( X ` 2 ) e. RR ) )
11 10 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( ( X ` 1 ) e. RR /\ ( 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 ` 1 ) e. RR /\ ( X ` 2 ) e. RR ) )
13 1 3 rrx2pxel 
 |-  ( Y e. P -> ( Y ` 1 ) e. RR )
14 1 3 rrx2pyel 
 |-  ( Y e. P -> ( Y ` 2 ) e. RR )
15 13 14 jca 
 |-  ( Y e. P -> ( ( Y ` 1 ) e. RR /\ ( Y ` 2 ) e. RR ) )
16 15 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( ( Y ` 1 ) e. RR /\ ( Y ` 2 ) e. RR ) )
17 16 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( Y ` 1 ) e. RR /\ ( Y ` 2 ) e. RR ) )
18 simpl3 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( X ` 2 ) =/= ( Y ` 2 ) )
19 rpre 
 |-  ( R e. RR+ -> R e. RR )
20 19 adantr 
 |-  ( ( R e. RR+ /\ ( X D .0. ) < R ) -> R e. RR )
21 20 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> R e. RR )
22 simpl1 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) -> X e. P )
23 2nn0 
 |-  2 e. NN0
24 eqid 
 |-  ( EEhil ` 2 ) = ( EEhil ` 2 )
25 24 ehlval 
 |-  ( 2 e. NN0 -> ( EEhil ` 2 ) = ( RR^ ` ( 1 ... 2 ) ) )
26 23 25 ax-mp 
 |-  ( EEhil ` 2 ) = ( RR^ ` ( 1 ... 2 ) )
27 fz12pr 
 |-  ( 1 ... 2 ) = { 1 , 2 }
28 27 1 eqtr4i 
 |-  ( 1 ... 2 ) = I
29 28 fveq2i 
 |-  ( RR^ ` ( 1 ... 2 ) ) = ( RR^ ` I )
30 26 29 eqtri 
 |-  ( EEhil ` 2 ) = ( RR^ ` I )
31 2 30 eqtr4i 
 |-  E = ( EEhil ` 2 )
32 1 oveq2i 
 |-  ( RR ^m I ) = ( RR ^m { 1 , 2 } )
33 3 32 eqtri 
 |-  P = ( RR ^m { 1 , 2 } )
34 1 xpeq1i 
 |-  ( I X. { 0 } ) = ( { 1 , 2 } X. { 0 } )
35 5 34 eqtri 
 |-  .0. = ( { 1 , 2 } X. { 0 } )
36 31 33 7 35 ehl2eudisval0 
 |-  ( X e. P -> ( X D .0. ) = ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) )
37 22 36 syl 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) -> ( X D .0. ) = ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) )
38 37 breq1d 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) -> ( ( X D .0. ) < R <-> ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) )
39 rpge0 
 |-  ( R e. RR+ -> 0 <_ R )
40 19 39 sqrtsqd 
 |-  ( R e. RR+ -> ( sqrt ` ( R ^ 2 ) ) = R )
41 40 eqcomd 
 |-  ( R e. RR+ -> R = ( sqrt ` ( R ^ 2 ) ) )
42 41 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) -> R = ( sqrt ` ( R ^ 2 ) ) )
43 42 breq2d 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) -> ( ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R <-> ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < ( sqrt ` ( R ^ 2 ) ) ) )
44 43 biimpa 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < ( sqrt ` ( R ^ 2 ) ) )
45 22 8 syl 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) -> ( X ` 1 ) e. RR )
46 45 adantr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> ( X ` 1 ) e. RR )
47 46 resqcld 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> ( ( X ` 1 ) ^ 2 ) e. RR )
48 22 9 syl 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) -> ( X ` 2 ) e. RR )
49 48 adantr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> ( X ` 2 ) e. RR )
50 49 resqcld 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> ( ( X ` 2 ) ^ 2 ) e. RR )
51 47 50 readdcld 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) e. RR )
52 46 sqge0d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> 0 <_ ( ( X ` 1 ) ^ 2 ) )
53 49 sqge0d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> 0 <_ ( ( X ` 2 ) ^ 2 ) )
54 47 50 52 53 addge0d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> 0 <_ ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) )
55 19 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) -> R e. RR )
56 55 adantr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> R e. RR )
57 56 resqcld 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> ( R ^ 2 ) e. RR )
58 56 sqge0d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> 0 <_ ( R ^ 2 ) )
59 51 54 57 58 sqrtltd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> ( ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) < ( R ^ 2 ) <-> ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < ( sqrt ` ( R ^ 2 ) ) ) )
60 44 59 mpbird 
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) /\ ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R ) -> ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) < ( R ^ 2 ) )
61 60 ex 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) -> ( ( sqrt ` ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) ) < R -> ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) < ( R ^ 2 ) ) )
62 38 61 sylbid 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ R e. RR+ ) -> ( ( X D .0. ) < R -> ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) < ( R ^ 2 ) ) )
63 62 impr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) < ( R ^ 2 ) )
64 eqid 
 |-  ( ( Y ` 1 ) - ( X ` 1 ) ) = ( ( Y ` 1 ) - ( X ` 1 ) )
65 eqid 
 |-  ( ( X ` 2 ) - ( Y ` 2 ) ) = ( ( X ` 2 ) - ( Y ` 2 ) )
66 eqid 
 |-  ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) )
67 64 65 66 itscnhlinecirc02plem2 
 |-  ( ( ( ( ( X ` 1 ) e. RR /\ ( X ` 2 ) e. RR ) /\ ( ( Y ` 1 ) e. RR /\ ( Y ` 2 ) e. RR ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) /\ ( R e. RR /\ ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) < ( R ^ 2 ) ) ) -> 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 ) ) ) ) ) ) )
68 12 17 18 21 63 67 syl32anc 
 |-  ( ( ( 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 ) ) ) ) ) ) )