archirngz - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > archirngz		Structured version Visualization version GIF version

Theorem archirngz 32602

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

**Hypotheses**
Ref	Expression
archirng.b	⊢ 𝐵 = (Base‘𝑊)
archirng.0	⊢ 0 = (0_g‘𝑊)
archirng.i	⊢ < = (lt‘𝑊)
archirng.l	⊢ ≤ = (le‘𝑊)
archirng.x	⊢ · = (._g‘𝑊)
archirng.1	⊢ (𝜑 → 𝑊 ∈ oGrp)
archirng.2	⊢ (𝜑 → 𝑊 ∈ Archi)
archirng.3	⊢ (𝜑 → 𝑋 ∈ 𝐵)
archirng.4	⊢ (𝜑 → 𝑌 ∈ 𝐵)
archirng.5	⊢ (𝜑 → 0 < 𝑋)
archirngz.1	⊢ (𝜑 → (opp_g‘𝑊) ∈ oGrp)

**Assertion**
Ref	Expression
archirngz	⊢ (𝜑 → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))

Distinct variable groups: 𝑛,𝑋 𝑛,𝑌 𝜑,𝑛 0 ,𝑛 ≤ ,𝑛 < ,𝑛 · ,𝑛 Allowed substitution hints: 𝐵(𝑛) 𝑊(𝑛)

