Theorem lenltd 11359

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2106   class class class wbr 5148  ℝcr 11108   < clt 11247   ≤ cle 11248

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-xr 11251  df-le 11253

This theorem is referenced by:  ltnsymd  11362  nltled  11363  lensymd  11364  leadd1  11681  leord1  11740  lediv1  12078  lemuldiv  12093  lerec  12096  le2msq  12113  suprleub  12179  infregelb  12197  suprfinzcl  12675  uzinfi  12911  rpnnen1lem5  12964  nn0disj  13616  fleqceilz  13818  modsumfzodifsn  13908  addmodlteq  13910  leexp2  14135  expnngt1  14203  hashf1  14417  swrdccatin2  14678  isercoll  15613  ruclem3  16175  sadcaddlem  16397  pcfac  16831  sylow1lem1  19465  fvmptnn04if  22350  chfacfisf  22355  chfacfisfcpmat  22356  ivthlem2  24968  ioorcl2  25088  itg1ge0a  25228  mbfi1fseqlem4  25235  itg2monolem1  25267  itg2cnlem1  25278  mdegmullem  25595  quotcan  25821  logdivle  26129  cxple  26202  gausslemma2dlem1a  26865  padicabv  27130  upgrewlkle2  28860  pthdlem1  29020  ssnnssfz  31993  smattr  32774  smatbl  32775  smatbr  32776  esumpcvgval  33071  eulerpartlems  33354  dstfrvunirn  33468  ballotlemodife  33491  erdszelem7  34183  erdszelem8  34184  unbdqndv2lem1  35380  poimirlem2  36485  poimirlem7  36490  poimirlem10  36493  poimirlem11  36494  areacirc  36576  aks4d1p1p7  40934  aks4d1p3  40938  aks4d1p5  40940  sticksstones22  40979  metakunt7  40986  metakunt12  40991  metakunt22  41001  metakunt28  41007  metakunt29  41008  metakunt30  41009  frlmvscadiccat  41082  rencldnfilem  41548  irrapxlem1  41550  monotoddzzfi  41671  sqrtcvallem1  42372  reabsifneg  42373  reabsifpos  42375  radcnvrat  43063  reclt0d  44087  reclt0  44091  sqrlearg  44256  dvnxpaek  44648  volico  44689  sublevolico  44690  fourierdlem12  44825  fourierdlem42  44855  elaa2lem  44939  iundjiun  45166  hoidmvval0  45293  hoidmv1lelem2  45298  hoidmv1lelem3  45299  hoidmvlelem4  45304  hspdifhsp  45322  volico2  45347  ovolval2lem  45349  vonioo  45388  smfconst  45455  fzopredsuc  46021  stgoldbwt  46434  nnsum3primesle9  46452  bgoldbtbndlem1  46463  ssnn0ssfz  47015