Theorem ltnle 10322

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.)

Assertion

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

Proof of Theorem ltnle

Step	Hyp	Ref	Expression
1		lenlt 10321	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
2	1	ancoms 446	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
3	2	con2bid 343	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   ∈ wcel 2145   class class class wbr 4787  ℝcr 10140   < clt 10279   ≤ cle 10280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-br 4788  df-opab 4848  df-xp 5256  df-cnv 5258  df-xr 10283  df-le 10285

This theorem is referenced by:  letric  10342  ltnled  10389  leaddsub  10709  mulge0b  11098  nnnle0  11256  nn0n0n1ge2b  11565  znnnlt1  11610  uzwo  11958  qsqueeze  12236  difreicc  12510  fzp1disj  12605  fzneuz  12627  fznuz  12628  uznfz  12629  difelfznle  12660  nelfzo  12682  ssfzoulel  12769  elfzonelfzo  12777  modfzo0difsn  12949  ssnn0fi  12991  discr1  13206  facdiv  13277  bcval5  13308  ccatsymb  13563  swrdnd  13640  swrdsbslen  13656  swrdspsleq  13657  swrdccat3  13700  repswswrd  13739  cnpart  14187  absmax  14276  rlimrege0  14517  znnenlem  15145  rpnnen2lem12  15159  alzdvds  15250  algcvgblem  15497  prmndvdsfaclt  15641  pcprendvds  15751  pcdvdsb  15779  pcmpt  15802  prmunb  15824  prmreclem2  15827  prmgaplem5  15965  prmgaplem6  15966  prmlem1  16020  prmlem2  16033  lt6abl  18502  metdseq0  22876  xrhmeo  22964  ovolicc2lem3  23506  itg2seq  23728  dvne0  23993  coeeulem  24199  radcnvlt1  24391  argimgt0  24578  cxple2  24663  ressatans  24881  eldmgm  24968  basellem2  25028  issqf  25082  bpos1  25228  bposlem3  25231  bposlem6  25234  pntpbnd2  25496  ostth2lem4  25545  crctcshwlkn0  26948  crctcsh  26951  eucrctshift  27422  ltflcei  33729  poimirlem4  33745  poimirlem13  33754  poimirlem14  33755  poimirlem15  33756  poimirlem31  33772  mblfinlem1  33778  mbfposadd  33788  itgaddnclem2  33800  ftc1anclem1  33816  ftc1anclem5  33820  dvasin  33827  icccncfext  40615  stoweidlem14  40745  stoweidlem34  40765  ltnltne  41838  pfxccat3  41951  pfxccat3a  41954  nnsum4primeseven  42213  nnsum4primesevenALTV  42214  ply1mulgsumlem2  42700