Metamath Proof Explorer

Theorem readdscl

Description: The surreal reals are closed under addition. Part of theorem 13(ii) of Conway p. 24. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Assertion readdscl 
|- ( ( A e. RR_s /\ B e. RR_s ) -> ( A +s B ) e. RR_s )

Proof

Step Hyp Ref Expression
1 addscl 
 |-  ( ( A e. No /\ B e. No ) -> ( A +s B ) e. No )
2 1 adantr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( E. n e. NN_s ( ( -us ` n )  ( A +s B ) e. No )
3 nnaddscl 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( n +s m ) e. NN_s )
4 3 adantr 
 |-  ( ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  ( n +s m ) e. NN_s )
5 4 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  ( n +s m ) e. NN_s )
6 simprll 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  n e. NN_s )
7 6 nnsnod 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  n e. No )
8 simprlr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  m e. NN_s )
9 8 nnsnod 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  m e. No )
10 negsdi 
 |-  ( ( n e. No /\ m e. No ) -> ( -us ` ( n +s m ) ) = ( ( -us ` n ) +s ( -us ` m ) ) )
11 7 9 10 syl2anc 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  ( -us ` ( n +s m ) ) = ( ( -us ` n ) +s ( -us ` m ) ) )
12 7 negscld 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  ( -us ` n ) e. No )
13 9 negscld 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  ( -us ` m ) e. No )
14 simpll 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  A e. No )
15 simplr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  B e. No )
16 simprll 
 |-  ( ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  ( -us ` n )
17 16 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  ( -us ` n )
18 simprrl 
 |-  ( ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  ( -us ` m )
19 18 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  ( -us ` m )
20 12 13 14 15 17 19 slt2addd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  ( ( -us ` n ) +s ( -us ` m ) )
21 11 20 eqbrtrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  ( -us ` ( n +s m ) )
22 simprlr 
 |-  ( ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  A
23 22 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  A
24 simprrr 
 |-  ( ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  B
25 24 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  B
26 14 15 7 9 23 25 slt2addd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  ( A +s B )
27 fveq2 
 |-  ( p = ( n +s m ) -> ( -us ` p ) = ( -us ` ( n +s m ) ) )
28 27 breq1d 
 |-  ( p = ( n +s m ) -> ( ( -us ` p )  ( -us ` ( n +s m ) )
29 breq2 
 |-  ( p = ( n +s m ) -> ( ( A +s B )  ( A +s B )
30 28 29 anbi12d 
 |-  ( p = ( n +s m ) -> ( ( ( -us ` p )  ( ( -us ` ( n +s m ) )
31 30 rspcev 
 |-  ( ( ( n +s m ) e. NN_s /\ ( ( -us ` ( n +s m ) )  E. p e. NN_s ( ( -us ` p )
32 5 21 26 31 syl12anc 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n )  E. p e. NN_s ( ( -us ` p )
33 32 expr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( n e. NN_s /\ m e. NN_s ) ) -> ( ( ( ( -us ` n )  E. p e. NN_s ( ( -us ` p )
34 33 rexlimdvva 
 |-  ( ( A e. No /\ B e. No ) -> ( E. n e. NN_s E. m e. NN_s ( ( ( -us ` n )  E. p e. NN_s ( ( -us ` p )
35 simpl 
 |-  ( ( E. n e. NN_s ( ( -us ` n )  E. n e. NN_s ( ( -us ` n )
36 simpl 
 |-  ( ( E. m e. NN_s ( ( -us ` m )  E. m e. NN_s ( ( -us ` m )
37 35 36 anim12i 
 |-  ( ( ( E. n e. NN_s ( ( -us ` n )  ( E. n e. NN_s ( ( -us ` n )
38 reeanv 
 |-  ( E. n e. NN_s E. m e. NN_s ( ( ( -us ` n )  ( E. n e. NN_s ( ( -us ` n )
39 37 38 sylibr 
 |-  ( ( ( E. n e. NN_s ( ( -us ` n )  E. n e. NN_s E. m e. NN_s ( ( ( -us ` n )
40 34 39 impel 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( E. n e. NN_s ( ( -us ` n )  E. p e. NN_s ( ( -us ` p )
41 simpr 
 |-  ( ( E. n e. NN_s ( ( -us ` n )  A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) )
42 simpr 
 |-  ( ( E. m e. NN_s ( ( -us ` m )  B = ( { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } |s { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } ) )
43 41 42 anim12i 
 |-  ( ( ( E. n e. NN_s ( ( -us ` n )  ( A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) /\ B = ( { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } |s { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } ) ) )
44 simpll 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) /\ B = ( { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } |s { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } ) ) ) -> A e. No )
45 recut 
 |-  ( A e. No -> { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } <
46 44 45 syl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) /\ B = ( { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } |s { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } ) ) ) -> { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } <
47 simplr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) /\ B = ( { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } |s { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } ) ) ) -> B e. No )
48 recut 
 |-  ( B e. No -> { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } <
49 47 48 syl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) /\ B = ( { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } |s { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } ) ) ) -> { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } <
50 simprl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) /\ B = ( { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } |s { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } ) ) ) -> A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) )
51 simprr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) /\ B = ( { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } |s { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } ) ) ) -> B = ( { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } |s { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } ) )
52 46 49 50 51 addsunif 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) /\ B = ( { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } |s { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } ) ) ) -> ( A +s B ) = ( ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } z = ( t +s B ) } u. { z | E. t e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( A +s t ) } ) |s ( { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } z = ( t +s B ) } u. { z | E. t e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( A +s t ) } ) ) )
53 ovex 
 |-  ( A -s ( 1s /su n ) ) e. _V
