Theorem lenltd 11291

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037   < clt 11178   ≤ cle 11179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-xr 11182  df-le 11184

This theorem is referenced by:  ltnsymd  11294  nltled  11295  lensymd  11296  leadd1  11617  leord1  11676  lediv1  12019  lemuldiv  12034  lerec  12037  le2msq  12054  suprleub  12120  infregelb  12138  suprfinzcl  12618  uzinfi  12853  rpnnen1lem5  12906  nn0disj  13572  fleqceilz  13786  modsumfzodifsn  13879  addmodlteq  13881  leexp2  14106  expnngt1  14176  hashf1  14392  swrdccatin2  14664  isercoll  15603  ruclem3  16170  sadcaddlem  16396  pcfac  16839  sylow1lem1  19539  fvmptnn04if  22805  chfacfisf  22810  chfacfisfcpmat  22811  ivthlem2  25421  ioorcl2  25541  itg1ge0a  25680  mbfi1fseqlem4  25687  itg2monolem1  25719  itg2cnlem1  25730  mdegmullem  26051  quotcan  26285  logdivle  26599  cxple  26672  gausslemma2dlem1a  27344  padicabv  27609  upgrewlkle2  29692  pthdlem1  29851  ssnnssfz  32878  smattr  33977  smatbl  33978  smatbr  33979  esumpcvgval  34256  eulerpartlems  34538  dstfrvunirn  34653  ballotlemodife  34676  erdszelem7  35413  erdszelem8  35414  unbdqndv2lem1  36731  poimirlem2  37873  poimirlem7  37878  poimirlem10  37881  poimirlem11  37882  areacirc  37964  aks4d1p1p7  42444  aks4d1p3  42448  aks4d1p5  42450  hashscontpow1  42491  sticksstones22  42538  aks6d1c6lem4  42543  aks5lem8  42571  readvrec  42732  frlmvscadiccat  42876  rencldnfilem  43177  irrapxlem1  43179  monotoddzzfi  43299  sqrtcvallem1  43987  reabsifneg  43988  reabsifpos  43990  radcnvrat  44670  reclt0d  45745  reclt0  45749  sqrlearg  45913  dvnxpaek  46300  volico  46341  sublevolico  46342  fourierdlem12  46477  fourierdlem42  46507  elaa2lem  46591  iundjiun  46818  hoidmvval0  46945  hoidmv1lelem2  46950  hoidmv1lelem3  46951  hoidmvlelem4  46956  hspdifhsp  46974  volico2  46999  ovolval2lem  47001  vonioo  47040  smfconst  47107  fzopredsuc  47683  stgoldbwt  48136  nnsum3primesle9  48154  bgoldbtbndlem1  48165  ssnn0ssfz  48709