Theorem fsumdvdsdiag

Description: A "diagonal commutation" of divisor sums analogous to fsum0diag . (Contributed by Mario Carneiro, 2-Jul-2015) (Revised by Mario Carneiro, 8-Apr-2016)

	Ref	Expression
Hypotheses	fsumdvdsdiag.1	|- ( ph -> N e. NN )
	fsumdvdsdiag.2	|- ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> A e. CC )
Assertion	fsumdvdsdiag	|- ( ph -> sum_ j e. { x e. NN | x || N } sum_ k e. { x e. NN | x || ( N / j ) } A = sum_ k e. { x e. NN | x || N } sum_ j e. { x e. NN | x || ( N / k ) } A )

Proof

Step	Hyp	Ref	Expression
1		fsumdvdsdiag.1	|- ( ph -> N e. NN )
2		fsumdvdsdiag.2	|- ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> A e. CC )
3		fzfid	|- ( ph -> ( 1 ... N ) e. Fin )
4		dvdsssfz1	|- ( N e. NN -> { x e. NN | x || N } C_ ( 1 ... N ) )
5	1 4	syl	|- ( ph -> { x e. NN | x || N } C_ ( 1 ... N ) )
6	3 5	ssfid	|- ( ph -> { x e. NN | x || N } e. Fin )
7		fzfid	|- ( ( ph /\ j e. { x e. NN | x || N } ) -> ( 1 ... ( N / j ) ) e. Fin )
8		ssrab2	|- { x e. NN | x || N } C_ NN
9		dvdsdivcl	|- ( ( N e. NN /\ j e. { x e. NN | x || N } ) -> ( N / j ) e. { x e. NN | x || N } )
10	1 9	sylan	|- ( ( ph /\ j e. { x e. NN | x || N } ) -> ( N / j ) e. { x e. NN | x || N } )
11	8 10	sselid	|- ( ( ph /\ j e. { x e. NN | x || N } ) -> ( N / j ) e. NN )
12		dvdsssfz1	|- ( ( N / j ) e. NN -> { x e. NN | x || ( N / j ) } C_ ( 1 ... ( N / j ) ) )
13	11 12	syl	|- ( ( ph /\ j e. { x e. NN | x || N } ) -> { x e. NN | x || ( N / j ) } C_ ( 1 ... ( N / j ) ) )
14	7 13	ssfid	|- ( ( ph /\ j e. { x e. NN | x || N } ) -> { x e. NN | x || ( N / j ) } e. Fin )
15	1	fsumdvdsdiaglem	|- ( ph -> ( ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) -> ( k e. { x e. NN | x || N } /\ j e. { x e. NN | x || ( N / k ) } ) ) )
16	1	fsumdvdsdiaglem	|- ( ph -> ( ( k e. { x e. NN | x || N } /\ j e. { x e. NN | x || ( N / k ) } ) -> ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) )
17	15 16	impbid	|- ( ph -> ( ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) <-> ( k e. { x e. NN | x || N } /\ j e. { x e. NN | x || ( N / k ) } ) ) )
18	6 6 14 17 2	fsumcom2	|- ( ph -> sum_ j e. { x e. NN | x || N } sum_ k e. { x e. NN | x || ( N / j ) } A = sum_ k e. { x e. NN | x || N } sum_ j e. { x e. NN | x || ( N / k ) } A )