Theorem 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	⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
	zindd.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
	zindd.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜏 ) )
	zindd.4	⊢ ( 𝑥 = - 𝑦 → ( 𝜑 ↔ 𝜃 ) )
	zindd.5	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜂 ) )
	zindd.6	⊢ ( 𝜁 → 𝜓 )
	zindd.7	⊢ ( 𝜁 → ( 𝑦 ∈ ℕ0 → ( 𝜒 → 𝜏 ) ) )
	zindd.8	⊢ ( 𝜁 → ( 𝑦 ∈ ℕ → ( 𝜒 → 𝜃 ) ) )
Assertion	zindd	⊢ ( 𝜁 → ( 𝐴 ∈ ℤ → 𝜂 ) )

Proof

Step	Hyp	Ref	Expression
1		zindd.1	⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
2		zindd.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3		zindd.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜏 ) )
4		zindd.4	⊢ ( 𝑥 = - 𝑦 → ( 𝜑 ↔ 𝜃 ) )
5		zindd.5	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜂 ) )
6		zindd.6	⊢ ( 𝜁 → 𝜓 )
7		zindd.7	⊢ ( 𝜁 → ( 𝑦 ∈ ℕ0 → ( 𝜒 → 𝜏 ) ) )
8		zindd.8	⊢ ( 𝜁 → ( 𝑦 ∈ ℕ → ( 𝜒 → 𝜃 ) ) )
9		znegcl	⊢ ( 𝑦 ∈ ℤ → - 𝑦 ∈ ℤ )
10		elznn0nn	⊢ ( - 𝑦 ∈ ℤ ↔ ( - 𝑦 ∈ ℕ0 ∨ ( - 𝑦 ∈ ℝ ∧ - - 𝑦 ∈ ℕ ) ) )
11	9 10	sylib	⊢ ( 𝑦 ∈ ℤ → ( - 𝑦 ∈ ℕ0 ∨ ( - 𝑦 ∈ ℝ ∧ - - 𝑦 ∈ ℕ ) ) )
12		simpr	⊢ ( ( - 𝑦 ∈ ℝ ∧ - - 𝑦 ∈ ℕ ) → - - 𝑦 ∈ ℕ )
13	12	orim2i	⊢ ( ( - 𝑦 ∈ ℕ0 ∨ ( - 𝑦 ∈ ℝ ∧ - - 𝑦 ∈ ℕ ) ) → ( - 𝑦 ∈ ℕ0 ∨ - - 𝑦 ∈ ℕ ) )
14	11 13	syl	⊢ ( 𝑦 ∈ ℤ → ( - 𝑦 ∈ ℕ0 ∨ - - 𝑦 ∈ ℕ ) )
15		zcn	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
16	15	negnegd	⊢ ( 𝑦 ∈ ℤ → - - 𝑦 = 𝑦 )
17	16	eleq1d	⊢ ( 𝑦 ∈ ℤ → ( - - 𝑦 ∈ ℕ ↔ 𝑦 ∈ ℕ ) )
18	17	orbi2d	⊢ ( 𝑦 ∈ ℤ → ( ( - 𝑦 ∈ ℕ0 ∨ - - 𝑦 ∈ ℕ ) ↔ ( - 𝑦 ∈ ℕ0 ∨ 𝑦 ∈ ℕ ) ) )
19	14 18	mpbid	⊢ ( 𝑦 ∈ ℤ → ( - 𝑦 ∈ ℕ0 ∨ 𝑦 ∈ ℕ ) )
20	1	imbi2d	⊢ ( 𝑥 = 0 → ( ( 𝜁 → 𝜑 ) ↔ ( 𝜁 → 𝜓 ) ) )
21	2	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜁 → 𝜑 ) ↔ ( 𝜁 → 𝜒 ) ) )
22	3	imbi2d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝜁 → 𝜑 ) ↔ ( 𝜁 → 𝜏 ) ) )
23	4	imbi2d	⊢ ( 𝑥 = - 𝑦 → ( ( 𝜁 → 𝜑 ) ↔ ( 𝜁 → 𝜃 ) ) )
24	7	com12	⊢ ( 𝑦 ∈ ℕ0 → ( 𝜁 → ( 𝜒 → 𝜏 ) ) )
25	24	a2d	⊢ ( 𝑦 ∈ ℕ0 → ( ( 𝜁 → 𝜒 ) → ( 𝜁 → 𝜏 ) ) )
26	20 21 22 23 6 25	nn0ind	⊢ ( - 𝑦 ∈ ℕ0 → ( 𝜁 → 𝜃 ) )
27	26	com12	⊢ ( 𝜁 → ( - 𝑦 ∈ ℕ0 → 𝜃 ) )
28	20 21 22 21 6 25	nn0ind	⊢ ( 𝑦 ∈ ℕ0 → ( 𝜁 → 𝜒 ) )
29		nnnn0	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℕ0 )
30	28 29	syl11	⊢ ( 𝜁 → ( 𝑦 ∈ ℕ → 𝜒 ) )
31	30 8	mpdd	⊢ ( 𝜁 → ( 𝑦 ∈ ℕ → 𝜃 ) )
32	27 31	jaod	⊢ ( 𝜁 → ( ( - 𝑦 ∈ ℕ0 ∨ 𝑦 ∈ ℕ ) → 𝜃 ) )
33	19 32	syl5	⊢ ( 𝜁 → ( 𝑦 ∈ ℤ → 𝜃 ) )
34	33	ralrimiv	⊢ ( 𝜁 → ∀ 𝑦 ∈ ℤ 𝜃 )
35		znegcl	⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ )
36		negeq	⊢ ( 𝑦 = - 𝑥 → - 𝑦 = - - 𝑥 )
37		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
38	37	negnegd	⊢ ( 𝑥 ∈ ℤ → - - 𝑥 = 𝑥 )
39	36 38	sylan9eqr	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = - 𝑥 ) → - 𝑦 = 𝑥 )
40	39	eqcomd	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = - 𝑥 ) → 𝑥 = - 𝑦 )
41	40 4	syl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = - 𝑥 ) → ( 𝜑 ↔ 𝜃 ) )
42	41	bicomd	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = - 𝑥 ) → ( 𝜃 ↔ 𝜑 ) )
43	35 42	rspcdv	⊢ ( 𝑥 ∈ ℤ → ( ∀ 𝑦 ∈ ℤ 𝜃 → 𝜑 ) )
44	43	com12	⊢ ( ∀ 𝑦 ∈ ℤ 𝜃 → ( 𝑥 ∈ ℤ → 𝜑 ) )
45	44	ralrimiv	⊢ ( ∀ 𝑦 ∈ ℤ 𝜃 → ∀ 𝑥 ∈ ℤ 𝜑 )
46	5	rspccv	⊢ ( ∀ 𝑥 ∈ ℤ 𝜑 → ( 𝐴 ∈ ℤ → 𝜂 ) )
47	34 45 46	3syl	⊢ ( 𝜁 → ( 𝐴 ∈ ℤ → 𝜂 ) )