Theorem lenlt 8245

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∈ wcel 2200   class class class wbr 4086  ℝcr 8021  ℝ^*cxr 8203   < clt 8204   ≤ cle 8205

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087  df-opab 4149  df-xp 4729  df-cnv 4731  df-xr 8208  df-le 8210

This theorem is referenced by:  letri3  8250  ltleletr  8251  letr  8252  leid  8253  eqlelt  8256  ltle  8257  lelttr  8258  ltletr  8259  lenlti  8270  lenltd  8287  lemul1  8763  msqge0  8786  mulge0  8789  ltleap  8802  recgt0  9020  lediv1  9039  dfinfre  9126  nnge1  9156  nnnlt1  9159  avgle1  9375  avgle2  9376  nn0nlt0  9418  zltnle  9515  zleloe  9516  zdcle  9546  recnz  9563  btwnnz  9564  prime  9569  fznlem  10266  nelfzo  10377  fzonlt0  10394  qltnle  10493  bcval4  11004  ccatsymb  11169  swrd0g  11231  resqrexlemgt0  11571  climge0  11876  infpnlem1  12922  efle  15490  logleb  15589  cxple  15631  cxple3  15635  lgsval2lem  15729  lgsneg  15743  lgsdilem  15746  gausslemma2dlem1a  15777  gausslemma2dlem3  15782  supfz  16611  inffz  16612