MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsumdvdscom Structured version   Visualization version   GIF version

Theorem fsumdvdscom 25110
Description: A double commutation of divisor sums based on fsumdvdsdiag 25109. Note that 𝐴 depends on both 𝑗 and 𝑘. (Contributed by Mario Carneiro, 13-May-2016.)
Hypotheses
Ref Expression
fsumdvdscom.1 (𝜑𝑁 ∈ ℕ)
fsumdvdscom.2 (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵)
fsumdvdscom.3 ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑗})) → 𝐴 ∈ ℂ)
Assertion
Ref Expression
fsumdvdscom (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
Distinct variable groups:   𝐴,𝑚   𝐵,𝑗   𝑗,𝑘,𝑚,𝑥,𝑁   𝜑,𝑗,𝑘,𝑚
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥,𝑗,𝑘)   𝐵(𝑥,𝑘,𝑚)

Proof of Theorem fsumdvdscom
Dummy variables 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfcv 2902 . . 3 𝑢Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑗}𝐴
2 nfcv 2902 . . . 4 𝑗{𝑥 ∈ ℕ ∣ 𝑥𝑢}
3 nfcsb1v 3690 . . . 4 𝑗𝑢 / 𝑗𝐴
42, 3nfsum 14620 . . 3 𝑗Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴
5 breq2 4808 . . . . 5 (𝑗 = 𝑢 → (𝑥𝑗𝑥𝑢))
65rabbidv 3329 . . . 4 (𝑗 = 𝑢 → {𝑥 ∈ ℕ ∣ 𝑥𝑗} = {𝑥 ∈ ℕ ∣ 𝑥𝑢})
7 csbeq1a 3683 . . . . 5 (𝑗 = 𝑢𝐴 = 𝑢 / 𝑗𝐴)
87adantr 472 . . . 4 ((𝑗 = 𝑢𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑗}) → 𝐴 = 𝑢 / 𝑗𝐴)
96, 8sumeq12dv 14636 . . 3 (𝑗 = 𝑢 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴)
101, 4, 9cbvsumi 14626 . 2 Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑗}𝐴 = Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴
11 breq2 4808 . . . . . 6 (𝑢 = (𝑁 / 𝑣) → (𝑥𝑢𝑥 ∥ (𝑁 / 𝑣)))
1211rabbidv 3329 . . . . 5 (𝑢 = (𝑁 / 𝑣) → {𝑥 ∈ ℕ ∣ 𝑥𝑢} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})
13 csbeq1 3677 . . . . . 6 (𝑢 = (𝑁 / 𝑣) → 𝑢 / 𝑗𝐴 = (𝑁 / 𝑣) / 𝑗𝐴)
1413adantr 472 . . . . 5 ((𝑢 = (𝑁 / 𝑣) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}) → 𝑢 / 𝑗𝐴 = (𝑁 / 𝑣) / 𝑗𝐴)
1512, 14sumeq12dv 14636 . . . 4 (𝑢 = (𝑁 / 𝑣) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}(𝑁 / 𝑣) / 𝑗𝐴)
16 fzfid 12966 . . . . 5 (𝜑 → (1...𝑁) ∈ Fin)
17 fsumdvdscom.1 . . . . . 6 (𝜑𝑁 ∈ ℕ)
18 dvdsssfz1 15242 . . . . . 6 (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥𝑁} ⊆ (1...𝑁))
1917, 18syl 17 . . . . 5 (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥𝑁} ⊆ (1...𝑁))
20 ssfi 8345 . . . . 5 (((1...𝑁) ∈ Fin ∧ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ⊆ (1...𝑁)) → {𝑥 ∈ ℕ ∣ 𝑥𝑁} ∈ Fin)
2116, 19, 20syl2anc 696 . . . 4 (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥𝑁} ∈ Fin)
22 eqid 2760 . . . . . 6 {𝑥 ∈ ℕ ∣ 𝑥𝑁} = {𝑥 ∈ ℕ ∣ 𝑥𝑁}
23 eqid 2760 . . . . . 6 (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ↦ (𝑁 / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ↦ (𝑁 / 𝑧))
2422, 23dvdsflip 15241 . . . . 5 (𝑁 ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥𝑁})
2517, 24syl 17 . . . 4 (𝜑 → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥𝑁})
26 oveq2 6821 . . . . . 6 (𝑧 = 𝑣 → (𝑁 / 𝑧) = (𝑁 / 𝑣))
27 ovex 6841 . . . . . 6 (𝑁 / 𝑧) ∈ V
2826, 23, 27fvmpt3i 6449 . . . . 5 (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ↦ (𝑁 / 𝑧))‘𝑣) = (𝑁 / 𝑣))
2928adantl 473 . . . 4 ((𝜑𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ↦ (𝑁 / 𝑧))‘𝑣) = (𝑁 / 𝑣))
30 fzfid 12966 . . . . . 6 ((𝜑𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → (1...𝑢) ∈ Fin)
31 ssrab2 3828 . . . . . . . 8 {𝑥 ∈ ℕ ∣ 𝑥𝑁} ⊆ ℕ
32 simpr 479 . . . . . . . 8 ((𝜑𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁})
3331, 32sseldi 3742 . . . . . . 7 ((𝜑𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → 𝑢 ∈ ℕ)
34 dvdsssfz1 15242 . . . . . . 7 (𝑢 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥𝑢} ⊆ (1...𝑢))
3533, 34syl 17 . . . . . 6 ((𝜑𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥𝑢} ⊆ (1...𝑢))
36 ssfi 8345 . . . . . 6 (((1...𝑢) ∈ Fin ∧ {𝑥 ∈ ℕ ∣ 𝑥𝑢} ⊆ (1...𝑢)) → {𝑥 ∈ ℕ ∣ 𝑥𝑢} ∈ Fin)
3730, 35, 36syl2anc 696 . . . . 5 ((𝜑𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥𝑢} ∈ Fin)
38 fsumdvdscom.3 . . . . . . . . 9 ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑗})) → 𝐴 ∈ ℂ)
3938ralrimivva 3109 . . . . . . . 8 (𝜑 → ∀𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑗}𝐴 ∈ ℂ)
40 nfv 1992 . . . . . . . . 9 𝑢𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑗}𝐴 ∈ ℂ
413nfel1 2917 . . . . . . . . . 10 𝑗𝑢 / 𝑗𝐴 ∈ ℂ
422, 41nfral 3083 . . . . . . . . 9 𝑗𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴 ∈ ℂ
437eleq1d 2824 . . . . . . . . . 10 (𝑗 = 𝑢 → (𝐴 ∈ ℂ ↔ 𝑢 / 𝑗𝐴 ∈ ℂ))
446, 43raleqbidv 3291 . . . . . . . . 9 (𝑗 = 𝑢 → (∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑗}𝐴 ∈ ℂ ↔ ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴 ∈ ℂ))
4540, 42, 44cbvral 3306 . . . . . . . 8 (∀𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑗}𝐴 ∈ ℂ ↔ ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴 ∈ ℂ)
4639, 45sylib 208 . . . . . . 7 (𝜑 → ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴 ∈ ℂ)
4746r19.21bi 3070 . . . . . 6 ((𝜑𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴 ∈ ℂ)
4847r19.21bi 3070 . . . . 5 (((𝜑𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}) → 𝑢 / 𝑗𝐴 ∈ ℂ)
4937, 48fsumcl 14663 . . . 4 ((𝜑𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴 ∈ ℂ)
5015, 21, 25, 29, 49fsumf1o 14653 . . 3 (𝜑 → Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴 = Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}(𝑁 / 𝑣) / 𝑗𝐴)
5113eleq1d 2824 . . . . . . . 8 (𝑢 = (𝑁 / 𝑣) → (𝑢 / 𝑗𝐴 ∈ ℂ ↔ (𝑁 / 𝑣) / 𝑗𝐴 ∈ ℂ))
5212, 51raleqbidv 3291 . . . . . . 7 (𝑢 = (𝑁 / 𝑣) → (∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴 ∈ ℂ ↔ ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}(𝑁 / 𝑣) / 𝑗𝐴 ∈ ℂ))
5346adantr 472 . . . . . . 7 ((𝜑𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴 ∈ ℂ)
54 dvdsdivcl 15240 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → (𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁})
5517, 54sylan 489 . . . . . . 7 ((𝜑𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → (𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁})
5652, 53, 55rspcdva 3455 . . . . . 6 ((𝜑𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}(𝑁 / 𝑣) / 𝑗𝐴 ∈ ℂ)
5756r19.21bi 3070 . . . . 5 (((𝜑𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) → (𝑁 / 𝑣) / 𝑗𝐴 ∈ ℂ)
5857anasss 682 . . . 4 ((𝜑 ∧ (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})) → (𝑁 / 𝑣) / 𝑗𝐴 ∈ ℂ)
5917, 58fsumdvdsdiag 25109 . . 3 (𝜑 → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}(𝑁 / 𝑣) / 𝑗𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}(𝑁 / 𝑣) / 𝑗𝐴)
60 oveq2 6821 . . . . . . 7 (𝑣 = ((𝑁 / 𝑘) / 𝑚) → (𝑁 / 𝑣) = (𝑁 / ((𝑁 / 𝑘) / 𝑚)))
6160csbeq1d 3681 . . . . . 6 (𝑣 = ((𝑁 / 𝑘) / 𝑚) → (𝑁 / 𝑣) / 𝑗𝐴 = (𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗𝐴)
62 fzfid 12966 . . . . . . 7 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → (1...(𝑁 / 𝑘)) ∈ Fin)
63 dvdsdivcl 15240 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → (𝑁 / 𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁})
6431, 63sseldi 3742 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → (𝑁 / 𝑘) ∈ ℕ)
6517, 64sylan 489 . . . . . . . 8 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → (𝑁 / 𝑘) ∈ ℕ)
66 dvdsssfz1 15242 . . . . . . . 8 ((𝑁 / 𝑘) ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘)))
6765, 66syl 17 . . . . . . 7 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘)))
68 ssfi 8345 . . . . . . 7 (((1...(𝑁 / 𝑘)) ∈ Fin ∧ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘))) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ∈ Fin)
6962, 67, 68syl2anc 696 . . . . . 6 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ∈ Fin)
70 eqid 2760 . . . . . . . 8 {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}
71 eqid 2760 . . . . . . . 8 (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))
7270, 71dvdsflip 15241 . . . . . . 7 ((𝑁 / 𝑘) ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)})
7365, 72syl 17 . . . . . 6 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)})
74 oveq2 6821 . . . . . . . 8 (𝑧 = 𝑚 → ((𝑁 / 𝑘) / 𝑧) = ((𝑁 / 𝑘) / 𝑚))
75 ovex 6841 . . . . . . . 8 ((𝑁 / 𝑘) / 𝑧) ∈ V
7674, 71, 75fvmpt3i 6449 . . . . . . 7 (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))‘𝑚) = ((𝑁 / 𝑘) / 𝑚))
7776adantl 473 . . . . . 6 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))‘𝑚) = ((𝑁 / 𝑘) / 𝑚))
7817fsumdvdsdiaglem 25108 . . . . . . . 8 (𝜑 → ((𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})))
7958ex 449 . . . . . . . 8 (𝜑 → ((𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) → (𝑁 / 𝑣) / 𝑗𝐴 ∈ ℂ))
8078, 79syld 47 . . . . . . 7 (𝜑 → ((𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / 𝑣) / 𝑗𝐴 ∈ ℂ))
8180impl 651 . . . . . 6 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / 𝑣) / 𝑗𝐴 ∈ ℂ)
8261, 69, 73, 77, 81fsumf1o 14653 . . . . 5 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}(𝑁 / 𝑣) / 𝑗𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗𝐴)
83 ovexd 6843 . . . . . . 7 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) ∈ V)
84 nncn 11220 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
85 nnne0 11245 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
8684, 85jca 555 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
8717, 86syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
8887ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
8988simpld 477 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑁 ∈ ℂ)
90 elrabi 3499 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} → 𝑘 ∈ ℕ)
9190adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → 𝑘 ∈ ℕ)
9291adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑘 ∈ ℕ)
93 nncn 11220 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
94 nnne0 11245 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
9593, 94jca 555 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0))
9692, 95syl 17 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0))
97 elrabi 3499 . . . . . . . . . . . . . . 15 (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} → 𝑚 ∈ ℕ)
9897adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑚 ∈ ℕ)
99 nncn 11220 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
100 nnne0 11245 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ≠ 0)
10199, 100jca 555 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
10298, 101syl 17 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
103 divdiv1 10928 . . . . . . . . . . . . 13 ((𝑁 ∈ ℂ ∧ (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑁 / 𝑘) / 𝑚) = (𝑁 / (𝑘 · 𝑚)))
10489, 96, 102, 103syl3anc 1477 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑁 / 𝑘) / 𝑚) = (𝑁 / (𝑘 · 𝑚)))
105104oveq2d 6829 . . . . . . . . . . 11 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) = (𝑁 / (𝑁 / (𝑘 · 𝑚))))
106 nnmulcl 11235 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑘 · 𝑚) ∈ ℕ)
10791, 97, 106syl2an 495 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑘 · 𝑚) ∈ ℕ)
108 nncn 11220 . . . . . . . . . . . . . 14 ((𝑘 · 𝑚) ∈ ℕ → (𝑘 · 𝑚) ∈ ℂ)
109 nnne0 11245 . . . . . . . . . . . . . 14 ((𝑘 · 𝑚) ∈ ℕ → (𝑘 · 𝑚) ≠ 0)
110108, 109jca 555 . . . . . . . . . . . . 13 ((𝑘 · 𝑚) ∈ ℕ → ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0))
111107, 110syl 17 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0))
112 ddcan 10931 . . . . . . . . . . . 12 (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0)) → (𝑁 / (𝑁 / (𝑘 · 𝑚))) = (𝑘 · 𝑚))
11388, 111, 112syl2anc 696 . . . . . . . . . . 11 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / (𝑁 / (𝑘 · 𝑚))) = (𝑘 · 𝑚))
114105, 113eqtrd 2794 . . . . . . . . . 10 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) = (𝑘 · 𝑚))
115114eqeq2d 2770 . . . . . . . . 9 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚)) ↔ 𝑗 = (𝑘 · 𝑚)))
116115biimpa 502 . . . . . . . 8 ((((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) ∧ 𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) → 𝑗 = (𝑘 · 𝑚))
117 fsumdvdscom.2 . . . . . . . 8 (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵)
118116, 117syl 17 . . . . . . 7 ((((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) ∧ 𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) → 𝐴 = 𝐵)
11983, 118csbied 3701 . . . . . 6 (((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗𝐴 = 𝐵)
120119sumeq2dv 14632 . . . . 5 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
12182, 120eqtrd 2794 . . . 4 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁}) → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}(𝑁 / 𝑣) / 𝑗𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
122121sumeq2dv 14632 . . 3 (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}(𝑁 / 𝑣) / 𝑗𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
12350, 59, 1223eqtrd 2798 . 2 (𝜑 → Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑢}𝑢 / 𝑗𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
12410, 123syl5eq 2806 1 (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2139  wne 2932  wral 3050  {crab 3054  Vcvv 3340  csb 3674  wss 3715   class class class wbr 4804  cmpt 4881  1-1-ontowf1o 6048  cfv 6049  (class class class)co 6813  Fincfn 8121  cc 10126  0cc0 10128  1c1 10129   · cmul 10133   / cdiv 10876  cn 11212  ...cfz 12519  Σcsu 14615  cdvds 15182
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-oi 8580  df-card 8955  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-n0 11485  df-z 11570  df-uz 11880  df-rp 12026  df-fz 12520  df-fzo 12660  df-seq 12996  df-exp 13055  df-hash 13312  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-clim 14418  df-sum 14616  df-dvds 15183
This theorem is referenced by:  logsqvma  25430
  Copyright terms: Public domain W3C validator