Metamath Proof Explorer

Theorem lcmineqlem11

Description: Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses lcmineqlem11.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
lcmineqlem11.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lcmineqlem11.3 ⊢ ( 𝜑 → 𝑀 < 𝑁 )
Assertion lcmineqlem11 ( 𝜑 → ( 1 / ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) ) = ( ( 𝑀 / ( 𝑁 − 𝑀 ) ) · ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem11.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 lcmineqlem11.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 lcmineqlem11.3 ⊢ ( 𝜑 → 𝑀 < 𝑁 )
4 1 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
5 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
6 4 5 addcld ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℂ )
7 1 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
8 1nn0 ⊢ 1 ∈ ℕ0
9 8 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
10 7 9 nn0addcld ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ0 )
11 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
12 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
13 zltp1le ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 + 1 ) ≤ 𝑁 ) )
14 11 12 13 syl2anc ⊢ ( 𝜑 → ( 𝑀 < 𝑁 ↔ ( 𝑀 + 1 ) ≤ 𝑁 ) )
15 3 14 mpbid ⊢ ( 𝜑 → ( 𝑀 + 1 ) ≤ 𝑁 )
16 2 10 15 bccl2d ⊢ ( 𝜑 → ( 𝑁 C ( 𝑀 + 1 ) ) ∈ ℕ )
17 16 nncnd ⊢ ( 𝜑 → ( 𝑁 C ( 𝑀 + 1 ) ) ∈ ℂ )
18 6 17 mulcld ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) ∈ ℂ )
19 18 div1d ⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) / 1 ) = ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) )
20 11 peano2zd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℤ )
21 1 peano2nnd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ )
22 21 nnge1d ⊢ ( 𝜑 → 1 ≤ ( 𝑀 + 1 ) )
23 20 22 15 3jca ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ∈ ℤ ∧ 1 ≤ ( 𝑀 + 1 ) ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) )
24 1z ⊢ 1 ∈ ℤ
25 elfz1 ⊢ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑀 + 1 ) ∈ ℤ ∧ 1 ≤ ( 𝑀 + 1 ) ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) )
26 24 25 mpan ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑀 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑀 + 1 ) ∈ ℤ ∧ 1 ≤ ( 𝑀 + 1 ) ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) )
27 12 26 syl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑀 + 1 ) ∈ ℤ ∧ 1 ≤ ( 𝑀 + 1 ) ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) )
28 23 27 mpbird ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( 1 ... 𝑁 ) )
29 bcm1k ⊢ ( ( 𝑀 + 1 ) ∈ ( 1 ... 𝑁 ) → ( 𝑁 C ( 𝑀 + 1 ) ) = ( ( 𝑁 C ( ( 𝑀 + 1 ) − 1 ) ) · ( ( 𝑁 − ( ( 𝑀 + 1 ) − 1 ) ) / ( 𝑀 + 1 ) ) ) )
30 28 29 syl ⊢ ( 𝜑 → ( 𝑁 C ( 𝑀 + 1 ) ) = ( ( 𝑁 C ( ( 𝑀 + 1 ) − 1 ) ) · ( ( 𝑁 − ( ( 𝑀 + 1 ) − 1 ) ) / ( 𝑀 + 1 ) ) ) )
31 4 5 pncand ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
32 31 oveq2d ⊢ ( 𝜑 → ( 𝑁 C ( ( 𝑀 + 1 ) − 1 ) ) = ( 𝑁 C 𝑀 ) )
33 31 oveq2d ⊢ ( 𝜑 → ( 𝑁 − ( ( 𝑀 + 1 ) − 1 ) ) = ( 𝑁 − 𝑀 ) )
34 33 oveq1d ⊢ ( 𝜑 → ( ( 𝑁 − ( ( 𝑀 + 1 ) − 1 ) ) / ( 𝑀 + 1 ) ) = ( ( 𝑁 − 𝑀 ) / ( 𝑀 + 1 ) ) )
35 32 34 oveq12d ⊢ ( 𝜑 → ( ( 𝑁 C ( ( 𝑀 + 1 ) − 1 ) ) · ( ( 𝑁 − ( ( 𝑀 + 1 ) − 1 ) ) / ( 𝑀 + 1 ) ) ) = ( ( 𝑁 C 𝑀 ) · ( ( 𝑁 − 𝑀 ) / ( 𝑀 + 1 ) ) ) )
36 30 35 eqtrd ⊢ ( 𝜑 → ( 𝑁 C ( 𝑀 + 1 ) ) = ( ( 𝑁 C 𝑀 ) · ( ( 𝑁 − 𝑀 ) / ( 𝑀 + 1 ) ) ) )
37 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
38 2 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
39 37 38 3 ltled ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
40 2 7 39 bccl2d ⊢ ( 𝜑 → ( 𝑁 C 𝑀 ) ∈ ℕ )
41 40 nncnd ⊢ ( 𝜑 → ( 𝑁 C 𝑀 ) ∈ ℂ )
42 2 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
43 42 4 subcld ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℂ )
44 21 nnne0d ⊢ ( 𝜑 → ( 𝑀 + 1 ) ≠ 0 )
45 41 43 6 44 divassd ⊢ ( 𝜑 → ( ( ( 𝑁 C 𝑀 ) · ( 𝑁 − 𝑀 ) ) / ( 𝑀 + 1 ) ) = ( ( 𝑁 C 𝑀 ) · ( ( 𝑁 − 𝑀 ) / ( 𝑀 + 1 ) ) ) )
46 36 45 eqtr4d ⊢ ( 𝜑 → ( 𝑁 C ( 𝑀 + 1 ) ) = ( ( ( 𝑁 C 𝑀 ) · ( 𝑁 − 𝑀 ) ) / ( 𝑀 + 1 ) ) )
47 46 eqcomd ⊢ ( 𝜑 → ( ( ( 𝑁 C 𝑀 ) · ( 𝑁 − 𝑀 ) ) / ( 𝑀 + 1 ) ) = ( 𝑁 C ( 𝑀 + 1 ) ) )
48 41 43 mulcld ⊢ ( 𝜑 → ( ( 𝑁 C 𝑀 ) · ( 𝑁 − 𝑀 ) ) ∈ ℂ )
49 48 17 6 44 divmul2d ⊢ ( 𝜑 → ( ( ( ( 𝑁 C 𝑀 ) · ( 𝑁 − 𝑀 ) ) / ( 𝑀 + 1 ) ) = ( 𝑁 C ( 𝑀 + 1 ) ) ↔ ( ( 𝑁 C 𝑀 ) · ( 𝑁 − 𝑀 ) ) = ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) ) )
50 47 49 mpbid ⊢ ( 𝜑 → ( ( 𝑁 C 𝑀 ) · ( 𝑁 − 𝑀 ) ) = ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) )
51 50 eqcomd ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) = ( ( 𝑁 C 𝑀 ) · ( 𝑁 − 𝑀 ) ) )
52 41 43 mulcomd ⊢ ( 𝜑 → ( ( 𝑁 C 𝑀 ) · ( 𝑁 − 𝑀 ) ) = ( ( 𝑁 − 𝑀 ) · ( 𝑁 C 𝑀 ) ) )
53 51 52 eqtrd ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) = ( ( 𝑁 − 𝑀 ) · ( 𝑁 C 𝑀 ) ) )
54 19 53 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) / 1 ) = ( ( 𝑁 − 𝑀 ) · ( 𝑁 C 𝑀 ) ) )
55 43 41 mulcld ⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) · ( 𝑁 C 𝑀 ) ) ∈ ℂ )
56 1 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
57 55 4 56 divcan3d ⊢ ( 𝜑 → ( ( 𝑀 · ( ( 𝑁 − 𝑀 ) · ( 𝑁 C 𝑀 ) ) ) / 𝑀 ) = ( ( 𝑁 − 𝑀 ) · ( 𝑁 C 𝑀 ) ) )
58 54 57 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) / 1 ) = ( ( 𝑀 · ( ( 𝑁 − 𝑀 ) · ( 𝑁 C 𝑀 ) ) ) / 𝑀 ) )
59 4 43 41 mul12d ⊢ ( 𝜑 → ( 𝑀 · ( ( 𝑁 − 𝑀 ) · ( 𝑁 C 𝑀 ) ) ) = ( ( 𝑁 − 𝑀 ) · ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) )
60 59 oveq1d ⊢ ( 𝜑 → ( ( 𝑀 · ( ( 𝑁 − 𝑀 ) · ( 𝑁 C 𝑀 ) ) ) / 𝑀 ) = ( ( ( 𝑁 − 𝑀 ) · ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) / 𝑀 ) )
61 58 60 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) / 1 ) = ( ( ( 𝑁 − 𝑀 ) · ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) / 𝑀 ) )
62 0ne1 ⊢ 0 ≠ 1
63 62 a1i ⊢ ( 𝜑 → 0 ≠ 1 )
64 63 necomd ⊢ ( 𝜑 → 1 ≠ 0 )
65 16 nnne0d ⊢ ( 𝜑 → ( 𝑁 C ( 𝑀 + 1 ) ) ≠ 0 )
66 6 17 44 65 mulne0d ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) ≠ 0 )
67 4 41 mulcld ⊢ ( 𝜑 → ( 𝑀 · ( 𝑁 C 𝑀 ) ) ∈ ℂ )
68 43 67 mulcld ⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) · ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ∈ ℂ )
69 37 3 gtned ⊢ ( 𝜑 → 𝑁 ≠ 𝑀 )
70 42 4 69 subne0d ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ≠ 0 )
71 40 nnne0d ⊢ ( 𝜑 → ( 𝑁 C 𝑀 ) ≠ 0 )
72 4 41 56 71 mulne0d ⊢ ( 𝜑 → ( 𝑀 · ( 𝑁 C 𝑀 ) ) ≠ 0 )
73 43 67 70 72 mulne0d ⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) · ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ≠ 0 )
74 5 64 18 66 4 56 68 73 recbothd ⊢ ( 𝜑 → ( ( 1 / ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) ) = ( 𝑀 / ( ( 𝑁 − 𝑀 ) · ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) ↔ ( ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) / 1 ) = ( ( ( 𝑁 − 𝑀 ) · ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) / 𝑀 ) ) )
75 61 74 mpbird ⊢ ( 𝜑 → ( 1 / ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) ) = ( 𝑀 / ( ( 𝑁 − 𝑀 ) · ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) )
76 4 mulridd ⊢ ( 𝜑 → ( 𝑀 · 1 ) = 𝑀 )
77 76 oveq1d ⊢ ( 𝜑 → ( ( 𝑀 · 1 ) / ( ( 𝑁 − 𝑀 ) · ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) = ( 𝑀 / ( ( 𝑁 − 𝑀 ) · ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) )
78 75 77 eqtr4d ⊢ ( 𝜑 → ( 1 / ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) ) = ( ( 𝑀 · 1 ) / ( ( 𝑁 − 𝑀 ) · ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) )
79 4 43 5 67 70 72 divmuldivd ⊢ ( 𝜑 → ( ( 𝑀 / ( 𝑁 − 𝑀 ) ) · ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) = ( ( 𝑀 · 1 ) / ( ( 𝑁 − 𝑀 ) · ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) )
80 78 79 eqtr4d ⊢ ( 𝜑 → ( 1 / ( ( 𝑀 + 1 ) · ( 𝑁 C ( 𝑀 + 1 ) ) ) ) = ( ( 𝑀 / ( 𝑁 − 𝑀 ) ) · ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) )