| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > absrpcld | Structured version Visualization version GIF version | ||
| Description: The absolute value of a nonzero number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.) |
| Ref | Expression |
|---|---|
| abscld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
| absne0d.2 | ⊢ (𝜑 → 𝐴 ≠ 0) |
| Ref | Expression |
|---|---|
| absrpcld | ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ+) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abscld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
| 2 | absne0d.2 | . 2 ⊢ (𝜑 → 𝐴 ≠ 0) | |
| 3 | absrpcl 15316 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℝ+) | |
| 4 | 1, 2, 3 | syl2anc 593 | 1 ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ+) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2143 ≠ wne 2958 ‘cfv 6522 ℂcc 11072 0cc0 11074 ℝ+crp 12994 abscabs 15262 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1816 ax-4 1830 ax-5 1931 ax-6 1988 ax-7 2029 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5247 ax-nul 5257 ax-pow 5323 ax-pr 5391 ax-un 7719 ax-cnex 11130 ax-resscn 11131 ax-1cn 11132 ax-icn 11133 ax-addcl 11134 ax-addrcl 11135 ax-mulcl 11136 ax-mulrcl 11137 ax-mulcom 11138 ax-addass 11139 ax-mulass 11140 ax-distr 11141 ax-i2m1 11142 ax-1ne0 11143 ax-1rid 11144 ax-rnegex 11145 ax-rrecex 11146 ax-cnre 11147 ax-pre-lttri 11148 ax-pre-lttrn 11149 ax-pre-ltadd 11150 ax-pre-mulgt0 11151 ax-pre-sup 11152 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1564 df-fal 1574 df-ex 1801 df-nf 1805 df-sb 2092 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3457 df-sbc 3746 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-iun 4952 df-br 5102 df-opab 5164 df-mpt 5183 df-tr 5209 df-id 5543 df-eprel 5548 df-po 5556 df-so 5557 df-fr 5601 df-we 5603 df-xp 5654 df-rel 5655 df-cnv 5656 df-co 5657 df-dm 5658 df-rn 5659 df-res 5660 df-ima 5661 df-pred 6289 df-ord 6350 df-on 6351 df-lim 6352 df-suc 6353 df-iota 6478 df-fun 6524 df-fn 6525 df-f 6526 df-f1 6527 df-fo 6528 df-f1o 6529 df-fv 6530 df-riota 7354 df-ov 7400 df-oprab 7401 df-mpo 7402 df-om 7848 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8382 df-er 8679 df-en 8929 df-dom 8930 df-sdom 8931 df-sup 9389 df-pnf 11219 df-mnf 11220 df-xr 11221 df-ltxr 11222 df-le 11223 df-sub 11417 df-neg 11418 df-div 11846 df-nn 12212 df-2 12281 df-3 12282 df-n0 12483 df-z 12570 df-uz 12841 df-rp 12995 df-seq 14016 df-exp 14076 df-cj 15127 df-re 15128 df-im 15129 df-sqrt 15263 df-abs 15264 |
| This theorem is referenced by: rlimuni 15578 climuni 15580 rlimrecl 15608 reccn2 15625 rlimno1 15682 georeclim 15903 4sqlem11 16992 recld2 24876 c1liplem1 26059 aalioulem2 26398 aaliou2b 26406 ulmdvlem1 26464 abelthlem7 26502 tanregt0 26605 eff1olem 26614 logcnlem2 26709 logcnlem4 26711 logcn 26713 asinlem3 26937 lgamgulmlem2 27095 lgamgulmlem5 27098 lgambdd 27102 lgamucov 27103 ftalem2 27139 ftalem4 27141 dchrabs 27325 sinccvglem 36023 unbdqndv2lem2 36949 readvrec 42972 rencldnfilem 43398 pellexlem6 43412 modabsdifz 43564 jm2.19 43571 imo72b2lem1 44746 cvgdvgrat 44890 binomcxplemnotnn0 44933 abssubrp 45856 dstregt0 45862 absimnre 46051 lptre2pt 46215 0ellimcdiv 46224 limclner 46226 climxrre 46325 cnrefiisplem 46404 cncficcgt0 46463 |
| Copyright terms: Public domain | W3C validator |