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 30190
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 11660 . . 3 -1 ∈ ℤ
2 archirng.1 . . . . . . . . . 10 (𝜑𝑊 ∈ oGrp)
3 ogrpgrp 30150 . . . . . . . . . 10 (𝑊 ∈ oGrp → 𝑊 ∈ Grp)
42, 3syl 17 . . . . . . . . 9 (𝜑𝑊 ∈ Grp)
5 1zzd 11655 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
6 archirng.3 . . . . . . . . 9 (𝜑𝑋𝐵)
7 archirng.b . . . . . . . . . 10 𝐵 = (Base‘𝑊)
8 archirng.x . . . . . . . . . 10 · = (.g𝑊)
9 eqid 2765 . . . . . . . . . 10 (invg𝑊) = (invg𝑊)
107, 8, 9mulgneg 17826 . . . . . . . . 9 ((𝑊 ∈ Grp ∧ 1 ∈ ℤ ∧ 𝑋𝐵) → (-1 · 𝑋) = ((invg𝑊)‘(1 · 𝑋)))
114, 5, 6, 10syl3anc 1490 . . . . . . . 8 (𝜑 → (-1 · 𝑋) = ((invg𝑊)‘(1 · 𝑋)))
127, 8mulg1 17815 . . . . . . . . . 10 (𝑋𝐵 → (1 · 𝑋) = 𝑋)
136, 12syl 17 . . . . . . . . 9 (𝜑 → (1 · 𝑋) = 𝑋)
1413fveq2d 6379 . . . . . . . 8 (𝜑 → ((invg𝑊)‘(1 · 𝑋)) = ((invg𝑊)‘𝑋))
1511, 14eqtrd 2799 . . . . . . 7 (𝜑 → (-1 · 𝑋) = ((invg𝑊)‘𝑋))
16 archirng.5 . . . . . . . 8 (𝜑0 < 𝑋)
17 archirng.i . . . . . . . . . 10 < = (lt‘𝑊)
18 archirng.0 . . . . . . . . . 10 0 = (0g𝑊)
197, 17, 9, 18ogrpinv0lt 30170 . . . . . . . . 9 ((𝑊 ∈ oGrp ∧ 𝑋𝐵) → ( 0 < 𝑋 ↔ ((invg𝑊)‘𝑋) < 0 ))
2019biimpa 468 . . . . . . . 8 (((𝑊 ∈ oGrp ∧ 𝑋𝐵) ∧ 0 < 𝑋) → ((invg𝑊)‘𝑋) < 0 )
212, 6, 16, 20syl21anc 866 . . . . . . 7 (𝜑 → ((invg𝑊)‘𝑋) < 0 )
2215, 21eqbrtrd 4831 . . . . . 6 (𝜑 → (-1 · 𝑋) < 0 )
2322adantr 472 . . . . 5 ((𝜑𝑌 = 0 ) → (-1 · 𝑋) < 0 )
24 simpr 477 . . . . 5 ((𝜑𝑌 = 0 ) → 𝑌 = 0 )
2523, 24breqtrrd 4837 . . . 4 ((𝜑𝑌 = 0 ) → (-1 · 𝑋) < 𝑌)
26 isogrp 30149 . . . . . . . . . 10 (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd))
2726simprbi 490 . . . . . . . . 9 (𝑊 ∈ oGrp → 𝑊 ∈ oMnd)
28 omndtos 30152 . . . . . . . . 9 (𝑊 ∈ oMnd → 𝑊 ∈ Toset)
292, 27, 283syl 18 . . . . . . . 8 (𝜑𝑊 ∈ Toset)
30 tospos 30105 . . . . . . . 8 (𝑊 ∈ Toset → 𝑊 ∈ Poset)
3129, 30syl 17 . . . . . . 7 (𝜑𝑊 ∈ Poset)
327, 18grpidcl 17717 . . . . . . . 8 (𝑊 ∈ Grp → 0𝐵)
332, 3, 323syl 18 . . . . . . 7 (𝜑0𝐵)
34 archirng.l . . . . . . . 8 = (le‘𝑊)
357, 34posref 17217 . . . . . . 7 ((𝑊 ∈ Poset ∧ 0𝐵) → 0 0 )
3631, 33, 35syl2anc 579 . . . . . 6 (𝜑0 0 )
3736adantr 472 . . . . 5 ((𝜑𝑌 = 0 ) → 0 0 )
38 1m1e0 11344 . . . . . . . . . 10 (1 − 1) = 0
3938negeqi 10528 . . . . . . . . 9 -(1 − 1) = -0
40 ax-1cn 10247 . . . . . . . . . 10 1 ∈ ℂ
4140, 40negsubdii 10620 . . . . . . . . 9 -(1 − 1) = (-1 + 1)
42 neg0 10581 . . . . . . . . 9 -0 = 0
4339, 41, 423eqtr3i 2795 . . . . . . . 8 (-1 + 1) = 0
4443oveq1i 6852 . . . . . . 7 ((-1 + 1) · 𝑋) = (0 · 𝑋)
457, 18, 8mulg0 17813 . . . . . . . 8 (𝑋𝐵 → (0 · 𝑋) = 0 )
466, 45syl 17 . . . . . . 7 (𝜑 → (0 · 𝑋) = 0 )
4744, 46syl5eq 2811 . . . . . 6 (𝜑 → ((-1 + 1) · 𝑋) = 0 )
4847adantr 472 . . . . 5 ((𝜑𝑌 = 0 ) → ((-1 + 1) · 𝑋) = 0 )
4937, 24, 483brtr4d 4841 . . . 4 ((𝜑𝑌 = 0 ) → 𝑌 ((-1 + 1) · 𝑋))
5025, 49jca 507 . . 3 ((𝜑𝑌 = 0 ) → ((-1 · 𝑋) < 𝑌𝑌 ((-1 + 1) · 𝑋)))
51 oveq1 6849 . . . . . 6 (𝑛 = -1 → (𝑛 · 𝑋) = (-1 · 𝑋))
5251breq1d 4819 . . . . 5 (𝑛 = -1 → ((𝑛 · 𝑋) < 𝑌 ↔ (-1 · 𝑋) < 𝑌))
53 oveq1 6849 . . . . . . 7 (𝑛 = -1 → (𝑛 + 1) = (-1 + 1))
5453oveq1d 6857 . . . . . 6 (𝑛 = -1 → ((𝑛 + 1) · 𝑋) = ((-1 + 1) · 𝑋))
5554breq2d 4821 . . . . 5 (𝑛 = -1 → (𝑌 ((𝑛 + 1) · 𝑋) ↔ 𝑌 ((-1 + 1) · 𝑋)))
5652, 55anbi12d 624 . . . 4 (𝑛 = -1 → (((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)) ↔ ((-1 · 𝑋) < 𝑌𝑌 ((-1 + 1) · 𝑋))))
5756rspcev 3461 . . 3 ((-1 ∈ ℤ ∧ ((-1 · 𝑋) < 𝑌𝑌 ((-1 + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
581, 50, 57sylancr 581 . 2 ((𝜑𝑌 = 0 ) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
59 simpr 477 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
6059nn0zd 11727 . . . . . . . 8 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℤ)
6160ad2antrr 717 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → 𝑚 ∈ ℤ)
6261znegcld 11731 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → -𝑚 ∈ ℤ)
63 2z 11656 . . . . . . 7 2 ∈ ℤ
6463a1i 11 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → 2 ∈ ℤ)
6562, 64zsubcld 11734 . . . . 5 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → (-𝑚 − 2) ∈ ℤ)
66 nn0cn 11549 . . . . . . . . . . 11 (𝑚 ∈ ℕ0𝑚 ∈ ℂ)
6766adantl 473 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℂ)
68 2cnd 11350 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 2 ∈ ℂ)
6967, 68negdi2d 10660 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -(𝑚 + 2) = (-𝑚 − 2))
7069oveq1d 6857 . . . . . . . 8 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) · 𝑋) = ((-𝑚 − 2) · 𝑋))
712ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ oGrp)
72 archirngz.1 . . . . . . . . . . . 12 (𝜑 → (oppg𝑊) ∈ oGrp)
7372ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (oppg𝑊) ∈ oGrp)
7471, 73jca 507 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp))
754ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ Grp)
7660peano2zd 11732 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈ ℤ)
776ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑋𝐵)
787, 8mulgcl 17825 . . . . . . . . . . 11 ((𝑊 ∈ Grp ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋𝐵) → ((𝑚 + 1) · 𝑋) ∈ 𝐵)
7975, 76, 77, 78syl3anc 1490 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · 𝑋) ∈ 𝐵)
8063a1i 11 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 2 ∈ ℤ)
8160, 80zaddcld 11733 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 2) ∈ ℤ)
827, 8mulgcl 17825 . . . . . . . . . . 11 ((𝑊 ∈ Grp ∧ (𝑚 + 2) ∈ ℤ ∧ 𝑋𝐵) → ((𝑚 + 2) · 𝑋) ∈ 𝐵)
8375, 81, 77, 82syl3anc 1490 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 2) · 𝑋) ∈ 𝐵)
8475, 32syl 17 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 0𝐵)
8516ad2antrr 717 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 0 < 𝑋)
86 eqid 2765 . . . . . . . . . . . . 13 (+g𝑊) = (+g𝑊)
877, 17, 86ogrpaddlt 30165 . . . . . . . . . . . 12 ((𝑊 ∈ oGrp ∧ ( 0𝐵𝑋𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ 0 < 𝑋) → ( 0 (+g𝑊)((𝑚 + 1) · 𝑋)) < (𝑋(+g𝑊)((𝑚 + 1) · 𝑋)))
8871, 84, 77, 79, 85, 87syl131anc 1502 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ( 0 (+g𝑊)((𝑚 + 1) · 𝑋)) < (𝑋(+g𝑊)((𝑚 + 1) · 𝑋)))
897, 86, 18grplid 17719 . . . . . . . . . . . 12 ((𝑊 ∈ Grp ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → ( 0 (+g𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) · 𝑋))
9075, 79, 89syl2anc 579 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ( 0 (+g𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) · 𝑋))
91 1cnd 10288 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ0 → 1 ∈ ℂ)
9266, 91, 91addassd 10316 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ0 → ((𝑚 + 1) + 1) = (𝑚 + (1 + 1)))
93 1p1e2 11404 . . . . . . . . . . . . . . . . 17 (1 + 1) = 2
9493oveq2i 6853 . . . . . . . . . . . . . . . 16 (𝑚 + (1 + 1)) = (𝑚 + 2)
9592, 94syl6eq 2815 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → ((𝑚 + 1) + 1) = (𝑚 + 2))
9666, 91addcld 10313 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ0 → (𝑚 + 1) ∈ ℂ)
9796, 91addcomd 10492 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → ((𝑚 + 1) + 1) = (1 + (𝑚 + 1)))
9895, 97eqtr3d 2801 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → (𝑚 + 2) = (1 + (𝑚 + 1)))
9998oveq1d 6857 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ0 → ((𝑚 + 2) · 𝑋) = ((1 + (𝑚 + 1)) · 𝑋))
10099adantl 473 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 2) · 𝑋) = ((1 + (𝑚 + 1)) · 𝑋))
101 1zzd 11655 . . . . . . . . . . . . 13 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 1 ∈ ℤ)
1027, 8, 86mulgdir 17838 . . . . . . . . . . . . 13 ((𝑊 ∈ Grp ∧ (1 ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋𝐵)) → ((1 + (𝑚 + 1)) · 𝑋) = ((1 · 𝑋)(+g𝑊)((𝑚 + 1) · 𝑋)))
10375, 101, 76, 77, 102syl13anc 1491 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((1 + (𝑚 + 1)) · 𝑋) = ((1 · 𝑋)(+g𝑊)((𝑚 + 1) · 𝑋)))
10477, 12syl 17 . . . . . . . . . . . . 13 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (1 · 𝑋) = 𝑋)
105104oveq1d 6857 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((1 · 𝑋)(+g𝑊)((𝑚 + 1) · 𝑋)) = (𝑋(+g𝑊)((𝑚 + 1) · 𝑋)))
106100, 103, 1053eqtrrd 2804 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑋(+g𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 2) · 𝑋))
10788, 90, 1063brtr3d 4840 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋))
1087, 17, 9ogrpinvlt 30171 . . . . . . . . . . 11 (((𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp) ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((𝑚 + 2) · 𝑋) ∈ 𝐵) → (((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋) ↔ ((invg𝑊)‘((𝑚 + 2) · 𝑋)) < ((invg𝑊)‘((𝑚 + 1) · 𝑋))))
109108biimpa 468 . . . . . . . . . 10 ((((𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp) ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((𝑚 + 2) · 𝑋) ∈ 𝐵) ∧ ((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋)) → ((invg𝑊)‘((𝑚 + 2) · 𝑋)) < ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
11074, 79, 83, 107, 109syl31anc 1492 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((invg𝑊)‘((𝑚 + 2) · 𝑋)) < ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
1117, 8, 9mulgneg 17826 . . . . . . . . . 10 ((𝑊 ∈ Grp ∧ (𝑚 + 2) ∈ ℤ ∧ 𝑋𝐵) → (-(𝑚 + 2) · 𝑋) = ((invg𝑊)‘((𝑚 + 2) · 𝑋)))
11275, 81, 77, 111syl3anc 1490 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) · 𝑋) = ((invg𝑊)‘((𝑚 + 2) · 𝑋)))
1137, 8, 9mulgneg 17826 . . . . . . . . . 10 ((𝑊 ∈ Grp ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋𝐵) → (-(𝑚 + 1) · 𝑋) = ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
11475, 76, 77, 113syl3anc 1490 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 1) · 𝑋) = ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
115110, 112, 1143brtr4d 4841 . . . . . . . 8 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) · 𝑋) < (-(𝑚 + 1) · 𝑋))
11670, 115eqbrtrrd 4833 . . . . . . 7 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-𝑚 − 2) · 𝑋) < (-(𝑚 + 1) · 𝑋))
117116ad2antrr 717 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((-𝑚 − 2) · 𝑋) < (-(𝑚 + 1) · 𝑋))
118114ad2antrr 717 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → (-(𝑚 + 1) · 𝑋) = ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
11931ad4antr 724 . . . . . . . . 9 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → 𝑊 ∈ Poset)
120 archirng.4 . . . . . . . . . . . 12 (𝜑𝑌𝐵)
1217, 9grpinvcl 17734 . . . . . . . . . . . 12 ((𝑊 ∈ Grp ∧ 𝑌𝐵) → ((invg𝑊)‘𝑌) ∈ 𝐵)
1224, 120, 121syl2anc 579 . . . . . . . . . . 11 (𝜑 → ((invg𝑊)‘𝑌) ∈ 𝐵)
123122ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((invg𝑊)‘𝑌) ∈ 𝐵)
124123ad2antrr 717 . . . . . . . . 9 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((invg𝑊)‘𝑌) ∈ 𝐵)
12579ad2antrr 717 . . . . . . . . 9 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((𝑚 + 1) · 𝑋) ∈ 𝐵)
126 simplrr 796 . . . . . . . . 9 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))
127 simpr 477 . . . . . . . . 9 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌))
1287, 34posasymb 17218 . . . . . . . . . 10 ((𝑊 ∈ Poset ∧ ((invg𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → ((((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) ↔ ((invg𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋)))
129128biimpa 468 . . . . . . . . 9 (((𝑊 ∈ Poset ∧ ((invg𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ (((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌))) → ((invg𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋))
130119, 124, 125, 126, 127, 129syl32anc 1497 . . . . . . . 8 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((invg𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋))
131130fveq2d 6379 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((invg𝑊)‘((invg𝑊)‘𝑌)) = ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
1327, 9grpinvinv 17749 . . . . . . . . 9 ((𝑊 ∈ Grp ∧ 𝑌𝐵) → ((invg𝑊)‘((invg𝑊)‘𝑌)) = 𝑌)
1334, 120, 132syl2anc 579 . . . . . . . 8 (𝜑 → ((invg𝑊)‘((invg𝑊)‘𝑌)) = 𝑌)
134133ad4antr 724 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((invg𝑊)‘((invg𝑊)‘𝑌)) = 𝑌)
135118, 131, 1343eqtr2rd 2806 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → 𝑌 = (-(𝑚 + 1) · 𝑋))
136117, 135breqtrrd 4837 . . . . 5 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ((-𝑚 − 2) · 𝑋) < 𝑌)
137 1cnd 10288 . . . . . . . . . . . . 13 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 1 ∈ ℂ)
13867, 68, 137addsubassd 10666 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 2) − 1) = (𝑚 + (2 − 1)))
139 2m1e1 11405 . . . . . . . . . . . . 13 (2 − 1) = 1
140139oveq2i 6853 . . . . . . . . . . . 12 (𝑚 + (2 − 1)) = (𝑚 + 1)
141138, 140syl6req 2816 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) = ((𝑚 + 2) − 1))
142141negeqd 10529 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -(𝑚 + 1) = -((𝑚 + 2) − 1))
14367, 68addcld 10313 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 2) ∈ ℂ)
144143, 137negsubdid 10661 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -((𝑚 + 2) − 1) = (-(𝑚 + 2) + 1))
14569oveq1d 6857 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) + 1) = ((-𝑚 − 2) + 1))
146142, 144, 1453eqtrrd 2804 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-𝑚 − 2) + 1) = -(𝑚 + 1))
147146oveq1d 6857 . . . . . . . 8 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((-𝑚 − 2) + 1) · 𝑋) = (-(𝑚 + 1) · 𝑋))
14829ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ Toset)
149148, 30syl 17 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ Poset)
15060znegcld 11731 . . . . . . . . . . . 12 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -𝑚 ∈ ℤ)
151150, 80zsubcld 11734 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-𝑚 − 2) ∈ ℤ)
152151peano2zd 11732 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-𝑚 − 2) + 1) ∈ ℤ)
1537, 8mulgcl 17825 . . . . . . . . . 10 ((𝑊 ∈ Grp ∧ ((-𝑚 − 2) + 1) ∈ ℤ ∧ 𝑋𝐵) → (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵)
15475, 152, 77, 153syl3anc 1490 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵)
1557, 34posref 17217 . . . . . . . . 9 ((𝑊 ∈ Poset ∧ (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵) → (((-𝑚 − 2) + 1) · 𝑋) (((-𝑚 − 2) + 1) · 𝑋))
156149, 154, 155syl2anc 579 . . . . . . . 8 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((-𝑚 − 2) + 1) · 𝑋) (((-𝑚 − 2) + 1) · 𝑋))
157147, 156eqbrtrrd 4833 . . . . . . 7 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 1) · 𝑋) (((-𝑚 − 2) + 1) · 𝑋))
158157ad2antrr 717 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → (-(𝑚 + 1) · 𝑋) (((-𝑚 − 2) + 1) · 𝑋))
159135, 158eqbrtrd 4831 . . . . 5 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → 𝑌 (((-𝑚 − 2) + 1) · 𝑋))
160 oveq1 6849 . . . . . . . 8 (𝑛 = (-𝑚 − 2) → (𝑛 · 𝑋) = ((-𝑚 − 2) · 𝑋))
161160breq1d 4819 . . . . . . 7 (𝑛 = (-𝑚 − 2) → ((𝑛 · 𝑋) < 𝑌 ↔ ((-𝑚 − 2) · 𝑋) < 𝑌))
162 oveq1 6849 . . . . . . . . 9 (𝑛 = (-𝑚 − 2) → (𝑛 + 1) = ((-𝑚 − 2) + 1))
163162oveq1d 6857 . . . . . . . 8 (𝑛 = (-𝑚 − 2) → ((𝑛 + 1) · 𝑋) = (((-𝑚 − 2) + 1) · 𝑋))
164163breq2d 4821 . . . . . . 7 (𝑛 = (-𝑚 − 2) → (𝑌 ((𝑛 + 1) · 𝑋) ↔ 𝑌 (((-𝑚 − 2) + 1) · 𝑋)))
165161, 164anbi12d 624 . . . . . 6 (𝑛 = (-𝑚 − 2) → (((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)) ↔ (((-𝑚 − 2) · 𝑋) < 𝑌𝑌 (((-𝑚 − 2) + 1) · 𝑋))))
166165rspcev 3461 . . . . 5 (((-𝑚 − 2) ∈ ℤ ∧ (((-𝑚 − 2) · 𝑋) < 𝑌𝑌 (((-𝑚 − 2) + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
16765, 136, 159, 166syl12anc 865 . . . 4 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
16876ad2antrr 717 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (𝑚 + 1) ∈ ℤ)
169168znegcld 11731 . . . . 5 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → -(𝑚 + 1) ∈ ℤ)
1702ad2antrr 717 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ (𝑚 ∈ ℕ0 ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋)) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) → 𝑊 ∈ oGrp)
17172ad2antrr 717 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ (𝑚 ∈ ℕ0 ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋)) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) → (oppg𝑊) ∈ oGrp)
172170, 171jca 507 . . . . . . . 8 (((𝜑𝑌 < 0 ) ∧ (𝑚 ∈ ℕ0 ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋)) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) → (𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp))
1731723anassrs 1469 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp))
174123ad2antrr 717 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘𝑌) ∈ 𝐵)
17579ad2antrr 717 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((𝑚 + 1) · 𝑋) ∈ 𝐵)
176 simpr 477 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))
1777, 17, 9ogrpinvlt 30171 . . . . . . . 8 (((𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp) ∧ ((invg𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → (((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋) ↔ ((invg𝑊)‘((𝑚 + 1) · 𝑋)) < ((invg𝑊)‘((invg𝑊)‘𝑌))))
178177biimpa 468 . . . . . . 7 ((((𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp) ∧ ((invg𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘((𝑚 + 1) · 𝑋)) < ((invg𝑊)‘((invg𝑊)‘𝑌)))
179173, 174, 175, 176, 178syl31anc 1492 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘((𝑚 + 1) · 𝑋)) < ((invg𝑊)‘((invg𝑊)‘𝑌)))
180114ad2antrr 717 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (-(𝑚 + 1) · 𝑋) = ((invg𝑊)‘((𝑚 + 1) · 𝑋)))
181180eqcomd 2771 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘((𝑚 + 1) · 𝑋)) = (-(𝑚 + 1) · 𝑋))
182133ad4antr 724 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘((invg𝑊)‘𝑌)) = 𝑌)
183179, 181, 1823brtr3d 4840 . . . . 5 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (-(𝑚 + 1) · 𝑋) < 𝑌)
184 simp-4l 801 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝜑)
1857, 8mulgcl 17825 . . . . . . . . . . . 12 ((𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋𝐵) → (𝑚 · 𝑋) ∈ 𝐵)
18675, 60, 77, 185syl3anc 1490 . . . . . . . . . . 11 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 · 𝑋) ∈ 𝐵)
1877, 17, 9ogrpinvlt 30171 . . . . . . . . . . 11 (((𝑊 ∈ oGrp ∧ (oppg𝑊) ∈ oGrp) ∧ (𝑚 · 𝑋) ∈ 𝐵 ∧ ((invg𝑊)‘𝑌) ∈ 𝐵) → ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ↔ ((invg𝑊)‘((invg𝑊)‘𝑌)) < ((invg𝑊)‘(𝑚 · 𝑋))))
18874, 186, 123, 187syl3anc 1490 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ↔ ((invg𝑊)‘((invg𝑊)‘𝑌)) < ((invg𝑊)‘(𝑚 · 𝑋))))
189188biimpa 468 . . . . . . . . 9 ((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ (𝑚 · 𝑋) < ((invg𝑊)‘𝑌)) → ((invg𝑊)‘((invg𝑊)‘𝑌)) < ((invg𝑊)‘(𝑚 · 𝑋)))
190189adantrr 708 . . . . . . . 8 ((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) → ((invg𝑊)‘((invg𝑊)‘𝑌)) < ((invg𝑊)‘(𝑚 · 𝑋)))
191190adantr 472 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘((invg𝑊)‘𝑌)) < ((invg𝑊)‘(𝑚 · 𝑋)))
192 negdi 10592 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → -(𝑚 + 1) = (-𝑚 + -1))
19366, 40, 192sylancl 580 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → -(𝑚 + 1) = (-𝑚 + -1))
194193oveq1d 6857 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ0 → (-(𝑚 + 1) + 1) = ((-𝑚 + -1) + 1))
19566negcld 10633 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → -𝑚 ∈ ℂ)
19691negcld 10633 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → -1 ∈ ℂ)
197195, 196, 91addassd 10316 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → ((-𝑚 + -1) + 1) = (-𝑚 + (-1 + 1)))
19843oveq2i 6853 . . . . . . . . . . . . . . 15 (-𝑚 + (-1 + 1)) = (-𝑚 + 0)
199198a1i 11 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → (-𝑚 + (-1 + 1)) = (-𝑚 + 0))
200195addid1d 10490 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → (-𝑚 + 0) = -𝑚)
201197, 199, 2003eqtrd 2803 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ0 → ((-𝑚 + -1) + 1) = -𝑚)
202194, 201eqtrd 2799 . . . . . . . . . . . 12 (𝑚 ∈ ℕ0 → (-(𝑚 + 1) + 1) = -𝑚)
203202oveq1d 6857 . . . . . . . . . . 11 (𝑚 ∈ ℕ0 → ((-(𝑚 + 1) + 1) · 𝑋) = (-𝑚 · 𝑋))
204203adantl 473 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-(𝑚 + 1) + 1) · 𝑋) = (-𝑚 · 𝑋))
2057, 8, 9mulgneg 17826 . . . . . . . . . . 11 ((𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋𝐵) → (-𝑚 · 𝑋) = ((invg𝑊)‘(𝑚 · 𝑋)))
20675, 60, 77, 205syl3anc 1490 . . . . . . . . . 10 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-𝑚 · 𝑋) = ((invg𝑊)‘(𝑚 · 𝑋)))
207204, 206eqtrd 2799 . . . . . . . . 9 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-(𝑚 + 1) + 1) · 𝑋) = ((invg𝑊)‘(𝑚 · 𝑋)))
208207ad2antrr 717 . . . . . . . 8 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((-(𝑚 + 1) + 1) · 𝑋) = ((invg𝑊)‘(𝑚 · 𝑋)))
209208eqcomd 2771 . . . . . . 7 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg𝑊)‘(𝑚 · 𝑋)) = ((-(𝑚 + 1) + 1) · 𝑋))
210191, 182, 2093brtr3d 4840 . . . . . 6 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝑌 < ((-(𝑚 + 1) + 1) · 𝑋))
211 ovexd 6876 . . . . . . 7 (𝜑 → ((-(𝑚 + 1) + 1) · 𝑋) ∈ V)
21234, 17pltle 17227 . . . . . . 7 ((𝑊 ∈ oGrp ∧ 𝑌𝐵 ∧ ((-(𝑚 + 1) + 1) · 𝑋) ∈ V) → (𝑌 < ((-(𝑚 + 1) + 1) · 𝑋) → 𝑌 ((-(𝑚 + 1) + 1) · 𝑋)))
2132, 120, 211, 212syl3anc 1490 . . . . . 6 (𝜑 → (𝑌 < ((-(𝑚 + 1) + 1) · 𝑋) → 𝑌 ((-(𝑚 + 1) + 1) · 𝑋)))
214184, 210, 213sylc 65 . . . . 5 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝑌 ((-(𝑚 + 1) + 1) · 𝑋))
215 oveq1 6849 . . . . . . . 8 (𝑛 = -(𝑚 + 1) → (𝑛 · 𝑋) = (-(𝑚 + 1) · 𝑋))
216215breq1d 4819 . . . . . . 7 (𝑛 = -(𝑚 + 1) → ((𝑛 · 𝑋) < 𝑌 ↔ (-(𝑚 + 1) · 𝑋) < 𝑌))
217 oveq1 6849 . . . . . . . . 9 (𝑛 = -(𝑚 + 1) → (𝑛 + 1) = (-(𝑚 + 1) + 1))
218217oveq1d 6857 . . . . . . . 8 (𝑛 = -(𝑚 + 1) → ((𝑛 + 1) · 𝑋) = ((-(𝑚 + 1) + 1) · 𝑋))
219218breq2d 4821 . . . . . . 7 (𝑛 = -(𝑚 + 1) → (𝑌 ((𝑛 + 1) · 𝑋) ↔ 𝑌 ((-(𝑚 + 1) + 1) · 𝑋)))
220216, 219anbi12d 624 . . . . . 6 (𝑛 = -(𝑚 + 1) → (((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)) ↔ ((-(𝑚 + 1) · 𝑋) < 𝑌𝑌 ((-(𝑚 + 1) + 1) · 𝑋))))
221220rspcev 3461 . . . . 5 ((-(𝑚 + 1) ∈ ℤ ∧ ((-(𝑚 + 1) · 𝑋) < 𝑌𝑌 ((-(𝑚 + 1) + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
222169, 183, 214, 221syl12anc 865 . . . 4 (((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) ∧ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
2237, 34, 17tlt2 30111 . . . . . 6 ((𝑊 ∈ Toset ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((invg𝑊)‘𝑌) ∈ 𝐵) → (((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌) ∨ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)))
224148, 79, 123, 223syl3anc 1490 . . . . 5 (((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌) ∨ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)))
225224adantr 472 . . . 4 ((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) → (((𝑚 + 1) · 𝑋) ((invg𝑊)‘𝑌) ∨ ((invg𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)))
226167, 222, 225mpjaodan 981 . . 3 ((((𝜑𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
2272adantr 472 . . . 4 ((𝜑𝑌 < 0 ) → 𝑊 ∈ oGrp)
228 archirng.2 . . . . 5 (𝜑𝑊 ∈ Archi)
229228adantr 472 . . . 4 ((𝜑𝑌 < 0 ) → 𝑊 ∈ Archi)
2306adantr 472 . . . 4 ((𝜑𝑌 < 0 ) → 𝑋𝐵)
231122adantr 472 . . . 4 ((𝜑𝑌 < 0 ) → ((invg𝑊)‘𝑌) ∈ 𝐵)
23216adantr 472 . . . 4 ((𝜑𝑌 < 0 ) → 0 < 𝑋)
233133breq1d 4819 . . . . . 6 (𝜑 → (((invg𝑊)‘((invg𝑊)‘𝑌)) < 0𝑌 < 0 ))
234233biimpar 469 . . . . 5 ((𝜑𝑌 < 0 ) → ((invg𝑊)‘((invg𝑊)‘𝑌)) < 0 )
2357, 17, 9, 18ogrpinv0lt 30170 . . . . . . 7 ((𝑊 ∈ oGrp ∧ ((invg𝑊)‘𝑌) ∈ 𝐵) → ( 0 < ((invg𝑊)‘𝑌) ↔ ((invg𝑊)‘((invg𝑊)‘𝑌)) < 0 ))
2362, 122, 235syl2anc 579 . . . . . 6 (𝜑 → ( 0 < ((invg𝑊)‘𝑌) ↔ ((invg𝑊)‘((invg𝑊)‘𝑌)) < 0 ))
237236biimpar 469 . . . . 5 ((𝜑 ∧ ((invg𝑊)‘((invg𝑊)‘𝑌)) < 0 ) → 0 < ((invg𝑊)‘𝑌))
238234, 237syldan 585 . . . 4 ((𝜑𝑌 < 0 ) → 0 < ((invg𝑊)‘𝑌))
2397, 18, 17, 34, 8, 227, 229, 230, 231, 232, 238archirng 30189 . . 3 ((𝜑𝑌 < 0 ) → ∃𝑚 ∈ ℕ0 ((𝑚 · 𝑋) < ((invg𝑊)‘𝑌) ∧ ((invg𝑊)‘𝑌) ((𝑚 + 1) · 𝑋)))
240226, 239r19.29a 3225 . 2 ((𝜑𝑌 < 0 ) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
241 nn0ssz 11645 . . 3 0 ⊆ ℤ
2422adantr 472 . . . 4 ((𝜑0 < 𝑌) → 𝑊 ∈ oGrp)
243228adantr 472 . . . 4 ((𝜑0 < 𝑌) → 𝑊 ∈ Archi)
2446adantr 472 . . . 4 ((𝜑0 < 𝑌) → 𝑋𝐵)
245120adantr 472 . . . 4 ((𝜑0 < 𝑌) → 𝑌𝐵)
24616adantr 472 . . . 4 ((𝜑0 < 𝑌) → 0 < 𝑋)
247 simpr 477 . . . 4 ((𝜑0 < 𝑌) → 0 < 𝑌)
2487, 18, 17, 34, 8, 242, 243, 244, 245, 246, 247archirng 30189 . . 3 ((𝜑0 < 𝑌) → ∃𝑛 ∈ ℕ0 ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
249 ssrexv 3827 . . 3 (ℕ0 ⊆ ℤ → (∃𝑛 ∈ ℕ0 ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋))))
250241, 248, 249mpsyl 68 . 2 ((𝜑0 < 𝑌) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
2517, 17tlt3 30112 . . 3 ((𝑊 ∈ Toset ∧ 𝑌𝐵0𝐵) → (𝑌 = 0𝑌 < 00 < 𝑌))
25229, 120, 33, 251syl3anc 1490 . 2 (𝜑 → (𝑌 = 0𝑌 < 00 < 𝑌))
25358, 240, 250, 252mpjao3dan 1556 1 (𝜑 → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌𝑌 ((𝑛 + 1) · 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wo 873  w3o 1106  w3a 1107   = wceq 1652  wcel 2155  wrex 3056  Vcvv 3350  wss 3732   class class class wbr 4809  cfv 6068  (class class class)co 6842  cc 10187  0cc0 10189  1c1 10190   + caddc 10192  cmin 10520  -cneg 10521  2c2 11327  0cn0 11538  cz 11624  Basecbs 16130  +gcplusg 16214  lecple 16221  0gc0g 16366  Posetcpo 17206  ltcplt 17207  Tosetctos 17299  Grpcgrp 17689  invgcminusg 17690  .gcmg 17807  oppgcoppg 18038  oMndcomnd 30144  oGrpcogrp 30145  Archicarchi 30178
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-tpos 7555  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-fz 12534  df-seq 13009  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-plusg 16227  df-ple 16234  df-0g 16368  df-proset 17194  df-poset 17212  df-plt 17224  df-toset 17300  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-grp 17692  df-minusg 17693  df-mulg 17808  df-oppg 18039  df-omnd 30146  df-ogrp 30147  df-inftm 30179  df-archi 30180
This theorem is referenced by:  archiabllem2c  30196
  Copyright terms: Public domain W3C validator