Theorem subge0d 11269

Description: Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
leidd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltnegd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
subge0d	⊢ (𝜑 → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴))

Proof of Theorem subge0d

Step	Hyp	Ref	Expression
1		leidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltnegd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		subge0 11192	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴))
4	1, 2, 3	syl2anc 588	1 ⊢ (𝜑 → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴))

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2112   class class class wbr 5033  (class class class)co 7151  ℝcr 10575  0cc0 10576   ≤ cle 10715   − cmin 10909

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 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-resscn 10633  ax-1cn 10634  ax-icn 10635  ax-addcl 10636  ax-addrcl 10637  ax-mulcl 10638  ax-mulrcl 10639  ax-mulcom 10640  ax-addass 10641  ax-mulass 10642  ax-distr 10643  ax-i2m1 10644  ax-1ne0 10645  ax-1rid 10646  ax-rnegex 10647  ax-rrecex 10648  ax-cnre 10649  ax-pre-lttri 10650  ax-pre-lttrn 10651  ax-pre-ltadd 10652

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 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-po 5444  df-so 5445  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  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 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-pnf 10716  df-mnf 10717  df-xr 10718  df-ltxr 10719  df-le 10720  df-sub 10911  df-neg 10912

This theorem is referenced by:  ofsubge0  11674  uzsubsubfz  12979  modsubdir  13358  modsumfzodifsn  13362  serle  13476  discr  13652  bcval5  13729  fzomaxdiflem  14751  sqreulem  14768  amgm2  14778  climle  15045  rlimle  15053  iseralt  15090  fsumle  15203  cvgcmp  15220  binomrisefac  15445  smuval2  15882  pcz  16273  4sqlem15  16351  mndodconglem  18737  ipcau2  23935  pjthlem1  24138  ovolicc2lem4  24221  vitalilem2  24310  itg1lea  24413  dvlip  24693  dvge0  24706  dvle  24707  dvivthlem1  24708  dvfsumlem2  24727  dvfsumlem4  24729  loglesqrt  25447  emcllem6  25686  harmoniclbnd  25694  basellem9  25774  gausslemma2dlem0h  26047  lgseisenlem1  26059  2sqmod  26120  vmadivsum  26166  rplogsumlem1  26168  dchrisumlem2  26174  rplogsum  26211  vmalogdivsum2  26222  selberg2lem  26234  logdivbnd  26240  pntpbnd2  26271  pntibndlem2  26275  pntlemg  26282  pntlemn  26284  ttgcontlem1  26779  brbtwn2  26799  axpaschlem  26834  axcontlem8  26865  crctcsh  27710  clwlkclwwlklem2a1  27877  clwlkclwwlklem2fv2  27881  pjhthlem1  29274  leop2  30007  pjssposi  30055  fdvposle  32101  rddif2  34207  dnibndlem4  34211  broucube  35372  areacirclem2  35427  areacirclem4  35429  areacirclem5  35430  areacirc  35431  metakunt29  39676  acongrep  40295  sqrtcvallem2  40711  sqrtcvallem4  40713  lptre2pt  42649  dvnmul  42952  dvnprodlem1  42955  dvnprodlem2  42956  stoweidlem1  43010  stoweidlem26  43035  stoweidlem62  43071  wallispilem4  43077  fourierdlem26  43142  fourierdlem42  43158  fourierdlem65  43180  fourierdlem75  43190  elaa2lem  43242  etransclem3  43246  etransclem7  43250  etransclem10  43253  etransclem20  43263  etransclem21  43264  etransclem22  43265  etransclem24  43267  etransclem27  43270  hoidmvlelem1  43601  nnpw2pmod  45363  2itscp  45561