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 ( 𝐴 ∈ ( 1 ..^ 𝐵 ) → ( 𝐴 · 𝐵 ) ∥ ( ! ‘ 𝐵 ) )

Proof

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