Theorem lenltd 11320

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067   < clt 11208   ≤ cle 11209

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-xr 11212  df-le 11214

This theorem is referenced by:  ltnsymd  11323  nltled  11324  lensymd  11325  leadd1  11646  leord1  11705  lediv1  12048  lemuldiv  12063  lerec  12066  le2msq  12083  suprleub  12149  infregelb  12167  suprfinzcl  12648  uzinfi  12887  rpnnen1lem5  12940  nn0disj  13605  fleqceilz  13816  modsumfzodifsn  13909  addmodlteq  13911  leexp2  14136  expnngt1  14206  hashf1  14422  swrdccatin2  14694  isercoll  15634  ruclem3  16201  sadcaddlem  16427  pcfac  16870  sylow1lem1  19528  fvmptnn04if  22736  chfacfisf  22741  chfacfisfcpmat  22742  ivthlem2  25353  ioorcl2  25473  itg1ge0a  25612  mbfi1fseqlem4  25619  itg2monolem1  25651  itg2cnlem1  25662  mdegmullem  25983  quotcan  26217  logdivle  26531  cxple  26604  gausslemma2dlem1a  27276  padicabv  27541  upgrewlkle2  29534  pthdlem1  29696  ssnnssfz  32710  smattr  33789  smatbl  33790  smatbr  33791  esumpcvgval  34068  eulerpartlems  34351  dstfrvunirn  34466  ballotlemodife  34489  erdszelem7  35184  erdszelem8  35185  unbdqndv2lem1  36497  poimirlem2  37616  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  areacirc  37707  aks4d1p1p7  42062  aks4d1p3  42066  aks4d1p5  42068  hashscontpow1  42109  sticksstones22  42156  aks6d1c6lem4  42161  aks5lem8  42189  readvrec  42350  frlmvscadiccat  42494  rencldnfilem  42808  irrapxlem1  42810  monotoddzzfi  42931  sqrtcvallem1  43620  reabsifneg  43621  reabsifpos  43623  radcnvrat  44303  reclt0d  45383  reclt0  45387  sqrlearg  45551  dvnxpaek  45940  volico  45981  sublevolico  45982  fourierdlem12  46117  fourierdlem42  46147  elaa2lem  46231  iundjiun  46458  hoidmvval0  46585  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmvlelem4  46596  hspdifhsp  46614  volico2  46639  ovolval2lem  46641  vonioo  46680  smfconst  46747  fzopredsuc  47324  stgoldbwt  47777  nnsum3primesle9  47795  bgoldbtbndlem1  47806  ssnn0ssfz  48337