archirngz

Description: Property of Archimedean left and right ordered groups. (Contributed by Thierry Arnoux, 6-May-2018)

	Ref	Expression
Hypotheses	archirng.b	$⊢ B = {Base}_{W}$
	archirng.0	$⊢ \underset{˙}{0} = 0_{W}$
	archirng.i	$⊢ \underset{˙}{<} = <_{W}$
	archirng.l	$⊢ \underset{˙}{\leq} = \leq_{W}$
	archirng.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	archirng.1	$⊢ φ \to W \in oGrp$
	archirng.2	$⊢ φ \to W \in Archi$
	archirng.3	$⊢ φ \to X \in B$
	archirng.4	$⊢ φ \to Y \in B$
	archirng.5	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} X$
	archirngz.1	$⊢ φ \to {opp}_{𝑔} (W) \in oGrp$
Assertion	archirngz	$⊢ φ \to \exists n \in ℤ ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$

Proof

Step	Hyp	Ref	Expression
1		archirng.b	$⊢ B = {Base}_{W}$
2		archirng.0	$⊢ \underset{˙}{0} = 0_{W}$
3		archirng.i	$⊢ \underset{˙}{<} = <_{W}$
4		archirng.l	$⊢ \underset{˙}{\leq} = \leq_{W}$
5		archirng.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		archirng.1	$⊢ φ \to W \in oGrp$
7		archirng.2	$⊢ φ \to W \in Archi$
8		archirng.3	$⊢ φ \to X \in B$
9		archirng.4	$⊢ φ \to Y \in B$
10		archirng.5	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} X$
11		archirngz.1	$⊢ φ \to {opp}_{𝑔} (W) \in oGrp$
12		neg1z	$⊢ - 1 \in ℤ$
13		ogrpgrp	$⊢ W \in oGrp \to W \in Grp$
14	6 13	syl	$⊢ φ \to W \in Grp$
15		1zzd	$⊢ φ \to 1 \in ℤ$
16		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
17	1 5 16	mulgneg	$⊢ (W \in Grp \land 1 \in ℤ \land X \in B) \to -1 \underset{˙}{\cdot} X = {inv}_{g} (W) (1 \underset{˙}{\cdot} X)$
18	14 15 8 17	syl3anc	$⊢ φ \to -1 \underset{˙}{\cdot} X = {inv}_{g} (W) (1 \underset{˙}{\cdot} X)$
19	1 5	mulg1	$⊢ X \in B \to 1 \underset{˙}{\cdot} X = X$
20	8 19	syl	$⊢ φ \to 1 \underset{˙}{\cdot} X = X$
21	20	fveq2d	$⊢ φ \to {inv}_{g} (W) (1 \underset{˙}{\cdot} X) = {inv}_{g} (W) (X)$
22	18 21	eqtrd	$⊢ φ \to -1 \underset{˙}{\cdot} X = {inv}_{g} (W) (X)$
23	1 3 16 2	ogrpinv0lt	$⊢ (W \in oGrp \land X \in B) \to (\underset{˙}{0} \underset{˙}{<} X \leftrightarrow {inv}_{g} (W) (X) \underset{˙}{<} \underset{˙}{0})$
24	23	biimpa	$⊢ ((W \in oGrp \land X \in B) \land \underset{˙}{0} \underset{˙}{<} X) \to {inv}_{g} (W) (X) \underset{˙}{<} \underset{˙}{0}$
25	6 8 10 24	syl21anc	$⊢ φ \to {inv}_{g} (W) (X) \underset{˙}{<} \underset{˙}{0}$
26	22 25	eqbrtrd	$⊢ φ \to (-1 \underset{˙}{\cdot} X) \underset{˙}{<} \underset{˙}{0}$
27	26	adantr	$⊢ (φ \land Y = \underset{˙}{0}) \to (-1 \underset{˙}{\cdot} X) \underset{˙}{<} \underset{˙}{0}$
28		simpr	$⊢ (φ \land Y = \underset{˙}{0}) \to Y = \underset{˙}{0}$
29	27 28	breqtrrd	$⊢ (φ \land Y = \underset{˙}{0}) \to (-1 \underset{˙}{\cdot} X) \underset{˙}{<} Y$
30		isogrp	$⊢ W \in oGrp \leftrightarrow (W \in Grp \land W \in oMnd)$
31	30	simprbi	$⊢ W \in oGrp \to W \in oMnd$
32		omndtos	$⊢ W \in oMnd \to W \in Toset$
33	6 31 32	3syl	$⊢ φ \to W \in Toset$
34		tospos	$⊢ W \in Toset \to W \in Poset$
35	33 34	syl	$⊢ φ \to W \in Poset$
36	1 2	grpidcl	$⊢ W \in Grp \to \underset{˙}{0} \in B$
37	6 13 36	3syl	$⊢ φ \to \underset{˙}{0} \in B$
38	1 4	posref	$⊢ (W \in Poset \land \underset{˙}{0} \in B) \to \underset{˙}{0} \underset{˙}{\leq} \underset{˙}{0}$
39	35 37 38	syl2anc	$⊢ φ \to \underset{˙}{0} \underset{˙}{\leq} \underset{˙}{0}$
40	39	adantr	$⊢ (φ \land Y = \underset{˙}{0}) \to \underset{˙}{0} \underset{˙}{\leq} \underset{˙}{0}$
41		1m1e0	$⊢ 1 - 1 = 0$
42	41	negeqi	$⊢ - (1 - 1) = - 0$
43		ax-1cn	$⊢ 1 \in ℂ$
44	43 43	negsubdii	$⊢ - (1 - 1) = - 1 + 1$
45		neg0	$⊢ - 0 = 0$
46	42 44 45	3eqtr3i	$⊢ - 1 + 1 = 0$
47	46	oveq1i	$⊢ (- 1 + 1) \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
48	1 2 5	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = \underset{˙}{0}$
49	8 48	syl	$⊢ φ \to 0 \underset{˙}{\cdot} X = \underset{˙}{0}$
50	47 49	eqtrid	$⊢ φ \to (- 1 + 1) \underset{˙}{\cdot} X = \underset{˙}{0}$
51	50	adantr	$⊢ (φ \land Y = \underset{˙}{0}) \to (- 1 + 1) \underset{˙}{\cdot} X = \underset{˙}{0}$
52	40 28 51	3brtr4d	$⊢ (φ \land Y = \underset{˙}{0}) \to Y \underset{˙}{\leq} ((- 1 + 1) \underset{˙}{\cdot} X)$
53	29 52	jca	$⊢ (φ \land Y = \underset{˙}{0}) \to ((-1 \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((- 1 + 1) \underset{˙}{\cdot} X))$
54		oveq1	$⊢ n = - 1 \to n \underset{˙}{\cdot} X = -1 \underset{˙}{\cdot} X$
55	54	breq1d	$⊢ n = - 1 \to ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \leftrightarrow (-1 \underset{˙}{\cdot} X) \underset{˙}{<} Y)$
56		oveq1	$⊢ n = - 1 \to n + 1 = - 1 + 1$
57	56	oveq1d	$⊢ n = - 1 \to (n + 1) \underset{˙}{\cdot} X = (- 1 + 1) \underset{˙}{\cdot} X$
58	57	breq2d	$⊢ n = - 1 \to (Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X) \leftrightarrow Y \underset{˙}{\leq} ((- 1 + 1) \underset{˙}{\cdot} X))$
59	55 58	anbi12d	$⊢ n = - 1 \to (((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X)) \leftrightarrow ((-1 \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((- 1 + 1) \underset{˙}{\cdot} X)))$
60	59	rspcev	$⊢ (- 1 \in ℤ \land ((-1 \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((- 1 + 1) \underset{˙}{\cdot} X))) \to \exists n \in ℤ ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$
61	12 53 60	sylancr	$⊢ (φ \land Y = \underset{˙}{0}) \to \exists n \in ℤ ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$
62		simpr	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to m \in ℕ_{0}$
63	62	nn0zd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to m \in ℤ$
64	63	ad2antrr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to m \in ℤ$
65	64	znegcld	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to - m \in ℤ$
66		2z	$⊢ 2 \in ℤ$
67	66	a1i	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to 2 \in ℤ$
68	65 67	zsubcld	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to - m - 2 \in ℤ$
69		nn0cn	$⊢ m \in ℕ_{0} \to m \in ℂ$
70	69	adantl	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to m \in ℂ$
71		2cnd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to 2 \in ℂ$
72	70 71	negdi2d	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to - (m + 2) = - m - 2$
73	72	oveq1d	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (- (m + 2)) \underset{˙}{\cdot} X = (- m - 2) \underset{˙}{\cdot} X$
74	6	ad2antrr	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to W \in oGrp$
75	11	ad2antrr	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to {opp}_{𝑔} (W) \in oGrp$
76	74 75	jca	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (W \in oGrp \land {opp}_{𝑔} (W) \in oGrp)$
77	14	ad2antrr	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to W \in Grp$
78	63	peano2zd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to m + 1 \in ℤ$
79	8	ad2antrr	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to X \in B$
80	1 5	mulgcl	$⊢ (W \in Grp \land m + 1 \in ℤ \land X \in B) \to (m + 1) \underset{˙}{\cdot} X \in B$
81	77 78 79 80	syl3anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (m + 1) \underset{˙}{\cdot} X \in B$
82	66	a1i	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to 2 \in ℤ$
83	63 82	zaddcld	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to m + 2 \in ℤ$
84	1 5	mulgcl	$⊢ (W \in Grp \land m + 2 \in ℤ \land X \in B) \to (m + 2) \underset{˙}{\cdot} X \in B$
85	77 83 79 84	syl3anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (m + 2) \underset{˙}{\cdot} X \in B$
86	77 36	syl	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to \underset{˙}{0} \in B$
87	10	ad2antrr	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to \underset{˙}{0} \underset{˙}{<} X$
88		eqid	$⊢ +_{W} = +_{W}$
89	1 3 88	ogrpaddlt	$⊢ (W \in oGrp \land (\underset{˙}{0} \in B \land X \in B \land (m + 1) \underset{˙}{\cdot} X \in B) \land \underset{˙}{0} \underset{˙}{<} X) \to (\underset{˙}{0} +_{W} ((m + 1) \underset{˙}{\cdot} X)) \underset{˙}{<} (X +_{W} ((m + 1) \underset{˙}{\cdot} X))$
90	74 86 79 81 87 89	syl131anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (\underset{˙}{0} +_{W} ((m + 1) \underset{˙}{\cdot} X)) \underset{˙}{<} (X +_{W} ((m + 1) \underset{˙}{\cdot} X))$
91	1 88 2	grplid	$⊢ (W \in Grp \land (m + 1) \underset{˙}{\cdot} X \in B) \to \underset{˙}{0} +_{W} ((m + 1) \underset{˙}{\cdot} X) = (m + 1) \underset{˙}{\cdot} X$
92	77 81 91	syl2anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to \underset{˙}{0} +_{W} ((m + 1) \underset{˙}{\cdot} X) = (m + 1) \underset{˙}{\cdot} X$
93		1cnd	$⊢ m \in ℕ_{0} \to 1 \in ℂ$
94	69 93 93	addassd	$⊢ m \in ℕ_{0} \to m + 1 + 1 = m + 1 + 1$
95		1p1e2	$⊢ 1 + 1 = 2$
96	95	oveq2i	$⊢ m + 1 + 1 = m + 2$
97	94 96	eqtrdi	$⊢ m \in ℕ_{0} \to m + 1 + 1 = m + 2$
98	69 93	addcld	$⊢ m \in ℕ_{0} \to m + 1 \in ℂ$
99	98 93	addcomd	$⊢ m \in ℕ_{0} \to m + 1 + 1 = 1 + m + 1$
100	97 99	eqtr3d	$⊢ m \in ℕ_{0} \to m + 2 = 1 + m + 1$
101	100	oveq1d	$⊢ m \in ℕ_{0} \to (m + 2) \underset{˙}{\cdot} X = (1 + m + 1) \underset{˙}{\cdot} X$
102	101	adantl	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (m + 2) \underset{˙}{\cdot} X = (1 + m + 1) \underset{˙}{\cdot} X$
103		1zzd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to 1 \in ℤ$
104	1 5 88	mulgdir	$⊢ (W \in Grp \land (1 \in ℤ \land m + 1 \in ℤ \land X \in B)) \to (1 + m + 1) \underset{˙}{\cdot} X = (1 \underset{˙}{\cdot} X) +_{W} ((m + 1) \underset{˙}{\cdot} X)$
105	77 103 78 79 104	syl13anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (1 + m + 1) \underset{˙}{\cdot} X = (1 \underset{˙}{\cdot} X) +_{W} ((m + 1) \underset{˙}{\cdot} X)$
106	79 19	syl	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to 1 \underset{˙}{\cdot} X = X$
107	106	oveq1d	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (1 \underset{˙}{\cdot} X) +_{W} ((m + 1) \underset{˙}{\cdot} X) = X +_{W} ((m + 1) \underset{˙}{\cdot} X)$
108	102 105 107	3eqtrrd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to X +_{W} ((m + 1) \underset{˙}{\cdot} X) = (m + 2) \underset{˙}{\cdot} X$
109	90 92 108	3brtr3d	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{<} ((m + 2) \underset{˙}{\cdot} X)$
110	1 3 16	ogrpinvlt	$⊢ ((W \in oGrp \land {opp}_{𝑔} (W) \in oGrp) \land (m + 1) \underset{˙}{\cdot} X \in B \land (m + 2) \underset{˙}{\cdot} X \in B) \to (((m + 1) \underset{˙}{\cdot} X) \underset{˙}{<} ((m + 2) \underset{˙}{\cdot} X) \leftrightarrow {inv}_{g} (W) ((m + 2) \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) ((m + 1) \underset{˙}{\cdot} X))$
111	110	biimpa	$⊢ (((W \in oGrp \land {opp}_{𝑔} (W) \in oGrp) \land (m + 1) \underset{˙}{\cdot} X \in B \land (m + 2) \underset{˙}{\cdot} X \in B) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{<} ((m + 2) \underset{˙}{\cdot} X)) \to {inv}_{g} (W) ((m + 2) \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) ((m + 1) \underset{˙}{\cdot} X)$
112	76 81 85 109 111	syl31anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to {inv}_{g} (W) ((m + 2) \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) ((m + 1) \underset{˙}{\cdot} X)$
113	1 5 16	mulgneg	$⊢ (W \in Grp \land m + 2 \in ℤ \land X \in B) \to (- (m + 2)) \underset{˙}{\cdot} X = {inv}_{g} (W) ((m + 2) \underset{˙}{\cdot} X)$
114	77 83 79 113	syl3anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (- (m + 2)) \underset{˙}{\cdot} X = {inv}_{g} (W) ((m + 2) \underset{˙}{\cdot} X)$
115	1 5 16	mulgneg	$⊢ (W \in Grp \land m + 1 \in ℤ \land X \in B) \to (- (m + 1)) \underset{˙}{\cdot} X = {inv}_{g} (W) ((m + 1) \underset{˙}{\cdot} X)$
116	77 78 79 115	syl3anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (- (m + 1)) \underset{˙}{\cdot} X = {inv}_{g} (W) ((m + 1) \underset{˙}{\cdot} X)$
117	112 114 116	3brtr4d	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to ((- (m + 2)) \underset{˙}{\cdot} X) \underset{˙}{<} ((- (m + 1)) \underset{˙}{\cdot} X)$
118	73 117	eqbrtrrd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to ((- m - 2) \underset{˙}{\cdot} X) \underset{˙}{<} ((- (m + 1)) \underset{˙}{\cdot} X)$
119	118	ad2antrr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to ((- m - 2) \underset{˙}{\cdot} X) \underset{˙}{<} ((- (m + 1)) \underset{˙}{\cdot} X)$
120	116	ad2antrr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to (- (m + 1)) \underset{˙}{\cdot} X = {inv}_{g} (W) ((m + 1) \underset{˙}{\cdot} X)$
121	35	ad4antr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to W \in Poset$
122	1 16	grpinvcl	$⊢ (W \in Grp \land Y \in B) \to {inv}_{g} (W) (Y) \in B$
123	14 9 122	syl2anc	$⊢ φ \to {inv}_{g} (W) (Y) \in B$
124	123	ad2antrr	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to {inv}_{g} (W) (Y) \in B$
125	124	ad2antrr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to {inv}_{g} (W) (Y) \in B$
126	81	ad2antrr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to (m + 1) \underset{˙}{\cdot} X \in B$
127		simplrr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X)$
128		simpr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)$
129	1 4	posasymb	$⊢ (W \in Poset \land {inv}_{g} (W) (Y) \in B \land (m + 1) \underset{˙}{\cdot} X \in B) \to (({inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \leftrightarrow {inv}_{g} (W) (Y) = (m + 1) \underset{˙}{\cdot} X)$
130	129	biimpa	$⊢ ((W \in Poset \land {inv}_{g} (W) (Y) \in B \land (m + 1) \underset{˙}{\cdot} X \in B) \land ({inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y))) \to {inv}_{g} (W) (Y) = (m + 1) \underset{˙}{\cdot} X$
131	121 125 126 127 128 130	syl32anc	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to {inv}_{g} (W) (Y) = (m + 1) \underset{˙}{\cdot} X$
132	131	fveq2d	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to {inv}_{g} (W) ({inv}_{g} (W) (Y)) = {inv}_{g} (W) ((m + 1) \underset{˙}{\cdot} X)$
133	1 16	grpinvinv	$⊢ (W \in Grp \land Y \in B) \to {inv}_{g} (W) ({inv}_{g} (W) (Y)) = Y$
134	14 9 133	syl2anc	$⊢ φ \to {inv}_{g} (W) ({inv}_{g} (W) (Y)) = Y$
135	134	ad4antr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to {inv}_{g} (W) ({inv}_{g} (W) (Y)) = Y$
136	120 132 135	3eqtr2rd	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to Y = (- (m + 1)) \underset{˙}{\cdot} X$
137	119 136	breqtrrd	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to ((- m - 2) \underset{˙}{\cdot} X) \underset{˙}{<} Y$
138		1cnd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to 1 \in ℂ$
139	70 71 138	addsubassd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to m + 2 - 1 = m + 2 - 1$
140		2m1e1	$⊢ 2 - 1 = 1$
141	140	oveq2i	$⊢ m + 2 - 1 = m + 1$
142	139 141	eqtr2di	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to m + 1 = m + 2 - 1$
143	142	negeqd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to - (m + 1) = - (m + 2 - 1)$
144	70 71	addcld	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to m + 2 \in ℂ$
145	144 138	negsubdid	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to - (m + 2 - 1) = - (m + 2) + 1$
146	72	oveq1d	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to - (m + 2) + 1 = (- m) - 2 + 1$
147	143 145 146	3eqtrrd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (- m) - 2 + 1 = - (m + 1)$
148	147	oveq1d	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to ((- m) - 2 + 1) \underset{˙}{\cdot} X = (- (m + 1)) \underset{˙}{\cdot} X$
149	33	ad2antrr	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to W \in Toset$
150	149 34	syl	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to W \in Poset$
151	63	znegcld	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to - m \in ℤ$
152	151 82	zsubcld	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to - m - 2 \in ℤ$
153	152	peano2zd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (- m) - 2 + 1 \in ℤ$
154	1 5	mulgcl	$⊢ (W \in Grp \land (- m) - 2 + 1 \in ℤ \land X \in B) \to ((- m) - 2 + 1) \underset{˙}{\cdot} X \in B$
155	77 153 79 154	syl3anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to ((- m) - 2 + 1) \underset{˙}{\cdot} X \in B$
156	1 4	posref	$⊢ (W \in Poset \land ((- m) - 2 + 1) \underset{˙}{\cdot} X \in B) \to (((- m) - 2 + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} (((- m) - 2 + 1) \underset{˙}{\cdot} X)$
157	150 155 156	syl2anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (((- m) - 2 + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} (((- m) - 2 + 1) \underset{˙}{\cdot} X)$
158	148 157	eqbrtrrd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to ((- (m + 1)) \underset{˙}{\cdot} X) \underset{˙}{\leq} (((- m) - 2 + 1) \underset{˙}{\cdot} X)$
159	158	ad2antrr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to ((- (m + 1)) \underset{˙}{\cdot} X) \underset{˙}{\leq} (((- m) - 2 + 1) \underset{˙}{\cdot} X)$
160	136 159	eqbrtrd	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to Y \underset{˙}{\leq} (((- m) - 2 + 1) \underset{˙}{\cdot} X)$
161		oveq1	$⊢ n = - m - 2 \to n \underset{˙}{\cdot} X = (- m - 2) \underset{˙}{\cdot} X$
162	161	breq1d	$⊢ n = - m - 2 \to ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \leftrightarrow ((- m - 2) \underset{˙}{\cdot} X) \underset{˙}{<} Y)$
163		oveq1	$⊢ n = - m - 2 \to n + 1 = (- m) - 2 + 1$
164	163	oveq1d	$⊢ n = - m - 2 \to (n + 1) \underset{˙}{\cdot} X = ((- m) - 2 + 1) \underset{˙}{\cdot} X$
165	164	breq2d	$⊢ n = - m - 2 \to (Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X) \leftrightarrow Y \underset{˙}{\leq} (((- m) - 2 + 1) \underset{˙}{\cdot} X))$
166	162 165	anbi12d	$⊢ n = - m - 2 \to (((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X)) \leftrightarrow (((- m - 2) \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} (((- m) - 2 + 1) \underset{˙}{\cdot} X)))$
167	166	rspcev	$⊢ (- m - 2 \in ℤ \land (((- m - 2) \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} (((- m) - 2 + 1) \underset{˙}{\cdot} X))) \to \exists n \in ℤ ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$
168	68 137 160 167	syl12anc	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y)) \to \exists n \in ℤ ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$
169	78	ad2antrr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to m + 1 \in ℤ$
170	169	znegcld	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to - (m + 1) \in ℤ$
171	6	ad2antrr	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land (m \in ℕ_{0} \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X)) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X))) \to W \in oGrp$
172	11	ad2antrr	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land (m \in ℕ_{0} \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X)) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X))) \to {opp}_{𝑔} (W) \in oGrp$
173	171 172	jca	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land (m \in ℕ_{0} \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X)) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X))) \to (W \in oGrp \land {opp}_{𝑔} (W) \in oGrp)$
174	173	3anassrs	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to (W \in oGrp \land {opp}_{𝑔} (W) \in oGrp)$
175	124	ad2antrr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to {inv}_{g} (W) (Y) \in B$
176	81	ad2antrr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to (m + 1) \underset{˙}{\cdot} X \in B$
177		simpr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)$
178	1 3 16	ogrpinvlt	$⊢ ((W \in oGrp \land {opp}_{𝑔} (W) \in oGrp) \land {inv}_{g} (W) (Y) \in B \land (m + 1) \underset{˙}{\cdot} X \in B) \to ({inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X) \leftrightarrow {inv}_{g} (W) ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) ({inv}_{g} (W) (Y)))$
179	178	biimpa	$⊢ (((W \in oGrp \land {opp}_{𝑔} (W) \in oGrp) \land {inv}_{g} (W) (Y) \in B \land (m + 1) \underset{˙}{\cdot} X \in B) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to {inv}_{g} (W) ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) ({inv}_{g} (W) (Y))$
180	174 175 176 177 179	syl31anc	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to {inv}_{g} (W) ((m + 1) \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) ({inv}_{g} (W) (Y))$
181	116	ad2antrr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to (- (m + 1)) \underset{˙}{\cdot} X = {inv}_{g} (W) ((m + 1) \underset{˙}{\cdot} X)$
182	181	eqcomd	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to {inv}_{g} (W) ((m + 1) \underset{˙}{\cdot} X) = (- (m + 1)) \underset{˙}{\cdot} X$
183	134	ad4antr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to {inv}_{g} (W) ({inv}_{g} (W) (Y)) = Y$
184	180 182 183	3brtr3d	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to ((- (m + 1)) \underset{˙}{\cdot} X) \underset{˙}{<} Y$
185		simp-4l	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to φ$
186	1 5	mulgcl	$⊢ (W \in Grp \land m \in ℤ \land X \in B) \to m \underset{˙}{\cdot} X \in B$
187	77 63 79 186	syl3anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to m \underset{˙}{\cdot} X \in B$
188	1 3 16	ogrpinvlt	$⊢ ((W \in oGrp \land {opp}_{𝑔} (W) \in oGrp) \land m \underset{˙}{\cdot} X \in B \land {inv}_{g} (W) (Y) \in B) \to ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \leftrightarrow {inv}_{g} (W) ({inv}_{g} (W) (Y)) \underset{˙}{<} {inv}_{g} (W) (m \underset{˙}{\cdot} X))$
189	76 187 124 188	syl3anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \leftrightarrow {inv}_{g} (W) ({inv}_{g} (W) (Y)) \underset{˙}{<} {inv}_{g} (W) (m \underset{˙}{\cdot} X))$
190	189	biimpa	$⊢ (((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land (m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y)) \to {inv}_{g} (W) ({inv}_{g} (W) (Y)) \underset{˙}{<} {inv}_{g} (W) (m \underset{˙}{\cdot} X)$
191	190	adantrr	$⊢ (((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \to {inv}_{g} (W) ({inv}_{g} (W) (Y)) \underset{˙}{<} {inv}_{g} (W) (m \underset{˙}{\cdot} X)$
192	191	adantr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to {inv}_{g} (W) ({inv}_{g} (W) (Y)) \underset{˙}{<} {inv}_{g} (W) (m \underset{˙}{\cdot} X)$
193		negdi	$⊢ (m \in ℂ \land 1 \in ℂ) \to - (m + 1) = - m + -1$
194	69 43 193	sylancl	$⊢ m \in ℕ_{0} \to - (m + 1) = - m + -1$
195	194	oveq1d	$⊢ m \in ℕ_{0} \to - (m + 1) + 1 = (- m) + -1 + 1$
196	69	negcld	$⊢ m \in ℕ_{0} \to - m \in ℂ$
197	93	negcld	$⊢ m \in ℕ_{0} \to - 1 \in ℂ$
198	196 197 93	addassd	$⊢ m \in ℕ_{0} \to (- m) + -1 + 1 = (- m) + -1 + 1$
199	46	oveq2i	$⊢ (- m) + -1 + 1 = - m + 0$
200	199	a1i	$⊢ m \in ℕ_{0} \to (- m) + -1 + 1 = - m + 0$
201	196	addridd	$⊢ m \in ℕ_{0} \to - m + 0 = - m$
202	198 200 201	3eqtrd	$⊢ m \in ℕ_{0} \to (- m) + -1 + 1 = - m$
203	195 202	eqtrd	$⊢ m \in ℕ_{0} \to - (m + 1) + 1 = - m$
204	203	oveq1d	$⊢ m \in ℕ_{0} \to (- (m + 1) + 1) \underset{˙}{\cdot} X = (- m) \underset{˙}{\cdot} X$
205	204	adantl	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (- (m + 1) + 1) \underset{˙}{\cdot} X = (- m) \underset{˙}{\cdot} X$
206	1 5 16	mulgneg	$⊢ (W \in Grp \land m \in ℤ \land X \in B) \to (- m) \underset{˙}{\cdot} X = {inv}_{g} (W) (m \underset{˙}{\cdot} X)$
207	77 63 79 206	syl3anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (- m) \underset{˙}{\cdot} X = {inv}_{g} (W) (m \underset{˙}{\cdot} X)$
208	205 207	eqtrd	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (- (m + 1) + 1) \underset{˙}{\cdot} X = {inv}_{g} (W) (m \underset{˙}{\cdot} X)$
209	208	ad2antrr	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to (- (m + 1) + 1) \underset{˙}{\cdot} X = {inv}_{g} (W) (m \underset{˙}{\cdot} X)$
210	209	eqcomd	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to {inv}_{g} (W) (m \underset{˙}{\cdot} X) = (- (m + 1) + 1) \underset{˙}{\cdot} X$
211	192 183 210	3brtr3d	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to Y \underset{˙}{<} ((- (m + 1) + 1) \underset{˙}{\cdot} X)$
212		ovexd	$⊢ φ \to (- (m + 1) + 1) \underset{˙}{\cdot} X \in V$
213	4 3	pltle	$⊢ (W \in oGrp \land Y \in B \land (- (m + 1) + 1) \underset{˙}{\cdot} X \in V) \to (Y \underset{˙}{<} ((- (m + 1) + 1) \underset{˙}{\cdot} X) \to Y \underset{˙}{\leq} ((- (m + 1) + 1) \underset{˙}{\cdot} X))$
214	6 9 212 213	syl3anc	$⊢ φ \to (Y \underset{˙}{<} ((- (m + 1) + 1) \underset{˙}{\cdot} X) \to Y \underset{˙}{\leq} ((- (m + 1) + 1) \underset{˙}{\cdot} X))$
215	185 211 214	sylc	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to Y \underset{˙}{\leq} ((- (m + 1) + 1) \underset{˙}{\cdot} X)$
216		oveq1	$⊢ n = - (m + 1) \to n \underset{˙}{\cdot} X = (- (m + 1)) \underset{˙}{\cdot} X$
217	216	breq1d	$⊢ n = - (m + 1) \to ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \leftrightarrow ((- (m + 1)) \underset{˙}{\cdot} X) \underset{˙}{<} Y)$
218		oveq1	$⊢ n = - (m + 1) \to n + 1 = - (m + 1) + 1$
219	218	oveq1d	$⊢ n = - (m + 1) \to (n + 1) \underset{˙}{\cdot} X = (- (m + 1) + 1) \underset{˙}{\cdot} X$
220	219	breq2d	$⊢ n = - (m + 1) \to (Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X) \leftrightarrow Y \underset{˙}{\leq} ((- (m + 1) + 1) \underset{˙}{\cdot} X))$
221	217 220	anbi12d	$⊢ n = - (m + 1) \to (((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X)) \leftrightarrow (((- (m + 1)) \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((- (m + 1) + 1) \underset{˙}{\cdot} X)))$
222	221	rspcev	$⊢ (- (m + 1) \in ℤ \land (((- (m + 1)) \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((- (m + 1) + 1) \underset{˙}{\cdot} X))) \to \exists n \in ℤ ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$
223	170 184 215 222	syl12anc	$⊢ ((((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \land {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X)) \to \exists n \in ℤ ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$
224	1 4 3	tlt2	$⊢ (W \in Toset \land (m + 1) \underset{˙}{\cdot} X \in B \land {inv}_{g} (W) (Y) \in B) \to (((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y) \lor {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X))$
225	149 81 124 224	syl3anc	$⊢ ((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \to (((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y) \lor {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X))$
226	225	adantr	$⊢ (((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \to (((m + 1) \underset{˙}{\cdot} X) \underset{˙}{\leq} {inv}_{g} (W) (Y) \lor {inv}_{g} (W) (Y) \underset{˙}{<} ((m + 1) \underset{˙}{\cdot} X))$
227	168 223 226	mpjaodan	$⊢ (((φ \land Y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))) \to \exists n \in ℤ ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$
228	6	adantr	$⊢ (φ \land Y \underset{˙}{<} \underset{˙}{0}) \to W \in oGrp$
229	7	adantr	$⊢ (φ \land Y \underset{˙}{<} \underset{˙}{0}) \to W \in Archi$
230	8	adantr	$⊢ (φ \land Y \underset{˙}{<} \underset{˙}{0}) \to X \in B$
231	123	adantr	$⊢ (φ \land Y \underset{˙}{<} \underset{˙}{0}) \to {inv}_{g} (W) (Y) \in B$
232	10	adantr	$⊢ (φ \land Y \underset{˙}{<} \underset{˙}{0}) \to \underset{˙}{0} \underset{˙}{<} X$
233	134	breq1d	$⊢ φ \to ({inv}_{g} (W) ({inv}_{g} (W) (Y)) \underset{˙}{<} \underset{˙}{0} \leftrightarrow Y \underset{˙}{<} \underset{˙}{0})$
234	233	biimpar	$⊢ (φ \land Y \underset{˙}{<} \underset{˙}{0}) \to {inv}_{g} (W) ({inv}_{g} (W) (Y)) \underset{˙}{<} \underset{˙}{0}$
235	1 3 16 2	ogrpinv0lt	$⊢ (W \in oGrp \land {inv}_{g} (W) (Y) \in B) \to (\underset{˙}{0} \underset{˙}{<} {inv}_{g} (W) (Y) \leftrightarrow {inv}_{g} (W) ({inv}_{g} (W) (Y)) \underset{˙}{<} \underset{˙}{0})$
236	6 123 235	syl2anc	$⊢ φ \to (\underset{˙}{0} \underset{˙}{<} {inv}_{g} (W) (Y) \leftrightarrow {inv}_{g} (W) ({inv}_{g} (W) (Y)) \underset{˙}{<} \underset{˙}{0})$
237	236	biimpar	$⊢ (φ \land {inv}_{g} (W) ({inv}_{g} (W) (Y)) \underset{˙}{<} \underset{˙}{0}) \to \underset{˙}{0} \underset{˙}{<} {inv}_{g} (W) (Y)$
238	234 237	syldan	$⊢ (φ \land Y \underset{˙}{<} \underset{˙}{0}) \to \underset{˙}{0} \underset{˙}{<} {inv}_{g} (W) (Y)$
239	1 2 3 4 5 228 229 230 231 232 238	archirng	$⊢ (φ \land Y \underset{˙}{<} \underset{˙}{0}) \to \exists m \in ℕ_{0} ((m \underset{˙}{\cdot} X) \underset{˙}{<} {inv}_{g} (W) (Y) \land {inv}_{g} (W) (Y) \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} X))$
240	227 239	r19.29a	$⊢ (φ \land Y \underset{˙}{<} \underset{˙}{0}) \to \exists n \in ℤ ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$
241		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
242	6	adantr	$⊢ (φ \land \underset{˙}{0} \underset{˙}{<} Y) \to W \in oGrp$
243	7	adantr	$⊢ (φ \land \underset{˙}{0} \underset{˙}{<} Y) \to W \in Archi$
244	8	adantr	$⊢ (φ \land \underset{˙}{0} \underset{˙}{<} Y) \to X \in B$
245	9	adantr	$⊢ (φ \land \underset{˙}{0} \underset{˙}{<} Y) \to Y \in B$
246	10	adantr	$⊢ (φ \land \underset{˙}{0} \underset{˙}{<} Y) \to \underset{˙}{0} \underset{˙}{<} X$
247		simpr	$⊢ (φ \land \underset{˙}{0} \underset{˙}{<} Y) \to \underset{˙}{0} \underset{˙}{<} Y$
248	1 2 3 4 5 242 243 244 245 246 247	archirng	$⊢ (φ \land \underset{˙}{0} \underset{˙}{<} Y) \to \exists n \in ℕ_{0} ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$
249		ssrexv	$⊢ ℕ_{0} \subseteq ℤ \to (\exists n \in ℕ_{0} ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X)) \to \exists n \in ℤ ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X)))$
250	241 248 249	mpsyl	$⊢ (φ \land \underset{˙}{0} \underset{˙}{<} Y) \to \exists n \in ℤ ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$
251	1 3	tlt3	$⊢ (W \in Toset \land Y \in B \land \underset{˙}{0} \in B) \to (Y = \underset{˙}{0} \lor Y \underset{˙}{<} \underset{˙}{0} \lor \underset{˙}{0} \underset{˙}{<} Y)$
252	33 9 37 251	syl3anc	$⊢ φ \to (Y = \underset{˙}{0} \lor Y \underset{˙}{<} \underset{˙}{0} \lor \underset{˙}{0} \underset{˙}{<} Y)$
253	61 240 250 252	mpjao3dan	$⊢ φ \to \exists n \in ℤ ((n \underset{˙}{\cdot} X) \underset{˙}{<} Y \land Y \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$

Metamath Proof Explorer

Theorem archirngz

Proof