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 \to (φ \leftrightarrow ψ)$
	rexzrexnn0.2	$⊢ x = - y \to (φ \leftrightarrow χ)$
Assertion	rexzrexnn0	$⊢ \exists x \in ℤ φ \leftrightarrow \exists y \in ℕ_{0} (ψ \lor χ)$

Proof

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

Metamath Proof Explorer

Theorem rexzrexnn0

Proof