Metamath Proof Explorer

Theorem uzsind

Description: Induction on the upper surreal integers that start at M . (Contributed by Scott Fenton, 25-Jul-2025)

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

Proof

Step Hyp Ref Expression
1 uzsind.1 
 |-  ( j = M -> ( ph <-> ps ) )
2 uzsind.2 
 |-  ( j = k -> ( ph <-> ch ) )
3 uzsind.3 
 |-  ( j = ( k +s 1s ) -> ( ph <-> th ) )
4 uzsind.4 
 |-  ( j = N -> ( ph <-> ta ) )
5 uzsind.5 
 |-  ( M e. ZZ_s -> ps )
6 uzsind.6 
 |-  ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) -> ( ch -> th ) )
7 id 
 |-  ( M e. ZZ_s -> M e. ZZ_s )
8 zno 
 |-  ( M e. ZZ_s -> M e. No )
9 slerflex 
 |-  ( M e. No -> M <_s M )
10 8 9 syl 
 |-  ( M e. ZZ_s -> M <_s M )
11 7 10 5 jca32 
 |-  ( M e. ZZ_s -> ( M e. ZZ_s /\ ( M <_s M /\ ps ) ) )
12 breq2 
 |-  ( j = M -> ( M <_s j <-> M <_s M ) )
13 12 1 anbi12d 
 |-  ( j = M -> ( ( M <_s j /\ ph ) <-> ( M <_s M /\ ps ) ) )
14 13 elrab 
 |-  ( M e. { j e. ZZ_s | ( M <_s j /\ ph ) } <-> ( M e. ZZ_s /\ ( M <_s M /\ ps ) ) )
15 11 14 sylibr 
 |-  ( M e. ZZ_s -> M e. { j e. ZZ_s | ( M <_s j /\ ph ) } )
16 simpl 
 |-  ( ( M e. ZZ_s /\ ( k e. ZZ_s /\ ( M <_s k /\ ch ) ) ) -> M e. ZZ_s )
17 simprl 
 |-  ( ( M e. ZZ_s /\ ( k e. ZZ_s /\ ( M <_s k /\ ch ) ) ) -> k e. ZZ_s )
18 simprrl 
 |-  ( ( M e. ZZ_s /\ ( k e. ZZ_s /\ ( M <_s k /\ ch ) ) ) -> M <_s k )
19 simprrr 
 |-  ( ( M e. ZZ_s /\ ( k e. ZZ_s /\ ( M <_s k /\ ch ) ) ) -> ch )
20 id 
 |-  ( k e. ZZ_s -> k e. ZZ_s )
21 1zs 
 |-  1s e. ZZ_s
22 21 a1i 
 |-  ( k e. ZZ_s -> 1s e. ZZ_s )
23 20 22 zaddscld 
 |-  ( k e. ZZ_s -> ( k +s 1s ) e. ZZ_s )
24 23 3ad2ant2 
 |-  ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) -> ( k +s 1s ) e. ZZ_s )
25 24 adantr 
 |-  ( ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) /\ ch ) -> ( k +s 1s ) e. ZZ_s )
26 8 3ad2ant1 
 |-  ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) -> M e. No )
27 23 znod 
 |-  ( k e. ZZ_s -> ( k +s 1s ) e. No )
28 27 3ad2ant2 
 |-  ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) -> ( k +s 1s ) e. No )
29 zno 
 |-  ( k e. ZZ_s -> k e. No )
30 29 3ad2ant2 
 |-  ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) -> k e. No )
31 simp3 
 |-  ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) -> M <_s k )
32 29 sltp1d 
 |-  ( k e. ZZ_s -> k
33 32 3ad2ant2 
 |-  ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) -> k
34 26 30 28 31 33 slelttrd 
 |-  ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) -> M
35 26 28 34 sltled 
 |-  ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) -> M <_s ( k +s 1s ) )
36 35 adantr 
 |-  ( ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) /\ ch ) -> M <_s ( k +s 1s ) )
