Theorem lenltd 11327

Description: 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

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

Assertion

Ref	Expression
lenltd	⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Proof of Theorem lenltd

Step	Hyp	Ref	Expression
1		ltd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		lenlt 11259	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074   < clt 11215   ≤ cle 11216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-xr 11219  df-le 11221

This theorem is referenced by:  ltnsymd  11330  nltled  11331  lensymd  11332  leadd1  11653  leord1  11712  lediv1  12055  lemuldiv  12070  lerec  12073  le2msq  12090  suprleub  12156  infregelb  12174  suprfinzcl  12655  uzinfi  12894  rpnnen1lem5  12947  nn0disj  13612  fleqceilz  13823  modsumfzodifsn  13916  addmodlteq  13918  leexp2  14143  expnngt1  14213  hashf1  14429  swrdccatin2  14701  isercoll  15641  ruclem3  16208  sadcaddlem  16434  pcfac  16877  sylow1lem1  19535  fvmptnn04if  22743  chfacfisf  22748  chfacfisfcpmat  22749  ivthlem2  25360  ioorcl2  25480  itg1ge0a  25619  mbfi1fseqlem4  25626  itg2monolem1  25658  itg2cnlem1  25669  mdegmullem  25990  quotcan  26224  logdivle  26538  cxple  26611  gausslemma2dlem1a  27283  padicabv  27548  upgrewlkle2  29541  pthdlem1  29703  ssnnssfz  32717  smattr  33796  smatbl  33797  smatbr  33798  esumpcvgval  34075  eulerpartlems  34358  dstfrvunirn  34473  ballotlemodife  34496  erdszelem7  35191  erdszelem8  35192  unbdqndv2lem1  36504  poimirlem2  37623  poimirlem7  37628  poimirlem10  37631  poimirlem11  37632  areacirc  37714  aks4d1p1p7  42069  aks4d1p3  42073  aks4d1p5  42075  hashscontpow1  42116  sticksstones22  42163  aks6d1c6lem4  42168  aks5lem8  42196  readvrec  42357  frlmvscadiccat  42501  rencldnfilem  42815  irrapxlem1  42817  monotoddzzfi  42938  sqrtcvallem1  43627  reabsifneg  43628  reabsifpos  43630  radcnvrat  44310  reclt0d  45390  reclt0  45394  sqrlearg  45558  dvnxpaek  45947  volico  45988  sublevolico  45989  fourierdlem12  46124  fourierdlem42  46154  elaa2lem  46238  iundjiun  46465  hoidmvval0  46592  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmvlelem4  46603  hspdifhsp  46621  volico2  46646  ovolval2lem  46648  vonioo  46687  smfconst  46754  fzopredsuc  47328  stgoldbwt  47781  nnsum3primesle9  47799  bgoldbtbndlem1  47810  ssnn0ssfz  48341