Theorem lenltd 10183

Description: 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
ltd.1	|- ( ph -> A e. RR )
ltd.2	|- ( ph -> B e. RR )

Assertion

Ref	Expression
lenltd	|- ( ph -> ( A <_ B <-> -. B < A ) )

Proof of Theorem lenltd

Step	Hyp	Ref	Expression
1		ltd.1	. 2 |- ( ph -> A e. RR )
2		ltd.2	. 2 |- ( ph -> B e. RR )
3		lenlt 10116	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> ( A <_ B <-> -. B < A ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   e. wcel 1990   class class class wbr 4653   RRcr 9935   < clt 10074   <_ cle 10075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-cnv 5122  df-xr 10078  df-le 10080

This theorem is referenced by:  ltnsymd  10186  nltled  10187  lensymd  10188  dedekind  10200  leadd1  10496  leord1  10555  prodge0  10870  lediv1  10888  lemuldiv  10903  lerec  10906  le2msq  10923  suprub  10984  suprleub  10989  supaddc  10990  supmul1  10992  infregelb  11007  suprfinzcl  11492  uzinfi  11768  zsupss  11777  suprzub  11779  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  fzdisj  12368  uzdisj  12413  nn0disj  12455  fzouzdisj  12504  fleqceilz  12653  modsumfzodifsn  12743  addmodlteq  12745  seqf1olem1  12840  seqf1olem2  12841  leexp2  12915  hashf1  13241  seqcoll  13248  seqcoll2  13249  ccatsymb  13366  swrdccatin2  13487  rlimcld2  14309  rlimno1  14384  isercoll  14398  ruclem3  14962  bitsfzolem  15156  bitsmod  15158  sadcaddlem  15179  smupvallem  15205  pcfac  15603  4sqlem11  15659  ramcl2lem  15713  sylow1lem1  18013  fvmptnn04if  20654  chfacfisf  20659  chfacfisfcpmat  20660  recld2  22617  reconnlem2  22630  ivthlem2  23221  ivthlem3  23222  ovolicopnf  23292  ioombl1lem4  23329  ioorcl2  23340  itg1ge0a  23478  mbfi1fseqlem4  23485  itg2monolem1  23517  itg2cnlem1  23528  dvferm1lem  23747  dvferm2lem  23749  mdegmullem  23838  dgrub  23990  dgrlb  23992  dgreq0  24021  quotcan  24064  aaliou3lem9  24105  radcnvle  24174  abelthlem2  24186  logdivle  24368  cxple  24441  lgsval2lem  25032  gausslemma2dlem1a  25090  padicabv  25319  pthdlem1  26662  ssnnssfz  29549  smattr  29865  smatbl  29866  smatbr  29867  esumpcvgval  30140  eulerpartlems  30422  dstfrvunirn  30536  ballotlemodife  30559  erdszelem7  31179  erdszelem8  31180  unblimceq0  32498  unbdqndv2lem1  32500  poimirlem2  33411  poimirlem7  33416  poimirlem10  33419  poimirlem11  33420  areacirc  33505  rencldnfilem  37384  irrapxlem1  37386  monotoddzzfi  37507  radcnvrat  38513  reclt0d  39607  reclt0  39614  sqrlearg  39780  dvnxpaek  40157  volico  40200  sublevolico  40201  fourierdlem12  40336  fourierdlem42  40366  elaa2lem  40450  iundjiun  40677  hoidmvval0  40801  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmvlelem4  40812  hspdifhsp  40830  volico2  40855  ovolval2lem  40857  vonioo  40896  smfconst  40958  fzopredsuc  41333  stgoldbwt  41664  nnsum3primesle9  41682  bgoldbtbndlem1  41693  ssnn0ssfz  42127