Step | Hyp | Ref
| Expression |
1 | | simplr 769 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 𝑚 ∈ ℕ0) |
2 | | nn0p1nn 12129 |
. . . 4
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (𝑚 + 1) ∈ ℕ) |
4 | | archiabllem1.u |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝐵) |
5 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 𝑈 ∈ 𝐵) |
6 | | archiabllem.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑊) |
7 | | archiabllem.m |
. . . . . . . 8
⊢ · =
(.g‘𝑊) |
8 | 6, 7 | mulg1 18499 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐵 → (1 · 𝑈) = 𝑈) |
9 | 5, 8 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (1 · 𝑈) = 𝑈) |
10 | 9 | oveq1d 7228 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → ((1 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈)) = (𝑈(+g‘𝑊)(𝑚 · 𝑈))) |
11 | | archiabllem.g |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ oGrp) |
12 | 11 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 𝑊 ∈ oGrp) |
13 | | ogrpgrp 31048 |
. . . . . . 7
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Grp) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 𝑊 ∈ Grp) |
15 | | 1zzd 12208 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 1 ∈
ℤ) |
16 | 1 | nn0zd 12280 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 𝑚 ∈ ℤ) |
17 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘𝑊) = (+g‘𝑊) |
18 | 6, 7, 17 | mulgdir 18523 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ (1 ∈
ℤ ∧ 𝑚 ∈
ℤ ∧ 𝑈 ∈
𝐵)) → ((1 + 𝑚) · 𝑈) = ((1 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) |
19 | 14, 15, 16, 5, 18 | syl13anc 1374 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → ((1 + 𝑚) · 𝑈) = ((1 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) |
20 | | isogrp 31047 |
. . . . . . . . . 10
⊢ (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd)) |
21 | 20 | simprbi 500 |
. . . . . . . . 9
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ oMnd) |
22 | | omndtos 31050 |
. . . . . . . . 9
⊢ (𝑊 ∈ oMnd → 𝑊 ∈ Toset) |
23 | | tospos 17926 |
. . . . . . . . 9
⊢ (𝑊 ∈ Toset → 𝑊 ∈ Poset) |
24 | 21, 22, 23 | 3syl 18 |
. . . . . . . 8
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Poset) |
25 | 12, 24 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 𝑊 ∈ Poset) |
26 | | archiabllem1a.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
27 | 26 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 𝑋 ∈ 𝐵) |
28 | 6, 7 | mulgcl 18509 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑈 ∈ 𝐵) → (𝑚 · 𝑈) ∈ 𝐵) |
29 | 14, 16, 5, 28 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (𝑚 · 𝑈) ∈ 𝐵) |
30 | | eqid 2737 |
. . . . . . . . 9
⊢
(-g‘𝑊) = (-g‘𝑊) |
31 | 6, 30 | grpsubcl 18443 |
. . . . . . . 8
⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ (𝑚 · 𝑈) ∈ 𝐵) → (𝑋(-g‘𝑊)(𝑚 · 𝑈)) ∈ 𝐵) |
32 | 14, 27, 29, 31 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (𝑋(-g‘𝑊)(𝑚 · 𝑈)) ∈ 𝐵) |
33 | 16 | peano2zd 12285 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (𝑚 + 1) ∈ ℤ) |
34 | 6, 7 | mulgcl 18509 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ (𝑚 + 1) ∈ ℤ ∧ 𝑈 ∈ 𝐵) → ((𝑚 + 1) · 𝑈) ∈ 𝐵) |
35 | 14, 33, 5, 34 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → ((𝑚 + 1) · 𝑈) ∈ 𝐵) |
36 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 𝑋 ≤ ((𝑚 + 1) · 𝑈)) |
37 | | archiabllem.e |
. . . . . . . . . 10
⊢ ≤ =
(le‘𝑊) |
38 | 6, 37, 30 | ogrpsub 31061 |
. . . . . . . . 9
⊢ ((𝑊 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ ((𝑚 + 1) · 𝑈) ∈ 𝐵 ∧ (𝑚 · 𝑈) ∈ 𝐵) ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈)) → (𝑋(-g‘𝑊)(𝑚 · 𝑈)) ≤ (((𝑚 + 1) · 𝑈)(-g‘𝑊)(𝑚 · 𝑈))) |
39 | 12, 27, 35, 29, 36, 38 | syl131anc 1385 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (𝑋(-g‘𝑊)(𝑚 · 𝑈)) ≤ (((𝑚 + 1) · 𝑈)(-g‘𝑊)(𝑚 · 𝑈))) |
40 | 1 | nn0cnd 12152 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 𝑚 ∈ ℂ) |
41 | | 1cnd 10828 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 1 ∈
ℂ) |
42 | 40, 41 | pncan2d 11191 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → ((𝑚 + 1) − 𝑚) = 1) |
43 | 42 | oveq1d 7228 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (((𝑚 + 1) − 𝑚) · 𝑈) = (1 · 𝑈)) |
44 | 6, 7, 30 | mulgsubdir 18531 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ ((𝑚 + 1) ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑈 ∈ 𝐵)) → (((𝑚 + 1) − 𝑚) · 𝑈) = (((𝑚 + 1) · 𝑈)(-g‘𝑊)(𝑚 · 𝑈))) |
45 | 14, 33, 16, 5, 44 | syl13anc 1374 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (((𝑚 + 1) − 𝑚) · 𝑈) = (((𝑚 + 1) · 𝑈)(-g‘𝑊)(𝑚 · 𝑈))) |
46 | 43, 45, 9 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (((𝑚 + 1) · 𝑈)(-g‘𝑊)(𝑚 · 𝑈)) = 𝑈) |
47 | 39, 46 | breqtrd 5079 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (𝑋(-g‘𝑊)(𝑚 · 𝑈)) ≤ 𝑈) |
48 | | archiabllem1.s |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥) → 𝑈 ≤ 𝑥) |
49 | 48 | 3expia 1123 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 < 𝑥 → 𝑈 ≤ 𝑥)) |
50 | 49 | ralrimiva 3105 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ( 0 < 𝑥 → 𝑈 ≤ 𝑥)) |
51 | 50 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → ∀𝑥 ∈ 𝐵 ( 0 < 𝑥 → 𝑈 ≤ 𝑥)) |
52 | | archiabllem.0 |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑊) |
53 | 6, 52, 30 | grpsubid 18447 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ (𝑚 · 𝑈) ∈ 𝐵) → ((𝑚 · 𝑈)(-g‘𝑊)(𝑚 · 𝑈)) = 0 ) |
54 | 14, 29, 53 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → ((𝑚 · 𝑈)(-g‘𝑊)(𝑚 · 𝑈)) = 0 ) |
55 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (𝑚 · 𝑈) < 𝑋) |
56 | | archiabllem.t |
. . . . . . . . . . 11
⊢ < =
(lt‘𝑊) |
57 | 6, 56, 30 | ogrpsublt 31066 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ oGrp ∧ ((𝑚 · 𝑈) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑚 · 𝑈) ∈ 𝐵) ∧ (𝑚 · 𝑈) < 𝑋) → ((𝑚 · 𝑈)(-g‘𝑊)(𝑚 · 𝑈)) < (𝑋(-g‘𝑊)(𝑚 · 𝑈))) |
58 | 12, 29, 27, 29, 55, 57 | syl131anc 1385 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → ((𝑚 · 𝑈)(-g‘𝑊)(𝑚 · 𝑈)) < (𝑋(-g‘𝑊)(𝑚 · 𝑈))) |
59 | 54, 58 | eqbrtrrd 5077 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 0 < (𝑋(-g‘𝑊)(𝑚 · 𝑈))) |
60 | | breq2 5057 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑋(-g‘𝑊)(𝑚 · 𝑈)) → ( 0 < 𝑥 ↔ 0 < (𝑋(-g‘𝑊)(𝑚 · 𝑈)))) |
61 | | breq2 5057 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑋(-g‘𝑊)(𝑚 · 𝑈)) → (𝑈 ≤ 𝑥 ↔ 𝑈 ≤ (𝑋(-g‘𝑊)(𝑚 · 𝑈)))) |
62 | 60, 61 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝑥 = (𝑋(-g‘𝑊)(𝑚 · 𝑈)) → (( 0 < 𝑥 → 𝑈 ≤ 𝑥) ↔ ( 0 < (𝑋(-g‘𝑊)(𝑚 · 𝑈)) → 𝑈 ≤ (𝑋(-g‘𝑊)(𝑚 · 𝑈))))) |
63 | 62 | rspcv 3532 |
. . . . . . . 8
⊢ ((𝑋(-g‘𝑊)(𝑚 · 𝑈)) ∈ 𝐵 → (∀𝑥 ∈ 𝐵 ( 0 < 𝑥 → 𝑈 ≤ 𝑥) → ( 0 < (𝑋(-g‘𝑊)(𝑚 · 𝑈)) → 𝑈 ≤ (𝑋(-g‘𝑊)(𝑚 · 𝑈))))) |
64 | 32, 51, 59, 63 | syl3c 66 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 𝑈 ≤ (𝑋(-g‘𝑊)(𝑚 · 𝑈))) |
65 | 6, 37 | posasymb 17826 |
. . . . . . . 8
⊢ ((𝑊 ∈ Poset ∧ (𝑋(-g‘𝑊)(𝑚 · 𝑈)) ∈ 𝐵 ∧ 𝑈 ∈ 𝐵) → (((𝑋(-g‘𝑊)(𝑚 · 𝑈)) ≤ 𝑈 ∧ 𝑈 ≤ (𝑋(-g‘𝑊)(𝑚 · 𝑈))) ↔ (𝑋(-g‘𝑊)(𝑚 · 𝑈)) = 𝑈)) |
66 | 65 | biimpa 480 |
. . . . . . 7
⊢ (((𝑊 ∈ Poset ∧ (𝑋(-g‘𝑊)(𝑚 · 𝑈)) ∈ 𝐵 ∧ 𝑈 ∈ 𝐵) ∧ ((𝑋(-g‘𝑊)(𝑚 · 𝑈)) ≤ 𝑈 ∧ 𝑈 ≤ (𝑋(-g‘𝑊)(𝑚 · 𝑈)))) → (𝑋(-g‘𝑊)(𝑚 · 𝑈)) = 𝑈) |
67 | 25, 32, 5, 47, 64, 66 | syl32anc 1380 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (𝑋(-g‘𝑊)(𝑚 · 𝑈)) = 𝑈) |
68 | 67 | oveq1d 7228 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → ((𝑋(-g‘𝑊)(𝑚 · 𝑈))(+g‘𝑊)(𝑚 · 𝑈)) = (𝑈(+g‘𝑊)(𝑚 · 𝑈))) |
69 | 10, 19, 68 | 3eqtr4rd 2788 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → ((𝑋(-g‘𝑊)(𝑚 · 𝑈))(+g‘𝑊)(𝑚 · 𝑈)) = ((1 + 𝑚) · 𝑈)) |
70 | 6, 17, 30 | grpnpcan 18455 |
. . . . 5
⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ (𝑚 · 𝑈) ∈ 𝐵) → ((𝑋(-g‘𝑊)(𝑚 · 𝑈))(+g‘𝑊)(𝑚 · 𝑈)) = 𝑋) |
71 | 14, 27, 29, 70 | syl3anc 1373 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → ((𝑋(-g‘𝑊)(𝑚 · 𝑈))(+g‘𝑊)(𝑚 · 𝑈)) = 𝑋) |
72 | 41, 40 | addcomd 11034 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → (1 + 𝑚) = (𝑚 + 1)) |
73 | 72 | oveq1d 7228 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → ((1 + 𝑚) · 𝑈) = ((𝑚 + 1) · 𝑈)) |
74 | 69, 71, 73 | 3eqtr3d 2785 |
. . 3
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → 𝑋 = ((𝑚 + 1) · 𝑈)) |
75 | | oveq1 7220 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → (𝑛 · 𝑈) = ((𝑚 + 1) · 𝑈)) |
76 | 75 | rspceeqv 3552 |
. . 3
⊢ (((𝑚 + 1) ∈ ℕ ∧ 𝑋 = ((𝑚 + 1) · 𝑈)) → ∃𝑛 ∈ ℕ 𝑋 = (𝑛 · 𝑈)) |
77 | 3, 74, 76 | syl2anc 587 |
. 2
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) → ∃𝑛 ∈ ℕ 𝑋 = (𝑛 · 𝑈)) |
78 | | archiabllem.a |
. . 3
⊢ (𝜑 → 𝑊 ∈ Archi) |
79 | | archiabllem1.p |
. . 3
⊢ (𝜑 → 0 < 𝑈) |
80 | | archiabllem1a.c |
. . 3
⊢ (𝜑 → 0 < 𝑋) |
81 | 6, 52, 56, 37, 7, 11, 78, 4, 26, 79, 80 | archirng 31161 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ ℕ0 ((𝑚 · 𝑈) < 𝑋 ∧ 𝑋 ≤ ((𝑚 + 1) · 𝑈))) |
82 | 77, 81 | r19.29a 3208 |
1
⊢ (𝜑 → ∃𝑛 ∈ ℕ 𝑋 = (𝑛 · 𝑈)) |