Theorem ne0gt0d 10576

Description: A nonzero nonnegative number is positive. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ne0gt0d.2	⊢ (𝜑 → 0 ≤ 𝐴)
ne0gt0d.3	⊢ (𝜑 → 𝐴 ≠ 0)

Assertion

Ref	Expression
ne0gt0d	⊢ (𝜑 → 0 < 𝐴)

Proof of Theorem ne0gt0d

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 < 𝐴)

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