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

Proof

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

Metamath Proof Explorer

Theorem remulscl

Proof