Metamath Proof Explorer

Theorem fsumdvdsdiaglem

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
Hypothesis fsumdvdsdiag.1 
|- ( ph -> N e. NN )
Assertion 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 ) } ) ) )

Proof

Step Hyp Ref Expression
1 fsumdvdsdiag.1 
 |-  ( ph -> N e. NN )
2 breq1 
 |-  ( x = k -> ( x || N <-> k || N ) )
3 elrabi 
 |-  ( k e. { x e. NN | x || ( N / j ) } -> k e. NN )
4 3 ad2antll 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> k e. NN )
5 4 nnzd 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> k e. ZZ )
6 1 adantr 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> N e. NN )
7 simprl 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> j e. { x e. NN | x || N } )
8 dvdsdivcl 
 |-  ( ( N e. NN /\ j e. { x e. NN | x || N } ) -> ( N / j ) e. { x e. NN | x || N } )
9 6 7 8 syl2anc 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( N / j ) e. { x e. NN | x || N } )
10 elrabi 
 |-  ( ( N / j ) e. { x e. NN | x || N } -> ( N / j ) e. NN )
11 9 10 syl 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( N / j ) e. NN )
12 11 nnzd 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( N / j ) e. ZZ )
13 6 nnzd 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> N e. ZZ )
14 breq1 
 |-  ( x = k -> ( x || ( N / j ) <-> k || ( N / j ) ) )
15 14 elrab 
 |-  ( k e. { x e. NN | x || ( N / j ) } <-> ( k e. NN /\ k || ( N / j ) ) )
16 15 simprbi 
 |-  ( k e. { x e. NN | x || ( N / j ) } -> k || ( N / j ) )
17 16 ad2antll 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> k || ( N / j ) )
18 breq1 
 |-  ( x = ( N / j ) -> ( x || N <-> ( N / j ) || N ) )
19 18 elrab 
 |-  ( ( N / j ) e. { x e. NN | x || N } <-> ( ( N / j ) e. NN /\ ( N / j ) || N ) )
20 19 simprbi 
 |-  ( ( N / j ) e. { x e. NN | x || N } -> ( N / j ) || N )
21 9 20 syl 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( N / j ) || N )
22 5 12 13 17 21 dvdstrd 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> k || N )
23 2 4 22 elrabd 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> k e. { x e. NN | x || N } )
24 breq1 
 |-  ( x = j -> ( x || ( N / k ) <-> j || ( N / k ) ) )
25 elrabi 
 |-  ( j e. { x e. NN | x || N } -> j e. NN )
26 25 ad2antrl 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> j e. NN )
27 26 nnzd 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> j e. ZZ )
28 26 nnne0d 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> j =/= 0 )
29 dvdsmulcr 
 |-  ( ( k e. ZZ /\ ( N / j ) e. ZZ /\ ( j e. ZZ /\ j =/= 0 ) ) -> ( ( k x. j ) || ( ( N / j ) x. j ) <-> k || ( N / j ) ) )
30 5 12 27 28 29 syl112anc 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( ( k x. j ) || ( ( N / j ) x. j ) <-> k || ( N / j ) ) )
31 17 30 mpbird 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( k x. j ) || ( ( N / j ) x. j ) )
32 6 nncnd 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> N e. CC )
33 26 nncnd 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> j e. CC )
34 32 33 28 divcan1d 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( ( N / j ) x. j ) = N )
35 4 nncnd 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> k e. CC )
36 4 nnne0d 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> k =/= 0 )
37 32 35 36 divcan2d 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( k x. ( N / k ) ) = N )
38 34 37 eqtr4d 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( ( N / j ) x. j ) = ( k x. ( N / k ) ) )
39 31 38 breqtrd 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( k x. j ) || ( k x. ( N / k ) ) )
40 ssrab2 
 |-  { x e. NN | x || N } C_ NN
41 dvdsdivcl 
 |-  ( ( N e. NN /\ k e. { x e. NN | x || N } ) -> ( N / k ) e. { x e. NN | x || N } )
42 6 23 41 syl2anc 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( N / k ) e. { x e. NN | x || N } )
43 40 42 sseldi 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( N / k ) e. NN )
44 43 nnzd 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( N / k ) e. ZZ )
45 dvdscmulr 
 |-  ( ( j e. ZZ /\ ( N / k ) e. ZZ /\ ( k e. ZZ /\ k =/= 0 ) ) -> ( ( k x. j ) || ( k x. ( N / k ) ) <-> j || ( N / k ) ) )
46 27 44 5 36 45 syl112anc 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> ( ( k x. j ) || ( k x. ( N / k ) ) <-> j || ( N / k ) ) )
47 39 46 mpbid 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> j || ( N / k ) )
48 24 26 47 elrabd 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> j e. { x e. NN | x || ( N / k ) } )
49 23 48 jca 
 |-  ( ( 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 ) } ) )
50 49 ex 
 |-  ( 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 ) } ) ) )