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 → 𝜏 )