37 6 imp 
 |-  ( ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) /\ ch ) -> th )
38 25 36 37 jca32 
 |-  ( ( ( M e. ZZ_s /\ k e. ZZ_s /\ M <_s k ) /\ ch ) -> ( ( k +s 1s ) e. ZZ_s /\ ( M <_s ( k +s 1s ) /\ th ) ) )
39 16 17 18 19 38 syl31anc 
 |-  ( ( M e. ZZ_s /\ ( k e. ZZ_s /\ ( M <_s k /\ ch ) ) ) -> ( ( k +s 1s ) e. ZZ_s /\ ( M <_s ( k +s 1s ) /\ th ) ) )
40 breq2 
 |-  ( j = k -> ( M <_s j <-> M <_s k ) )
41 40 2 anbi12d 
 |-  ( j = k -> ( ( M <_s j /\ ph ) <-> ( M <_s k /\ ch ) ) )
42 41 elrab 
 |-  ( k e. { j e. ZZ_s | ( M <_s j /\ ph ) } <-> ( k e. ZZ_s /\ ( M <_s k /\ ch ) ) )
43 42 anbi2i 
 |-  ( ( M e. ZZ_s /\ k e. { j e. ZZ_s | ( M <_s j /\ ph ) } ) <-> ( M e. ZZ_s /\ ( k e. ZZ_s /\ ( M <_s k /\ ch ) ) ) )
44 breq2 
 |-  ( j = ( k +s 1s ) -> ( M <_s j <-> M <_s ( k +s 1s ) ) )
45 44 3 anbi12d 
 |-  ( j = ( k +s 1s ) -> ( ( M <_s j /\ ph ) <-> ( M <_s ( k +s 1s ) /\ th ) ) )
46 45 elrab 
 |-  ( ( k +s 1s ) e. { j e. ZZ_s | ( M <_s j /\ ph ) } <-> ( ( k +s 1s ) e. ZZ_s /\ ( M <_s ( k +s 1s ) /\ th ) ) )
47 39 43 46 3imtr4i 
 |-  ( ( M e. ZZ_s /\ k e. { j e. ZZ_s | ( M <_s j /\ ph ) } ) -> ( k +s 1s ) e. { j e. ZZ_s | ( M <_s j /\ ph ) } )
48 7 15 47 peano5uzs 
 |-  ( M e. ZZ_s -> { w e. ZZ_s | M <_s w } C_ { j e. ZZ_s | ( M <_s j /\ ph ) } )
49 48 sseld 
 |-  ( M e. ZZ_s -> ( N e. { w e. ZZ_s | M <_s w } -> N e. { j e. ZZ_s | ( M <_s j /\ ph ) } ) )
50 breq2 
 |-  ( w = N -> ( M <_s w <-> M <_s N ) )
51 50 elrab 
 |-  ( N e. { w e. ZZ_s | M <_s w } <-> ( N e. ZZ_s /\ M <_s N ) )
52 breq2 
 |-  ( j = N -> ( M <_s j <-> M <_s N ) )
53 52 4 anbi12d 
 |-  ( j = N -> ( ( M <_s j /\ ph ) <-> ( M <_s N /\ ta ) ) )
54 53 elrab 
 |-  ( N e. { j e. ZZ_s | ( M <_s j /\ ph ) } <-> ( N e. ZZ_s /\ ( M <_s N /\ ta ) ) )
55 49 51 54 3imtr3g 
 |-  ( M e. ZZ_s -> ( ( N e. ZZ_s /\ M <_s N ) -> ( N e. ZZ_s /\ ( M <_s N /\ ta ) ) ) )
56 55 3impib 
 |-  ( ( M e. ZZ_s /\ N e. ZZ_s /\ M <_s N ) -> ( N e. ZZ_s /\ ( M <_s N /\ ta ) ) )
57 56 simprrd 
 |-  ( ( M e. ZZ_s /\ N e. ZZ_s /\ M <_s N ) -> ta )