Metamath Proof Explorer

Theorem uzind

Description: Induction on the upper integers that start at 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, 5-Jul-2005)

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

Proof

Step Hyp Ref Expression
1 uzind.1 
 |-  ( j = M -> ( ph <-> ps ) )
2 uzind.2 
 |-  ( j = k -> ( ph <-> ch ) )
3 uzind.3 
 |-  ( j = ( k + 1 ) -> ( ph <-> th ) )
4 uzind.4 
 |-  ( j = N -> ( ph <-> ta ) )
5 uzind.5 
 |-  ( M e. ZZ -> ps )
6 uzind.6 
 |-  ( ( M e. ZZ /\ k e. ZZ /\ M <_ k ) -> ( ch -> th ) )
7 zre 
 |-  ( M e. ZZ -> M e. RR )
8 7 leidd 
 |-  ( M e. ZZ -> M <_ M )
9 8 5 jca 
 |-  ( M e. ZZ -> ( M <_ M /\ ps ) )
10 9 ancli 
 |-  ( M e. ZZ -> ( M e. ZZ /\ ( M <_ M /\ ps ) ) )
11 breq2 
 |-  ( j = M -> ( M <_ j <-> M <_ M ) )
12 11 1 anbi12d 
 |-  ( j = M -> ( ( M <_ j /\ ph ) <-> ( M <_ M /\ ps ) ) )
13 12 elrab 
 |-  ( M e. { j e. ZZ | ( M <_ j /\ ph ) } <-> ( M e. ZZ /\ ( M <_ M /\ ps ) ) )
14 10 13 sylibr 
 |-  ( M e. ZZ -> M e. { j e. ZZ | ( M <_ j /\ ph ) } )
15 peano2z 
 |-  ( k e. ZZ -> ( k + 1 ) e. ZZ )
16 15 a1i 
 |-  ( M e. ZZ -> ( k e. ZZ -> ( k + 1 ) e. ZZ ) )
17 16 adantrd 
 |-  ( M e. ZZ -> ( ( k e. ZZ /\ ( M <_ k /\ ch ) ) -> ( k + 1 ) e. ZZ ) )
18 zre 
 |-  ( k e. ZZ -> k e. RR )
19 ltp1 
 |-  ( k e. RR -> k < ( k + 1 ) )
20 19 adantl 
 |-  ( ( M e. RR /\ k e. RR ) -> k < ( k + 1 ) )
21 peano2re 
 |-  ( k e. RR -> ( k + 1 ) e. RR )
22 21 ancli 
 |-  ( k e. RR -> ( k e. RR /\ ( k + 1 ) e. RR ) )
23 lelttr 
 |-  ( ( M e. RR /\ k e. RR /\ ( k + 1 ) e. RR ) -> ( ( M <_ k /\ k < ( k + 1 ) ) -> M < ( k + 1 ) ) )
24 23 3expb 
 |-  ( ( M e. RR /\ ( k e. RR /\ ( k + 1 ) e. RR ) ) -> ( ( M <_ k /\ k < ( k + 1 ) ) -> M < ( k + 1 ) ) )
25 22 24 sylan2 
 |-  ( ( M e. RR /\ k e. RR ) -> ( ( M <_ k /\ k < ( k + 1 ) ) -> M < ( k + 1 ) ) )
26 20 25 mpan2d 
 |-  ( ( M e. RR /\ k e. RR ) -> ( M <_ k -> M < ( k + 1 ) ) )
27 ltle 
 |-  ( ( M e. RR /\ ( k + 1 ) e. RR ) -> ( M < ( k + 1 ) -> M <_ ( k + 1 ) ) )
28 21 27 sylan2 
 |-  ( ( M e. RR /\ k e. RR ) -> ( M < ( k + 1 ) -> M <_ ( k + 1 ) ) )
29 26 28 syld 
 |-  ( ( M e. RR /\ k e. RR ) -> ( M <_ k -> M <_ ( k + 1 ) ) )
30 7 18 29 syl2an 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( M <_ k -> M <_ ( k + 1 ) ) )
31 30 adantrd 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( ( M <_ k /\ ch ) -> M <_ ( k + 1 ) ) )
32 31 expimpd 
 |-  ( M e. ZZ -> ( ( k e. ZZ /\ ( M <_ k /\ ch ) ) -> M <_ ( k + 1 ) ) )
