This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜁 → ( 𝐴 ∈ ℤ → 𝜂 ) )