Metamath Proof Explorer

Theorem archirngz

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

Ref Expression
Hypotheses 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 archirngz ( 𝜑 → ∃ 𝑛 ∈ ℤ ( ( 𝑛 · 𝑋 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) )

Proof

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