Theorem ltle 8175

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

Assertion

Ref	Expression
ltle	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))

Proof of Theorem ltle

Step	Hyp	Ref	Expression
1		ltnsym 8173	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴))
2		lenlt 8163	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
3	1, 2	sylibrd 169	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∈ wcel 2177   class class class wbr 4050  ℝcr 7939   < clt 8122   ≤ cle 8123

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4169  ax-pow 4225  ax-pr 4260  ax-un 4487  ax-setind 4592  ax-cnex 8031  ax-resscn 8032  ax-pre-ltirr 8052  ax-pre-lttrn 8054

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-nel 2473  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-dif 3172  df-un 3174  df-in 3176  df-ss 3183  df-pw 3622  df-sn 3643  df-pr 3644  df-op 3646  df-uni 3856  df-br 4051  df-opab 4113  df-xp 4688  df-cnv 4690  df-pnf 8124  df-mnf 8125  df-xr 8126  df-ltxr 8127  df-le 8128

This theorem is referenced by:  ltlei  8189  ltled  8206  ltleap  8720  lep1  8933  lem1  8935  letrp1  8936  ltmul12a  8948  bndndx  9309  nn0ge0  9335  zletric  9431  zlelttric  9432  zltnle  9433  zleloe  9434  ltsubnn0  9455  zdcle  9464  uzind  9499  fnn0ind  9504  eluz2b2  9739  rpge0  9803  zltaddlt1le  10144  difelfznle  10272  elfzouz2  10299  elfzo0le  10326  fzosplitprm1  10380  fzostep1  10383  qletric  10401  qlelttric  10402  qltnle  10403  expgt1  10739  expnlbnd2  10827  faclbnd  10903  swrdsbslen  11137  swrdspsleq  11138  caucvgrelemcau  11361  resqrexlemdecn  11393  mulcn2  11693  efcllemp  12039  sin01bnd  12138  cos01bnd  12139  sin01gt0  12143  cos01gt0  12144  absef  12151  efieq1re  12153  nn0o  12288  pythagtriplem12  12668  pythagtriplem13  12669  pythagtriplem14  12670  pythagtriplem16  12672  pclemub  12680  sincosq1lem  15367  tangtx  15380