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 32376
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 12600 . . 3 -1 ∈ β„€
2 archirng.1 . . . . . . . . . 10 (πœ‘ β†’ π‘Š ∈ oGrp)
3 ogrpgrp 32262 . . . . . . . . . 10 (π‘Š ∈ oGrp β†’ π‘Š ∈ Grp)
42, 3syl 17 . . . . . . . . 9 (πœ‘ β†’ π‘Š ∈ Grp)
5 1zzd 12595 . . . . . . . . 9 (πœ‘ β†’ 1 ∈ β„€)
6 archirng.3 . . . . . . . . 9 (πœ‘ β†’ 𝑋 ∈ 𝐡)
7 archirng.b . . . . . . . . . 10 𝐡 = (Baseβ€˜π‘Š)
8 archirng.x . . . . . . . . . 10 Β· = (.gβ€˜π‘Š)
9 eqid 2732 . . . . . . . . . 10 (invgβ€˜π‘Š) = (invgβ€˜π‘Š)
107, 8, 9mulgneg 18974 . . . . . . . . 9 ((π‘Š ∈ Grp ∧ 1 ∈ β„€ ∧ 𝑋 ∈ 𝐡) β†’ (-1 Β· 𝑋) = ((invgβ€˜π‘Š)β€˜(1 Β· 𝑋)))
114, 5, 6, 10syl3anc 1371 . . . . . . . 8 (πœ‘ β†’ (-1 Β· 𝑋) = ((invgβ€˜π‘Š)β€˜(1 Β· 𝑋)))
127, 8mulg1 18963 . . . . . . . . . 10 (𝑋 ∈ 𝐡 β†’ (1 Β· 𝑋) = 𝑋)
136, 12syl 17 . . . . . . . . 9 (πœ‘ β†’ (1 Β· 𝑋) = 𝑋)
1413fveq2d 6895 . . . . . . . 8 (πœ‘ β†’ ((invgβ€˜π‘Š)β€˜(1 Β· 𝑋)) = ((invgβ€˜π‘Š)β€˜π‘‹))
1511, 14eqtrd 2772 . . . . . . 7 (πœ‘ β†’ (-1 Β· 𝑋) = ((invgβ€˜π‘Š)β€˜π‘‹))
16 archirng.5 . . . . . . . 8 (πœ‘ β†’ 0 < 𝑋)
17 archirng.i . . . . . . . . . 10 < = (ltβ€˜π‘Š)
18 archirng.0 . . . . . . . . . 10 0 = (0gβ€˜π‘Š)
197, 17, 9, 18ogrpinv0lt 32281 . . . . . . . . 9 ((π‘Š ∈ oGrp ∧ 𝑋 ∈ 𝐡) β†’ ( 0 < 𝑋 ↔ ((invgβ€˜π‘Š)β€˜π‘‹) < 0 ))
2019biimpa 477 . . . . . . . 8 (((π‘Š ∈ oGrp ∧ 𝑋 ∈ 𝐡) ∧ 0 < 𝑋) β†’ ((invgβ€˜π‘Š)β€˜π‘‹) < 0 )
212, 6, 16, 20syl21anc 836 . . . . . . 7 (πœ‘ β†’ ((invgβ€˜π‘Š)β€˜π‘‹) < 0 )
2215, 21eqbrtrd 5170 . . . . . 6 (πœ‘ β†’ (-1 Β· 𝑋) < 0 )
2322adantr 481 . . . . 5 ((πœ‘ ∧ π‘Œ = 0 ) β†’ (-1 Β· 𝑋) < 0 )
24 simpr 485 . . . . 5 ((πœ‘ ∧ π‘Œ = 0 ) β†’ π‘Œ = 0 )
2523, 24breqtrrd 5176 . . . 4 ((πœ‘ ∧ π‘Œ = 0 ) β†’ (-1 Β· 𝑋) < π‘Œ)
26 isogrp 32261 . . . . . . . . . 10 (π‘Š ∈ oGrp ↔ (π‘Š ∈ Grp ∧ π‘Š ∈ oMnd))
2726simprbi 497 . . . . . . . . 9 (π‘Š ∈ oGrp β†’ π‘Š ∈ oMnd)
28 omndtos 32264 . . . . . . . . 9 (π‘Š ∈ oMnd β†’ π‘Š ∈ Toset)
292, 27, 283syl 18 . . . . . . . 8 (πœ‘ β†’ π‘Š ∈ Toset)
30 tospos 18375 . . . . . . . 8 (π‘Š ∈ Toset β†’ π‘Š ∈ Poset)
3129, 30syl 17 . . . . . . 7 (πœ‘ β†’ π‘Š ∈ Poset)
327, 18grpidcl 18852 . . . . . . . 8 (π‘Š ∈ Grp β†’ 0 ∈ 𝐡)
332, 3, 323syl 18 . . . . . . 7 (πœ‘ β†’ 0 ∈ 𝐡)
34 archirng.l . . . . . . . 8 ≀ = (leβ€˜π‘Š)
357, 34posref 18273 . . . . . . 7 ((π‘Š ∈ Poset ∧ 0 ∈ 𝐡) β†’ 0 ≀ 0 )
3631, 33, 35syl2anc 584 . . . . . 6 (πœ‘ β†’ 0 ≀ 0 )
3736adantr 481 . . . . 5 ((πœ‘ ∧ π‘Œ = 0 ) β†’ 0 ≀ 0 )
38 1m1e0 12286 . . . . . . . . . 10 (1 βˆ’ 1) = 0
3938negeqi 11455 . . . . . . . . 9 -(1 βˆ’ 1) = -0
40 ax-1cn 11170 . . . . . . . . . 10 1 ∈ β„‚
4140, 40negsubdii 11547 . . . . . . . . 9 -(1 βˆ’ 1) = (-1 + 1)
42 neg0 11508 . . . . . . . . 9 -0 = 0
4339, 41, 423eqtr3i 2768 . . . . . . . 8 (-1 + 1) = 0
4443oveq1i 7421 . . . . . . 7 ((-1 + 1) Β· 𝑋) = (0 Β· 𝑋)
457, 18, 8mulg0 18959 . . . . . . . 8 (𝑋 ∈ 𝐡 β†’ (0 Β· 𝑋) = 0 )
466, 45syl 17 . . . . . . 7 (πœ‘ β†’ (0 Β· 𝑋) = 0 )
4744, 46eqtrid 2784 . . . . . 6 (πœ‘ β†’ ((-1 + 1) Β· 𝑋) = 0 )
4847adantr 481 . . . . 5 ((πœ‘ ∧ π‘Œ = 0 ) β†’ ((-1 + 1) Β· 𝑋) = 0 )
4937, 24, 483brtr4d 5180 . . . 4 ((πœ‘ ∧ π‘Œ = 0 ) β†’ π‘Œ ≀ ((-1 + 1) Β· 𝑋))
5025, 49jca 512 . . 3 ((πœ‘ ∧ π‘Œ = 0 ) β†’ ((-1 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((-1 + 1) Β· 𝑋)))
51 oveq1 7418 . . . . . 6 (𝑛 = -1 β†’ (𝑛 Β· 𝑋) = (-1 Β· 𝑋))
5251breq1d 5158 . . . . 5 (𝑛 = -1 β†’ ((𝑛 Β· 𝑋) < π‘Œ ↔ (-1 Β· 𝑋) < π‘Œ))
53 oveq1 7418 . . . . . . 7 (𝑛 = -1 β†’ (𝑛 + 1) = (-1 + 1))
5453oveq1d 7426 . . . . . 6 (𝑛 = -1 β†’ ((𝑛 + 1) Β· 𝑋) = ((-1 + 1) Β· 𝑋))
5554breq2d 5160 . . . . 5 (𝑛 = -1 β†’ (π‘Œ ≀ ((𝑛 + 1) Β· 𝑋) ↔ π‘Œ ≀ ((-1 + 1) Β· 𝑋)))
5652, 55anbi12d 631 . . . 4 (𝑛 = -1 β†’ (((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)) ↔ ((-1 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((-1 + 1) Β· 𝑋))))
5756rspcev 3612 . . 3 ((-1 ∈ β„€ ∧ ((-1 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((-1 + 1) Β· 𝑋))) β†’ βˆƒπ‘› ∈ β„€ ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)))
581, 50, 57sylancr 587 . 2 ((πœ‘ ∧ π‘Œ = 0 ) β†’ βˆƒπ‘› ∈ β„€ ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)))
59 simpr 485 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ π‘š ∈ β„•0)
6059nn0zd 12586 . . . . . . . 8 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ π‘š ∈ β„€)
6160ad2antrr 724 . . . . . . 7 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ π‘š ∈ β„€)
6261znegcld 12670 . . . . . 6 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ -π‘š ∈ β„€)
63 2z 12596 . . . . . . 7 2 ∈ β„€
6463a1i 11 . . . . . 6 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ 2 ∈ β„€)
6562, 64zsubcld 12673 . . . . 5 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ (-π‘š βˆ’ 2) ∈ β„€)
66 nn0cn 12484 . . . . . . . . . . 11 (π‘š ∈ β„•0 β†’ π‘š ∈ β„‚)
6766adantl 482 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ π‘š ∈ β„‚)
68 2cnd 12292 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ 2 ∈ β„‚)
6967, 68negdi2d 11587 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ -(π‘š + 2) = (-π‘š βˆ’ 2))
7069oveq1d 7426 . . . . . . . 8 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (-(π‘š + 2) Β· 𝑋) = ((-π‘š βˆ’ 2) Β· 𝑋))
712ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ π‘Š ∈ oGrp)
72 archirngz.1 . . . . . . . . . . . 12 (πœ‘ β†’ (oppgβ€˜π‘Š) ∈ oGrp)
7372ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (oppgβ€˜π‘Š) ∈ oGrp)
7471, 73jca 512 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (π‘Š ∈ oGrp ∧ (oppgβ€˜π‘Š) ∈ oGrp))
754ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ π‘Š ∈ Grp)
7660peano2zd 12671 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (π‘š + 1) ∈ β„€)
776ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ 𝑋 ∈ 𝐡)
787, 8mulgcl 18973 . . . . . . . . . . 11 ((π‘Š ∈ Grp ∧ (π‘š + 1) ∈ β„€ ∧ 𝑋 ∈ 𝐡) β†’ ((π‘š + 1) Β· 𝑋) ∈ 𝐡)
7975, 76, 77, 78syl3anc 1371 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((π‘š + 1) Β· 𝑋) ∈ 𝐡)
8063a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ 2 ∈ β„€)
8160, 80zaddcld 12672 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (π‘š + 2) ∈ β„€)
827, 8mulgcl 18973 . . . . . . . . . . 11 ((π‘Š ∈ Grp ∧ (π‘š + 2) ∈ β„€ ∧ 𝑋 ∈ 𝐡) β†’ ((π‘š + 2) Β· 𝑋) ∈ 𝐡)
8375, 81, 77, 82syl3anc 1371 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((π‘š + 2) Β· 𝑋) ∈ 𝐡)
8475, 32syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ 0 ∈ 𝐡)
8516ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ 0 < 𝑋)
86 eqid 2732 . . . . . . . . . . . . 13 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
877, 17, 86ogrpaddlt 32276 . . . . . . . . . . . 12 ((π‘Š ∈ oGrp ∧ ( 0 ∈ 𝐡 ∧ 𝑋 ∈ 𝐡 ∧ ((π‘š + 1) Β· 𝑋) ∈ 𝐡) ∧ 0 < 𝑋) β†’ ( 0 (+gβ€˜π‘Š)((π‘š + 1) Β· 𝑋)) < (𝑋(+gβ€˜π‘Š)((π‘š + 1) Β· 𝑋)))
8871, 84, 77, 79, 85, 87syl131anc 1383 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ( 0 (+gβ€˜π‘Š)((π‘š + 1) Β· 𝑋)) < (𝑋(+gβ€˜π‘Š)((π‘š + 1) Β· 𝑋)))
897, 86, 18grplid 18854 . . . . . . . . . . . 12 ((π‘Š ∈ Grp ∧ ((π‘š + 1) Β· 𝑋) ∈ 𝐡) β†’ ( 0 (+gβ€˜π‘Š)((π‘š + 1) Β· 𝑋)) = ((π‘š + 1) Β· 𝑋))
9075, 79, 89syl2anc 584 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ( 0 (+gβ€˜π‘Š)((π‘š + 1) Β· 𝑋)) = ((π‘š + 1) Β· 𝑋))
91 1cnd 11211 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„•0 β†’ 1 ∈ β„‚)
9266, 91, 91addassd 11238 . . . . . . . . . . . . . . . 16 (π‘š ∈ β„•0 β†’ ((π‘š + 1) + 1) = (π‘š + (1 + 1)))
93 1p1e2 12339 . . . . . . . . . . . . . . . . 17 (1 + 1) = 2
9493oveq2i 7422 . . . . . . . . . . . . . . . 16 (π‘š + (1 + 1)) = (π‘š + 2)
9592, 94eqtrdi 2788 . . . . . . . . . . . . . . 15 (π‘š ∈ β„•0 β†’ ((π‘š + 1) + 1) = (π‘š + 2))
9666, 91addcld 11235 . . . . . . . . . . . . . . . 16 (π‘š ∈ β„•0 β†’ (π‘š + 1) ∈ β„‚)
9796, 91addcomd 11418 . . . . . . . . . . . . . . 15 (π‘š ∈ β„•0 β†’ ((π‘š + 1) + 1) = (1 + (π‘š + 1)))
9895, 97eqtr3d 2774 . . . . . . . . . . . . . 14 (π‘š ∈ β„•0 β†’ (π‘š + 2) = (1 + (π‘š + 1)))
9998oveq1d 7426 . . . . . . . . . . . . 13 (π‘š ∈ β„•0 β†’ ((π‘š + 2) Β· 𝑋) = ((1 + (π‘š + 1)) Β· 𝑋))
10099adantl 482 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((π‘š + 2) Β· 𝑋) = ((1 + (π‘š + 1)) Β· 𝑋))
101 1zzd 12595 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ 1 ∈ β„€)
1027, 8, 86mulgdir 18988 . . . . . . . . . . . . 13 ((π‘Š ∈ Grp ∧ (1 ∈ β„€ ∧ (π‘š + 1) ∈ β„€ ∧ 𝑋 ∈ 𝐡)) β†’ ((1 + (π‘š + 1)) Β· 𝑋) = ((1 Β· 𝑋)(+gβ€˜π‘Š)((π‘š + 1) Β· 𝑋)))
10375, 101, 76, 77, 102syl13anc 1372 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((1 + (π‘š + 1)) Β· 𝑋) = ((1 Β· 𝑋)(+gβ€˜π‘Š)((π‘š + 1) Β· 𝑋)))
10477, 12syl 17 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (1 Β· 𝑋) = 𝑋)
105104oveq1d 7426 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((1 Β· 𝑋)(+gβ€˜π‘Š)((π‘š + 1) Β· 𝑋)) = (𝑋(+gβ€˜π‘Š)((π‘š + 1) Β· 𝑋)))
106100, 103, 1053eqtrrd 2777 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (𝑋(+gβ€˜π‘Š)((π‘š + 1) Β· 𝑋)) = ((π‘š + 2) Β· 𝑋))
10788, 90, 1063brtr3d 5179 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((π‘š + 1) Β· 𝑋) < ((π‘š + 2) Β· 𝑋))
1087, 17, 9ogrpinvlt 32282 . . . . . . . . . . 11 (((π‘Š ∈ oGrp ∧ (oppgβ€˜π‘Š) ∈ oGrp) ∧ ((π‘š + 1) Β· 𝑋) ∈ 𝐡 ∧ ((π‘š + 2) Β· 𝑋) ∈ 𝐡) β†’ (((π‘š + 1) Β· 𝑋) < ((π‘š + 2) Β· 𝑋) ↔ ((invgβ€˜π‘Š)β€˜((π‘š + 2) Β· 𝑋)) < ((invgβ€˜π‘Š)β€˜((π‘š + 1) Β· 𝑋))))
109108biimpa 477 . . . . . . . . . 10 ((((π‘Š ∈ oGrp ∧ (oppgβ€˜π‘Š) ∈ oGrp) ∧ ((π‘š + 1) Β· 𝑋) ∈ 𝐡 ∧ ((π‘š + 2) Β· 𝑋) ∈ 𝐡) ∧ ((π‘š + 1) Β· 𝑋) < ((π‘š + 2) Β· 𝑋)) β†’ ((invgβ€˜π‘Š)β€˜((π‘š + 2) Β· 𝑋)) < ((invgβ€˜π‘Š)β€˜((π‘š + 1) Β· 𝑋)))
11074, 79, 83, 107, 109syl31anc 1373 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((invgβ€˜π‘Š)β€˜((π‘š + 2) Β· 𝑋)) < ((invgβ€˜π‘Š)β€˜((π‘š + 1) Β· 𝑋)))
1117, 8, 9mulgneg 18974 . . . . . . . . . 10 ((π‘Š ∈ Grp ∧ (π‘š + 2) ∈ β„€ ∧ 𝑋 ∈ 𝐡) β†’ (-(π‘š + 2) Β· 𝑋) = ((invgβ€˜π‘Š)β€˜((π‘š + 2) Β· 𝑋)))
11275, 81, 77, 111syl3anc 1371 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (-(π‘š + 2) Β· 𝑋) = ((invgβ€˜π‘Š)β€˜((π‘š + 2) Β· 𝑋)))
1137, 8, 9mulgneg 18974 . . . . . . . . . 10 ((π‘Š ∈ Grp ∧ (π‘š + 1) ∈ β„€ ∧ 𝑋 ∈ 𝐡) β†’ (-(π‘š + 1) Β· 𝑋) = ((invgβ€˜π‘Š)β€˜((π‘š + 1) Β· 𝑋)))
11475, 76, 77, 113syl3anc 1371 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (-(π‘š + 1) Β· 𝑋) = ((invgβ€˜π‘Š)β€˜((π‘š + 1) Β· 𝑋)))
115110, 112, 1143brtr4d 5180 . . . . . . . 8 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (-(π‘š + 2) Β· 𝑋) < (-(π‘š + 1) Β· 𝑋))
11670, 115eqbrtrrd 5172 . . . . . . 7 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((-π‘š βˆ’ 2) Β· 𝑋) < (-(π‘š + 1) Β· 𝑋))
117116ad2antrr 724 . . . . . 6 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ ((-π‘š βˆ’ 2) Β· 𝑋) < (-(π‘š + 1) Β· 𝑋))
118114ad2antrr 724 . . . . . . 7 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ (-(π‘š + 1) Β· 𝑋) = ((invgβ€˜π‘Š)β€˜((π‘š + 1) Β· 𝑋)))
11931ad4antr 730 . . . . . . . . 9 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ π‘Š ∈ Poset)
120 archirng.4 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ 𝐡)
1217, 9grpinvcl 18874 . . . . . . . . . . . 12 ((π‘Š ∈ Grp ∧ π‘Œ ∈ 𝐡) β†’ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡)
1224, 120, 121syl2anc 584 . . . . . . . . . . 11 (πœ‘ β†’ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡)
123122ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡)
124123ad2antrr 724 . . . . . . . . 9 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡)
12579ad2antrr 724 . . . . . . . . 9 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ ((π‘š + 1) Β· 𝑋) ∈ 𝐡)
126 simplrr 776 . . . . . . . . 9 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))
127 simpr 485 . . . . . . . . 9 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ))
1287, 34posasymb 18274 . . . . . . . . . 10 ((π‘Š ∈ Poset ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡 ∧ ((π‘š + 1) Β· 𝑋) ∈ 𝐡) β†’ ((((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) ↔ ((invgβ€˜π‘Š)β€˜π‘Œ) = ((π‘š + 1) Β· 𝑋)))
129128biimpa 477 . . . . . . . . 9 (((π‘Š ∈ Poset ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡 ∧ ((π‘š + 1) Β· 𝑋) ∈ 𝐡) ∧ (((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ))) β†’ ((invgβ€˜π‘Š)β€˜π‘Œ) = ((π‘š + 1) Β· 𝑋))
130119, 124, 125, 126, 127, 129syl32anc 1378 . . . . . . . 8 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ ((invgβ€˜π‘Š)β€˜π‘Œ) = ((π‘š + 1) Β· 𝑋))
131130fveq2d 6895 . . . . . . 7 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) = ((invgβ€˜π‘Š)β€˜((π‘š + 1) Β· 𝑋)))
1327, 9grpinvinv 18892 . . . . . . . . 9 ((π‘Š ∈ Grp ∧ π‘Œ ∈ 𝐡) β†’ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) = π‘Œ)
1334, 120, 132syl2anc 584 . . . . . . . 8 (πœ‘ β†’ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) = π‘Œ)
134133ad4antr 730 . . . . . . 7 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) = π‘Œ)
135118, 131, 1343eqtr2rd 2779 . . . . . 6 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ π‘Œ = (-(π‘š + 1) Β· 𝑋))
136117, 135breqtrrd 5176 . . . . 5 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ ((-π‘š βˆ’ 2) Β· 𝑋) < π‘Œ)
137 1cnd 11211 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ 1 ∈ β„‚)
13867, 68, 137addsubassd 11593 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((π‘š + 2) βˆ’ 1) = (π‘š + (2 βˆ’ 1)))
139 2m1e1 12340 . . . . . . . . . . . . 13 (2 βˆ’ 1) = 1
140139oveq2i 7422 . . . . . . . . . . . 12 (π‘š + (2 βˆ’ 1)) = (π‘š + 1)
141138, 140eqtr2di 2789 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (π‘š + 1) = ((π‘š + 2) βˆ’ 1))
142141negeqd 11456 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ -(π‘š + 1) = -((π‘š + 2) βˆ’ 1))
14367, 68addcld 11235 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (π‘š + 2) ∈ β„‚)
144143, 137negsubdid 11588 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ -((π‘š + 2) βˆ’ 1) = (-(π‘š + 2) + 1))
14569oveq1d 7426 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (-(π‘š + 2) + 1) = ((-π‘š βˆ’ 2) + 1))
146142, 144, 1453eqtrrd 2777 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((-π‘š βˆ’ 2) + 1) = -(π‘š + 1))
147146oveq1d 7426 . . . . . . . 8 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (((-π‘š βˆ’ 2) + 1) Β· 𝑋) = (-(π‘š + 1) Β· 𝑋))
14829ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ π‘Š ∈ Toset)
149148, 30syl 17 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ π‘Š ∈ Poset)
15060znegcld 12670 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ -π‘š ∈ β„€)
151150, 80zsubcld 12673 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (-π‘š βˆ’ 2) ∈ β„€)
152151peano2zd 12671 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((-π‘š βˆ’ 2) + 1) ∈ β„€)
1537, 8mulgcl 18973 . . . . . . . . . 10 ((π‘Š ∈ Grp ∧ ((-π‘š βˆ’ 2) + 1) ∈ β„€ ∧ 𝑋 ∈ 𝐡) β†’ (((-π‘š βˆ’ 2) + 1) Β· 𝑋) ∈ 𝐡)
15475, 152, 77, 153syl3anc 1371 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (((-π‘š βˆ’ 2) + 1) Β· 𝑋) ∈ 𝐡)
1557, 34posref 18273 . . . . . . . . 9 ((π‘Š ∈ Poset ∧ (((-π‘š βˆ’ 2) + 1) Β· 𝑋) ∈ 𝐡) β†’ (((-π‘š βˆ’ 2) + 1) Β· 𝑋) ≀ (((-π‘š βˆ’ 2) + 1) Β· 𝑋))
156149, 154, 155syl2anc 584 . . . . . . . 8 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (((-π‘š βˆ’ 2) + 1) Β· 𝑋) ≀ (((-π‘š βˆ’ 2) + 1) Β· 𝑋))
157147, 156eqbrtrrd 5172 . . . . . . 7 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (-(π‘š + 1) Β· 𝑋) ≀ (((-π‘š βˆ’ 2) + 1) Β· 𝑋))
158157ad2antrr 724 . . . . . 6 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ (-(π‘š + 1) Β· 𝑋) ≀ (((-π‘š βˆ’ 2) + 1) Β· 𝑋))
159135, 158eqbrtrd 5170 . . . . 5 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ π‘Œ ≀ (((-π‘š βˆ’ 2) + 1) Β· 𝑋))
160 oveq1 7418 . . . . . . . 8 (𝑛 = (-π‘š βˆ’ 2) β†’ (𝑛 Β· 𝑋) = ((-π‘š βˆ’ 2) Β· 𝑋))
161160breq1d 5158 . . . . . . 7 (𝑛 = (-π‘š βˆ’ 2) β†’ ((𝑛 Β· 𝑋) < π‘Œ ↔ ((-π‘š βˆ’ 2) Β· 𝑋) < π‘Œ))
162 oveq1 7418 . . . . . . . . 9 (𝑛 = (-π‘š βˆ’ 2) β†’ (𝑛 + 1) = ((-π‘š βˆ’ 2) + 1))
163162oveq1d 7426 . . . . . . . 8 (𝑛 = (-π‘š βˆ’ 2) β†’ ((𝑛 + 1) Β· 𝑋) = (((-π‘š βˆ’ 2) + 1) Β· 𝑋))
164163breq2d 5160 . . . . . . 7 (𝑛 = (-π‘š βˆ’ 2) β†’ (π‘Œ ≀ ((𝑛 + 1) Β· 𝑋) ↔ π‘Œ ≀ (((-π‘š βˆ’ 2) + 1) Β· 𝑋)))
165161, 164anbi12d 631 . . . . . 6 (𝑛 = (-π‘š βˆ’ 2) β†’ (((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)) ↔ (((-π‘š βˆ’ 2) Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ (((-π‘š βˆ’ 2) + 1) Β· 𝑋))))
166165rspcev 3612 . . . . 5 (((-π‘š βˆ’ 2) ∈ β„€ ∧ (((-π‘š βˆ’ 2) Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ (((-π‘š βˆ’ 2) + 1) Β· 𝑋))) β†’ βˆƒπ‘› ∈ β„€ ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)))
16765, 136, 159, 166syl12anc 835 . . . 4 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ βˆƒπ‘› ∈ β„€ ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)))
16876ad2antrr 724 . . . . . 6 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ (π‘š + 1) ∈ β„€)
169168znegcld 12670 . . . . 5 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ -(π‘š + 1) ∈ β„€)
1702ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ < 0 ) ∧ (π‘š ∈ β„•0 ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋)) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋))) β†’ π‘Š ∈ oGrp)
17172ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ < 0 ) ∧ (π‘š ∈ β„•0 ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋)) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋))) β†’ (oppgβ€˜π‘Š) ∈ oGrp)
172170, 171jca 512 . . . . . . . 8 (((πœ‘ ∧ π‘Œ < 0 ) ∧ (π‘š ∈ β„•0 ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋)) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋))) β†’ (π‘Š ∈ oGrp ∧ (oppgβ€˜π‘Š) ∈ oGrp))
1731723anassrs 1360 . . . . . . 7 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ (π‘Š ∈ oGrp ∧ (oppgβ€˜π‘Š) ∈ oGrp))
174123ad2antrr 724 . . . . . . 7 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡)
17579ad2antrr 724 . . . . . . 7 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ ((π‘š + 1) Β· 𝑋) ∈ 𝐡)
176 simpr 485 . . . . . . 7 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋))
1777, 17, 9ogrpinvlt 32282 . . . . . . . 8 (((π‘Š ∈ oGrp ∧ (oppgβ€˜π‘Š) ∈ oGrp) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡 ∧ ((π‘š + 1) Β· 𝑋) ∈ 𝐡) β†’ (((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋) ↔ ((invgβ€˜π‘Š)β€˜((π‘š + 1) Β· 𝑋)) < ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ))))
178177biimpa 477 . . . . . . 7 ((((π‘Š ∈ oGrp ∧ (oppgβ€˜π‘Š) ∈ oGrp) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡 ∧ ((π‘š + 1) Β· 𝑋) ∈ 𝐡) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ ((invgβ€˜π‘Š)β€˜((π‘š + 1) Β· 𝑋)) < ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)))
179173, 174, 175, 176, 178syl31anc 1373 . . . . . 6 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ ((invgβ€˜π‘Š)β€˜((π‘š + 1) Β· 𝑋)) < ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)))
180114ad2antrr 724 . . . . . . 7 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ (-(π‘š + 1) Β· 𝑋) = ((invgβ€˜π‘Š)β€˜((π‘š + 1) Β· 𝑋)))
181180eqcomd 2738 . . . . . 6 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ ((invgβ€˜π‘Š)β€˜((π‘š + 1) Β· 𝑋)) = (-(π‘š + 1) Β· 𝑋))
182133ad4antr 730 . . . . . 6 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) = π‘Œ)
183179, 181, 1823brtr3d 5179 . . . . 5 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ (-(π‘š + 1) Β· 𝑋) < π‘Œ)
184 simp-4l 781 . . . . . 6 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ πœ‘)
1857, 8mulgcl 18973 . . . . . . . . . . . 12 ((π‘Š ∈ Grp ∧ π‘š ∈ β„€ ∧ 𝑋 ∈ 𝐡) β†’ (π‘š Β· 𝑋) ∈ 𝐡)
18675, 60, 77, 185syl3anc 1371 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (π‘š Β· 𝑋) ∈ 𝐡)
1877, 17, 9ogrpinvlt 32282 . . . . . . . . . . 11 (((π‘Š ∈ oGrp ∧ (oppgβ€˜π‘Š) ∈ oGrp) ∧ (π‘š Β· 𝑋) ∈ 𝐡 ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡) β†’ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ↔ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) < ((invgβ€˜π‘Š)β€˜(π‘š Β· 𝑋))))
18874, 186, 123, 187syl3anc 1371 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ↔ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) < ((invgβ€˜π‘Š)β€˜(π‘š Β· 𝑋))))
189188biimpa 477 . . . . . . . . 9 ((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ (π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ)) β†’ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) < ((invgβ€˜π‘Š)β€˜(π‘š Β· 𝑋)))
190189adantrr 715 . . . . . . . 8 ((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) β†’ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) < ((invgβ€˜π‘Š)β€˜(π‘š Β· 𝑋)))
191190adantr 481 . . . . . . 7 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) < ((invgβ€˜π‘Š)β€˜(π‘š Β· 𝑋)))
192 negdi 11519 . . . . . . . . . . . . . . 15 ((π‘š ∈ β„‚ ∧ 1 ∈ β„‚) β†’ -(π‘š + 1) = (-π‘š + -1))
19366, 40, 192sylancl 586 . . . . . . . . . . . . . 14 (π‘š ∈ β„•0 β†’ -(π‘š + 1) = (-π‘š + -1))
194193oveq1d 7426 . . . . . . . . . . . . 13 (π‘š ∈ β„•0 β†’ (-(π‘š + 1) + 1) = ((-π‘š + -1) + 1))
19566negcld 11560 . . . . . . . . . . . . . . 15 (π‘š ∈ β„•0 β†’ -π‘š ∈ β„‚)
19691negcld 11560 . . . . . . . . . . . . . . 15 (π‘š ∈ β„•0 β†’ -1 ∈ β„‚)
197195, 196, 91addassd 11238 . . . . . . . . . . . . . 14 (π‘š ∈ β„•0 β†’ ((-π‘š + -1) + 1) = (-π‘š + (-1 + 1)))
19843oveq2i 7422 . . . . . . . . . . . . . . 15 (-π‘š + (-1 + 1)) = (-π‘š + 0)
199198a1i 11 . . . . . . . . . . . . . 14 (π‘š ∈ β„•0 β†’ (-π‘š + (-1 + 1)) = (-π‘š + 0))
200195addridd 11416 . . . . . . . . . . . . . 14 (π‘š ∈ β„•0 β†’ (-π‘š + 0) = -π‘š)
201197, 199, 2003eqtrd 2776 . . . . . . . . . . . . 13 (π‘š ∈ β„•0 β†’ ((-π‘š + -1) + 1) = -π‘š)
202194, 201eqtrd 2772 . . . . . . . . . . . 12 (π‘š ∈ β„•0 β†’ (-(π‘š + 1) + 1) = -π‘š)
203202oveq1d 7426 . . . . . . . . . . 11 (π‘š ∈ β„•0 β†’ ((-(π‘š + 1) + 1) Β· 𝑋) = (-π‘š Β· 𝑋))
204203adantl 482 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((-(π‘š + 1) + 1) Β· 𝑋) = (-π‘š Β· 𝑋))
2057, 8, 9mulgneg 18974 . . . . . . . . . . 11 ((π‘Š ∈ Grp ∧ π‘š ∈ β„€ ∧ 𝑋 ∈ 𝐡) β†’ (-π‘š Β· 𝑋) = ((invgβ€˜π‘Š)β€˜(π‘š Β· 𝑋)))
20675, 60, 77, 205syl3anc 1371 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (-π‘š Β· 𝑋) = ((invgβ€˜π‘Š)β€˜(π‘š Β· 𝑋)))
207204, 206eqtrd 2772 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ ((-(π‘š + 1) + 1) Β· 𝑋) = ((invgβ€˜π‘Š)β€˜(π‘š Β· 𝑋)))
208207ad2antrr 724 . . . . . . . 8 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ ((-(π‘š + 1) + 1) Β· 𝑋) = ((invgβ€˜π‘Š)β€˜(π‘š Β· 𝑋)))
209208eqcomd 2738 . . . . . . 7 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ ((invgβ€˜π‘Š)β€˜(π‘š Β· 𝑋)) = ((-(π‘š + 1) + 1) Β· 𝑋))
210191, 182, 2093brtr3d 5179 . . . . . 6 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ π‘Œ < ((-(π‘š + 1) + 1) Β· 𝑋))
211 ovexd 7446 . . . . . . 7 (πœ‘ β†’ ((-(π‘š + 1) + 1) Β· 𝑋) ∈ V)
21234, 17pltle 18288 . . . . . . 7 ((π‘Š ∈ oGrp ∧ π‘Œ ∈ 𝐡 ∧ ((-(π‘š + 1) + 1) Β· 𝑋) ∈ V) β†’ (π‘Œ < ((-(π‘š + 1) + 1) Β· 𝑋) β†’ π‘Œ ≀ ((-(π‘š + 1) + 1) Β· 𝑋)))
2132, 120, 211, 212syl3anc 1371 . . . . . 6 (πœ‘ β†’ (π‘Œ < ((-(π‘š + 1) + 1) Β· 𝑋) β†’ π‘Œ ≀ ((-(π‘š + 1) + 1) Β· 𝑋)))
214184, 210, 213sylc 65 . . . . 5 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ π‘Œ ≀ ((-(π‘š + 1) + 1) Β· 𝑋))
215 oveq1 7418 . . . . . . . 8 (𝑛 = -(π‘š + 1) β†’ (𝑛 Β· 𝑋) = (-(π‘š + 1) Β· 𝑋))
216215breq1d 5158 . . . . . . 7 (𝑛 = -(π‘š + 1) β†’ ((𝑛 Β· 𝑋) < π‘Œ ↔ (-(π‘š + 1) Β· 𝑋) < π‘Œ))
217 oveq1 7418 . . . . . . . . 9 (𝑛 = -(π‘š + 1) β†’ (𝑛 + 1) = (-(π‘š + 1) + 1))
218217oveq1d 7426 . . . . . . . 8 (𝑛 = -(π‘š + 1) β†’ ((𝑛 + 1) Β· 𝑋) = ((-(π‘š + 1) + 1) Β· 𝑋))
219218breq2d 5160 . . . . . . 7 (𝑛 = -(π‘š + 1) β†’ (π‘Œ ≀ ((𝑛 + 1) Β· 𝑋) ↔ π‘Œ ≀ ((-(π‘š + 1) + 1) Β· 𝑋)))
220216, 219anbi12d 631 . . . . . 6 (𝑛 = -(π‘š + 1) β†’ (((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)) ↔ ((-(π‘š + 1) Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((-(π‘š + 1) + 1) Β· 𝑋))))
221220rspcev 3612 . . . . 5 ((-(π‘š + 1) ∈ β„€ ∧ ((-(π‘š + 1) Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((-(π‘š + 1) + 1) Β· 𝑋))) β†’ βˆƒπ‘› ∈ β„€ ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)))
222169, 183, 214, 221syl12anc 835 . . . 4 (((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)) β†’ βˆƒπ‘› ∈ β„€ ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)))
2237, 34, 17tlt2 32177 . . . . . 6 ((π‘Š ∈ Toset ∧ ((π‘š + 1) Β· 𝑋) ∈ 𝐡 ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡) β†’ (((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ) ∨ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)))
224148, 79, 123, 223syl3anc 1371 . . . . 5 (((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) β†’ (((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ) ∨ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)))
225224adantr 481 . . . 4 ((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) β†’ (((π‘š + 1) Β· 𝑋) ≀ ((invgβ€˜π‘Š)β€˜π‘Œ) ∨ ((invgβ€˜π‘Š)β€˜π‘Œ) < ((π‘š + 1) Β· 𝑋)))
226167, 222, 225mpjaodan 957 . . 3 ((((πœ‘ ∧ π‘Œ < 0 ) ∧ π‘š ∈ β„•0) ∧ ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋))) β†’ βˆƒπ‘› ∈ β„€ ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)))
2272adantr 481 . . . 4 ((πœ‘ ∧ π‘Œ < 0 ) β†’ π‘Š ∈ oGrp)
228 archirng.2 . . . . 5 (πœ‘ β†’ π‘Š ∈ Archi)
229228adantr 481 . . . 4 ((πœ‘ ∧ π‘Œ < 0 ) β†’ π‘Š ∈ Archi)
2306adantr 481 . . . 4 ((πœ‘ ∧ π‘Œ < 0 ) β†’ 𝑋 ∈ 𝐡)
231122adantr 481 . . . 4 ((πœ‘ ∧ π‘Œ < 0 ) β†’ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡)
23216adantr 481 . . . 4 ((πœ‘ ∧ π‘Œ < 0 ) β†’ 0 < 𝑋)
233133breq1d 5158 . . . . . 6 (πœ‘ β†’ (((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) < 0 ↔ π‘Œ < 0 ))
234233biimpar 478 . . . . 5 ((πœ‘ ∧ π‘Œ < 0 ) β†’ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) < 0 )
2357, 17, 9, 18ogrpinv0lt 32281 . . . . . . 7 ((π‘Š ∈ oGrp ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ∈ 𝐡) β†’ ( 0 < ((invgβ€˜π‘Š)β€˜π‘Œ) ↔ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) < 0 ))
2362, 122, 235syl2anc 584 . . . . . 6 (πœ‘ β†’ ( 0 < ((invgβ€˜π‘Š)β€˜π‘Œ) ↔ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) < 0 ))
237236biimpar 478 . . . . 5 ((πœ‘ ∧ ((invgβ€˜π‘Š)β€˜((invgβ€˜π‘Š)β€˜π‘Œ)) < 0 ) β†’ 0 < ((invgβ€˜π‘Š)β€˜π‘Œ))
238234, 237syldan 591 . . . 4 ((πœ‘ ∧ π‘Œ < 0 ) β†’ 0 < ((invgβ€˜π‘Š)β€˜π‘Œ))
2397, 18, 17, 34, 8, 227, 229, 230, 231, 232, 238archirng 32375 . . 3 ((πœ‘ ∧ π‘Œ < 0 ) β†’ βˆƒπ‘š ∈ β„•0 ((π‘š Β· 𝑋) < ((invgβ€˜π‘Š)β€˜π‘Œ) ∧ ((invgβ€˜π‘Š)β€˜π‘Œ) ≀ ((π‘š + 1) Β· 𝑋)))
240226, 239r19.29a 3162 . 2 ((πœ‘ ∧ π‘Œ < 0 ) β†’ βˆƒπ‘› ∈ β„€ ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)))
241 nn0ssz 12583 . . 3 β„•0 βŠ† β„€
2422adantr 481 . . . 4 ((πœ‘ ∧ 0 < π‘Œ) β†’ π‘Š ∈ oGrp)
243228adantr 481 . . . 4 ((πœ‘ ∧ 0 < π‘Œ) β†’ π‘Š ∈ Archi)
2446adantr 481 . . . 4 ((πœ‘ ∧ 0 < π‘Œ) β†’ 𝑋 ∈ 𝐡)
245120adantr 481 . . . 4 ((πœ‘ ∧ 0 < π‘Œ) β†’ π‘Œ ∈ 𝐡)
24616adantr 481 . . . 4 ((πœ‘ ∧ 0 < π‘Œ) β†’ 0 < 𝑋)
247 simpr 485 . . . 4 ((πœ‘ ∧ 0 < π‘Œ) β†’ 0 < π‘Œ)
2487, 18, 17, 34, 8, 242, 243, 244, 245, 246, 247archirng 32375 . . 3 ((πœ‘ ∧ 0 < π‘Œ) β†’ βˆƒπ‘› ∈ β„•0 ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)))
249 ssrexv 4051 . . 3 (β„•0 βŠ† β„€ β†’ (βˆƒπ‘› ∈ β„•0 ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)) β†’ βˆƒπ‘› ∈ β„€ ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋))))
250241, 248, 249mpsyl 68 . 2 ((πœ‘ ∧ 0 < π‘Œ) β†’ βˆƒπ‘› ∈ β„€ ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)))
2517, 17tlt3 32178 . . 3 ((π‘Š ∈ Toset ∧ π‘Œ ∈ 𝐡 ∧ 0 ∈ 𝐡) β†’ (π‘Œ = 0 ∨ π‘Œ < 0 ∨ 0 < π‘Œ))
25229, 120, 33, 251syl3anc 1371 . 2 (πœ‘ β†’ (π‘Œ = 0 ∨ π‘Œ < 0 ∨ 0 < π‘Œ))
25358, 240, 250, 252mpjao3dan 1431 1 (πœ‘ β†’ βˆƒπ‘› ∈ β„€ ((𝑛 Β· 𝑋) < π‘Œ ∧ π‘Œ ≀ ((𝑛 + 1) Β· 𝑋)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∨ w3o 1086   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆƒwrex 3070  Vcvv 3474   βŠ† wss 3948   class class class wbr 5148  β€˜cfv 6543  (class class class)co 7411  β„‚cc 11110  0cc0 11112  1c1 11113   + caddc 11115   βˆ’ cmin 11446  -cneg 11447  2c2 12269  β„•0cn0 12474  β„€cz 12560  Basecbs 17146  +gcplusg 17199  lecple 17206  0gc0g 17387  Posetcpo 18262  ltcplt 18263  Tosetctos 18371  Grpcgrp 18821  invgcminusg 18822  .gcmg 18952  oppgcoppg 19211  oMndcomnd 32256  oGrpcogrp 32257  Archicarchi 32364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-tpos 8213  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12475  df-z 12561  df-dec 12680  df-uz 12825  df-fz 13487  df-seq 13969  df-sets 17099  df-slot 17117  df-ndx 17129  df-base 17147  df-plusg 17212  df-ple 17219  df-0g 17389  df-proset 18250  df-poset 18268  df-plt 18285  df-toset 18372  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-grp 18824  df-minusg 18825  df-mulg 18953  df-oppg 19212  df-omnd 32258  df-ogrp 32259  df-inftm 32365  df-archi 32366
This theorem is referenced by:  archiabllem2c  32382
  Copyright terms: Public domain W3C validator