Metamath Proof Explorer

Theorem addhalfcut

Description: The cut of a surreal non-negative integer and its successor is the original number plus one half. Part of theorem 4.2 of Gonshor p. 30. (Contributed by Scott Fenton, 13-Aug-2025)

Ref Expression
Hypothesis addhalfcut.1 
|- ( ph -> A e. NN0_s )
Assertion addhalfcut 
|- ( ph -> ( { A } |s { ( A +s 1s ) } ) = ( A +s ( 1s /su 2s ) ) )

Proof

Step Hyp Ref Expression
1 addhalfcut.1 
 |-  ( ph -> A e. NN0_s )
2 1 n0snod 
 |-  ( ph -> A e. No )
3 1sno 
 |-  1s e. No
4 3 a1i 
 |-  ( ph -> 1s e. No )
5 2 4 addscld 
 |-  ( ph -> ( A +s 1s ) e. No )
6 2 sltp1d 
 |-  ( ph -> A
7 no2times 
 |-  ( A e. No -> ( 2s x.s A ) = ( A +s A ) )
8 2 7 syl 
 |-  ( ph -> ( 2s x.s A ) = ( A +s A ) )
9 8 oveq1d 
 |-  ( ph -> ( ( 2s x.s A ) +s 1s ) = ( ( A +s A ) +s 1s ) )
10 2 2 4 addsassd 
 |-  ( ph -> ( ( A +s A ) +s 1s ) = ( A +s ( A +s 1s ) ) )
11 9 10 eqtr2d 
 |-  ( ph -> ( A +s ( A +s 1s ) ) = ( ( 2s x.s A ) +s 1s ) )
12 2nns 
 |-  2s e. NN_s
13 nnn0s 
 |-  ( 2s e. NN_s -> 2s e. NN0_s )
14 12 13 ax-mp 
 |-  2s e. NN0_s
15 14 a1i 
 |-  ( ph -> 2s e. NN0_s )
16 n0mulscl 
 |-  ( ( 2s e. NN0_s /\ A e. NN0_s ) -> ( 2s x.s A ) e. NN0_s )
17 15 1 16 syl2anc 
 |-  ( ph -> ( 2s x.s A ) e. NN0_s )
18 1n0s 
 |-  1s e. NN0_s
19 18 a1i 
 |-  ( ph -> 1s e. NN0_s )
20 n0addscl 
 |-  ( ( ( 2s x.s A ) e. NN0_s /\ 1s e. NN0_s ) -> ( ( 2s x.s A ) +s 1s ) e. NN0_s )
21 17 19 20 syl2anc 
 |-  ( ph -> ( ( 2s x.s A ) +s 1s ) e. NN0_s )
22 n0scut 
 |-  ( ( ( 2s x.s A ) +s 1s ) e. NN0_s -> ( ( 2s x.s A ) +s 1s ) = ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s (/) ) )
23 21 22 syl 
 |-  ( ph -> ( ( 2s x.s A ) +s 1s ) = ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s (/) ) )
24 2sno 
 |-  2s e. No
25 24 a1i 
 |-  ( ph -> 2s e. No )
26 25 2 mulscld 
 |-  ( ph -> ( 2s x.s A ) e. No )
