Metamath Proof Explorer

Theorem modmulnn

Description: Move a positive integer in and out of a floor in the first argument of a modulo operation. (Contributed by NM, 2-Jan-2009)

Ref Expression
Assertion modmulnn 
|- ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( ( N x. ( |_ ` A ) ) mod ( N x. M ) ) <_ ( ( |_ ` ( N x. A ) ) mod ( N x. M ) ) )

Proof

Step Hyp Ref Expression
1 nnre 
 |-  ( N e. NN -> N e. RR )
2 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
3 remulcl 
 |-  ( ( N e. RR /\ ( |_ ` A ) e. RR ) -> ( N x. ( |_ ` A ) ) e. RR )
4 1 2 3 syl2an 
 |-  ( ( N e. NN /\ A e. RR ) -> ( N x. ( |_ ` A ) ) e. RR )
5 4 3adant3 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( N x. ( |_ ` A ) ) e. RR )
6 remulcl 
 |-  ( ( N e. RR /\ A e. RR ) -> ( N x. A ) e. RR )
7 1 6 sylan 
 |-  ( ( N e. NN /\ A e. RR ) -> ( N x. A ) e. RR )
8 reflcl 
 |-  ( ( N x. A ) e. RR -> ( |_ ` ( N x. A ) ) e. RR )
9 7 8 syl 
 |-  ( ( N e. NN /\ A e. RR ) -> ( |_ ` ( N x. A ) ) e. RR )
10 9 3adant3 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( |_ ` ( N x. A ) ) e. RR )
11 nnmulcl 
 |-  ( ( N e. NN /\ M e. NN ) -> ( N x. M ) e. NN )
12 11 nnred 
 |-  ( ( N e. NN /\ M e. NN ) -> ( N x. M ) e. RR )
13 12 3adant2 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( N x. M ) e. RR )
14 nncn 
 |-  ( N e. NN -> N e. CC )
15 nnne0 
 |-  ( N e. NN -> N =/= 0 )
16 14 15 jca 
 |-  ( N e. NN -> ( N e. CC /\ N =/= 0 ) )
17 nncn 
 |-  ( M e. NN -> M e. CC )
18 nnne0 
 |-  ( M e. NN -> M =/= 0 )
19 17 18 jca 
 |-  ( M e. NN -> ( M e. CC /\ M =/= 0 ) )
20 mulne0 
 |-  ( ( ( N e. CC /\ N =/= 0 ) /\ ( M e. CC /\ M =/= 0 ) ) -> ( N x. M ) =/= 0 )
21 16 19 20 syl2an 
 |-  ( ( N e. NN /\ M e. NN ) -> ( N x. M ) =/= 0 )
22 21 3adant2 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( N x. M ) =/= 0 )
23 5 13 22 redivcld 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) e. RR )
24 reflcl 
 |-  ( ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) e. RR -> ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) e. RR )
25 23 24 syl 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) e. RR )
26 13 25 remulcld 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( ( N x. M ) x. ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) ) e. RR )
27 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
28 flmulnn0 
 |-  ( ( N e. NN0 /\ A e. RR ) -> ( N x. ( |_ ` A ) ) <_ ( |_ ` ( N x. A ) ) )
29 27 28 sylan 
 |-  ( ( N e. NN /\ A e. RR ) -> ( N x. ( |_ ` A ) ) <_ ( |_ ` ( N x. A ) ) )
30 29 3adant3 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( N x. ( |_ ` A ) ) <_ ( |_ ` ( N x. A ) ) )
31 5 10 26 30 lesub1dd 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( ( N x. ( |_ ` A ) ) - ( ( N x. M ) x. ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) ) ) <_ ( ( |_ ` ( N x. A ) ) - ( ( N x. M ) x. ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) ) ) )
32 11 nnrpd 
 |-  ( ( N e. NN /\ M e. NN ) -> ( N x. M ) e. RR+ )
33 modval 
 |-  ( ( ( N x. ( |_ ` A ) ) e. RR /\ ( N x. M ) e. RR+ ) -> ( ( N x. ( |_ ` A ) ) mod ( N x. M ) ) = ( ( N x. ( |_ ` A ) ) - ( ( N x. M ) x. ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) ) ) )
