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

Metamath Proof Explorer

Theorem nn0ind-raph

Description: Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Raph Levien remarks: "This seems a bit painful. I wonder if an explicit substitution version would be easier." (Contributed by Raph Levien, 10-Apr-2004)

Ref Expression
Hypotheses nn0ind-raph.1 ⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
nn0ind-raph.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
nn0ind-raph.3 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
nn0ind-raph.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
nn0ind-raph.5 ⊢ 𝜓
nn0ind-raph.6 ⊢ ( 𝑦 ∈ ℕ0 → ( 𝜒 → 𝜃 ) )
Assertion nn0ind-raph ( 𝐴 ∈ ℕ0 → 𝜏 )

Proof

Step Hyp Ref Expression
1 nn0ind-raph.1 ⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
2 nn0ind-raph.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3 nn0ind-raph.3 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4 nn0ind-raph.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5 nn0ind-raph.5 ⊢ 𝜓
6 nn0ind-raph.6 ⊢ ( 𝑦 ∈ ℕ0 → ( 𝜒 → 𝜃 ) )
7 elnn0 ⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
8 dfsbcq2 ⊢ ( 𝑧 = 1 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 1 / 𝑥 ] 𝜑 ) )
9 nfv ⊢ Ⅎ 𝑥 𝜒
10 9 2 sbhypf ⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜒 ) )
11 nfv ⊢ Ⅎ 𝑥 𝜃
12 11 3 sbhypf ⊢ ( 𝑧 = ( 𝑦 + 1 ) → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜃 ) )
13 nfv ⊢ Ⅎ 𝑥 𝜏
14 13 4 sbhypf ⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜏 ) )
15 nfsbc1v ⊢ Ⅎ 𝑥 [ 1 / 𝑥 ] 𝜑
16 1ex ⊢ 1 ∈ V
17 c0ex ⊢ 0 ∈ V
18 0nn0 ⊢ 0 ∈ ℕ0
19 eleq1a ⊢ ( 0 ∈ ℕ0 → ( 𝑦 = 0 → 𝑦 ∈ ℕ0 ) )
20 18 19 ax-mp ⊢ ( 𝑦 = 0 → 𝑦 ∈ ℕ0 )
21 5 1 mpbiri ⊢ ( 𝑥 = 0 → 𝜑 )
22 eqeq2 ⊢ ( 𝑦 = 0 → ( 𝑥 = 𝑦 ↔ 𝑥 = 0 ) )
23 22 2 biimtrrdi ⊢ ( 𝑦 = 0 → ( 𝑥 = 0 → ( 𝜑 ↔ 𝜒 ) ) )
24 23 pm5.74d ⊢ ( 𝑦 = 0 → ( ( 𝑥 = 0 → 𝜑 ) ↔ ( 𝑥 = 0 → 𝜒 ) ) )
25 21 24 mpbii ⊢ ( 𝑦 = 0 → ( 𝑥 = 0 → 𝜒 ) )
26 25 com12 ⊢ ( 𝑥 = 0 → ( 𝑦 = 0 → 𝜒 ) )
27 17 26 vtocle ⊢ ( 𝑦 = 0 → 𝜒 )
28 20 27 6 sylc ⊢ ( 𝑦 = 0 → 𝜃 )
29 28 adantr ⊢ ( ( 𝑦 = 0 ∧ 𝑥 = 1 ) → 𝜃 )
30 oveq1 ⊢ ( 𝑦 = 0 → ( 𝑦 + 1 ) = ( 0 + 1 ) )
31 0p1e1 ⊢ ( 0 + 1 ) = 1
32 30 31 eqtrdi ⊢ ( 𝑦 = 0 → ( 𝑦 + 1 ) = 1 )
33 32 eqeq2d ⊢ ( 𝑦 = 0 → ( 𝑥 = ( 𝑦 + 1 ) ↔ 𝑥 = 1 ) )
34 33 3 biimtrrdi ⊢ ( 𝑦 = 0 → ( 𝑥 = 1 → ( 𝜑 ↔ 𝜃 ) ) )
35 34 imp ⊢ ( ( 𝑦 = 0 ∧ 𝑥 = 1 ) → ( 𝜑 ↔ 𝜃 ) )
36 29 35 mpbird ⊢ ( ( 𝑦 = 0 ∧ 𝑥 = 1 ) → 𝜑 )
37 36 ex ⊢ ( 𝑦 = 0 → ( 𝑥 = 1 → 𝜑 ) )
38 17 37 vtocle ⊢ ( 𝑥 = 1 → 𝜑 )
39 sbceq1a ⊢ ( 𝑥 = 1 → ( 𝜑 ↔ [ 1 / 𝑥 ] 𝜑 ) )
40 38 39 mpbid ⊢ ( 𝑥 = 1 → [ 1 / 𝑥 ] 𝜑 )
41 15 16 40 vtoclef ⊢ [ 1 / 𝑥 ] 𝜑
42 nnnn0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℕ0 )
43 42 6 syl ⊢ ( 𝑦 ∈ ℕ → ( 𝜒 → 𝜃 ) )
44 8 10 12 14 41 43 nnind ⊢ ( 𝐴 ∈ ℕ → 𝜏 )
45 nfv ⊢ Ⅎ 𝑥 ( 0 = 𝐴 → 𝜏 )
46 eqeq1 ⊢ ( 𝑥 = 0 → ( 𝑥 = 𝐴 ↔ 0 = 𝐴 ) )
47 1 bicomd ⊢ ( 𝑥 = 0 → ( 𝜓 ↔ 𝜑 ) )
48 47 4 sylan9bb ⊢ ( ( 𝑥 = 0 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜏 ) )
49 5 48 mpbii ⊢ ( ( 𝑥 = 0 ∧ 𝑥 = 𝐴 ) → 𝜏 )
50 49 ex ⊢ ( 𝑥 = 0 → ( 𝑥 = 𝐴 → 𝜏 ) )
51 46 50 sylbird ⊢ ( 𝑥 = 0 → ( 0 = 𝐴 → 𝜏 ) )
52 45 17 51 vtoclef ⊢ ( 0 = 𝐴 → 𝜏 )
53 52 eqcoms ⊢ ( 𝐴 = 0 → 𝜏 )
54 44 53 jaoi ⊢ ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) → 𝜏 )
55 7 54 sylbi ⊢ ( 𝐴 ∈ ℕ0 → 𝜏 )