Proof of Theorem archirngz Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		neg1z 12603	. . 3 ⊢ -1 ∈ ℤ
2		archirng.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ oGrp)
3		ogrpgrp 32488	. . . . . . . . . 10 ⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Grp)
4	2, 3	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ Grp)
5		1zzd 12598	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℤ)
6		archirng.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
7		archirng.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝑊)
8		archirng.x	. . . . . . . . . 10 ⊢ · = (._g‘𝑊)
9		eqid 2731	. . . . . . . . . 10 ⊢ (inv_g‘𝑊) = (inv_g‘𝑊)
10	7, 8, 9	mulgneg 19009	. . . . . . . . 9 ⊢ ((𝑊 ∈ Grp ∧ 1 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-1 · 𝑋) = ((inv_g‘𝑊)‘(1 · 𝑋)))
11	4, 5, 6, 10	syl3anc 1370	. . . . . . . 8 ⊢ (𝜑 → (-1 · 𝑋) = ((inv_g‘𝑊)‘(1 · 𝑋)))
12	7, 8	mulg1 18998	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝐵 → (1 · 𝑋) = 𝑋)
13	6, 12	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (1 · 𝑋) = 𝑋)
14	13	fveq2d 6896	. . . . . . . 8 ⊢ (𝜑 → ((inv_g‘𝑊)‘(1 · 𝑋)) = ((inv_g‘𝑊)‘𝑋))
15	11, 14	eqtrd 2771	. . . . . . 7 ⊢ (𝜑 → (-1 · 𝑋) = ((inv_g‘𝑊)‘𝑋))
16		archirng.5	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑋)
17		archirng.i	. . . . . . . . . 10 ⊢ < = (lt‘𝑊)
18		archirng.0	. . . . . . . . . 10 ⊢ 0 = (0_g‘𝑊)
19	7, 17, 9, 18	ogrpinv0lt 32507	. . . . . . . . 9 ⊢ ((𝑊 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ ((inv_g‘𝑊)‘𝑋) < 0 ))
20	19	biimpa 476	. . . . . . . 8 ⊢ (((𝑊 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → ((inv_g‘𝑊)‘𝑋) < 0 )
21	2, 6, 16, 20	syl21anc 835	. . . . . . 7 ⊢ (𝜑 → ((inv_g‘𝑊)‘𝑋) < 0 )
22	15, 21	eqbrtrd 5171	. . . . . 6 ⊢ (𝜑 → (-1 · 𝑋) < 0 )
23	22	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → (-1 · 𝑋) < 0 )
24		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → 𝑌 = 0 )
25	23, 24	breqtrrd 5177	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → (-1 · 𝑋) < 𝑌)
26		isogrp 32487	. . . . . . . . . 10 ⊢ (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd))
27	26	simprbi 496	. . . . . . . . 9 ⊢ (𝑊 ∈ oGrp → 𝑊 ∈ oMnd)
28		omndtos 32490	. . . . . . . . 9 ⊢ (𝑊 ∈ oMnd → 𝑊 ∈ Toset)
29	2, 27, 28	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Toset)
30		tospos 18378	. . . . . . . 8 ⊢ (𝑊 ∈ Toset → 𝑊 ∈ Poset)
31	29, 30	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Poset)
32	7, 18	grpidcl 18887	. . . . . . . 8 ⊢ (𝑊 ∈ Grp → 0 ∈ 𝐵)
33	2, 3, 32	3syl 18	. . . . . . 7 ⊢ (𝜑 → 0 ∈ 𝐵)
34		archirng.l	. . . . . . . 8 ⊢ ≤ = (le‘𝑊)
35	7, 34	posref 18276	. . . . . . 7 ⊢ ((𝑊 ∈ Poset ∧ 0 ∈ 𝐵) → 0 ≤ 0 )
36	31, 33, 35	syl2anc 583	. . . . . 6 ⊢ (𝜑 → 0 ≤ 0 )
37	36	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → 0 ≤ 0 )
38		1m1e0 12289	. . . . . . . . . 10 ⊢ (1 − 1) = 0
39	38	negeqi 11458	. . . . . . . . 9 ⊢ -(1 − 1) = -0
40		ax-1cn 11171	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
41	40, 40	negsubdii 11550	. . . . . . . . 9 ⊢ -(1 − 1) = (-1 + 1)
42		neg0 11511	. . . . . . . . 9 ⊢ -0 = 0
43	39, 41, 42	3eqtr3i 2767	. . . . . . . 8 ⊢ (-1 + 1) = 0
44	43	oveq1i 7422	. . . . . . 7 ⊢ ((-1 + 1) · 𝑋) = (0 · 𝑋)
45	7, 18, 8	mulg0 18994	. . . . . . . 8 ⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 )
46	6, 45	syl 17	. . . . . . 7 ⊢ (𝜑 → (0 · 𝑋) = 0 )
47	44, 46	eqtrid 2783	. . . . . 6 ⊢ (𝜑 → ((-1 + 1) · 𝑋) = 0 )
48	47	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → ((-1 + 1) · 𝑋) = 0 )
49	37, 24, 48	3brtr4d 5181	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → 𝑌 ≤ ((-1 + 1) · 𝑋))
50	25, 49	jca 511	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → ((-1 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-1 + 1) · 𝑋)))
51		oveq1 7419	. . . . . 6 ⊢ (𝑛 = -1 → (𝑛 · 𝑋) = (-1 · 𝑋))
52	51	breq1d 5159	. . . . 5 ⊢ (𝑛 = -1 → ((𝑛 · 𝑋) < 𝑌 ↔ (-1 · 𝑋) < 𝑌))
53		oveq1 7419	. . . . . . 7 ⊢ (𝑛 = -1 → (𝑛 + 1) = (-1 + 1))
54	53	oveq1d 7427	. . . . . 6 ⊢ (𝑛 = -1 → ((𝑛 + 1) · 𝑋) = ((-1 + 1) · 𝑋))
55	54	breq2d 5161	. . . . 5 ⊢ (𝑛 = -1 → (𝑌 ≤ ((𝑛 + 1) · 𝑋) ↔ 𝑌 ≤ ((-1 + 1) · 𝑋)))
56	52, 55	anbi12d 630	. . . 4 ⊢ (𝑛 = -1 → (((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) ↔ ((-1 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-1 + 1) · 𝑋))))
57	56	rspcev 3613	. . 3 ⊢ ((-1 ∈ ℤ ∧ ((-1 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-1 + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))
58	1, 50, 57	sylancr 586	. 2 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))
59		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 𝑚 ∈ ℕ₀)
60	59	nn0zd 12589	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 𝑚 ∈ ℤ)
61	60	ad2antrr 723	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → 𝑚 ∈ ℤ)
62	61	znegcld 12673	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → -𝑚 ∈ ℤ)
63		2z 12599	. . . . . . 7 ⊢ 2 ∈ ℤ
64	63	a1i 11	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → 2 ∈ ℤ)
65	62, 64	zsubcld 12676	. . . . 5 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → (-𝑚 − 2) ∈ ℤ)
66		nn0cn 12487	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℂ)
67	66	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 𝑚 ∈ ℂ)
68		2cnd 12295	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 2 ∈ ℂ)
69	67, 68	negdi2d 11590	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → -(𝑚 + 2) = (-𝑚 − 2))
70	69	oveq1d 7427	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (-(𝑚 + 2) · 𝑋) = ((-𝑚 − 2) · 𝑋))
71	2	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 𝑊 ∈ oGrp)
72		archirngz.1	. . . . . . . . . . . 12 ⊢ (𝜑 → (opp_g‘𝑊) ∈ oGrp)
73	72	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (opp_g‘𝑊) ∈ oGrp)
74	71, 73	jca 511	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (𝑊 ∈ oGrp ∧ (opp_g‘𝑊) ∈ oGrp))
75	4	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 𝑊 ∈ Grp)
76	60	peano2zd 12674	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (𝑚 + 1) ∈ ℤ)
77	6	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 𝑋 ∈ 𝐵)
78	7, 8	mulgcl 19008	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑚 + 1) · 𝑋) ∈ 𝐵)
79	75, 76, 77, 78	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((𝑚 + 1) · 𝑋) ∈ 𝐵)
80	63	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 2 ∈ ℤ)
81	60, 80	zaddcld 12675	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (𝑚 + 2) ∈ ℤ)
82	7, 8	mulgcl 19008	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 2) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑚 + 2) · 𝑋) ∈ 𝐵)
83	75, 81, 77, 82	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((𝑚 + 2) · 𝑋) ∈ 𝐵)
84	75, 32	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 0 ∈ 𝐵)
85	16	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 0 < 𝑋)
86		eqid 2731	. . . . . . . . . . . . 13 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
87	7, 17, 86	ogrpaddlt 32502	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ oGrp ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ 0 < 𝑋) → ( 0 (+_g‘𝑊)((𝑚 + 1) · 𝑋)) < (𝑋(+_g‘𝑊)((𝑚 + 1) · 𝑋)))
88	71, 84, 77, 79, 85, 87	syl131anc 1382	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ( 0 (+_g‘𝑊)((𝑚 + 1) · 𝑋)) < (𝑋(+_g‘𝑊)((𝑚 + 1) · 𝑋)))
89	7, 86, 18	grplid 18889	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Grp ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → ( 0 (+_g‘𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) · 𝑋))
90	75, 79, 89	syl2anc 583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ( 0 (+_g‘𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) · 𝑋))
91		1cnd 11214	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ₀ → 1 ∈ ℂ)
92	66, 91, 91	addassd 11241	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) = (𝑚 + (1 + 1)))
93		1p1e2 12342	. . . . . . . . . . . . . . . . 17 ⊢ (1 + 1) = 2
94	93	oveq2i 7423	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 + (1 + 1)) = (𝑚 + 2)
95	92, 94	eqtrdi 2787	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) = (𝑚 + 2))
96	66, 91	addcld 11238	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℂ)
97	96, 91	addcomd 11421	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) = (1 + (𝑚 + 1)))
98	95, 97	eqtr3d 2773	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 2) = (1 + (𝑚 + 1)))
99	98	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 2) · 𝑋) = ((1 + (𝑚 + 1)) · 𝑋))
100	99	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((𝑚 + 2) · 𝑋) = ((1 + (𝑚 + 1)) · 𝑋))
101		1zzd 12598	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 1 ∈ ℤ)
102	7, 8, 86	mulgdir 19023	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ Grp ∧ (1 ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((1 + (𝑚 + 1)) · 𝑋) = ((1 · 𝑋)(+_g‘𝑊)((𝑚 + 1) · 𝑋)))
103	75, 101, 76, 77, 102	syl13anc 1371	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((1 + (𝑚 + 1)) · 𝑋) = ((1 · 𝑋)(+_g‘𝑊)((𝑚 + 1) · 𝑋)))
104	77, 12	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (1 · 𝑋) = 𝑋)
105	104	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((1 · 𝑋)(+_g‘𝑊)((𝑚 + 1) · 𝑋)) = (𝑋(+_g‘𝑊)((𝑚 + 1) · 𝑋)))
106	100, 103, 105	3eqtrrd 2776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (𝑋(+_g‘𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 2) · 𝑋))
107	88, 90, 106	3brtr3d 5180	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋))
108	7, 17, 9	ogrpinvlt 32508	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ oGrp ∧ (opp_g‘𝑊) ∈ oGrp) ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((𝑚 + 2) · 𝑋) ∈ 𝐵) → (((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋) ↔ ((inv_g‘𝑊)‘((𝑚 + 2) · 𝑋)) < ((inv_g‘𝑊)‘((𝑚 + 1) · 𝑋))))
109	108	biimpa 476	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ oGrp ∧ (opp_g‘𝑊) ∈ oGrp) ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((𝑚 + 2) · 𝑋) ∈ 𝐵) ∧ ((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋)) → ((inv_g‘𝑊)‘((𝑚 + 2) · 𝑋)) < ((inv_g‘𝑊)‘((𝑚 + 1) · 𝑋)))
110	74, 79, 83, 107, 109	syl31anc 1372	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((inv_g‘𝑊)‘((𝑚 + 2) · 𝑋)) < ((inv_g‘𝑊)‘((𝑚 + 1) · 𝑋)))
111	7, 8, 9	mulgneg 19009	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 2) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-(𝑚 + 2) · 𝑋) = ((inv_g‘𝑊)‘((𝑚 + 2) · 𝑋)))
112	75, 81, 77, 111	syl3anc 1370	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (-(𝑚 + 2) · 𝑋) = ((inv_g‘𝑊)‘((𝑚 + 2) · 𝑋)))
113	7, 8, 9	mulgneg 19009	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-(𝑚 + 1) · 𝑋) = ((inv_g‘𝑊)‘((𝑚 + 1) · 𝑋)))
114	75, 76, 77, 113	syl3anc 1370	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (-(𝑚 + 1) · 𝑋) = ((inv_g‘𝑊)‘((𝑚 + 1) · 𝑋)))
115	110, 112, 114	3brtr4d 5181	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (-(𝑚 + 2) · 𝑋) < (-(𝑚 + 1) · 𝑋))
116	70, 115	eqbrtrrd 5173	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((-𝑚 − 2) · 𝑋) < (-(𝑚 + 1) · 𝑋))
117	116	ad2antrr 723	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → ((-𝑚 − 2) · 𝑋) < (-(𝑚 + 1) · 𝑋))
118	114	ad2antrr 723	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → (-(𝑚 + 1) · 𝑋) = ((inv_g‘𝑊)‘((𝑚 + 1) · 𝑋)))
119	31	ad4antr 729	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → 𝑊 ∈ Poset)
120		archirng.4	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
121	7, 9	grpinvcl 18909	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝐵) → ((inv_g‘𝑊)‘𝑌) ∈ 𝐵)
122	4, 120, 121	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜑 → ((inv_g‘𝑊)‘𝑌) ∈ 𝐵)
123	122	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((inv_g‘𝑊)‘𝑌) ∈ 𝐵)
124	123	ad2antrr 723	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → ((inv_g‘𝑊)‘𝑌) ∈ 𝐵)
125	79	ad2antrr 723	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → ((𝑚 + 1) · 𝑋) ∈ 𝐵)
126		simplrr 775	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))
127		simpr 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌))
128	7, 34	posasymb 18277	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Poset ∧ ((inv_g‘𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → ((((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) ↔ ((inv_g‘𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋)))
129	128	biimpa 476	. . . . . . . . 9 ⊢ (((𝑊 ∈ Poset ∧ ((inv_g‘𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ (((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌))) → ((inv_g‘𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋))
130	119, 124, 125, 126, 127, 129	syl32anc 1377	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → ((inv_g‘𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋))
131	130	fveq2d 6896	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) = ((inv_g‘𝑊)‘((𝑚 + 1) · 𝑋)))
132	7, 9	grpinvinv 18927	. . . . . . . . 9 ⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝐵) → ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) = 𝑌)
133	4, 120, 132	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) = 𝑌)
134	133	ad4antr 729	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) = 𝑌)
135	118, 131, 134	3eqtr2rd 2778	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → 𝑌 = (-(𝑚 + 1) · 𝑋))
136	117, 135	breqtrrd 5177	. . . . 5 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → ((-𝑚 − 2) · 𝑋) < 𝑌)
137		1cnd 11214	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 1 ∈ ℂ)
138	67, 68, 137	addsubassd 11596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((𝑚 + 2) − 1) = (𝑚 + (2 − 1)))
139		2m1e1 12343	. . . . . . . . . . . . 13 ⊢ (2 − 1) = 1
140	139	oveq2i 7423	. . . . . . . . . . . 12 ⊢ (𝑚 + (2 − 1)) = (𝑚 + 1)
141	138, 140	eqtr2di 2788	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (𝑚 + 1) = ((𝑚 + 2) − 1))
142	141	negeqd 11459	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → -(𝑚 + 1) = -((𝑚 + 2) − 1))
143	67, 68	addcld 11238	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (𝑚 + 2) ∈ ℂ)
144	143, 137	negsubdid 11591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → -((𝑚 + 2) − 1) = (-(𝑚 + 2) + 1))
145	69	oveq1d 7427	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (-(𝑚 + 2) + 1) = ((-𝑚 − 2) + 1))
146	142, 144, 145	3eqtrrd 2776	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((-𝑚 − 2) + 1) = -(𝑚 + 1))
147	146	oveq1d 7427	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (((-𝑚 − 2) + 1) · 𝑋) = (-(𝑚 + 1) · 𝑋))
148	29	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 𝑊 ∈ Toset)
149	148, 30	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → 𝑊 ∈ Poset)
150	60	znegcld 12673	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → -𝑚 ∈ ℤ)
151	150, 80	zsubcld 12676	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (-𝑚 − 2) ∈ ℤ)
152	151	peano2zd 12674	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((-𝑚 − 2) + 1) ∈ ℤ)
153	7, 8	mulgcl 19008	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Grp ∧ ((-𝑚 − 2) + 1) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵)
154	75, 152, 77, 153	syl3anc 1370	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵)
155	7, 34	posref 18276	. . . . . . . . 9 ⊢ ((𝑊 ∈ Poset ∧ (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵) → (((-𝑚 − 2) + 1) · 𝑋) ≤ (((-𝑚 − 2) + 1) · 𝑋))
156	149, 154, 155	syl2anc 583	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (((-𝑚 − 2) + 1) · 𝑋) ≤ (((-𝑚 − 2) + 1) · 𝑋))
157	147, 156	eqbrtrrd 5173	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (-(𝑚 + 1) · 𝑋) ≤ (((-𝑚 − 2) + 1) · 𝑋))
158	157	ad2antrr 723	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → (-(𝑚 + 1) · 𝑋) ≤ (((-𝑚 − 2) + 1) · 𝑋))
159	135, 158	eqbrtrd 5171	. . . . 5 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → 𝑌 ≤ (((-𝑚 − 2) + 1) · 𝑋))
160		oveq1 7419	. . . . . . . 8 ⊢ (𝑛 = (-𝑚 − 2) → (𝑛 · 𝑋) = ((-𝑚 − 2) · 𝑋))
161	160	breq1d 5159	. . . . . . 7 ⊢ (𝑛 = (-𝑚 − 2) → ((𝑛 · 𝑋) < 𝑌 ↔ ((-𝑚 − 2) · 𝑋) < 𝑌))
162		oveq1 7419	. . . . . . . . 9 ⊢ (𝑛 = (-𝑚 − 2) → (𝑛 + 1) = ((-𝑚 − 2) + 1))
163	162	oveq1d 7427	. . . . . . . 8 ⊢ (𝑛 = (-𝑚 − 2) → ((𝑛 + 1) · 𝑋) = (((-𝑚 − 2) + 1) · 𝑋))
164	163	breq2d 5161	. . . . . . 7 ⊢ (𝑛 = (-𝑚 − 2) → (𝑌 ≤ ((𝑛 + 1) · 𝑋) ↔ 𝑌 ≤ (((-𝑚 − 2) + 1) · 𝑋)))
165	161, 164	anbi12d 630	. . . . . 6 ⊢ (𝑛 = (-𝑚 − 2) → (((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) ↔ (((-𝑚 − 2) · 𝑋) < 𝑌 ∧ 𝑌 ≤ (((-𝑚 − 2) + 1) · 𝑋))))
166	165	rspcev 3613	. . . . 5 ⊢ (((-𝑚 − 2) ∈ ℤ ∧ (((-𝑚 − 2) · 𝑋) < 𝑌 ∧ 𝑌 ≤ (((-𝑚 − 2) + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))
167	65, 136, 159, 166	syl12anc 834	. . . 4 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))
168	76	ad2antrr 723	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (𝑚 + 1) ∈ ℤ)
169	168	znegcld 12673	. . . . 5 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → -(𝑚 + 1) ∈ ℤ)
170	2	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ (𝑚 ∈ ℕ₀ ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋)) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) → 𝑊 ∈ oGrp)
171	72	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ (𝑚 ∈ ℕ₀ ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋)) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) → (opp_g‘𝑊) ∈ oGrp)
172	170, 171	jca 511	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ (𝑚 ∈ ℕ₀ ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋)) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) → (𝑊 ∈ oGrp ∧ (opp_g‘𝑊) ∈ oGrp))
173	172	3anassrs 1359	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (𝑊 ∈ oGrp ∧ (opp_g‘𝑊) ∈ oGrp))
174	123	ad2antrr 723	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((inv_g‘𝑊)‘𝑌) ∈ 𝐵)
175	79	ad2antrr 723	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((𝑚 + 1) · 𝑋) ∈ 𝐵)
176		simpr 484	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))
177	7, 17, 9	ogrpinvlt 32508	. . . . . . . 8 ⊢ (((𝑊 ∈ oGrp ∧ (opp_g‘𝑊) ∈ oGrp) ∧ ((inv_g‘𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → (((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋) ↔ ((inv_g‘𝑊)‘((𝑚 + 1) · 𝑋)) < ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌))))
178	177	biimpa 476	. . . . . . 7 ⊢ ((((𝑊 ∈ oGrp ∧ (opp_g‘𝑊) ∈ oGrp) ∧ ((inv_g‘𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((inv_g‘𝑊)‘((𝑚 + 1) · 𝑋)) < ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)))
179	173, 174, 175, 176, 178	syl31anc 1372	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((inv_g‘𝑊)‘((𝑚 + 1) · 𝑋)) < ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)))
180	114	ad2antrr 723	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (-(𝑚 + 1) · 𝑋) = ((inv_g‘𝑊)‘((𝑚 + 1) · 𝑋)))
181	180	eqcomd 2737	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((inv_g‘𝑊)‘((𝑚 + 1) · 𝑋)) = (-(𝑚 + 1) · 𝑋))
182	133	ad4antr 729	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) = 𝑌)
183	179, 181, 182	3brtr3d 5180	. . . . 5 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (-(𝑚 + 1) · 𝑋) < 𝑌)
184		simp-4l 780	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝜑)
185	7, 8	mulgcl 19008	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑚 · 𝑋) ∈ 𝐵)
186	75, 60, 77, 185	syl3anc 1370	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (𝑚 · 𝑋) ∈ 𝐵)
187	7, 17, 9	ogrpinvlt 32508	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ oGrp ∧ (opp_g‘𝑊) ∈ oGrp) ∧ (𝑚 · 𝑋) ∈ 𝐵 ∧ ((inv_g‘𝑊)‘𝑌) ∈ 𝐵) → ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ↔ ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) < ((inv_g‘𝑊)‘(𝑚 · 𝑋))))
188	74, 186, 123, 187	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ↔ ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) < ((inv_g‘𝑊)‘(𝑚 · 𝑋))))
189	188	biimpa 476	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ (𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌)) → ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) < ((inv_g‘𝑊)‘(𝑚 · 𝑋)))
190	189	adantrr 714	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) → ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) < ((inv_g‘𝑊)‘(𝑚 · 𝑋)))
191	190	adantr 480	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) < ((inv_g‘𝑊)‘(𝑚 · 𝑋)))
192		negdi 11522	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → -(𝑚 + 1) = (-𝑚 + -1))
193	66, 40, 192	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → -(𝑚 + 1) = (-𝑚 + -1))
194	193	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (-(𝑚 + 1) + 1) = ((-𝑚 + -1) + 1))
195	66	negcld 11563	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → -𝑚 ∈ ℂ)
196	91	negcld 11563	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → -1 ∈ ℂ)
197	195, 196, 91	addassd 11241	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((-𝑚 + -1) + 1) = (-𝑚 + (-1 + 1)))
198	43	oveq2i 7423	. . . . . . . . . . . . . . 15 ⊢ (-𝑚 + (-1 + 1)) = (-𝑚 + 0)
199	198	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (-𝑚 + (-1 + 1)) = (-𝑚 + 0))
200	195	addridd 11419	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (-𝑚 + 0) = -𝑚)
201	197, 199, 200	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((-𝑚 + -1) + 1) = -𝑚)
202	194, 201	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (-(𝑚 + 1) + 1) = -𝑚)
203	202	oveq1d 7427	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((-(𝑚 + 1) + 1) · 𝑋) = (-𝑚 · 𝑋))
204	203	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((-(𝑚 + 1) + 1) · 𝑋) = (-𝑚 · 𝑋))
205	7, 8, 9	mulgneg 19009	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑚 · 𝑋) = ((inv_g‘𝑊)‘(𝑚 · 𝑋)))
206	75, 60, 77, 205	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (-𝑚 · 𝑋) = ((inv_g‘𝑊)‘(𝑚 · 𝑋)))
207	204, 206	eqtrd 2771	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → ((-(𝑚 + 1) + 1) · 𝑋) = ((inv_g‘𝑊)‘(𝑚 · 𝑋)))
208	207	ad2antrr 723	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((-(𝑚 + 1) + 1) · 𝑋) = ((inv_g‘𝑊)‘(𝑚 · 𝑋)))
209	208	eqcomd 2737	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((inv_g‘𝑊)‘(𝑚 · 𝑋)) = ((-(𝑚 + 1) + 1) · 𝑋))
210	191, 182, 209	3brtr3d 5180	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝑌 < ((-(𝑚 + 1) + 1) · 𝑋))
211		ovexd 7447	. . . . . . 7 ⊢ (𝜑 → ((-(𝑚 + 1) + 1) · 𝑋) ∈ V)
212	34, 17	pltle 18291	. . . . . . 7 ⊢ ((𝑊 ∈ oGrp ∧ 𝑌 ∈ 𝐵 ∧ ((-(𝑚 + 1) + 1) · 𝑋) ∈ V) → (𝑌 < ((-(𝑚 + 1) + 1) · 𝑋) → 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋)))
213	2, 120, 211, 212	syl3anc 1370	. . . . . 6 ⊢ (𝜑 → (𝑌 < ((-(𝑚 + 1) + 1) · 𝑋) → 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋)))
214	184, 210, 213	sylc 65	. . . . 5 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋))
215		oveq1 7419	. . . . . . . 8 ⊢ (𝑛 = -(𝑚 + 1) → (𝑛 · 𝑋) = (-(𝑚 + 1) · 𝑋))
216	215	breq1d 5159	. . . . . . 7 ⊢ (𝑛 = -(𝑚 + 1) → ((𝑛 · 𝑋) < 𝑌 ↔ (-(𝑚 + 1) · 𝑋) < 𝑌))
217		oveq1 7419	. . . . . . . . 9 ⊢ (𝑛 = -(𝑚 + 1) → (𝑛 + 1) = (-(𝑚 + 1) + 1))
218	217	oveq1d 7427	. . . . . . . 8 ⊢ (𝑛 = -(𝑚 + 1) → ((𝑛 + 1) · 𝑋) = ((-(𝑚 + 1) + 1) · 𝑋))
219	218	breq2d 5161	. . . . . . 7 ⊢ (𝑛 = -(𝑚 + 1) → (𝑌 ≤ ((𝑛 + 1) · 𝑋) ↔ 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋)))
220	216, 219	anbi12d 630	. . . . . 6 ⊢ (𝑛 = -(𝑚 + 1) → (((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) ↔ ((-(𝑚 + 1) · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋))))
221	220	rspcev 3613	. . . . 5 ⊢ ((-(𝑚 + 1) ∈ ℤ ∧ ((-(𝑚 + 1) · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))
222	169, 183, 214, 221	syl12anc 834	. . . 4 ⊢ (((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))
223	7, 34, 17	tlt2 32403	. . . . . 6 ⊢ ((𝑊 ∈ Toset ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((inv_g‘𝑊)‘𝑌) ∈ 𝐵) → (((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌) ∨ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)))
224	148, 79, 123, 223	syl3anc 1370	. . . . 5 ⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) → (((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌) ∨ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)))
225	224	adantr 480	. . . 4 ⊢ ((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) → (((𝑚 + 1) · 𝑋) ≤ ((inv_g‘𝑊)‘𝑌) ∨ ((inv_g‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)))
226	167, 222, 225	mpjaodan 956	. . 3 ⊢ ((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ₀) ∧ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))
227	2	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑌 < 0 ) → 𝑊 ∈ oGrp)
228		archirng.2	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ Archi)
229	228	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑌 < 0 ) → 𝑊 ∈ Archi)
230	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑌 < 0 ) → 𝑋 ∈ 𝐵)
231	122	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑌 < 0 ) → ((inv_g‘𝑊)‘𝑌) ∈ 𝐵)
232	16	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑌 < 0 ) → 0 < 𝑋)
233	133	breq1d 5159	. . . . . 6 ⊢ (𝜑 → (((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) < 0 ↔ 𝑌 < 0 ))
234	233	biimpar 477	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 < 0 ) → ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) < 0 )
235	7, 17, 9, 18	ogrpinv0lt 32507	. . . . . . 7 ⊢ ((𝑊 ∈ oGrp ∧ ((inv_g‘𝑊)‘𝑌) ∈ 𝐵) → ( 0 < ((inv_g‘𝑊)‘𝑌) ↔ ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) < 0 ))
236	2, 122, 235	syl2anc 583	. . . . . 6 ⊢ (𝜑 → ( 0 < ((inv_g‘𝑊)‘𝑌) ↔ ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) < 0 ))
237	236	biimpar 477	. . . . 5 ⊢ ((𝜑 ∧ ((inv_g‘𝑊)‘((inv_g‘𝑊)‘𝑌)) < 0 ) → 0 < ((inv_g‘𝑊)‘𝑌))
238	234, 237	syldan 590	. . . 4 ⊢ ((𝜑 ∧ 𝑌 < 0 ) → 0 < ((inv_g‘𝑊)‘𝑌))
239	7, 18, 17, 34, 8, 227, 229, 230, 231, 232, 238	archirng 32601	. . 3 ⊢ ((𝜑 ∧ 𝑌 < 0 ) → ∃𝑚 ∈ ℕ₀ ((𝑚 · 𝑋) < ((inv_g‘𝑊)‘𝑌) ∧ ((inv_g‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋)))
240	226, 239	r19.29a 3161	. 2 ⊢ ((𝜑 ∧ 𝑌 < 0 ) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))
241		nn0ssz 12586	. . 3 ⊢ ℕ₀ ⊆ ℤ
242	2	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 0 < 𝑌) → 𝑊 ∈ oGrp)
243	228	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 0 < 𝑌) → 𝑊 ∈ Archi)
244	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 0 < 𝑌) → 𝑋 ∈ 𝐵)
245	120	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 0 < 𝑌) → 𝑌 ∈ 𝐵)
246	16	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 0 < 𝑌) → 0 < 𝑋)
247		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 0 < 𝑌) → 0 < 𝑌)
248	7, 18, 17, 34, 8, 242, 243, 244, 245, 246, 247	archirng 32601	. . 3 ⊢ ((𝜑 ∧ 0 < 𝑌) → ∃𝑛 ∈ ℕ₀ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))
249		ssrexv 4052	. . 3 ⊢ (ℕ₀ ⊆ ℤ → (∃𝑛 ∈ ℕ₀ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))))
250	241, 248, 249	mpsyl 68	. 2 ⊢ ((𝜑 ∧ 0 < 𝑌) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))
251	7, 17	tlt3 32404	. . 3 ⊢ ((𝑊 ∈ Toset ∧ 𝑌 ∈ 𝐵 ∧ 0 ∈ 𝐵) → (𝑌 = 0 ∨ 𝑌 < 0 ∨ 0 < 𝑌))
252	29, 120, 33, 251	syl3anc 1370	. 2 ⊢ (𝜑 → (𝑌 = 0 ∨ 𝑌 < 0 ∨ 0 < 𝑌))
253	58, 240, 250, 252	mpjao3dan 1430	1 ⊢ (𝜑 → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 844 ∨ w3o 1085 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ∃wrex 3069 Vcvv 3473 ⊆ wss 3949 class class class wbr 5149 ‘cfv 6544 (class class class)co 7412 ℂcc 11111 0cc0 11113 1c1 11114 + caddc 11116 − cmin 11449 -cneg 11450 2c2 12272 ℕ₀cn0 12477 ℤcz 12563 Basecbs 17149 +_gcplusg 17202 lecple 17209 0_gc0g 17390 Posetcpo 18265 ltcplt 18266 Tosetctos 18374 Grpcgrp 18856 inv_gcminusg 18857 ._gcmg 18987 opp_gcoppg 19251 oMndcomnd 32482 oGrpcogrp 32483 Archicarchi 32590

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7728 ax-cnex 11169 ax-resscn 11170 ax-1cn 11171 ax-icn 11172 ax-addcl 11173 ax-addrcl 11174 ax-mulcl 11175 ax-mulrcl 11176 ax-mulcom 11177 ax-addass 11178 ax-mulass 11179 ax-distr 11180 ax-i2m1 11181 ax-1ne0 11182 ax-1rid 11183 ax-rnegex 11184 ax-rrecex 11185 ax-cnre 11186 ax-pre-lttri 11187 ax-pre-lttrn 11188 ax-pre-ltadd 11189 ax-pre-mulgt0 11190

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7859 df-1st 7978 df-2nd 7979 df-tpos 8214 df-frecs 8269 df-wrecs 8300 df-recs 8374 df-rdg 8413 df-er 8706 df-en 8943 df-dom 8944 df-sdom 8945 df-pnf 11255 df-mnf 11256 df-xr 11257 df-ltxr 11258 df-le 11259 df-sub 11451 df-neg 11452 df-nn 12218 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12478 df-z 12564 df-dec 12683 df-uz 12828 df-fz 13490 df-seq 13972 df-sets 17102 df-slot 17120 df-ndx 17132 df-base 17150 df-plusg 17215 df-ple 17222 df-0g 17392 df-proset 18253 df-poset 18271 df-plt 18288 df-toset 18375 df-mgm 18566 df-sgrp 18645 df-mnd 18661 df-grp 18859 df-minusg 18860 df-mulg 18988 df-oppg 19252 df-omnd 32484 df-ogrp 32485 df-inftm 32591 df-archi 32592

This theorem is referenced by: archiabllem2c 32608

W3C validator