54 oveq1 
 |-  ( t = ( A -s ( 1s /su n ) ) -> ( t +s B ) = ( ( A -s ( 1s /su n ) ) +s B ) )
55 54 eqeq2d 
 |-  ( t = ( A -s ( 1s /su n ) ) -> ( z = ( t +s B ) <-> z = ( ( A -s ( 1s /su n ) ) +s B ) ) )
56 53 55 ceqsexv 
 |-  ( E. t ( t = ( A -s ( 1s /su n ) ) /\ z = ( t +s B ) ) <-> z = ( ( A -s ( 1s /su n ) ) +s B ) )
57 simpll 
 |-  ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> A e. No )
58 simplr 
 |-  ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> B e. No )
59 1sno 
 |-  1s e. No
60 59 a1i 
 |-  ( n e. NN_s -> 1s e. No )
61 nnsno 
 |-  ( n e. NN_s -> n e. No )
62 nnne0s 
 |-  ( n e. NN_s -> n =/= 0s )
63 60 61 62 divscld 
 |-  ( n e. NN_s -> ( 1s /su n ) e. No )
64 63 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( 1s /su n ) e. No )
65 57 58 64 addsubsd 
 |-  ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( ( A +s B ) -s ( 1s /su n ) ) = ( ( A -s ( 1s /su n ) ) +s B ) )
66 65 eqeq2d 
 |-  ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( z = ( ( A +s B ) -s ( 1s /su n ) ) <-> z = ( ( A -s ( 1s /su n ) ) +s B ) ) )
67 56 66 bitr4id 
 |-  ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( E. t ( t = ( A -s ( 1s /su n ) ) /\ z = ( t +s B ) ) <-> z = ( ( A +s B ) -s ( 1s /su n ) ) ) )
68 67 rexbidva 
 |-  ( ( A e. No /\ B e. No ) -> ( E. n e. NN_s E. t ( t = ( A -s ( 1s /su n ) ) /\ z = ( t +s B ) ) <-> E. n e. NN_s z = ( ( A +s B ) -s ( 1s /su n ) ) ) )
