Theorem 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	⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
	fnn0ind.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
	fnn0ind.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
	fnn0ind.4	⊢ ( 𝑥 = 𝐾 → ( 𝜑 ↔ 𝜏 ) )
	fnn0ind.5	⊢ ( 𝑁 ∈ ℕ0 → 𝜓 )
	fnn0ind.6	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ∧ 𝑦 < 𝑁 ) → ( 𝜒 → 𝜃 ) )
Assertion	fnn0ind	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		fnn0ind.1	⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
2		fnn0ind.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3		fnn0ind.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4		fnn0ind.4	⊢ ( 𝑥 = 𝐾 → ( 𝜑 ↔ 𝜏 ) )
5		fnn0ind.5	⊢ ( 𝑁 ∈ ℕ0 → 𝜓 )
6		fnn0ind.6	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ∧ 𝑦 < 𝑁 ) → ( 𝜒 → 𝜃 ) )
7		elnn0z	⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
8		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
9		0z	⊢ 0 ∈ ℤ
10		elnn0z	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
11	10 5	sylbir	⊢ ( ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) → 𝜓 )
12	11	3adant1	⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) → 𝜓 )
13		0re	⊢ 0 ∈ ℝ
14		zre	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ )
15		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
16		lelttr	⊢ ( ( 0 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → 0 < 𝑁 ) )
17		ltle	⊢ ( ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 < 𝑁 → 0 ≤ 𝑁 ) )
18	17	3adant2	⊢ ( ( 0 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 < 𝑁 → 0 ≤ 𝑁 ) )
19	16 18	syld	⊢ ( ( 0 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → 0 ≤ 𝑁 ) )
20	13 14 15 19	mp3an3an	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → 0 ≤ 𝑁 ) )
21	20	ex	⊢ ( 𝑦 ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → 0 ≤ 𝑁 ) ) )
22	21	com23	⊢ ( 𝑦 ∈ ℤ → ( ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝑁 ∈ ℤ → 0 ≤ 𝑁 ) ) )
23	22	3impib	⊢ ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝑁 ∈ ℤ → 0 ≤ 𝑁 ) )
24	23	impcom	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → 0 ≤ 𝑁 )
25		elnn0z	⊢ ( 𝑦 ∈ ℕ0 ↔ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ) )
26	25	anbi1i	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑦 < 𝑁 ) ↔ ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) )
27	6	3expb	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) )
28	10 26 27	syl2anbr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) ∧ ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) )
29	28	expcom	⊢ ( ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) → ( ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
30	29	3impa	⊢ ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
31	30	expd	⊢ ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝑁 ∈ ℤ → ( 0 ≤ 𝑁 → ( 𝜒 → 𝜃 ) ) ) )
32	31	impcom	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 0 ≤ 𝑁 → ( 𝜒 → 𝜃 ) ) )
33	24 32	mpd	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) )
34	33	adantll	⊢ ( ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) )
35	1 2 3 4 12 34	fzind	⊢ ( ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) → 𝜏 )
36	9 35	mpanl1	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) → 𝜏 )
37	36	expcom	⊢ ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → ( 𝑁 ∈ ℤ → 𝜏 ) )
38	8 37	syl5	⊢ ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → ( 𝑁 ∈ ℕ0 → 𝜏 ) )
39	38	3expa	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) ∧ 𝐾 ≤ 𝑁 ) → ( 𝑁 ∈ ℕ0 → 𝜏 ) )
40	7 39	sylanb	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) → ( 𝑁 ∈ ℕ0 → 𝜏 ) )
41	40	impcom	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ) → 𝜏 )
42	41	3impb	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) → 𝜏 )