34 5 32 33 3imp3i2an 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( ( N x. ( |_ ` A ) ) mod ( N x. M ) ) = ( ( N x. ( |_ ` A ) ) - ( ( N x. M ) x. ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) ) ) )
35 modval 
 |-  ( ( ( |_ ` ( N x. A ) ) e. RR /\ ( N x. M ) e. RR+ ) -> ( ( |_ ` ( N x. A ) ) mod ( N x. M ) ) = ( ( |_ ` ( N x. A ) ) - ( ( N x. M ) x. ( |_ ` ( ( |_ ` ( N x. A ) ) / ( N x. M ) ) ) ) ) )
36 10 32 35 3imp3i2an 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( ( |_ ` ( N x. A ) ) mod ( N x. M ) ) = ( ( |_ ` ( N x. A ) ) - ( ( N x. M ) x. ( |_ ` ( ( |_ ` ( N x. A ) ) / ( N x. M ) ) ) ) ) )
37 7 3adant3 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( N x. A ) e. RR )
38 fldiv 
 |-  ( ( ( N x. A ) e. RR /\ ( N x. M ) e. NN ) -> ( |_ ` ( ( |_ ` ( N x. A ) ) / ( N x. M ) ) ) = ( |_ ` ( ( N x. A ) / ( N x. M ) ) ) )
39 37 11 38 3imp3i2an 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( |_ ` ( ( |_ ` ( N x. A ) ) / ( N x. M ) ) ) = ( |_ ` ( ( N x. A ) / ( N x. M ) ) ) )
40 fldiv 
 |-  ( ( A e. RR /\ M e. NN ) -> ( |_ ` ( ( |_ ` A ) / M ) ) = ( |_ ` ( A / M ) ) )
41 40 3adant3 
 |-  ( ( A e. RR /\ M e. NN /\ N e. NN ) -> ( |_ ` ( ( |_ ` A ) / M ) ) = ( |_ ` ( A / M ) ) )
42 2 recnd 
 |-  ( A e. RR -> ( |_ ` A ) e. CC )
43 divcan5 
 |-  ( ( ( |_ ` A ) e. CC /\ ( M e. CC /\ M =/= 0 ) /\ ( N e. CC /\ N =/= 0 ) ) -> ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) = ( ( |_ ` A ) / M ) )
44 42 19 16 43 syl3an 
 |-  ( ( A e. RR /\ M e. NN /\ N e. NN ) -> ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) = ( ( |_ ` A ) / M ) )
45 44 fveq2d 
 |-  ( ( A e. RR /\ M e. NN /\ N e. NN ) -> ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) = ( |_ ` ( ( |_ ` A ) / M ) ) )
46 recn 
 |-  ( A e. RR -> A e. CC )
47 divcan5 
 |-  ( ( A e. CC /\ ( M e. CC /\ M =/= 0 ) /\ ( N e. CC /\ N =/= 0 ) ) -> ( ( N x. A ) / ( N x. M ) ) = ( A / M ) )
48 46 19 16 47 syl3an 
 |-  ( ( A e. RR /\ M e. NN /\ N e. NN ) -> ( ( N x. A ) / ( N x. M ) ) = ( A / M ) )
49 48 fveq2d 
 |-  ( ( A e. RR /\ M e. NN /\ N e. NN ) -> ( |_ ` ( ( N x. A ) / ( N x. M ) ) ) = ( |_ ` ( A / M ) ) )
50 41 45 49 3eqtr4rd 
 |-  ( ( A e. RR /\ M e. NN /\ N e. NN ) -> ( |_ ` ( ( N x. A ) / ( N x. M ) ) ) = ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) )
51 50 3comr 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( |_ ` ( ( N x. A ) / ( N x. M ) ) ) = ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) )
52 39 51 eqtrd 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( |_ ` ( ( |_ ` ( N x. A ) ) / ( N x. M ) ) ) = ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) )
53 52 oveq2d 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( ( N x. M ) x. ( |_ ` ( ( |_ ` ( N x. A ) ) / ( N x. M ) ) ) ) = ( ( N x. M ) x. ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) ) )
54 53 oveq2d 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( ( |_ ` ( N x. A ) ) - ( ( N x. M ) x. ( |_ ` ( ( |_ ` ( N x. A ) ) / ( N x. M ) ) ) ) ) = ( ( |_ ` ( N x. A ) ) - ( ( N x. M ) x. ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) ) ) )
55 36 54 eqtrd 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( ( |_ ` ( N x. A ) ) mod ( N x. M ) ) = ( ( |_ ` ( N x. A ) ) - ( ( N x. M ) x. ( |_ ` ( ( N x. ( |_ ` A ) ) / ( N x. M ) ) ) ) ) )
56 31 34 55 3brtr4d 
 |-  ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( ( N x. ( |_ ` A ) ) mod ( N x. M ) ) <_ ( ( |_ ` ( N x. A ) ) mod ( N x. M ) ) )