69 r19.41v 
 |-  ( E. n e. NN_s ( t = ( A -s ( 1s /su n ) ) /\ z = ( t +s B ) ) <-> ( E. n e. NN_s t = ( A -s ( 1s /su n ) ) /\ z = ( t +s B ) ) )
70 69 exbii 
 |-  ( E. t E. n e. NN_s ( t = ( A -s ( 1s /su n ) ) /\ z = ( t +s B ) ) <-> E. t ( E. n e. NN_s t = ( A -s ( 1s /su n ) ) /\ z = ( t +s B ) ) )
71 rexcom4 
 |-  ( E. n e. NN_s E. t ( t = ( A -s ( 1s /su n ) ) /\ z = ( t +s B ) ) <-> E. t E. n e. NN_s ( t = ( A -s ( 1s /su n ) ) /\ z = ( t +s B ) ) )
72 eqeq1 
 |-  ( x = t -> ( x = ( A -s ( 1s /su n ) ) <-> t = ( A -s ( 1s /su n ) ) ) )
73 72 rexbidv 
 |-  ( x = t -> ( E. n e. NN_s x = ( A -s ( 1s /su n ) ) <-> E. n e. NN_s t = ( A -s ( 1s /su n ) ) ) )
74 73 rexab 
 |-  ( E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } z = ( t +s B ) <-> E. t ( E. n e. NN_s t = ( A -s ( 1s /su n ) ) /\ z = ( t +s B ) ) )
75 70 71 74 3bitr4ri 
 |-  ( E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } z = ( t +s B ) <-> E. n e. NN_s E. t ( t = ( A -s ( 1s /su n ) ) /\ z = ( t +s B ) ) )
76 oveq2 
 |-  ( p = n -> ( 1s /su p ) = ( 1s /su n ) )
77 76 oveq2d 
 |-  ( p = n -> ( ( A +s B ) -s ( 1s /su p ) ) = ( ( A +s B ) -s ( 1s /su n ) ) )
78 77 eqeq2d 
 |-  ( p = n -> ( z = ( ( A +s B ) -s ( 1s /su p ) ) <-> z = ( ( A +s B ) -s ( 1s /su n ) ) ) )
79 78 cbvrexvw 
 |-  ( E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) <-> E. n e. NN_s z = ( ( A +s B ) -s ( 1s /su n ) ) )
80 68 75 79 3bitr4g 
 |-  ( ( A e. No /\ B e. No ) -> ( E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } z = ( t +s B ) <-> E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) ) )
81 80 abbidv 
 |-  ( ( A e. No /\ B e. No ) -> { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } z = ( t +s B ) } = { z | E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) } )
82 ovex 
 |-  ( B -s ( 1s /su m ) ) e. _V
83 oveq2 
 |-  ( t = ( B -s ( 1s /su m ) ) -> ( A +s t ) = ( A +s ( B -s ( 1s /su m ) ) ) )
84 83 eqeq2d 
 |-  ( t = ( B -s ( 1s /su m ) ) -> ( z = ( A +s t ) <-> z = ( A +s ( B -s ( 1s /su m ) ) ) ) )
85 82 84 ceqsexv 
 |-  ( E. t ( t = ( B -s ( 1s /su m ) ) /\ z = ( A +s t ) ) <-> z = ( A +s ( B -s ( 1s /su m ) ) ) )
86 simpll 
 |-  ( ( ( A e. No /\ B e. No ) /\ m e. NN_s ) -> A e. No )
87 simplr 
 |-  ( ( ( A e. No /\ B e. No ) /\ m e. NN_s ) -> B e. No )
88 59 a1i 
 |-  ( m e. NN_s -> 1s e. No )
89 nnsno 
 |-  ( m e. NN_s -> m e. No )
90 nnne0s 
 |-  ( m e. NN_s -> m =/= 0s )
91 88 89 90 divscld 
 |-  ( m e. NN_s -> ( 1s /su m ) e. No )
