zdcle - Intuitionistic Logic Explorer

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

Theorem zdcle 9421

Description: Integer ≤ is decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)

**Assertion**
Ref	Expression
zdcle	⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID 𝐴 ≤ 𝐵)

**Proof of Theorem zdcle**
Step	Hyp	Ref	Expression
1		ztri3or 9388	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴))
2		zre 9349	. . 3 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
3		zre 9349	. . 3 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℝ)
4		ltle 8133	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
5		orc 713	. . . . . 6 ⊢ (𝐴 ≤ 𝐵 → (𝐴 ≤ 𝐵 ∨ ¬ 𝐴 ≤ 𝐵))
6		df-dc 836	. . . . . 6 ⊢ (DECID 𝐴 ≤ 𝐵 ↔ (𝐴 ≤ 𝐵 ∨ ¬ 𝐴 ≤ 𝐵))
7	5, 6	sylibr 134	. . . . 5 ⊢ (𝐴 ≤ 𝐵 → DECID 𝐴 ≤ 𝐵)
8	4, 7	syl6 33	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → DECID 𝐴 ≤ 𝐵))
9		eqle 8137	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵)
10	9, 7	syl 14	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → DECID 𝐴 ≤ 𝐵)
11	10	ex 115	. . . . 5 ⊢ (𝐴 ∈ ℝ → (𝐴 = 𝐵 → DECID 𝐴 ≤ 𝐵))
12	11	adantr 276	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 → DECID 𝐴 ≤ 𝐵))
13		lenlt 8121	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
14	13	biimpd 144	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 → ¬ 𝐵 < 𝐴))
15	14	con2d 625	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 < 𝐴 → ¬ 𝐴 ≤ 𝐵))
16		olc 712	. . . . . 6 ⊢ (¬ 𝐴 ≤ 𝐵 → (𝐴 ≤ 𝐵 ∨ ¬ 𝐴 ≤ 𝐵))
17	16, 6	sylibr 134	. . . . 5 ⊢ (¬ 𝐴 ≤ 𝐵 → DECID 𝐴 ≤ 𝐵)
18	15, 17	syl6 33	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 < 𝐴 → DECID 𝐴 ≤ 𝐵))
19	8, 12, 18	3jaod 1315	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴) → DECID 𝐴 ≤ 𝐵))
20	2, 3, 19	syl2an 289	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴) → DECID 𝐴 ≤ 𝐵))
21	1, 20	mpd 13	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID 𝐴 ≤ 𝐵)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ∨ wo 709 DECID wdc 835 ∨ w3o 979 = wceq 1364 ∈ wcel 2167 class class class wbr 4034 ℝcr 7897 < clt 8080 ≤ cle 8081 ℤcz 9345

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 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4152 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-cnex 7989 ax-resscn 7990 ax-1cn 7991 ax-1re 7992 ax-icn 7993 ax-addcl 7994 ax-addrcl 7995 ax-mulcl 7996 ax-addcom 7998 ax-addass 8000 ax-distr 8002 ax-i2m1 8003 ax-0lt1 8004 ax-0id 8006 ax-rnegex 8007 ax-cnre 8009 ax-pre-ltirr 8010 ax-pre-ltwlin 8011 ax-pre-lttrn 8012 ax-pre-ltadd 8014

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rab 2484 df-v 2765 df-sbc 2990 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-br 4035 df-opab 4096 df-id 4329 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-iota 5220 df-fun 5261 df-fv 5267 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-pnf 8082 df-mnf 8083 df-xr 8084 df-ltxr 8085 df-le 8086 df-sub 8218 df-neg 8219 df-inn 9010 df-n0 9269 df-z 9346

This theorem is referenced by: uzin 9653 xnn0dcle 9896 nelfzo 10246 exfzdc 10335 infssuzex 10342 modfzo0difsn 10506 fzfig 10541 iseqf1olemjpcl 10619 iseqf1olemqpcl 10620 seq3f1oleml 10627 seq3f1o 10628 fser0const 10646 uzin2 11171 2zsupmax 11410 2zinfmin 11427 sumeq2 11543 summodclem2a 11565 fsum3 11571 fsumcl2lem 11582 fsumadd 11590 sumsnf 11593 fsummulc2 11632 explecnv 11689 prodeq2 11741 prodmodclem3 11759 prodmodclem2a 11760 fprodseq 11767 prod1dc 11770 fprodmul 11775 prodsnf 11776 pcdvdsb 12516 pcmpt2 12540 pcmptdvds 12541 pcprod 12542 pcfac 12546 1arithlem4 12562 plyaddlem1 15091 plyaddlem 15093

W3C validator