Metamath Proof Explorer


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 x = 0 φ ψ
fnn0ind.2 x = y φ χ
fnn0ind.3 x = y + 1 φ θ
fnn0ind.4 x = K φ τ
fnn0ind.5 N 0 ψ
fnn0ind.6 N 0 y 0 y < N χ θ
Assertion fnn0ind N 0 K 0 K N τ

Proof

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