![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > zapne | GIF version |
Description: Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.) |
Ref | Expression |
---|---|
zapne | ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 # 𝑁 ↔ 𝑀 ≠ 𝑁)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zcn 8523 | . . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ) | |
2 | zcn 8523 | . . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) | |
3 | apne 7876 | . . 3 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 # 𝑁 → 𝑀 ≠ 𝑁)) | |
4 | 1, 2, 3 | syl2an 283 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 # 𝑁 → 𝑀 ≠ 𝑁)) |
5 | df-ne 2250 | . . 3 ⊢ (𝑀 ≠ 𝑁 ↔ ¬ 𝑀 = 𝑁) | |
6 | ztri3or 8561 | . . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) | |
7 | 3orrot 926 | . . . . . . 7 ⊢ ((𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀) ↔ (𝑀 = 𝑁 ∨ 𝑁 < 𝑀 ∨ 𝑀 < 𝑁)) | |
8 | 3orass 923 | . . . . . . 7 ⊢ ((𝑀 = 𝑁 ∨ 𝑁 < 𝑀 ∨ 𝑀 < 𝑁) ↔ (𝑀 = 𝑁 ∨ (𝑁 < 𝑀 ∨ 𝑀 < 𝑁))) | |
9 | 7, 8 | bitri 182 | . . . . . 6 ⊢ ((𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀) ↔ (𝑀 = 𝑁 ∨ (𝑁 < 𝑀 ∨ 𝑀 < 𝑁))) |
10 | 6, 9 | sylib 120 | . . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 𝑁 ∨ (𝑁 < 𝑀 ∨ 𝑀 < 𝑁))) |
11 | 10 | ord 676 | . . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑀 = 𝑁 → (𝑁 < 𝑀 ∨ 𝑀 < 𝑁))) |
12 | zre 8522 | . . . . 5 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ) | |
13 | zre 8522 | . . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) | |
14 | reaplt 7841 | . . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 # 𝑁 ↔ (𝑀 < 𝑁 ∨ 𝑁 < 𝑀))) | |
15 | orcom 680 | . . . . . 6 ⊢ ((𝑀 < 𝑁 ∨ 𝑁 < 𝑀) ↔ (𝑁 < 𝑀 ∨ 𝑀 < 𝑁)) | |
16 | 14, 15 | syl6bb 194 | . . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 # 𝑁 ↔ (𝑁 < 𝑀 ∨ 𝑀 < 𝑁))) |
17 | 12, 13, 16 | syl2an 283 | . . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 # 𝑁 ↔ (𝑁 < 𝑀 ∨ 𝑀 < 𝑁))) |
18 | 11, 17 | sylibrd 167 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑀 = 𝑁 → 𝑀 # 𝑁)) |
19 | 5, 18 | syl5bi 150 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≠ 𝑁 → 𝑀 # 𝑁)) |
20 | 4, 19 | impbid 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 |