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 -> ( ph <-> ps ) )
fnn0ind.2 
|- ( x = y -> ( ph <-> ch ) )
fnn0ind.3 
|- ( x = ( y + 1 ) -> ( ph <-> th ) )
fnn0ind.4 
|- ( x = K -> ( ph <-> ta ) )
fnn0ind.5 
|- ( N e. NN0 -> ps )
fnn0ind.6 
|- ( ( N e. NN0 /\ y e. NN0 /\ y < N ) -> ( ch -> th ) )
Assertion fnn0ind 
|- ( ( N e. NN0 /\ K e. NN0 /\ K <_ N ) -> ta )

Proof

Step Hyp Ref Expression
1 fnn0ind.1 
 |-  ( x = 0 -> ( ph <-> ps ) )
2 fnn0ind.2 
 |-  ( x = y -> ( ph <-> ch ) )
3 fnn0ind.3 
 |-  ( x = ( y + 1 ) -> ( ph <-> th ) )
4 fnn0ind.4 
 |-  ( x = K -> ( ph <-> ta ) )
5 fnn0ind.5 
 |-  ( N e. NN0 -> ps )
6 fnn0ind.6 
 |-  ( ( N e. NN0 /\ y e. NN0 /\ y < N ) -> ( ch -> th ) )
7 elnn0z 
 |-  ( K e. NN0 <-> ( K e. ZZ /\ 0 <_ K ) )
8 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
9 0z 
 |-  0 e. ZZ
10 elnn0z 
 |-  ( N e. NN0 <-> ( N e. ZZ /\ 0 <_ N ) )
11 10 5 sylbir 
 |-  ( ( N e. ZZ /\ 0 <_ N ) -> ps )
12 11 3adant1 
 |-  ( ( 0 e. ZZ /\ N e. ZZ /\ 0 <_ N ) -> ps )
13 0re 
 |-  0 e. RR
14 zre 
 |-  ( y e. ZZ -> y e. RR )
15 zre 
 |-  ( N e. ZZ -> N e. RR )
16 lelttr 
 |-  ( ( 0 e. RR /\ y e. RR /\ N e. RR ) -> ( ( 0 <_ y /\ y < N ) -> 0 < N ) )
17 ltle 
 |-  ( ( 0 e. RR /\ N e. RR ) -> ( 0 < N -> 0 <_ N ) )
18 17 3adant2 
 |-  ( ( 0 e. RR /\ y e. RR /\ N e. RR ) -> ( 0 < N -> 0 <_ N ) )
19 16 18 syld 
 |-  ( ( 0 e. RR /\ y e. RR /\ N e. RR ) -> ( ( 0 <_ y /\ y < N ) -> 0 <_ N ) )
20 13 14 15 19 mp3an3an 
 |-  ( ( y e. ZZ /\ N e. ZZ ) -> ( ( 0 <_ y /\ y < N ) -> 0 <_ N ) )
21 20 ex 
 |-  ( y e. ZZ -> ( N e. ZZ -> ( ( 0 <_ y /\ y < N ) -> 0 <_ N ) ) )
22 21 com23 
 |-  ( y e. ZZ -> ( ( 0 <_ y /\ y < N ) -> ( N e. ZZ -> 0 <_ N ) ) )
23 22 3impib 
 |-  ( ( y e. ZZ /\ 0 <_ y /\ y < N ) -> ( N e. ZZ -> 0 <_ N ) )
24 23 impcom 
 |-  ( ( N e. ZZ /\ ( y e. ZZ /\ 0 <_ y /\ y < N ) ) -> 0 <_ N )
25 elnn0z 
 |-  ( y e. NN0 <-> ( y e. ZZ /\ 0 <_ y ) )
26 25 anbi1i 
 |-  ( ( y e. NN0 /\ y < N ) <-> ( ( y e. ZZ /\ 0 <_ y ) /\ y < N ) )
27 6 3expb 
 |-  ( ( N e. NN0 /\ ( y e. NN0 /\ y < N ) ) -> ( ch -> th ) )
28 10 26 27 syl2anbr 
 |-  ( ( ( N e. ZZ /\ 0 <_ N ) /\ ( ( y e. ZZ /\ 0 <_ y ) /\ y < N ) ) -> ( ch -> th ) )
29 28 expcom 
 |-  ( ( ( y e. ZZ /\ 0 <_ y ) /\ y < N ) -> ( ( N e. ZZ /\ 0 <_ N ) -> ( ch -> th ) ) )
30 29 3impa 
 |-  ( ( y e. ZZ /\ 0 <_ y /\ y < N ) -> ( ( N e. ZZ /\ 0 <_ N ) -> ( ch -> th ) ) )
31 30 expd 
 |-  ( ( y e. ZZ /\ 0 <_ y /\ y < N ) -> ( N e. ZZ -> ( 0 <_ N -> ( ch -> th ) ) ) )
32 31 impcom 
 |-  ( ( N e. ZZ /\ ( y e. ZZ /\ 0 <_ y /\ y < N ) ) -> ( 0 <_ N -> ( ch -> th ) ) )
33 24 32 mpd 
 |-  ( ( N e. ZZ /\ ( y e. ZZ /\ 0 <_ y /\ y < N ) ) -> ( ch -> th ) )
34 33 adantll 
 |-  ( ( ( 0 e. ZZ /\ N e. ZZ ) /\ ( y e. ZZ /\ 0 <_ y /\ y < N ) ) -> ( ch -> th ) )
35 1 2 3 4 12 34 fzind 
 |-  ( ( ( 0 e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ 0 <_ K /\ K <_ N ) ) -> ta )
36 9 35 mpanl1 
 |-  ( ( N e. ZZ /\ ( K e. ZZ /\ 0 <_ K /\ K <_ N ) ) -> ta )
37 36 expcom 
 |-  ( ( K e. ZZ /\ 0 <_ K /\ K <_ N ) -> ( N e. ZZ -> ta ) )
38 8 37 syl5 
 |-  ( ( K e. ZZ /\ 0 <_ K /\ K <_ N ) -> ( N e. NN0 -> ta ) )
39 38 3expa 
 |-  ( ( ( K e. ZZ /\ 0 <_ K ) /\ K <_ N ) -> ( N e. NN0 -> ta ) )
40 7 39 sylanb 
 |-  ( ( K e. NN0 /\ K <_ N ) -> ( N e. NN0 -> ta ) )
41 40 impcom 
 |-  ( ( N e. NN0 /\ ( K e. NN0 /\ K <_ N ) ) -> ta )
42 41 3impb 
 |-  ( ( N e. NN0 /\ K e. NN0 /\ K <_ N ) -> ta )