ltnle - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ltnle		Structured version Visualization version GIF version

Theorem ltnle 11329

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 11328	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
2	1	ancoms 457	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
3	2	con2bid 353	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∈ wcel 2098 class class class wbr 5150 ℝcr 11143 < clt 11284 ≤ cle 11285

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698 ax-sep 5301 ax-nul 5308 ax-pr 5431

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5151 df-opab 5213 df-xp 5686 df-cnv 5688 df-xr 11288 df-le 11290

This theorem is referenced by: letric 11350 ltnled 11397 leaddsub 11726 mulge0b 12120 nnnle0 12281 nn0n0n1ge2b 12576 znnnlt1 12625 uzwo 12931 qsqueeze 13218 difreicc 13499 fzp1disj 13598 fzneuz 13620 fznuz 13621 uznfz 13622 difelfznle 13653 nelfzo 13675 ssfzoulel 13764 elfzonelfzo 13772 modfzo0difsn 13946 ssnn0fi 13988 discr1 14239 bcval5 14315 swrdnd 14642 swrdnnn0nd 14644 swrdnd0 14645 swrdsbslen 14652 swrdspsleq 14653 pfxnd0 14676 pfxccat3 14722 swrdccat 14723 pfxccat3a 14726 repswswrd 14772 cnpart 15225 absmax 15314 rlimrege0 15561 rpnnen2lem12 16207 alzdvds 16302 algcvgblem 16553 prmndvdsfaclt 16702 pcprendvds 16814 pcdvdsb 16843 pcmpt 16866 prmunb 16888 prmreclem2 16891 prmgaplem5 17029 prmgaplem6 17030 prmlem1 17082 prmlem2 17094 lt6abl 19855 metdseq0 24788 xrhmeo 24889 ovolicc2lem3 25466 itg2seq 25690 dvne0 25962 coeeulem 26176 radcnvlt1 26372 argimgt0 26564 cxple2 26649 ressatans 26884 eldmgm 26972 basellem2 27032 issqf 27086 bpos1 27234 bposlem3 27237 bposlem6 27240 2sqreulem1 27397 2sqreunnlem1 27400 pntpbnd2 27538 ostth2lem4 27587 crctcshwlkn0 29650 crctcsh 29653 eucrctshift 30071 ltflcei 37086 poimirlem4 37102 poimirlem13 37111 poimirlem14 37112 poimirlem15 37113 poimirlem31 37129 mblfinlem1 37135 mbfposadd 37145 itgaddnclem2 37157 ftc1anclem1 37171 ftc1anclem5 37175 dvasin 37182 reabsifnpos 43066 reabsifnneg 43068 icccncfext 45277 stoweidlem14 45404 stoweidlem34 45424 ltnltne 46681 nnsum4primeseven 47142 nnsum4primesevenALTV 47143 ply1mulgsumlem2 47506

	
		OSZAR »