92 91 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ m e. NN_s ) -> ( 1s /su m ) e. No )
93 86 87 92 addsubsassd 
 |-  ( ( ( A e. No /\ B e. No ) /\ m e. NN_s ) -> ( ( A +s B ) -s ( 1s /su m ) ) = ( A +s ( B -s ( 1s /su m ) ) ) )
94 93 eqeq2d 
 |-  ( ( ( A e. No /\ B e. No ) /\ m e. NN_s ) -> ( z = ( ( A +s B ) -s ( 1s /su m ) ) <-> z = ( A +s ( B -s ( 1s /su m ) ) ) ) )
95 85 94 bitr4id 
 |-  ( ( ( A e. No /\ B e. No ) /\ m e. NN_s ) -> ( E. t ( t = ( B -s ( 1s /su m ) ) /\ z = ( A +s t ) ) <-> z = ( ( A +s B ) -s ( 1s /su m ) ) ) )
96 95 rexbidva 
 |-  ( ( A e. No /\ B e. No ) -> ( E. m e. NN_s E. t ( t = ( B -s ( 1s /su m ) ) /\ z = ( A +s t ) ) <-> E. m e. NN_s z = ( ( A +s B ) -s ( 1s /su m ) ) ) )
97 r19.41v 
 |-  ( E. m e. NN_s ( t = ( B -s ( 1s /su m ) ) /\ z = ( A +s t ) ) <-> ( E. m e. NN_s t = ( B -s ( 1s /su m ) ) /\ z = ( A +s t ) ) )
98 97 exbii 
 |-  ( E. t E. m e. NN_s ( t = ( B -s ( 1s /su m ) ) /\ z = ( A +s t ) ) <-> E. t ( E. m e. NN_s t = ( B -s ( 1s /su m ) ) /\ z = ( A +s t ) ) )
99 rexcom4 
 |-  ( E. m e. NN_s E. t ( t = ( B -s ( 1s /su m ) ) /\ z = ( A +s t ) ) <-> E. t E. m e. NN_s ( t = ( B -s ( 1s /su m ) ) /\ z = ( A +s t ) ) )
100 eqeq1 
 |-  ( y = t -> ( y = ( B -s ( 1s /su m ) ) <-> t = ( B -s ( 1s /su m ) ) ) )
101 100 rexbidv 
 |-  ( y = t -> ( E. m e. NN_s y = ( B -s ( 1s /su m ) ) <-> E. m e. NN_s t = ( B -s ( 1s /su m ) ) ) )
102 101 rexab 
 |-  ( E. t e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( A +s t ) <-> E. t ( E. m e. NN_s t = ( B -s ( 1s /su m ) ) /\ z = ( A +s t ) ) )
103 98 99 102 3bitr4ri 
 |-  ( E. t e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( A +s t ) <-> E. m e. NN_s E. t ( t = ( B -s ( 1s /su m ) ) /\ z = ( A +s t ) ) )
104 oveq2 
 |-  ( p = m -> ( 1s /su p ) = ( 1s /su m ) )
105 104 oveq2d 
 |-  ( p = m -> ( ( A +s B ) -s ( 1s /su p ) ) = ( ( A +s B ) -s ( 1s /su m ) ) )
106 105 eqeq2d 
 |-  ( p = m -> ( z = ( ( A +s B ) -s ( 1s /su p ) ) <-> z = ( ( A +s B ) -s ( 1s /su m ) ) ) )
107 106 cbvrexvw 
 |-  ( E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) <-> E. m e. NN_s z = ( ( A +s B ) -s ( 1s /su m ) ) )
108 96 103 107 3bitr4g 
 |-  ( ( A e. No /\ B e. No ) -> ( E. t e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( A +s t ) <-> E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) ) )
109 108 abbidv 
 |-  ( ( A e. No /\ B e. No ) -> { z | E. t e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( A +s t ) } = { z | E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) } )
