Metamath Proof Explorer

Theorem fzind2

Description: Induction on the integers from M to N inclusive. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Version of fzind using integer range definitions. (Contributed by Mario Carneiro, 6-Feb-2016)

Ref Expression
Hypotheses fzind2.1 
|- ( x = M -> ( ph <-> ps ) )
fzind2.2 
|- ( x = y -> ( ph <-> ch ) )
fzind2.3 
|- ( x = ( y + 1 ) -> ( ph <-> th ) )
fzind2.4 
|- ( x = K -> ( ph <-> ta ) )
fzind2.5 
|- ( N e. ( ZZ>= ` M ) -> ps )
fzind2.6 
|- ( y e. ( M ..^ N ) -> ( ch -> th ) )
Assertion fzind2 
|- ( K e. ( M ... N ) -> ta )

Proof

Step Hyp Ref Expression
1 fzind2.1 
 |-  ( x = M -> ( ph <-> ps ) )
2 fzind2.2 
 |-  ( x = y -> ( ph <-> ch ) )
3 fzind2.3 
 |-  ( x = ( y + 1 ) -> ( ph <-> th ) )
4 fzind2.4 
 |-  ( x = K -> ( ph <-> ta ) )
5 fzind2.5 
 |-  ( N e. ( ZZ>= ` M ) -> ps )
6 fzind2.6 
 |-  ( y e. ( M ..^ N ) -> ( ch -> th ) )
7 elfz2 
 |-  ( K e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) )
8 anass 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) ) )
9 df-3an 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) )
10 9 anbi1i 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) <-> ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) )
11 3anass 
 |-  ( ( K e. ZZ /\ M <_ K /\ K <_ N ) <-> ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) )
12 11 anbi2i 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M <_ K /\ K <_ N ) ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( M <_ K /\ K <_ N ) ) ) )
13 8 10 12 3bitr4i 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M <_ K /\ K <_ N ) ) )
14 7 13 bitri 
 |-  ( K e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M <_ K /\ K <_ N ) ) )
15 eluz2 
 |-  ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
16 15 5 sylbir 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ps )
17 3anass 
 |-  ( ( y e. ZZ /\ M <_ y /\ y < N ) <-> ( y e. ZZ /\ ( M <_ y /\ y < N ) ) )
18 elfzo 
 |-  ( ( y e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( y e. ( M ..^ N ) <-> ( M <_ y /\ y < N ) ) )
19 18 6 syl6bir 
 |-  ( ( y e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M <_ y /\ y < N ) -> ( ch -> th ) ) )
20 19 3coml 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ y e. ZZ ) -> ( ( M <_ y /\ y < N ) -> ( ch -> th ) ) )
21 20 3expa 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ y e. ZZ ) -> ( ( M <_ y /\ y < N ) -> ( ch -> th ) ) )
22 21 impr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( y e. ZZ /\ ( M <_ y /\ y < N ) ) ) -> ( ch -> th ) )
23 17 22 sylan2b 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( y e. ZZ /\ M <_ y /\ y < N ) ) -> ( ch -> th ) )
24 1 2 3 4 16 23 fzind 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M <_ K /\ K <_ N ) ) -> ta )
25 14 24 sylbi 
 |-  ( K e. ( M ... N ) -> ta )