Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3rp | Structured version Visualization version GIF version |
Description: 3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
3rp | ⊢ 3 ∈ ℝ+ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3re 11699 | . 2 ⊢ 3 ∈ ℝ | |
2 | 3pos 11724 | . 2 ⊢ 0 < 3 | |
3 | 1, 2 | elrpii 12374 | 1 ⊢ 3 ∈ ℝ+ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 3c3 11675 ℝ+crp 12371 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2792 ax-sep 5184 ax-nul 5191 ax-pow 5247 ax-pr 5311 ax-un 7442 ax-resscn 10575 ax-1cn 10576 ax-icn 10577 ax-addcl 10578 ax-addrcl 10579 ax-mulcl 10580 ax-mulrcl 10581 ax-mulcom 10582 ax-addass 10583 ax-mulass 10584 ax-distr 10585 ax-i2m1 10586 ax-1ne0 10587 ax-1rid 10588 ax-rnegex 10589 ax-rrecex 10590 ax-cnre 10591 ax-pre-lttri 10592 ax-pre-lttrn 10593 ax-pre-ltadd 10594 ax-pre-mulgt0 10595 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2653 df-clab 2799 df-cleq 2813 df-clel 2891 df-nfc 2959 df-ne 3012 df-nel 3119 df-ral 3138 df-rex 3139 df-reu 3140 df-rab 3142 df-v 3483 df-sbc 3759 df-csb 3867 df-dif 3922 df-un 3924 df-in 3926 df-ss 3935 df-nul 4275 df-if 4449 df-pw 4522 df-sn 4549 df-pr 4551 df-op 4555 df-uni 4820 df-br 5048 df-opab 5110 df-mpt 5128 df-id 5441 df-po 5455 df-so 5456 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-iota 6295 df-fun 6338 df-fn 6339 df-f 6340 df-f1 6341 df-fo 6342 df-f1o 6343 df-fv 6344 df-riota 7095 df-ov 7140 df-oprab 7141 df-mpo 7142 df-er 8270 df-en 8491 df-dom 8492 df-sdom 8493 df-pnf 10658 df-mnf 10659 df-xr 10660 df-ltxr 10661 df-le 10662 df-sub 10853 df-neg 10854 df-2 11682 df-3 11683 df-rp 12372 |
This theorem is referenced by: sqrlem7 14588 caurcvgr 15010 vitalilem4 24190 pige3ALT 25086 2logb9irrALT 25357 log2cnv 25503 cht3 25731 bposlem9 25849 chto1ub 26033 dchrvmasumiflem1 26058 pntibndlem1 26146 pntibndlem2 26148 pntlema 26153 pntlemb 26154 hgt750lemd 31921 hgt750lem 31924 hgt750lem2 31925 hgt750leme 31931 fourierdlem87 42563 lighneallem2 43851 |
Copyright terms: Public domain | W3C validator |