Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . 3
⊢ (𝜑 → (1...(⌊‘𝐴)) ∈ Fin) |
2 | | fzfid 12772 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (1...𝑛) ∈ Fin) |
3 | | elfznn 12370 |
. . . . . 6
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
4 | 3 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ) |
5 | | dvdsssfz1 15040 |
. . . . 5
⊢ (𝑛 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ⊆ (1...𝑛)) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ⊆ (1...𝑛)) |
7 | | ssfi 8180 |
. . . 4
⊢
(((1...𝑛) ∈ Fin
∧ {𝑥 ∈ ℕ
∣ 𝑥 ∥ 𝑛} ⊆ (1...𝑛)) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ∈ Fin) |
8 | 2, 6, 7 | syl2anc 693 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ∈ Fin) |
9 | | nnre 11027 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ ℕ → 𝑑 ∈
ℝ) |
10 | 9 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝑑 ∈ ℝ) |
11 | 4 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝑛 ∈ ℕ) |
12 | 11 | nnred 11035 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝑛 ∈ ℝ) |
13 | | dvdsflsumcom.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℝ) |
14 | 13 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝐴 ∈ ℝ) |
15 | | nnz 11399 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ ℕ → 𝑑 ∈
ℤ) |
16 | | dvdsle 15032 |
. . . . . . . . . . . . 13
⊢ ((𝑑 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑑 ∥ 𝑛 → 𝑑 ≤ 𝑛)) |
17 | 15, 4, 16 | syl2anr 495 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ 𝑑 ∈ ℕ) → (𝑑 ∥ 𝑛 → 𝑑 ≤ 𝑛)) |
18 | 17 | impr 649 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝑑 ≤ 𝑛) |
19 | | fznnfl 12661 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ → (𝑛 ∈
(1...(⌊‘𝐴))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝐴))) |
20 | 13, 19 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑛 ∈ (1...(⌊‘𝐴)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝐴))) |
21 | 20 | simplbda 654 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ≤ 𝐴) |
22 | 21 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝑛 ≤ 𝐴) |
23 | 10, 12, 14, 18, 22 | letrd 10194 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) → 𝑑 ≤ 𝐴) |
24 | 23 | ex 450 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛) → 𝑑 ≤ 𝐴)) |
25 | 24 | pm4.71rd 667 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛) ↔ (𝑑 ≤ 𝐴 ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)))) |
26 | | ancom 466 |
. . . . . . . . 9
⊢ ((𝑑 ≤ 𝐴 ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) ↔ ((𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛) ∧ 𝑑 ≤ 𝐴)) |
27 | | an32 839 |
. . . . . . . . 9
⊢ (((𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛) ∧ 𝑑 ≤ 𝐴) ↔ ((𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴) ∧ 𝑑 ∥ 𝑛)) |
28 | 26, 27 | bitri 264 |
. . . . . . . 8
⊢ ((𝑑 ≤ 𝐴 ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) ↔ ((𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴) ∧ 𝑑 ∥ 𝑛)) |
29 | 25, 28 | syl6bb 276 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛) ↔ ((𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴) ∧ 𝑑 ∥ 𝑛))) |
30 | | fznnfl 12661 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝑑 ∈
(1...(⌊‘𝐴))
↔ (𝑑 ∈ ℕ
∧ 𝑑 ≤ 𝐴))) |
31 | 13, 30 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑑 ∈ (1...(⌊‘𝐴)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴))) |
32 | 31 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑑 ∈ (1...(⌊‘𝐴)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴))) |
33 | 32 | anbi1d 741 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛) ↔ ((𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴) ∧ 𝑑 ∥ 𝑛))) |
34 | 29, 33 | bitr4d 271 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛))) |
35 | 34 | pm5.32da 673 |
. . . . 5
⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛)))) |
36 | | an12 838 |
. . . . 5
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ (𝑑 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∥ 𝑛)) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛))) |
37 | 35, 36 | syl6bb 276 |
. . . 4
⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛)))) |
38 | | breq1 4656 |
. . . . . 6
⊢ (𝑥 = 𝑑 → (𝑥 ∥ 𝑛 ↔ 𝑑 ∥ 𝑛)) |
39 | 38 | elrab 3363 |
. . . . 5
⊢ (𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ↔ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛)) |
40 | 39 | anbi2i 730 |
. . . 4
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛))) |
41 | | breq2 4657 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (𝑑 ∥ 𝑥 ↔ 𝑑 ∥ 𝑛)) |
42 | 41 | elrab 3363 |
. . . . 5
⊢ (𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥} ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛)) |
43 | 42 | anbi2i 730 |
. . . 4
⊢ ((𝑑 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑑 ∥ 𝑥}) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∥ 𝑛))) |
44 | 37, 40, 43 | 3bitr4g 303 |
. . 3
⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥}))) |
45 | | dvdsflsumcom.3 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → 𝐵 ∈ ℂ) |
46 | 1, 1, 8, 44, 45 | fsumcom2 14505 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥}𝐵) |
47 | | dvdsflsumcom.1 |
. . . 4
⊢ (𝑛 = (𝑑 · 𝑚) → 𝐵 = 𝐶) |
48 | | fzfid 12772 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘(𝐴 / 𝑑))) ∈ Fin) |
49 | 13 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝐴 ∈ ℝ) |
50 | 31 | simprbda 653 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ∈ ℕ) |
51 | | eqid 2622 |
. . . . 5
⊢ (𝑦 ∈
(1...(⌊‘(𝐴 /
𝑑))) ↦ (𝑑 · 𝑦)) = (𝑦 ∈ (1...(⌊‘(𝐴 / 𝑑))) ↦ (𝑑 · 𝑦)) |
52 | 49, 50, 51 | dvdsflf1o 24913 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (𝑦 ∈ (1...(⌊‘(𝐴 / 𝑑))) ↦ (𝑑 · 𝑦)):(1...(⌊‘(𝐴 / 𝑑)))–1-1-onto→{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥}) |
53 | | oveq2 6658 |
. . . . . 6
⊢ (𝑦 = 𝑚 → (𝑑 · 𝑦) = (𝑑 · 𝑚)) |
54 | | ovex 6678 |
. . . . . 6
⊢ (𝑑 · 𝑚) ∈ V |
55 | 53, 51, 54 | fvmpt 6282 |
. . . . 5
⊢ (𝑚 ∈
(1...(⌊‘(𝐴 /
𝑑))) → ((𝑦 ∈
(1...(⌊‘(𝐴 /
𝑑))) ↦ (𝑑 · 𝑦))‘𝑚) = (𝑑 · 𝑚)) |
56 | 55 | adantl 482 |
. . . 4
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑦 ∈ (1...(⌊‘(𝐴 / 𝑑))) ↦ (𝑑 · 𝑦))‘𝑚) = (𝑑 · 𝑚)) |
57 | 44 | biimpar 502 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥})) → (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) |
58 | 57, 45 | syldan 487 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥})) → 𝐵 ∈ ℂ) |
59 | 58 | anassrs 680 |
. . . 4
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥}) → 𝐵 ∈ ℂ) |
60 | 47, 48, 52, 56, 59 | fsumf1o 14454 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥}𝐵 = Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶) |
61 | 60 | sumeq2dv 14433 |
. 2
⊢ (𝜑 → Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑑 ∥ 𝑥}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶) |
62 | 46, 61 | eqtrd 2656 |
1
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}𝐵 = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))𝐶) |