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 ⊢ 𝐸 = ( 𝔼hil ‘ 2 )
ehl2eudisval0.x ⊢ 𝑋 = ( ℝ ↑m { 1 , 2 } )
ehl2eudisval0.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
ehl2eudisval0.0 ⊢ 0 = ( { 1 , 2 } × { 0 } )
Assertion ehl2eudis0lt ( ( 𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝐹 𝐷 0 ) < 𝑅 ↔ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 ehl2eudisval0.e ⊢ 𝐸 = ( 𝔼hil ‘ 2 )
2 ehl2eudisval0.x ⊢ 𝑋 = ( ℝ ↑m { 1 , 2 } )
3 ehl2eudisval0.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
4 ehl2eudisval0.0 ⊢ 0 = ( { 1 , 2 } × { 0 } )
5 1 2 3 4 ehl2eudisval0 ⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 𝐷 0 ) = ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) )
6 5 adantr ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝐹 𝐷 0 ) = ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) )
7 6 breq1d ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝐹 𝐷 0 ) < 𝑅 ↔ ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) < 𝑅 ) )
8 eqid ⊢ { 1 , 2 } = { 1 , 2 }
9 8 2 rrx2pxel ⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 ‘ 1 ) ∈ ℝ )
10 8 2 rrx2pyel ⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 ‘ 2 ) ∈ ℝ )
11 eqid ⊢ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) = ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) )
12 11 resum2sqcl ⊢ ( ( ( 𝐹 ‘ 1 ) ∈ ℝ ∧ ( 𝐹 ‘ 2 ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ∈ ℝ )
13 9 10 12 syl2anc ⊢ ( 𝐹 ∈ 𝑋 → ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ∈ ℝ )
14 resqcl ⊢ ( ( 𝐹 ‘ 1 ) ∈ ℝ → ( ( 𝐹 ‘ 1 ) ↑ 2 ) ∈ ℝ )
15 resqcl ⊢ ( ( 𝐹 ‘ 2 ) ∈ ℝ → ( ( 𝐹 ‘ 2 ) ↑ 2 ) ∈ ℝ )
16 14 15 anim12i ⊢ ( ( ( 𝐹 ‘ 1 ) ∈ ℝ ∧ ( 𝐹 ‘ 2 ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) ∈ ℝ ∧ ( ( 𝐹 ‘ 2 ) ↑ 2 ) ∈ ℝ ) )
17 sqge0 ⊢ ( ( 𝐹 ‘ 1 ) ∈ ℝ → 0 ≤ ( ( 𝐹 ‘ 1 ) ↑ 2 ) )
18 sqge0 ⊢ ( ( 𝐹 ‘ 2 ) ∈ ℝ → 0 ≤ ( ( 𝐹 ‘ 2 ) ↑ 2 ) )
19 17 18 anim12i ⊢ ( ( ( 𝐹 ‘ 1 ) ∈ ℝ ∧ ( 𝐹 ‘ 2 ) ∈ ℝ ) → ( 0 ≤ ( ( 𝐹 ‘ 1 ) ↑ 2 ) ∧ 0 ≤ ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) )
20 addge0 ⊢ ( ( ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) ∈ ℝ ∧ ( ( 𝐹 ‘ 2 ) ↑ 2 ) ∈ ℝ ) ∧ ( 0 ≤ ( ( 𝐹 ‘ 1 ) ↑ 2 ) ∧ 0 ≤ ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) → 0 ≤ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) )
21 16 19 20 syl2anc ⊢ ( ( ( 𝐹 ‘ 1 ) ∈ ℝ ∧ ( 𝐹 ‘ 2 ) ∈ ℝ ) → 0 ≤ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) )
22 9 10 21 syl2anc ⊢ ( 𝐹 ∈ 𝑋 → 0 ≤ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) )
23 13 22 resqrtcld ⊢ ( 𝐹 ∈ 𝑋 → ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) ∈ ℝ )
24 13 22 sqrtge0d ⊢ ( 𝐹 ∈ 𝑋 → 0 ≤ ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) )
25 23 24 jca ⊢ ( 𝐹 ∈ 𝑋 → ( ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) ∈ ℝ ∧ 0 ≤ ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) ) )
26 rprege0 ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
27 lt2sq ⊢ ( ( ( ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) ∈ ℝ ∧ 0 ≤ ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) ) ∧ ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ) → ( ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) < 𝑅 ↔ ( ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) ↑ 2 ) < ( 𝑅 ↑ 2 ) ) )
28 25 26 27 syl2an ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) < 𝑅 ↔ ( ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) ↑ 2 ) < ( 𝑅 ↑ 2 ) ) )
29 13 22 jca ⊢ ( 𝐹 ∈ 𝑋 → ( ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) )
30 29 adantr ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) )
31 resqrtth ⊢ ( ( ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) → ( ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) )
32 30 31 syl ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) )
33 32 breq1d ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ( ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) ↑ 2 ) < ( 𝑅 ↑ 2 ) ↔ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) )
34 7 28 33 3bitrd ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝐹 𝐷 0 ) < 𝑅 ↔ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) )