27 pncans 
 |-  ( ( ( 2s x.s A ) e. No /\ 1s e. No ) -> ( ( ( 2s x.s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) )
28 26 4 27 syl2anc 
 |-  ( ph -> ( ( ( 2s x.s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) )
29 28 sneqd 
 |-  ( ph -> { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } = { ( 2s x.s A ) } )
30 29 oveq1d 
 |-  ( ph -> ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s (/) ) = ( { ( 2s x.s A ) } |s (/) ) )
31 23 30 eqtrd 
 |-  ( ph -> ( ( 2s x.s A ) +s 1s ) = ( { ( 2s x.s A ) } |s (/) ) )
32 snelpwi 
 |-  ( ( 2s x.s A ) e. No -> { ( 2s x.s A ) } e. ~P No )
33 nulssgt 
 |-  ( { ( 2s x.s A ) } e. ~P No -> { ( 2s x.s A ) } <
34 26 32 33 3syl 
 |-  ( ph -> { ( 2s x.s A ) } <
35 slerflex 
 |-  ( ( 2s x.s A ) e. No -> ( 2s x.s A ) <_s ( 2s x.s A ) )
36 26 35 syl 
 |-  ( ph -> ( 2s x.s A ) <_s ( 2s x.s A ) )
37 ovex 
 |-  ( 2s x.s A ) e. _V
38 breq2 
 |-  ( y = ( 2s x.s A ) -> ( x <_s y <-> x <_s ( 2s x.s A ) ) )
39 37 38 rexsn 
 |-  ( E. y e. { ( 2s x.s A ) } x <_s y <-> x <_s ( 2s x.s A ) )
40 39 ralbii 
 |-  ( A. x e. { ( 2s x.s A ) } E. y e. { ( 2s x.s A ) } x <_s y <-> A. x e. { ( 2s x.s A ) } x <_s ( 2s x.s A ) )
41 breq1 
 |-  ( x = ( 2s x.s A ) -> ( x <_s ( 2s x.s A ) <-> ( 2s x.s A ) <_s ( 2s x.s A ) ) )
42 37 41 ralsn 
 |-  ( A. x e. { ( 2s x.s A ) } x <_s ( 2s x.s A ) <-> ( 2s x.s A ) <_s ( 2s x.s A ) )
43 40 42 bitri 
 |-  ( A. x e. { ( 2s x.s A ) } E. y e. { ( 2s x.s A ) } x <_s y <-> ( 2s x.s A ) <_s ( 2s x.s A ) )
44 36 43 sylibr 
 |-  ( ph -> A. x e. { ( 2s x.s A ) } E. y e. { ( 2s x.s A ) } x <_s y )
45 ral0 
 |-  A. x e. (/) E. y e. { ( 2s x.s ( A +s 1s ) ) } y <_s x
46 45 a1i 
 |-  ( ph -> A. x e. (/) E. y e. { ( 2s x.s ( A +s 1s ) ) } y <_s x )
47 26 4 addscld 
 |-  ( ph -> ( ( 2s x.s A ) +s 1s ) e. No )
48 26 sltp1d 
 |-  ( ph -> ( 2s x.s A )
49 26 47 48 ssltsn 
 |-  ( ph -> { ( 2s x.s A ) } <
50 31 sneqd 
 |-  ( ph -> { ( ( 2s x.s A ) +s 1s ) } = { ( { ( 2s x.s A ) } |s (/) ) } )
51 49 50 breqtrd 
 |-  ( ph -> { ( 2s x.s A ) } <
52 25 5 mulscld 
 |-  ( ph -> ( 2s x.s ( A +s 1s ) ) e. No )
53 4 sltp1d 
 |-  ( ph -> 1s
54 1p1e2s 
 |-  ( 1s +s 1s ) = 2s
55 53 54 breqtrdi 
 |-  ( ph -> 1s
56 4 25 26 sltadd2d 
 |-  ( ph -> ( 1s  ( ( 2s x.s A ) +s 1s )
57 55 56 mpbid 
 |-  ( ph -> ( ( 2s x.s A ) +s 1s )
58 25 2 4 addsdid 
 |-  ( ph -> ( 2s x.s ( A +s 1s ) ) = ( ( 2s x.s A ) +s ( 2s x.s 1s ) ) )
59 mulsrid 
 |-  ( 2s e. No -> ( 2s x.s 1s ) = 2s )
60 24 59 ax-mp 
 |-  ( 2s x.s 1s ) = 2s
61 60 oveq2i 
 |-  ( ( 2s x.s A ) +s ( 2s x.s 1s ) ) = ( ( 2s x.s A ) +s 2s )
62 58 61 eqtrdi 
 |-  ( ph -> ( 2s x.s ( A +s 1s ) ) = ( ( 2s x.s A ) +s 2s ) )
63 57 62 breqtrrd 
 |-  ( ph -> ( ( 2s x.s A ) +s 1s )
64 47 52 63 ssltsn 
 |-  ( ph -> { ( ( 2s x.s A ) +s 1s ) } <
65 50 64 eqbrtrrd 
 |-  ( ph -> { ( { ( 2s x.s A ) } |s (/) ) } <
66 34 44 46 51 65 cofcut1d 
 |-  ( ph -> ( { ( 2s x.s A ) } |s (/) ) = ( { ( 2s x.s A ) } |s { ( 2s x.s ( A +s 1s ) ) } ) )
67 11 31 66 3eqtrrd 
 |-  ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s ( A +s 1s ) ) } ) = ( A +s ( A +s 1s ) ) )
68 eqid 
 |-  ( { A } |s { ( A +s 1s ) } ) = ( { A } |s { ( A +s 1s ) } )
69 2 5 6 67 68 halfcut 
 |-  ( ph -> ( { A } |s { ( A +s 1s ) } ) = ( ( A +s ( A +s 1s ) ) /su 2s ) )
70 11 oveq1d 
 |-  ( ph -> ( ( A +s ( A +s 1s ) ) /su 2s ) = ( ( ( 2s x.s A ) +s 1s ) /su 2s ) )
71 2ne0s 
 |-  2s =/= 0s
72 71 a1i 
 |-  ( ph -> 2s =/= 0s )
73 26 4 25 72 divsdird 
 |-  ( ph -> ( ( ( 2s x.s A ) +s 1s ) /su 2s ) = ( ( ( 2s x.s A ) /su 2s ) +s ( 1s /su 2s ) ) )
74 2 25 72 divscan3d 
 |-  ( ph -> ( ( 2s x.s A ) /su 2s ) = A )
75 74 oveq1d 
 |-  ( ph -> ( ( ( 2s x.s A ) /su 2s ) +s ( 1s /su 2s ) ) = ( A +s ( 1s /su 2s ) ) )
76 73 75 eqtrd 
 |-  ( ph -> ( ( ( 2s x.s A ) +s 1s ) /su 2s ) = ( A +s ( 1s /su 2s ) ) )
77 69 70 76 3eqtrd 
 |-  ( ph -> ( { A } |s { ( A +s 1s ) } ) = ( A +s ( 1s /su 2s ) ) )