Theorem lenltd 10786

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∈ wcel 2114   class class class wbr 5066  ℝcr 10536   < clt 10675   ≤ cle 10676

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-cnv 5563  df-xr 10679  df-le 10681

This theorem is referenced by:  ltnsymd  10789  nltled  10790  lensymd  10791  leadd1  11108  leord1  11167  lediv1  11505  lemuldiv  11520  lerec  11523  le2msq  11540  suprleub  11607  infregelb  11625  suprfinzcl  12098  uzinfi  12329  rpnnen1lem5  12381  nn0disj  13024  fleqceilz  13223  modsumfzodifsn  13313  addmodlteq  13315  leexp2  13536  expnngt1  13603  hashf1  13816  swrdccatin2  14091  isercoll  15024  ruclem3  15586  sadcaddlem  15806  pcfac  16235  sylow1lem1  18723  fvmptnn04if  21457  chfacfisf  21462  chfacfisfcpmat  21463  ivthlem2  24053  ioorcl2  24173  itg1ge0a  24312  mbfi1fseqlem4  24319  itg2monolem1  24351  itg2cnlem1  24362  mdegmullem  24672  quotcan  24898  logdivle  25205  cxple  25278  gausslemma2dlem1a  25941  padicabv  26206  upgrewlkle2  27388  pthdlem1  27547  ssnnssfz  30510  smattr  31064  smatbl  31065  smatbr  31066  esumpcvgval  31337  eulerpartlems  31618  dstfrvunirn  31732  ballotlemodife  31755  erdszelem7  32444  erdszelem8  32445  unbdqndv2lem1  33848  poimirlem2  34909  poimirlem7  34914  poimirlem10  34917  poimirlem11  34918  areacirc  35002  frlmvscadiccat  39194  rencldnfilem  39466  irrapxlem1  39468  monotoddzzfi  39588  radcnvrat  40695  reclt0d  41707  reclt0  41712  sqrlearg  41878  dvnxpaek  42276  volico  42317  sublevolico  42318  fourierdlem12  42453  fourierdlem42  42483  elaa2lem  42567  iundjiun  42791  hoidmvval0  42918  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmvlelem4  42929  hspdifhsp  42947  volico2  42972  ovolval2lem  42974  vonioo  43013  smfconst  43075  fzopredsuc  43572  stgoldbwt  43990  nnsum3primesle9  44008  bgoldbtbndlem1  44019  ssnn0ssfz  44446