Metamath Proof Explorer

Theorem muldvdsfacm1

Description: The product of two different positive integers less than a third integer divides the factorial of the third integer decreased by 1. By assumption, the third integer must be greater than 3. (Contributed by AV, 6-Apr-2026)

Ref Expression
Assertion muldvdsfacm1 
|- ( ( A e. ( 1 ..^ B ) /\ B e. ( 1 ..^ N ) ) -> ( A x. B ) || ( ! ` ( N - 1 ) ) )

Proof

Step Hyp Ref Expression
1 elfzoelz 
 |-  ( A e. ( 1 ..^ B ) -> A e. ZZ )
2 elfzoelz 
 |-  ( B e. ( 1 ..^ N ) -> B e. ZZ )
3 zmulcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A x. B ) e. ZZ )
4 1 2 3 syl2an 
 |-  ( ( A e. ( 1 ..^ B ) /\ B e. ( 1 ..^ N ) ) -> ( A x. B ) e. ZZ )
5 elfzo2 
 |-  ( B e. ( 1 ..^ N ) <-> ( B e. ( ZZ>= ` 1 ) /\ N e. ZZ /\ B < N ) )
6 elnnuz 
 |-  ( B e. NN <-> B e. ( ZZ>= ` 1 ) )
7 nnnn0 
 |-  ( B e. NN -> B e. NN0 )
8 6 7 sylbir 
 |-  ( B e. ( ZZ>= ` 1 ) -> B e. NN0 )
9 8 3ad2ant1 
 |-  ( ( B e. ( ZZ>= ` 1 ) /\ N e. ZZ /\ B < N ) -> B e. NN0 )
10 5 9 sylbi 
 |-  ( B e. ( 1 ..^ N ) -> B e. NN0 )
11 10 adantl 
 |-  ( ( A e. ( 1 ..^ B ) /\ B e. ( 1 ..^ N ) ) -> B e. NN0 )
12 11 faccld 
 |-  ( ( A e. ( 1 ..^ B ) /\ B e. ( 1 ..^ N ) ) -> ( ! ` B ) e. NN )
13 12 nnzd 
 |-  ( ( A e. ( 1 ..^ B ) /\ B e. ( 1 ..^ N ) ) -> ( ! ` B ) e. ZZ )
14 simp2 
 |-  ( ( B e. ( ZZ>= ` 1 ) /\ N e. ZZ /\ B < N ) -> N e. ZZ )
15 eluz2 
 |-  ( B e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ B e. ZZ /\ 1 <_ B ) )
16 1red 
 |-  ( ( B e. ZZ /\ N e. ZZ ) -> 1 e. RR )
17 zre 
 |-  ( B e. ZZ -> B e. RR )
18 17 adantr 
 |-  ( ( B e. ZZ /\ N e. ZZ ) -> B e. RR )
19 zre 
 |-  ( N e. ZZ -> N e. RR )
20 19 adantl 
 |-  ( ( B e. ZZ /\ N e. ZZ ) -> N e. RR )
21 lelttr 
 |-  ( ( 1 e. RR /\ B e. RR /\ N e. RR ) -> ( ( 1 <_ B /\ B < N ) -> 1 < N ) )
22 16 18 20 21 syl3anc 
 |-  ( ( B e. ZZ /\ N e. ZZ ) -> ( ( 1 <_ B /\ B < N ) -> 1 < N ) )
23 0lt1 
 |-  0 < 1
24 0red 
 |-  ( N e. ZZ -> 0 e. RR )
25 1red 
 |-  ( N e. ZZ -> 1 e. RR )
26 lttr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( 0 < 1 /\ 1 < N ) -> 0 < N ) )
27 24 25 19 26 syl3anc 
 |-  ( N e. ZZ -> ( ( 0 < 1 /\ 1 < N ) -> 0 < N ) )
28 23 27 mpani 
 |-  ( N e. ZZ -> ( 1 < N -> 0 < N ) )
29 28 adantl 
 |-  ( ( B e. ZZ /\ N e. ZZ ) -> ( 1 < N -> 0 < N ) )
30 22 29 syld 
 |-  ( ( B e. ZZ /\ N e. ZZ ) -> ( ( 1 <_ B /\ B < N ) -> 0 < N ) )