110 81 109 uneq12d 
 |-  ( ( A e. No /\ B e. No ) -> ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } z = ( t +s B ) } u. { z | E. t e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( A +s t ) } ) = ( { z | E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) } u. { z | E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) } ) )
111 unidm 
 |-  ( { z | E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) } u. { z | E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) } ) = { z | E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) }
112 110 111 eqtrdi 
 |-  ( ( A e. No /\ B e. No ) -> ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } z = ( t +s B ) } u. { z | E. t e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( A +s t ) } ) = { z | E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) } )
113 ovex 
 |-  ( A +s ( 1s /su n ) ) e. _V
114 oveq1 
 |-  ( t = ( A +s ( 1s /su n ) ) -> ( t +s B ) = ( ( A +s ( 1s /su n ) ) +s B ) )
115 114 eqeq2d 
 |-  ( t = ( A +s ( 1s /su n ) ) -> ( z = ( t +s B ) <-> z = ( ( A +s ( 1s /su n ) ) +s B ) ) )
116 113 115 ceqsexv 
 |-  ( E. t ( t = ( A +s ( 1s /su n ) ) /\ z = ( t +s B ) ) <-> z = ( ( A +s ( 1s /su n ) ) +s B ) )
117 57 64 58 adds32d 
 |-  ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( ( A +s ( 1s /su n ) ) +s B ) = ( ( A +s B ) +s ( 1s /su n ) ) )
118 117 eqeq2d 
 |-  ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( z = ( ( A +s ( 1s /su n ) ) +s B ) <-> z = ( ( A +s B ) +s ( 1s /su n ) ) ) )
119 116 118 bitrid 
 |-  ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( E. t ( t = ( A +s ( 1s /su n ) ) /\ z = ( t +s B ) ) <-> z = ( ( A +s B ) +s ( 1s /su n ) ) ) )
120 119 rexbidva 
 |-  ( ( A e. No /\ B e. No ) -> ( E. n e. NN_s E. t ( t = ( A +s ( 1s /su n ) ) /\ z = ( t +s B ) ) <-> E. n e. NN_s z = ( ( A +s B ) +s ( 1s /su n ) ) ) )
121 r19.41v 
 |-  ( E. n e. NN_s ( t = ( A +s ( 1s /su n ) ) /\ z = ( t +s B ) ) <-> ( E. n e. NN_s t = ( A +s ( 1s /su n ) ) /\ z = ( t +s B ) ) )
122 121 exbii 
 |-  ( E. t E. n e. NN_s ( t = ( A +s ( 1s /su n ) ) /\ z = ( t +s B ) ) <-> E. t ( E. n e. NN_s t = ( A +s ( 1s /su n ) ) /\ z = ( t +s B ) ) )
123 rexcom4 
 |-  ( E. n e. NN_s E. t ( t = ( A +s ( 1s /su n ) ) /\ z = ( t +s B ) ) <-> E. t E. n e. NN_s ( t = ( A +s ( 1s /su n ) ) /\ z = ( t +s B ) ) )
124 eqeq1 
 |-  ( x = t -> ( x = ( A +s ( 1s /su n ) ) <-> t = ( A +s ( 1s /su n ) ) ) )
125 124 rexbidv 
 |-  ( x = t -> ( E. n e. NN_s x = ( A +s ( 1s /su n ) ) <-> E. n e. NN_s t = ( A +s ( 1s /su n ) ) ) )
126 125 rexab 
 |-  ( E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } z = ( t +s B ) <-> E. t ( E. n e. NN_s t = ( A +s ( 1s /su n ) ) /\ z = ( t +s B ) ) )
127 122 123 126 3bitr4ri 
 |-  ( E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } z = ( t +s B ) <-> E. n e. NN_s E. t ( t = ( A +s ( 1s /su n ) ) /\ z = ( t +s B ) ) )
128 76 oveq2d 
 |-  ( p = n -> ( ( A +s B ) +s ( 1s /su p ) ) = ( ( A +s B ) +s ( 1s /su n ) ) )
