Theorem lenlt 7624

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 1439   class class class wbr 3853  ℝcr 7412  ℝ^*cxr 7584   < clt 7585   ≤ cle 7586

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-pow 4017  ax-pr 4047

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-v 2624  df-dif 3004  df-un 3006  df-in 3008  df-ss 3015  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-br 3854  df-opab 3908  df-xp 4460  df-cnv 4462  df-xr 7589  df-le 7591

This theorem is referenced by:  letri3  7629  ltleletr  7630  letr  7631  leid  7632  ltle  7635  lelttr  7636  ltletr  7637  lenlti  7648  lenltd  7664  lemul1  8133  msqge0  8156  mulge0  8159  ltleap  8170  recgt0  8374  lediv1  8393  dfinfre  8480  nnge1  8508  nnnlt1  8511  avgle1  8719  avgle2  8720  nn0nlt0  8762  zltnle  8859  zleloe  8860  zdcle  8886  recnz  8902  btwnnz  8903  prime  8908  fznlem  9518  fzonlt0  9641  qltnle  9720  bcval4  10223  resqrexlemgt0  10516  climge0  10776  efler  11052  supfz  12219  inffz  12220