Metamath Proof Explorer

Theorem fzmul

Description: Membership of a product in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010)

Ref Expression
Assertion fzmul 
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. NN ) -> ( J e. ( M ... N ) -> ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) ) )

Proof

Step Hyp Ref Expression
1 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( J e. ( M ... N ) <-> ( J e. ZZ /\ M <_ J /\ J <_ N ) ) )
2 1 3adant3 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. NN ) -> ( J e. ( M ... N ) <-> ( J e. ZZ /\ M <_ J /\ J <_ N ) ) )
3 zre 
 |-  ( M e. ZZ -> M e. RR )
4 zre 
 |-  ( J e. ZZ -> J e. RR )
5 nnre 
 |-  ( K e. NN -> K e. RR )
6 nngt0 
 |-  ( K e. NN -> 0 < K )
7 5 6 jca 
 |-  ( K e. NN -> ( K e. RR /\ 0 < K ) )
8 lemul2 
 |-  ( ( M e. RR /\ J e. RR /\ ( K e. RR /\ 0 < K ) ) -> ( M <_ J <-> ( K x. M ) <_ ( K x. J ) ) )
9 3 4 7 8 syl3an 
 |-  ( ( M e. ZZ /\ J e. ZZ /\ K e. NN ) -> ( M <_ J <-> ( K x. M ) <_ ( K x. J ) ) )
10 9 3expa 
 |-  ( ( ( M e. ZZ /\ J e. ZZ ) /\ K e. NN ) -> ( M <_ J <-> ( K x. M ) <_ ( K x. J ) ) )
11 10 biimpd 
 |-  ( ( ( M e. ZZ /\ J e. ZZ ) /\ K e. NN ) -> ( M <_ J -> ( K x. M ) <_ ( K x. J ) ) )
12 11 adantllr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ J e. ZZ ) /\ K e. NN ) -> ( M <_ J -> ( K x. M ) <_ ( K x. J ) ) )
13 zre 
 |-  ( N e. ZZ -> N e. RR )
14 lemul2 
 |-  ( ( J e. RR /\ N e. RR /\ ( K e. RR /\ 0 < K ) ) -> ( J <_ N <-> ( K x. J ) <_ ( K x. N ) ) )
15 4 13 7 14 syl3an 
 |-  ( ( J e. ZZ /\ N e. ZZ /\ K e. NN ) -> ( J <_ N <-> ( K x. J ) <_ ( K x. N ) ) )
16 15 3expa 
 |-  ( ( ( J e. ZZ /\ N e. ZZ ) /\ K e. NN ) -> ( J <_ N <-> ( K x. J ) <_ ( K x. N ) ) )
17 16 ancom1s 
 |-  ( ( ( N e. ZZ /\ J e. ZZ ) /\ K e. NN ) -> ( J <_ N <-> ( K x. J ) <_ ( K x. N ) ) )
18 17 biimpd 
 |-  ( ( ( N e. ZZ /\ J e. ZZ ) /\ K e. NN ) -> ( J <_ N -> ( K x. J ) <_ ( K x. N ) ) )
19 18 adantlll 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ J e. ZZ ) /\ K e. NN ) -> ( J <_ N -> ( K x. J ) <_ ( K x. N ) ) )
20 12 19 anim12d 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ J e. ZZ ) /\ K e. NN ) -> ( ( M <_ J /\ J <_ N ) -> ( ( K x. M ) <_ ( K x. J ) /\ ( K x. J ) <_ ( K x. N ) ) ) )
21 zmulcl 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( K x. M ) e. ZZ )
22 21 ex 
 |-  ( K e. ZZ -> ( M e. ZZ -> ( K x. M ) e. ZZ ) )
23 zmulcl 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( K x. N ) e. ZZ )
24 23 ex 
 |-  ( K e. ZZ -> ( N e. ZZ -> ( K x. N ) e. ZZ ) )
25 zmulcl 
 |-  ( ( K e. ZZ /\ J e. ZZ ) -> ( K x. J ) e. ZZ )
26 25 ex 
 |-  ( K e. ZZ -> ( J e. ZZ -> ( K x. J ) e. ZZ ) )
27 22 24 26 3anim123d 
 |-  ( K e. ZZ -> ( ( M e. ZZ /\ N e. ZZ /\ J e. ZZ ) -> ( ( K x. M ) e. ZZ /\ ( K x. N ) e. ZZ /\ ( K x. J ) e. ZZ ) ) )
28 elfz 
 |-  ( ( ( K x. J ) e. ZZ /\ ( K x. M ) e. ZZ /\ ( K x. N ) e. ZZ ) -> ( ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) <-> ( ( K x. M ) <_ ( K x. J ) /\ ( K x. J ) <_ ( K x. N ) ) ) )
29 28 3coml 
 |-  ( ( ( K x. M ) e. ZZ /\ ( K x. N ) e. ZZ /\ ( K x. J ) e. ZZ ) -> ( ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) <-> ( ( K x. M ) <_ ( K x. J ) /\ ( K x. J ) <_ ( K x. N ) ) ) )
30 27 29 syl6 
 |-  ( K e. ZZ -> ( ( M e. ZZ /\ N e. ZZ /\ J e. ZZ ) -> ( ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) <-> ( ( K x. M ) <_ ( K x. J ) /\ ( K x. J ) <_ ( K x. N ) ) ) ) )
31 nnz 
 |-  ( K e. NN -> K e. ZZ )
32 30 31 syl11 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ J e. ZZ ) -> ( K e. NN -> ( ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) <-> ( ( K x. M ) <_ ( K x. J ) /\ ( K x. J ) <_ ( K x. N ) ) ) ) )
33 32 3expa 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ J e. ZZ ) -> ( K e. NN -> ( ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) <-> ( ( K x. M ) <_ ( K x. J ) /\ ( K x. J ) <_ ( K x. N ) ) ) ) )
34 33 imp 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ J e. ZZ ) /\ K e. NN ) -> ( ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) <-> ( ( K x. M ) <_ ( K x. J ) /\ ( K x. J ) <_ ( K x. N ) ) ) )
35 20 34 sylibrd 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ J e. ZZ ) /\ K e. NN ) -> ( ( M <_ J /\ J <_ N ) -> ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) ) )
36 35 an32s 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. NN ) /\ J e. ZZ ) -> ( ( M <_ J /\ J <_ N ) -> ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) ) )
37 36 exp4b 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. NN ) -> ( J e. ZZ -> ( M <_ J -> ( J <_ N -> ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) ) ) ) )
38 37 3impd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. NN ) -> ( ( J e. ZZ /\ M <_ J /\ J <_ N ) -> ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) ) )
39 38 3impa 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. NN ) -> ( ( J e. ZZ /\ M <_ J /\ J <_ N ) -> ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) ) )
40 2 39 sylbid 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. NN ) -> ( J e. ( M ... N ) -> ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) ) )