Theorem zdceq 9240

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 9211	. 2 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B \/ A = B \/ B < A ) )
2		zre 9172	. . . 4 |- ( A e. ZZ -> A e. RR )
3		ltne 7963	. . . . . . . 8 |- ( ( A e. RR /\ A < B ) -> B =/= A )
4	3	necomd 2413	. . . . . . 7 |- ( ( A e. RR /\ A < B ) -> A =/= B )
5		olc 701	. . . . . . . 8 |- ( A =/= B -> ( A = B \/ A =/= B ) )
6		dcne 2338	. . . . . . . 8 |- (DECID A = B <-> ( A = B \/ A =/= B ) )
7	5, 6	sylibr 133	. . . . . . 7 |- ( A =/= B -> DECID A = B )
8	4, 7	syl 14	. . . . . 6 |- ( ( A e. RR /\ A < B ) -> DECID A = B )
9	8	ex 114	. . . . 5 |- ( A e. RR -> ( A < B -> DECID A = B ) )
10	9	adantr 274	. . . 4 |- ( ( A e. RR /\ B e. ZZ ) -> ( A < B -> DECID A = B ) )
11	2, 10	sylan 281	. . 3 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B -> DECID A = B ) )
12		orc 702	. . . . 5 |- ( A = B -> ( A = B \/ A =/= B ) )
13	12, 6	sylibr 133	. . . 4 |- ( A = B -> DECID A = B )
14	13	a1i 9	. . 3 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( A = B -> DECID A = B ) )
15		zre 9172	. . . . 5 |- ( B e. ZZ -> B e. RR )
16		ltne 7963	. . . . . . 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 114	. . . . 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 275	. . 3 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( B < A -> DECID A = B ) )
21	11, 14, 20	3jaod 1286	. 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 103   \/ wo 698  DECID wdc 820   \/ w3o 962   = wceq 1335   e. wcel 2128   =/= wne 2327   class class class wbr 3966   RRcr 7732   < clt 7913   ZZcz 9168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4083  ax-pow 4136  ax-pr 4170  ax-un 4394  ax-setind 4497  ax-cnex 7824  ax-resscn 7825  ax-1cn 7826  ax-1re 7827  ax-icn 7828  ax-addcl 7829  ax-addrcl 7830  ax-mulcl 7831  ax-addcom 7833  ax-addass 7835  ax-distr 7837  ax-i2m1 7838  ax-0lt1 7839  ax-0id 7841  ax-rnegex 7842  ax-cnre 7844  ax-pre-ltirr 7845  ax-pre-ltwlin 7846  ax-pre-lttrn 7847  ax-pre-ltadd 7849

This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3774  df-int 3809  df-br 3967  df-opab 4027  df-id 4254  df-xp 4593  df-rel 4594  df-cnv 4595  df-co 4596  df-dm 4597  df-iota 5136  df-fun 5173  df-fv 5179  df-riota 5781  df-ov 5828  df-oprab 5829  df-mpo 5830  df-pnf 7915  df-mnf 7916  df-xr 7917  df-ltxr 7918  df-le 7919  df-sub 8049  df-neg 8050  df-inn 8835  df-n0 9092  df-z 9169

This theorem is referenced by:  nn0n0n1ge2b  9244  nn0lt2  9246  prime  9264  elnn1uz2  9519  iseqf1olemqcl  10389  iseqf1olemnab  10391  iseqf1olemab  10392  seq3f1olemstep  10404  exp3val  10425  hashfzp1  10702  fprod1p  11500  dvdsdc  11698  zdvdsdc  11712  dvdsabseq  11743  alzdvds  11750  fzo0dvdseq  11753  gcdmndc  11835  gcdsupex  11845  gcdsupcl  11846  gcd0id  11867  gcdaddm  11872  dfgcd2  11902  gcdmultiplez  11909  dvdssq  11919  nn0seqcvgd  11922  algcvgblem  11930  eucalgval2  11934  lcmmndc  11943  lcmdvds  11960  lcmid  11961  mulgcddvds  11975  cncongr2  11985  isprm3  11999  isprm4  12000  prm2orodd  12007  rpexp  12032  phivalfi  12091  phiprmpw  12101  phimullem  12104  eulerthlemfi  12107  hashgcdeq  12118  phisum  12119  ennnfonelemim  12195  unbendc  12227  strsetsid  12265  nninffeq  13634  nconstwlpolem  13677