Proof of Theorem fsumdvdsdiaglem
| Step | Hyp | Ref
| Expression |
| 1 | | breq1 5146 |
. . . 4
⊢ (𝑥 = 𝑘 → (𝑥 ∥ 𝑁 ↔ 𝑘 ∥ 𝑁)) |
| 2 | | elrabi 3687 |
. . . . 5
⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)} → 𝑘 ∈ ℕ) |
| 3 | 2 | ad2antll 729 |
. . . 4
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑘 ∈ ℕ) |
| 4 | 3 | nnzd 12640 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑘 ∈ ℤ) |
| 5 | | fsumdvdsdiag.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 6 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑁 ∈ ℕ) |
| 7 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
| 8 | | dvdsdivcl 16353 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑗) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
| 9 | 6, 7, 8 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → (𝑁 / 𝑗) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
| 10 | | elrabi 3687 |
. . . . . . 7
⊢ ((𝑁 / 𝑗) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → (𝑁 / 𝑗) ∈ ℕ) |
| 11 | 9, 10 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → (𝑁 / 𝑗) ∈ ℕ) |
| 12 | 11 | nnzd 12640 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → (𝑁 / 𝑗) ∈ ℤ) |
| 13 | 6 | nnzd 12640 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑁 ∈ ℤ) |
| 14 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (𝑥 ∥ (𝑁 / 𝑗) ↔ 𝑘 ∥ (𝑁 / 𝑗))) |
| 15 | 14 | elrab 3692 |
. . . . . . 7
⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)} ↔ (𝑘 ∈ ℕ ∧ 𝑘 ∥ (𝑁 / 𝑗))) |
| 16 | 15 | simprbi 496 |
. . . . . 6
⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)} → 𝑘 ∥ (𝑁 / 𝑗)) |
| 17 | 16 | ad2antll 729 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑘 ∥ (𝑁 / 𝑗)) |
| 18 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑥 = (𝑁 / 𝑗) → (𝑥 ∥ 𝑁 ↔ (𝑁 / 𝑗) ∥ 𝑁)) |
| 19 | 18 | elrab 3692 |
. . . . . . 7
⊢ ((𝑁 / 𝑗) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↔ ((𝑁 / 𝑗) ∈ ℕ ∧ (𝑁 / 𝑗) ∥ 𝑁)) |
| 20 | 19 | simprbi 496 |
. . . . . 6
⊢ ((𝑁 / 𝑗) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → (𝑁 / 𝑗) ∥ 𝑁) |
| 21 | 9, 20 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → (𝑁 / 𝑗) ∥ 𝑁) |
| 22 | 4, 12, 13, 17, 21 | dvdstrd 16332 |
. . . 4
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑘 ∥ 𝑁) |
| 23 | 1, 3, 22 | elrabd 3694 |
. . 3
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
| 24 | | breq1 5146 |
. . . 4
⊢ (𝑥 = 𝑗 → (𝑥 ∥ (𝑁 / 𝑘) ↔ 𝑗 ∥ (𝑁 / 𝑘))) |
| 25 | | elrabi 3687 |
. . . . 5
⊢ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → 𝑗 ∈ ℕ) |
| 26 | 25 | ad2antrl 728 |
. . . 4
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑗 ∈ ℕ) |
| 27 | 26 | nnzd 12640 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑗 ∈ ℤ) |
| 28 | 26 | nnne0d 12316 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑗 ≠ 0) |
| 29 | | dvdsmulcr 16323 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ (𝑁 / 𝑗) ∈ ℤ ∧ (𝑗 ∈ ℤ ∧ 𝑗 ≠ 0)) → ((𝑘 · 𝑗) ∥ ((𝑁 / 𝑗) · 𝑗) ↔ 𝑘 ∥ (𝑁 / 𝑗))) |
| 30 | 4, 12, 27, 28, 29 | syl112anc 1376 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → ((𝑘 · 𝑗) ∥ ((𝑁 / 𝑗) · 𝑗) ↔ 𝑘 ∥ (𝑁 / 𝑗))) |
| 31 | 17, 30 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → (𝑘 · 𝑗) ∥ ((𝑁 / 𝑗) · 𝑗)) |
| 32 | 6 | nncnd 12282 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑁 ∈ ℂ) |
| 33 | 26 | nncnd 12282 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑗 ∈ ℂ) |
| 34 | 32, 33, 28 | divcan1d 12044 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → ((𝑁 / 𝑗) · 𝑗) = 𝑁) |
| 35 | 3 | nncnd 12282 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑘 ∈ ℂ) |
| 36 | 3 | nnne0d 12316 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑘 ≠ 0) |
| 37 | 32, 35, 36 | divcan2d 12045 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → (𝑘 · (𝑁 / 𝑘)) = 𝑁) |
| 38 | 34, 37 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → ((𝑁 / 𝑗) · 𝑗) = (𝑘 · (𝑁 / 𝑘))) |
| 39 | 31, 38 | breqtrd 5169 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → (𝑘 · 𝑗) ∥ (𝑘 · (𝑁 / 𝑘))) |
| 40 | | ssrab2 4080 |
. . . . . . . 8
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ ℕ |
| 41 | | dvdsdivcl 16353 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
| 42 | 6, 23, 41 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → (𝑁 / 𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
| 43 | 40, 42 | sselid 3981 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → (𝑁 / 𝑘) ∈ ℕ) |
| 44 | 43 | nnzd 12640 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → (𝑁 / 𝑘) ∈ ℤ) |
| 45 | | dvdscmulr 16322 |
. . . . . 6
⊢ ((𝑗 ∈ ℤ ∧ (𝑁 / 𝑘) ∈ ℤ ∧ (𝑘 ∈ ℤ ∧ 𝑘 ≠ 0)) → ((𝑘 · 𝑗) ∥ (𝑘 · (𝑁 / 𝑘)) ↔ 𝑗 ∥ (𝑁 / 𝑘))) |
| 46 | 27, 44, 4, 36, 45 | syl112anc 1376 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → ((𝑘 · 𝑗) ∥ (𝑘 · (𝑁 / 𝑘)) ↔ 𝑗 ∥ (𝑁 / 𝑘))) |
| 47 | 39, 46 | mpbid 232 |
. . . 4
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑗 ∥ (𝑁 / 𝑘)) |
| 48 | 24, 26, 47 | elrabd 3694 |
. . 3
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) |
| 49 | 23, 48 | jca 511 |
. 2
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)})) → (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)})) |
| 50 | 49 | ex 412 |
1
⊢ (𝜑 → ((𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑗)}) → (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}))) |