Theorem lenltd 10441

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197   ∈ wcel 2155   class class class wbr 4811  ℝcr 10192   < clt 10332   ≤ cle 10333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-br 4812  df-opab 4874  df-xp 5285  df-cnv 5287  df-xr 10336  df-le 10338

This theorem is referenced by:  ltnsymd  10444  nltled  10445  lensymd  10446  dedekind  10458  leadd1  10754  leord1  10813  prodge0OLD  11128  lediv1  11146  lemuldiv  11161  lerec  11164  le2msq  11181  suprub  11242  suprleub  11247  supaddc  11248  supmul1  11250  infregelb  11265  suprfinzcl  11744  uzinfi  11974  zsupss  11983  suprzub  11985  rpnnen1lem5  12024  fzdisj  12580  uzdisj  12625  nn0disj  12668  fzouzdisj  12717  fleqceilz  12866  modsumfzodifsn  12956  addmodlteq  12958  seqf1olem1  13052  seqf1olem2  13053  leexp2  13127  hashf1  13447  seqcoll  13454  seqcoll2  13455  ccatsymb  13559  swrdccatin2  13748  rlimcld2  14608  rlimno1  14683  isercoll  14697  ruclem3  15258  bitsfzolem  15451  bitsmod  15453  sadcaddlem  15474  smupvallem  15500  pcfac  15896  4sqlem11  15952  ramcl2lem  16006  sylow1lem1  18291  fvmptnn04if  20947  chfacfisf  20952  chfacfisfcpmat  20953  recld2  22910  reconnlem2  22923  ivthlem2  23524  ivthlem3  23525  ovolicopnf  23596  ioombl1lem4  23633  ioorcl2  23644  itg1ge0a  23783  mbfi1fseqlem4  23790  itg2monolem1  23822  itg2cnlem1  23833  dvferm1lem  24052  dvferm2lem  24054  mdegmullem  24143  dgrub  24295  dgrlb  24297  dgreq0  24326  quotcan  24369  aaliou3lem9  24410  radcnvle  24479  abelthlem2  24491  logdivle  24673  cxple  24746  lgsval2lem  25337  gausslemma2dlem1a  25395  padicabv  25624  pthdlem1  26972  ssnnssfz  30019  smattr  30333  smatbl  30334  smatbr  30335  esumpcvgval  30608  eulerpartlems  30890  dstfrvunirn  31005  ballotlemodife  31028  erdszelem7  31648  erdszelem8  31649  unblimceq0  32958  unbdqndv2lem1  32960  poimirlem2  33856  poimirlem7  33861  poimirlem10  33864  poimirlem11  33865  areacirc  33949  rencldnfilem  38086  irrapxlem1  38088  monotoddzzfi  38208  radcnvrat  39211  reclt0d  40269  reclt0  40275  sqrlearg  40442  dvnxpaek  40819  volico  40861  sublevolico  40862  fourierdlem12  40997  fourierdlem42  41027  elaa2lem  41111  iundjiun  41338  hoidmvval0  41465  hoidmv1lelem2  41470  hoidmv1lelem3  41471  hoidmvlelem4  41476  hspdifhsp  41494  volico2  41519  ovolval2lem  41521  vonioo  41560  smfconst  41622  fzopredsuc  42091  stgoldbwt  42364  nnsum3primesle9  42382  bgoldbtbndlem1  42393  ssnn0ssfz  42820