| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | neg1z 12655 | . . 3
⊢ -1 ∈
ℤ | 
| 2 |  | archirng.1 | . . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ oGrp) | 
| 3 |  | ogrpgrp 33081 | . . . . . . . . . 10
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Grp) | 
| 4 | 2, 3 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ Grp) | 
| 5 |  | 1zzd 12650 | . . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) | 
| 6 |  | archirng.3 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 7 |  | archirng.b | . . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑊) | 
| 8 |  | archirng.x | . . . . . . . . . 10
⊢  · =
(.g‘𝑊) | 
| 9 |  | eqid 2736 | . . . . . . . . . 10
⊢
(invg‘𝑊) = (invg‘𝑊) | 
| 10 | 7, 8, 9 | mulgneg 19111 | . . . . . . . . 9
⊢ ((𝑊 ∈ Grp ∧ 1 ∈
ℤ ∧ 𝑋 ∈
𝐵) → (-1 · 𝑋) =
((invg‘𝑊)‘(1 · 𝑋))) | 
| 11 | 4, 5, 6, 10 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → (-1 · 𝑋) = ((invg‘𝑊)‘(1 · 𝑋))) | 
| 12 | 7, 8 | mulg1 19100 | . . . . . . . . . 10
⊢ (𝑋 ∈ 𝐵 → (1 · 𝑋) = 𝑋) | 
| 13 | 6, 12 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (1 · 𝑋) = 𝑋) | 
| 14 | 13 | fveq2d 6909 | . . . . . . . 8
⊢ (𝜑 →
((invg‘𝑊)‘(1 · 𝑋)) = ((invg‘𝑊)‘𝑋)) | 
| 15 | 11, 14 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → (-1 · 𝑋) = ((invg‘𝑊)‘𝑋)) | 
| 16 |  | archirng.5 | . . . . . . . 8
⊢ (𝜑 → 0 < 𝑋) | 
| 17 |  | archirng.i | . . . . . . . . . 10
⊢  < =
(lt‘𝑊) | 
| 18 |  | archirng.0 | . . . . . . . . . 10
⊢  0 =
(0g‘𝑊) | 
| 19 | 7, 17, 9, 18 | ogrpinv0lt 33100 | . . . . . . . . 9
⊢ ((𝑊 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ ((invg‘𝑊)‘𝑋) < 0 )) | 
| 20 | 19 | biimpa 476 | . . . . . . . 8
⊢ (((𝑊 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → ((invg‘𝑊)‘𝑋) < 0 ) | 
| 21 | 2, 6, 16, 20 | syl21anc 837 | . . . . . . 7
⊢ (𝜑 →
((invg‘𝑊)‘𝑋) < 0 ) | 
| 22 | 15, 21 | eqbrtrd 5164 | . . . . . 6
⊢ (𝜑 → (-1 · 𝑋) < 0 ) | 
| 23 | 22 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑌 = 0 ) → (-1 · 𝑋) < 0 ) | 
| 24 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑌 = 0 ) → 𝑌 = 0 ) | 
| 25 | 23, 24 | breqtrrd 5170 | . . . 4
⊢ ((𝜑 ∧ 𝑌 = 0 ) → (-1 · 𝑋) < 𝑌) | 
| 26 |  | isogrp 33080 | . . . . . . . . . 10
⊢ (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd)) | 
| 27 | 26 | simprbi 496 | . . . . . . . . 9
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ oMnd) | 
| 28 |  | omndtos 33083 | . . . . . . . . 9
⊢ (𝑊 ∈ oMnd → 𝑊 ∈ Toset) | 
| 29 | 2, 27, 28 | 3syl 18 | . . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Toset) | 
| 30 |  | tospos 18466 | . . . . . . . 8
⊢ (𝑊 ∈ Toset → 𝑊 ∈ Poset) | 
| 31 | 29, 30 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Poset) | 
| 32 | 7, 18 | grpidcl 18984 | . . . . . . . 8
⊢ (𝑊 ∈ Grp → 0 ∈ 𝐵) | 
| 33 | 2, 3, 32 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → 0 ∈ 𝐵) | 
| 34 |  | archirng.l | . . . . . . . 8
⊢  ≤ =
(le‘𝑊) | 
| 35 | 7, 34 | posref 18365 | . . . . . . 7
⊢ ((𝑊 ∈ Poset ∧ 0 ∈ 𝐵) → 0 ≤ 0 ) | 
| 36 | 31, 33, 35 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → 0 ≤ 0 ) | 
| 37 | 36 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑌 = 0 ) → 0 ≤ 0
) | 
| 38 |  | 1m1e0 12339 | . . . . . . . . . 10
⊢ (1
− 1) = 0 | 
| 39 | 38 | negeqi 11502 | . . . . . . . . 9
⊢ -(1
− 1) = -0 | 
| 40 |  | ax-1cn 11214 | . . . . . . . . . 10
⊢ 1 ∈
ℂ | 
| 41 | 40, 40 | negsubdii 11595 | . . . . . . . . 9
⊢ -(1
− 1) = (-1 + 1) | 
| 42 |  | neg0 11556 | . . . . . . . . 9
⊢ -0 =
0 | 
| 43 | 39, 41, 42 | 3eqtr3i 2772 | . . . . . . . 8
⊢ (-1 + 1)
= 0 | 
| 44 | 43 | oveq1i 7442 | . . . . . . 7
⊢ ((-1 + 1)
·
𝑋) = (0 · 𝑋) | 
| 45 | 7, 18, 8 | mulg0 19093 | . . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 ) | 
| 46 | 6, 45 | syl 17 | . . . . . . 7
⊢ (𝜑 → (0 · 𝑋) = 0 ) | 
| 47 | 44, 46 | eqtrid 2788 | . . . . . 6
⊢ (𝜑 → ((-1 + 1) · 𝑋) = 0 ) | 
| 48 | 47 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑌 = 0 ) → ((-1 + 1) · 𝑋) = 0 ) | 
| 49 | 37, 24, 48 | 3brtr4d 5174 | . . . 4
⊢ ((𝜑 ∧ 𝑌 = 0 ) → 𝑌 ≤ ((-1 + 1) · 𝑋)) | 
| 50 | 25, 49 | jca 511 | . . 3
⊢ ((𝜑 ∧ 𝑌 = 0 ) → ((-1 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-1 + 1) · 𝑋))) | 
| 51 |  | oveq1 7439 | . . . . . 6
⊢ (𝑛 = -1 → (𝑛 · 𝑋) = (-1 · 𝑋)) | 
| 52 | 51 | breq1d 5152 | . . . . 5
⊢ (𝑛 = -1 → ((𝑛 · 𝑋) < 𝑌 ↔ (-1 · 𝑋) < 𝑌)) | 
| 53 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑛 = -1 → (𝑛 + 1) = (-1 + 1)) | 
| 54 | 53 | oveq1d 7447 | . . . . . 6
⊢ (𝑛 = -1 → ((𝑛 + 1) · 𝑋) = ((-1 + 1) · 𝑋)) | 
| 55 | 54 | breq2d 5154 | . . . . 5
⊢ (𝑛 = -1 → (𝑌 ≤ ((𝑛 + 1) · 𝑋) ↔ 𝑌 ≤ ((-1 + 1) · 𝑋))) | 
| 56 | 52, 55 | anbi12d 632 | . . . 4
⊢ (𝑛 = -1 → (((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) ↔ ((-1 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-1 + 1) · 𝑋)))) | 
| 57 | 56 | rspcev 3621 | . . 3
⊢ ((-1
∈ ℤ ∧ ((-1 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-1 + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) | 
| 58 | 1, 50, 57 | sylancr 587 | . 2
⊢ ((𝜑 ∧ 𝑌 = 0 ) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) | 
| 59 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) | 
| 60 | 59 | nn0zd 12641 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℤ) | 
| 61 | 60 | ad2antrr 726 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → 𝑚 ∈ ℤ) | 
| 62 | 61 | znegcld 12726 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → -𝑚 ∈ ℤ) | 
| 63 |  | 2z 12651 | . . . . . . 7
⊢ 2 ∈
ℤ | 
| 64 | 63 | a1i 11 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → 2 ∈ ℤ) | 
| 65 | 62, 64 | zsubcld 12729 | . . . . 5
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → (-𝑚 − 2) ∈ ℤ) | 
| 66 |  | nn0cn 12538 | . . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) | 
| 67 | 66 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℂ) | 
| 68 |  | 2cnd 12345 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 2 ∈
ℂ) | 
| 69 | 67, 68 | negdi2d 11635 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -(𝑚 + 2) = (-𝑚 − 2)) | 
| 70 | 69 | oveq1d 7447 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) · 𝑋) = ((-𝑚 − 2) · 𝑋)) | 
| 71 | 2 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ oGrp) | 
| 72 |  | archirngz.1 | . . . . . . . . . . . 12
⊢ (𝜑 →
(oppg‘𝑊) ∈ oGrp) | 
| 73 | 72 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) →
(oppg‘𝑊) ∈ oGrp) | 
| 74 | 71, 73 | jca 511 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp)) | 
| 75 | 4 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ Grp) | 
| 76 | 60 | peano2zd 12727 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈
ℤ) | 
| 77 | 6 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑋 ∈ 𝐵) | 
| 78 | 7, 8 | mulgcl 19110 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑚 + 1) · 𝑋) ∈ 𝐵) | 
| 79 | 75, 76, 77, 78 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · 𝑋) ∈ 𝐵) | 
| 80 | 63 | a1i 11 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 2 ∈
ℤ) | 
| 81 | 60, 80 | zaddcld 12728 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 2) ∈
ℤ) | 
| 82 | 7, 8 | mulgcl 19110 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 2) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑚 + 2) · 𝑋) ∈ 𝐵) | 
| 83 | 75, 81, 77, 82 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 2) · 𝑋) ∈ 𝐵) | 
| 84 | 75, 32 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 0 ∈ 𝐵) | 
| 85 | 16 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 0 < 𝑋) | 
| 86 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(+g‘𝑊) = (+g‘𝑊) | 
| 87 | 7, 17, 86 | ogrpaddlt 33095 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ oGrp ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ 0 < 𝑋) → ( 0 (+g‘𝑊)((𝑚 + 1) · 𝑋)) < (𝑋(+g‘𝑊)((𝑚 + 1) · 𝑋))) | 
| 88 | 71, 84, 77, 79, 85, 87 | syl131anc 1384 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ( 0
(+g‘𝑊)((𝑚 + 1) · 𝑋)) < (𝑋(+g‘𝑊)((𝑚 + 1) · 𝑋))) | 
| 89 | 7, 86, 18 | grplid 18986 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ Grp ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → ( 0 (+g‘𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) · 𝑋)) | 
| 90 | 75, 79, 89 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ( 0
(+g‘𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) · 𝑋)) | 
| 91 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ0
→ 1 ∈ ℂ) | 
| 92 | 66, 91, 91 | addassd 11284 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ0
→ ((𝑚 + 1) + 1) =
(𝑚 + (1 +
1))) | 
| 93 |  | 1p1e2 12392 | . . . . . . . . . . . . . . . . 17
⊢ (1 + 1) =
2 | 
| 94 | 93 | oveq2i 7443 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 + (1 + 1)) = (𝑚 + 2) | 
| 95 | 92, 94 | eqtrdi 2792 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ0
→ ((𝑚 + 1) + 1) =
(𝑚 + 2)) | 
| 96 | 66, 91 | addcld 11281 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℂ) | 
| 97 | 96, 91 | addcomd 11464 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ0
→ ((𝑚 + 1) + 1) = (1 +
(𝑚 + 1))) | 
| 98 | 95, 97 | eqtr3d 2778 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 2) = (1 +
(𝑚 + 1))) | 
| 99 | 98 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ ((𝑚 + 2) · 𝑋) = ((1 + (𝑚 + 1)) · 𝑋)) | 
| 100 | 99 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 2) · 𝑋) = ((1 + (𝑚 + 1)) · 𝑋)) | 
| 101 |  | 1zzd 12650 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 1 ∈
ℤ) | 
| 102 | 7, 8, 86 | mulgdir 19125 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Grp ∧ (1 ∈
ℤ ∧ (𝑚 + 1)
∈ ℤ ∧ 𝑋
∈ 𝐵)) → ((1 +
(𝑚 + 1)) · 𝑋) = ((1 · 𝑋)(+g‘𝑊)((𝑚 + 1) · 𝑋))) | 
| 103 | 75, 101, 76, 77, 102 | syl13anc 1373 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((1 +
(𝑚 + 1)) · 𝑋) = ((1 · 𝑋)(+g‘𝑊)((𝑚 + 1) · 𝑋))) | 
| 104 | 77, 12 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (1 · 𝑋) = 𝑋) | 
| 105 | 104 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((1 · 𝑋)(+g‘𝑊)((𝑚 + 1) · 𝑋)) = (𝑋(+g‘𝑊)((𝑚 + 1) · 𝑋))) | 
| 106 | 100, 103,
105 | 3eqtrrd 2781 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑋(+g‘𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 2) · 𝑋)) | 
| 107 | 88, 90, 106 | 3brtr3d 5173 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋)) | 
| 108 | 7, 17, 9 | ogrpinvlt 33101 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp) ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((𝑚 + 2) · 𝑋) ∈ 𝐵) → (((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋) ↔ ((invg‘𝑊)‘((𝑚 + 2) · 𝑋)) <
((invg‘𝑊)‘((𝑚 + 1) · 𝑋)))) | 
| 109 | 108 | biimpa 476 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp) ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((𝑚 + 2) · 𝑋) ∈ 𝐵) ∧ ((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋)) → ((invg‘𝑊)‘((𝑚 + 2) · 𝑋)) <
((invg‘𝑊)‘((𝑚 + 1) · 𝑋))) | 
| 110 | 74, 79, 83, 107, 109 | syl31anc 1374 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) →
((invg‘𝑊)‘((𝑚 + 2) · 𝑋)) <
((invg‘𝑊)‘((𝑚 + 1) · 𝑋))) | 
| 111 | 7, 8, 9 | mulgneg 19111 | . . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 2) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-(𝑚 + 2) · 𝑋) = ((invg‘𝑊)‘((𝑚 + 2) · 𝑋))) | 
| 112 | 75, 81, 77, 111 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) · 𝑋) = ((invg‘𝑊)‘((𝑚 + 2) · 𝑋))) | 
| 113 | 7, 8, 9 | mulgneg 19111 | . . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-(𝑚 + 1) · 𝑋) = ((invg‘𝑊)‘((𝑚 + 1) · 𝑋))) | 
| 114 | 75, 76, 77, 113 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 1) · 𝑋) = ((invg‘𝑊)‘((𝑚 + 1) · 𝑋))) | 
| 115 | 110, 112,
114 | 3brtr4d 5174 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) · 𝑋) < (-(𝑚 + 1) · 𝑋)) | 
| 116 | 70, 115 | eqbrtrrd 5166 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-𝑚 − 2) · 𝑋) < (-(𝑚 + 1) · 𝑋)) | 
| 117 | 116 | ad2antrr 726 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((-𝑚 − 2) · 𝑋) < (-(𝑚 + 1) · 𝑋)) | 
| 118 | 114 | ad2antrr 726 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → (-(𝑚 + 1) · 𝑋) = ((invg‘𝑊)‘((𝑚 + 1) · 𝑋))) | 
| 119 | 31 | ad4antr 732 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → 𝑊 ∈ Poset) | 
| 120 |  | archirng.4 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ 𝐵) | 
| 121 | 7, 9 | grpinvcl 19006 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝐵) → ((invg‘𝑊)‘𝑌) ∈ 𝐵) | 
| 122 | 4, 120, 121 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 →
((invg‘𝑊)‘𝑌) ∈ 𝐵) | 
| 123 | 122 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) →
((invg‘𝑊)‘𝑌) ∈ 𝐵) | 
| 124 | 123 | ad2antrr 726 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((invg‘𝑊)‘𝑌) ∈ 𝐵) | 
| 125 | 79 | ad2antrr 726 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((𝑚 + 1) · 𝑋) ∈ 𝐵) | 
| 126 |  | simplrr 777 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋)) | 
| 127 |  | simpr 484 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) | 
| 128 | 7, 34 | posasymb 18366 | . . . . . . . . . 10
⊢ ((𝑊 ∈ Poset ∧
((invg‘𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → ((((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) ↔ ((invg‘𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋))) | 
| 129 | 128 | biimpa 476 | . . . . . . . . 9
⊢ (((𝑊 ∈ Poset ∧
((invg‘𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ (((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌))) → ((invg‘𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋)) | 
| 130 | 119, 124,
125, 126, 127, 129 | syl32anc 1379 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((invg‘𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋)) | 
| 131 | 130 | fveq2d 6909 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) = ((invg‘𝑊)‘((𝑚 + 1) · 𝑋))) | 
| 132 | 7, 9 | grpinvinv 19024 | . . . . . . . . 9
⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝐵) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) = 𝑌) | 
| 133 | 4, 120, 132 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 →
((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) = 𝑌) | 
| 134 | 133 | ad4antr 732 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) = 𝑌) | 
| 135 | 118, 131,
134 | 3eqtr2rd 2783 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → 𝑌 = (-(𝑚 + 1) · 𝑋)) | 
| 136 | 117, 135 | breqtrrd 5170 | . . . . 5
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((-𝑚 − 2) · 𝑋) < 𝑌) | 
| 137 |  | 1cnd 11257 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 1 ∈
ℂ) | 
| 138 | 67, 68, 137 | addsubassd 11641 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 2) − 1) = (𝑚 + (2 −
1))) | 
| 139 |  | 2m1e1 12393 | . . . . . . . . . . . . 13
⊢ (2
− 1) = 1 | 
| 140 | 139 | oveq2i 7443 | . . . . . . . . . . . 12
⊢ (𝑚 + (2 − 1)) = (𝑚 + 1) | 
| 141 | 138, 140 | eqtr2di 2793 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) = ((𝑚 + 2) − 1)) | 
| 142 | 141 | negeqd 11503 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -(𝑚 + 1) = -((𝑚 + 2) − 1)) | 
| 143 | 67, 68 | addcld 11281 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 2) ∈
ℂ) | 
| 144 | 143, 137 | negsubdid 11636 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -((𝑚 + 2) − 1) = (-(𝑚 + 2) + 1)) | 
| 145 | 69 | oveq1d 7447 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) + 1) = ((-𝑚 − 2) +
1)) | 
| 146 | 142, 144,
145 | 3eqtrrd 2781 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-𝑚 − 2) + 1) = -(𝑚 + 1)) | 
| 147 | 146 | oveq1d 7447 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((-𝑚 − 2) + 1) · 𝑋) = (-(𝑚 + 1) · 𝑋)) | 
| 148 | 29 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ Toset) | 
| 149 | 148, 30 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ Poset) | 
| 150 | 60 | znegcld 12726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -𝑚 ∈
ℤ) | 
| 151 | 150, 80 | zsubcld 12729 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-𝑚 − 2) ∈
ℤ) | 
| 152 | 151 | peano2zd 12727 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-𝑚 − 2) + 1) ∈
ℤ) | 
| 153 | 7, 8 | mulgcl 19110 | . . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ ((-𝑚 − 2) + 1) ∈ ℤ
∧ 𝑋 ∈ 𝐵) → (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵) | 
| 154 | 75, 152, 77, 153 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵) | 
| 155 | 7, 34 | posref 18365 | . . . . . . . . 9
⊢ ((𝑊 ∈ Poset ∧ (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵) → (((-𝑚 − 2) + 1) · 𝑋) ≤ (((-𝑚 − 2) + 1) · 𝑋)) | 
| 156 | 149, 154,
155 | syl2anc 584 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((-𝑚 − 2) + 1) · 𝑋) ≤ (((-𝑚 − 2) + 1) · 𝑋)) | 
| 157 | 147, 156 | eqbrtrrd 5166 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 1) · 𝑋) ≤ (((-𝑚 − 2) + 1) · 𝑋)) | 
| 158 | 157 | ad2antrr 726 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → (-(𝑚 + 1) · 𝑋) ≤ (((-𝑚 − 2) + 1) · 𝑋)) | 
| 159 | 135, 158 | eqbrtrd 5164 | . . . . 5
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → 𝑌 ≤ (((-𝑚 − 2) + 1) · 𝑋)) | 
| 160 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑛 = (-𝑚 − 2) → (𝑛 · 𝑋) = ((-𝑚 − 2) · 𝑋)) | 
| 161 | 160 | breq1d 5152 | . . . . . . 7
⊢ (𝑛 = (-𝑚 − 2) → ((𝑛 · 𝑋) < 𝑌 ↔ ((-𝑚 − 2) · 𝑋) < 𝑌)) | 
| 162 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑛 = (-𝑚 − 2) → (𝑛 + 1) = ((-𝑚 − 2) + 1)) | 
| 163 | 162 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑛 = (-𝑚 − 2) → ((𝑛 + 1) · 𝑋) = (((-𝑚 − 2) + 1) · 𝑋)) | 
| 164 | 163 | breq2d 5154 | . . . . . . 7
⊢ (𝑛 = (-𝑚 − 2) → (𝑌 ≤ ((𝑛 + 1) · 𝑋) ↔ 𝑌 ≤ (((-𝑚 − 2) + 1) · 𝑋))) | 
| 165 | 161, 164 | anbi12d 632 | . . . . . 6
⊢ (𝑛 = (-𝑚 − 2) → (((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) ↔ (((-𝑚 − 2) · 𝑋) < 𝑌 ∧ 𝑌 ≤ (((-𝑚 − 2) + 1) · 𝑋)))) | 
| 166 | 165 | rspcev 3621 | . . . . 5
⊢ (((-𝑚 − 2) ∈ ℤ ∧
(((-𝑚 − 2) · 𝑋) < 𝑌 ∧ 𝑌 ≤ (((-𝑚 − 2) + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) | 
| 167 | 65, 136, 159, 166 | syl12anc 836 | . . . 4
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) | 
| 168 | 76 | ad2antrr 726 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (𝑚 + 1) ∈ ℤ) | 
| 169 | 168 | znegcld 12726 | . . . . 5
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → -(𝑚 + 1) ∈ ℤ) | 
| 170 | 2 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ (𝑚 ∈ ℕ0
∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋)) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) → 𝑊 ∈ oGrp) | 
| 171 | 72 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ (𝑚 ∈ ℕ0
∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋)) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) →
(oppg‘𝑊) ∈ oGrp) | 
| 172 | 170, 171 | jca 511 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ (𝑚 ∈ ℕ0
∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋)) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) → (𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp)) | 
| 173 | 172 | 3anassrs 1360 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp)) | 
| 174 | 123 | ad2antrr 726 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg‘𝑊)‘𝑌) ∈ 𝐵) | 
| 175 | 79 | ad2antrr 726 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((𝑚 + 1) · 𝑋) ∈ 𝐵) | 
| 176 |  | simpr 484 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) | 
| 177 | 7, 17, 9 | ogrpinvlt 33101 | . . . . . . . 8
⊢ (((𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp) ∧
((invg‘𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → (((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋) ↔ ((invg‘𝑊)‘((𝑚 + 1) · 𝑋)) <
((invg‘𝑊)‘((invg‘𝑊)‘𝑌)))) | 
| 178 | 177 | biimpa 476 | . . . . . . 7
⊢ ((((𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp) ∧
((invg‘𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg‘𝑊)‘((𝑚 + 1) · 𝑋)) <
((invg‘𝑊)‘((invg‘𝑊)‘𝑌))) | 
| 179 | 173, 174,
175, 176, 178 | syl31anc 1374 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg‘𝑊)‘((𝑚 + 1) · 𝑋)) <
((invg‘𝑊)‘((invg‘𝑊)‘𝑌))) | 
| 180 | 114 | ad2antrr 726 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (-(𝑚 + 1) · 𝑋) = ((invg‘𝑊)‘((𝑚 + 1) · 𝑋))) | 
| 181 | 180 | eqcomd 2742 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg‘𝑊)‘((𝑚 + 1) · 𝑋)) = (-(𝑚 + 1) · 𝑋)) | 
| 182 | 133 | ad4antr 732 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) = 𝑌) | 
| 183 | 179, 181,
182 | 3brtr3d 5173 | . . . . 5
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (-(𝑚 + 1) · 𝑋) < 𝑌) | 
| 184 |  | simp-4l 782 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝜑) | 
| 185 | 7, 8 | mulgcl 19110 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑚 · 𝑋) ∈ 𝐵) | 
| 186 | 75, 60, 77, 185 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 · 𝑋) ∈ 𝐵) | 
| 187 | 7, 17, 9 | ogrpinvlt 33101 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp) ∧ (𝑚 · 𝑋) ∈ 𝐵 ∧ ((invg‘𝑊)‘𝑌) ∈ 𝐵) → ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ↔ ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) <
((invg‘𝑊)‘(𝑚 · 𝑋)))) | 
| 188 | 74, 186, 123, 187 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ↔ ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) <
((invg‘𝑊)‘(𝑚 · 𝑋)))) | 
| 189 | 188 | biimpa 476 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ (𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) <
((invg‘𝑊)‘(𝑚 · 𝑋))) | 
| 190 | 189 | adantrr 717 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) <
((invg‘𝑊)‘(𝑚 · 𝑋))) | 
| 191 | 190 | adantr 480 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) <
((invg‘𝑊)‘(𝑚 · 𝑋))) | 
| 192 |  | negdi 11567 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℂ ∧ 1 ∈
ℂ) → -(𝑚 + 1) =
(-𝑚 + -1)) | 
| 193 | 66, 40, 192 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ -(𝑚 + 1) = (-𝑚 + -1)) | 
| 194 | 193 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ (-(𝑚 + 1) + 1) =
((-𝑚 + -1) +
1)) | 
| 195 | 66 | negcld 11608 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ0
→ -𝑚 ∈
ℂ) | 
| 196 | 91 | negcld 11608 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ0
→ -1 ∈ ℂ) | 
| 197 | 195, 196,
91 | addassd 11284 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ ((-𝑚 + -1) + 1) =
(-𝑚 + (-1 +
1))) | 
| 198 | 43 | oveq2i 7443 | . . . . . . . . . . . . . . 15
⊢ (-𝑚 + (-1 + 1)) = (-𝑚 + 0) | 
| 199 | 198 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ (-𝑚 + (-1 + 1)) =
(-𝑚 + 0)) | 
| 200 | 195 | addridd 11462 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ (-𝑚 + 0) = -𝑚) | 
| 201 | 197, 199,
200 | 3eqtrd 2780 | . . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ ((-𝑚 + -1) + 1) =
-𝑚) | 
| 202 | 194, 201 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ (-(𝑚 + 1) + 1) =
-𝑚) | 
| 203 | 202 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
→ ((-(𝑚 + 1) + 1)
·
𝑋) = (-𝑚 · 𝑋)) | 
| 204 | 203 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-(𝑚 + 1) + 1) · 𝑋) = (-𝑚 · 𝑋)) | 
| 205 | 7, 8, 9 | mulgneg 19111 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑚 · 𝑋) = ((invg‘𝑊)‘(𝑚 · 𝑋))) | 
| 206 | 75, 60, 77, 205 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-𝑚 · 𝑋) = ((invg‘𝑊)‘(𝑚 · 𝑋))) | 
| 207 | 204, 206 | eqtrd 2776 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-(𝑚 + 1) + 1) · 𝑋) = ((invg‘𝑊)‘(𝑚 · 𝑋))) | 
| 208 | 207 | ad2antrr 726 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((-(𝑚 + 1) + 1) · 𝑋) = ((invg‘𝑊)‘(𝑚 · 𝑋))) | 
| 209 | 208 | eqcomd 2742 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg‘𝑊)‘(𝑚 · 𝑋)) = ((-(𝑚 + 1) + 1) · 𝑋)) | 
| 210 | 191, 182,
209 | 3brtr3d 5173 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝑌 < ((-(𝑚 + 1) + 1) · 𝑋)) | 
| 211 |  | ovexd 7467 | . . . . . . 7
⊢ (𝜑 → ((-(𝑚 + 1) + 1) · 𝑋) ∈ V) | 
| 212 | 34, 17 | pltle 18379 | . . . . . . 7
⊢ ((𝑊 ∈ oGrp ∧ 𝑌 ∈ 𝐵 ∧ ((-(𝑚 + 1) + 1) · 𝑋) ∈ V) → (𝑌 < ((-(𝑚 + 1) + 1) · 𝑋) → 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋))) | 
| 213 | 2, 120, 211, 212 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → (𝑌 < ((-(𝑚 + 1) + 1) · 𝑋) → 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋))) | 
| 214 | 184, 210,
213 | sylc 65 | . . . . 5
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋)) | 
| 215 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑛 = -(𝑚 + 1) → (𝑛 · 𝑋) = (-(𝑚 + 1) · 𝑋)) | 
| 216 | 215 | breq1d 5152 | . . . . . . 7
⊢ (𝑛 = -(𝑚 + 1) → ((𝑛 · 𝑋) < 𝑌 ↔ (-(𝑚 + 1) · 𝑋) < 𝑌)) | 
| 217 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑛 = -(𝑚 + 1) → (𝑛 + 1) = (-(𝑚 + 1) + 1)) | 
| 218 | 217 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑛 = -(𝑚 + 1) → ((𝑛 + 1) · 𝑋) = ((-(𝑚 + 1) + 1) · 𝑋)) | 
| 219 | 218 | breq2d 5154 | . . . . . . 7
⊢ (𝑛 = -(𝑚 + 1) → (𝑌 ≤ ((𝑛 + 1) · 𝑋) ↔ 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋))) | 
| 220 | 216, 219 | anbi12d 632 | . . . . . 6
⊢ (𝑛 = -(𝑚 + 1) → (((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) ↔ ((-(𝑚 + 1) · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋)))) | 
| 221 | 220 | rspcev 3621 | . . . . 5
⊢ ((-(𝑚 + 1) ∈ ℤ ∧
((-(𝑚 + 1) · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) | 
| 222 | 169, 183,
214, 221 | syl12anc 836 | . . . 4
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) | 
| 223 | 7, 34, 17 | tlt2 32960 | . . . . . 6
⊢ ((𝑊 ∈ Toset ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((invg‘𝑊)‘𝑌) ∈ 𝐵) → (((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌) ∨ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) | 
| 224 | 148, 79, 123, 223 | syl3anc 1372 | . . . . 5
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌) ∨ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) | 
| 225 | 224 | adantr 480 | . . . 4
⊢ ((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) → (((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌) ∨ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) | 
| 226 | 167, 222,
225 | mpjaodan 960 | . . 3
⊢ ((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) | 
| 227 | 2 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑌 < 0 ) → 𝑊 ∈ oGrp) | 
| 228 |  | archirng.2 | . . . . 5
⊢ (𝜑 → 𝑊 ∈ Archi) | 
| 229 | 228 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑌 < 0 ) → 𝑊 ∈ Archi) | 
| 230 | 6 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑌 < 0 ) → 𝑋 ∈ 𝐵) | 
| 231 | 122 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑌 < 0 ) →
((invg‘𝑊)‘𝑌) ∈ 𝐵) | 
| 232 | 16 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑌 < 0 ) → 0 < 𝑋) | 
| 233 | 133 | breq1d 5152 | . . . . . 6
⊢ (𝜑 →
(((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) < 0 ↔ 𝑌 < 0 )) | 
| 234 | 233 | biimpar 477 | . . . . 5
⊢ ((𝜑 ∧ 𝑌 < 0 ) →
((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) < 0 ) | 
| 235 | 7, 17, 9, 18 | ogrpinv0lt 33100 | . . . . . . 7
⊢ ((𝑊 ∈ oGrp ∧
((invg‘𝑊)‘𝑌) ∈ 𝐵) → ( 0 <
((invg‘𝑊)‘𝑌) ↔ ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) < 0 )) | 
| 236 | 2, 122, 235 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → ( 0 <
((invg‘𝑊)‘𝑌) ↔ ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) < 0 )) | 
| 237 | 236 | biimpar 477 | . . . . 5
⊢ ((𝜑 ∧
((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) < 0 ) → 0 <
((invg‘𝑊)‘𝑌)) | 
| 238 | 234, 237 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝑌 < 0 ) → 0 <
((invg‘𝑊)‘𝑌)) | 
| 239 | 7, 18, 17, 34, 8, 227, 229, 230, 231, 232, 238 | archirng 33196 | . . 3
⊢ ((𝜑 ∧ 𝑌 < 0 ) → ∃𝑚 ∈ ℕ0
((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) | 
| 240 | 226, 239 | r19.29a 3161 | . 2
⊢ ((𝜑 ∧ 𝑌 < 0 ) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) | 
| 241 |  | nn0ssz 12638 | . . 3
⊢
ℕ0 ⊆ ℤ | 
| 242 | 2 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 0 < 𝑌) → 𝑊 ∈ oGrp) | 
| 243 | 228 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 0 < 𝑌) → 𝑊 ∈ Archi) | 
| 244 | 6 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 0 < 𝑌) → 𝑋 ∈ 𝐵) | 
| 245 | 120 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 0 < 𝑌) → 𝑌 ∈ 𝐵) | 
| 246 | 16 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 0 < 𝑌) → 0 < 𝑋) | 
| 247 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 0 < 𝑌) → 0 < 𝑌) | 
| 248 | 7, 18, 17, 34, 8, 242, 243, 244, 245, 246, 247 | archirng 33196 | . . 3
⊢ ((𝜑 ∧ 0 < 𝑌) → ∃𝑛 ∈ ℕ0 ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) | 
| 249 |  | ssrexv 4052 | . . 3
⊢
(ℕ0 ⊆ ℤ → (∃𝑛 ∈ ℕ0 ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))) | 
| 250 | 241, 248,
249 | mpsyl 68 | . 2
⊢ ((𝜑 ∧ 0 < 𝑌) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) | 
| 251 | 7, 17 | tlt3 32961 | . . 3
⊢ ((𝑊 ∈ Toset ∧ 𝑌 ∈ 𝐵 ∧ 0 ∈ 𝐵) → (𝑌 = 0 ∨ 𝑌 < 0 ∨ 0 < 𝑌)) | 
| 252 | 29, 120, 33, 251 | syl3anc 1372 | . 2
⊢ (𝜑 → (𝑌 = 0 ∨ 𝑌 < 0 ∨ 0 < 𝑌)) | 
| 253 | 58, 240, 250, 252 | mpjao3dan 1433 | 1
⊢ (𝜑 → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |