Theorem zdceq 9653

Description: Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.)

Assertion

Ref	Expression
zdceq	⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID 𝐴 = 𝐵)

Proof of Theorem zdceq

Step	Hyp	Ref	Expression
1		ztri3or 9620	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴))
2		zre 9581	. . . 4 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
3		ltne 8358	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴)
4	3	necomd 2498	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ≠ 𝐵)
5		olc 719	. . . . . . . 8 ⊢ (𝐴 ≠ 𝐵 → (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))
6		dcne 2423	. . . . . . . 8 ⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))
7	5, 6	sylibr 134	. . . . . . 7 ⊢ (𝐴 ≠ 𝐵 → DECID 𝐴 = 𝐵)
8	4, 7	syl 14	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → DECID 𝐴 = 𝐵)
9	8	ex 115	. . . . 5 ⊢ (𝐴 ∈ ℝ → (𝐴 < 𝐵 → DECID 𝐴 = 𝐵))
10	9	adantr 276	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 → DECID 𝐴 = 𝐵))
11	2, 10	sylan 283	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 → DECID 𝐴 = 𝐵))
12		orc 720	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))
13	12, 6	sylibr 134	. . . 4 ⊢ (𝐴 = 𝐵 → DECID 𝐴 = 𝐵)
14	13	a1i 9	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 = 𝐵 → DECID 𝐴 = 𝐵))
15		zre 9581	. . . . 5 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℝ)
16		ltne 8358	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 < 𝐴) → 𝐴 ≠ 𝐵)
17	16, 7	syl 14	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 < 𝐴) → DECID 𝐴 = 𝐵)
18	17	ex 115	. . . . 5 ⊢ (𝐵 ∈ ℝ → (𝐵 < 𝐴 → DECID 𝐴 = 𝐵))
19	15, 18	syl 14	. . . 4 ⊢ (𝐵 ∈ ℤ → (𝐵 < 𝐴 → DECID 𝐴 = 𝐵))
20	19	adantl 277	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 < 𝐴 → DECID 𝐴 = 𝐵))
21	11, 14, 20	3jaod 1341	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴) → DECID 𝐴 = 𝐵))
22	1, 21	mpd 13	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 716  DECID wdc 842   ∨ w3o 1004   = wceq 1398   ∈ wcel 2203   ≠ wne 2412   class class class wbr 4109  ℝcr 8126   < clt 8308  ℤcz 9577

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659  ax-cnex 8218  ax-resscn 8219  ax-1cn 8220  ax-1re 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-addcom 8227  ax-addass 8229  ax-distr 8231  ax-i2m1 8232  ax-0lt1 8233  ax-0id 8235  ax-rnegex 8236  ax-cnre 8238  ax-pre-ltirr 8239  ax-pre-ltwlin 8240  ax-pre-lttrn 8241  ax-pre-ltadd 8243

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2815  df-sbc 3043  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-int 3950  df-br 4110  df-opab 4172  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-iota 5312  df-fun 5354  df-fv 5360  df-riota 6003  df-ov 6053  df-oprab 6054  df-mpo 6055  df-pnf 8310  df-mnf 8311  df-xr 8312  df-ltxr 8313  df-le 8314  df-sub 8446  df-neg 8447  df-inn 9238  df-n0 9497  df-z 9578

This theorem is referenced by:  nn0n0n1ge2b  9657  nn0lt2  9659  prime  9677  elnn1uz2  9939  iseqf1olemqcl  10861  iseqf1olemnab  10863  iseqf1olemab  10864  seq3f1olemstep  10876  exp3val  10903  hashfzp1  11189  hashfibclem  11206  ccat1st1st  11329  swrdccatin1  11417  fprod1p  12285  dvdsdc  12484  zdvdsdc  12498  fsumdvds  12528  dvdsabseq  12533  alzdvds  12540  fzo0dvdseq  12543  gcdmndc  12651  gcdsupex  12653  gcdsupcl  12654  gcd0id  12675  gcdaddm  12680  dfgcd2  12710  gcdmultiplez  12717  dvdssq  12727  nn0seqcvgd  12738  algcvgblem  12746  eucalgval2  12750  lcmmndc  12759  lcmdvds  12776  lcmid  12777  mulgcddvds  12791  cncongr2  12801  isprm3  12815  isprm4  12816  prm2orodd  12823  rpexp  12850  phivalfi  12909  phiprmpw  12919  phimullem  12922  eulerthlemfi  12925  hashgcdeq  12937  phisum  12938  pcxnn0cl  13008  pcge0  13011  pcdvdsb  13018  pcneg  13023  pcdvdstr  13025  pcgcd1  13026  pc2dvds  13028  pcz  13030  pcprmpw2  13031  pcmpt  13041  4sqlemafi  13093  4sqleminfi  13095  4sqexercise1  13096  4sqexercise2  13097  4sqlemsdc  13098  4sqlem11  13099  4sqlem19  13107  ballotfilemofi  13138  ennnfonelemim  13175  unbendc  13205  strsetsid  13245  bassetsnn  13269  mulgval  13839  mulgfng  13841  subgmulg  13905  znf1o  14799  psr1clfi  14843  ply1term  15608  dvply1  15630  perfectlem2  15868  lgsval  15877  lgsfvalg  15878  lgsfcl2  15879  lgscllem  15880  lgsval2lem  15883  lgsneg1  15898  lgsdir2  15906  lgsdirprm  15907  lgsdir  15908  lgsne0  15911  lgsprme0  15915  lgsdirnn0  15920  lgsdinn0  15921  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad3  15957  2lgs  15977  2lgsoddprm  15986  2sqlem9  15997  umgrclwwlkge2  16397  nninffeq  16798  nconstwlpolem  16851