This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uzind4i

Description: Induction on the upper integers that start at M . The first four give us the substitution instances we need, and the last two are the basis and the induction step. This is a stronger version of uzind4 assuming that ps holds unconditionally. Notice that N e. ( ZZ>=M ) implies that the lower bound M is an integer ( M e. ZZ , see eluzel2 ). (Contributed by NM, 4-Sep-2005) (Revised by AV, 13-Jul-2022)

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

Proof

Step Hyp Ref Expression
1 uzind4i.1 
 |-  ( j = M -> ( ph <-> ps ) )
2 uzind4i.2 
 |-  ( j = k -> ( ph <-> ch ) )
3 uzind4i.3 
 |-  ( j = ( k + 1 ) -> ( ph <-> th ) )
4 uzind4i.4 
 |-  ( j = N -> ( ph <-> ta ) )
5 uzind4i.5 
 |-  ps
6 uzind4i.6 
 |-  ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )
7 5 a1i 
 |-  ( M e. ZZ -> ps )
8 1 2 3 4 7 6 uzind4 
 |-  ( N e. ( ZZ>= ` M ) -> ta )