Proof of Theorem lcmf
| Step | Hyp | Ref
| Expression |
| 1 | | dvdslcmf 16668 |
. . . . . 6
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin) →
∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍)) |
| 2 | 1 | 3adant3 1133 |
. . . . 5
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍) → ∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍)) |
| 3 | | lcmfledvds 16669 |
. . . . . . 7
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍) → ((𝑘 ∈ ℕ ∧
∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘) → (lcm‘𝑍) ≤ 𝑘)) |
| 4 | 3 | expdimp 452 |
. . . . . 6
⊢ (((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍) ∧ 𝑘 ∈ ℕ) → (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → (lcm‘𝑍) ≤ 𝑘)) |
| 5 | 4 | ralrimiva 3146 |
. . . . 5
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍) → ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → (lcm‘𝑍) ≤ 𝑘)) |
| 6 | 2, 5 | jca 511 |
. . . 4
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍) → (∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍) ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → (lcm‘𝑍) ≤ 𝑘))) |
| 7 | 6 | adantl 481 |
. . 3
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → (∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍) ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → (lcm‘𝑍) ≤ 𝑘))) |
| 8 | | breq2 5147 |
. . . . 5
⊢ (𝐾 = (lcm‘𝑍) → (𝑚 ∥ 𝐾 ↔ 𝑚 ∥ (lcm‘𝑍))) |
| 9 | 8 | ralbidv 3178 |
. . . 4
⊢ (𝐾 = (lcm‘𝑍) → (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ↔ ∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍))) |
| 10 | | breq1 5146 |
. . . . . 6
⊢ (𝐾 = (lcm‘𝑍) → (𝐾 ≤ 𝑘 ↔ (lcm‘𝑍) ≤ 𝑘)) |
| 11 | 10 | imbi2d 340 |
. . . . 5
⊢ (𝐾 = (lcm‘𝑍) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘) ↔ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → (lcm‘𝑍) ≤ 𝑘))) |
| 12 | 11 | ralbidv 3178 |
. . . 4
⊢ (𝐾 = (lcm‘𝑍) → (∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘) ↔ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → (lcm‘𝑍) ≤ 𝑘))) |
| 13 | 9, 12 | anbi12d 632 |
. . 3
⊢ (𝐾 = (lcm‘𝑍) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)) ↔ (∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍) ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → (lcm‘𝑍) ≤ 𝑘)))) |
| 14 | 7, 13 | syl5ibrcom 247 |
. 2
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → (𝐾 = (lcm‘𝑍) → (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)))) |
| 15 | | lcmfn0cl 16663 |
. . . . . 6
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍) →
(lcm‘𝑍) ∈
ℕ) |
| 16 | 15 | adantl 481 |
. . . . 5
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) →
(lcm‘𝑍) ∈
ℕ) |
| 17 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑘 = (lcm‘𝑍) → (𝑚 ∥ 𝑘 ↔ 𝑚 ∥ (lcm‘𝑍))) |
| 18 | 17 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑘 = (lcm‘𝑍) → (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 ↔ ∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍))) |
| 19 | | breq2 5147 |
. . . . . . 7
⊢ (𝑘 = (lcm‘𝑍) → (𝐾 ≤ 𝑘 ↔ 𝐾 ≤ (lcm‘𝑍))) |
| 20 | 18, 19 | imbi12d 344 |
. . . . . 6
⊢ (𝑘 = (lcm‘𝑍) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘) ↔ (∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍) → 𝐾 ≤ (lcm‘𝑍)))) |
| 21 | 20 | rspcv 3618 |
. . . . 5
⊢
((lcm‘𝑍) ∈ ℕ → (∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘) → (∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍) → 𝐾 ≤ (lcm‘𝑍)))) |
| 22 | 16, 21 | syl 17 |
. . . 4
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → (∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘) → (∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍) → 𝐾 ≤ (lcm‘𝑍)))) |
| 23 | 22 | adantld 490 |
. . 3
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)) → (∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍) → 𝐾 ≤ (lcm‘𝑍)))) |
| 24 | 2 | adantl 481 |
. . . . 5
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → ∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍)) |
| 25 | | nnre 12273 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℝ) |
| 26 | 15 | nnred 12281 |
. . . . . . 7
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍) →
(lcm‘𝑍) ∈
ℝ) |
| 27 | | leloe 11347 |
. . . . . . 7
⊢ ((𝐾 ∈ ℝ ∧
(lcm‘𝑍) ∈
ℝ) → (𝐾 ≤
(lcm‘𝑍) ↔
(𝐾 <
(lcm‘𝑍) ∨
𝐾 = (lcm‘𝑍)))) |
| 28 | 25, 26, 27 | syl2an 596 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → (𝐾 ≤ (lcm‘𝑍) ↔ (𝐾 < (lcm‘𝑍) ∨ 𝐾 = (lcm‘𝑍)))) |
| 29 | | lcmfledvds 16669 |
. . . . . . . . . . . . 13
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍) → ((𝐾 ∈ ℕ ∧
∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾) → (lcm‘𝑍) ≤ 𝐾)) |
| 30 | 29 | expd 415 |
. . . . . . . . . . . 12
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍) → (𝐾 ∈ ℕ →
(∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 → (lcm‘𝑍) ≤ 𝐾))) |
| 31 | 30 | impcom 407 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 → (lcm‘𝑍) ≤ 𝐾)) |
| 32 | | lenlt 11339 |
. . . . . . . . . . . . 13
⊢
(((lcm‘𝑍) ∈ ℝ ∧ 𝐾 ∈ ℝ) →
((lcm‘𝑍) ≤
𝐾 ↔ ¬ 𝐾 < (lcm‘𝑍))) |
| 33 | 26, 25, 32 | syl2anr 597 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) →
((lcm‘𝑍) ≤
𝐾 ↔ ¬ 𝐾 < (lcm‘𝑍))) |
| 34 | | pm2.21 123 |
. . . . . . . . . . . 12
⊢ (¬
𝐾 <
(lcm‘𝑍) →
(𝐾 <
(lcm‘𝑍) →
𝐾 = (lcm‘𝑍))) |
| 35 | 33, 34 | biimtrdi 253 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) →
((lcm‘𝑍) ≤
𝐾 → (𝐾 < (lcm‘𝑍) → 𝐾 = (lcm‘𝑍)))) |
| 36 | 31, 35 | syldc 48 |
. . . . . . . . . 10
⊢
(∀𝑚 ∈
𝑍 𝑚 ∥ 𝐾 → ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍)) → (𝐾 < (lcm‘𝑍) → 𝐾 = (lcm‘𝑍)))) |
| 37 | 36 | adantr 480 |
. . . . . . . . 9
⊢
((∀𝑚 ∈
𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)) → ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍)) → (𝐾 < (lcm‘𝑍) → 𝐾 = (lcm‘𝑍)))) |
| 38 | 37 | com13 88 |
. . . . . . . 8
⊢ (𝐾 < (lcm‘𝑍) → ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍)) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)) → 𝐾 = (lcm‘𝑍)))) |
| 39 | | 2a1 28 |
. . . . . . . 8
⊢ (𝐾 = (lcm‘𝑍) → ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍)) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)) → 𝐾 = (lcm‘𝑍)))) |
| 40 | 38, 39 | jaoi 858 |
. . . . . . 7
⊢ ((𝐾 < (lcm‘𝑍) ∨ 𝐾 = (lcm‘𝑍)) → ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍)) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)) → 𝐾 = (lcm‘𝑍)))) |
| 41 | 40 | com12 32 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → ((𝐾 < (lcm‘𝑍) ∨ 𝐾 = (lcm‘𝑍)) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)) → 𝐾 = (lcm‘𝑍)))) |
| 42 | 28, 41 | sylbid 240 |
. . . . 5
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → (𝐾 ≤ (lcm‘𝑍) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)) → 𝐾 = (lcm‘𝑍)))) |
| 43 | 24, 42 | embantd 59 |
. . . 4
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍) → 𝐾 ≤ (lcm‘𝑍)) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)) → 𝐾 = (lcm‘𝑍)))) |
| 44 | 43 | com23 86 |
. . 3
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ (lcm‘𝑍) → 𝐾 ≤ (lcm‘𝑍)) → 𝐾 = (lcm‘𝑍)))) |
| 45 | 23, 44 | mpdd 43 |
. 2
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → ((∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)) → 𝐾 = (lcm‘𝑍))) |
| 46 | 14, 45 | impbid 212 |
1
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉
𝑍)) → (𝐾 = (lcm‘𝑍) ↔ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘)))) |