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	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	rexzrexnn0.2	⊢ ( 𝑥 = - 𝑦 → ( 𝜑 ↔ 𝜒 ) )
Assertion	rexzrexnn0	⊢ ( ∃ 𝑥 ∈ ℤ 𝜑 ↔ ∃ 𝑦 ∈ ℕ0 ( 𝜓 ∨ 𝜒 ) )

Proof

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