Metamath Proof Explorer

Theorem uzind2

Description: Induction on the upper integers that startafter an integer M . The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by NM, 25-Jul-2005)

Ref Expression
Hypotheses uzind2.1 
|- ( j = ( M + 1 ) -> ( ph <-> ps ) )
uzind2.2 
|- ( j = k -> ( ph <-> ch ) )
uzind2.3 
|- ( j = ( k + 1 ) -> ( ph <-> th ) )
uzind2.4 
|- ( j = N -> ( ph <-> ta ) )
uzind2.5 
|- ( M e. ZZ -> ps )
uzind2.6 
|- ( ( M e. ZZ /\ k e. ZZ /\ M < k ) -> ( ch -> th ) )
Assertion uzind2 
|- ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ta )

Proof

Step Hyp Ref Expression
1 uzind2.1 
 |-  ( j = ( M + 1 ) -> ( ph <-> ps ) )
2 uzind2.2 
 |-  ( j = k -> ( ph <-> ch ) )
3 uzind2.3 
 |-  ( j = ( k + 1 ) -> ( ph <-> th ) )
4 uzind2.4 
 |-  ( j = N -> ( ph <-> ta ) )
5 uzind2.5 
 |-  ( M e. ZZ -> ps )
6 uzind2.6 
 |-  ( ( M e. ZZ /\ k e. ZZ /\ M < k ) -> ( ch -> th ) )
7 zltp1le 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) )
8 peano2z 
 |-  ( M e. ZZ -> ( M + 1 ) e. ZZ )
9 1 imbi2d 
 |-  ( j = ( M + 1 ) -> ( ( M e. ZZ -> ph ) <-> ( M e. ZZ -> ps ) ) )
10 2 imbi2d 
 |-  ( j = k -> ( ( M e. ZZ -> ph ) <-> ( M e. ZZ -> ch ) ) )
11 3 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( M e. ZZ -> ph ) <-> ( M e. ZZ -> th ) ) )
12 4 imbi2d 
 |-  ( j = N -> ( ( M e. ZZ -> ph ) <-> ( M e. ZZ -> ta ) ) )
13 5 a1i 
 |-  ( ( M + 1 ) e. ZZ -> ( M e. ZZ -> ps ) )
14 zltp1le 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( M < k <-> ( M + 1 ) <_ k ) )
15 6 3expia 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( M < k -> ( ch -> th ) ) )
16 14 15 sylbird 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( ( M + 1 ) <_ k -> ( ch -> th ) ) )
17 16 ex 
 |-  ( M e. ZZ -> ( k e. ZZ -> ( ( M + 1 ) <_ k -> ( ch -> th ) ) ) )
18 17 com3l 
 |-  ( k e. ZZ -> ( ( M + 1 ) <_ k -> ( M e. ZZ -> ( ch -> th ) ) ) )
19 18 imp 
 |-  ( ( k e. ZZ /\ ( M + 1 ) <_ k ) -> ( M e. ZZ -> ( ch -> th ) ) )
20 19 3adant1 
 |-  ( ( ( M + 1 ) e. ZZ /\ k e. ZZ /\ ( M + 1 ) <_ k ) -> ( M e. ZZ -> ( ch -> th ) ) )
21 20 a2d 
 |-  ( ( ( M + 1 ) e. ZZ /\ k e. ZZ /\ ( M + 1 ) <_ k ) -> ( ( M e. ZZ -> ch ) -> ( M e. ZZ -> th ) ) )
22 9 10 11 12 13 21 uzind 
 |-  ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ ( M + 1 ) <_ N ) -> ( M e. ZZ -> ta ) )
23 22 3exp 
 |-  ( ( M + 1 ) e. ZZ -> ( N e. ZZ -> ( ( M + 1 ) <_ N -> ( M e. ZZ -> ta ) ) ) )
24 8 23 syl 
 |-  ( M e. ZZ -> ( N e. ZZ -> ( ( M + 1 ) <_ N -> ( M e. ZZ -> ta ) ) ) )
25 24 com34 
 |-  ( M e. ZZ -> ( N e. ZZ -> ( M e. ZZ -> ( ( M + 1 ) <_ N -> ta ) ) ) )
26 25 pm2.43a 
 |-  ( M e. ZZ -> ( N e. ZZ -> ( ( M + 1 ) <_ N -> ta ) ) )
27 26 imp 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M + 1 ) <_ N -> ta ) )
28 7 27 sylbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N -> ta ) )
29 28 3impia 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ta )