Theorem lenlt 8254

Description: 'Less than or equal to' expressed in terms of 'less than'. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 13-May-1999.)

Assertion

Ref	Expression
lenlt	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Proof of Theorem lenlt

Step	Hyp	Ref	Expression
1		rexr 8224	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2		rexr 8224	. 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3		xrlenlt 8243	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
4	1, 2, 3	syl2an 289	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∈ wcel 2202   class class class wbr 4088  ℝcr 8030  ℝ^*cxr 8212   < clt 8213   ≤ cle 8214

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089  df-opab 4151  df-xp 4731  df-cnv 4733  df-xr 8217  df-le 8219

This theorem is referenced by:  letri3  8259  ltleletr  8260  letr  8261  leid  8262  eqlelt  8265  ltle  8266  lelttr  8267  ltletr  8268  lenlti  8279  lenltd  8296  lemul1  8772  msqge0  8795  mulge0  8798  ltleap  8811  recgt0  9029  lediv1  9048  dfinfre  9135  nnge1  9165  nnnlt1  9168  avgle1  9384  avgle2  9385  nn0nlt0  9427  zltnle  9524  zleloe  9525  zdcle  9555  recnz  9572  btwnnz  9573  prime  9578  fznlem  10275  nelfzo  10386  fzonlt0  10403  qltnle  10502  bcval4  11013  ccatsymb  11178  swrd0g  11240  resqrexlemgt0  11580  climge0  11885  infpnlem1  12931  efle  15499  logleb  15598  cxple  15640  cxple3  15644  lgsval2lem  15738  lgsneg  15752  lgsdilem  15755  gausslemma2dlem1a  15786  gausslemma2dlem3  15791  supfz  16675  inffz  16676