Theorem lenltd 11223

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2105   class class class wbr 5093  ℝcr 10972   < clt 11111   ≤ cle 11112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5244  ax-nul 5251  ax-pr 5373

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-sn 4575  df-pr 4577  df-op 4581  df-br 5094  df-opab 5156  df-xp 5627  df-cnv 5629  df-xr 11115  df-le 11117

This theorem is referenced by:  ltnsymd  11226  nltled  11227  lensymd  11228  leadd1  11545  leord1  11604  lediv1  11942  lemuldiv  11957  lerec  11960  le2msq  11977  suprleub  12043  infregelb  12061  suprfinzcl  12538  uzinfi  12770  rpnnen1lem5  12823  nn0disj  13474  fleqceilz  13676  modsumfzodifsn  13766  addmodlteq  13768  leexp2  13991  expnngt1  14058  hashf1  14272  swrdccatin2  14541  isercoll  15479  ruclem3  16042  sadcaddlem  16264  pcfac  16698  sylow1lem1  19300  fvmptnn04if  22105  chfacfisf  22110  chfacfisfcpmat  22111  ivthlem2  24723  ioorcl2  24843  itg1ge0a  24983  mbfi1fseqlem4  24990  itg2monolem1  25022  itg2cnlem1  25033  mdegmullem  25350  quotcan  25576  logdivle  25884  cxple  25957  gausslemma2dlem1a  26620  padicabv  26885  upgrewlkle2  28263  pthdlem1  28423  ssnnssfz  31395  smattr  32047  smatbl  32048  smatbr  32049  esumpcvgval  32344  eulerpartlems  32627  dstfrvunirn  32741  ballotlemodife  32764  erdszelem7  33458  erdszelem8  33459  unbdqndv2lem1  34828  poimirlem2  35935  poimirlem7  35940  poimirlem10  35943  poimirlem11  35944  areacirc  36026  aks4d1p1p7  40387  aks4d1p3  40391  aks4d1p5  40393  sticksstones22  40432  metakunt7  40439  metakunt12  40444  metakunt22  40454  metakunt28  40460  metakunt29  40461  metakunt30  40462  frlmvscadiccat  40542  rencldnfilem  40955  irrapxlem1  40957  monotoddzzfi  41078  sqrtcvallem1  41612  reabsifneg  41613  reabsifpos  41615  radcnvrat  42305  reclt0d  43313  reclt0  43318  sqrlearg  43479  dvnxpaek  43871  volico  43912  sublevolico  43913  fourierdlem12  44048  fourierdlem42  44078  elaa2lem  44162  iundjiun  44387  hoidmvval0  44514  hoidmv1lelem2  44519  hoidmv1lelem3  44520  hoidmvlelem4  44525  hspdifhsp  44543  volico2  44568  ovolval2lem  44570  vonioo  44609  smfconst  44676  fzopredsuc  45233  stgoldbwt  45646  nnsum3primesle9  45664  bgoldbtbndlem1  45675  ssnn0ssfz  46103