Step | Hyp | Ref
| Expression |
1 | | 0zd 11389 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 = 0 ) → 0 ∈
ℤ) |
2 | | simpr 477 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 = 0 ) → 𝑦 = 0 ) |
3 | | archiabllem1.u |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ 𝐵) |
4 | | archiabllem.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑊) |
5 | | archiabllem.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝑊) |
6 | | archiabllem.m |
. . . . . . 7
⊢ · =
(.g‘𝑊) |
7 | 4, 5, 6 | mulg0 17546 |
. . . . . 6
⊢ (𝑈 ∈ 𝐵 → (0 · 𝑈) = 0 ) |
8 | 3, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → (0 · 𝑈) = 0 ) |
9 | 8 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 = 0 ) → (0 · 𝑈) = 0 ) |
10 | 2, 9 | eqtr4d 2659 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 = 0 ) → 𝑦 = (0 · 𝑈)) |
11 | | oveq1 6657 |
. . . . 5
⊢ (𝑛 = 0 → (𝑛 · 𝑈) = (0 · 𝑈)) |
12 | 11 | eqeq2d 2632 |
. . . 4
⊢ (𝑛 = 0 → (𝑦 = (𝑛 · 𝑈) ↔ 𝑦 = (0 · 𝑈))) |
13 | 12 | rspcev 3309 |
. . 3
⊢ ((0
∈ ℤ ∧ 𝑦 = (0
·
𝑈)) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) |
14 | 1, 10, 13 | syl2anc 693 |
. 2
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 = 0 ) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) |
15 | | simplr 792 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → 𝑚 ∈ ℕ) |
16 | 15 | nnzd 11481 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → 𝑚 ∈ ℤ) |
17 | 16 | znegcld 11484 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → -𝑚 ∈ ℤ) |
18 | 3 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑈 ∈ 𝐵) |
19 | 18 | ad2antrr 762 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → 𝑈 ∈ 𝐵) |
20 | | eqid 2622 |
. . . . . . . 8
⊢
(invg‘𝑊) = (invg‘𝑊) |
21 | 4, 6, 20 | mulgnegnn 17551 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ ∧ 𝑈 ∈ 𝐵) → (-𝑚 · 𝑈) = ((invg‘𝑊)‘(𝑚 · 𝑈))) |
22 | 15, 19, 21 | syl2anc 693 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → (-𝑚 · 𝑈) = ((invg‘𝑊)‘(𝑚 · 𝑈))) |
23 | | simpr 477 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → ((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) |
24 | 23 | fveq2d 6195 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑦)) = ((invg‘𝑊)‘(𝑚 · 𝑈))) |
25 | | archiabllem.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ oGrp) |
26 | 25 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑊 ∈ oGrp) |
27 | | ogrpgrp 29703 |
. . . . . . . . 9
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Grp) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑊 ∈ Grp) |
29 | | simp2 1062 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑦 ∈ 𝐵) |
30 | 4, 20 | grpinvinv 17482 |
. . . . . . . 8
⊢ ((𝑊 ∈ Grp ∧ 𝑦 ∈ 𝐵) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑦)) = 𝑦) |
31 | 28, 29, 30 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) →
((invg‘𝑊)‘((invg‘𝑊)‘𝑦)) = 𝑦) |
32 | 31 | ad2antrr 762 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑦)) = 𝑦) |
33 | 22, 24, 32 | 3eqtr2rd 2663 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → 𝑦 = (-𝑚 · 𝑈)) |
34 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = -𝑚 → (𝑛 · 𝑈) = (-𝑚 · 𝑈)) |
35 | 34 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑛 = -𝑚 → (𝑦 = (𝑛 · 𝑈) ↔ 𝑦 = (-𝑚 · 𝑈))) |
36 | 35 | rspcev 3309 |
. . . . 5
⊢ ((-𝑚 ∈ ℤ ∧ 𝑦 = (-𝑚 · 𝑈)) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) |
37 | 17, 33, 36 | syl2anc 693 |
. . . 4
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) |
38 | | archiabllem.e |
. . . . 5
⊢ ≤ =
(le‘𝑊) |
39 | | archiabllem.t |
. . . . 5
⊢ < =
(lt‘𝑊) |
40 | | archiabllem.a |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ Archi) |
41 | 40 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑊 ∈ Archi) |
42 | | archiabllem1.p |
. . . . . 6
⊢ (𝜑 → 0 < 𝑈) |
43 | 42 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 0 < 𝑈) |
44 | | simp1 1061 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝜑) |
45 | | archiabllem1.s |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥) → 𝑈 ≤ 𝑥) |
46 | 44, 45 | syl3an1 1359 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥) → 𝑈 ≤ 𝑥) |
47 | 4, 20 | grpinvcl 17467 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝑦 ∈ 𝐵) → ((invg‘𝑊)‘𝑦) ∈ 𝐵) |
48 | 28, 29, 47 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) →
((invg‘𝑊)‘𝑦) ∈ 𝐵) |
49 | 4, 5 | grpidcl 17450 |
. . . . . . . 8
⊢ (𝑊 ∈ Grp → 0 ∈ 𝐵) |
50 | 28, 49 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 0 ∈ 𝐵) |
51 | | simp3 1063 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑦 < 0 ) |
52 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘𝑊) = (+g‘𝑊) |
53 | 4, 39, 52 | ogrpaddlt 29718 |
. . . . . . 7
⊢ ((𝑊 ∈ oGrp ∧ (𝑦 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ ((invg‘𝑊)‘𝑦) ∈ 𝐵) ∧ 𝑦 < 0 ) → (𝑦(+g‘𝑊)((invg‘𝑊)‘𝑦)) < ( 0 (+g‘𝑊)((invg‘𝑊)‘𝑦))) |
54 | 26, 29, 50, 48, 51, 53 | syl131anc 1339 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → (𝑦(+g‘𝑊)((invg‘𝑊)‘𝑦)) < ( 0 (+g‘𝑊)((invg‘𝑊)‘𝑦))) |
55 | 4, 52, 5, 20 | grprinv 17469 |
. . . . . . 7
⊢ ((𝑊 ∈ Grp ∧ 𝑦 ∈ 𝐵) → (𝑦(+g‘𝑊)((invg‘𝑊)‘𝑦)) = 0 ) |
56 | 28, 29, 55 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → (𝑦(+g‘𝑊)((invg‘𝑊)‘𝑦)) = 0 ) |
57 | 4, 52, 5 | grplid 17452 |
. . . . . . 7
⊢ ((𝑊 ∈ Grp ∧
((invg‘𝑊)‘𝑦) ∈ 𝐵) → ( 0 (+g‘𝑊)((invg‘𝑊)‘𝑦)) = ((invg‘𝑊)‘𝑦)) |
58 | 28, 48, 57 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ( 0
(+g‘𝑊)((invg‘𝑊)‘𝑦)) = ((invg‘𝑊)‘𝑦)) |
59 | 54, 56, 58 | 3brtr3d 4684 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 0 <
((invg‘𝑊)‘𝑦)) |
60 | 4, 5, 38, 39, 6, 26, 41, 18, 43, 46, 48, 59 | archiabllem1a 29745 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ∃𝑚 ∈ ℕ
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) |
61 | 37, 60 | r19.29a 3078 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) |
62 | 61 | 3expa 1265 |
. 2
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 < 0 ) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) |
63 | | nnssz 11397 |
. . 3
⊢ ℕ
⊆ ℤ |
64 | 25 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 𝑊 ∈ oGrp) |
65 | 40 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 𝑊 ∈ Archi) |
66 | 3 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 𝑈 ∈ 𝐵) |
67 | 42 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 0 < 𝑈) |
68 | | simp1 1061 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 𝜑) |
69 | 68, 45 | syl3an1 1359 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥) → 𝑈 ≤ 𝑥) |
70 | | simp2 1062 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 𝑦 ∈ 𝐵) |
71 | | simp3 1063 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 0 < 𝑦) |
72 | 4, 5, 38, 39, 6, 64, 65, 66, 67, 69, 70, 71 | archiabllem1a 29745 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝑛 · 𝑈)) |
73 | 72 | 3expa 1265 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝑛 · 𝑈)) |
74 | | ssrexv 3667 |
. . 3
⊢ (ℕ
⊆ ℤ → (∃𝑛 ∈ ℕ 𝑦 = (𝑛 · 𝑈) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈))) |
75 | 63, 73, 74 | mpsyl 68 |
. 2
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑦) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) |
76 | | isogrp 29702 |
. . . . . 6
⊢ (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd)) |
77 | 76 | simprbi 480 |
. . . . 5
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ oMnd) |
78 | | omndtos 29705 |
. . . . 5
⊢ (𝑊 ∈ oMnd → 𝑊 ∈ Toset) |
79 | 25, 77, 78 | 3syl 18 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ Toset) |
80 | 79 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑊 ∈ Toset) |
81 | | simpr 477 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
82 | 25, 27, 49 | 3syl 18 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝐵) |
83 | 82 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 0 ∈ 𝐵) |
84 | 4, 39 | tlt3 29665 |
. . 3
⊢ ((𝑊 ∈ Toset ∧ 𝑦 ∈ 𝐵 ∧ 0 ∈ 𝐵) → (𝑦 = 0 ∨ 𝑦 < 0 ∨ 0 < 𝑦)) |
85 | 80, 81, 83, 84 | syl3anc 1326 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 = 0 ∨ 𝑦 < 0 ∨ 0 < 𝑦)) |
86 | 14, 62, 75, 85 | mpjao3dan 1395 |
1
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) |