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 mulid1d ( 𝜑 → ( 𝑀 · 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 𝑀 ) ) ) ) )