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 )