zltnle - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > zltnle		GIF version

Theorem zltnle 9690

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.)

**Assertion**
Ref	Expression
zltnle	⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

**Proof of Theorem zltnle**
Step	Hyp	Ref	Expression
1		zre 9648	. . . . 5 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℝ)
2		zre 9648	. . . . 5 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
3		lenlt 8401	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
4	1, 2, 3	syl2anr 290	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
5	4	biimpd 144	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 ≤ 𝐴 → ¬ 𝐴 < 𝐵))
6	5	con2d 633	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 → ¬ 𝐵 ≤ 𝐴))
7		ztri3or 9687	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴))
8		ax-1 6	. . . . 5 ⊢ (𝐴 < 𝐵 → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵))
9	8	a1i 9	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵)))
10		eqcom 2240	. . . . . . . . 9 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
11		eqle 8417	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 = 𝐴) → 𝐵 ≤ 𝐴)
12	10, 11	sylan2b 287	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐵 ≤ 𝐴)
13	12	ex 115	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → (𝐴 = 𝐵 → 𝐵 ≤ 𝐴))
14	13	adantl 277	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 → 𝐵 ≤ 𝐴))
15	1, 14	sylan2 286	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 = 𝐵 → 𝐵 ≤ 𝐴))
16		pm2.24 630	. . . . 5 ⊢ (𝐵 ≤ 𝐴 → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵))
17	15, 16	syl6 33	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 = 𝐵 → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵)))
18		ltle 8413	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 < 𝐴 → 𝐵 ≤ 𝐴))
19	1, 2, 18	syl2anr 290	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 < 𝐴 → 𝐵 ≤ 𝐴))
20	19, 16	syl6 33	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 < 𝐴 → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵)))
21	9, 17, 20	3jaod 1345	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴) → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵)))
22	7, 21	mpd 13	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵))
23	6, 22	impbid 129	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Colors of variables: wff set class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ w3o 1008 = wceq 1402 ∈ wcel 2209 class class class wbr 4130 ℝcr 8178 < clt 8360 ≤ cle 8361 ℤcz 9644

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-sep 4249 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-addcom 8279 ax-addass 8281 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-0id 8287 ax-rnegex 8288 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-ltadd 8295

This proof depends on definitions: df-bi 117 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rab 2537 df-v 2823 df-sbc 3052 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-br 4131 df-opab 4193 df-id 4438 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-iota 5337 df-fun 5379 df-fv 5385 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-inn 9305 df-n0 9564 df-z 9645

This theorem is used by: znnnlt1 9692 nnnle0 9693 nn0n0n1ge2b 9725 eluzdc 10010 fzdcel 10444 fzn 10446 fzpreddisj 10478 fzp1disj 10487 fzneuz 10508 fznuz 10509 uznfz 10510 fzp1nel 10511 difelfznle 10542 nelfzo 10559 fzodisj 10587 exfzdc 10659 modfzo0difsn 10832 fzfig 10867 iseqf1olemqk 10944 exp3val 10978 facdiv 11176 bcval5 11201 zfz1isolemiso 11291 ccatsymb 11370 swrdnd 11431 swrdsbslen 11438 swrdspsleq 11439 pfxccat3 11506 swrdccat 11507 pfxccat3a 11510 2zsupmax 11992 2zinfmin 12009 summodclem3 12147 fprodntrivap 12351 alzdvds 12621 fzm1ndvds 12623 fzo0dvdseq 12624 n2dvds1 12679 bitsfzolem 12721 bitsfzo 12722 dvdsbnd 12733 algcvgblem 12827 prmndvdsfaclt 12934 odzdvds 13024 pcprendvds 13069 pcdvdsb 13099 pc2dvds 13109 pcmpt 13122 pockthg 13136 prmunb 13141 1arith 13146 4sqlem11 13180 ballotfilem2 13228 ballotfilemfc0 13232 ballotfilemfcc 13233 ballotfilemodife 13240 ballotfilemrv2 13265 gzsumgsum 14155 perfectlem2 16114 lgsdilem2 16155 lgsquadlem2 16197 uzdcinzz 16826

W3C validator