| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . 4
⊢ (𝑚 = 0 → (𝑚 · 𝑋) = (0 · 𝑋)) |
| 2 | 1 | breq2d 5155 |
. . 3
⊢ (𝑚 = 0 → (𝑌 ≤ (𝑚 · 𝑋) ↔ 𝑌 ≤ (0 · 𝑋))) |
| 3 | | oveq1 7438 |
. . . 4
⊢ (𝑚 = 𝑛 → (𝑚 · 𝑋) = (𝑛 · 𝑋)) |
| 4 | 3 | breq2d 5155 |
. . 3
⊢ (𝑚 = 𝑛 → (𝑌 ≤ (𝑚 · 𝑋) ↔ 𝑌 ≤ (𝑛 · 𝑋))) |
| 5 | | oveq1 7438 |
. . . 4
⊢ (𝑚 = (𝑛 + 1) → (𝑚 · 𝑋) = ((𝑛 + 1) · 𝑋)) |
| 6 | 5 | breq2d 5155 |
. . 3
⊢ (𝑚 = (𝑛 + 1) → (𝑌 ≤ (𝑚 · 𝑋) ↔ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |
| 7 | | archirng.6 |
. . . . 5
⊢ (𝜑 → 0 < 𝑌) |
| 8 | | archirng.1 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ oGrp) |
| 9 | | isogrp 33079 |
. . . . . . . 8
⊢ (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd)) |
| 10 | 9 | simprbi 496 |
. . . . . . 7
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ oMnd) |
| 11 | | omndtos 33082 |
. . . . . . 7
⊢ (𝑊 ∈ oMnd → 𝑊 ∈ Toset) |
| 12 | 8, 10, 11 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ Toset) |
| 13 | | ogrpgrp 33080 |
. . . . . . . 8
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Grp) |
| 14 | 8, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Grp) |
| 15 | | archirng.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑊) |
| 16 | | archirng.0 |
. . . . . . . 8
⊢ 0 =
(0g‘𝑊) |
| 17 | 15, 16 | grpidcl 18983 |
. . . . . . 7
⊢ (𝑊 ∈ Grp → 0 ∈ 𝐵) |
| 18 | 14, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ∈ 𝐵) |
| 19 | | archirng.4 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 20 | | archirng.l |
. . . . . . 7
⊢ ≤ =
(le‘𝑊) |
| 21 | | archirng.i |
. . . . . . 7
⊢ < =
(lt‘𝑊) |
| 22 | 15, 20, 21 | tltnle 18467 |
. . . . . 6
⊢ ((𝑊 ∈ Toset ∧ 0 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( 0 < 𝑌 ↔ ¬ 𝑌 ≤ 0 )) |
| 23 | 12, 18, 19, 22 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ( 0 < 𝑌 ↔ ¬ 𝑌 ≤ 0 )) |
| 24 | 7, 23 | mpbid 232 |
. . . 4
⊢ (𝜑 → ¬ 𝑌 ≤ 0 ) |
| 25 | | archirng.3 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 26 | | archirng.x |
. . . . . . 7
⊢ · =
(.g‘𝑊) |
| 27 | 15, 16, 26 | mulg0 19092 |
. . . . . 6
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 ) |
| 28 | 25, 27 | syl 17 |
. . . . 5
⊢ (𝜑 → (0 · 𝑋) = 0 ) |
| 29 | 28 | breq2d 5155 |
. . . 4
⊢ (𝜑 → (𝑌 ≤ (0 · 𝑋) ↔ 𝑌 ≤ 0 )) |
| 30 | 24, 29 | mtbird 325 |
. . 3
⊢ (𝜑 → ¬ 𝑌 ≤ (0 · 𝑋)) |
| 31 | 25, 19 | jca 511 |
. . . 4
⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) |
| 32 | | omndmnd 33081 |
. . . . . 6
⊢ (𝑊 ∈ oMnd → 𝑊 ∈ Mnd) |
| 33 | 8, 10, 32 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ Mnd) |
| 34 | | archirng.2 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ Archi) |
| 35 | 15, 16, 26, 20, 21 | isarchi2 33192 |
. . . . . 6
⊢ ((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) → (𝑊 ∈ Archi ↔
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑚 ∈ ℕ 𝑦 ≤ (𝑚 · 𝑥)))) |
| 36 | 35 | biimpa 476 |
. . . . 5
⊢ (((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑊 ∈ Archi) →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑚 ∈ ℕ 𝑦 ≤ (𝑚 · 𝑥))) |
| 37 | 12, 33, 34, 36 | syl21anc 838 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑚 ∈ ℕ 𝑦 ≤ (𝑚 · 𝑥))) |
| 38 | | archirng.5 |
. . . 4
⊢ (𝜑 → 0 < 𝑋) |
| 39 | | breq2 5147 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ( 0 < 𝑥 ↔ 0 < 𝑋)) |
| 40 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑚 · 𝑥) = (𝑚 · 𝑋)) |
| 41 | 40 | breq2d 5155 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑦 ≤ (𝑚 · 𝑥) ↔ 𝑦 ≤ (𝑚 · 𝑋))) |
| 42 | 41 | rexbidv 3179 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (∃𝑚 ∈ ℕ 𝑦 ≤ (𝑚 · 𝑥) ↔ ∃𝑚 ∈ ℕ 𝑦 ≤ (𝑚 · 𝑋))) |
| 43 | 39, 42 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝑋 → (( 0 < 𝑥 → ∃𝑚 ∈ ℕ 𝑦 ≤ (𝑚 · 𝑥)) ↔ ( 0 < 𝑋 → ∃𝑚 ∈ ℕ 𝑦 ≤ (𝑚 · 𝑋)))) |
| 44 | | breq1 5146 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → (𝑦 ≤ (𝑚 · 𝑋) ↔ 𝑌 ≤ (𝑚 · 𝑋))) |
| 45 | 44 | rexbidv 3179 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (∃𝑚 ∈ ℕ 𝑦 ≤ (𝑚 · 𝑋) ↔ ∃𝑚 ∈ ℕ 𝑌 ≤ (𝑚 · 𝑋))) |
| 46 | 45 | imbi2d 340 |
. . . . 5
⊢ (𝑦 = 𝑌 → (( 0 < 𝑋 → ∃𝑚 ∈ ℕ 𝑦 ≤ (𝑚 · 𝑋)) ↔ ( 0 < 𝑋 → ∃𝑚 ∈ ℕ 𝑌 ≤ (𝑚 · 𝑋)))) |
| 47 | 43, 46 | rspc2v 3633 |
. . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑚 ∈ ℕ 𝑦 ≤ (𝑚 · 𝑥)) → ( 0 < 𝑋 → ∃𝑚 ∈ ℕ 𝑌 ≤ (𝑚 · 𝑋)))) |
| 48 | 31, 37, 38, 47 | syl3c 66 |
. . 3
⊢ (𝜑 → ∃𝑚 ∈ ℕ 𝑌 ≤ (𝑚 · 𝑋)) |
| 49 | 2, 4, 6, 30, 48 | nn0min 32822 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ ℕ0 (¬ 𝑌 ≤ (𝑛 · 𝑋) ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |
| 50 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑊 ∈ Toset) |
| 51 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑊 ∈ Grp) |
| 52 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
| 53 | 52 | nn0zd 12639 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℤ) |
| 54 | 25 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
| 55 | 15, 26 | mulgcl 19109 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑛 · 𝑋) ∈ 𝐵) |
| 56 | 51, 53, 54, 55 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑛 · 𝑋) ∈ 𝐵) |
| 57 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑌 ∈ 𝐵) |
| 58 | 15, 20, 21 | tltnle 18467 |
. . . . 5
⊢ ((𝑊 ∈ Toset ∧ (𝑛 · 𝑋) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑛 · 𝑋) < 𝑌 ↔ ¬ 𝑌 ≤ (𝑛 · 𝑋))) |
| 59 | 50, 56, 57, 58 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 · 𝑋) < 𝑌 ↔ ¬ 𝑌 ≤ (𝑛 · 𝑋))) |
| 60 | 59 | anbi1d 631 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) ↔ (¬ 𝑌 ≤ (𝑛 · 𝑋) ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))) |
| 61 | 60 | rexbidva 3177 |
. 2
⊢ (𝜑 → (∃𝑛 ∈ ℕ0 ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)) ↔ ∃𝑛 ∈ ℕ0 (¬ 𝑌 ≤ (𝑛 · 𝑋) ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋)))) |
| 62 | 49, 61 | mpbird 257 |
1
⊢ (𝜑 → ∃𝑛 ∈ ℕ0 ((𝑛 · 𝑋) < 𝑌 ∧ 𝑌 ≤ ((𝑛 + 1) · 𝑋))) |