archiabllem2c

	Ref	Expression
Hypotheses	archiabllem.b	$⊢ B = {Base}_{W}$
	archiabllem.0	$⊢ \underset{˙}{0} = 0_{W}$
	archiabllem.e	$⊢ \underset{˙}{\leq} = \leq_{W}$
	archiabllem.t	$⊢ \underset{˙}{<} = <_{W}$
	archiabllem.m	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	archiabllem.g	$⊢ φ \to W \in oGrp$
	archiabllem.a	$⊢ φ \to W \in Archi$
	archiabllem2.1	$⊢ \underset{˙}{+} = +_{W}$
	archiabllem2.2	$⊢ φ \to {opp}_{𝑔} (W) \in oGrp$
	archiabllem2.3	$⊢ (φ \land a \in B \land \underset{˙}{0} \underset{˙}{<} a) \to \exists b \in B (\underset{˙}{0} \underset{˙}{<} b \land b \underset{˙}{<} a)$
	archiabllem2b.4	$⊢ φ \to X \in B$
	archiabllem2b.5	$⊢ φ \to Y \in B$
Assertion	archiabllem2c	$⊢ φ \to \neg (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)$

Proof

Step	Hyp	Ref	Expression
1		archiabllem.b	$⊢ B = {Base}_{W}$
2		archiabllem.0	$⊢ \underset{˙}{0} = 0_{W}$
3		archiabllem.e	$⊢ \underset{˙}{\leq} = \leq_{W}$
4		archiabllem.t	$⊢ \underset{˙}{<} = <_{W}$
5		archiabllem.m	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		archiabllem.g	$⊢ φ \to W \in oGrp$
7		archiabllem.a	$⊢ φ \to W \in Archi$
8		archiabllem2.1	$⊢ \underset{˙}{+} = +_{W}$
9		archiabllem2.2	$⊢ φ \to {opp}_{𝑔} (W) \in oGrp$
10		archiabllem2.3	$⊢ (φ \land a \in B \land \underset{˙}{0} \underset{˙}{<} a) \to \exists b \in B (\underset{˙}{0} \underset{˙}{<} b \land b \underset{˙}{<} a)$
11		archiabllem2b.4	$⊢ φ \to X \in B$
12		archiabllem2b.5	$⊢ φ \to Y \in B$
13		simprr	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B) \land (\underset{˙}{0} \underset{˙}{<} t \land (t \underset{˙}{+} t) \underset{˙}{\leq} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)))) \to (t \underset{˙}{+} t) \underset{˙}{\leq} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y))$
14		simpl1l	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to φ$
15	14 6	syl	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to W \in oGrp$
16		simpl1r	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)$
17	6	adantr	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to W \in oGrp$
18		ogrpgrp	$⊢ W \in oGrp \to W \in Grp$
19	17 18	syl	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to W \in Grp$
20	12	adantr	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to Y \in B$
21	11	adantr	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to X \in B$
22	1 8	grpcl	$⊢ (W \in Grp \land Y \in B \land X \in B) \to Y \underset{˙}{+} X \in B$
23	19 20 21 22	syl3anc	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to Y \underset{˙}{+} X \in B$
24	14 16 23	syl2anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to Y \underset{˙}{+} X \in B$
25	14 6 18	3syl	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to W \in Grp$
26		simpr2	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to m \in ℤ$
27	26	peano2zd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to m + 1 \in ℤ$
28		simp2	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to t \in B$
29	28	adantr	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to t \in B$
30	1 5	mulgcl	$⊢ (W \in Grp \land m + 1 \in ℤ \land t \in B) \to (m + 1) \underset{˙}{\cdot} t \in B$
31	25 27 29 30	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (m + 1) \underset{˙}{\cdot} t \in B$
32		simpr1	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to n \in ℤ$
33	32	peano2zd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to n + 1 \in ℤ$
34	1 5	mulgcl	$⊢ (W \in Grp \land n + 1 \in ℤ \land t \in B) \to (n + 1) \underset{˙}{\cdot} t \in B$
35	25 33 29 34	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (n + 1) \underset{˙}{\cdot} t \in B$
36	1 8	grpcl	$⊢ (W \in Grp \land (m + 1) \underset{˙}{\cdot} t \in B \land (n + 1) \underset{˙}{\cdot} t \in B) \to ((m + 1) \underset{˙}{\cdot} t) \underset{˙}{+} ((n + 1) \underset{˙}{\cdot} t) \in B$
37	25 31 35 36	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((m + 1) \underset{˙}{\cdot} t) \underset{˙}{+} ((n + 1) \underset{˙}{\cdot} t) \in B$
38	21	3ad2ant1	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to X \in B$
39	38	adantr	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to X \in B$
40	20	3ad2ant1	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to Y \in B$
41	40	adantr	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to Y \in B$
42	1 8	grpcl	$⊢ (W \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
43	25 39 41 42	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to X \underset{˙}{+} Y \in B$
44		isogrp	$⊢ W \in oGrp \leftrightarrow (W \in Grp \land W \in oMnd)$
45	44	simprbi	$⊢ W \in oGrp \to W \in oMnd$
46	14 6 45	3syl	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to W \in oMnd$
47		simpr3	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t)))$
48	47	simprd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))$
49	48	simprd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t)$
50	47	simpld	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t))$
51	50	simprd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)$
52		isogrp	$⊢ {opp}_{𝑔} (W) \in oGrp \leftrightarrow ({opp}_{𝑔} (W) \in Grp \land {opp}_{𝑔} (W) \in oMnd)$
53	52	simprbi	$⊢ {opp}_{𝑔} (W) \in oGrp \to {opp}_{𝑔} (W) \in oMnd$
54	14 9 53	3syl	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to {opp}_{𝑔} (W) \in oMnd$
55	1 3 8 46 35 41 39 31 49 51 54	omndadd2rd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (Y \underset{˙}{+} X) \underset{˙}{\leq} (((m + 1) \underset{˙}{\cdot} t) \underset{˙}{+} ((n + 1) \underset{˙}{\cdot} t))$
56		eqid	$⊢ -_{W} = -_{W}$
57	1 3 56	ogrpsub	$⊢ (W \in oGrp \land (Y \underset{˙}{+} X \in B \land ((m + 1) \underset{˙}{\cdot} t) \underset{˙}{+} ((n + 1) \underset{˙}{\cdot} t) \in B \land X \underset{˙}{+} Y \in B) \land (Y \underset{˙}{+} X) \underset{˙}{\leq} (((m + 1) \underset{˙}{\cdot} t) \underset{˙}{+} ((n + 1) \underset{˙}{\cdot} t))) \to ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{\leq} ((((m + 1) \underset{˙}{\cdot} t) \underset{˙}{+} ((n + 1) \underset{˙}{\cdot} t)) -_{W} (X \underset{˙}{+} Y))$
58	15 24 37 43 55 57	syl131anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{\leq} ((((m + 1) \underset{˙}{\cdot} t) \underset{˙}{+} ((n + 1) \underset{˙}{\cdot} t)) -_{W} (X \underset{˙}{+} Y))$
59	26	zcnd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to m \in ℂ$
60	32	zcnd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to n \in ℂ$
61		1cnd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to 1 \in ℂ$
62	59 60 61 61	add4d	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to m + n + 1 + 1 = m + 1 + n + 1$
63		1p1e2	$⊢ 1 + 1 = 2$
64	63	oveq2i	$⊢ m + n + 1 + 1 = m + n + 2$
65		addcom	$⊢ (m \in ℂ \land n \in ℂ) \to m + n = n + m$
66	65	oveq1d	$⊢ (m \in ℂ \land n \in ℂ) \to m + n + 2 = n + m + 2$
67	64 66	eqtrid	$⊢ (m \in ℂ \land n \in ℂ) \to m + n + 1 + 1 = n + m + 2$
68		2cnd	$⊢ (m \in ℂ \land n \in ℂ) \to 2 \in ℂ$
69		simpr	$⊢ (m \in ℂ \land n \in ℂ) \to n \in ℂ$
70		simpl	$⊢ (m \in ℂ \land n \in ℂ) \to m \in ℂ$
71	69 70	addcld	$⊢ (m \in ℂ \land n \in ℂ) \to n + m \in ℂ$
72	68 71	addcomd	$⊢ (m \in ℂ \land n \in ℂ) \to 2 + n + m = n + m + 2$
73	67 72	eqtr4d	$⊢ (m \in ℂ \land n \in ℂ) \to m + n + 1 + 1 = 2 + n + m$
74	59 60 73	syl2anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to m + n + 1 + 1 = 2 + n + m$
75	62 74	eqtr3d	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to m + 1 + n + 1 = 2 + n + m$
76	75	oveq1d	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (m + 1 + n + 1) \underset{˙}{\cdot} t = (2 + n + m) \underset{˙}{\cdot} t$
77		2z	$⊢ 2 \in ℤ$
78	77	a1i	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to 2 \in ℤ$
79	32 26	zaddcld	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to n + m \in ℤ$
80	1 5 8	mulgdir	$⊢ (W \in Grp \land (2 \in ℤ \land n + m \in ℤ \land t \in B)) \to (2 + n + m) \underset{˙}{\cdot} t = (2 \underset{˙}{\cdot} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)$
81	25 78 79 29 80	syl13anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (2 + n + m) \underset{˙}{\cdot} t = (2 \underset{˙}{\cdot} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)$
82	76 81	eqtrd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (m + 1 + n + 1) \underset{˙}{\cdot} t = (2 \underset{˙}{\cdot} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)$
83	1 5 8	mulgdir	$⊢ (W \in Grp \land (m + 1 \in ℤ \land n + 1 \in ℤ \land t \in B)) \to (m + 1 + n + 1) \underset{˙}{\cdot} t = ((m + 1) \underset{˙}{\cdot} t) \underset{˙}{+} ((n + 1) \underset{˙}{\cdot} t)$
84	25 27 33 29 83	syl13anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (m + 1 + n + 1) \underset{˙}{\cdot} t = ((m + 1) \underset{˙}{\cdot} t) \underset{˙}{+} ((n + 1) \underset{˙}{\cdot} t)$
85	1 5 8	mulg2	$⊢ t \in B \to 2 \underset{˙}{\cdot} t = t \underset{˙}{+} t$
86	29 85	syl	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to 2 \underset{˙}{\cdot} t = t \underset{˙}{+} t$
87	86	oveq1d	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (2 \underset{˙}{\cdot} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t) = (t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)$
88	82 84 87	3eqtr3d	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((m + 1) \underset{˙}{\cdot} t) \underset{˙}{+} ((n + 1) \underset{˙}{\cdot} t) = (t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)$
89	88	oveq1d	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (((m + 1) \underset{˙}{\cdot} t) \underset{˙}{+} ((n + 1) \underset{˙}{\cdot} t)) -_{W} (X \underset{˙}{+} Y) = ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) -_{W} (X \underset{˙}{+} Y)$
90	58 89	breqtrd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{\leq} (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) -_{W} (X \underset{˙}{+} Y))$
91	88 37	eqeltrrd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t) \in B$
92		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
93	1 8 92 56	grpsubval	$⊢ ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t) \in B \land X \underset{˙}{+} Y \in B) \to ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) -_{W} (X \underset{˙}{+} Y) = ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} {inv}_{g} (W) (X \underset{˙}{+} Y)$
94	91 43 93	syl2anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) -_{W} (X \underset{˙}{+} Y) = ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} {inv}_{g} (W) (X \underset{˙}{+} Y)$
95	90 94	breqtrd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{\leq} (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} {inv}_{g} (W) (X \underset{˙}{+} Y))$
96	14 9	syl	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to {opp}_{𝑔} (W) \in oGrp$
97	1 92	grpinvcl	$⊢ (W \in Grp \land X \underset{˙}{+} Y \in B) \to {inv}_{g} (W) (X \underset{˙}{+} Y) \in B$
98	25 43 97	syl2anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to {inv}_{g} (W) (X \underset{˙}{+} Y) \in B$
99	79	znegcld	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to - (n + m) \in ℤ$
100	1 5	mulgcl	$⊢ (W \in Grp \land - (n + m) \in ℤ \land t \in B) \to (- (n + m)) \underset{˙}{\cdot} t \in B$
101	25 99 29 100	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (- (n + m)) \underset{˙}{\cdot} t \in B$
102	1 5 8	mulgdir	$⊢ (W \in Grp \land (n \in ℤ \land m \in ℤ \land t \in B)) \to (n + m) \underset{˙}{\cdot} t = (n \underset{˙}{\cdot} t) \underset{˙}{+} (m \underset{˙}{\cdot} t)$
103	25 32 26 29 102	syl13anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (n + m) \underset{˙}{\cdot} t = (n \underset{˙}{\cdot} t) \underset{˙}{+} (m \underset{˙}{\cdot} t)$
104	1 5	mulgcl	$⊢ (W \in Grp \land n \in ℤ \land t \in B) \to n \underset{˙}{\cdot} t \in B$
105	25 32 29 104	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to n \underset{˙}{\cdot} t \in B$
106	1 5	mulgcl	$⊢ (W \in Grp \land m \in ℤ \land t \in B) \to m \underset{˙}{\cdot} t \in B$
107	25 26 29 106	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to m \underset{˙}{\cdot} t \in B$
108	50	simpld	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (n \underset{˙}{\cdot} t) \underset{˙}{<} X$
109	1 4 8	ogrpaddlt	$⊢ (W \in oGrp \land (n \underset{˙}{\cdot} t \in B \land X \in B \land m \underset{˙}{\cdot} t \in B) \land (n \underset{˙}{\cdot} t) \underset{˙}{<} X) \to ((n \underset{˙}{\cdot} t) \underset{˙}{+} (m \underset{˙}{\cdot} t)) \underset{˙}{<} (X \underset{˙}{+} (m \underset{˙}{\cdot} t))$
110	15 105 39 107 108 109	syl131anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((n \underset{˙}{\cdot} t) \underset{˙}{+} (m \underset{˙}{\cdot} t)) \underset{˙}{<} (X \underset{˙}{+} (m \underset{˙}{\cdot} t))$
111	48	simpld	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (m \underset{˙}{\cdot} t) \underset{˙}{<} Y$
112	1 4 8 15 96 107 41 39 111	ogrpaddltrd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (X \underset{˙}{+} (m \underset{˙}{\cdot} t)) \underset{˙}{<} (X \underset{˙}{+} Y)$
113		omndtos	$⊢ W \in oMnd \to W \in Toset$
114		tospos	$⊢ W \in Toset \to W \in Poset$
115	46 113 114	3syl	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to W \in Poset$
116	1 8	grpcl	$⊢ (W \in Grp \land n \underset{˙}{\cdot} t \in B \land m \underset{˙}{\cdot} t \in B) \to (n \underset{˙}{\cdot} t) \underset{˙}{+} (m \underset{˙}{\cdot} t) \in B$
117	25 105 107 116	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (n \underset{˙}{\cdot} t) \underset{˙}{+} (m \underset{˙}{\cdot} t) \in B$
118	1 8	grpcl	$⊢ (W \in Grp \land X \in B \land m \underset{˙}{\cdot} t \in B) \to X \underset{˙}{+} (m \underset{˙}{\cdot} t) \in B$
119	25 39 107 118	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to X \underset{˙}{+} (m \underset{˙}{\cdot} t) \in B$
120	1 4	plttr	$⊢ (W \in Poset \land ((n \underset{˙}{\cdot} t) \underset{˙}{+} (m \underset{˙}{\cdot} t) \in B \land X \underset{˙}{+} (m \underset{˙}{\cdot} t) \in B \land X \underset{˙}{+} Y \in B)) \to ((((n \underset{˙}{\cdot} t) \underset{˙}{+} (m \underset{˙}{\cdot} t)) \underset{˙}{<} (X \underset{˙}{+} (m \underset{˙}{\cdot} t)) \land (X \underset{˙}{+} (m \underset{˙}{\cdot} t)) \underset{˙}{<} (X \underset{˙}{+} Y)) \to ((n \underset{˙}{\cdot} t) \underset{˙}{+} (m \underset{˙}{\cdot} t)) \underset{˙}{<} (X \underset{˙}{+} Y))$
121	115 117 119 43 120	syl13anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((((n \underset{˙}{\cdot} t) \underset{˙}{+} (m \underset{˙}{\cdot} t)) \underset{˙}{<} (X \underset{˙}{+} (m \underset{˙}{\cdot} t)) \land (X \underset{˙}{+} (m \underset{˙}{\cdot} t)) \underset{˙}{<} (X \underset{˙}{+} Y)) \to ((n \underset{˙}{\cdot} t) \underset{˙}{+} (m \underset{˙}{\cdot} t)) \underset{˙}{<} (X \underset{˙}{+} Y))$
122	110 112 121	mp2and	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((n \underset{˙}{\cdot} t) \underset{˙}{+} (m \underset{˙}{\cdot} t)) \underset{˙}{<} (X \underset{˙}{+} Y)$
123	103 122	eqbrtrd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((n + m) \underset{˙}{\cdot} t) \underset{˙}{<} (X \underset{˙}{+} Y)$
124	103 117	eqeltrd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (n + m) \underset{˙}{\cdot} t \in B$
125	1 4 92	ogrpinvlt	$⊢ ((W \in oGrp \land {opp}_{𝑔} (W) \in oGrp) \land (n + m) \underset{˙}{\cdot} t \in B \land X \underset{˙}{+} Y \in B) \to (((n + m) \underset{˙}{\cdot} t) \underset{˙}{<} (X \underset{˙}{+} Y) \leftrightarrow {inv}_{g} (W) (X \underset{˙}{+} Y) \underset{˙}{<} {inv}_{g} (W) ((n + m) \underset{˙}{\cdot} t))$
126	15 96 124 43 125	syl211anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (((n + m) \underset{˙}{\cdot} t) \underset{˙}{<} (X \underset{˙}{+} Y) \leftrightarrow {inv}_{g} (W) (X \underset{˙}{+} Y) \underset{˙}{<} {inv}_{g} (W) ((n + m) \underset{˙}{\cdot} t))$
127	123 126	mpbid	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to {inv}_{g} (W) (X \underset{˙}{+} Y) \underset{˙}{<} {inv}_{g} (W) ((n + m) \underset{˙}{\cdot} t)$
128	1 5 92	mulgneg	$⊢ (W \in Grp \land n + m \in ℤ \land t \in B) \to (- (n + m)) \underset{˙}{\cdot} t = {inv}_{g} (W) ((n + m) \underset{˙}{\cdot} t)$
129	25 79 29 128	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (- (n + m)) \underset{˙}{\cdot} t = {inv}_{g} (W) ((n + m) \underset{˙}{\cdot} t)$
130	127 129	breqtrrd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to {inv}_{g} (W) (X \underset{˙}{+} Y) \underset{˙}{<} ((- (n + m)) \underset{˙}{\cdot} t)$
131	1 4 8 15 96 98 101 91 130	ogrpaddltrd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} {inv}_{g} (W) (X \underset{˙}{+} Y)) \underset{˙}{<} (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t))$
132	1 56	grpsubcl	$⊢ (W \in Grp \land Y \underset{˙}{+} X \in B \land X \underset{˙}{+} Y \in B) \to (Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y) \in B$
133	25 24 43 132	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y) \in B$
134	1 8	grpcl	$⊢ (W \in Grp \land (t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t) \in B \land {inv}_{g} (W) (X \underset{˙}{+} Y) \in B) \to ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} {inv}_{g} (W) (X \underset{˙}{+} Y) \in B$
135	25 91 98 134	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} {inv}_{g} (W) (X \underset{˙}{+} Y) \in B$
136	1 8	grpcl	$⊢ (W \in Grp \land (t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t) \in B \land (- (n + m)) \underset{˙}{\cdot} t \in B) \to ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t) \in B$
137	25 91 101 136	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t) \in B$
138	1 3 4	plelttr	$⊢ (W \in Poset \land ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y) \in B \land ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} {inv}_{g} (W) (X \underset{˙}{+} Y) \in B \land ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t) \in B)) \to ((((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{\leq} (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} {inv}_{g} (W) (X \underset{˙}{+} Y)) \land (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} {inv}_{g} (W) (X \underset{˙}{+} Y)) \underset{˙}{<} (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t))) \to ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{<} (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t)))$
139	115 133 135 137 138	syl13anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{\leq} (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} {inv}_{g} (W) (X \underset{˙}{+} Y)) \land (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} {inv}_{g} (W) (X \underset{˙}{+} Y)) \underset{˙}{<} (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t))) \to ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{<} (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t)))$
140	95 131 139	mp2and	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{<} (((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t))$
141	1 8	grpcl	$⊢ (W \in Grp \land t \in B \land t \in B) \to t \underset{˙}{+} t \in B$
142	25 29 29 141	syl3anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to t \underset{˙}{+} t \in B$
143	1 8	grpass	$⊢ (W \in Grp \land (t \underset{˙}{+} t \in B \land (n + m) \underset{˙}{\cdot} t \in B \land (- (n + m)) \underset{˙}{\cdot} t \in B)) \to ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t) = (t \underset{˙}{+} t) \underset{˙}{+} (((n + m) \underset{˙}{\cdot} t) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t))$
144	25 142 124 101 143	syl13anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t) = (t \underset{˙}{+} t) \underset{˙}{+} (((n + m) \underset{˙}{\cdot} t) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t))$
145	60 59	addcld	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to n + m \in ℂ$
146	145	negidd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to n + m + (- (n + m)) = 0$
147	146	oveq1d	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (n + m + (- (n + m))) \underset{˙}{\cdot} t = 0 \underset{˙}{\cdot} t$
148	1 5 8	mulgdir	$⊢ (W \in Grp \land (n + m \in ℤ \land - (n + m) \in ℤ \land t \in B)) \to (n + m + (- (n + m))) \underset{˙}{\cdot} t = ((n + m) \underset{˙}{\cdot} t) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t)$
149	25 79 99 29 148	syl13anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (n + m + (- (n + m))) \underset{˙}{\cdot} t = ((n + m) \underset{˙}{\cdot} t) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t)$
150	1 2 5	mulg0	$⊢ t \in B \to 0 \underset{˙}{\cdot} t = \underset{˙}{0}$
151	29 150	syl	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to 0 \underset{˙}{\cdot} t = \underset{˙}{0}$
152	147 149 151	3eqtr3d	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((n + m) \underset{˙}{\cdot} t) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t) = \underset{˙}{0}$
153	152	oveq2d	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (t \underset{˙}{+} t) \underset{˙}{+} (((n + m) \underset{˙}{\cdot} t) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t)) = (t \underset{˙}{+} t) \underset{˙}{+} \underset{˙}{0}$
154	1 8 2	grprid	$⊢ (W \in Grp \land t \underset{˙}{+} t \in B) \to (t \underset{˙}{+} t) \underset{˙}{+} \underset{˙}{0} = t \underset{˙}{+} t$
155	25 142 154	syl2anc	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to (t \underset{˙}{+} t) \underset{˙}{+} \underset{˙}{0} = t \underset{˙}{+} t$
156	144 153 155	3eqtrd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((t \underset{˙}{+} t) \underset{˙}{+} ((n + m) \underset{˙}{\cdot} t)) \underset{˙}{+} ((- (n + m)) \underset{˙}{\cdot} t) = t \underset{˙}{+} t$
157	140 156	breqtrd	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land (n \in ℤ \land m \in ℤ \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))))) \to ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{<} (t \underset{˙}{+} t)$
158	157	3anassrs	$⊢ (((((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \land n \in ℤ) \land m \in ℤ) \land (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t)))) \to ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{<} (t \underset{˙}{+} t)$
159	17	3ad2ant1	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to W \in oGrp$
160	7	adantr	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to W \in Archi$
161	160	3ad2ant1	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to W \in Archi$
162		simp3	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to \underset{˙}{0} \underset{˙}{<} t$
163	9	adantr	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to {opp}_{𝑔} (W) \in oGrp$
164	163	3ad2ant1	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to {opp}_{𝑔} (W) \in oGrp$
165	1 2 4 3 5 159 161 28 38 162 164	archirngz	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to \exists n \in ℤ ((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t))$
166	1 2 4 3 5 159 161 28 40 162 164	archirngz	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to \exists m \in ℤ ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))$
167		reeanv	$⊢ \exists n \in ℤ \exists m \in ℤ (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t))) \leftrightarrow (\exists n \in ℤ ((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land \exists m \in ℤ ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t)))$
168	165 166 167	sylanbrc	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to \exists n \in ℤ \exists m \in ℤ (((n \underset{˙}{\cdot} t) \underset{˙}{<} X \land X \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} t)) \land ((m \underset{˙}{\cdot} t) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} t)))$
169	158 168	r19.29vva	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{<} (t \underset{˙}{+} t)$
170	159 45 113	3syl	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to W \in Toset$
171	19 21 20 42	syl3anc	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to X \underset{˙}{+} Y \in B$
172	19 23 171 132	syl3anc	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to (Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y) \in B$
173	172	3ad2ant1	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to (Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y) \in B$
174	159 18	syl	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to W \in Grp$
175	174 28 28 141	syl3anc	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to t \underset{˙}{+} t \in B$
176	1 3 4	tltnle	$⊢ (W \in Toset \land (Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y) \in B \land t \underset{˙}{+} t \in B) \to (((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{<} (t \underset{˙}{+} t) \leftrightarrow \neg (t \underset{˙}{+} t) \underset{˙}{\leq} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)))$
177	170 173 175 176	syl3anc	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to (((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{<} (t \underset{˙}{+} t) \leftrightarrow \neg (t \underset{˙}{+} t) \underset{˙}{\leq} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)))$
178	169 177	mpbid	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B \land \underset{˙}{0} \underset{˙}{<} t) \to \neg (t \underset{˙}{+} t) \underset{˙}{\leq} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y))$
179	178	3expa	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B) \land \underset{˙}{0} \underset{˙}{<} t) \to \neg (t \underset{˙}{+} t) \underset{˙}{\leq} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y))$
180	179	adantrr	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B) \land (\underset{˙}{0} \underset{˙}{<} t \land (t \underset{˙}{+} t) \underset{˙}{\leq} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)))) \to \neg (t \underset{˙}{+} t) \underset{˙}{\leq} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y))$
181	13 180	pm2.21fal	$⊢ (((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land t \in B) \land (\underset{˙}{0} \underset{˙}{<} t \land (t \underset{˙}{+} t) \underset{˙}{\leq} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)))) \to ⊥$
182	10	3adant1r	$⊢ ((φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \land a \in B \land \underset{˙}{0} \underset{˙}{<} a) \to \exists b \in B (\underset{˙}{0} \underset{˙}{<} b \land b \underset{˙}{<} a)$
183	1 2 56	grpsubid	$⊢ (W \in Grp \land X \underset{˙}{+} Y \in B) \to (X \underset{˙}{+} Y) -_{W} (X \underset{˙}{+} Y) = \underset{˙}{0}$
184	19 171 183	syl2anc	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to (X \underset{˙}{+} Y) -_{W} (X \underset{˙}{+} Y) = \underset{˙}{0}$
185		simpr	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)$
186	1 4 56	ogrpsublt	$⊢ (W \in oGrp \land (X \underset{˙}{+} Y \in B \land Y \underset{˙}{+} X \in B \land X \underset{˙}{+} Y \in B) \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to ((X \underset{˙}{+} Y) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{<} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y))$
187	17 171 23 171 185 186	syl131anc	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to ((X \underset{˙}{+} Y) -_{W} (X \underset{˙}{+} Y)) \underset{˙}{<} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y))$
188	184 187	eqbrtrrd	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to \underset{˙}{0} \underset{˙}{<} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y))$
189	1 2 3 4 5 17 160 8 163 182 172 188	archiabllem2a	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to \exists t \in B (\underset{˙}{0} \underset{˙}{<} t \land (t \underset{˙}{+} t) \underset{˙}{\leq} ((Y \underset{˙}{+} X) -_{W} (X \underset{˙}{+} Y)))$
190	181 189	r19.29a	$⊢ (φ \land (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)) \to ⊥$
191	190	inegd	$⊢ φ \to \neg (X \underset{˙}{+} Y) \underset{˙}{<} (Y \underset{˙}{+} X)$

Metamath Proof Explorer

Theorem archiabllem2c

Proof