Metamath Proof Explorer

Theorem uzindd

Description: Induction on the upper integers that start at M . The first four hypotheses give us the substitution instances we need; the following two are the basis and the induction step, a deduction version. (Contributed by metakunt, 8-Jun-2024)

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

Proof

Step Hyp Ref Expression
1 uzindd.1 
 |-  ( j = M -> ( ps <-> ch ) )
2 uzindd.2 
 |-  ( j = k -> ( ps <-> th ) )
3 uzindd.3 
 |-  ( j = ( k + 1 ) -> ( ps <-> ta ) )
4 uzindd.4 
 |-  ( j = N -> ( ps <-> et ) )
5 uzindd.5 
 |-  ( ph -> ch )
6 uzindd.6 
 |-  ( ( ph /\ th /\ ( k e. ZZ /\ M <_ k ) ) -> ta )
7 uzindd.7 
 |-  ( ph -> M e. ZZ )
8 uzindd.8 
 |-  ( ph -> N e. ZZ )
9 uzindd.9 
 |-  ( ph -> M <_ N )
10 7 8 9 3jca 
 |-  ( ph -> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
11 1 imbi2d 
 |-  ( j = M -> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
12 2 imbi2d 
 |-  ( j = k -> ( ( ph -> ps ) <-> ( ph -> th ) ) )
13 3 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( ph -> ps ) <-> ( ph -> ta ) ) )
14 4 imbi2d 
 |-  ( j = N -> ( ( ph -> ps ) <-> ( ph -> et ) ) )
15 5 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> ch )
16 15 expcom 
 |-  ( M e. ZZ -> ( ph -> ch ) )
17 3anass 
 |-  ( ( M e. ZZ /\ k e. ZZ /\ M <_ k ) <-> ( M e. ZZ /\ ( k e. ZZ /\ M <_ k ) ) )
18 ancom 
 |-  ( ( M e. ZZ /\ ( k e. ZZ /\ M <_ k ) ) <-> ( ( k e. ZZ /\ M <_ k ) /\ M e. ZZ ) )
19 17 18 bitri 
 |-  ( ( M e. ZZ /\ k e. ZZ /\ M <_ k ) <-> ( ( k e. ZZ /\ M <_ k ) /\ M e. ZZ ) )
20 6 ad4ant123 
 |-  ( ( ( ( ph /\ th ) /\ ( k e. ZZ /\ M <_ k ) ) /\ M e. ZZ ) -> ta )
21 20 anasss 
 |-  ( ( ( ph /\ th ) /\ ( ( k e. ZZ /\ M <_ k ) /\ M e. ZZ ) ) -> ta )
22 19 21 sylan2b 
 |-  ( ( ( ph /\ th ) /\ ( M e. ZZ /\ k e. ZZ /\ M <_ k ) ) -> ta )
23 22 3impa 
 |-  ( ( ph /\ th /\ ( M e. ZZ /\ k e. ZZ /\ M <_ k ) ) -> ta )
24 23 3com23 
 |-  ( ( ph /\ ( M e. ZZ /\ k e. ZZ /\ M <_ k ) /\ th ) -> ta )
25 24 3expia 
 |-  ( ( ph /\ ( M e. ZZ /\ k e. ZZ /\ M <_ k ) ) -> ( th -> ta ) )
26 25 expcom 
 |-  ( ( M e. ZZ /\ k e. ZZ /\ M <_ k ) -> ( ph -> ( th -> ta ) ) )
27 26 a2d 
 |-  ( ( M e. ZZ /\ k e. ZZ /\ M <_ k ) -> ( ( ph -> th ) -> ( ph -> ta ) ) )
28 11 12 13 14 16 27 uzind 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( ph -> et ) )
29 10 28 mpcom 
 |-  ( ph -> et )