Theorem remulscl

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

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

Proof

Step	Hyp	Ref	Expression
1		mulscl	|- ( ( A e. No /\ B e. No ) -> ( A x.s B ) e. No )
2	1	adantr	|- ( ( ( A e. No /\ B e. No ) /\ ( ( E. n e. NN_s ( ( -us ` n ) ( A x.s B ) e. No )
3		remulscllem2	|- ( ( ( A e. No /\ B e. No ) /\ ( ( n e. NN_s /\ m e. NN_s ) /\ ( ( ( -us ` n ) E. p e. NN_s ( ( -us ` p )
4	3	expr	|- ( ( ( A e. No /\ B e. No ) /\ ( n e. NN_s /\ m e. NN_s ) ) -> ( ( ( ( -us ` n ) E. p e. NN_s ( ( -us ` p )
5	4	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 )
6		simpl	|- ( ( E. n e. NN_s ( ( -us ` n ) E. n e. NN_s ( ( -us ` n )
7		simpl	|- ( ( E. m e. NN_s ( ( -us ` m ) E. m e. NN_s ( ( -us ` m )
8	6 7	anim12i	|- ( ( ( E. n e. NN_s ( ( -us ` n ) ( E. n e. NN_s ( ( -us ` n )
9		reeanv	|- ( E. n e. NN_s E. m e. NN_s ( ( ( -us ` n ) ( E. n e. NN_s ( ( -us ` n )
10	8 9	sylibr	|- ( ( ( E. n e. NN_s ( ( -us ` n ) E. n e. NN_s E. m e. NN_s ( ( ( -us ` n )
11	5 10	impel	|- ( ( ( A e. No /\ B e. No ) /\ ( ( E. n e. NN_s ( ( -us ` n ) E. p e. NN_s ( ( -us ` p )
12		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 ) ) } ) )
13		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 ) ) } ) )
14	12 13	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 ) ) } ) ) )
15		recut	|- ( A e. No -> { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } <
16	15	adantr	|- ( ( A e. No /\ B e. No ) -> { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } <
17	16	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 ) ) } ) ) ) -> { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } <
18		recut	|- ( B e. No -> { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } <
19	18	ad2antlr	|- ( ( ( 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 ) ) } <
20		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 ) ) } ) )
21		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 ) ) } ) )
22	17 19 20 21	mulsunif2	|- ( ( ( 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.s B ) = ( ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) } u. { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) } ) |s ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) } u. { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) } ) ) )
23		r19.41v	|- ( E. n e. NN_s ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) <-> ( E. n e. NN_s t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) )
24	23	exbii	|- ( E. t E. n e. NN_s ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) <-> E. t ( E. n e. NN_s t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) )
25		rexcom4	|- ( E. n e. NN_s E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) <-> E. t E. n e. NN_s ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) )
26		eqeq1	|- ( x = t -> ( x = ( A -s ( 1s /su n ) ) <-> t = ( A -s ( 1s /su n ) ) ) )
27	26	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 ) ) ) )
28	27	rexab	|- ( E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) <-> E. t ( E. n e. NN_s t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) )
29	24 25 28	3bitr4ri	|- ( E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) <-> E. n e. NN_s E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) )
30		ovex	|- ( A -s ( 1s /su n ) ) e. _V
31		oveq2	|- ( t = ( A -s ( 1s /su n ) ) -> ( A -s t ) = ( A -s ( A -s ( 1s /su n ) ) ) )
32	31	oveq1d	|- ( t = ( A -s ( 1s /su n ) ) -> ( ( A -s t ) x.s ( B -s u ) ) = ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) )
33	32	oveq2d	|- ( t = ( A -s ( 1s /su n ) ) -> ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) )
34	33	eqeq2d	|- ( t = ( A -s ( 1s /su n ) ) -> ( z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) <-> z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) )
35	34	rexbidv	|- ( t = ( A -s ( 1s /su n ) ) -> ( E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) <-> E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) )
36	30 35	ceqsexv	|- ( E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) <-> E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) )
37		r19.41v	|- ( E. m e. NN_s ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) <-> ( E. m e. NN_s u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) )
38	37	exbii	|- ( E. u E. m e. NN_s ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) <-> E. u ( E. m e. NN_s u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) )
39		rexcom4	|- ( E. m e. NN_s E. u ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) <-> E. u E. m e. NN_s ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) )
40		eqeq1	|- ( y = u -> ( y = ( B -s ( 1s /su m ) ) <-> u = ( B -s ( 1s /su m ) ) ) )
41	40	rexbidv	|- ( y = u -> ( E. m e. NN_s y = ( B -s ( 1s /su m ) ) <-> E. m e. NN_s u = ( B -s ( 1s /su m ) ) ) )
42	41	rexab	|- ( E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) <-> E. u ( E. m e. NN_s u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) )
43	38 39 42	3bitr4ri	|- ( E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) <-> E. m e. NN_s E. u ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) )
44	36 43	bitri	|- ( E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) <-> E. m e. NN_s E. u ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) )
45		ovex	|- ( B -s ( 1s /su m ) ) e. _V
46		oveq2	|- ( u = ( B -s ( 1s /su m ) ) -> ( B -s u ) = ( B -s ( B -s ( 1s /su m ) ) ) )
47	46	oveq2d	|- ( u = ( B -s ( 1s /su m ) ) -> ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) = ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) )
48	47	oveq2d	|- ( u = ( B -s ( 1s /su m ) ) -> ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) ) )
49	48	eqeq2d	|- ( u = ( B -s ( 1s /su m ) ) -> ( z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) <-> z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) ) ) )
50	45 49	ceqsexv	|- ( E. u ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) <-> z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) ) )
51		simplll	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> A e. No )
52		1sno	|- 1s e. No
53	52	a1i	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> 1s e. No )
54		nnsno	|- ( n e. NN_s -> n e. No )
55	54	ad2antlr	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> n e. No )
56		nnne0s	|- ( n e. NN_s -> n =/= 0s )
57	56	ad2antlr	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> n =/= 0s )
58	53 55 57	divscld	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( 1s /su n ) e. No )
59	51 58	nncansd	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( A -s ( A -s ( 1s /su n ) ) ) = ( 1s /su n ) )
60		simpllr	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> B e. No )
61		nnsno	|- ( m e. NN_s -> m e. No )
62	61	adantl	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> m e. No )
63		nnne0s	|- ( m e. NN_s -> m =/= 0s )
64	63	adantl	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> m =/= 0s )
65	53 62 64	divscld	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( 1s /su m ) e. No )
66	60 65	nncansd	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( B -s ( B -s ( 1s /su m ) ) ) = ( 1s /su m ) )
67	59 66	oveq12d	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) = ( ( 1s /su n ) x.s ( 1s /su m ) ) )
68	67	oveq2d	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) ) = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) )
69	68	eqeq2d	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) ) <-> z = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
70	50 69	bitrid	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( E. u ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) <-> z = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
71	70	rexbidva	|- ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( E. m e. NN_s E. u ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( B -s u ) ) ) ) <-> E. m e. NN_s z = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
72	44 71	bitrid	|- ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) <-> E. m e. NN_s z = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
73	72	rexbidva	|- ( ( A e. No /\ B e. No ) -> ( E. n e. NN_s E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) <-> E. n e. NN_s E. m e. NN_s z = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
74		remulscllem1	|- ( E. n e. NN_s E. m e. NN_s z = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) <-> E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) )
75	73 74	bitrdi	|- ( ( A e. No /\ B e. No ) -> ( E. n e. NN_s E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) ) <-> E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) ) )
76	29 75	bitrid	|- ( ( A e. No /\ B e. No ) -> ( E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) <-> E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) ) )
77	76	abbidv	|- ( ( A e. No /\ B e. No ) -> { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) } = { z | E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) } )
78		r19.41v	|- ( E. n e. NN_s ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) <-> ( E. n e. NN_s t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) )
79	78	exbii	|- ( E. t E. n e. NN_s ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) <-> E. t ( E. n e. NN_s t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) )
80		rexcom4	|- ( E. n e. NN_s E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) <-> E. t E. n e. NN_s ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) )
81		eqeq1	|- ( x = t -> ( x = ( A +s ( 1s /su n ) ) <-> t = ( A +s ( 1s /su n ) ) ) )
82	81	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 ) ) ) )
83	82	rexab	|- ( E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) <-> E. t ( E. n e. NN_s t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) )
84	79 80 83	3bitr4ri	|- ( E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) <-> E. n e. NN_s E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) )
85		ovex	|- ( A +s ( 1s /su n ) ) e. _V
86		oveq1	|- ( t = ( A +s ( 1s /su n ) ) -> ( t -s A ) = ( ( A +s ( 1s /su n ) ) -s A ) )
87	86	oveq1d	|- ( t = ( A +s ( 1s /su n ) ) -> ( ( t -s A ) x.s ( u -s B ) ) = ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) )
88	87	oveq2d	|- ( t = ( A +s ( 1s /su n ) ) -> ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) )
89	88	eqeq2d	|- ( t = ( A +s ( 1s /su n ) ) -> ( z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) <-> z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) )
90	89	rexbidv	|- ( t = ( A +s ( 1s /su n ) ) -> ( E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) <-> E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) )
91	85 90	ceqsexv	|- ( E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) <-> E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) )
92		r19.41v	|- ( E. m e. NN_s ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) <-> ( E. m e. NN_s u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) )
93	92	exbii	|- ( E. u E. m e. NN_s ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) <-> E. u ( E. m e. NN_s u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) )
94		rexcom4	|- ( E. m e. NN_s E. u ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) <-> E. u E. m e. NN_s ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) )
95		eqeq1	|- ( y = u -> ( y = ( B +s ( 1s /su m ) ) <-> u = ( B +s ( 1s /su m ) ) ) )
96	95	rexbidv	|- ( y = u -> ( E. m e. NN_s y = ( B +s ( 1s /su m ) ) <-> E. m e. NN_s u = ( B +s ( 1s /su m ) ) ) )
97	96	rexab	|- ( E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) <-> E. u ( E. m e. NN_s u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) )
98	93 94 97	3bitr4ri	|- ( E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) <-> E. m e. NN_s E. u ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) )
99	91 98	bitri	|- ( E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) <-> E. m e. NN_s E. u ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) )
100		ovex	|- ( B +s ( 1s /su m ) ) e. _V
101		oveq1	|- ( u = ( B +s ( 1s /su m ) ) -> ( u -s B ) = ( ( B +s ( 1s /su m ) ) -s B ) )
102	101	oveq2d	|- ( u = ( B +s ( 1s /su m ) ) -> ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) = ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) )
103	102	oveq2d	|- ( u = ( B +s ( 1s /su m ) ) -> ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) ) )
104	103	eqeq2d	|- ( u = ( B +s ( 1s /su m ) ) -> ( z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) <-> z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) ) ) )
105	100 104	ceqsexv	|- ( E. u ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) <-> z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) ) )
106		pncan2s	|- ( ( A e. No /\ ( 1s /su n ) e. No ) -> ( ( A +s ( 1s /su n ) ) -s A ) = ( 1s /su n ) )
107	51 58 106	syl2anc	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( ( A +s ( 1s /su n ) ) -s A ) = ( 1s /su n ) )
108		pncan2s	|- ( ( B e. No /\ ( 1s /su m ) e. No ) -> ( ( B +s ( 1s /su m ) ) -s B ) = ( 1s /su m ) )
109	60 65 108	syl2anc	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( ( B +s ( 1s /su m ) ) -s B ) = ( 1s /su m ) )
110	107 109	oveq12d	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) = ( ( 1s /su n ) x.s ( 1s /su m ) ) )
111	110	oveq2d	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) ) = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) )
112	111	eqeq2d	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) ) <-> z = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
113	105 112	bitrid	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( E. u ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) <-> z = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
114	113	rexbidva	|- ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( E. m e. NN_s E. u ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) -s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( u -s B ) ) ) ) <-> E. m e. NN_s z = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
115	99 114	bitrid	|- ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) <-> E. m e. NN_s z = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
116	115	rexbidva	|- ( ( A e. No /\ B e. No ) -> ( E. n e. NN_s E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) <-> E. n e. NN_s E. m e. NN_s z = ( ( A x.s B ) -s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
117	116 74	bitrdi	|- ( ( A e. No /\ B e. No ) -> ( E. n e. NN_s E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) ) <-> E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) ) )
118	84 117	bitrid	|- ( ( A e. No /\ B e. No ) -> ( E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) <-> E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) ) )
119	118	abbidv	|- ( ( A e. No /\ B e. No ) -> { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) } = { z | E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) } )
120	77 119	uneq12d	|- ( ( A e. No /\ B e. No ) -> ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) } u. { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) } ) = ( { z | E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) } u. { z | E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) } ) )
121		unidm	|- ( { z | E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) } u. { z | E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) } ) = { z | E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) }
122	120 121	eqtrdi	|- ( ( A e. No /\ B e. No ) -> ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) } u. { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) } ) = { z | E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) } )
123		r19.41v	|- ( E. n e. NN_s ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) <-> ( E. n e. NN_s t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) )
124	123	exbii	|- ( E. t E. n e. NN_s ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) <-> E. t ( E. n e. NN_s t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) )
125		rexcom4	|- ( E. n e. NN_s E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) <-> E. t E. n e. NN_s ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) )
126	27	rexab	|- ( E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) <-> E. t ( E. n e. NN_s t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) )
127	124 125 126	3bitr4ri	|- ( E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) <-> E. n e. NN_s E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) )
128	31	oveq1d	|- ( t = ( A -s ( 1s /su n ) ) -> ( ( A -s t ) x.s ( u -s B ) ) = ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) )
129	128	oveq2d	|- ( t = ( A -s ( 1s /su n ) ) -> ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) )
130	129	eqeq2d	|- ( t = ( A -s ( 1s /su n ) ) -> ( z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) <-> z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) )
131	130	rexbidv	|- ( t = ( A -s ( 1s /su n ) ) -> ( E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) <-> E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) )
132	30 131	ceqsexv	|- ( E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) <-> E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) )
133		r19.41v	|- ( E. m e. NN_s ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) <-> ( E. m e. NN_s u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) )
134	133	exbii	|- ( E. u E. m e. NN_s ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) <-> E. u ( E. m e. NN_s u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) )
135		rexcom4	|- ( E. m e. NN_s E. u ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) <-> E. u E. m e. NN_s ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) )
136	96	rexab	|- ( E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) <-> E. u ( E. m e. NN_s u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) )
137	134 135 136	3bitr4ri	|- ( E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) <-> E. m e. NN_s E. u ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) )
138	132 137	bitri	|- ( E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) <-> E. m e. NN_s E. u ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) )
139	101	oveq2d	|- ( u = ( B +s ( 1s /su m ) ) -> ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) = ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) )
140	139	oveq2d	|- ( u = ( B +s ( 1s /su m ) ) -> ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) ) )
141	140	eqeq2d	|- ( u = ( B +s ( 1s /su m ) ) -> ( z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) <-> z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) ) ) )
142	100 141	ceqsexv	|- ( E. u ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) <-> z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) ) )
143	59 109	oveq12d	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) = ( ( 1s /su n ) x.s ( 1s /su m ) ) )
144	143	oveq2d	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) ) = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) )
145	144	eqeq2d	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( ( B +s ( 1s /su m ) ) -s B ) ) ) <-> z = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
146	142 145	bitrid	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( E. u ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) <-> z = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
147	146	rexbidva	|- ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( E. m e. NN_s E. u ( u = ( B +s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( A -s ( A -s ( 1s /su n ) ) ) x.s ( u -s B ) ) ) ) <-> E. m e. NN_s z = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
148	138 147	bitrid	|- ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) <-> E. m e. NN_s z = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
149	148	rexbidva	|- ( ( A e. No /\ B e. No ) -> ( E. n e. NN_s E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) <-> E. n e. NN_s E. m e. NN_s z = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
150		remulscllem1	|- ( E. n e. NN_s E. m e. NN_s z = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) <-> E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) )
151	149 150	bitrdi	|- ( ( A e. No /\ B e. No ) -> ( E. n e. NN_s E. t ( t = ( A -s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) <-> E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) ) )
152	127 151	bitrid	|- ( ( A e. No /\ B e. No ) -> ( E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) <-> E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) ) )
153	152	abbidv	|- ( ( A e. No /\ B e. No ) -> { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) } = { z | E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) } )
154		r19.41v	|- ( E. n e. NN_s ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) <-> ( E. n e. NN_s t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) )
155	154	exbii	|- ( E. t E. n e. NN_s ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) <-> E. t ( E. n e. NN_s t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) )
156		rexcom4	|- ( E. n e. NN_s E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) <-> E. t E. n e. NN_s ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) )
157	82	rexab	|- ( E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) <-> E. t ( E. n e. NN_s t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) )
158	155 156 157	3bitr4ri	|- ( E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) <-> E. n e. NN_s E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) )
159	86	oveq1d	|- ( t = ( A +s ( 1s /su n ) ) -> ( ( t -s A ) x.s ( B -s u ) ) = ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) )
160	159	oveq2d	|- ( t = ( A +s ( 1s /su n ) ) -> ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) )
161	160	eqeq2d	|- ( t = ( A +s ( 1s /su n ) ) -> ( z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) <-> z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) )
162	161	rexbidv	|- ( t = ( A +s ( 1s /su n ) ) -> ( E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) <-> E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) )
163	85 162	ceqsexv	|- ( E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) <-> E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) )
164		r19.41v	|- ( E. m e. NN_s ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) <-> ( E. m e. NN_s u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) )
165	164	exbii	|- ( E. u E. m e. NN_s ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) <-> E. u ( E. m e. NN_s u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) )
166		rexcom4	|- ( E. m e. NN_s E. u ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) <-> E. u E. m e. NN_s ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) )
167	41	rexab	|- ( E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) <-> E. u ( E. m e. NN_s u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) )
168	165 166 167	3bitr4ri	|- ( E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) <-> E. m e. NN_s E. u ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) )
169	163 168	bitri	|- ( E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) <-> E. m e. NN_s E. u ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) )
170	46	oveq2d	|- ( u = ( B -s ( 1s /su m ) ) -> ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) = ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) )
171	170	oveq2d	|- ( u = ( B -s ( 1s /su m ) ) -> ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) ) )
172	171	eqeq2d	|- ( u = ( B -s ( 1s /su m ) ) -> ( z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) <-> z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) ) ) )
173	45 172	ceqsexv	|- ( E. u ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) <-> z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) ) )
174	107 66	oveq12d	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) = ( ( 1s /su n ) x.s ( 1s /su m ) ) )
175	174	oveq2d	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) ) = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) )
176	175	eqeq2d	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s ( B -s ( 1s /su m ) ) ) ) ) <-> z = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
177	173 176	bitrid	|- ( ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) /\ m e. NN_s ) -> ( E. u ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) <-> z = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
178	177	rexbidva	|- ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( E. m e. NN_s E. u ( u = ( B -s ( 1s /su m ) ) /\ z = ( ( A x.s B ) +s ( ( ( A +s ( 1s /su n ) ) -s A ) x.s ( B -s u ) ) ) ) <-> E. m e. NN_s z = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
179	169 178	bitrid	|- ( ( ( A e. No /\ B e. No ) /\ n e. NN_s ) -> ( E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) <-> E. m e. NN_s z = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
180	179	rexbidva	|- ( ( A e. No /\ B e. No ) -> ( E. n e. NN_s E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) <-> E. n e. NN_s E. m e. NN_s z = ( ( A x.s B ) +s ( ( 1s /su n ) x.s ( 1s /su m ) ) ) ) )
181	180 150	bitrdi	|- ( ( A e. No /\ B e. No ) -> ( E. n e. NN_s E. t ( t = ( A +s ( 1s /su n ) ) /\ E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) ) <-> E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) ) )
182	158 181	bitrid	|- ( ( A e. No /\ B e. No ) -> ( E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) <-> E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) ) )
183	182	abbidv	|- ( ( A e. No /\ B e. No ) -> { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) } = { z | E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) } )
184	153 183	uneq12d	|- ( ( A e. No /\ B e. No ) -> ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) } u. { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) } ) = ( { z | E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) } u. { z | E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) } ) )
185		unidm	|- ( { z | E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) } u. { z | E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) } ) = { z | E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) }
186	184 185	eqtrdi	|- ( ( A e. No /\ B e. No ) -> ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) } u. { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) } ) = { z | E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) } )
187	122 186	oveq12d	|- ( ( A e. No /\ B e. No ) -> ( ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) } u. { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) } ) |s ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) } u. { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) } ) ) = ( { z | E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) } |s { z | E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) } ) )
188	187	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 ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( A -s t ) x.s ( B -s u ) ) ) } u. { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) -s ( ( t -s A ) x.s ( u -s B ) ) ) } ) |s ( { z | E. t e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B +s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) } u. { z | E. t e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } E. u e. { y | E. m e. NN_s y = ( B -s ( 1s /su m ) ) } z = ( ( A x.s B ) +s ( ( t -s A ) x.s ( B -s u ) ) ) } ) ) = ( { z | E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) } |s { z | E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) } ) )
189	22 188	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 x.s B ) = ( { z | E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) } |s { z | E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) } ) )
190	14 189	sylan2	|- ( ( ( A e. No /\ B e. No ) /\ ( ( E. n e. NN_s ( ( -us ` n ) ( A x.s B ) = ( { z | E. p e. NN_s z = ( ( A x.s B ) -s ( 1s /su p ) ) } |s { z | E. p e. NN_s z = ( ( A x.s B ) +s ( 1s /su p ) ) } ) )
191	2 11 190	jca32	|- ( ( ( A e. No /\ B e. No ) /\ ( ( E. n e. NN_s ( ( -us ` n ) ( ( A x.s B ) e. No /\ ( E. p e. NN_s ( ( -us ` p )
192	191	an4s	|- ( ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n ) ( ( A x.s B ) e. No /\ ( E. p e. NN_s ( ( -us ` p )
193		elreno	|- ( A e. RR_s <-> ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )
194		elreno	|- ( B e. RR_s <-> ( B e. No /\ ( E. m e. NN_s ( ( -us ` m )
195	193 194	anbi12i	|- ( ( A e. RR_s /\ B e. RR_s ) <-> ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )
196		elreno	|- ( ( A x.s B ) e. RR_s <-> ( ( A x.s B ) e. No /\ ( E. p e. NN_s ( ( -us ` p )
197	192 195 196	3imtr4i	|- ( ( A e. RR_s /\ B e. RR_s ) -> ( A x.s B ) e. RR_s )