129 128 eqeq2d 
 |-  ( p = n -> ( z = ( ( A +s B ) +s ( 1s /su p ) ) <-> z = ( ( A +s B ) +s ( 1s /su n ) ) ) )
130 129 cbvrexvw 
 |-  ( E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) <-> E. n e. NN_s z = ( ( A +s B ) +s ( 1s /su n ) ) )
131 120 127 130 3bitr4g 
 |-  ( ( A e. No /\ B e. No ) -> ( E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } z = ( t +s B ) <-> E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) ) )
132 131 abbidv 
 |-  ( ( A e. No /\ B e. No ) -> { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } z = ( t +s B ) } = { z | E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) } )
133 ovex 
 |-  ( B +s ( 1s /su m ) ) e. _V
134 oveq2 
 |-  ( t = ( B +s ( 1s /su m ) ) -> ( A +s t ) = ( A +s ( B +s ( 1s /su m ) ) ) )
135 134 eqeq2d 
 |-  ( t = ( B +s ( 1s /su m ) ) -> ( z = ( A +s t ) <-> z = ( A +s ( B +s ( 1s /su m ) ) ) ) )
136 133 135 ceqsexv 
 |-  ( E. t ( t = ( B +s ( 1s /su m ) ) /\ z = ( A +s t ) ) <-> z = ( A +s ( B +s ( 1s /su m ) ) ) )
137 86 87 92 addsassd 
 |-  ( ( ( A e. No /\ B e. No ) /\ m e. NN_s ) -> ( ( A +s B ) +s ( 1s /su m ) ) = ( A +s ( B +s ( 1s /su m ) ) ) )
138 137 eqeq2d 
 |-  ( ( ( A e. No /\ B e. No ) /\ m e. NN_s ) -> ( z = ( ( A +s B ) +s ( 1s /su m ) ) <-> z = ( A +s ( B +s ( 1s /su m ) ) ) ) )
139 136 138 bitr4id 
 |-  ( ( ( A e. No /\ B e. No ) /\ m e. NN_s ) -> ( E. t ( t = ( B +s ( 1s /su m ) ) /\ z = ( A +s t ) ) <-> z = ( ( A +s B ) +s ( 1s /su m ) ) ) )
140 139 rexbidva 
 |-  ( ( A e. No /\ B e. No ) -> ( E. m e. NN_s E. t ( t = ( B +s ( 1s /su m ) ) /\ z = ( A +s t ) ) <-> E. m e. NN_s z = ( ( A +s B ) +s ( 1s /su m ) ) ) )
141 r19.41v 
 |-  ( E. m e. NN_s ( t = ( B +s ( 1s /su m ) ) /\ z = ( A +s t ) ) <-> ( E. m e. NN_s t = ( B +s ( 1s /su m ) ) /\ z = ( A +s t ) ) )
142 141 exbii 
 |-  ( E. t E. m e. NN_s ( t = ( B +s ( 1s /su m ) ) /\ z = ( A +s t ) ) <-> E. t ( E. m e. NN_s t = ( B +s ( 1s /su m ) ) /\ z = ( A +s t ) ) )
143 rexcom4 
 |-  ( E. m e. NN_s E. t ( t = ( B +s ( 1s /su m ) ) /\ z = ( A +s t ) ) <-> E. t E. m e. NN_s ( t = ( B +s ( 1s /su m ) ) /\ z = ( A +s t ) ) )
144 eqeq1 
 |-  ( y = t -> ( y = ( B +s ( 1s /su m ) ) <-> t = ( B +s ( 1s /su m ) ) ) )
145 144 rexbidv 
 |-  ( y = t -> ( E. m e. NN_s y = ( B +s ( 1s /su m ) ) <-> E. m e. NN_s t = ( B +s ( 1s /su m ) ) ) )
