zindd

Description: Principle of Mathematical Induction on all integers, deduction version. The first five hypotheses give the substitutions; the last three are the basis, the induction, and the extension to negative numbers. (Contributed by Paul Chapman, 17-Apr-2009) (Proof shortened by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	zindd.1	$⊢ x = 0 \to (φ \leftrightarrow ψ)$
	zindd.2	$⊢ x = y \to (φ \leftrightarrow χ)$
	zindd.3	$⊢ x = y + 1 \to (φ \leftrightarrow τ)$
	zindd.4	$⊢ x = - y \to (φ \leftrightarrow θ)$
	zindd.5	$⊢ x = A \to (φ \leftrightarrow η)$
	zindd.6	$⊢ ζ \to ψ$
	zindd.7	$⊢ ζ \to (y \in ℕ_{0} \to (χ \to τ))$
	zindd.8	$⊢ ζ \to (y \in ℕ \to (χ \to θ))$
Assertion	zindd	$⊢ ζ \to (A \in ℤ \to η)$

Proof

Step	Hyp	Ref	Expression
1		zindd.1	$⊢ x = 0 \to (φ \leftrightarrow ψ)$
2		zindd.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		zindd.3	$⊢ x = y + 1 \to (φ \leftrightarrow τ)$
4		zindd.4	$⊢ x = - y \to (φ \leftrightarrow θ)$
5		zindd.5	$⊢ x = A \to (φ \leftrightarrow η)$
6		zindd.6	$⊢ ζ \to ψ$
7		zindd.7	$⊢ ζ \to (y \in ℕ_{0} \to (χ \to τ))$
8		zindd.8	$⊢ ζ \to (y \in ℕ \to (χ \to θ))$
9		znegcl	$⊢ y \in ℤ \to - y \in ℤ$
10		elznn0nn	$⊢ - y \in ℤ \leftrightarrow (- y \in ℕ_{0} \lor (- y \in ℝ \land - (- y) \in ℕ))$
11	9 10	sylib	$⊢ y \in ℤ \to (- y \in ℕ_{0} \lor (- y \in ℝ \land - (- y) \in ℕ))$
12		simpr	$⊢ (- y \in ℝ \land - (- y) \in ℕ) \to - (- y) \in ℕ$
13	12	orim2i	$⊢ (- y \in ℕ_{0} \lor (- y \in ℝ \land - (- y) \in ℕ)) \to (- y \in ℕ_{0} \lor - (- y) \in ℕ)$
14	11 13	syl	$⊢ y \in ℤ \to (- y \in ℕ_{0} \lor - (- y) \in ℕ)$
15		zcn	$⊢ y \in ℤ \to y \in ℂ$
16	15	negnegd	$⊢ y \in ℤ \to - (- y) = y$
17	16	eleq1d	$⊢ y \in ℤ \to (- (- y) \in ℕ \leftrightarrow y \in ℕ)$
18	17	orbi2d	$⊢ y \in ℤ \to ((- y \in ℕ_{0} \lor - (- y) \in ℕ) \leftrightarrow (- y \in ℕ_{0} \lor y \in ℕ))$
19	14 18	mpbid	$⊢ y \in ℤ \to (- y \in ℕ_{0} \lor y \in ℕ)$
20	1	imbi2d	$⊢ x = 0 \to ((ζ \to φ) \leftrightarrow (ζ \to ψ))$
21	2	imbi2d	$⊢ x = y \to ((ζ \to φ) \leftrightarrow (ζ \to χ))$
22	3	imbi2d	$⊢ x = y + 1 \to ((ζ \to φ) \leftrightarrow (ζ \to τ))$
23	4	imbi2d	$⊢ x = - y \to ((ζ \to φ) \leftrightarrow (ζ \to θ))$
24	7	com12	$⊢ y \in ℕ_{0} \to (ζ \to (χ \to τ))$
25	24	a2d	$⊢ y \in ℕ_{0} \to ((ζ \to χ) \to (ζ \to τ))$
26	20 21 22 23 6 25	nn0ind	$⊢ - y \in ℕ_{0} \to (ζ \to θ)$
27	26	com12	$⊢ ζ \to (- y \in ℕ_{0} \to θ)$
28	20 21 22 21 6 25	nn0ind	$⊢ y \in ℕ_{0} \to (ζ \to χ)$
29		nnnn0	$⊢ y \in ℕ \to y \in ℕ_{0}$
30	28 29	syl11	$⊢ ζ \to (y \in ℕ \to χ)$
31	30 8	mpdd	$⊢ ζ \to (y \in ℕ \to θ)$
32	27 31	jaod	$⊢ ζ \to ((- y \in ℕ_{0} \lor y \in ℕ) \to θ)$
33	19 32	syl5	$⊢ ζ \to (y \in ℤ \to θ)$
34	33	ralrimiv	$⊢ ζ \to \forall y \in ℤ θ$
35		znegcl	$⊢ x \in ℤ \to - x \in ℤ$
36		negeq	$⊢ y = - x \to - y = - (- x)$
37		zcn	$⊢ x \in ℤ \to x \in ℂ$
38	37	negnegd	$⊢ x \in ℤ \to - (- x) = x$
39	36 38	sylan9eqr	$⊢ (x \in ℤ \land y = - x) \to - y = x$
40	39	eqcomd	$⊢ (x \in ℤ \land y = - x) \to x = - y$
41	40 4	syl	$⊢ (x \in ℤ \land y = - x) \to (φ \leftrightarrow θ)$
42	41	bicomd	$⊢ (x \in ℤ \land y = - x) \to (θ \leftrightarrow φ)$
43	35 42	rspcdv	$⊢ x \in ℤ \to (\forall y \in ℤ θ \to φ)$
44	43	com12	$⊢ \forall y \in ℤ θ \to (x \in ℤ \to φ)$
45	44	ralrimiv	$⊢ \forall y \in ℤ θ \to \forall x \in ℤ φ$
46	5	rspccv	$⊢ \forall x \in ℤ φ \to (A \in ℤ \to η)$
47	34 45 46	3syl	$⊢ ζ \to (A \in ℤ \to η)$

Metamath Proof Explorer

Theorem zindd

Proof