Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elz2 Structured version   Visualization version   GIF version

Theorem elz2 11991
 Description: Membership in the set of integers. Commonly used in constructions of the integers as equivalence classes under subtraction of the positive integers. (Contributed by Mario Carneiro, 16-May-2014.)
Assertion
Ref Expression
elz2 (𝑁 ∈ ℤ ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑁 = (𝑥𝑦))
Distinct variable group:   𝑥,𝑦,𝑁

Proof of Theorem elz2
StepHypRef Expression
1 elznn0 11988 . 2 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
2 nn0p1nn 11928 . . . . . 6 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)
32adantl 485 . . . . 5 ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈ ℕ)
4 1nn 11640 . . . . . 6 1 ∈ ℕ
54a1i 11 . . . . 5 ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → 1 ∈ ℕ)
6 recn 10620 . . . . . . . 8 (𝑁 ∈ ℝ → 𝑁 ∈ ℂ)
76adantr 484 . . . . . . 7 ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℂ)
8 ax-1cn 10588 . . . . . . 7 1 ∈ ℂ
9 pncan 10885 . . . . . . 7 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
107, 8, 9sylancl 589 . . . . . 6 ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 1) − 1) = 𝑁)
1110eqcomd 2807 . . . . 5 ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → 𝑁 = ((𝑁 + 1) − 1))
12 rspceov 7186 . . . . 5 (((𝑁 + 1) ∈ ℕ ∧ 1 ∈ ℕ ∧ 𝑁 = ((𝑁 + 1) − 1)) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑁 = (𝑥𝑦))
133, 5, 11, 12syl3anc 1368 . . . 4 ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑁 = (𝑥𝑦))
144a1i 11 . . . . 5 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0) → 1 ∈ ℕ)
156adantr 484 . . . . . . 7 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0) → 𝑁 ∈ ℂ)
16 negsub 10927 . . . . . . 7 ((1 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (1 + -𝑁) = (1 − 𝑁))
178, 15, 16sylancr 590 . . . . . 6 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0) → (1 + -𝑁) = (1 − 𝑁))
18 simpr 488 . . . . . . 7 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0) → -𝑁 ∈ ℕ0)
19 nnnn0addcl 11919 . . . . . . 7 ((1 ∈ ℕ ∧ -𝑁 ∈ ℕ0) → (1 + -𝑁) ∈ ℕ)
204, 18, 19sylancr 590 . . . . . 6 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0) → (1 + -𝑁) ∈ ℕ)
2117, 20eqeltrrd 2894 . . . . 5 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0) → (1 − 𝑁) ∈ ℕ)
22 nncan 10908 . . . . . . 7 ((1 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (1 − (1 − 𝑁)) = 𝑁)
238, 15, 22sylancr 590 . . . . . 6 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0) → (1 − (1 − 𝑁)) = 𝑁)
2423eqcomd 2807 . . . . 5 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0) → 𝑁 = (1 − (1 − 𝑁)))
25 rspceov 7186 . . . . 5 ((1 ∈ ℕ ∧ (1 − 𝑁) ∈ ℕ ∧ 𝑁 = (1 − (1 − 𝑁))) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑁 = (𝑥𝑦))
2614, 21, 24, 25syl3anc 1368 . . . 4 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑁 = (𝑥𝑦))
2713, 26jaodan 955 . . 3 ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑁 = (𝑥𝑦))
28 nnre 11636 . . . . . . 7 (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
29 nnre 11636 . . . . . . 7 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
30 resubcl 10943 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦) ∈ ℝ)
3128, 29, 30syl2an 598 . . . . . 6 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥𝑦) ∈ ℝ)
32 letric 10733 . . . . . . . 8 ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦𝑥𝑥𝑦))
3329, 28, 32syl2anr 599 . . . . . . 7 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑦𝑥𝑥𝑦))
34 nnnn0 11896 . . . . . . . . 9 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
35 nnnn0 11896 . . . . . . . . 9 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ0)
36 nn0sub 11939 . . . . . . . . 9 ((𝑦 ∈ ℕ0𝑥 ∈ ℕ0) → (𝑦𝑥 ↔ (𝑥𝑦) ∈ ℕ0))
3734, 35, 36syl2anr 599 . . . . . . . 8 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑦𝑥 ↔ (𝑥𝑦) ∈ ℕ0))
38 nn0sub 11939 . . . . . . . . . 10 ((𝑥 ∈ ℕ0𝑦 ∈ ℕ0) → (𝑥𝑦 ↔ (𝑦𝑥) ∈ ℕ0))
3935, 34, 38syl2an 598 . . . . . . . . 9 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥𝑦 ↔ (𝑦𝑥) ∈ ℕ0))
40 nncn 11637 . . . . . . . . . . 11 (𝑥 ∈ ℕ → 𝑥 ∈ ℂ)
41 nncn 11637 . . . . . . . . . . 11 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
42 negsubdi2 10938 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → -(𝑥𝑦) = (𝑦𝑥))
4340, 41, 42syl2an 598 . . . . . . . . . 10 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → -(𝑥𝑦) = (𝑦𝑥))
4443eleq1d 2877 . . . . . . . . 9 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (-(𝑥𝑦) ∈ ℕ0 ↔ (𝑦𝑥) ∈ ℕ0))
4539, 44bitr4d 285 . . . . . . . 8 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥𝑦 ↔ -(𝑥𝑦) ∈ ℕ0))
4637, 45orbi12d 916 . . . . . . 7 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑦𝑥𝑥𝑦) ↔ ((𝑥𝑦) ∈ ℕ0 ∨ -(𝑥𝑦) ∈ ℕ0)))
4733, 46mpbid 235 . . . . . 6 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑥𝑦) ∈ ℕ0 ∨ -(𝑥𝑦) ∈ ℕ0))
4831, 47jca 515 . . . . 5 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑥𝑦) ∈ ℝ ∧ ((𝑥𝑦) ∈ ℕ0 ∨ -(𝑥𝑦) ∈ ℕ0)))
49 eleq1 2880 . . . . . 6 (𝑁 = (𝑥𝑦) → (𝑁 ∈ ℝ ↔ (𝑥𝑦) ∈ ℝ))
50 eleq1 2880 . . . . . . 7 (𝑁 = (𝑥𝑦) → (𝑁 ∈ ℕ0 ↔ (𝑥𝑦) ∈ ℕ0))
51 negeq 10871 . . . . . . . 8 (𝑁 = (𝑥𝑦) → -𝑁 = -(𝑥𝑦))
5251eleq1d 2877 . . . . . . 7 (𝑁 = (𝑥𝑦) → (-𝑁 ∈ ℕ0 ↔ -(𝑥𝑦) ∈ ℕ0))
5350, 52orbi12d 916 . . . . . 6 (𝑁 = (𝑥𝑦) → ((𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0) ↔ ((𝑥𝑦) ∈ ℕ0 ∨ -(𝑥𝑦) ∈ ℕ0)))
5449, 53anbi12d 633 . . . . 5 (𝑁 = (𝑥𝑦) → ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)) ↔ ((𝑥𝑦) ∈ ℝ ∧ ((𝑥𝑦) ∈ ℕ0 ∨ -(𝑥𝑦) ∈ ℕ0))))
5548, 54syl5ibrcom 250 . . . 4 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑁 = (𝑥𝑦) → (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0))))
5655rexlimivv 3254 . . 3 (∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑁 = (𝑥𝑦) → (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
5727, 56impbii 212 . 2 ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)) ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑁 = (𝑥𝑦))
581, 57bitri 278 1 (𝑁 ∈ ℤ ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑁 = (𝑥𝑦))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2112  ∃wrex 3110   class class class wbr 5033  (class class class)co 7139  ℂcc 10528  ℝcr 10529  1c1 10531   + caddc 10533   ≤ cle 10669   − cmin 10863  -cneg 10864  ℕcn 11629  ℕ0cn0 11889  ℤcz 11973 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11630  df-n0 11890  df-z 11974 This theorem is referenced by:  dfz2  11992  zaddcl  12014
 Copyright terms: Public domain W3C validator