zltnle - Intuitionistic Logic Explorer

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

Theorem zltnle 9420

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 9378	. . . . 5 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℝ)
2		zre 9378	. . . . 5 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
3		lenlt 8150	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
4	1, 2, 3	syl2anr 290	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
5	4	biimpd 144	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 ≤ 𝐴 → ¬ 𝐴 < 𝐵))
6	5	con2d 625	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 → ¬ 𝐵 ≤ 𝐴))
7		ztri3or 9417	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴))
8		ax-1 6	. . . . 5 ⊢ (𝐴 < 𝐵 → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵))
9	8	a1i 9	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵)))
10		eqcom 2207	. . . . . . . . 9 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
11		eqle 8166	. . . . . . . . 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 622	. . . . 5 ⊢ (𝐵 ≤ 𝐴 → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵))
17	15, 16	syl6 33	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 = 𝐵 → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵)))
18		ltle 8162	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 < 𝐴 → 𝐵 ≤ 𝐴))
19	1, 2, 18	syl2anr 290	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 < 𝐴 → 𝐵 ≤ 𝐴))
20	19, 16	syl6 33	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 < 𝐴 → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵)))
21	9, 17, 20	3jaod 1317	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴) → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵)))
22	7, 21	mpd 13	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (¬ 𝐵 ≤ 𝐴 → 𝐴 < 𝐵))
23	6, 22	impbid 129	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ w3o 980 = wceq 1373 ∈ wcel 2176 class class class wbr 4045 ℝcr 7926 < clt 8109 ≤ cle 8110 ℤcz 9374

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 615 ax-in2 616 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-sep 4163 ax-pow 4219 ax-pr 4254 ax-un 4481 ax-setind 4586 ax-cnex 8018 ax-resscn 8019 ax-1cn 8020 ax-1re 8021 ax-icn 8022 ax-addcl 8023 ax-addrcl 8024 ax-mulcl 8025 ax-addcom 8027 ax-addass 8029 ax-distr 8031 ax-i2m1 8032 ax-0lt1 8033 ax-0id 8035 ax-rnegex 8036 ax-cnre 8038 ax-pre-ltirr 8039 ax-pre-ltwlin 8040 ax-pre-lttrn 8041 ax-pre-ltadd 8043

This theorem depends on definitions: df-bi 117 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-nel 2472 df-ral 2489 df-rex 2490 df-reu 2491 df-rab 2493 df-v 2774 df-sbc 2999 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-br 4046 df-opab 4107 df-id 4341 df-xp 4682 df-rel 4683 df-cnv 4684 df-co 4685 df-dm 4686 df-iota 5233 df-fun 5274 df-fv 5280 df-riota 5901 df-ov 5949 df-oprab 5950 df-mpo 5951 df-pnf 8111 df-mnf 8112 df-xr 8113 df-ltxr 8114 df-le 8115 df-sub 8247 df-neg 8248 df-inn 9039 df-n0 9298 df-z 9375

This theorem is referenced by: znnnlt1 9422 nnnle0 9423 nn0n0n1ge2b 9454 eluzdc 9733 fzdcel 10164 fzn 10166 fzpreddisj 10195 fzp1disj 10204 fzneuz 10225 fznuz 10226 uznfz 10227 fzp1nel 10228 difelfznle 10259 nelfzo 10276 fzodisj 10304 exfzdc 10371 modfzo0difsn 10542 fzfig 10577 iseqf1olemqk 10654 exp3val 10688 facdiv 10885 bcval5 10910 zfz1isolemiso 10986 ccatsymb 11061 swrdnd 11115 swrdsbslen 11122 swrdspsleq 11123 2zsupmax 11570 2zinfmin 11587 summodclem3 11724 fprodntrivap 11928 alzdvds 12198 fzm1ndvds 12200 fzo0dvdseq 12201 n2dvds1 12256 bitsfzolem 12298 bitsfzo 12299 dvdsbnd 12310 algcvgblem 12404 prmndvdsfaclt 12511 odzdvds 12601 pcprendvds 12646 pcdvdsb 12676 pc2dvds 12686 pcmpt 12699 pockthg 12713 prmunb 12718 1arith 12723 4sqlem11 12757 perfectlem2 15505 lgsdilem2 15546 lgsquadlem2 15588 uzdcinzz 15771

W3C validator