31 30 exp4b 
 |-  ( B e. ZZ -> ( N e. ZZ -> ( 1 <_ B -> ( B < N -> 0 < N ) ) ) )
32 31 com23 
 |-  ( B e. ZZ -> ( 1 <_ B -> ( N e. ZZ -> ( B < N -> 0 < N ) ) ) )
33 32 a1i 
 |-  ( 1 e. ZZ -> ( B e. ZZ -> ( 1 <_ B -> ( N e. ZZ -> ( B < N -> 0 < N ) ) ) ) )
34 33 3imp 
 |-  ( ( 1 e. ZZ /\ B e. ZZ /\ 1 <_ B ) -> ( N e. ZZ -> ( B < N -> 0 < N ) ) )
35 15 34 sylbi 
 |-  ( B e. ( ZZ>= ` 1 ) -> ( N e. ZZ -> ( B < N -> 0 < N ) ) )
36 35 3imp 
 |-  ( ( B e. ( ZZ>= ` 1 ) /\ N e. ZZ /\ B < N ) -> 0 < N )
37 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
38 14 36 37 sylanbrc 
 |-  ( ( B e. ( ZZ>= ` 1 ) /\ N e. ZZ /\ B < N ) -> N e. NN )
39 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
40 38 39 syl 
 |-  ( ( B e. ( ZZ>= ` 1 ) /\ N e. ZZ /\ B < N ) -> ( N - 1 ) e. NN0 )
41 5 40 sylbi 
 |-  ( B e. ( 1 ..^ N ) -> ( N - 1 ) e. NN0 )
42 41 adantl 
 |-  ( ( A e. ( 1 ..^ B ) /\ B e. ( 1 ..^ N ) ) -> ( N - 1 ) e. NN0 )
43 42 faccld 
 |-  ( ( A e. ( 1 ..^ B ) /\ B e. ( 1 ..^ N ) ) -> ( ! ` ( N - 1 ) ) e. NN )
44 43 nnzd 
 |-  ( ( A e. ( 1 ..^ B ) /\ B e. ( 1 ..^ N ) ) -> ( ! ` ( N - 1 ) ) e. ZZ )
45 muldvdsfacgt 
 |-  ( A e. ( 1 ..^ B ) -> ( A x. B ) || ( ! ` B ) )
46 45 adantr 
 |-  ( ( A e. ( 1 ..^ B ) /\ B e. ( 1 ..^ N ) ) -> ( A x. B ) || ( ! ` B ) )
47 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
48 fzoss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ..^ N ) C_ ( 0 ..^ N ) )
49 48 sseld 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( B e. ( 1 ..^ N ) -> B e. ( 0 ..^ N ) ) )
50 47 49 ax-mp 
 |-  ( B e. ( 1 ..^ N ) -> B e. ( 0 ..^ N ) )
51 elfzoel2 
 |-  ( B e. ( 1 ..^ N ) -> N e. ZZ )
52 fzoval 
 |-  ( N e. ZZ -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
53 52 eleq2d 
 |-  ( N e. ZZ -> ( B e. ( 0 ..^ N ) <-> B e. ( 0 ... ( N - 1 ) ) ) )
54 51 53 syl 
 |-  ( B e. ( 1 ..^ N ) -> ( B e. ( 0 ..^ N ) <-> B e. ( 0 ... ( N - 1 ) ) ) )
55 50 54 mpbid 
 |-  ( B e. ( 1 ..^ N ) -> B e. ( 0 ... ( N - 1 ) ) )
56 55 adantl 
 |-  ( ( A e. ( 1 ..^ B ) /\ B e. ( 1 ..^ N ) ) -> B e. ( 0 ... ( N - 1 ) ) )
57 facnn0dvdsfac 
 |-  ( B e. ( 0 ... ( N - 1 ) ) -> ( ! ` B ) || ( ! ` ( N - 1 ) ) )
58 56 57 syl 
 |-  ( ( A e. ( 1 ..^ B ) /\ B e. ( 1 ..^ N ) ) -> ( ! ` B ) || ( ! ` ( N - 1 ) ) )
59 4 13 44 46 58 dvdstrd 
 |-  ( ( A e. ( 1 ..^ B ) /\ B e. ( 1 ..^ N ) ) -> ( A x. B ) || ( ! ` ( N - 1 ) ) )