Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ehl2eudis0lt | Structured version Visualization version GIF version |
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 |
---|---|
ehl2eudisval0.e | ⊢ 𝐸 = (𝔼hil‘2) |
ehl2eudisval0.x | ⊢ 𝑋 = (ℝ ↑m {1, 2}) |
ehl2eudisval0.d | ⊢ 𝐷 = (dist‘𝐸) |
ehl2eudisval0.0 | ⊢ 0 = ({1, 2} × {0}) |
Ref | Expression |
---|---|
ehl2eudis0lt | ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → ((𝐹𝐷 0 ) < 𝑅 ↔ (((𝐹‘1)↑2) + ((𝐹‘2)↑2)) < (𝑅↑2))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ehl2eudisval0.e | . . . . 5 ⊢ 𝐸 = (𝔼hil‘2) | |
2 | ehl2eudisval0.x | . . . . 5 ⊢ 𝑋 = (ℝ ↑m {1, 2}) | |
3 | ehl2eudisval0.d | . . . . 5 ⊢ 𝐷 = (dist‘𝐸) | |
4 | ehl2eudisval0.0 | . . . . 5 ⊢ 0 = ({1, 2} × {0}) | |
5 | 1, 2, 3, 4 | ehl2eudisval0 46328 | . . . 4 ⊢ (𝐹 ∈ 𝑋 → (𝐹𝐷 0 ) = (√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2)))) |
6 | 5 | adantr 481 | . . 3 ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝐹𝐷 0 ) = (√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2)))) |
7 | 6 | breq1d 5090 | . 2 ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → ((𝐹𝐷 0 ) < 𝑅 ↔ (√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2))) < 𝑅)) |
8 | eqid 2735 | . . . . . . 7 ⊢ {1, 2} = {1, 2} | |
9 | 8, 2 | rrx2pxel 46314 | . . . . . 6 ⊢ (𝐹 ∈ 𝑋 → (𝐹‘1) ∈ ℝ) |
10 | 8, 2 | rrx2pyel 46315 | . . . . . 6 ⊢ (𝐹 ∈ 𝑋 → (𝐹‘2) ∈ ℝ) |
11 | eqid 2735 | . . . . . . 7 ⊢ (((𝐹‘1)↑2) + ((𝐹‘2)↑2)) = (((𝐹‘1)↑2) + ((𝐹‘2)↑2)) | |
12 | 11 | resum2sqcl 46309 | . . . . . 6 ⊢ (((𝐹‘1) ∈ ℝ ∧ (𝐹‘2) ∈ ℝ) → (((𝐹‘1)↑2) + ((𝐹‘2)↑2)) ∈ ℝ) |
13 | 9, 10, 12 | syl2anc 584 | . . . . 5 ⊢ (𝐹 ∈ 𝑋 → (((𝐹‘1)↑2) + ((𝐹‘2)↑2)) ∈ ℝ) |
14 | resqcl 13904 | . . . . . . . 8 ⊢ ((𝐹‘1) ∈ ℝ → ((𝐹‘1)↑2) ∈ ℝ) | |
15 | resqcl 13904 | . . . . . . . 8 ⊢ ((𝐹‘2) ∈ ℝ → ((𝐹‘2)↑2) ∈ ℝ) | |
16 | 14, 15 | anim12i 613 | . . . . . . 7 ⊢ (((𝐹‘1) ∈ ℝ ∧ (𝐹‘2) ∈ ℝ) → (((𝐹‘1)↑2) ∈ ℝ ∧ ((𝐹‘2)↑2) ∈ ℝ)) |
17 | sqge0 13915 | . . . . . . . 8 ⊢ ((𝐹‘1) ∈ ℝ → 0 ≤ ((𝐹‘1)↑2)) | |
18 | sqge0 13915 | . . . . . . . 8 ⊢ ((𝐹‘2) ∈ ℝ → 0 ≤ ((𝐹‘2)↑2)) | |
19 | 17, 18 | anim12i 613 | . . . . . . 7 ⊢ (((𝐹‘1) ∈ ℝ ∧ (𝐹‘2) ∈ ℝ) → (0 ≤ ((𝐹‘1)↑2) ∧ 0 ≤ ((𝐹‘2)↑2))) |
20 | addge0 11524 | . . . . . . 7 ⊢ (((((𝐹‘1)↑2) ∈ ℝ ∧ ((𝐹‘2)↑2) ∈ ℝ) ∧ (0 ≤ ((𝐹‘1)↑2) ∧ 0 ≤ ((𝐹‘2)↑2))) → 0 ≤ (((𝐹‘1)↑2) + ((𝐹‘2)↑2))) | |
21 | 16, 19, 20 | syl2anc 584 | . . . . . 6 ⊢ (((𝐹‘1) ∈ ℝ ∧ (𝐹‘2) ∈ ℝ) → 0 ≤ (((𝐹‘1)↑2) + ((𝐹‘2)↑2))) |
22 | 9, 10, 21 | syl2anc 584 | . . . . 5 ⊢ (𝐹 ∈ 𝑋 → 0 ≤ (((𝐹‘1)↑2) + ((𝐹‘2)↑2))) |
23 | 13, 22 | resqrtcld 15188 | . . . 4 ⊢ (𝐹 ∈ 𝑋 → (√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2))) ∈ ℝ) |
24 | 13, 22 | sqrtge0d 15191 | . . . 4 ⊢ (𝐹 ∈ 𝑋 → 0 ≤ (√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2)))) |
25 | 23, 24 | jca 512 | . . 3 ⊢ (𝐹 ∈ 𝑋 → ((√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2))) ∈ ℝ ∧ 0 ≤ (√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2))))) |
26 | rprege0 12805 | . . 3 ⊢ (𝑅 ∈ ℝ+ → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) | |
27 | lt2sq 13912 | . . 3 ⊢ ((((√‘(((𝐹‘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 596 | . 2 ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → ((√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2))) < 𝑅 ↔ ((√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2)))↑2) < (𝑅↑2))) |
29 | 13, 22 | jca 512 | . . . . 5 ⊢ (𝐹 ∈ 𝑋 → ((((𝐹‘1)↑2) + ((𝐹‘2)↑2)) ∈ ℝ ∧ 0 ≤ (((𝐹‘1)↑2) + ((𝐹‘2)↑2)))) |
30 | 29 | adantr 481 | . . . 4 ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → ((((𝐹‘1)↑2) + ((𝐹‘2)↑2)) ∈ ℝ ∧ 0 ≤ (((𝐹‘1)↑2) + ((𝐹‘2)↑2)))) |
31 | resqrtth 15026 | . . . 4 ⊢ (((((𝐹‘1)↑2) + ((𝐹‘2)↑2)) ∈ ℝ ∧ 0 ≤ (((𝐹‘1)↑2) + ((𝐹‘2)↑2))) → ((√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2)))↑2) = (((𝐹‘1)↑2) + ((𝐹‘2)↑2))) | |
32 | 30, 31 | syl 17 | . . 3 ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → ((√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2)))↑2) = (((𝐹‘1)↑2) + ((𝐹‘2)↑2))) |
33 | 32 | breq1d 5090 | . 2 ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (((√‘(((𝐹‘1)↑2) + ((𝐹‘2)↑2)))↑2) < (𝑅↑2) ↔ (((𝐹‘1)↑2) + ((𝐹‘2)↑2)) < (𝑅↑2))) |
34 | 7, 28, 33 | 3bitrd 304 | 1 ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → ((𝐹𝐷 0 ) < 𝑅 ↔ (((𝐹‘1)↑2) + ((𝐹‘2)↑2)) < (𝑅↑2))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1538 ∈ wcel 2103 {csn 4564 {cpr 4566 class class class wbr 5080 × cxp 5598 ‘cfv 6458 (class class class)co 7308 ↑m cmap 8651 ℝcr 10930 0cc0 10931 1c1 10932 + caddc 10934 < clt 11069 ≤ cle 11070 2c2 12088 ℝ+crp 12790 ↑cexp 13842 √csqrt 15003 distcds 17030 𝔼hilcehl 24611 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1910 ax-6 1968 ax-7 2008 ax-8 2105 ax-9 2113 ax-10 2134 ax-11 2151 ax-12 2168 ax-ext 2706 ax-rep 5217 ax-sep 5231 ax-nul 5238 ax-pow 5296 ax-pr 5360 ax-un 7621 ax-inf2 9457 ax-cnex 10987 ax-resscn 10988 ax-1cn 10989 ax-icn 10990 ax-addcl 10991 ax-addrcl 10992 ax-mulcl 10993 ax-mulrcl 10994 ax-mulcom 10995 ax-addass 10996 ax-mulass 10997 ax-distr 10998 ax-i2m1 10999 ax-1ne0 11000 ax-1rid 11001 ax-rnegex 11002 ax-rrecex 11003 ax-cnre 11004 ax-pre-lttri 11005 ax-pre-lttrn 11006 ax-pre-ltadd 11007 ax-pre-mulgt0 11008 ax-pre-sup 11009 ax-addf 11010 ax-mulf 11011 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1541 df-fal 1551 df-ex 1779 df-nf 1783 df-sb 2065 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2727 df-clel 2813 df-nfc 2885 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3339 df-reu 3340 df-rab 3357 df-v 3438 df-sbc 3721 df-csb 3837 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-pss 3910 df-nul 4262 df-if 4465 df-pw 4540 df-sn 4565 df-pr 4567 df-tp 4569 df-op 4571 df-uni 4844 df-int 4886 df-iun 4932 df-br 5081 df-opab 5143 df-mpt 5164 df-tr 5198 df-id 5500 df-eprel 5506 df-po 5514 df-so 5515 df-fr 5555 df-se 5556 df-we 5557 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-res 5612 df-ima 5613 df-pred 6217 df-ord 6284 df-on 6285 df-lim 6286 df-suc 6287 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463 df-fo 6464 df-f1o 6465 df-fv 6466 df-isom 6467 df-riota 7265 df-ov 7311 df-oprab 7312 df-mpo 7313 df-of 7566 df-om 7749 df-1st 7867 df-2nd 7868 df-supp 8013 df-tpos 8077 df-frecs 8132 df-wrecs 8163 df-recs 8237 df-rdg 8276 df-1o 8332 df-er 8534 df-map 8653 df-ixp 8722 df-en 8770 df-dom 8771 df-sdom 8772 df-fin 8773 df-fsupp 9187 df-sup 9259 df-oi 9327 df-card 9755 df-pnf 11071 df-mnf 11072 df-xr 11073 df-ltxr 11074 df-le 11075 df-sub 11267 df-neg 11268 df-div 11693 df-nn 12034 df-2 12096 df-3 12097 df-4 12098 df-5 12099 df-6 12100 df-7 12101 df-8 12102 df-9 12103 df-n0 12294 df-z 12380 df-dec 12498 df-uz 12643 df-rp 12791 df-fz 13300 df-fzo 13443 df-seq 13782 df-exp 13843 df-hash 14105 df-cj 14869 df-re 14870 df-im 14871 df-sqrt 15005 df-abs 15006 df-clim 15256 df-sum 15457 df-struct 16907 df-sets 16924 df-slot 16942 df-ndx 16954 df-base 16972 df-ress 17001 df-plusg 17034 df-mulr 17035 df-starv 17036 df-sca 17037 df-vsca 17038 df-ip 17039 df-tset 17040 df-ple 17041 df-ds 17043 df-unif 17044 df-hom 17045 df-cco 17046 df-0g 17211 df-gsum 17212 df-prds 17217 df-pws 17219 df-mgm 18385 df-sgrp 18434 df-mnd 18445 df-mhm 18489 df-grp 18639 df-minusg 18640 df-sbg 18641 df-subg 18811 df-ghm 18891 df-cntz 18982 df-cmn 19447 df-abl 19448 df-mgp 19780 df-ur 19797 df-ring 19844 df-cring 19845 df-oppr 19921 df-dvdsr 19942 df-unit 19943 df-invr 19973 df-dvr 19984 df-rnghom 20018 df-drng 20056 df-field 20057 df-subrg 20085 df-staf 20168 df-srng 20169 df-lmod 20188 df-lss 20257 df-sra 20497 df-rgmod 20498 df-cnfld 20661 df-refld 20873 df-dsmm 21002 df-frlm 21017 df-nm 23801 df-tng 23803 df-tcph 24396 df-rrx 24612 df-ehl 24613 |
This theorem is referenced by: inlinecirc02p 46390 |
Copyright terms: Public domain | W3C validator |