This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

|- ( 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 )