Metamath Proof Explorer

Theorem fsumdvdscom

Description: A double commutation of divisor sums based on fsumdvdsdiag . Note that A depends on both j and k . (Contributed by Mario Carneiro, 13-May-2016)

Ref Expression
Hypotheses fsumdvdscom.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
fsumdvdscom.2 ⊢ ( 𝑗 = ( 𝑘 · 𝑚 ) → 𝐴 = 𝐵 )
fsumdvdscom.3 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } ) ) → 𝐴 ∈ ℂ )
Assertion fsumdvdscom ( 𝜑 → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐵 )

Proof

Step Hyp Ref Expression
1 fsumdvdscom.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 fsumdvdscom.2 ⊢ ( 𝑗 = ( 𝑘 · 𝑚 ) → 𝐴 = 𝐵 )
3 fsumdvdscom.3 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } ) ) → 𝐴 ∈ ℂ )
4 nfcv ⊢ Ⅎ 𝑢 Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴
5 nfcv ⊢ Ⅎ 𝑗 { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 }
6 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑢 / 𝑗 ⦌ 𝐴
7 5 6 nfsum ⊢ Ⅎ 𝑗 Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴
8 breq2 ⊢ ( 𝑗 = 𝑢 → ( 𝑥 ∥ 𝑗 ↔ 𝑥 ∥ 𝑢 ) )
9 8 rabbidv ⊢ ( 𝑗 = 𝑢 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } )
10 csbeq1a ⊢ ( 𝑗 = 𝑢 → 𝐴 = ⦋ 𝑢 / 𝑗 ⦌ 𝐴 )
11 10 adantr ⊢ ( ( 𝑗 = 𝑢 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } ) → 𝐴 = ⦋ 𝑢 / 𝑗 ⦌ 𝐴 )
12 9 11 sumeq12dv ⊢ ( 𝑗 = 𝑢 → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 )
13 4 7 12 cbvsumi ⊢ Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 = Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴
14 breq2 ⊢ ( 𝑢 = ( 𝑁 / 𝑣 ) → ( 𝑥 ∥ 𝑢 ↔ 𝑥 ∥ ( 𝑁 / 𝑣 ) ) )
15 14 rabbidv ⊢ ( 𝑢 = ( 𝑁 / 𝑣 ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } )
16 csbeq1 ⊢ ( 𝑢 = ( 𝑁 / 𝑣 ) → ⦋ 𝑢 / 𝑗 ⦌ 𝐴 = ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 )
17 16 adantr ⊢ ( ( 𝑢 = ( 𝑁 / 𝑣 ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ) → ⦋ 𝑢 / 𝑗 ⦌ 𝐴 = ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 )
18 15 17 sumeq12dv ⊢ ( 𝑢 = ( 𝑁 / 𝑣 ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 )
19 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
20 dvdsssfz1 ⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
21 1 20 syl ⊢ ( 𝜑 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
22 19 21 ssfid ⊢ ( 𝜑 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∈ Fin )
23 eqid ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
24 eqid ⊢ ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) = ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) )
25 23 24 dvdsflip ⊢ ( 𝑁 ∈ ℕ → ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) : { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
26 1 25 syl ⊢ ( 𝜑 → ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) : { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
27 oveq2 ⊢ ( 𝑧 = 𝑣 → ( 𝑁 / 𝑧 ) = ( 𝑁 / 𝑣 ) )
28 ovex ⊢ ( 𝑁 / 𝑧 ) ∈ V
29 27 24 28 fvmpt3i ⊢ ( 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } → ( ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) ‘ 𝑣 ) = ( 𝑁 / 𝑣 ) )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) ‘ 𝑣 ) = ( 𝑁 / 𝑣 ) )
31 fzfid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 1 ... 𝑢 ) ∈ Fin )
32 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ℕ
33 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
34 32 33 sselid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ∈ ℕ )
35 dvdsssfz1 ⊢ ( 𝑢 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⊆ ( 1 ... 𝑢 ) )
36 34 35 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⊆ ( 1 ... 𝑢 ) )
37 31 36 ssfid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ∈ Fin )
38 3 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 ∈ ℂ )
39 nfv ⊢ Ⅎ 𝑢 ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 ∈ ℂ
40 6 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ
41 5 40 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ
42 10 eleq1d ⊢ ( 𝑗 = 𝑢 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
43 9 42 raleqbidv ⊢ ( 𝑗 = 𝑢 → ( ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 ∈ ℂ ↔ ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
44 39 41 43 cbvralw ⊢ ( ∀ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 ∈ ℂ ↔ ∀ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ )
45 38 44 sylib ⊢ ( 𝜑 → ∀ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ )
46 45 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ )
47 46 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ) → ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ )
48 37 47 fsumcl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ )
49 18 22 26 30 48 fsumf1o ⊢ ( 𝜑 → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 = Σ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 )
50 16 eleq1d ⊢ ( 𝑢 = ( 𝑁 / 𝑣 ) → ( ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ ↔ ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
51 15 50 raleqbidv ⊢ ( 𝑢 = ( 𝑁 / 𝑣 ) → ( ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ ↔ ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
52 45 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ∀ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ )
53 dvdsdivcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑣 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
54 1 53 sylan ⊢ ( ( 𝜑 ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑣 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
55 51 52 54 rspcdva ⊢ ( ( 𝜑 ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ )
56 55 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ) → ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ )
57 56 anasss ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ) ) → ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ )
58 1 57 fsumdvdsdiag ⊢ ( 𝜑 → Σ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 )
59 oveq2 ⊢ ( 𝑣 = ( ( 𝑁 / 𝑘 ) / 𝑚 ) → ( 𝑁 / 𝑣 ) = ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) )
60 59 csbeq1d ⊢ ( 𝑣 = ( ( 𝑁 / 𝑘 ) / 𝑚 ) → ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 = ⦋ ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) / 𝑗 ⦌ 𝐴 )
61 fzfid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 1 ... ( 𝑁 / 𝑘 ) ) ∈ Fin )
62 dvdsdivcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
63 32 62 sselid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑘 ) ∈ ℕ )
64 1 63 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑘 ) ∈ ℕ )
65 dvdsssfz1 ⊢ ( ( 𝑁 / 𝑘 ) ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⊆ ( 1 ... ( 𝑁 / 𝑘 ) ) )
66 64 65 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⊆ ( 1 ... ( 𝑁 / 𝑘 ) ) )
67 61 66 ssfid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ∈ Fin )
68 eqid ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) }
69 eqid ⊢ ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ↦ ( ( 𝑁 / 𝑘 ) / 𝑧 ) ) = ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ↦ ( ( 𝑁 / 𝑘 ) / 𝑧 ) )
70 68 69 dvdsflip ⊢ ( ( 𝑁 / 𝑘 ) ∈ ℕ → ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ↦ ( ( 𝑁 / 𝑘 ) / 𝑧 ) ) : { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } )
71 64 70 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ↦ ( ( 𝑁 / 𝑘 ) / 𝑧 ) ) : { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } )
72 oveq2 ⊢ ( 𝑧 = 𝑚 → ( ( 𝑁 / 𝑘 ) / 𝑧 ) = ( ( 𝑁 / 𝑘 ) / 𝑚 ) )
73 ovex ⊢ ( ( 𝑁 / 𝑘 ) / 𝑧 ) ∈ V
74 72 69 73 fvmpt3i ⊢ ( 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } → ( ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ↦ ( ( 𝑁 / 𝑘 ) / 𝑧 ) ) ‘ 𝑚 ) = ( ( 𝑁 / 𝑘 ) / 𝑚 ) )
75 74 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ↦ ( ( 𝑁 / 𝑘 ) / 𝑧 ) ) ‘ 𝑚 ) = ( ( 𝑁 / 𝑘 ) / 𝑚 ) )
76 1 fsumdvdsdiaglem ⊢ ( 𝜑 → ( ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ) ) )
77 57 ex ⊢ ( 𝜑 → ( ( 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ) → ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
78 76 77 syld ⊢ ( 𝜑 → ( ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
79 78 impl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ )
80 60 67 71 75 79 fsumf1o ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 = Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⦋ ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) / 𝑗 ⦌ 𝐴 )
81 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) ∈ V )
82 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
83 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
84 82 83 jca ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
85 1 84 syl ⊢ ( 𝜑 → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
86 85 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
87 86 simpld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → 𝑁 ∈ ℂ )
88 elrabi ⊢ ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } → 𝑘 ∈ ℕ )
89 88 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑘 ∈ ℕ )
90 89 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → 𝑘 ∈ ℕ )
91 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
92 nnne0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
93 91 92 jca ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) )
94 90 93 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) )
95 elrabi ⊢ ( 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } → 𝑚 ∈ ℕ )
96 95 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → 𝑚 ∈ ℕ )
97 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
98 nnne0 ⊢ ( 𝑚 ∈ ℕ → 𝑚 ≠ 0 )
99 97 98 jca ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) )
100 96 99 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) )
101 divdiv1 ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) → ( ( 𝑁 / 𝑘 ) / 𝑚 ) = ( 𝑁 / ( 𝑘 · 𝑚 ) ) )
102 87 94 100 101 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( ( 𝑁 / 𝑘 ) / 𝑚 ) = ( 𝑁 / ( 𝑘 · 𝑚 ) ) )
103 102 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) = ( 𝑁 / ( 𝑁 / ( 𝑘 · 𝑚 ) ) ) )
104 nnmulcl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( 𝑘 · 𝑚 ) ∈ ℕ )
105 89 95 104 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑘 · 𝑚 ) ∈ ℕ )
106 nncn ⊢ ( ( 𝑘 · 𝑚 ) ∈ ℕ → ( 𝑘 · 𝑚 ) ∈ ℂ )
107 nnne0 ⊢ ( ( 𝑘 · 𝑚 ) ∈ ℕ → ( 𝑘 · 𝑚 ) ≠ 0 )
108 106 107 jca ⊢ ( ( 𝑘 · 𝑚 ) ∈ ℕ → ( ( 𝑘 · 𝑚 ) ∈ ℂ ∧ ( 𝑘 · 𝑚 ) ≠ 0 ) )
109 105 108 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( ( 𝑘 · 𝑚 ) ∈ ℂ ∧ ( 𝑘 · 𝑚 ) ≠ 0 ) )
110 ddcan ⊢ ( ( ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ∧ ( ( 𝑘 · 𝑚 ) ∈ ℂ ∧ ( 𝑘 · 𝑚 ) ≠ 0 ) ) → ( 𝑁 / ( 𝑁 / ( 𝑘 · 𝑚 ) ) ) = ( 𝑘 · 𝑚 ) )
111 86 109 110 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑁 / ( 𝑁 / ( 𝑘 · 𝑚 ) ) ) = ( 𝑘 · 𝑚 ) )
112 103 111 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) = ( 𝑘 · 𝑚 ) )
113 112 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑗 = ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) ↔ 𝑗 = ( 𝑘 · 𝑚 ) ) )
114 113 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) ∧ 𝑗 = ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) ) → 𝑗 = ( 𝑘 · 𝑚 ) )
115 114 2 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) ∧ 𝑗 = ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) ) → 𝐴 = 𝐵 )
116 81 115 csbied ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ⦋ ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) / 𝑗 ⦌ 𝐴 = 𝐵 )
117 116 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⦋ ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) / 𝑗 ⦌ 𝐴 = Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐵 )
118 80 117 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 = Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐵 )
119 118 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐵 )
120 49 58 119 3eqtrd ⊢ ( 𝜑 → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐵 )
121 13 120 syl5eq ⊢ ( 𝜑 → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐵 )