Metamath Proof Explorer

Theorem ehl2eudis0lt

Description: An upper bound of the Euclidean distance of a point to the origin in a real Euclidean space of dimension 2. (Contributed by AV, 9-May-2023)

Ref Expression
Hypotheses ehl2eudisval0.e 
|- E = ( EEhil ` 2 )
ehl2eudisval0.x 
|- X = ( RR ^m { 1 , 2 } )
ehl2eudisval0.d 
|- D = ( dist ` E )
ehl2eudisval0.0 
|- .0. = ( { 1 , 2 } X. { 0 } )
Assertion ehl2eudis0lt 
|- ( ( F e. X /\ R e. RR+ ) -> ( ( F D .0. ) < R <-> ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) < ( R ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 ehl2eudisval0.e 
 |-  E = ( EEhil ` 2 )
2 ehl2eudisval0.x 
 |-  X = ( RR ^m { 1 , 2 } )
3 ehl2eudisval0.d 
 |-  D = ( dist ` E )
4 ehl2eudisval0.0 
 |-  .0. = ( { 1 , 2 } X. { 0 } )
5 1 2 3 4 ehl2eudisval0 
 |-  ( F e. X -> ( F D .0. ) = ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) )
6 5 adantr 
 |-  ( ( F e. X /\ R e. RR+ ) -> ( F D .0. ) = ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) )
7 6 breq1d 
 |-  ( ( F e. X /\ R e. RR+ ) -> ( ( F D .0. ) < R <-> ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) < R ) )
8 eqid 
 |-  { 1 , 2 } = { 1 , 2 }
9 8 2 rrx2pxel 
 |-  ( F e. X -> ( F ` 1 ) e. RR )
10 8 2 rrx2pyel 
 |-  ( F e. X -> ( F ` 2 ) e. RR )
11 eqid 
 |-  ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) = ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) )
12 11 resum2sqcl 
 |-  ( ( ( F ` 1 ) e. RR /\ ( F ` 2 ) e. RR ) -> ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) e. RR )
13 9 10 12 syl2anc 
 |-  ( F e. X -> ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) e. RR )
14 resqcl 
 |-  ( ( F ` 1 ) e. RR -> ( ( F ` 1 ) ^ 2 ) e. RR )
15 resqcl 
 |-  ( ( F ` 2 ) e. RR -> ( ( F ` 2 ) ^ 2 ) e. RR )
16 14 15 anim12i 
 |-  ( ( ( F ` 1 ) e. RR /\ ( F ` 2 ) e. RR ) -> ( ( ( F ` 1 ) ^ 2 ) e. RR /\ ( ( F ` 2 ) ^ 2 ) e. RR ) )
17 sqge0 
 |-  ( ( F ` 1 ) e. RR -> 0 <_ ( ( F ` 1 ) ^ 2 ) )
18 sqge0 
 |-  ( ( F ` 2 ) e. RR -> 0 <_ ( ( F ` 2 ) ^ 2 ) )
19 17 18 anim12i 
 |-  ( ( ( F ` 1 ) e. RR /\ ( F ` 2 ) e. RR ) -> ( 0 <_ ( ( F ` 1 ) ^ 2 ) /\ 0 <_ ( ( F ` 2 ) ^ 2 ) ) )
20 addge0 
 |-  ( ( ( ( ( F ` 1 ) ^ 2 ) e. RR /\ ( ( F ` 2 ) ^ 2 ) e. RR ) /\ ( 0 <_ ( ( F ` 1 ) ^ 2 ) /\ 0 <_ ( ( F ` 2 ) ^ 2 ) ) ) -> 0 <_ ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) )
21 16 19 20 syl2anc 
 |-  ( ( ( F ` 1 ) e. RR /\ ( F ` 2 ) e. RR ) -> 0 <_ ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) )
22 9 10 21 syl2anc 
 |-  ( F e. X -> 0 <_ ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) )
23 13 22 resqrtcld 
 |-  ( F e. X -> ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) e. RR )
24 13 22 sqrtge0d 
 |-  ( F e. X -> 0 <_ ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) )
25 23 24 jca 
 |-  ( F e. X -> ( ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) e. RR /\ 0 <_ ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) ) )
26 rprege0 
 |-  ( R e. RR+ -> ( R e. RR /\ 0 <_ R ) )
27 lt2sq 
 |-  ( ( ( ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) e. RR /\ 0 <_ ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) ) /\ ( R e. RR /\ 0 <_ R ) ) -> ( ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) < R <-> ( ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) ^ 2 ) < ( R ^ 2 ) ) )
28 25 26 27 syl2an 
 |-  ( ( F e. X /\ R e. RR+ ) -> ( ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) < R <-> ( ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) ^ 2 ) < ( R ^ 2 ) ) )
29 13 22 jca 
 |-  ( F e. X -> ( ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) e. RR /\ 0 <_ ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) )
30 29 adantr 
 |-  ( ( F e. X /\ R e. RR+ ) -> ( ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) e. RR /\ 0 <_ ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) )
31 resqrtth 
 |-  ( ( ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) e. RR /\ 0 <_ ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) -> ( ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) ^ 2 ) = ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) )
32 30 31 syl 
 |-  ( ( F e. X /\ R e. RR+ ) -> ( ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) ^ 2 ) = ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) )
33 32 breq1d 
 |-  ( ( F e. X /\ R e. RR+ ) -> ( ( ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) ^ 2 ) < ( R ^ 2 ) <-> ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) < ( R ^ 2 ) ) )
34 7 28 33 3bitrd 
 |-  ( ( F e. X /\ R e. RR+ ) -> ( ( F D .0. ) < R <-> ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) < ( R ^ 2 ) ) )