33 6 3exp 
 |-  ( M e. ZZ -> ( k e. ZZ -> ( M <_ k -> ( ch -> th ) ) ) )
34 33 imp4d 
 |-  ( M e. ZZ -> ( ( k e. ZZ /\ ( M <_ k /\ ch ) ) -> th ) )
35 32 34 jcad 
 |-  ( M e. ZZ -> ( ( k e. ZZ /\ ( M <_ k /\ ch ) ) -> ( M <_ ( k + 1 ) /\ th ) ) )
36 17 35 jcad 
 |-  ( M e. ZZ -> ( ( k e. ZZ /\ ( M <_ k /\ ch ) ) -> ( ( k + 1 ) e. ZZ /\ ( M <_ ( k + 1 ) /\ th ) ) ) )
37 breq2 
 |-  ( j = k -> ( M <_ j <-> M <_ k ) )
38 37 2 anbi12d 
 |-  ( j = k -> ( ( M <_ j /\ ph ) <-> ( M <_ k /\ ch ) ) )
39 38 elrab 
 |-  ( k e. { j e. ZZ | ( M <_ j /\ ph ) } <-> ( k e. ZZ /\ ( M <_ k /\ ch ) ) )
40 breq2 
 |-  ( j = ( k + 1 ) -> ( M <_ j <-> M <_ ( k + 1 ) ) )
41 40 3 anbi12d 
 |-  ( j = ( k + 1 ) -> ( ( M <_ j /\ ph ) <-> ( M <_ ( k + 1 ) /\ th ) ) )
42 41 elrab 
 |-  ( ( k + 1 ) e. { j e. ZZ | ( M <_ j /\ ph ) } <-> ( ( k + 1 ) e. ZZ /\ ( M <_ ( k + 1 ) /\ th ) ) )
43 36 39 42 3imtr4g 
 |-  ( M e. ZZ -> ( k e. { j e. ZZ | ( M <_ j /\ ph ) } -> ( k + 1 ) e. { j e. ZZ | ( M <_ j /\ ph ) } ) )
44 43 ralrimiv 
 |-  ( M e. ZZ -> A. k e. { j e. ZZ | ( M <_ j /\ ph ) } ( k + 1 ) e. { j e. ZZ | ( M <_ j /\ ph ) } )
45 peano5uzti 
 |-  ( M e. ZZ -> ( ( M e. { j e. ZZ | ( M <_ j /\ ph ) } /\ A. k e. { j e. ZZ | ( M <_ j /\ ph ) } ( k + 1 ) e. { j e. ZZ | ( M <_ j /\ ph ) } ) -> { w e. ZZ | M <_ w } C_ { j e. ZZ | ( M <_ j /\ ph ) } ) )
46 14 44 45 mp2and 
 |-  ( M e. ZZ -> { w e. ZZ | M <_ w } C_ { j e. ZZ | ( M <_ j /\ ph ) } )
47 46 sseld 
 |-  ( M e. ZZ -> ( N e. { w e. ZZ | M <_ w } -> N e. { j e. ZZ | ( M <_ j /\ ph ) } ) )
48 breq2 
 |-  ( w = N -> ( M <_ w <-> M <_ N ) )
49 48 elrab 
 |-  ( N e. { w e. ZZ | M <_ w } <-> ( N e. ZZ /\ M <_ N ) )
50 breq2 
 |-  ( j = N -> ( M <_ j <-> M <_ N ) )
51 50 4 anbi12d 
 |-  ( j = N -> ( ( M <_ j /\ ph ) <-> ( M <_ N /\ ta ) ) )
52 51 elrab 
 |-  ( N e. { j e. ZZ | ( M <_ j /\ ph ) } <-> ( N e. ZZ /\ ( M <_ N /\ ta ) ) )
53 47 49 52 3imtr3g 
 |-  ( M e. ZZ -> ( ( N e. ZZ /\ M <_ N ) -> ( N e. ZZ /\ ( M <_ N /\ ta ) ) ) )
54 53 3impib 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( N e. ZZ /\ ( M <_ N /\ ta ) ) )
55 54 simprrd 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ta )