Theorem lenltd 11051

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801   < clt 10940   ≤ cle 10941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-cnv 5588  df-xr 10944  df-le 10946

This theorem is referenced by:  ltnsymd  11054  nltled  11055  lensymd  11056  leadd1  11373  leord1  11432  lediv1  11770  lemuldiv  11785  lerec  11788  le2msq  11805  suprleub  11871  infregelb  11889  suprfinzcl  12365  uzinfi  12597  rpnnen1lem5  12650  nn0disj  13301  fleqceilz  13502  modsumfzodifsn  13592  addmodlteq  13594  leexp2  13817  expnngt1  13884  hashf1  14099  swrdccatin2  14370  isercoll  15307  ruclem3  15870  sadcaddlem  16092  pcfac  16528  sylow1lem1  19118  fvmptnn04if  21906  chfacfisf  21911  chfacfisfcpmat  21912  ivthlem2  24521  ioorcl2  24641  itg1ge0a  24781  mbfi1fseqlem4  24788  itg2monolem1  24820  itg2cnlem1  24831  mdegmullem  25148  quotcan  25374  logdivle  25682  cxple  25755  gausslemma2dlem1a  26418  padicabv  26683  upgrewlkle2  27876  pthdlem1  28035  ssnnssfz  31010  smattr  31651  smatbl  31652  smatbr  31653  esumpcvgval  31946  eulerpartlems  32227  dstfrvunirn  32341  ballotlemodife  32364  erdszelem7  33059  erdszelem8  33060  unbdqndv2lem1  34616  poimirlem2  35706  poimirlem7  35711  poimirlem10  35714  poimirlem11  35715  areacirc  35797  aks4d1p1p7  40010  aks4d1p3  40014  aks4d1p5  40016  sticksstones22  40052  metakunt7  40059  metakunt12  40064  metakunt22  40074  metakunt28  40080  metakunt29  40081  metakunt30  40082  frlmvscadiccat  40163  rencldnfilem  40558  irrapxlem1  40560  monotoddzzfi  40680  sqrtcvallem1  41128  reabsifneg  41129  reabsifpos  41131  radcnvrat  41821  reclt0d  42816  reclt0  42821  sqrlearg  42981  dvnxpaek  43373  volico  43414  sublevolico  43415  fourierdlem12  43550  fourierdlem42  43580  elaa2lem  43664  iundjiun  43888  hoidmvval0  44015  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmvlelem4  44026  hspdifhsp  44044  volico2  44069  ovolval2lem  44071  vonioo  44110  smfconst  44172  fzopredsuc  44703  stgoldbwt  45116  nnsum3primesle9  45134  bgoldbtbndlem1  45145  ssnn0ssfz  45573