Theorem lenlt 7999

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 2142   class class class wbr 3990  ℝcr 7777  ℝ^*cxr 7957   < clt 7958   ≤ cle 7959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-pow 4161  ax-pr 4195

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-v 2733  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-br 3991  df-opab 4052  df-xp 4618  df-cnv 4620  df-xr 7962  df-le 7964

This theorem is referenced by:  letri3  8004  ltleletr  8005  letr  8006  leid  8007  eqlelt  8010  ltle  8011  lelttr  8012  ltletr  8013  lenlti  8024  lenltd  8041  lemul1  8516  msqge0  8539  mulge0  8542  ltleap  8555  recgt0  8770  lediv1  8789  dfinfre  8876  nnge1  8905  nnnlt1  8908  avgle1  9122  avgle2  9123  nn0nlt0  9165  zltnle  9262  zleloe  9263  zdcle  9292  recnz  9309  btwnnz  9310  prime  9315  fznlem  10001  fzonlt0  10127  qltnle  10206  bcval4  10690  resqrexlemgt0  10988  climge0  11292  infpnlem1  12315  efle  13576  logleb  13675  cxple  13716  cxple3  13720  lgsval2lem  13790  lgsneg  13804  lgsdilem  13807  supfz  14185  inffz  14186