| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0zd 12625 | . . 3
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 = 0 ) → 0 ∈
ℤ) | 
| 2 |  | simpr 484 | . . . 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 19092 | . . . . . 6
⊢ (𝑈 ∈ 𝐵 → (0 · 𝑈) = 0 ) | 
| 8 | 3, 7 | syl 17 | . . . . 5
⊢ (𝜑 → (0 · 𝑈) = 0 ) | 
| 9 | 8 | ad2antrr 726 | . . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 = 0 ) → (0 · 𝑈) = 0 ) | 
| 10 | 2, 9 | eqtr4d 2780 | . . 3
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 = 0 ) → 𝑦 = (0 · 𝑈)) | 
| 11 |  | oveq1 7438 | . . . 4
⊢ (𝑛 = 0 → (𝑛 · 𝑈) = (0 · 𝑈)) | 
| 12 | 11 | rspceeqv 3645 | . . 3
⊢ ((0
∈ ℤ ∧ 𝑦 = (0
·
𝑈)) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) | 
| 13 | 1, 10, 12 | syl2anc 584 | . 2
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 = 0 ) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) | 
| 14 |  | simplr 769 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → 𝑚 ∈ ℕ) | 
| 15 | 14 | nnzd 12640 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → 𝑚 ∈ ℤ) | 
| 16 | 15 | znegcld 12724 | . . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → -𝑚 ∈ ℤ) | 
| 17 | 3 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑈 ∈ 𝐵) | 
| 18 | 17 | ad2antrr 726 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → 𝑈 ∈ 𝐵) | 
| 19 |  | eqid 2737 | . . . . . . . 8
⊢
(invg‘𝑊) = (invg‘𝑊) | 
| 20 | 4, 6, 19 | mulgnegnn 19102 | . . . . . . 7
⊢ ((𝑚 ∈ ℕ ∧ 𝑈 ∈ 𝐵) → (-𝑚 · 𝑈) = ((invg‘𝑊)‘(𝑚 · 𝑈))) | 
| 21 | 14, 18, 20 | syl2anc 584 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → (-𝑚 · 𝑈) = ((invg‘𝑊)‘(𝑚 · 𝑈))) | 
| 22 |  | simpr 484 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → ((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) | 
| 23 | 22 | fveq2d 6910 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑦)) = ((invg‘𝑊)‘(𝑚 · 𝑈))) | 
| 24 |  | archiabllem.g | . . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ oGrp) | 
| 25 | 24 | 3ad2ant1 1134 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑊 ∈ oGrp) | 
| 26 |  | ogrpgrp 33080 | . . . . . . . . 9
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Grp) | 
| 27 | 25, 26 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑊 ∈ Grp) | 
| 28 |  | simp2 1138 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑦 ∈ 𝐵) | 
| 29 | 4, 19 | grpinvinv 19023 | . . . . . . . 8
⊢ ((𝑊 ∈ Grp ∧ 𝑦 ∈ 𝐵) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑦)) = 𝑦) | 
| 30 | 27, 28, 29 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) →
((invg‘𝑊)‘((invg‘𝑊)‘𝑦)) = 𝑦) | 
| 31 | 30 | ad2antrr 726 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑦)) = 𝑦) | 
| 32 | 21, 23, 31 | 3eqtr2rd 2784 | . . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → 𝑦 = (-𝑚 · 𝑈)) | 
| 33 |  | oveq1 7438 | . . . . . 6
⊢ (𝑛 = -𝑚 → (𝑛 · 𝑈) = (-𝑚 · 𝑈)) | 
| 34 | 33 | rspceeqv 3645 | . . . . 5
⊢ ((-𝑚 ∈ ℤ ∧ 𝑦 = (-𝑚 · 𝑈)) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) | 
| 35 | 16, 32, 34 | syl2anc 584 | . . . 4
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ) ∧
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) | 
| 36 |  | archiabllem.e | . . . . 5
⊢  ≤ =
(le‘𝑊) | 
| 37 |  | archiabllem.t | . . . . 5
⊢  < =
(lt‘𝑊) | 
| 38 |  | archiabllem.a | . . . . . 6
⊢ (𝜑 → 𝑊 ∈ Archi) | 
| 39 | 38 | 3ad2ant1 1134 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑊 ∈ Archi) | 
| 40 |  | archiabllem1.p | . . . . . 6
⊢ (𝜑 → 0 < 𝑈) | 
| 41 | 40 | 3ad2ant1 1134 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 0 < 𝑈) | 
| 42 |  | simp1 1137 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝜑) | 
| 43 |  | archiabllem1.s | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥) → 𝑈 ≤ 𝑥) | 
| 44 | 42, 43 | syl3an1 1164 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥) → 𝑈 ≤ 𝑥) | 
| 45 | 4, 19 | grpinvcl 19005 | . . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝑦 ∈ 𝐵) → ((invg‘𝑊)‘𝑦) ∈ 𝐵) | 
| 46 | 27, 28, 45 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) →
((invg‘𝑊)‘𝑦) ∈ 𝐵) | 
| 47 | 4, 5 | grpidcl 18983 | . . . . . . . 8
⊢ (𝑊 ∈ Grp → 0 ∈ 𝐵) | 
| 48 | 27, 47 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 0 ∈ 𝐵) | 
| 49 |  | simp3 1139 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑦 < 0 ) | 
| 50 |  | eqid 2737 | . . . . . . . 8
⊢
(+g‘𝑊) = (+g‘𝑊) | 
| 51 | 4, 37, 50 | ogrpaddlt 33094 | . . . . . . 7
⊢ ((𝑊 ∈ oGrp ∧ (𝑦 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ ((invg‘𝑊)‘𝑦) ∈ 𝐵) ∧ 𝑦 < 0 ) → (𝑦(+g‘𝑊)((invg‘𝑊)‘𝑦)) < ( 0 (+g‘𝑊)((invg‘𝑊)‘𝑦))) | 
| 52 | 25, 28, 48, 46, 49, 51 | syl131anc 1385 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → (𝑦(+g‘𝑊)((invg‘𝑊)‘𝑦)) < ( 0 (+g‘𝑊)((invg‘𝑊)‘𝑦))) | 
| 53 | 4, 50, 5, 19 | grprinv 19008 | . . . . . . 7
⊢ ((𝑊 ∈ Grp ∧ 𝑦 ∈ 𝐵) → (𝑦(+g‘𝑊)((invg‘𝑊)‘𝑦)) = 0 ) | 
| 54 | 27, 28, 53 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → (𝑦(+g‘𝑊)((invg‘𝑊)‘𝑦)) = 0 ) | 
| 55 | 4, 50, 5 | grplid 18985 | . . . . . . 7
⊢ ((𝑊 ∈ Grp ∧
((invg‘𝑊)‘𝑦) ∈ 𝐵) → ( 0 (+g‘𝑊)((invg‘𝑊)‘𝑦)) = ((invg‘𝑊)‘𝑦)) | 
| 56 | 27, 46, 55 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ( 0
(+g‘𝑊)((invg‘𝑊)‘𝑦)) = ((invg‘𝑊)‘𝑦)) | 
| 57 | 52, 54, 56 | 3brtr3d 5174 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 0 <
((invg‘𝑊)‘𝑦)) | 
| 58 | 4, 5, 36, 37, 6, 25, 39, 17, 41, 44, 46, 57 | archiabllem1a 33198 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ∃𝑚 ∈ ℕ
((invg‘𝑊)‘𝑦) = (𝑚 · 𝑈)) | 
| 59 | 35, 58 | r19.29a 3162 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) | 
| 60 | 59 | 3expa 1119 | . 2
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 < 0 ) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) | 
| 61 |  | nnssz 12635 | . . 3
⊢ ℕ
⊆ ℤ | 
| 62 | 24 | 3ad2ant1 1134 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 𝑊 ∈ oGrp) | 
| 63 | 38 | 3ad2ant1 1134 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 𝑊 ∈ Archi) | 
| 64 | 3 | 3ad2ant1 1134 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 𝑈 ∈ 𝐵) | 
| 65 | 40 | 3ad2ant1 1134 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 0 < 𝑈) | 
| 66 |  | simp1 1137 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 𝜑) | 
| 67 | 66, 43 | syl3an1 1164 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥) → 𝑈 ≤ 𝑥) | 
| 68 |  | simp2 1138 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 𝑦 ∈ 𝐵) | 
| 69 |  | simp3 1139 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → 0 < 𝑦) | 
| 70 | 4, 5, 36, 37, 6, 62, 63, 64, 65, 67, 68, 69 | archiabllem1a 33198 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝑛 · 𝑈)) | 
| 71 | 70 | 3expa 1119 | . . 3
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝑛 · 𝑈)) | 
| 72 |  | ssrexv 4053 | . . 3
⊢ (ℕ
⊆ ℤ → (∃𝑛 ∈ ℕ 𝑦 = (𝑛 · 𝑈) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈))) | 
| 73 | 61, 71, 72 | mpsyl 68 | . 2
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 0 < 𝑦) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) | 
| 74 |  | isogrp 33079 | . . . . . 6
⊢ (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd)) | 
| 75 | 74 | simprbi 496 | . . . . 5
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ oMnd) | 
| 76 |  | omndtos 33082 | . . . . 5
⊢ (𝑊 ∈ oMnd → 𝑊 ∈ Toset) | 
| 77 | 24, 75, 76 | 3syl 18 | . . . 4
⊢ (𝜑 → 𝑊 ∈ Toset) | 
| 78 | 77 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑊 ∈ Toset) | 
| 79 |  | simpr 484 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) | 
| 80 | 24, 26, 47 | 3syl 18 | . . . 4
⊢ (𝜑 → 0 ∈ 𝐵) | 
| 81 | 80 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 0 ∈ 𝐵) | 
| 82 | 4, 37 | tlt3 32960 | . . 3
⊢ ((𝑊 ∈ Toset ∧ 𝑦 ∈ 𝐵 ∧ 0 ∈ 𝐵) → (𝑦 = 0 ∨ 𝑦 < 0 ∨ 0 < 𝑦)) | 
| 83 | 78, 79, 81, 82 | syl3anc 1373 | . 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 = 0 ∨ 𝑦 < 0 ∨ 0 < 𝑦)) | 
| 84 | 13, 60, 73, 83 | mpjao3dan 1434 | 1
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑈)) |