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

Theorem zapne 8589
Description: Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.)
Assertion
Ref Expression
zapne ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 # 𝑁𝑀𝑁))

Proof of Theorem zapne
StepHypRef Expression
1 zcn 8523 . . 3 (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
2 zcn 8523 . . 3 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
3 apne 7876 . . 3 ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 # 𝑁𝑀𝑁))
41, 2, 3syl2an 283 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 # 𝑁𝑀𝑁))
5 df-ne 2250 . . 3 (𝑀𝑁 ↔ ¬ 𝑀 = 𝑁)
6 ztri3or 8561 . . . . . 6 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁𝑀 = 𝑁𝑁 < 𝑀))
7 3orrot 926 . . . . . . 7 ((𝑀 < 𝑁𝑀 = 𝑁𝑁 < 𝑀) ↔ (𝑀 = 𝑁𝑁 < 𝑀𝑀 < 𝑁))
8 3orass 923 . . . . . . 7 ((𝑀 = 𝑁𝑁 < 𝑀𝑀 < 𝑁) ↔ (𝑀 = 𝑁 ∨ (𝑁 < 𝑀𝑀 < 𝑁)))
97, 8bitri 182 . . . . . 6 ((𝑀 < 𝑁𝑀 = 𝑁𝑁 < 𝑀) ↔ (𝑀 = 𝑁 ∨ (𝑁 < 𝑀𝑀 < 𝑁)))
106, 9sylib 120 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 𝑁 ∨ (𝑁 < 𝑀𝑀 < 𝑁)))
1110ord 676 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑀 = 𝑁 → (𝑁 < 𝑀𝑀 < 𝑁)))
12 zre 8522 . . . . 5 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
13 zre 8522 . . . . 5 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
14 reaplt 7841 . . . . . 6 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 # 𝑁 ↔ (𝑀 < 𝑁𝑁 < 𝑀)))
15 orcom 680 . . . . . 6 ((𝑀 < 𝑁𝑁 < 𝑀) ↔ (𝑁 < 𝑀𝑀 < 𝑁))
1614, 15syl6bb 194 . . . . 5 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 # 𝑁 ↔ (𝑁 < 𝑀𝑀 < 𝑁)))
1712, 13, 16syl2an 283 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 # 𝑁 ↔ (𝑁 < 𝑀𝑀 < 𝑁)))
1811, 17sylibrd 167 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑀 = 𝑁𝑀 # 𝑁))
195, 18syl5bi 150 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀𝑁𝑀 # 𝑁))
204, 19impbid 127 1 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 # 𝑁𝑀𝑁))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 662  w3o 919   = wceq 1285  wcel 1434  wne 2249   class class class wbr 3806  cc 7127  cr 7128   < clt 7301   # cap 7834  cz 8518
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3917  ax-pow 3969  ax-pr 3994  ax-un 4218  ax-setind 4310  ax-cnex 7215  ax-resscn 7216  ax-1cn 7217  ax-1re 7218  ax-icn 7219  ax-addcl 7220  ax-addrcl 7221  ax-mulcl 7222  ax-mulrcl 7223  ax-addcom 7224  ax-mulcom 7225  ax-addass 7226  ax-mulass 7227  ax-distr 7228  ax-i2m1 7229  ax-0lt1 7230  ax-1rid 7231  ax-0id 7232  ax-rnegex 7233  ax-precex 7234  ax-cnre 7235  ax-pre-ltirr 7236  ax-pre-ltwlin 7237  ax-pre-lttrn 7238  ax-pre-apti 7239  ax-pre-ltadd 7240  ax-pre-mulgt0 7241
This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-nel 2345  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2613  df-sbc 2826  df-dif 2985  df-un 2987  df-in 2989  df-ss 2996  df-pw 3403  df-sn 3423  df-pr 3424  df-op 3426  df-uni 3623  df-int 3658  df-br 3807  df-opab 3861  df-id 4078  df-xp 4400  df-rel 4401  df-cnv 4402  df-co 4403  df-dm 4404  df-iota 4920  df-fun 4957  df-fv 4963  df-riota 5525  df-ov 5572  df-oprab 5573  df-mpt2 5574  df-pnf 7303  df-mnf 7304  df-xr 7305  df-ltxr 7306  df-le 7307  df-sub 7434  df-neg 7435  df-reap 7828  df-ap 7835  df-inn 8193  df-n0 8442  df-z 8519
This theorem is referenced by:  zltlen  8593  msqznn  8614  qapne  8891  qreccl  8894  nn0opthd  9832  fihashneq0  9905  nnabscl  10221  dvdsval2  10440  dvdscmulr  10466  dvdsmulcr  10467  divconjdvds  10491  gcdn0gt0  10610  lcmcllem  10690  lcmid  10703  3lcm2e6woprm  10709  6lcm4e12  10710  mulgcddvds  10717  divgcdcoprmex  10725  cncongr1  10726  cncongr2  10727  isprm3  10741
  Copyright terms: Public domain W3C validator