Theorem lenltd 10788

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∈ wcel 2114   class class class wbr 5068  ℝcr 10538   < clt 10677   ≤ cle 10678

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 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-xp 5563  df-cnv 5565  df-xr 10681  df-le 10683

This theorem is referenced by:  ltnsymd  10791  nltled  10792  lensymd  10793  leadd1  11110  leord1  11169  lediv1  11507  lemuldiv  11522  lerec  11525  le2msq  11542  suprleub  11609  infregelb  11627  suprfinzcl  12100  uzinfi  12331  rpnnen1lem5  12383  nn0disj  13026  fleqceilz  13225  modsumfzodifsn  13315  addmodlteq  13317  leexp2  13538  expnngt1  13605  hashf1  13818  swrdccatin2  14093  isercoll  15026  ruclem3  15588  sadcaddlem  15808  pcfac  16237  sylow1lem1  18725  fvmptnn04if  21459  chfacfisf  21464  chfacfisfcpmat  21465  ivthlem2  24055  ioorcl2  24175  itg1ge0a  24314  mbfi1fseqlem4  24321  itg2monolem1  24353  itg2cnlem1  24364  mdegmullem  24674  quotcan  24900  logdivle  25207  cxple  25280  gausslemma2dlem1a  25943  padicabv  26208  upgrewlkle2  27390  pthdlem1  27549  ssnnssfz  30512  smattr  31066  smatbl  31067  smatbr  31068  esumpcvgval  31339  eulerpartlems  31620  dstfrvunirn  31734  ballotlemodife  31757  erdszelem7  32446  erdszelem8  32447  unbdqndv2lem1  33850  poimirlem2  34896  poimirlem7  34901  poimirlem10  34904  poimirlem11  34905  areacirc  34989  frlmvscadiccat  39152  rencldnfilem  39424  irrapxlem1  39426  monotoddzzfi  39546  radcnvrat  40653  reclt0d  41665  reclt0  41670  sqrlearg  41836  dvnxpaek  42234  volico  42275  sublevolico  42276  fourierdlem12  42411  fourierdlem42  42441  elaa2lem  42525  iundjiun  42749  hoidmvval0  42876  hoidmv1lelem2  42881  hoidmv1lelem3  42882  hoidmvlelem4  42887  hspdifhsp  42905  volico2  42930  ovolval2lem  42932  vonioo  42971  smfconst  43033  fzopredsuc  43530  stgoldbwt  43948  nnsum3primesle9  43966  bgoldbtbndlem1  43977  ssnn0ssfz  44404