Metamath Proof Explorer

Theorem fzindd

Description: Induction on the integers from M to N inclusive, a deduction version. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses fzindd.1 
|- ( x = M -> ( ps <-> ch ) )
fzindd.2 
|- ( x = y -> ( ps <-> th ) )
fzindd.3 
|- ( x = ( y + 1 ) -> ( ps <-> ta ) )
fzindd.4 
|- ( x = A -> ( ps <-> et ) )
fzindd.5 
|- ( ph -> ch )
fzindd.6 
|- ( ( ph /\ ( y e. ZZ /\ M <_ y /\ y < N ) /\ th ) -> ta )
fzindd.7 
|- ( ph -> M e. ZZ )
fzindd.8 
|- ( ph -> N e. ZZ )
fzindd.9 
|- ( ph -> M <_ N )
Assertion fzindd 
|- ( ( ph /\ ( A e. ZZ /\ M <_ A /\ A <_ N ) ) -> et )

Proof

Step Hyp Ref Expression
1 fzindd.1 
 |-  ( x = M -> ( ps <-> ch ) )
2 fzindd.2 
 |-  ( x = y -> ( ps <-> th ) )
3 fzindd.3 
 |-  ( x = ( y + 1 ) -> ( ps <-> ta ) )
4 fzindd.4 
 |-  ( x = A -> ( ps <-> et ) )
5 fzindd.5 
 |-  ( ph -> ch )
6 fzindd.6 
 |-  ( ( ph /\ ( y e. ZZ /\ M <_ y /\ y < N ) /\ th ) -> ta )
7 fzindd.7 
 |-  ( ph -> M e. ZZ )
8 fzindd.8 
 |-  ( ph -> N e. ZZ )
9 fzindd.9 
 |-  ( ph -> M <_ N )
10 7 8 jca 
 |-  ( ph -> ( M e. ZZ /\ N e. ZZ ) )
11 1 imbi2d 
 |-  ( x = M -> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
12 2 imbi2d 
 |-  ( x = y -> ( ( ph -> ps ) <-> ( ph -> th ) ) )
13 3 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( ph -> ps ) <-> ( ph -> ta ) ) )
14 4 imbi2d 
 |-  ( x = A -> ( ( ph -> ps ) <-> ( ph -> et ) ) )
15 5 a1i 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( ph -> ch ) )
16 6 3expa 
 |-  ( ( ( ph /\ ( y e. ZZ /\ M <_ y /\ y < N ) ) /\ th ) -> ta )
17 16 ex 
 |-  ( ( ph /\ ( y e. ZZ /\ M <_ y /\ y < N ) ) -> ( th -> ta ) )
18 17 expcom 
 |-  ( ( y e. ZZ /\ M <_ y /\ y < N ) -> ( ph -> ( th -> ta ) ) )
19 18 a2d 
 |-  ( ( y e. ZZ /\ M <_ y /\ y < N ) -> ( ( ph -> th ) -> ( ph -> ta ) ) )
20 19 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( y e. ZZ /\ M <_ y /\ y < N ) ) -> ( ( ph -> th ) -> ( ph -> ta ) ) )
21 11 12 13 14 15 20 fzind 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( A e. ZZ /\ M <_ A /\ A <_ N ) ) -> ( ph -> et ) )
22 10 21 sylan 
 |-  ( ( ph /\ ( A e. ZZ /\ M <_ A /\ A <_ N ) ) -> ( ph -> et ) )
23 22 imp 
 |-  ( ( ( ph /\ ( A e. ZZ /\ M <_ A /\ A <_ N ) ) /\ ph ) -> et )
24 23 anabss1 
 |-  ( ( ph /\ ( A e. ZZ /\ M <_ A /\ A <_ N ) ) -> et )