Step | Hyp | Ref
| Expression |
1 | | neg1z 12213 |
. . 3
⊢ -1 ∈
ℤ |
2 | | archirng.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ oGrp) |
3 | | ogrpgrp 31048 |
. . . . . . . . . 10
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Grp) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ Grp) |
5 | | 1zzd 12208 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
6 | | archirng.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
7 | | archirng.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑊) |
8 | | archirng.x |
. . . . . . . . . 10
⊢ · =
(.g‘𝑊) |
9 | | eqid 2737 |
. . . . . . . . . 10
⊢
(invg‘𝑊) = (invg‘𝑊) |
10 | 7, 8, 9 | mulgneg 18510 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Grp ∧ 1 ∈
ℤ ∧ 𝑋 ∈
𝐵) → (-1 · 𝑋) =
((invg‘𝑊)‘(1 · 𝑋))) |
11 | 4, 5, 6, 10 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (-1 · 𝑋) = ((invg‘𝑊)‘(1 · 𝑋))) |
12 | 7, 8 | mulg1 18499 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝐵 → (1 · 𝑋) = 𝑋) |
13 | 6, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (1 · 𝑋) = 𝑋) |
14 | 13 | fveq2d 6721 |
. . . . . . . 8
⊢ (𝜑 →
((invg‘𝑊)‘(1 · 𝑋)) = ((invg‘𝑊)‘𝑋)) |
15 | 11, 14 | eqtrd 2777 |
. . . . . . 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 31067 |
. . . . . . . . 9
⊢ ((𝑊 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ ((invg‘𝑊)‘𝑋) < 0 )) |
20 | 19 | biimpa 480 |
. . . . . . . 8
⊢ (((𝑊 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → ((invg‘𝑊)‘𝑋) < 0 ) |
21 | 2, 6, 16, 20 | syl21anc 838 |
. . . . . . 7
⊢ (𝜑 →
((invg‘𝑊)‘𝑋) < 0 ) |
22 | 15, 21 | eqbrtrd 5075 |
. . . . . 6
⊢ (𝜑 → (-1 · 𝑋) < 0 ) |
23 | 22 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 0 ) → (-1 · 𝑋) < 0 ) |
24 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 0 ) → 𝑌 = 0 ) |
25 | 23, 24 | breqtrrd 5081 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 0 ) → (-1 · 𝑋) < 𝑌) |
26 | | isogrp 31047 |
. . . . . . . . . 10
⊢ (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd)) |
27 | 26 | simprbi 500 |
. . . . . . . . 9
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ oMnd) |
28 | | omndtos 31050 |
. . . . . . . . 9
⊢ (𝑊 ∈ oMnd → 𝑊 ∈ Toset) |
29 | 2, 27, 28 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Toset) |
30 | | tospos 17926 |
. . . . . . . 8
⊢ (𝑊 ∈ Toset → 𝑊 ∈ Poset) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Poset) |
32 | 7, 18 | grpidcl 18395 |
. . . . . . . 8
⊢ (𝑊 ∈ Grp → 0 ∈ 𝐵) |
33 | 2, 3, 32 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ 𝐵) |
34 | | archirng.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝑊) |
35 | 7, 34 | posref 17825 |
. . . . . . 7
⊢ ((𝑊 ∈ Poset ∧ 0 ∈ 𝐵) → 0 ≤ 0 ) |
36 | 31, 33, 35 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 0 ) |
37 | 36 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 0 ) → 0 ≤ 0
) |
38 | | 1m1e0 11902 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
39 | 38 | negeqi 11071 |
. . . . . . . . 9
⊢ -(1
− 1) = -0 |
40 | | ax-1cn 10787 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
41 | 40, 40 | negsubdii 11163 |
. . . . . . . . 9
⊢ -(1
− 1) = (-1 + 1) |
42 | | neg0 11124 |
. . . . . . . . 9
⊢ -0 =
0 |
43 | 39, 41, 42 | 3eqtr3i 2773 |
. . . . . . . 8
⊢ (-1 + 1)
= 0 |
44 | 43 | oveq1i 7223 |
. . . . . . 7
⊢ ((-1 + 1)
·
𝑋) = (0 · 𝑋) |
45 | 7, 18, 8 | mulg0 18495 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 ) |
46 | 6, 45 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0 · 𝑋) = 0 ) |
47 | 44, 46 | syl5eq 2790 |
. . . . . 6
⊢ (𝜑 → ((-1 + 1) · 𝑋) = 0 ) |
48 | 47 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 0 ) → ((-1 + 1) · 𝑋) = 0 ) |
49 | 37, 24, 48 | 3brtr4d 5085 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 0 ) → 𝑌 ≤ ((-1 + 1) · 𝑋)) |
50 | 25, 49 | jca 515 |
. . 3
⊢ ((𝜑 ∧ 𝑌 = 0 ) → ((-1 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-1 + 1) · 𝑋))) |
51 | | oveq1 7220 |
. . . . . 6
⊢ (𝑛 = -1 → (𝑛 · 𝑋) = (-1 · 𝑋)) |
52 | 51 | breq1d 5063 |
. . . . 5
⊢ (𝑛 = -1 → ((𝑛 · 𝑋) < 𝑌 ↔ (-1 · 𝑋) < 𝑌)) |
53 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑛 = -1 → (𝑛 + 1) = (-1 + 1)) |
54 | 53 | oveq1d 7228 |
. . . . . 6
⊢ (𝑛 = -1 → ((𝑛 + 1) · 𝑋) = ((-1 + 1) · 𝑋)) |
55 | 54 | breq2d 5065 |
. . . . 5
⊢ (𝑛 = -1 → (𝑌 ≤ ((𝑛 + 1) · 𝑋) ↔ 𝑌 ≤ ((-1 + 1) · 𝑋))) |
56 | 52, 55 | anbi12d 634 |
. . . 4
⊢ (𝑛 = -1 → (((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) ↔ ((-1 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-1 + 1) · 𝑋)))) |
57 | 56 | rspcev 3537 |
. . 3
⊢ ((-1
∈ ℤ ∧ ((-1 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-1 + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |
58 | 1, 50, 57 | sylancr 590 |
. 2
⊢ ((𝜑 ∧ 𝑌 = 0 ) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |
59 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) |
60 | 59 | nn0zd 12280 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℤ) |
61 | 60 | ad2antrr 726 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → 𝑚 ∈ ℤ) |
62 | 61 | znegcld 12284 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → -𝑚 ∈ ℤ) |
63 | | 2z 12209 |
. . . . . . 7
⊢ 2 ∈
ℤ |
64 | 63 | a1i 11 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → 2 ∈ ℤ) |
65 | 62, 64 | zsubcld 12287 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → (-𝑚 − 2) ∈ ℤ) |
66 | | nn0cn 12100 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) |
67 | 66 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℂ) |
68 | | 2cnd 11908 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 2 ∈
ℂ) |
69 | 67, 68 | negdi2d 11203 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -(𝑚 + 2) = (-𝑚 − 2)) |
70 | 69 | oveq1d 7228 |
. . . . . . . 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 515 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp)) |
75 | 4 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑊 ∈ Grp) |
76 | 60 | peano2zd 12285 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈
ℤ) |
77 | 6 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
78 | 7, 8 | mulgcl 18509 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑚 + 1) · 𝑋) ∈ 𝐵) |
79 | 75, 76, 77, 78 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · 𝑋) ∈ 𝐵) |
80 | 63 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 2 ∈
ℤ) |
81 | 60, 80 | zaddcld 12286 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 2) ∈
ℤ) |
82 | 7, 8 | mulgcl 18509 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 2) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑚 + 2) · 𝑋) ∈ 𝐵) |
83 | 75, 81, 77, 82 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 2) · 𝑋) ∈ 𝐵) |
84 | 75, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 0 ∈ 𝐵) |
85 | 16 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 0 < 𝑋) |
86 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(+g‘𝑊) = (+g‘𝑊) |
87 | 7, 17, 86 | ogrpaddlt 31062 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ oGrp ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ 0 < 𝑋) → ( 0 (+g‘𝑊)((𝑚 + 1) · 𝑋)) < (𝑋(+g‘𝑊)((𝑚 + 1) · 𝑋))) |
88 | 71, 84, 77, 79, 85, 87 | syl131anc 1385 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ( 0
(+g‘𝑊)((𝑚 + 1) · 𝑋)) < (𝑋(+g‘𝑊)((𝑚 + 1) · 𝑋))) |
89 | 7, 86, 18 | grplid 18397 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Grp ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → ( 0 (+g‘𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) · 𝑋)) |
90 | 75, 79, 89 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ( 0
(+g‘𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) · 𝑋)) |
91 | | 1cnd 10828 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ0
→ 1 ∈ ℂ) |
92 | 66, 91, 91 | addassd 10855 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ0
→ ((𝑚 + 1) + 1) =
(𝑚 + (1 +
1))) |
93 | | 1p1e2 11955 |
. . . . . . . . . . . . . . . . 17
⊢ (1 + 1) =
2 |
94 | 93 | oveq2i 7224 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 + (1 + 1)) = (𝑚 + 2) |
95 | 92, 94 | eqtrdi 2794 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ0
→ ((𝑚 + 1) + 1) =
(𝑚 + 2)) |
96 | 66, 91 | addcld 10852 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℂ) |
97 | 96, 91 | addcomd 11034 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ0
→ ((𝑚 + 1) + 1) = (1 +
(𝑚 + 1))) |
98 | 95, 97 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 2) = (1 +
(𝑚 + 1))) |
99 | 98 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ ((𝑚 + 2) · 𝑋) = ((1 + (𝑚 + 1)) · 𝑋)) |
100 | 99 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 2) · 𝑋) = ((1 + (𝑚 + 1)) · 𝑋)) |
101 | | 1zzd 12208 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 1 ∈
ℤ) |
102 | 7, 8, 86 | mulgdir 18523 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Grp ∧ (1 ∈
ℤ ∧ (𝑚 + 1)
∈ ℤ ∧ 𝑋
∈ 𝐵)) → ((1 +
(𝑚 + 1)) · 𝑋) = ((1 · 𝑋)(+g‘𝑊)((𝑚 + 1) · 𝑋))) |
103 | 75, 101, 76, 77, 102 | syl13anc 1374 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((1 +
(𝑚 + 1)) · 𝑋) = ((1 · 𝑋)(+g‘𝑊)((𝑚 + 1) · 𝑋))) |
104 | 77, 12 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (1 · 𝑋) = 𝑋) |
105 | 104 | oveq1d 7228 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((1 · 𝑋)(+g‘𝑊)((𝑚 + 1) · 𝑋)) = (𝑋(+g‘𝑊)((𝑚 + 1) · 𝑋))) |
106 | 100, 103,
105 | 3eqtrrd 2782 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑋(+g‘𝑊)((𝑚 + 1) · 𝑋)) = ((𝑚 + 2) · 𝑋)) |
107 | 88, 90, 106 | 3brtr3d 5084 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋)) |
108 | 7, 17, 9 | ogrpinvlt 31068 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp) ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((𝑚 + 2) · 𝑋) ∈ 𝐵) → (((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋) ↔ ((invg‘𝑊)‘((𝑚 + 2) · 𝑋)) <
((invg‘𝑊)‘((𝑚 + 1) · 𝑋)))) |
109 | 108 | biimpa 480 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp) ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((𝑚 + 2) · 𝑋) ∈ 𝐵) ∧ ((𝑚 + 1) · 𝑋) < ((𝑚 + 2) · 𝑋)) → ((invg‘𝑊)‘((𝑚 + 2) · 𝑋)) <
((invg‘𝑊)‘((𝑚 + 1) · 𝑋))) |
110 | 74, 79, 83, 107, 109 | syl31anc 1375 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) →
((invg‘𝑊)‘((𝑚 + 2) · 𝑋)) <
((invg‘𝑊)‘((𝑚 + 1) · 𝑋))) |
111 | 7, 8, 9 | mulgneg 18510 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 2) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-(𝑚 + 2) · 𝑋) = ((invg‘𝑊)‘((𝑚 + 2) · 𝑋))) |
112 | 75, 81, 77, 111 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) · 𝑋) = ((invg‘𝑊)‘((𝑚 + 2) · 𝑋))) |
113 | 7, 8, 9 | mulgneg 18510 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-(𝑚 + 1) · 𝑋) = ((invg‘𝑊)‘((𝑚 + 1) · 𝑋))) |
114 | 75, 76, 77, 113 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 1) · 𝑋) = ((invg‘𝑊)‘((𝑚 + 1) · 𝑋))) |
115 | 110, 112,
114 | 3brtr4d 5085 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) · 𝑋) < (-(𝑚 + 1) · 𝑋)) |
116 | 70, 115 | eqbrtrrd 5077 |
. . . . . . 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 18415 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝐵) → ((invg‘𝑊)‘𝑌) ∈ 𝐵) |
122 | 4, 120, 121 | syl2anc 587 |
. . . . . . . . . . 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 778 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋)) |
127 | | simpr 488 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) |
128 | 7, 34 | posasymb 17826 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Poset ∧
((invg‘𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → ((((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) ↔ ((invg‘𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋))) |
129 | 128 | biimpa 480 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Poset ∧
((invg‘𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ (((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌))) → ((invg‘𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋)) |
130 | 119, 124,
125, 126, 127, 129 | syl32anc 1380 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((invg‘𝑊)‘𝑌) = ((𝑚 + 1) · 𝑋)) |
131 | 130 | fveq2d 6721 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) = ((invg‘𝑊)‘((𝑚 + 1) · 𝑋))) |
132 | 7, 9 | grpinvinv 18430 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝐵) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) = 𝑌) |
133 | 4, 120, 132 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 →
((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) = 𝑌) |
134 | 133 | ad4antr 732 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) = 𝑌) |
135 | 118, 131,
134 | 3eqtr2rd 2784 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → 𝑌 = (-(𝑚 + 1) · 𝑋)) |
136 | 117, 135 | breqtrrd 5081 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → ((-𝑚 − 2) · 𝑋) < 𝑌) |
137 | | 1cnd 10828 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → 1 ∈
ℂ) |
138 | 67, 68, 137 | addsubassd 11209 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 2) − 1) = (𝑚 + (2 −
1))) |
139 | | 2m1e1 11956 |
. . . . . . . . . . . . 13
⊢ (2
− 1) = 1 |
140 | 139 | oveq2i 7224 |
. . . . . . . . . . . 12
⊢ (𝑚 + (2 − 1)) = (𝑚 + 1) |
141 | 138, 140 | eqtr2di 2795 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) = ((𝑚 + 2) − 1)) |
142 | 141 | negeqd 11072 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -(𝑚 + 1) = -((𝑚 + 2) − 1)) |
143 | 67, 68 | addcld 10852 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 2) ∈
ℂ) |
144 | 143, 137 | negsubdid 11204 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -((𝑚 + 2) − 1) = (-(𝑚 + 2) + 1)) |
145 | 69 | oveq1d 7228 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-(𝑚 + 2) + 1) = ((-𝑚 − 2) +
1)) |
146 | 142, 144,
145 | 3eqtrrd 2782 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-𝑚 − 2) + 1) = -(𝑚 + 1)) |
147 | 146 | oveq1d 7228 |
. . . . . . . 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 12284 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → -𝑚 ∈
ℤ) |
151 | 150, 80 | zsubcld 12287 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-𝑚 − 2) ∈
ℤ) |
152 | 151 | peano2zd 12285 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-𝑚 − 2) + 1) ∈
ℤ) |
153 | 7, 8 | mulgcl 18509 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ ((-𝑚 − 2) + 1) ∈ ℤ
∧ 𝑋 ∈ 𝐵) → (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵) |
154 | 75, 152, 77, 153 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵) |
155 | 7, 34 | posref 17825 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Poset ∧ (((-𝑚 − 2) + 1) · 𝑋) ∈ 𝐵) → (((-𝑚 − 2) + 1) · 𝑋) ≤ (((-𝑚 − 2) + 1) · 𝑋)) |
156 | 149, 154,
155 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((-𝑚 − 2) + 1) · 𝑋) ≤ (((-𝑚 − 2) + 1) · 𝑋)) |
157 | 147, 156 | eqbrtrrd 5077 |
. . . . . . 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 5075 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌)) → 𝑌 ≤ (((-𝑚 − 2) + 1) · 𝑋)) |
160 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑛 = (-𝑚 − 2) → (𝑛 · 𝑋) = ((-𝑚 − 2) · 𝑋)) |
161 | 160 | breq1d 5063 |
. . . . . . 7
⊢ (𝑛 = (-𝑚 − 2) → ((𝑛 · 𝑋) < 𝑌 ↔ ((-𝑚 − 2) · 𝑋) < 𝑌)) |
162 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑛 = (-𝑚 − 2) → (𝑛 + 1) = ((-𝑚 − 2) + 1)) |
163 | 162 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝑛 = (-𝑚 − 2) → ((𝑛 + 1) · 𝑋) = (((-𝑚 − 2) + 1) · 𝑋)) |
164 | 163 | breq2d 5065 |
. . . . . . 7
⊢ (𝑛 = (-𝑚 − 2) → (𝑌 ≤ ((𝑛 + 1) · 𝑋) ↔ 𝑌 ≤ (((-𝑚 − 2) + 1) · 𝑋))) |
165 | 161, 164 | anbi12d 634 |
. . . . . 6
⊢ (𝑛 = (-𝑚 − 2) → (((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) ↔ (((-𝑚 − 2) · 𝑋) < 𝑌 ∧ 𝑌 ≤ (((-𝑚 − 2) + 1) · 𝑋)))) |
166 | 165 | rspcev 3537 |
. . . . 5
⊢ (((-𝑚 − 2) ∈ ℤ ∧
(((-𝑚 − 2) · 𝑋) < 𝑌 ∧ 𝑌 ≤ (((-𝑚 − 2) + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |
167 | 65, 136, 159, 166 | syl12anc 837 |
. . . 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 12284 |
. . . . 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 515 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ (𝑚 ∈ ℕ0
∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋)) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) → (𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp)) |
173 | 172 | 3anassrs 1362 |
. . . . . . 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 488 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) |
177 | 7, 17, 9 | ogrpinvlt 31068 |
. . . . . . . 8
⊢ (((𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp) ∧
((invg‘𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) → (((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋) ↔ ((invg‘𝑊)‘((𝑚 + 1) · 𝑋)) <
((invg‘𝑊)‘((invg‘𝑊)‘𝑌)))) |
178 | 177 | biimpa 480 |
. . . . . . 7
⊢ ((((𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp) ∧
((invg‘𝑊)‘𝑌) ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg‘𝑊)‘((𝑚 + 1) · 𝑋)) <
((invg‘𝑊)‘((invg‘𝑊)‘𝑌))) |
179 | 173, 174,
175, 176, 178 | syl31anc 1375 |
. . . . . 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 2743 |
. . . . . 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 5084 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → (-(𝑚 + 1) · 𝑋) < 𝑌) |
184 | | simp-4l 783 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝜑) |
185 | 7, 8 | mulgcl 18509 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑚 · 𝑋) ∈ 𝐵) |
186 | 75, 60, 77, 185 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (𝑚 · 𝑋) ∈ 𝐵) |
187 | 7, 17, 9 | ogrpinvlt 31068 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ oGrp ∧
(oppg‘𝑊) ∈ oGrp) ∧ (𝑚 · 𝑋) ∈ 𝐵 ∧ ((invg‘𝑊)‘𝑌) ∈ 𝐵) → ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ↔ ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) <
((invg‘𝑊)‘(𝑚 · 𝑋)))) |
188 | 74, 186, 123, 187 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ↔ ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) <
((invg‘𝑊)‘(𝑚 · 𝑋)))) |
189 | 188 | biimpa 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ (𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) <
((invg‘𝑊)‘(𝑚 · 𝑋))) |
190 | 189 | adantrr 717 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) <
((invg‘𝑊)‘(𝑚 · 𝑋))) |
191 | 190 | adantr 484 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) <
((invg‘𝑊)‘(𝑚 · 𝑋))) |
192 | | negdi 11135 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℂ ∧ 1 ∈
ℂ) → -(𝑚 + 1) =
(-𝑚 + -1)) |
193 | 66, 40, 192 | sylancl 589 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ -(𝑚 + 1) = (-𝑚 + -1)) |
194 | 193 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ (-(𝑚 + 1) + 1) =
((-𝑚 + -1) +
1)) |
195 | 66 | negcld 11176 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ0
→ -𝑚 ∈
ℂ) |
196 | 91 | negcld 11176 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ0
→ -1 ∈ ℂ) |
197 | 195, 196,
91 | addassd 10855 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ ((-𝑚 + -1) + 1) =
(-𝑚 + (-1 +
1))) |
198 | 43 | oveq2i 7224 |
. . . . . . . . . . . . . . 15
⊢ (-𝑚 + (-1 + 1)) = (-𝑚 + 0) |
199 | 198 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ (-𝑚 + (-1 + 1)) =
(-𝑚 + 0)) |
200 | 195 | addid1d 11032 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ (-𝑚 + 0) = -𝑚) |
201 | 197, 199,
200 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ ((-𝑚 + -1) + 1) =
-𝑚) |
202 | 194, 201 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ (-(𝑚 + 1) + 1) =
-𝑚) |
203 | 202 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
→ ((-(𝑚 + 1) + 1)
·
𝑋) = (-𝑚 · 𝑋)) |
204 | 203 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-(𝑚 + 1) + 1) · 𝑋) = (-𝑚 · 𝑋)) |
205 | 7, 8, 9 | mulgneg 18510 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑚 · 𝑋) = ((invg‘𝑊)‘(𝑚 · 𝑋))) |
206 | 75, 60, 77, 205 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (-𝑚 · 𝑋) = ((invg‘𝑊)‘(𝑚 · 𝑋))) |
207 | 204, 206 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → ((-(𝑚 + 1) + 1) · 𝑋) = ((invg‘𝑊)‘(𝑚 · 𝑋))) |
208 | 207 | ad2antrr 726 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((-(𝑚 + 1) + 1) · 𝑋) = ((invg‘𝑊)‘(𝑚 · 𝑋))) |
209 | 208 | eqcomd 2743 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ((invg‘𝑊)‘(𝑚 · 𝑋)) = ((-(𝑚 + 1) + 1) · 𝑋)) |
210 | 191, 182,
209 | 3brtr3d 5084 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝑌 < ((-(𝑚 + 1) + 1) · 𝑋)) |
211 | | ovexd 7248 |
. . . . . . 7
⊢ (𝜑 → ((-(𝑚 + 1) + 1) · 𝑋) ∈ V) |
212 | 34, 17 | pltle 17839 |
. . . . . . 7
⊢ ((𝑊 ∈ oGrp ∧ 𝑌 ∈ 𝐵 ∧ ((-(𝑚 + 1) + 1) · 𝑋) ∈ V) → (𝑌 < ((-(𝑚 + 1) + 1) · 𝑋) → 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋))) |
213 | 2, 120, 211, 212 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝑌 < ((-(𝑚 + 1) + 1) · 𝑋) → 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋))) |
214 | 184, 210,
213 | sylc 65 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋)) |
215 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑛 = -(𝑚 + 1) → (𝑛 · 𝑋) = (-(𝑚 + 1) · 𝑋)) |
216 | 215 | breq1d 5063 |
. . . . . . 7
⊢ (𝑛 = -(𝑚 + 1) → ((𝑛 · 𝑋) < 𝑌 ↔ (-(𝑚 + 1) · 𝑋) < 𝑌)) |
217 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑛 = -(𝑚 + 1) → (𝑛 + 1) = (-(𝑚 + 1) + 1)) |
218 | 217 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝑛 = -(𝑚 + 1) → ((𝑛 + 1) · 𝑋) = ((-(𝑚 + 1) + 1) · 𝑋)) |
219 | 218 | breq2d 5065 |
. . . . . . 7
⊢ (𝑛 = -(𝑚 + 1) → (𝑌 ≤ ((𝑛 + 1) · 𝑋) ↔ 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋))) |
220 | 216, 219 | anbi12d 634 |
. . . . . 6
⊢ (𝑛 = -(𝑚 + 1) → (((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) ↔ ((-(𝑚 + 1) · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋)))) |
221 | 220 | rspcev 3537 |
. . . . 5
⊢ ((-(𝑚 + 1) ∈ ℤ ∧
((-(𝑚 + 1) · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((-(𝑚 + 1) + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |
222 | 169, 183,
214, 221 | syl12anc 837 |
. . . 4
⊢
(((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) ∧ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |
223 | 7, 34, 17 | tlt2 30966 |
. . . . . 6
⊢ ((𝑊 ∈ Toset ∧ ((𝑚 + 1) · 𝑋) ∈ 𝐵 ∧ ((invg‘𝑊)‘𝑌) ∈ 𝐵) → (((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌) ∨ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) |
224 | 148, 79, 123, 223 | syl3anc 1373 |
. . . . 5
⊢ (((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) → (((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌) ∨ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) |
225 | 224 | adantr 484 |
. . . 4
⊢ ((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) → (((𝑚 + 1) · 𝑋) ≤
((invg‘𝑊)‘𝑌) ∨ ((invg‘𝑊)‘𝑌) < ((𝑚 + 1) · 𝑋))) |
226 | 167, 222,
225 | mpjaodan 959 |
. . 3
⊢ ((((𝜑 ∧ 𝑌 < 0 ) ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |
227 | 2 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 < 0 ) → 𝑊 ∈ oGrp) |
228 | | archirng.2 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ Archi) |
229 | 228 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 < 0 ) → 𝑊 ∈ Archi) |
230 | 6 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 < 0 ) → 𝑋 ∈ 𝐵) |
231 | 122 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 < 0 ) →
((invg‘𝑊)‘𝑌) ∈ 𝐵) |
232 | 16 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 < 0 ) → 0 < 𝑋) |
233 | 133 | breq1d 5063 |
. . . . . 6
⊢ (𝜑 →
(((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) < 0 ↔ 𝑌 < 0 )) |
234 | 233 | biimpar 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 < 0 ) →
((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) < 0 ) |
235 | 7, 17, 9, 18 | ogrpinv0lt 31067 |
. . . . . . 7
⊢ ((𝑊 ∈ oGrp ∧
((invg‘𝑊)‘𝑌) ∈ 𝐵) → ( 0 <
((invg‘𝑊)‘𝑌) ↔ ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) < 0 )) |
236 | 2, 122, 235 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ( 0 <
((invg‘𝑊)‘𝑌) ↔ ((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) < 0 )) |
237 | 236 | biimpar 481 |
. . . . 5
⊢ ((𝜑 ∧
((invg‘𝑊)‘((invg‘𝑊)‘𝑌)) < 0 ) → 0 <
((invg‘𝑊)‘𝑌)) |
238 | 234, 237 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 < 0 ) → 0 <
((invg‘𝑊)‘𝑌)) |
239 | 7, 18, 17, 34, 8, 227, 229, 230, 231, 232, 238 | archirng 31161 |
. . 3
⊢ ((𝜑 ∧ 𝑌 < 0 ) → ∃𝑚 ∈ ℕ0
((𝑚 · 𝑋) <
((invg‘𝑊)‘𝑌) ∧ ((invg‘𝑊)‘𝑌) ≤ ((𝑚 + 1) · 𝑋))) |
240 | 226, 239 | r19.29a 3208 |
. 2
⊢ ((𝜑 ∧ 𝑌 < 0 ) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |
241 | | nn0ssz 12198 |
. . 3
⊢
ℕ0 ⊆ ℤ |
242 | 2 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝑌) → 𝑊 ∈ oGrp) |
243 | 228 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝑌) → 𝑊 ∈ Archi) |
244 | 6 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝑌) → 𝑋 ∈ 𝐵) |
245 | 120 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝑌) → 𝑌 ∈ 𝐵) |
246 | 16 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝑌) → 0 < 𝑋) |
247 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝑌) → 0 < 𝑌) |
248 | 7, 18, 17, 34, 8, 242, 243, 244, 245, 246, 247 | archirng 31161 |
. . 3
⊢ ((𝜑 ∧ 0 < 𝑌) → ∃𝑛 ∈ ℕ0 ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |
249 | | ssrexv 3968 |
. . 3
⊢
(ℕ0 ⊆ ℤ → (∃𝑛 ∈ ℕ0 ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))) |
250 | 241, 248,
249 | mpsyl 68 |
. 2
⊢ ((𝜑 ∧ 0 < 𝑌) → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |
251 | 7, 17 | tlt3 30967 |
. . 3
⊢ ((𝑊 ∈ Toset ∧ 𝑌 ∈ 𝐵 ∧ 0 ∈ 𝐵) → (𝑌 = 0 ∨ 𝑌 < 0 ∨ 0 < 𝑌)) |
252 | 29, 120, 33, 251 | syl3anc 1373 |
. 2
⊢ (𝜑 → (𝑌 = 0 ∨ 𝑌 < 0 ∨ 0 < 𝑌)) |
253 | 58, 240, 250, 252 | mpjao3dan 1433 |
1
⊢ (𝜑 → ∃𝑛 ∈ ℤ ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |