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 )