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 syl6bir ( 𝑦 = 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 syl6bir ( 𝑦 = 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𝜏 )