![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ne0gt0d | Structured version Visualization version GIF version |
Description: A nonzero nonnegative number is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
ltd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ne0gt0d.2 | ⊢ (𝜑 → 0 ≤ 𝐴) |
ne0gt0d.3 | ⊢ (𝜑 → 𝐴 ≠ 0) |
Ref | Expression |
---|---|
ne0gt0d | ⊢ (𝜑 → 0 < 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ne0gt0d.3 | . 2 ⊢ (𝜑 → 𝐴 ≠ 0) | |
2 | ltd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
3 | ne0gt0d.2 | . . 3 ⊢ (𝜑 → 0 ≤ 𝐴) | |
4 | ne0gt0 10544 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 ≠ 0 ↔ 0 < 𝐴)) | |
5 | 2, 3, 4 | syl2anc 576 | . 2 ⊢ (𝜑 → (𝐴 ≠ 0 ↔ 0 < 𝐴)) |
6 | 1, 5 | mpbid 224 | 1 ⊢ (𝜑 → 0 < 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∈ wcel 2051 ≠ wne 2962 class class class wbr 4926 ℝcr 10333 0cc0 10334 < clt 10473 ≤ cle 10474 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-sep 5057 ax-nul 5064 ax-pow 5116 ax-pr 5183 ax-un 7278 ax-resscn 10391 ax-1cn 10392 ax-addrcl 10395 ax-rnegex 10405 ax-cnre 10407 ax-pre-lttri 10408 ax-pre-lttrn 10409 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ne 2963 df-nel 3069 df-ral 3088 df-rex 3089 df-rab 3092 df-v 3412 df-sbc 3677 df-csb 3782 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 df-if 4346 df-pw 4419 df-sn 4437 df-pr 4439 df-op 4443 df-uni 4710 df-br 4927 df-opab 4989 df-mpt 5006 df-id 5309 df-po 5323 df-so 5324 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193 df-fv 6194 df-er 8088 df-en 8306 df-dom 8307 df-sdom 8308 df-pnf 10475 df-mnf 10476 df-xr 10477 df-ltxr 10478 df-le 10479 |
This theorem is referenced by: sqrtgt0 14478 absrpcl 14508 sqreulem 14579 fprodle 15209 efgt0 15315 abvgt0 19334 nmrpcl 22948 lebnumlem1 23284 ipcau2 23556 recxpcl 24975 mulcxp 24985 rlimcnp 25261 lgsdilem 25618 pntleml 25905 ttgcontlem1 26390 axsegconlem6 26427 axpaschlem 26445 axcontlem2 26470 axcontlem4 26472 axcontlem7 26475 xrge0iifhom 30857 cndprobprob 31375 tan2h 34358 dvasin 34452 radcnvrat 40096 ioodvbdlimc1lem2 41677 ioodvbdlimc2lem 41679 fourierdlem30 41883 fourierdlem48 41900 fourierdlem49 41901 fourierdlem54 41906 fourierdlem102 41954 fourierdlem114 41966 sqwvfoura 41974 |
Copyright terms: Public domain | W3C validator |