Step | Hyp | Ref
| Expression |
1 | | fzfid 13074 |
. . 3
⊢ (𝜑 → (1...(⌊‘𝐴)) ∈ Fin) |
2 | | fzfid 13074 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (1...𝑛) ∈ Fin) |
3 | | elfznn 12670 |
. . . . . 6
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
4 | 3 | adantl 475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ) |
5 | | dvdsssfz1 15424 |
. . . . 5
⊢ (𝑛 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ⊆ (1...𝑛)) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ⊆ (1...𝑛)) |
7 | | ssfi 8455 |
. . . 4
⊢
(((1...𝑛) ∈ Fin
∧ {𝑥 ∈ ℕ
∣ 𝑥 ∥ 𝑛} ⊆ (1...𝑛)) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ∈ Fin) |
8 | 2, 6, 7 | syl2anc 579 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ∈ Fin) |
9 | | nnre 11365 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ ℕ → 𝑑 ∈
ℝ) |
10 | 9 | ad2antrl 719 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝑑 ∈ ℝ) |
11 | 4 | adantr 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝑛 ∈ ℕ) |
12 | 11 | nnred 11374 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝑛 ∈ ℝ) |
13 | | dvdsflsumcom.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℝ) |
14 | 13 | ad2antrr 717 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝐴 ∈ ℝ) |
15 | | nnz 11734 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ ℕ → 𝑑 ∈
ℤ) |
16 | | dvdsle 15416 |
. . . . . . . . . . . . 13
⊢ ((𝑑 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑑 ∥ 𝑛 → 𝑑 ≤ 𝑛)) |
17 | 15, 4, 16 | syl2anr 590 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ 𝑑 ∈ ℕ) → (𝑑 ∥ 𝑛 → 𝑑 ≤ 𝑛)) |
18 | 17 | impr 448 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝑑 ≤ 𝑛) |
19 | | fznnfl 12963 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ → (𝑛 ∈
(1...(⌊‘𝐴))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝐴))) |
20 | 13, 19 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑛 ∈ (1...(⌊‘𝐴)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝐴))) |
21 | 20 | simplbda 495 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ≤ 𝐴) |
22 | 21 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝑛 ≤ 𝐴) |
23 | 10, 12, 14, 18, 22 | letrd 10520 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝑑 ≤ 𝐴) |
24 | 23 | ex 403 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛) → 𝑑 ≤ 𝐴)) |
25 | 24 | pm4.71rd 558 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛) ↔ (𝑑 ≤ 𝐴 ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)))) |
26 | | ancom 454 |
. . . . . . . . 9
⊢ ((𝑑 ≤ 𝐴 ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) ↔ ((𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛) ∧ 𝑑 ≤ 𝐴)) |
27 | | an32 636 |
. . . . . . . . 9
⊢ (((𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛) ∧ 𝑑 ≤ 𝐴) ↔ ((𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴) ∧ 𝑑 ∥ 𝑛)) |
28 | 26, 27 | bitri 267 |
. . . . . . . 8
⊢ ((𝑑 ≤ 𝐴 ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) ↔ ((𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴) ∧ 𝑑 ∥ 𝑛)) |
29 | 25, 28 | syl6bb 279 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛) ↔ ((𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴) ∧ 𝑑 ∥ 𝑛))) |
30 | | fznnfl 12963 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝑑 ∈
(1...(⌊‘𝐴))
↔ (𝑑 ∈ ℕ
∧ 𝑑 ≤ 𝐴))) |
31 | 13, 30 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑑 ∈ (1...(⌊‘𝐴)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴))) |
32 | 31 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑑 ∈ (1...(⌊‘𝐴)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴))) |
33 | 32 | anbi1d 623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛) ↔ ((𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴) ∧ 𝑑 ∥ 𝑛))) |
34 | 29, 33 | bitr4d 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛))) |
35 | 34 | pm5.32da 574 |
. . . . 5
⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛)))) |
36 | | an12 635 |
. . . . 5
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ (𝑑 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∥ 𝑛)) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛))) |
37 | 35, 36 | syl6bb 279 |
. . . 4
⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛)))) |
38 | | breq1 4878 |
. . . . . 6
⊢ (𝑥 = 𝑑 → (𝑥 ∥ 𝑛 ↔ 𝑑 ∥ 𝑛)) |
39 | 38 | elrab 3585 |
. . . . 5
⊢ (𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ↔ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) |
40 | 39 | anbi2i 616 |
. . . 4
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛))) |
41 | | breq2 4879 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (𝑑 ∥ 𝑥 ↔ 𝑑 ∥ 𝑛)) |
42 | 41 | elrab 3585 |
. . . . 5
⊢ (𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥} ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛)) |
43 | 42 | anbi2i 616 |
. . . 4
⊢ ((𝑑 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑑 ∥ 𝑥}) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛))) |
44 | 37, 40, 43 | 3bitr4g 306 |
. . 3
⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥}))) |
45 | | dvdsflsumcom.3 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → 𝐵 ∈ ℂ) |
46 | 1, 1, 8, 44, 45 | fsumcom2 14887 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥}𝐵) |
47 | | dvdsflsumcom.1 |
. . . 4
⊢ (𝑛 = (𝑑 · 𝑚) → 𝐵 = 𝐶) |
48 | | fzfid 13074 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘(𝐴 / 𝑑))) ∈ Fin) |
49 | 13 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝐴 ∈ ℝ) |
50 | 31 | simprbda 494 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ∈ ℕ) |
51 | | eqid 2825 |
. . . . 5
⊢ (𝑦 ∈
(1...(⌊‘(𝐴 /
𝑑))) ↦ (𝑑 · 𝑦)) = (𝑦 ∈ (1...(⌊‘(𝐴 / 𝑑))) ↦ (𝑑 · 𝑦)) |
52 | 49, 50, 51 | dvdsflf1o 25333 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (𝑦 ∈ (1...(⌊‘(𝐴 / 𝑑))) ↦ (𝑑 · 𝑦)):(1...(⌊‘(𝐴 / 𝑑)))–1-1-onto→{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥}) |
53 | | oveq2 6918 |
. . . . . 6
⊢ (𝑦 = 𝑚 → (𝑑 · 𝑦) = (𝑑 · 𝑚)) |
54 | | ovex 6942 |
. . . . . 6
⊢ (𝑑 · 𝑚) ∈ V |
55 | 53, 51, 54 | fvmpt 6533 |
. . . . 5
⊢ (𝑚 ∈
(1...(⌊‘(𝐴 /
𝑑))) → ((𝑦 ∈
(1...(⌊‘(𝐴 /
𝑑))) ↦ (𝑑 · 𝑦))‘𝑚) = (𝑑 · 𝑚)) |
56 | 55 | adantl 475 |
. . . 4
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑦 ∈ (1...(⌊‘(𝐴 / 𝑑))) ↦ (𝑑 · 𝑦))‘𝑚) = (𝑑 · 𝑚)) |
57 | 44 | biimpar 471 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥})) → (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) |
58 | 57, 45 | syldan 585 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥})) → 𝐵 ∈ ℂ) |
59 | 58 | anassrs 461 |
. . . 4
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥}) → 𝐵 ∈ ℂ) |
60 | 47, 48, 52, 56, 59 | fsumf1o 14838 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥}𝐵 = Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶) |
61 | 60 | sumeq2dv 14817 |
. 2
⊢ (𝜑 → Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶) |
62 | 46, 61 | eqtrd 2861 |
1
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶) |