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

Theorem archirngz 32313
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 = (0g𝑊)
archirng.i < = (lt‘𝑊)
archirng.l = (le‘𝑊)
archirng.x · = (.g𝑊)
archirng.1 (𝜑𝑊 ∈ oGrp)
archirng.2 (𝜑𝑊 ∈ Archi)
archirng.3 (𝜑𝑋𝐵)
archirng.4 (𝜑𝑌𝐵)
archirng.5 (𝜑0 < 𝑋)
archirngz.1 (𝜑 → (oppg𝑊) ∈ 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.
StepHypRef Expression
1 neg1z 12594 . . 3 -1 ∈ ℤ
2 archirng.1 . . . . . . . . . 10 (𝜑𝑊 ∈ oGrp)
3 ogrpgrp 32199 . . . . . . . . . 10 (𝑊 ∈ oGrp → 𝑊 ∈ Grp)
42, 3syl 17 . . . . . . . . 9 (𝜑𝑊 ∈ Grp)
5 1zzd 12589 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
6 archirng.3 . . . . . . . . 9 (𝜑𝑋𝐵)
7 archirng.b . . . . . . . . . 10 𝐵 = (Base‘𝑊)
8 archirng.x . . . . . . . . . 10 · = (.g𝑊)
9 eqid 2733 . . . . . . . . . 10 (invg𝑊) = (invg𝑊)
107, 8, 9mulgneg 18966 . . . . . . . . 9 ((𝑊 ∈ Grp ∧ 1 ∈ ℤ ∧ 𝑋𝐵) → (-1 · 𝑋) = ((invg𝑊)‘(1 · 𝑋)))
114, 5, 6, 10syl3anc 1372 . . . . . . . 8 (𝜑 → (-1 · 𝑋) = ((invg𝑊)‘(1 · 𝑋)))
127, 8mulg1 18955 . . . . . . . . . 10 (𝑋𝐵 → (1 · 𝑋) = 𝑋)
136, 12syl 17 . . . . . . . . 9 (𝜑 → (1 · 𝑋) = 𝑋)
1413fveq2d 6892 . . . . . . . 8 (𝜑 → ((invg𝑊)‘(1 · 𝑋)) = ((invg𝑊)‘𝑋))
1511, 14eqtrd 2773 . . . . . . 7 (𝜑 → (-1 · 𝑋) = ((invg𝑊)‘𝑋))
16 archirng.5 . . . . . . . 8 (𝜑0 < 𝑋)
17 archirng.i . . . . . . . . . 10 < = (lt‘𝑊)
18 archirng.0 . . . . . . . . . 10 0 = (0g𝑊)
197, 17, 9, 18ogrpinv0lt 32218 . . . . . . . . 9 ((𝑊 ∈ oGrp ∧ 𝑋𝐵) → ( 0 < 𝑋 ↔ ((invg𝑊)‘𝑋) < 0 ))
2019biimpa 478 . . . . . . . 8 (((𝑊 ∈ oGrp ∧ 𝑋𝐵) ∧ 0 < 𝑋) → ((invg𝑊)‘𝑋) < 0 )
212, 6, 16, 20syl21anc 837 . . . . . . 7 (𝜑 → ((invg𝑊)‘𝑋) < 0 )
2215, 21eqbrtrd 5169 . . . . . 6 (𝜑 → (-1 · 𝑋) < 0 )
2322adantr 482 . . . . 5 ((𝜑𝑌 = 0 ) → (-1 · 𝑋) < 0 )
24 simpr 486 . . . . 5 ((𝜑𝑌 = 0 ) → 𝑌 = 0 )
2523, 24breqtrrd 5175 . . . 4 ((𝜑𝑌 = 0 ) → (-1 · 𝑋) < 𝑌)
26 isogrp 32198 . . . . . . . . . 10 (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd))
2726simprbi 498 . . . . . . . . 9 (𝑊 ∈ oGrp → 𝑊 ∈ oMnd)
28 omndtos 32201 . . . . . . . . 9 (𝑊 ∈ oMnd → 𝑊 ∈ Toset)
292, 27, 283syl 18 . . . . . . . 8 (𝜑𝑊 ∈ Toset)
30 tospos 18369 . . . . . . . 8 (𝑊 ∈ Toset → 𝑊 ∈ Poset)
3129, 30syl 17 . . . . . . 7 (𝜑𝑊 ∈ Poset)
327, 18grpidcl 18846 . . . . . . . 8 (𝑊 ∈ Grp → 0𝐵)
332, 3, 323syl 18 . . . . . . 7 (𝜑0𝐵)
34 archirng.l . . . . . . . 8 = (le‘𝑊)
357, 34posref 18267 . . . . . . 7 ((𝑊 ∈ Poset ∧ 0𝐵) → 0 0 )
3631, 33, 35syl2anc 585 . . . . . 6 (𝜑0 0 )
3736adantr 482 . . . . 5 ((𝜑𝑌 = 0 ) → 0 0 )
38 1m1e0 12280 . . . . . . . . . 10 (1 − 1) = 0
3938negeqi 11449 . . . . . . . . 9 -(1 − 1) = -0
40 ax-1cn 11164 . . . . . . . . . 10 1 ∈ ℂ
4140, 40negsubdii 11541 . . . . . . . . 9 -(1 − 1) = (-1 + 1)
42 neg0 11502 . . . . . . . . 9 -0 = 0
4339, 41, 423eqtr3i 2769 . . . . . . . 8 (-1 + 1) = 0
4443oveq1i 7414 . . . . . . 7 ((-1 + 1) · 𝑋) = (0 · 𝑋)
457, 18, 8mulg0 18951 . . . . . . . 8 (𝑋𝐵 → (0 · 𝑋) = 0 )
466, 45syl 17 . . . . . . 7 (𝜑 → (0 · 𝑋) = 0 )
4744, 46eqtrid 2785 . . . . . 6 (𝜑 → ((-1 + 1) · 𝑋) = 0 )
4847adantr 482 . . . . 5 ((𝜑𝑌 = 0 ) → ((-1 + 1) · 𝑋) = 0 )
4937, 24, 483brtr4d 5179 . . . 4 ((𝜑𝑌 = 0 ) → 𝑌 ((-1 + 1) · 𝑋))
5025, 49jca 513 . . 3 ((𝜑𝑌 = 0 ) → ((-1 · 𝑋) < 𝑌𝑌 ((-1 + 1) · 𝑋)))
51 oveq1 7411 . . . . . 6 (𝑛 = -1 → (𝑛 · 𝑋) = (-1 · 𝑋))
5251breq1d 5157 . . . . 5 (𝑛 = -1 → ((𝑛 · 𝑋) < 𝑌 ↔ (-1 · 𝑋) < 𝑌))
53 oveq1 7411 . . . . . . 7 (𝑛 = -1 → (𝑛 + 1) = (-1 + 1))
5453oveq1d 7419 . . . . . 6 (𝑛 = -1 → ((𝑛 + 1) · 𝑋) = ((-1 + 1) · 𝑋))
5554breq2d 5159 . . . . 5 (𝑛 = -1 → (𝑌 ((𝑛 + 1) · 𝑋) ↔ 𝑌 ((-1 + 1) · 𝑋)))
5652, 55anbi12d 632 . . . 4 (𝑛 = -1 → (((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)) ↔ ((-1 · 𝑋) < 𝑌𝑌 ((-1 + 1) · 𝑋))))
5756rspcev 3612 . . 3 ((-1 ∈ ℤ ∧ ((-1 · 𝑋) < 𝑌𝑌 ((-1 + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
581, 50, 57sylancr 588 . 2 ((𝜑𝑌 = 0 ) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
59 simpr 486 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
6059nn0zd 12580 . . . . . . . 8 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℤ)
6160ad2antrr 725 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → 𝑚 ∈ ℤ)
6261znegcld 12664 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → -𝑚 ∈ ℤ)
63 2z 12590 . . . . . . 7 2 ∈ ℤ
6463a1i 11 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → 2 ∈ ℤ)
6562, 64zsubcld 12667 . . . . 5 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → (-𝑚 − 2) ∈ ℤ)
66 nn0cn 12478 . . . . . . . . . . 11 (𝑚 ∈ ℕ0𝑚 ∈ ℂ)
6766adantl 483 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℂ)
68 2cnd 12286 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 2 ∈ ℂ)
6967, 68negdi2d 11581 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -(𝑚 + 2) = (-𝑚 − 2))
7069oveq1d 7419 . . . . . . . 8 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) · 𝑋) = ((-𝑚 − 2) · 𝑋))
712ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ oGrp)
72 archirngz.1 . . . . . . . . . . . 12 (𝜑 → (oppg𝑊) ∈ oGrp)
7372ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (oppg𝑊) ∈ oGrp)
7471, 73jca 513 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp))
754ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ Grp)
7660peano2zd 12665 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈ ℤ)
776ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑋𝐵)
787, 8mulgcl 18965 . . . . . . . . . . 11 ((𝑊 ∈ Grp ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋𝐵) → ((𝑚 + 1) · 𝑋) ∈ 𝐵)
7975, 76, 77, 78syl3anc 1372 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · 𝑋) ∈ 𝐵)
8063a1i 11 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 2 ∈ ℤ)
8160, 80zaddcld 12666 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 2) ∈ ℤ)
827, 8mulgcl 18965 . . . . . . . . . . 11 ((𝑊 ∈ Grp ∧ (𝑚 + 2) ∈ ℤ ∧ 𝑋𝐵) → ((𝑚 + 2) · 𝑋) ∈ 𝐵)
8375, 81, 77, 82syl3anc 1372 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 2) · 𝑋) ∈ 𝐵)
8475, 32syl 17 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 0𝐵)
8516ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 0 < 𝑋)
86 eqid 2733 . . . . . . . . . . . . 13 (+g𝑊) = (+g𝑊)
877, 17, 86ogrpaddlt 32213 . . . . . . . . . . . 12 ((𝑊 ∈ oGrp ∧ ( 0𝐵𝑋𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ 0 < 𝑋) → ( 0 (+g𝑊)((𝑚 + 1) · 𝑋)) < (𝑋(+g𝑊)((𝑚 + 1) · 𝑋)))
8871, 84, 77, 79, 85, 87syl131anc 1384 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ( 0 (+g𝑊)((𝑚 + 1) · 𝑋)) < (𝑋(+g𝑊)((𝑚 + 1) · 𝑋)))
897, 86, 18grplid 18848 . . . . . . . . . . . 12 ((𝑊 ∈ Grp ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → ( 0 (+g𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) · 𝑋))
9075, 79, 89syl2anc 585 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ( 0 (+g𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) · 𝑋))
91 1cnd 11205 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ0 → 1 ∈ ℂ)
9266, 91, 91addassd 11232 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ0 → ((𝑚 + 1) + 1) = (𝑚 + (1 + 1)))
93 1p1e2 12333 . . . . . . . . . . . . . . . . 17 (1 + 1) = 2
9493oveq2i 7415 . . . . . . . . . . . . . . . 16 (𝑚 + (1 + 1)) = (𝑚 + 2)
9592, 94eqtrdi 2789 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → ((𝑚 + 1) + 1) = (𝑚 + 2))
9666, 91addcld 11229 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ0 → (𝑚 + 1) ∈ ℂ)
9796, 91addcomd 11412 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → ((𝑚 + 1) + 1) = (1 + (𝑚 + 1)))
9895, 97eqtr3d 2775 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → (𝑚 + 2) = (1 + (𝑚 + 1)))
9998oveq1d 7419 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ0 → ((𝑚 + 2) · 𝑋) = ((1 + (𝑚 + 1)) · 𝑋))
10099adantl 483 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 2) · 𝑋) = ((1 + (𝑚 + 1)) · 𝑋))
101 1zzd 12589 . . . . . . . . . . . . 13 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 1 ∈ ℤ)
1027, 8, 86mulgdir 18980 . . . . . . . . . . . . 13 ((𝑊 ∈ Grp ∧ (1 ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋𝐵)) → ((1 + (𝑚 + 1)) · 𝑋) = ((1 · 𝑋)(+g𝑊)((𝑚 + 1) · 𝑋)))
10375, 101, 76, 77, 102syl13anc 1373 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((1 + (𝑚 + 1)) · 𝑋) = ((1 · 𝑋)(+g𝑊)((𝑚 + 1) · 𝑋)))
10477, 12syl 17 . . . . . . . . . . . . 13 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (1 · 𝑋) = 𝑋)
105104oveq1d 7419 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((1 · 𝑋)(+g𝑊)((𝑚 + 1) · 𝑋)) = (𝑋(+g𝑊)((𝑚 + 1) · 𝑋)))
106100, 103, 1053eqtrrd 2778 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑋(+g𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 2) · 𝑋))
10788, 90, 1063brtr3d 5178 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋))
1087, 17, 9ogrpinvlt 32219 . . . . . . . . . . 11 (((𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp) ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((𝑚 + 2) · 𝑋) ∈ 𝐵) → (((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋) ↔ ((invg𝑊)‘((𝑚 + 2) · 𝑋)) < ((invg𝑊)‘((𝑚 + 1) · 𝑋))))
109108biimpa 478 . . . . . . . . . 10 ((((𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp) ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((𝑚 + 2) · 𝑋) ∈ 𝐵) ∧ ((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋)) → ((invg𝑊)‘((𝑚 + 2) · 𝑋)) < ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
11074, 79, 83, 107, 109syl31anc 1374 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((invg𝑊)‘((𝑚 + 2) · 𝑋)) < ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
1117, 8, 9mulgneg 18966 . . . . . . . . . 10 ((𝑊 ∈ Grp ∧ (𝑚 + 2) ∈ ℤ ∧ 𝑋𝐵) → (-(𝑚 + 2) · 𝑋) = ((invg𝑊)‘((𝑚 + 2) · 𝑋)))
11275, 81, 77, 111syl3anc 1372 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) · 𝑋) = ((invg𝑊)‘((𝑚 + 2) · 𝑋)))
1137, 8, 9mulgneg 18966 . . . . . . . . . 10 ((𝑊 ∈ Grp ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋𝐵) → (-(𝑚 + 1) · 𝑋) = ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
11475, 76, 77, 113syl3anc 1372 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 1) · 𝑋) = ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
115110, 112, 1143brtr4d 5179 . . . . . . . 8 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) · 𝑋) < (-(𝑚 + 1) · 𝑋))
11670, 115eqbrtrrd 5171 . . . . . . 7 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-𝑚 − 2) · 𝑋) < (-(𝑚 + 1) · 𝑋))
117116ad2antrr 725 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((-𝑚 − 2) · 𝑋) < (-(𝑚 + 1) · 𝑋))
118114ad2antrr 725 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → (-(𝑚 + 1) · 𝑋) = ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
11931ad4antr 731 . . . . . . . . 9 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → 𝑊 ∈ Poset)
120 archirng.4 . . . . . . . . . . . 12 (𝜑𝑌𝐵)
1217, 9grpinvcl 18868 . . . . . . . . . . . 12 ((𝑊 ∈ Grp ∧ 𝑌𝐵) → ((invg𝑊)‘𝑌) ∈ 𝐵)
1224, 120, 121syl2anc 585 . . . . . . . . . . 11 (𝜑 → ((invg𝑊)‘𝑌) ∈ 𝐵)
123122ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((invg𝑊)‘𝑌) ∈ 𝐵)
124123ad2antrr 725 . . . . . . . . 9 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((invg𝑊)‘𝑌) ∈ 𝐵)
12579ad2antrr 725 . . . . . . . . 9 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((𝑚 + 1) · 𝑋) ∈ 𝐵)
126 simplrr 777 . . . . . . . . 9 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))
127 simpr 486 . . . . . . . . 9 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌))
1287, 34posasymb 18268 . . . . . . . . . 10 ((𝑊 ∈ Poset ∧ ((invg𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → ((((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) ↔ ((invg𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋)))
129128biimpa 478 . . . . . . . . 9 (((𝑊 ∈ Poset ∧ ((invg𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ (((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌))) → ((invg𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋))
130119, 124, 125, 126, 127, 129syl32anc 1379 . . . . . . . 8 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((invg𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋))
131130fveq2d 6892 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((invg𝑊)‘((invg𝑊)‘𝑌)) = ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
1327, 9grpinvinv 18886 . . . . . . . . 9 ((𝑊 ∈ Grp ∧ 𝑌𝐵) → ((invg𝑊)‘((invg𝑊)‘𝑌)) = 𝑌)
1334, 120, 132syl2anc 585 . . . . . . . 8 (𝜑 → ((invg𝑊)‘((invg𝑊)‘𝑌)) = 𝑌)
134133ad4antr 731 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((invg𝑊)‘((invg𝑊)‘𝑌)) = 𝑌)
135118, 131, 1343eqtr2rd 2780 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → 𝑌 = (-(𝑚 + 1) · 𝑋))
136117, 135breqtrrd 5175 . . . . 5 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((-𝑚 − 2) · 𝑋) < 𝑌)
137 1cnd 11205 . . . . . . . . . . . . 13 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 1 ∈ ℂ)
13867, 68, 137addsubassd 11587 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 2) − 1) = (𝑚 + (2 − 1)))
139 2m1e1 12334 . . . . . . . . . . . . 13 (2 − 1) = 1
140139oveq2i 7415 . . . . . . . . . . . 12 (𝑚 + (2 − 1)) = (𝑚 + 1)
141138, 140eqtr2di 2790 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) = ((𝑚 + 2) − 1))
142141negeqd 11450 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -(𝑚 + 1) = -((𝑚 + 2) − 1))
14367, 68addcld 11229 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 2) ∈ ℂ)
144143, 137negsubdid 11582 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -((𝑚 + 2) − 1) = (-(𝑚 + 2) + 1))
14569oveq1d 7419 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) + 1) = ((-𝑚 − 2) + 1))
146142, 144, 1453eqtrrd 2778 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-𝑚 − 2) + 1) = -(𝑚 + 1))
147146oveq1d 7419 . . . . . . . 8 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((-𝑚 − 2) + 1) · 𝑋) = (-(𝑚 + 1) · 𝑋))
14829ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ Toset)
149148, 30syl 17 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ Poset)
15060znegcld 12664 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -𝑚 ∈ ℤ)
151150, 80zsubcld 12667 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-𝑚 − 2) ∈ ℤ)
152151peano2zd 12665 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-𝑚 − 2) + 1) ∈ ℤ)
1537, 8mulgcl 18965 . . . . . . . . . 10 ((𝑊 ∈ Grp ∧ ((-𝑚 − 2) + 1) ∈ ℤ ∧ 𝑋𝐵) → (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵)
15475, 152, 77, 153syl3anc 1372 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵)
1557, 34posref 18267 . . . . . . . . 9 ((𝑊 ∈ Poset ∧ (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵) → (((-𝑚 − 2) + 1) · 𝑋) (((-𝑚 − 2) + 1) · 𝑋))
156149, 154, 155syl2anc 585 . . . . . . . 8 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((-𝑚 − 2) + 1) · 𝑋) (((-𝑚 − 2) + 1) · 𝑋))
157147, 156eqbrtrrd 5171 . . . . . . 7 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 1) · 𝑋) (((-𝑚 − 2) + 1) · 𝑋))
158157ad2antrr 725 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → (-(𝑚 + 1) · 𝑋) (((-𝑚 − 2) + 1) · 𝑋))
159135, 158eqbrtrd 5169 . . . . 5 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → 𝑌 (((-𝑚 − 2) + 1) · 𝑋))
160 oveq1 7411 . . . . . . . 8 (𝑛 = (-𝑚 − 2) → (𝑛 · 𝑋) = ((-𝑚 − 2) · 𝑋))
161160breq1d 5157 . . . . . . 7 (𝑛 = (-𝑚 − 2) → ((𝑛 · 𝑋) < 𝑌 ↔ ((-𝑚 − 2) · 𝑋) < 𝑌))
162 oveq1 7411 . . . . . . . . 9 (𝑛 = (-𝑚 − 2) → (𝑛 + 1) = ((-𝑚 − 2) + 1))
163162oveq1d 7419 . . . . . . . 8 (𝑛 = (-𝑚 − 2) → ((𝑛 + 1) · 𝑋) = (((-𝑚 − 2) + 1) · 𝑋))
164163breq2d 5159 . . . . . . 7 (𝑛 = (-𝑚 − 2) → (𝑌 ((𝑛 + 1) · 𝑋) ↔ 𝑌 (((-𝑚 − 2) + 1) · 𝑋)))
165161, 164anbi12d 632 . . . . . 6 (𝑛 = (-𝑚 − 2) → (((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)) ↔ (((-𝑚 − 2) · 𝑋) < 𝑌𝑌 (((-𝑚 − 2) + 1) · 𝑋))))
166165rspcev 3612 . . . . 5 (((-𝑚 − 2) ∈ ℤ ∧ (((-𝑚 − 2) · 𝑋) < 𝑌𝑌 (((-𝑚 − 2) + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
16765, 136, 159, 166syl12anc 836 . . . 4 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
16876ad2antrr 725 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (𝑚 + 1) ∈ ℤ)
169168znegcld 12664 . . . . 5 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → -(𝑚 + 1) ∈ ℤ)
1702ad2antrr 725 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ (𝑚 ∈ ℕ0 ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋)) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) → 𝑊 ∈ oGrp)
17172ad2antrr 725 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ (𝑚 ∈ ℕ0 ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋)) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) → (oppg𝑊) ∈ oGrp)
172170, 171jca 513 . . . . . . . 8 (((𝜑𝑌 < 0 ) ∧ (𝑚 ∈ ℕ0 ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋)) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) → (𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp))
1731723anassrs 1361 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp))
174123ad2antrr 725 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘𝑌) ∈ 𝐵)
17579ad2antrr 725 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((𝑚 + 1) · 𝑋) ∈ 𝐵)
176 simpr 486 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))
1777, 17, 9ogrpinvlt 32219 . . . . . . . 8 (((𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp) ∧ ((invg𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → (((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋) ↔ ((invg𝑊)‘((𝑚 + 1) · 𝑋)) < ((invg𝑊)‘((invg𝑊)‘𝑌))))
178177biimpa 478 . . . . . . 7 ((((𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp) ∧ ((invg𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘((𝑚 + 1) · 𝑋)) < ((invg𝑊)‘((invg𝑊)‘𝑌)))
179173, 174, 175, 176, 178syl31anc 1374 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘((𝑚 + 1) · 𝑋)) < ((invg𝑊)‘((invg𝑊)‘𝑌)))
180114ad2antrr 725 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (-(𝑚 + 1) · 𝑋) = ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
181180eqcomd 2739 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘((𝑚 + 1) · 𝑋)) = (-(𝑚 + 1) · 𝑋))
182133ad4antr 731 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘((invg𝑊)‘𝑌)) = 𝑌)
183179, 181, 1823brtr3d 5178 . . . . 5 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (-(𝑚 + 1) · 𝑋) < 𝑌)
184 simp-4l 782 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝜑)
1857, 8mulgcl 18965 . . . . . . . . . . . 12 ((𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋𝐵) → (𝑚 · 𝑋) ∈ 𝐵)
18675, 60, 77, 185syl3anc 1372 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 · 𝑋) ∈ 𝐵)
1877, 17, 9ogrpinvlt 32219 . . . . . . . . . . 11 (((𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp) ∧ (𝑚 · 𝑋) ∈ 𝐵 ∧ ((invg𝑊)‘𝑌) ∈ 𝐵) → ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ↔ ((invg𝑊)‘((invg𝑊)‘𝑌)) < ((invg𝑊)‘(𝑚 · 𝑋))))
18874, 186, 123, 187syl3anc 1372 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ↔ ((invg𝑊)‘((invg𝑊)‘𝑌)) < ((invg𝑊)‘(𝑚 · 𝑋))))
189188biimpa 478 . . . . . . . . 9 ((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ (𝑚 · 𝑋) < ((invg𝑊)‘𝑌)) → ((invg𝑊)‘((invg𝑊)‘𝑌)) < ((invg𝑊)‘(𝑚 · 𝑋)))
190189adantrr 716 . . . . . . . 8 ((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) → ((invg𝑊)‘((invg𝑊)‘𝑌)) < ((invg𝑊)‘(𝑚 · 𝑋)))
191190adantr 482 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘((invg𝑊)‘𝑌)) < ((invg𝑊)‘(𝑚 · 𝑋)))
192 negdi 11513 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → -(𝑚 + 1) = (-𝑚 + -1))
19366, 40, 192sylancl 587 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → -(𝑚 + 1) = (-𝑚 + -1))
194193oveq1d 7419 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ0 → (-(𝑚 + 1) + 1) = ((-𝑚 + -1) + 1))
19566negcld 11554 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → -𝑚 ∈ ℂ)
19691negcld 11554 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → -1 ∈ ℂ)
197195, 196, 91addassd 11232 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → ((-𝑚 + -1) + 1) = (-𝑚 + (-1 + 1)))
19843oveq2i 7415 . . . . . . . . . . . . . . 15 (-𝑚 + (-1 + 1)) = (-𝑚 + 0)
199198a1i 11 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → (-𝑚 + (-1 + 1)) = (-𝑚 + 0))
200195addridd 11410 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → (-𝑚 + 0) = -𝑚)
201197, 199, 2003eqtrd 2777 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ0 → ((-𝑚 + -1) + 1) = -𝑚)
202194, 201eqtrd 2773 . . . . . . . . . . . 12 (𝑚 ∈ ℕ0 → (-(𝑚 + 1) + 1) = -𝑚)
203202oveq1d 7419 . . . . . . . . . . 11 (𝑚 ∈ ℕ0 → ((-(𝑚 + 1) + 1) · 𝑋) = (-𝑚 · 𝑋))
204203adantl 483 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-(𝑚 + 1) + 1) · 𝑋) = (-𝑚 · 𝑋))
2057, 8, 9mulgneg 18966 . . . . . . . . . . 11 ((𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋𝐵) → (-𝑚 · 𝑋) = ((invg𝑊)‘(𝑚 · 𝑋)))
20675, 60, 77, 205syl3anc 1372 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-𝑚 · 𝑋) = ((invg𝑊)‘(𝑚 · 𝑋)))
207204, 206eqtrd 2773 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-(𝑚 + 1) + 1) · 𝑋) = ((invg𝑊)‘(𝑚 · 𝑋)))
208207ad2antrr 725 . . . . . . . 8 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((-(𝑚 + 1) + 1) · 𝑋) = ((invg𝑊)‘(𝑚 · 𝑋)))
209208eqcomd 2739 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘(𝑚 · 𝑋)) = ((-(𝑚 + 1) + 1) · 𝑋))
210191, 182, 2093brtr3d 5178 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝑌 < ((-(𝑚 + 1) + 1) · 𝑋))
211 ovexd 7439 . . . . . . 7 (𝜑 → ((-(𝑚 + 1) + 1) · 𝑋) ∈ V)
21234, 17pltle 18282 . . . . . . 7 ((𝑊 ∈ oGrp ∧ 𝑌𝐵 ∧ ((-(𝑚 + 1) + 1) · 𝑋) ∈ V) → (𝑌 < ((-(𝑚 + 1) + 1) · 𝑋) → 𝑌 ((-(𝑚 + 1) + 1) · 𝑋)))
2132, 120, 211, 212syl3anc 1372 . . . . . 6 (𝜑 → (𝑌 < ((-(𝑚 + 1) + 1) · 𝑋) → 𝑌 ((-(𝑚 + 1) + 1) · 𝑋)))
214184, 210, 213sylc 65 . . . . 5 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝑌 ((-(𝑚 + 1) + 1) · 𝑋))
215 oveq1 7411 . . . . . . . 8 (𝑛 = -(𝑚 + 1) → (𝑛 · 𝑋) = (-(𝑚 + 1) · 𝑋))
216215breq1d 5157 . . . . . . 7 (𝑛 = -(𝑚 + 1) → ((𝑛 · 𝑋) < 𝑌 ↔ (-(𝑚 + 1) · 𝑋) < 𝑌))
217 oveq1 7411 . . . . . . . . 9 (𝑛 = -(𝑚 + 1) → (𝑛 + 1) = (-(𝑚 + 1) + 1))
218217oveq1d 7419 . . . . . . . 8 (𝑛 = -(𝑚 + 1) → ((𝑛 + 1) · 𝑋) = ((-(𝑚 + 1) + 1) · 𝑋))
219218breq2d 5159 . . . . . . 7 (𝑛 = -(𝑚 + 1) → (𝑌 ((𝑛 + 1) · 𝑋) ↔ 𝑌 ((-(𝑚 + 1) + 1) · 𝑋)))
220216, 219anbi12d 632 . . . . . 6 (𝑛 = -(𝑚 + 1) → (((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)) ↔ ((-(𝑚 + 1) · 𝑋) < 𝑌𝑌 ((-(𝑚 + 1) + 1) · 𝑋))))
221220rspcev 3612 . . . . 5 ((-(𝑚 + 1) ∈ ℤ ∧ ((-(𝑚 + 1) · 𝑋) < 𝑌𝑌 ((-(𝑚 + 1) + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
222169, 183, 214, 221syl12anc 836 . . . 4 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
2237, 34, 17tlt2 32117 . . . . . 6 ((𝑊 ∈ Toset ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((invg𝑊)‘𝑌) ∈ 𝐵) → (((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌) ∨ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)))
224148, 79, 123, 223syl3anc 1372 . . . . 5 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌) ∨ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)))
225224adantr 482 . . . 4 ((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) → (((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌) ∨ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)))
226167, 222, 225mpjaodan 958 . . 3 ((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
2272adantr 482 . . . 4 ((𝜑𝑌 < 0 ) → 𝑊 ∈ oGrp)
228 archirng.2 . . . . 5 (𝜑𝑊 ∈ Archi)
229228adantr 482 . . . 4 ((𝜑𝑌 < 0 ) → 𝑊 ∈ Archi)
2306adantr 482 . . . 4 ((𝜑𝑌 < 0 ) → 𝑋𝐵)
231122adantr 482 . . . 4 ((𝜑𝑌 < 0 ) → ((invg𝑊)‘𝑌) ∈ 𝐵)
23216adantr 482 . . . 4 ((𝜑𝑌 < 0 ) → 0 < 𝑋)
233133breq1d 5157 . . . . . 6 (𝜑 → (((invg𝑊)‘((invg𝑊)‘𝑌)) < 0𝑌 < 0 ))
234233biimpar 479 . . . . 5 ((𝜑𝑌 < 0 ) → ((invg𝑊)‘((invg𝑊)‘𝑌)) < 0 )
2357, 17, 9, 18ogrpinv0lt 32218 . . . . . . 7 ((𝑊 ∈ oGrp ∧ ((invg𝑊)‘𝑌) ∈ 𝐵) → ( 0 < ((invg𝑊)‘𝑌) ↔ ((invg𝑊)‘((invg𝑊)‘𝑌)) < 0 ))
2362, 122, 235syl2anc 585 . . . . . 6 (𝜑 → ( 0 < ((invg𝑊)‘𝑌) ↔ ((invg𝑊)‘((invg𝑊)‘𝑌)) < 0 ))
237236biimpar 479 . . . . 5 ((𝜑 ∧ ((invg𝑊)‘((invg𝑊)‘𝑌)) < 0 ) → 0 < ((invg𝑊)‘𝑌))
238234, 237syldan 592 . . . 4 ((𝜑𝑌 < 0 ) → 0 < ((invg𝑊)‘𝑌))
2397, 18, 17, 34, 8, 227, 229, 230, 231, 232, 238archirng 32312 . . 3 ((𝜑𝑌 < 0 ) → ∃𝑚 ∈ ℕ0 ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋)))
240226, 239r19.29a 3163 . 2 ((𝜑𝑌 < 0 ) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
241 nn0ssz 12577 . . 3 0 ⊆ ℤ
2422adantr 482 . . . 4 ((𝜑0 < 𝑌) → 𝑊 ∈ oGrp)
243228adantr 482 . . . 4 ((𝜑0 < 𝑌) → 𝑊 ∈ Archi)
2446adantr 482 . . . 4 ((𝜑0 < 𝑌) → 𝑋𝐵)
245120adantr 482 . . . 4 ((𝜑0 < 𝑌) → 𝑌𝐵)
24616adantr 482 . . . 4 ((𝜑0 < 𝑌) → 0 < 𝑋)
247 simpr 486 . . . 4 ((𝜑0 < 𝑌) → 0 < 𝑌)
2487, 18, 17, 34, 8, 242, 243, 244, 245, 246, 247archirng 32312 . . 3 ((𝜑0 < 𝑌) → ∃𝑛 ∈ ℕ0 ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
249 ssrexv 4050 . . 3 (ℕ0 ⊆ ℤ → (∃𝑛 ∈ ℕ0 ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋))))
250241, 248, 249mpsyl 68 . 2 ((𝜑0 < 𝑌) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
2517, 17tlt3 32118 . . 3 ((𝑊 ∈ Toset ∧ 𝑌𝐵0𝐵) → (𝑌 = 0𝑌 < 00 < 𝑌))
25229, 120, 33, 251syl3anc 1372 . 2 (𝜑 → (𝑌 = 0𝑌 < 00 < 𝑌))
25358, 240, 250, 252mpjao3dan 1432 1 (𝜑 → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wo 846  w3o 1087  w3a 1088   = wceq 1542  wcel 2107  wrex 3071  Vcvv 3475  wss 3947   class class class wbr 5147  cfv 6540  (class class class)co 7404  cc 11104  0cc0 11106  1c1 11107   + caddc 11109  cmin 11440  -cneg 11441  2c2 12263  0cn0 12468  cz 12554  Basecbs 17140  +gcplusg 17193  lecple 17200  0gc0g 17381  Posetcpo 18256  ltcplt 18257  Tosetctos 18365  Grpcgrp 18815  invgcminusg 18816  .gcmg 18944  oppgcoppg 19202  oMndcomnd 32193  oGrpcogrp 32194  Archicarchi 32301
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7851  df-1st 7970  df-2nd 7971  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-fz 13481  df-seq 13963  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-plusg 17206  df-ple 17213  df-0g 17383  df-proset 18244  df-poset 18262  df-plt 18279  df-toset 18366  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-grp 18818  df-minusg 18819  df-mulg 18945  df-oppg 19203  df-omnd 32195  df-ogrp 32196  df-inftm 32302  df-archi 32303
This theorem is referenced by:  archiabllem2c  32319
  Copyright terms: Public domain W3C validator