Theorem zdceq 9395

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

Assertion

Ref	Expression
zdceq	|- ( ( A e. ZZ /\ B e. ZZ ) -> DECID A = B )

Proof of Theorem zdceq

Step	Hyp	Ref	Expression
1		ztri3or 9363	. 2 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B \/ A = B \/ B < A ) )
2		zre 9324	. . . 4 |- ( A e. ZZ -> A e. RR )
3		ltne 8106	. . . . . . . 8 |- ( ( A e. RR /\ A < B ) -> B =/= A )
4	3	necomd 2450	. . . . . . 7 |- ( ( A e. RR /\ A < B ) -> A =/= B )
5		olc 712	. . . . . . . 8 |- ( A =/= B -> ( A = B \/ A =/= B ) )
6		dcne 2375	. . . . . . . 8 |- (DECID A = B <-> ( A = B \/ A =/= B ) )
7	5, 6	sylibr 134	. . . . . . 7 |- ( A =/= B -> DECID A = B )
8	4, 7	syl 14	. . . . . 6 |- ( ( A e. RR /\ A < B ) -> DECID A = B )
9	8	ex 115	. . . . 5 |- ( A e. RR -> ( A < B -> DECID A = B ) )
10	9	adantr 276	. . . 4 |- ( ( A e. RR /\ B e. ZZ ) -> ( A < B -> DECID A = B ) )
11	2, 10	sylan 283	. . 3 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B -> DECID A = B ) )
12		orc 713	. . . . 5 |- ( A = B -> ( A = B \/ A =/= B ) )
13	12, 6	sylibr 134	. . . 4 |- ( A = B -> DECID A = B )
14	13	a1i 9	. . 3 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( A = B -> DECID A = B ) )
15		zre 9324	. . . . 5 |- ( B e. ZZ -> B e. RR )
16		ltne 8106	. . . . . . 7 |- ( ( B e. RR /\ B < A ) -> A =/= B )
17	16, 7	syl 14	. . . . . 6 |- ( ( B e. RR /\ B < A ) -> DECID A = B )
18	17	ex 115	. . . . 5 |- ( B e. RR -> ( B < A -> DECID A = B ) )
19	15, 18	syl 14	. . . 4 |- ( B e. ZZ -> ( B < A -> DECID A = B ) )
20	19	adantl 277	. . 3 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( B < A -> DECID A = B ) )
21	11, 14, 20	3jaod 1315	. 2 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A < B \/ A = B \/ B < A ) -> DECID A = B ) )
22	1, 21	mpd 13	1 |- ( ( A e. ZZ /\ B e. ZZ ) -> DECID A = B )

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 709  DECID wdc 835   \/ w3o 979   = wceq 1364   e. wcel 2164   =/= wne 2364   class class class wbr 4030   RRcr 7873   < clt 8056   ZZcz 9320

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570  ax-cnex 7965  ax-resscn 7966  ax-1cn 7967  ax-1re 7968  ax-icn 7969  ax-addcl 7970  ax-addrcl 7971  ax-mulcl 7972  ax-addcom 7974  ax-addass 7976  ax-distr 7978  ax-i2m1 7979  ax-0lt1 7980  ax-0id 7982  ax-rnegex 7983  ax-cnre 7985  ax-pre-ltirr 7986  ax-pre-ltwlin 7987  ax-pre-lttrn 7988  ax-pre-ltadd 7990

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 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2987  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-int 3872  df-br 4031  df-opab 4092  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-iota 5216  df-fun 5257  df-fv 5263  df-riota 5874  df-ov 5922  df-oprab 5923  df-mpo 5924  df-pnf 8058  df-mnf 8059  df-xr 8060  df-ltxr 8061  df-le 8062  df-sub 8194  df-neg 8195  df-inn 8985  df-n0 9244  df-z 9321

This theorem is referenced by:  nn0n0n1ge2b  9399  nn0lt2  9401  prime  9419  elnn1uz2  9675  iseqf1olemqcl  10573  iseqf1olemnab  10575  iseqf1olemab  10576  seq3f1olemstep  10588  exp3val  10615  hashfzp1  10898  fprod1p  11745  dvdsdc  11944  zdvdsdc  11958  dvdsabseq  11992  alzdvds  11999  fzo0dvdseq  12002  gcdmndc  12084  gcdsupex  12097  gcdsupcl  12098  gcd0id  12119  gcdaddm  12124  dfgcd2  12154  gcdmultiplez  12161  dvdssq  12171  nn0seqcvgd  12182  algcvgblem  12190  eucalgval2  12194  lcmmndc  12203  lcmdvds  12220  lcmid  12221  mulgcddvds  12235  cncongr2  12245  isprm3  12259  isprm4  12260  prm2orodd  12267  rpexp  12294  phivalfi  12353  phiprmpw  12363  phimullem  12366  eulerthlemfi  12369  hashgcdeq  12380  phisum  12381  pcxnn0cl  12451  pcge0  12454  pcdvdsb  12461  pcneg  12466  pcdvdstr  12468  pcgcd1  12469  pc2dvds  12471  pcz  12473  pcprmpw2  12474  pcmpt  12484  4sqlemafi  12536  4sqleminfi  12538  4sqexercise1  12539  4sqexercise2  12540  4sqlemsdc  12541  4sqlem11  12542  4sqlem19  12550  ennnfonelemim  12584  unbendc  12614  strsetsid  12654  mulgval  13195  mulgfng  13197  subgmulg  13261  znf1o  14150  ply1term  14922  dvply1  14943  lgsval  15161  lgsfvalg  15162  lgsfcl2  15163  lgscllem  15164  lgsval2lem  15167  lgsneg1  15182  lgsdir2  15190  lgsdirprm  15191  lgsdir  15192  lgsne0  15195  lgsprme0  15199  lgsdirnn0  15204  lgsdinn0  15205  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad3  15241  2lgs  15261  2lgsoddprm  15270  2sqlem9  15281  nninffeq  15580  nconstwlpolem  15625