Metamath Proof Explorer

Theorem rexzrexnn0

Description: Rewrite an existential quantification restricted to integers into an existential quantification restricted to naturals. (Contributed by Stefan O'Rear, 11-Oct-2014)

Ref Expression
Hypotheses rexzrexnn0.1 ⊢ x = y → φ ↔ ψ
rexzrexnn0.2 ⊢ x = − y → φ ↔ χ
Assertion rexzrexnn0 ⊢ ∃ x ∈ ℤ φ ↔ ∃ y ∈ ℕ 0 ψ ∨ χ

Proof

Step Hyp Ref Expression
1 rexzrexnn0.1 ⊢ x = y → φ ↔ ψ
2 rexzrexnn0.2 ⊢ x = − y → φ ↔ χ
3 elznn0 ⊢ x ∈ ℤ ↔ x ∈ ℝ ∧ x ∈ ℕ 0 ∨ − x ∈ ℕ 0
4 3 simprbi ⊢ x ∈ ℤ → x ∈ ℕ 0 ∨ − x ∈ ℕ 0
5 4 adantr ⊢ x ∈ ℤ ∧ φ → x ∈ ℕ 0 ∨ − x ∈ ℕ 0
6 simpr ⊢ x ∈ ℤ ∧ φ ∧ x ∈ ℕ 0 → x ∈ ℕ 0
7 simplr ⊢ x ∈ ℤ ∧ φ ∧ x ∈ ℕ 0 → φ
8 1 equcoms ⊢ y = x → φ ↔ ψ
9 8 bicomd ⊢ y = x → ψ ↔ φ
10 9 rspcev ⊢ x ∈ ℕ 0 ∧ φ → ∃ y ∈ ℕ 0 ψ
11 6 7 10 syl2anc ⊢ x ∈ ℤ ∧ φ ∧ x ∈ ℕ 0 → ∃ y ∈ ℕ 0 ψ
12 11 ex ⊢ x ∈ ℤ ∧ φ → x ∈ ℕ 0 → ∃ y ∈ ℕ 0 ψ
13 simpr ⊢ x ∈ ℤ ∧ − x ∈ ℕ 0 → − x ∈ ℕ 0
14 zcn ⊢ x ∈ ℤ → x ∈ ℂ
15 14 negnegd ⊢ x ∈ ℤ → − − x = x
16 15 eqcomd ⊢ x ∈ ℤ → x = − − x
17 negeq ⊢ y = − x → − y = − − x
18 17 eqeq2d ⊢ y = − x → x = − y ↔ x = − − x
19 16 18 syl5ibrcom ⊢ x ∈ ℤ → y = − x → x = − y
20 19 imp ⊢ x ∈ ℤ ∧ y = − x → x = − y
21 20 2 syl ⊢ x ∈ ℤ ∧ y = − x → φ ↔ χ
22 21 bicomd ⊢ x ∈ ℤ ∧ y = − x → χ ↔ φ
23 22 adantlr ⊢ x ∈ ℤ ∧ − x ∈ ℕ 0 ∧ y = − x → χ ↔ φ
24 13 23 rspcedv ⊢ x ∈ ℤ ∧ − x ∈ ℕ 0 → φ → ∃ y ∈ ℕ 0 χ
25 24 impancom ⊢ x ∈ ℤ ∧ φ → − x ∈ ℕ 0 → ∃ y ∈ ℕ 0 χ
26 12 25 orim12d ⊢ x ∈ ℤ ∧ φ → x ∈ ℕ 0 ∨ − x ∈ ℕ 0 → ∃ y ∈ ℕ 0 ψ ∨ ∃ y ∈ ℕ 0 χ
27 5 26 mpd ⊢ x ∈ ℤ ∧ φ → ∃ y ∈ ℕ 0 ψ ∨ ∃ y ∈ ℕ 0 χ
28 r19.43 ⊢ ∃ y ∈ ℕ 0 ψ ∨ χ ↔ ∃ y ∈ ℕ 0 ψ ∨ ∃ y ∈ ℕ 0 χ
29 27 28 sylibr ⊢ x ∈ ℤ ∧ φ → ∃ y ∈ ℕ 0 ψ ∨ χ
30 29 rexlimiva ⊢ ∃ x ∈ ℤ φ → ∃ y ∈ ℕ 0 ψ ∨ χ
31 nn0z ⊢ y ∈ ℕ 0 → y ∈ ℤ
32 1 rspcev ⊢ y ∈ ℤ ∧ ψ → ∃ x ∈ ℤ φ
33 31 32 sylan ⊢ y ∈ ℕ 0 ∧ ψ → ∃ x ∈ ℤ φ
34 nn0negz ⊢ y ∈ ℕ 0 → − y ∈ ℤ
35 2 rspcev ⊢ − y ∈ ℤ ∧ χ → ∃ x ∈ ℤ φ
36 34 35 sylan ⊢ y ∈ ℕ 0 ∧ χ → ∃ x ∈ ℤ φ
37 33 36 jaodan ⊢ y ∈ ℕ 0 ∧ ψ ∨ χ → ∃ x ∈ ℤ φ
38 37 rexlimiva ⊢ ∃ y ∈ ℕ 0 ψ ∨ χ → ∃ x ∈ ℤ φ
39 30 38 impbii ⊢ ∃ x ∈ ℤ φ ↔ ∃ y ∈ ℕ 0 ψ ∨ χ