Theorem ltle 8114

Description: 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)

Assertion

Ref	Expression
ltle	|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )

Proof of Theorem ltle

Step	Hyp	Ref	Expression
1		ltnsym 8112	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A < B -> -. B < A ) )
2		lenlt 8102	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
3	1, 2	sylibrd 169	1 |- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   e. wcel 2167   class class class wbr 4033   RRcr 7878   < clt 8061   <_ cle 8062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-cnex 7970  ax-resscn 7971  ax-pre-ltirr 7991  ax-pre-lttrn 7993

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-rab 2484  df-v 2765  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-opab 4095  df-xp 4669  df-cnv 4671  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067

This theorem is referenced by:  ltlei  8128  ltled  8145  ltleap  8659  lep1  8872  lem1  8874  letrp1  8875  ltmul12a  8887  bndndx  9248  nn0ge0  9274  zletric  9370  zlelttric  9371  zltnle  9372  zleloe  9373  ltsubnn0  9393  zdcle  9402  uzind  9437  fnn0ind  9442  eluz2b2  9677  rpge0  9741  zltaddlt1le  10082  difelfznle  10210  elfzouz2  10237  elfzo0le  10261  fzosplitprm1  10310  fzostep1  10313  qletric  10331  qlelttric  10332  qltnle  10333  expgt1  10669  expnlbnd2  10757  faclbnd  10833  caucvgrelemcau  11145  resqrexlemdecn  11177  mulcn2  11477  efcllemp  11823  sin01bnd  11922  cos01bnd  11923  sin01gt0  11927  cos01gt0  11928  absef  11935  efieq1re  11937  nn0o  12072  pythagtriplem12  12444  pythagtriplem13  12445  pythagtriplem14  12446  pythagtriplem16  12448  pclemub  12456  sincosq1lem  15061  tangtx  15074