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	$⊢ x = 0 \to (φ \leftrightarrow ψ)$
	nn0ind-raph.2	$⊢ x = y \to (φ \leftrightarrow χ)$
	nn0ind-raph.3	$⊢ x = y + 1 \to (φ \leftrightarrow θ)$
	nn0ind-raph.4	$⊢ x = A \to (φ \leftrightarrow τ)$
	nn0ind-raph.5	$⊢ ψ$
	nn0ind-raph.6	$⊢ y \in ℕ_{0} \to (χ \to θ)$
Assertion	nn0ind-raph	$⊢ A \in ℕ_{0} \to τ$

Proof

Step	Hyp	Ref	Expression
1		nn0ind-raph.1	$⊢ x = 0 \to (φ \leftrightarrow ψ)$
2		nn0ind-raph.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		nn0ind-raph.3	$⊢ x = y + 1 \to (φ \leftrightarrow θ)$
4		nn0ind-raph.4	$⊢ x = A \to (φ \leftrightarrow τ)$
5		nn0ind-raph.5	$⊢ ψ$
6		nn0ind-raph.6	$⊢ y \in ℕ_{0} \to (χ \to θ)$
7		elnn0	$⊢ A \in ℕ_{0} \leftrightarrow (A \in ℕ \lor A = 0)$
8		dfsbcq2	$⊢ z = 1 \to ([z/ x] φ \leftrightarrow \underset{˙}{[} 1 / x \underset{˙}{]} φ)$
9		nfv	$⊢ Ⅎ x χ$
10	9 2	sbhypf	$⊢ z = y \to ([z/ x] φ \leftrightarrow χ)$
11		nfv	$⊢ Ⅎ x θ$
12	11 3	sbhypf	$⊢ z = y + 1 \to ([z/ x] φ \leftrightarrow θ)$
13		nfv	$⊢ Ⅎ x τ$
14	13 4	sbhypf	$⊢ z = A \to ([z/ x] φ \leftrightarrow τ)$
15		nfsbc1v	$⊢ Ⅎ x \underset{˙}{[} 1 / x \underset{˙}{]} φ$
16		1ex	$⊢ 1 \in V$
17		c0ex	$⊢ 0 \in V$
18		0nn0	$⊢ 0 \in ℕ_{0}$
19		eleq1a	$⊢ 0 \in ℕ_{0} \to (y = 0 \to y \in ℕ_{0})$
20	18 19	ax-mp	$⊢ y = 0 \to y \in ℕ_{0}$
21	5 1	mpbiri	$⊢ x = 0 \to φ$
22		eqeq2	$⊢ y = 0 \to (x = y \leftrightarrow x = 0)$
23	22 2	biimtrrdi	$⊢ y = 0 \to (x = 0 \to (φ \leftrightarrow χ))$
24	23	pm5.74d	$⊢ y = 0 \to ((x = 0 \to φ) \leftrightarrow (x = 0 \to χ))$
25	21 24	mpbii	$⊢ y = 0 \to (x = 0 \to χ)$
26	25	com12	$⊢ x = 0 \to (y = 0 \to χ)$
27	17 26	vtocle	$⊢ y = 0 \to χ$
28	20 27 6	sylc	$⊢ y = 0 \to θ$
29	28	adantr	$⊢ (y = 0 \land x = 1) \to θ$
30		oveq1	$⊢ y = 0 \to y + 1 = 0 + 1$
31		0p1e1	$⊢ 0 + 1 = 1$
32	30 31	eqtrdi	$⊢ y = 0 \to y + 1 = 1$
33	32	eqeq2d	$⊢ y = 0 \to (x = y + 1 \leftrightarrow x = 1)$
34	33 3	biimtrrdi	$⊢ y = 0 \to (x = 1 \to (φ \leftrightarrow θ))$
35	34	imp	$⊢ (y = 0 \land x = 1) \to (φ \leftrightarrow θ)$
36	29 35	mpbird	$⊢ (y = 0 \land x = 1) \to φ$
37	36	ex	$⊢ y = 0 \to (x = 1 \to φ)$
38	17 37	vtocle	$⊢ x = 1 \to φ$
39		sbceq1a	$⊢ x = 1 \to (φ \leftrightarrow \underset{˙}{[} 1 / x \underset{˙}{]} φ)$
40	38 39	mpbid	$⊢ x = 1 \to \underset{˙}{[} 1 / x \underset{˙}{]} φ$
41	15 16 40	vtoclef	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} φ$
42		nnnn0	$⊢ y \in ℕ \to y \in ℕ_{0}$
43	42 6	syl	$⊢ y \in ℕ \to (χ \to θ)$
44	8 10 12 14 41 43	nnind	$⊢ A \in ℕ \to τ$
45		nfv	$⊢ Ⅎ x (0 = A \to τ)$
46		eqeq1	$⊢ x = 0 \to (x = A \leftrightarrow 0 = A)$
47	1	bicomd	$⊢ x = 0 \to (ψ \leftrightarrow φ)$
48	47 4	sylan9bb	$⊢ (x = 0 \land x = A) \to (ψ \leftrightarrow τ)$
49	5 48	mpbii	$⊢ (x = 0 \land x = A) \to τ$
50	49	ex	$⊢ x = 0 \to (x = A \to τ)$
51	46 50	sylbird	$⊢ x = 0 \to (0 = A \to τ)$
52	45 17 51	vtoclef	$⊢ 0 = A \to τ$
53	52	eqcoms	$⊢ A = 0 \to τ$
54	44 53	jaoi	$⊢ (A \in ℕ \lor A = 0) \to τ$
55	7 54	sylbi	$⊢ A \in ℕ_{0} \to τ$

Metamath Proof Explorer

Theorem nn0ind-raph

Proof