Theorem lenltd 11408

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 11340	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2107   class class class wbr 5142  ℝcr 11155   < clt 11296   ≤ cle 11297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-xp 5690  df-cnv 5692  df-xr 11300  df-le 11302

This theorem is referenced by:  ltnsymd  11411  nltled  11412  lensymd  11413  leadd1  11732  leord1  11791  lediv1  12134  lemuldiv  12149  lerec  12152  le2msq  12169  suprleub  12235  infregelb  12253  suprfinzcl  12734  uzinfi  12971  rpnnen1lem5  13024  nn0disj  13685  fleqceilz  13895  modsumfzodifsn  13986  addmodlteq  13988  leexp2  14212  expnngt1  14281  hashf1  14497  swrdccatin2  14768  isercoll  15705  ruclem3  16270  sadcaddlem  16495  pcfac  16938  sylow1lem1  19617  fvmptnn04if  22856  chfacfisf  22861  chfacfisfcpmat  22862  ivthlem2  25488  ioorcl2  25608  itg1ge0a  25747  mbfi1fseqlem4  25754  itg2monolem1  25786  itg2cnlem1  25797  mdegmullem  26118  quotcan  26352  logdivle  26665  cxple  26738  gausslemma2dlem1a  27410  padicabv  27675  upgrewlkle2  29625  pthdlem1  29787  ssnnssfz  32790  smattr  33799  smatbl  33800  smatbr  33801  esumpcvgval  34080  eulerpartlems  34363  dstfrvunirn  34478  ballotlemodife  34501  erdszelem7  35203  erdszelem8  35204  unbdqndv2lem1  36511  poimirlem2  37630  poimirlem7  37635  poimirlem10  37638  poimirlem11  37639  areacirc  37721  aks4d1p1p7  42076  aks4d1p3  42080  aks4d1p5  42082  hashscontpow1  42123  sticksstones22  42170  aks6d1c6lem4  42175  aks5lem8  42203  metakunt7  42213  metakunt12  42218  metakunt22  42228  metakunt28  42234  metakunt29  42235  metakunt30  42236  readvrec  42397  frlmvscadiccat  42521  rencldnfilem  42836  irrapxlem1  42838  monotoddzzfi  42959  sqrtcvallem1  43649  reabsifneg  43650  reabsifpos  43652  radcnvrat  44338  reclt0d  45403  reclt0  45407  sqrlearg  45571  dvnxpaek  45962  volico  46003  sublevolico  46004  fourierdlem12  46139  fourierdlem42  46169  elaa2lem  46253  iundjiun  46480  hoidmvval0  46607  hoidmv1lelem2  46612  hoidmv1lelem3  46613  hoidmvlelem4  46618  hspdifhsp  46636  volico2  46661  ovolval2lem  46663  vonioo  46702  smfconst  46769  fzopredsuc  47340  stgoldbwt  47768  nnsum3primesle9  47786  bgoldbtbndlem1  47797  ssnn0ssfz  48270