Theorem lenlt 8349

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 8319	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2		rexr 8319	. 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3		xrlenlt 8338	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
4	1, 2, 3	syl2an 289	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∈ wcel 2203   class class class wbr 4109  ℝcr 8126  ℝ^*cxr 8307   < clt 8308   ≤ cle 8309

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110  df-opab 4172  df-xp 4755  df-cnv 4757  df-xr 8312  df-le 8314

This theorem is referenced by:  letri3  8354  ltleletr  8355  letr  8356  leid  8357  eqlelt  8360  ltle  8361  lelttr  8362  ltletr  8363  lenlti  8374  lenltd  8391  lemul1  8867  msqge0  8890  mulge0  8893  ltleap  8906  recgt0  9124  lediv1  9143  dfinfre  9230  nnge1  9260  nnnlt1  9263  avgle1  9479  avgle2  9480  nn0nlt0  9522  zltnle  9623  zleloe  9624  zdcle  9654  recnz  9671  btwnnz  9672  prime  9677  fznlem  10375  nelfzo  10486  fzonlt0  10503  qltnle  10603  bcval4  11114  ccatsymb  11290  swrd0g  11352  resqrexlemgt0  11705  climge0  12010  infpnlem1  13057  efle  15641  logleb  15740  cxple  15782  cxple3  15786  lgsval2lem  15883  lgsneg  15897  lgsdilem  15900  gausslemma2dlem1a  15931  gausslemma2dlem3  15936  supfz  16857  inffz  16858