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 ∈ 1 ..^ B → A ⁢ B ∥ B !

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢ A ∈ 1 ..^ B → A ∈ ℤ
2 simp2 ⊢ A ∈ ℤ ≥ 1 ∧ B ∈ ℤ ∧ A < B → B ∈ ℤ
3 eluz2 ⊢ A ∈ ℤ ≥ 1 ↔ 1 ∈ ℤ ∧ A ∈ ℤ ∧ 1 ≤ A
4 1re ⊢ 1 ∈ ℝ
5 zre ⊢ A ∈ ℤ → A ∈ ℝ
6 zre ⊢ B ∈ ℤ → B ∈ ℝ
7 lelttr ⊢ 1 ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ → 1 ≤ A ∧ A < B → 1 < B
8 4 5 6 7 mp3an3an ⊢ A ∈ ℤ ∧ B ∈ ℤ → 1 ≤ A ∧ A < B → 1 < B
9 0lt1 ⊢ 0 < 1
10 0re ⊢ 0 ∈ ℝ
11 lttr ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ B ∈ ℝ → 0 < 1 ∧ 1 < B → 0 < B
12 10 4 6 11 mp3an12i ⊢ B ∈ ℤ → 0 < 1 ∧ 1 < B → 0 < B
13 9 12 mpani ⊢ B ∈ ℤ → 1 < B → 0 < B
14 13 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ → 1 < B → 0 < B
15 8 14 syld ⊢ A ∈ ℤ ∧ B ∈ ℤ → 1 ≤ A ∧ A < B → 0 < B
16 15 exp4b ⊢ A ∈ ℤ → B ∈ ℤ → 1 ≤ A → A < B → 0 < B
17 16 com23 ⊢ A ∈ ℤ → 1 ≤ A → B ∈ ℤ → A < B → 0 < B
18 17 a1i ⊢ 1 ∈ ℤ → A ∈ ℤ → 1 ≤ A → B ∈ ℤ → A < B → 0 < B
19 18 3imp ⊢ 1 ∈ ℤ ∧ A ∈ ℤ ∧ 1 ≤ A → B ∈ ℤ → A < B → 0 < B
20 3 19 sylbi ⊢ A ∈ ℤ ≥ 1 → B ∈ ℤ → A < B → 0 < B
21 20 3imp ⊢ A ∈ ℤ ≥ 1 ∧ B ∈ ℤ ∧ A < B → 0 < B
22 2 21 jca ⊢ A ∈ ℤ ≥ 1 ∧ B ∈ ℤ ∧ A < B → B ∈ ℤ ∧ 0 < B
23 elfzo2 ⊢ A ∈ 1 ..^ B ↔ A ∈ ℤ ≥ 1 ∧ B ∈ ℤ ∧ A < B
24 elnnz ⊢ B ∈ ℕ ↔ B ∈ ℤ ∧ 0 < B
25 22 23 24 3imtr4i ⊢ A ∈ 1 ..^ B → B ∈ ℕ
26 nnm1nn0 ⊢ B ∈ ℕ → B − 1 ∈ ℕ 0
27 25 26 syl ⊢ A ∈ 1 ..^ B → B − 1 ∈ ℕ 0
28 faccl ⊢ B − 1 ∈ ℕ 0 → B − 1 ! ∈ ℕ
29 28 nnzd ⊢ B − 1 ∈ ℕ 0 → B − 1 ! ∈ ℤ
30 27 29 syl ⊢ A ∈ 1 ..^ B → B − 1 ! ∈ ℤ
31 elfzoel2 ⊢ A ∈ 1 ..^ B → B ∈ ℤ
32 1 30 31 3jca ⊢ A ∈ 1 ..^ B → A ∈ ℤ ∧ B − 1 ! ∈ ℤ ∧ B ∈ ℤ
33 elfzo1 ⊢ A ∈ 1 ..^ B ↔ A ∈ ℕ ∧ B ∈ ℕ ∧ A < B
34 33 simp1bi ⊢ A ∈ 1 ..^ B → A ∈ ℕ
35 nnz ⊢ A ∈ ℕ → A ∈ ℤ
36 35 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A < B → A ∈ ℤ
37 nnz ⊢ B ∈ ℕ → B ∈ ℤ
38 peano2zm ⊢ B ∈ ℤ → B − 1 ∈ ℤ
39 37 38 syl ⊢ B ∈ ℕ → B − 1 ∈ ℤ
40 39 3ad2ant2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A < B → B − 1 ∈ ℤ
41 nnltlem1 ⊢ A ∈ ℕ ∧ B ∈ ℕ → A < B ↔ A ≤ B − 1
42 41 biimp3a ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A < B → A ≤ B − 1
43 36 40 42 3jca ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A < B → A ∈ ℤ ∧ B − 1 ∈ ℤ ∧ A ≤ B − 1
44 eluz2 ⊢ B − 1 ∈ ℤ ≥ A ↔ A ∈ ℤ ∧ B − 1 ∈ ℤ ∧ A ≤ B − 1
45 43 33 44 3imtr4i ⊢ A ∈ 1 ..^ B → B − 1 ∈ ℤ ≥ A
46 dvdsfac ⊢ A ∈ ℕ ∧ B − 1 ∈ ℤ ≥ A → A ∥ B − 1 !
47 34 45 46 syl2anc ⊢ A ∈ 1 ..^ B → A ∥ B − 1 !
48 dvdsmulc ⊢ A ∈ ℤ ∧ B − 1 ! ∈ ℤ ∧ B ∈ ℤ → A ∥ B − 1 ! → A ⁢ B ∥ B − 1 ! ⁢ B
49 32 47 48 sylc ⊢ A ∈ 1 ..^ B → A ⁢ B ∥ B − 1 ! ⁢ B
50 facnn2 ⊢ B ∈ ℕ → B ! = B − 1 ! ⁢ B
51 25 50 syl ⊢ A ∈ 1 ..^ B → B ! = B − 1 ! ⁢ B
52 49 51 breqtrrd ⊢ A ∈ 1 ..^ B → A ⁢ B ∥ B !