fnn0ind

Description: Induction on the integers from 0 to N inclusive. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 31-Mar-2011)

	Ref	Expression
Hypotheses	fnn0ind.1	$⊢ x = 0 \to (φ \leftrightarrow ψ)$
	fnn0ind.2	$⊢ x = y \to (φ \leftrightarrow χ)$
	fnn0ind.3	$⊢ x = y + 1 \to (φ \leftrightarrow θ)$
	fnn0ind.4	$⊢ x = K \to (φ \leftrightarrow τ)$
	fnn0ind.5	$⊢ N \in ℕ_{0} \to ψ$
	fnn0ind.6	$⊢ (N \in ℕ_{0} \land y \in ℕ_{0} \land y < N) \to (χ \to θ)$
Assertion	fnn0ind	$⊢ (N \in ℕ_{0} \land K \in ℕ_{0} \land K \leq N) \to τ$

Proof

Step	Hyp	Ref	Expression
1		fnn0ind.1	$⊢ x = 0 \to (φ \leftrightarrow ψ)$
2		fnn0ind.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		fnn0ind.3	$⊢ x = y + 1 \to (φ \leftrightarrow θ)$
4		fnn0ind.4	$⊢ x = K \to (φ \leftrightarrow τ)$
5		fnn0ind.5	$⊢ N \in ℕ_{0} \to ψ$
6		fnn0ind.6	$⊢ (N \in ℕ_{0} \land y \in ℕ_{0} \land y < N) \to (χ \to θ)$
7		elnn0z	$⊢ K \in ℕ_{0} \leftrightarrow (K \in ℤ \land 0 \leq K)$
8		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
9		0z	$⊢ 0 \in ℤ$
10		elnn0z	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℤ \land 0 \leq N)$
11	10 5	sylbir	$⊢ (N \in ℤ \land 0 \leq N) \to ψ$
12	11	3adant1	$⊢ (0 \in ℤ \land N \in ℤ \land 0 \leq N) \to ψ$
13		0re	$⊢ 0 \in ℝ$
14		zre	$⊢ y \in ℤ \to y \in ℝ$
15		zre	$⊢ N \in ℤ \to N \in ℝ$
16		lelttr	$⊢ (0 \in ℝ \land y \in ℝ \land N \in ℝ) \to ((0 \leq y \land y < N) \to 0 < N)$
17		ltle	$⊢ (0 \in ℝ \land N \in ℝ) \to (0 < N \to 0 \leq N)$
18	17	3adant2	$⊢ (0 \in ℝ \land y \in ℝ \land N \in ℝ) \to (0 < N \to 0 \leq N)$
19	16 18	syld	$⊢ (0 \in ℝ \land y \in ℝ \land N \in ℝ) \to ((0 \leq y \land y < N) \to 0 \leq N)$
20	13 14 15 19	mp3an3an	$⊢ (y \in ℤ \land N \in ℤ) \to ((0 \leq y \land y < N) \to 0 \leq N)$
21	20	ex	$⊢ y \in ℤ \to (N \in ℤ \to ((0 \leq y \land y < N) \to 0 \leq N))$
22	21	com23	$⊢ y \in ℤ \to ((0 \leq y \land y < N) \to (N \in ℤ \to 0 \leq N))$
23	22	3impib	$⊢ (y \in ℤ \land 0 \leq y \land y < N) \to (N \in ℤ \to 0 \leq N)$
24	23	impcom	$⊢ (N \in ℤ \land (y \in ℤ \land 0 \leq y \land y < N)) \to 0 \leq N$
25		elnn0z	$⊢ y \in ℕ_{0} \leftrightarrow (y \in ℤ \land 0 \leq y)$
26	25	anbi1i	$⊢ (y \in ℕ_{0} \land y < N) \leftrightarrow ((y \in ℤ \land 0 \leq y) \land y < N)$
27	6	3expb	$⊢ (N \in ℕ_{0} \land (y \in ℕ_{0} \land y < N)) \to (χ \to θ)$
28	10 26 27	syl2anbr	$⊢ ((N \in ℤ \land 0 \leq N) \land ((y \in ℤ \land 0 \leq y) \land y < N)) \to (χ \to θ)$
29	28	expcom	$⊢ ((y \in ℤ \land 0 \leq y) \land y < N) \to ((N \in ℤ \land 0 \leq N) \to (χ \to θ))$
30	29	3impa	$⊢ (y \in ℤ \land 0 \leq y \land y < N) \to ((N \in ℤ \land 0 \leq N) \to (χ \to θ))$
31	30	expd	$⊢ (y \in ℤ \land 0 \leq y \land y < N) \to (N \in ℤ \to (0 \leq N \to (χ \to θ)))$
32	31	impcom	$⊢ (N \in ℤ \land (y \in ℤ \land 0 \leq y \land y < N)) \to (0 \leq N \to (χ \to θ))$
33	24 32	mpd	$⊢ (N \in ℤ \land (y \in ℤ \land 0 \leq y \land y < N)) \to (χ \to θ)$
34	33	adantll	$⊢ ((0 \in ℤ \land N \in ℤ) \land (y \in ℤ \land 0 \leq y \land y < N)) \to (χ \to θ)$
35	1 2 3 4 12 34	fzind	$⊢ ((0 \in ℤ \land N \in ℤ) \land (K \in ℤ \land 0 \leq K \land K \leq N)) \to τ$
36	9 35	mpanl1	$⊢ (N \in ℤ \land (K \in ℤ \land 0 \leq K \land K \leq N)) \to τ$
37	36	expcom	$⊢ (K \in ℤ \land 0 \leq K \land K \leq N) \to (N \in ℤ \to τ)$
38	8 37	syl5	$⊢ (K \in ℤ \land 0 \leq K \land K \leq N) \to (N \in ℕ_{0} \to τ)$
39	38	3expa	$⊢ ((K \in ℤ \land 0 \leq K) \land K \leq N) \to (N \in ℕ_{0} \to τ)$
40	7 39	sylanb	$⊢ (K \in ℕ_{0} \land K \leq N) \to (N \in ℕ_{0} \to τ)$
41	40	impcom	$⊢ (N \in ℕ_{0} \land (K \in ℕ_{0} \land K \leq N)) \to τ$
42	41	3impb	$⊢ (N \in ℕ_{0} \land K \in ℕ_{0} \land K \leq N) \to τ$

Metamath Proof Explorer

Theorem fnn0ind

Proof