146 145 rexab 
 |-  ( E. t e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( A +s t ) <-> E. t ( E. m e. NN_s t = ( B +s ( 1s /su m ) ) /\ z = ( A +s t ) ) )
147 142 143 146 3bitr4ri 
 |-  ( E. t e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( A +s t ) <-> E. m e. NN_s E. t ( t = ( B +s ( 1s /su m ) ) /\ z = ( A +s t ) ) )
148 104 oveq2d 
 |-  ( p = m -> ( ( A +s B ) +s ( 1s /su p ) ) = ( ( A +s B ) +s ( 1s /su m ) ) )
149 148 eqeq2d 
 |-  ( p = m -> ( z = ( ( A +s B ) +s ( 1s /su p ) ) <-> z = ( ( A +s B ) +s ( 1s /su m ) ) ) )
150 149 cbvrexvw 
 |-  ( E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) <-> E. m e. NN_s z = ( ( A +s B ) +s ( 1s /su m ) ) )
151 140 147 150 3bitr4g 
 |-  ( ( A e. No /\ B e. No ) -> ( E. t e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( A +s t ) <-> E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) ) )
152 151 abbidv 
 |-  ( ( A e. No /\ B e. No ) -> { z | E. t e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( A +s t ) } = { z | E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) } )
153 132 152 uneq12d 
 |-  ( ( A e. No /\ B e. No ) -> ( { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } z = ( t +s B ) } u. { z | E. t e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( A +s t ) } ) = ( { z | E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) } u. { z | E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) } ) )
154 unidm 
 |-  ( { z | E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) } u. { z | E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) } ) = { z | E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) }
155 153 154 eqtrdi 
 |-  ( ( A e. No /\ B e. No ) -> ( { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } z = ( t +s B ) } u. { z | E. t e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( A +s t ) } ) = { z | E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) } )
156 112 155 oveq12d 
 |-  ( ( A e. No /\ B e. No ) -> ( ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } z = ( t +s B ) } u. { z | E. t e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( A +s t ) } ) |s ( { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } z = ( t +s B ) } u. { z | E. t e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( A +s t ) } ) ) = ( { z | E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) } |s { z | E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) } ) )
157 156 adantr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) /\ B = ( { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } |s { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } ) ) ) -> ( ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } z = ( t +s B ) } u. { z | E. t e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( A +s t ) } ) |s ( { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } z = ( t +s B ) } u. { z | E. t e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( A +s t ) } ) ) = ( { z | E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) } |s { z | E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) } ) )
158 52 157 eqtrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) /\ B = ( { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } |s { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } ) ) ) -> ( A +s B ) = ( { z | E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) } |s { z | E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) } ) )
159 43 158 sylan2 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( E. n e. NN_s ( ( -us ` n )  ( A +s B ) = ( { z | E. p e. NN_s z = ( ( A +s B ) -s ( 1s /su p ) ) } |s { z | E. p e. NN_s z = ( ( A +s B ) +s ( 1s /su p ) ) } ) )
160 2 40 159 jca32 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( E. n e. NN_s ( ( -us ` n )  ( ( A +s B ) e. No /\ ( E. p e. NN_s ( ( -us ` p )
161 160 an4s 
 |-  ( ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )  ( ( A +s B ) e. No /\ ( E. p e. NN_s ( ( -us ` p )
162 elreno 
 |-  ( A e. RR_s <-> ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )
163 elreno 
 |-  ( B e. RR_s <-> ( B e. No /\ ( E. m e. NN_s ( ( -us ` m )
164 162 163 anbi12i 
 |-  ( ( A e. RR_s /\ B e. RR_s ) <-> ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )
165 elreno 
 |-  ( ( A +s B ) e. RR_s <-> ( ( A +s B ) e. No /\ ( E. p e. NN_s ( ( -us ` p )
166 161 164 165 3imtr4i 
 |-  ( ( A e. RR_s /\ B e. RR_s ) -> ( A +s B ) e. RR_s )