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 \in ℝ_{s} \land B \in ℝ_{s}) \to A +_{s} B \in ℝ_{s}$

Proof

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

Metamath Proof Explorer

Theorem readdscl

Proof