Theorem ltleii 8174

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

Hypotheses

Ref	Expression
lt.1	⊢ 𝐴 ∈ ℝ
lt.2	⊢ 𝐵 ∈ ℝ
ltlei.1	⊢ 𝐴 < 𝐵

Assertion

Ref	Expression
ltleii	⊢ 𝐴 ≤ 𝐵

Proof of Theorem ltleii

Step	Hyp	Ref	Expression
1		ltlei.1	. 2 ⊢ 𝐴 < 𝐵
2		lt.1	. . 3 ⊢ 𝐴 ∈ ℝ
3		lt.2	. . 3 ⊢ 𝐵 ∈ ℝ
4	2, 3	ltlei 8173	. 2 ⊢ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)
5	1, 4	ax-mp 5	1 ⊢ 𝐴 ≤ 𝐵

Syntax hints:   ∈ wcel 2175   class class class wbr 4043  ℝcr 7923   < clt 8106   ≤ cle 8107

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4479  ax-setind 4584  ax-cnex 8015  ax-resscn 8016  ax-pre-ltirr 8036  ax-pre-lttrn 8038

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-nel 2471  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-opab 4105  df-xp 4680  df-cnv 4682  df-pnf 8108  df-mnf 8109  df-xr 8110  df-ltxr 8111  df-le 8112

This theorem is referenced by:  0le1  8553  1le2  9244  1le3  9247  halfge0  9252  decleh  9537  eluz4eluz2  9687  uzuzle23  9691  fz0to4untppr  10245  fzo0to42pr  10347  xnn0nnen  10580  4bc2eq6  10917  resqrexlemga  11276  sqrt9  11301  sqrt2gt1lt2  11302  sqrtpclii  11383  0.999...  11774  ef01bndlem  12009  sin01bnd  12010  cos01bnd  12011  cos2bnd  12013  cos12dec  12021  flodddiv4  12189  strleun  12878  dveflem  15140  sinhalfpilem  15205  sincosq1lem  15239  sincos4thpi  15254  sincos6thpi  15256  pigt3  15258  pige3  15259  cosq34lt1  15264  cos02pilt1  15265  cos0pilt1  15266  rpabscxpbnd  15354  2logb9irr  15385  2logb9irrap  15391  lgsdir2lem1  15447  ex-fl  15594  ex-gcd  15600