Step | Hyp | Ref
| Expression |
1 | | isogrp 31047 |
. . . . 5
⊢ (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd)) |
2 | 1 | simprbi 500 |
. . . 4
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ oMnd) |
3 | | omndtos 31050 |
. . . 4
⊢ (𝑊 ∈ oMnd → 𝑊 ∈ Toset) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Toset) |
5 | | grpmnd 18372 |
. . . . 5
⊢ (𝑊 ∈ Grp → 𝑊 ∈ Mnd) |
6 | 5 | adantr 484 |
. . . 4
⊢ ((𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd) → 𝑊 ∈ Mnd) |
7 | 1, 6 | sylbi 220 |
. . 3
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Mnd) |
8 | | isarchi3.b |
. . . 4
⊢ 𝐵 = (Base‘𝑊) |
9 | | isarchi3.0 |
. . . 4
⊢ 0 =
(0g‘𝑊) |
10 | | isarchi3.x |
. . . 4
⊢ · =
(.g‘𝑊) |
11 | | eqid 2737 |
. . . 4
⊢
(le‘𝑊) =
(le‘𝑊) |
12 | | isarchi3.i |
. . . 4
⊢ < =
(lt‘𝑊) |
13 | 8, 9, 10, 11, 12 | isarchi2 31158 |
. . 3
⊢ ((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) → (𝑊 ∈ Archi ↔
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦(le‘𝑊)(𝑛 · 𝑥)))) |
14 | 4, 7, 13 | syl2anc 587 |
. 2
⊢ (𝑊 ∈ oGrp → (𝑊 ∈ Archi ↔
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦(le‘𝑊)(𝑛 · 𝑥)))) |
15 | | simpr 488 |
. . . . . . . . . . 11
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
16 | 15 | adantr 484 |
. . . . . . . . . 10
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → 𝑛 ∈ ℕ) |
17 | 16 | peano2nnd 11847 |
. . . . . . . . 9
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → (𝑛 + 1) ∈ ℕ) |
18 | | simp-4l 783 |
. . . . . . . . . . . . 13
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ oGrp) |
19 | 18 | adantr 484 |
. . . . . . . . . . . 12
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → 𝑊 ∈ oGrp) |
20 | | ogrpgrp 31048 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Grp) |
21 | 8, 9 | grpidcl 18395 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Grp → 0 ∈ 𝐵) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . . . 12
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → 0 ∈ 𝐵) |
23 | | simp-4r 784 |
. . . . . . . . . . . . 13
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ 𝐵) |
24 | 23 | adantr 484 |
. . . . . . . . . . . 12
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → 𝑥 ∈ 𝐵) |
25 | 20 | ad4antr 732 |
. . . . . . . . . . . . . 14
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ Grp) |
26 | 15 | nnzd 12281 |
. . . . . . . . . . . . . 14
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ) |
27 | 8, 10 | mulgcl 18509 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) → (𝑛 · 𝑥) ∈ 𝐵) |
28 | 25, 26, 23, 27 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) → (𝑛 · 𝑥) ∈ 𝐵) |
29 | 28 | adantr 484 |
. . . . . . . . . . . 12
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → (𝑛 · 𝑥) ∈ 𝐵) |
30 | | simpllr 776 |
. . . . . . . . . . . 12
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → 0 < 𝑥) |
31 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(+g‘𝑊) = (+g‘𝑊) |
32 | 8, 12, 31 | ogrpaddlt 31062 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ oGrp ∧ ( 0 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ (𝑛 · 𝑥) ∈ 𝐵) ∧ 0 < 𝑥) → ( 0 (+g‘𝑊)(𝑛 · 𝑥)) < (𝑥(+g‘𝑊)(𝑛 · 𝑥))) |
33 | 19, 22, 24, 29, 30, 32 | syl131anc 1385 |
. . . . . . . . . . 11
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → ( 0 (+g‘𝑊)(𝑛 · 𝑥)) < (𝑥(+g‘𝑊)(𝑛 · 𝑥))) |
34 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → 𝑊 ∈ Grp) |
35 | 8, 31, 9 | grplid 18397 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Grp ∧ (𝑛 · 𝑥) ∈ 𝐵) → ( 0 (+g‘𝑊)(𝑛 · 𝑥)) = (𝑛 · 𝑥)) |
36 | 34, 29, 35 | syl2anc 587 |
. . . . . . . . . . 11
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → ( 0 (+g‘𝑊)(𝑛 · 𝑥)) = (𝑛 · 𝑥)) |
37 | | nncn 11838 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
38 | | ax-1cn 10787 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
39 | | addcom 11018 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑛 + 1) =
(1 + 𝑛)) |
40 | 37, 38, 39 | sylancl 589 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) = (1 + 𝑛)) |
41 | 40 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 + 1) · 𝑥) = ((1 + 𝑛) · 𝑥)) |
42 | 16, 41 | syl 17 |
. . . . . . . . . . . 12
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → ((𝑛 + 1) · 𝑥) = ((1 + 𝑛) · 𝑥)) |
43 | | grpsgrp 18391 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Grp → 𝑊 ∈ Smgrp) |
44 | 19, 20, 43 | 3syl 18 |
. . . . . . . . . . . . 13
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → 𝑊 ∈ Smgrp) |
45 | | 1nn 11841 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ |
46 | 45 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → 1 ∈ ℕ) |
47 | 8, 10, 31 | mulgnndir 18520 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Smgrp ∧ (1 ∈
ℕ ∧ 𝑛 ∈
ℕ ∧ 𝑥 ∈
𝐵)) → ((1 + 𝑛) · 𝑥) = ((1 · 𝑥)(+g‘𝑊)(𝑛 · 𝑥))) |
48 | 44, 46, 16, 24, 47 | syl13anc 1374 |
. . . . . . . . . . . 12
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → ((1 + 𝑛) · 𝑥) = ((1 · 𝑥)(+g‘𝑊)(𝑛 · 𝑥))) |
49 | 8, 10 | mulg1 18499 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐵 → (1 · 𝑥) = 𝑥) |
50 | 24, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → (1 · 𝑥) = 𝑥) |
51 | 50 | oveq1d 7228 |
. . . . . . . . . . . 12
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → ((1 · 𝑥)(+g‘𝑊)(𝑛 · 𝑥)) = (𝑥(+g‘𝑊)(𝑛 · 𝑥))) |
52 | 42, 48, 51 | 3eqtrrd 2782 |
. . . . . . . . . . 11
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → (𝑥(+g‘𝑊)(𝑛 · 𝑥)) = ((𝑛 + 1) · 𝑥)) |
53 | 33, 36, 52 | 3brtr3d 5084 |
. . . . . . . . . 10
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → (𝑛 · 𝑥) < ((𝑛 + 1) · 𝑥)) |
54 | | tospos 17926 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Toset → 𝑊 ∈ Poset) |
55 | 18, 4, 54 | 3syl 18 |
. . . . . . . . . . . 12
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ Poset) |
56 | | simpllr 776 |
. . . . . . . . . . . 12
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) → 𝑦 ∈ 𝐵) |
57 | 26 | peano2zd 12285 |
. . . . . . . . . . . . 13
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℤ) |
58 | 8, 10 | mulgcl 18509 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Grp ∧ (𝑛 + 1) ∈ ℤ ∧ 𝑥 ∈ 𝐵) → ((𝑛 + 1) · 𝑥) ∈ 𝐵) |
59 | 25, 57, 23, 58 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) → ((𝑛 + 1) · 𝑥) ∈ 𝐵) |
60 | 8, 11, 12 | plelttr 17850 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Poset ∧ (𝑦 ∈ 𝐵 ∧ (𝑛 · 𝑥) ∈ 𝐵 ∧ ((𝑛 + 1) · 𝑥) ∈ 𝐵)) → ((𝑦(le‘𝑊)(𝑛 · 𝑥) ∧ (𝑛 · 𝑥) < ((𝑛 + 1) · 𝑥)) → 𝑦 < ((𝑛 + 1) · 𝑥))) |
61 | 55, 56, 28, 59, 60 | syl13anc 1374 |
. . . . . . . . . . 11
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) → ((𝑦(le‘𝑊)(𝑛 · 𝑥) ∧ (𝑛 · 𝑥) < ((𝑛 + 1) · 𝑥)) → 𝑦 < ((𝑛 + 1) · 𝑥))) |
62 | 61 | impl 459 |
. . . . . . . . . 10
⊢
(((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) ∧ (𝑛 · 𝑥) < ((𝑛 + 1) · 𝑥)) → 𝑦 < ((𝑛 + 1) · 𝑥)) |
63 | 53, 62 | mpdan 687 |
. . . . . . . . 9
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → 𝑦 < ((𝑛 + 1) · 𝑥)) |
64 | | oveq1 7220 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (𝑚 · 𝑥) = ((𝑛 + 1) · 𝑥)) |
65 | 64 | breq2d 5065 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → (𝑦 < (𝑚 · 𝑥) ↔ 𝑦 < ((𝑛 + 1) · 𝑥))) |
66 | 65 | rspcev 3537 |
. . . . . . . . 9
⊢ (((𝑛 + 1) ∈ ℕ ∧ 𝑦 < ((𝑛 + 1) · 𝑥)) → ∃𝑚 ∈ ℕ 𝑦 < (𝑚 · 𝑥)) |
67 | 17, 63, 66 | syl2anc 587 |
. . . . . . . 8
⊢
((((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) ∧ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → ∃𝑚 ∈ ℕ 𝑦 < (𝑚 · 𝑥)) |
68 | 67 | r19.29an 3207 |
. . . . . . 7
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ ∃𝑛 ∈ ℕ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → ∃𝑚 ∈ ℕ 𝑦 < (𝑚 · 𝑥)) |
69 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝑚 · 𝑥) = (𝑛 · 𝑥)) |
70 | 69 | breq2d 5065 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝑦 < (𝑚 · 𝑥) ↔ 𝑦 < (𝑛 · 𝑥))) |
71 | 70 | cbvrexvw 3359 |
. . . . . . 7
⊢
(∃𝑚 ∈
ℕ 𝑦 < (𝑚 · 𝑥) ↔ ∃𝑛 ∈ ℕ 𝑦 < (𝑛 · 𝑥)) |
72 | 68, 71 | sylib 221 |
. . . . . 6
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ ∃𝑛 ∈ ℕ 𝑦(le‘𝑊)(𝑛 · 𝑥)) → ∃𝑛 ∈ ℕ 𝑦 < (𝑛 · 𝑥)) |
73 | 11, 12 | pltle 17839 |
. . . . . . . . 9
⊢ ((𝑊 ∈ oGrp ∧ 𝑦 ∈ 𝐵 ∧ (𝑛 · 𝑥) ∈ 𝐵) → (𝑦 < (𝑛 · 𝑥) → 𝑦(le‘𝑊)(𝑛 · 𝑥))) |
74 | 18, 56, 28, 73 | syl3anc 1373 |
. . . . . . . 8
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ 𝑛 ∈ ℕ) → (𝑦 < (𝑛 · 𝑥) → 𝑦(le‘𝑊)(𝑛 · 𝑥))) |
75 | 74 | reximdva 3193 |
. . . . . . 7
⊢ ((((𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) → (∃𝑛 ∈ ℕ 𝑦 < (𝑛 · 𝑥) → ∃𝑛 ∈ ℕ 𝑦(le‘𝑊)(𝑛 · 𝑥))) |
76 | 75 | imp 410 |
. . . . . 6
⊢
(((((𝑊 ∈ oGrp
∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) ∧ ∃𝑛 ∈ ℕ 𝑦 < (𝑛 · 𝑥)) → ∃𝑛 ∈ ℕ 𝑦(le‘𝑊)(𝑛 · 𝑥)) |
77 | 72, 76 | impbida 801 |
. . . . 5
⊢ ((((𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑥) → (∃𝑛 ∈ ℕ 𝑦(le‘𝑊)(𝑛 · 𝑥) ↔ ∃𝑛 ∈ ℕ 𝑦 < (𝑛 · 𝑥))) |
78 | 77 | pm5.74da 804 |
. . . 4
⊢ (((𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦(le‘𝑊)(𝑛 · 𝑥)) ↔ ( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦 < (𝑛 · 𝑥)))) |
79 | 78 | ralbidva 3117 |
. . 3
⊢ ((𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵) → (∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦(le‘𝑊)(𝑛 · 𝑥)) ↔ ∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦 < (𝑛 · 𝑥)))) |
80 | 79 | ralbidva 3117 |
. 2
⊢ (𝑊 ∈ oGrp →
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦(le‘𝑊)(𝑛 · 𝑥)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦 < (𝑛 · 𝑥)))) |
81 | 14, 80 | bitrd 282 |
1
⊢ (𝑊 ∈ oGrp → (𝑊 ∈ Archi ↔
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦 < (𝑛 · 𝑥)))) |