![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rpsqrtcl | Structured version Visualization version GIF version |
Description: The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.) |
Ref | Expression |
---|---|
rpsqrtcl | ⊢ (𝐴 ∈ ℝ+ → (√‘𝐴) ∈ ℝ+) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpre 12423 | . . 3 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) | |
2 | rpge0 12428 | . . 3 ⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴) | |
3 | resqrtcl 14646 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈ ℝ) | |
4 | 1, 2, 3 | syl2anc 588 | . 2 ⊢ (𝐴 ∈ ℝ+ → (√‘𝐴) ∈ ℝ) |
5 | rpgt0 12427 | . . 3 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) | |
6 | sqrtgt0 14651 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 0 < (√‘𝐴)) | |
7 | 1, 5, 6 | syl2anc 588 | . 2 ⊢ (𝐴 ∈ ℝ+ → 0 < (√‘𝐴)) |
8 | 4, 7 | elrpd 12454 | 1 ⊢ (𝐴 ∈ ℝ+ → (√‘𝐴) ∈ ℝ+) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2112 class class class wbr 5025 ‘cfv 6328 ℝcr 10559 0cc0 10560 < clt 10698 ≤ cle 10699 ℝ+crp 12415 √csqrt 14625 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 ax-un 7452 ax-cnex 10616 ax-resscn 10617 ax-1cn 10618 ax-icn 10619 ax-addcl 10620 ax-addrcl 10621 ax-mulcl 10622 ax-mulrcl 10623 ax-mulcom 10624 ax-addass 10625 ax-mulass 10626 ax-distr 10627 ax-i2m1 10628 ax-1ne0 10629 ax-1rid 10630 ax-rnegex 10631 ax-rrecex 10632 ax-cnre 10633 ax-pre-lttri 10634 ax-pre-lttrn 10635 ax-pre-ltadd 10636 ax-pre-mulgt0 10637 ax-pre-sup 10638 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ne 2950 df-nel 3054 df-ral 3073 df-rex 3074 df-reu 3075 df-rmo 3076 df-rab 3077 df-v 3409 df-sbc 3694 df-csb 3802 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-pss 3873 df-nul 4222 df-if 4414 df-pw 4489 df-sn 4516 df-pr 4518 df-tp 4520 df-op 4522 df-uni 4792 df-iun 4878 df-br 5026 df-opab 5088 df-mpt 5106 df-tr 5132 df-id 5423 df-eprel 5428 df-po 5436 df-so 5437 df-fr 5476 df-we 5478 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-rn 5528 df-res 5529 df-ima 5530 df-pred 6119 df-ord 6165 df-on 6166 df-lim 6167 df-suc 6168 df-iota 6287 df-fun 6330 df-fn 6331 df-f 6332 df-f1 6333 df-fo 6334 df-f1o 6335 df-fv 6336 df-riota 7101 df-ov 7146 df-oprab 7147 df-mpo 7148 df-om 7573 df-2nd 7687 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-er 8292 df-en 8521 df-dom 8522 df-sdom 8523 df-sup 8924 df-pnf 10700 df-mnf 10701 df-xr 10702 df-ltxr 10703 df-le 10704 df-sub 10895 df-neg 10896 df-div 11321 df-nn 11660 df-2 11722 df-3 11723 df-n0 11920 df-z 12006 df-uz 12268 df-rp 12416 df-seq 13404 df-exp 13465 df-cj 14491 df-re 14492 df-im 14493 df-sqrt 14627 |
This theorem is referenced by: sqrtdiv 14658 absrpcl 14681 rpsqrtcld 14804 2irrexpq 25405 dvsqrt 25415 loglesqrt 25431 divsqrtsumlem 25649 divsqrtsumo1 25653 bposlem7 25958 bposlem8 25959 dchrisum0fno1 26179 dchrisum0lema 26182 dchrisum0 26188 rpsqrtcn 32077 divsqrtid 32078 logdivsqrle 32134 |
Copyright terms: Public domain | W3C validator |