Metamath Proof Explorer

Theorem muldvdsfacgt

Description: The product of two different positive integers divides the factorial of the bigger integer. (Contributed by AV, 6-Apr-2026)

Ref Expression
Assertion muldvdsfacgt 
|- ( A e. ( 1 ..^ B ) -> ( A x. B ) || ( ! ` B ) )

Proof

Step Hyp Ref Expression
1 elfzoelz 
 |-  ( A e. ( 1 ..^ B ) -> A e. ZZ )
2 simp2 
 |-  ( ( A e. ( ZZ>= ` 1 ) /\ B e. ZZ /\ A < B ) -> B e. ZZ )
3 eluz2 
 |-  ( A e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ A e. ZZ /\ 1 <_ A ) )
4 1re 
 |-  1 e. RR
5 zre 
 |-  ( A e. ZZ -> A e. RR )
6 zre 
 |-  ( B e. ZZ -> B e. RR )
7 lelttr 
 |-  ( ( 1 e. RR /\ A e. RR /\ B e. RR ) -> ( ( 1 <_ A /\ A < B ) -> 1 < B ) )
8 4 5 6 7 mp3an3an 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 1 <_ A /\ A < B ) -> 1 < B ) )
9 0lt1 
 |-  0 < 1
10 0re 
 |-  0 e. RR
11 lttr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ B e. RR ) -> ( ( 0 < 1 /\ 1 < B ) -> 0 < B ) )
12 10 4 6 11 mp3an12i 
 |-  ( B e. ZZ -> ( ( 0 < 1 /\ 1 < B ) -> 0 < B ) )
13 9 12 mpani 
 |-  ( B e. ZZ -> ( 1 < B -> 0 < B ) )
14 13 adantl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( 1 < B -> 0 < B ) )
15 8 14 syld 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 1 <_ A /\ A < B ) -> 0 < B ) )
16 15 exp4b 
 |-  ( A e. ZZ -> ( B e. ZZ -> ( 1 <_ A -> ( A < B -> 0 < B ) ) ) )
17 16 com23 
 |-  ( A e. ZZ -> ( 1 <_ A -> ( B e. ZZ -> ( A < B -> 0 < B ) ) ) )
18 17 a1i 
 |-  ( 1 e. ZZ -> ( A e. ZZ -> ( 1 <_ A -> ( B e. ZZ -> ( A < B -> 0 < B ) ) ) ) )
19 18 3imp 
 |-  ( ( 1 e. ZZ /\ A e. ZZ /\ 1 <_ A ) -> ( B e. ZZ -> ( A < B -> 0 < B ) ) )
20 3 19 sylbi 
 |-  ( A e. ( ZZ>= ` 1 ) -> ( B e. ZZ -> ( A < B -> 0 < B ) ) )
21 20 3imp 
 |-  ( ( A e. ( ZZ>= ` 1 ) /\ B e. ZZ /\ A < B ) -> 0 < B )
22 2 21 jca 
 |-  ( ( A e. ( ZZ>= ` 1 ) /\ B e. ZZ /\ A < B ) -> ( B e. ZZ /\ 0 < B ) )
23 elfzo2 
 |-  ( A e. ( 1 ..^ B ) <-> ( A e. ( ZZ>= ` 1 ) /\ B e. ZZ /\ A < B ) )
24 elnnz 
 |-  ( B e. NN <-> ( B e. ZZ /\ 0 < B ) )
25 22 23 24 3imtr4i 
 |-  ( A e. ( 1 ..^ B ) -> B e. NN )
26 nnm1nn0 
 |-  ( B e. NN -> ( B - 1 ) e. NN0 )
27 25 26 syl 
 |-  ( A e. ( 1 ..^ B ) -> ( B - 1 ) e. NN0 )
28 faccl 
 |-  ( ( B - 1 ) e. NN0 -> ( ! ` ( B - 1 ) ) e. NN )
29 28 nnzd 
 |-  ( ( B - 1 ) e. NN0 -> ( ! ` ( B - 1 ) ) e. ZZ )
30 27 29 syl 
 |-  ( A e. ( 1 ..^ B ) -> ( ! ` ( B - 1 ) ) e. ZZ )
31 elfzoel2 
 |-  ( A e. ( 1 ..^ B ) -> B e. ZZ )
32 1 30 31 3jca 
 |-  ( A e. ( 1 ..^ B ) -> ( A e. ZZ /\ ( ! ` ( B - 1 ) ) e. ZZ /\ B e. ZZ ) )
33 elfzo1 
 |-  ( A e. ( 1 ..^ B ) <-> ( A e. NN /\ B e. NN /\ A < B ) )
34 33 simp1bi 
 |-  ( A e. ( 1 ..^ B ) -> A e. NN )
35 nnz 
 |-  ( A e. NN -> A e. ZZ )
36 35 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ A < B ) -> A e. ZZ )
37 nnz 
 |-  ( B e. NN -> B e. ZZ )
38 peano2zm 
 |-  ( B e. ZZ -> ( B - 1 ) e. ZZ )
39 37 38 syl 
 |-  ( B e. NN -> ( B - 1 ) e. ZZ )
40 39 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ A < B ) -> ( B - 1 ) e. ZZ )
41 nnltlem1 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A < B <-> A <_ ( B - 1 ) ) )
42 41 biimp3a 
 |-  ( ( A e. NN /\ B e. NN /\ A < B ) -> A <_ ( B - 1 ) )
43 36 40 42 3jca 
 |-  ( ( A e. NN /\ B e. NN /\ A < B ) -> ( A e. ZZ /\ ( B - 1 ) e. ZZ /\ A <_ ( B - 1 ) ) )
44 eluz2 
 |-  ( ( B - 1 ) e. ( ZZ>= ` A ) <-> ( A e. ZZ /\ ( B - 1 ) e. ZZ /\ A <_ ( B - 1 ) ) )
45 43 33 44 3imtr4i 
 |-  ( A e. ( 1 ..^ B ) -> ( B - 1 ) e. ( ZZ>= ` A ) )
46 dvdsfac 
 |-  ( ( A e. NN /\ ( B - 1 ) e. ( ZZ>= ` A ) ) -> A || ( ! ` ( B - 1 ) ) )
47 34 45 46 syl2anc 
 |-  ( A e. ( 1 ..^ B ) -> A || ( ! ` ( B - 1 ) ) )
48 dvdsmulc 
 |-  ( ( A e. ZZ /\ ( ! ` ( B - 1 ) ) e. ZZ /\ B e. ZZ ) -> ( A || ( ! ` ( B - 1 ) ) -> ( A x. B ) || ( ( ! ` ( B - 1 ) ) x. B ) ) )
49 32 47 48 sylc 
 |-  ( A e. ( 1 ..^ B ) -> ( A x. B ) || ( ( ! ` ( B - 1 ) ) x. B ) )
50 facnn2 
 |-  ( B e. NN -> ( ! ` B ) = ( ( ! ` ( B - 1 ) ) x. B ) )
51 25 50 syl 
 |-  ( A e. ( 1 ..^ B ) -> ( ! ` B ) = ( ( ! ` ( B - 1 ) ) x. B ) )
52 49 51 breqtrrd 
 |-  ( A e. ( 1 ..^ B ) -> ( A x. B ) || ( ! ` B ) )