Proof of Theorem lcmineqlem11
Step | Hyp | Ref
| Expression |
1 | | lcmineqlem11.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
2 | 1 | nncnd 11675 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) |
3 | | 1cnd 10659 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
4 | 2, 3 | addcld 10683 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 + 1) ∈ ℂ) |
5 | | lcmineqlem11.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
6 | 1 | nnnn0d 11979 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
7 | | 1nn0 11935 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ0 |
8 | 7 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℕ0) |
9 | 6, 8 | nn0addcld 11983 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 + 1) ∈
ℕ0) |
10 | | lcmineqlem11.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 < 𝑁) |
11 | 1 | nnzd 12110 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℤ) |
12 | 5 | nnzd 12110 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℤ) |
13 | | zltp1le 12056 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
14 | 11, 12, 13 | syl2anc 588 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
15 | 10, 14 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 + 1) ≤ 𝑁) |
16 | 5, 9, 15 | bccl2d 39544 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁C(𝑀 + 1)) ∈ ℕ) |
17 | 16 | nncnd 11675 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁C(𝑀 + 1)) ∈ ℂ) |
18 | 4, 17 | mulcld 10684 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 + 1) · (𝑁C(𝑀 + 1))) ∈ ℂ) |
19 | 18 | div1d 11431 |
. . . . . . 7
⊢ (𝜑 → (((𝑀 + 1) · (𝑁C(𝑀 + 1))) / 1) = ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) |
20 | 11 | peano2zd 12114 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
21 | 1 | peano2nnd 11676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
22 | 21 | nnge1d 11707 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ≤ (𝑀 + 1)) |
23 | 20, 22, 15 | 3jca 1126 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑀 + 1) ∈ ℤ ∧ 1 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁)) |
24 | | 1z 12036 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℤ |
25 | | elfz1 12929 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℤ ∧ 𝑁
∈ ℤ) → ((𝑀
+ 1) ∈ (1...𝑁) ↔
((𝑀 + 1) ∈ ℤ
∧ 1 ≤ (𝑀 + 1) ∧
(𝑀 + 1) ≤ 𝑁))) |
26 | 24, 25 | mpan 690 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → ((𝑀 + 1) ∈ (1...𝑁) ↔ ((𝑀 + 1) ∈ ℤ ∧ 1 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁))) |
27 | 12, 26 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑀 + 1) ∈ (1...𝑁) ↔ ((𝑀 + 1) ∈ ℤ ∧ 1 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁))) |
28 | 23, 27 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 + 1) ∈ (1...𝑁)) |
29 | | bcm1k 13710 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 + 1) ∈ (1...𝑁) → (𝑁C(𝑀 + 1)) = ((𝑁C((𝑀 + 1) − 1)) · ((𝑁 − ((𝑀 + 1) − 1)) / (𝑀 + 1)))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁C(𝑀 + 1)) = ((𝑁C((𝑀 + 1) − 1)) · ((𝑁 − ((𝑀 + 1) − 1)) / (𝑀 + 1)))) |
31 | 2, 3 | pncand 11021 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) |
32 | 31 | oveq2d 7159 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁C((𝑀 + 1) − 1)) = (𝑁C𝑀)) |
33 | 31 | oveq2d 7159 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − ((𝑀 + 1) − 1)) = (𝑁 − 𝑀)) |
34 | 33 | oveq1d 7158 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − ((𝑀 + 1) − 1)) / (𝑀 + 1)) = ((𝑁 − 𝑀) / (𝑀 + 1))) |
35 | 32, 34 | oveq12d 7161 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁C((𝑀 + 1) − 1)) · ((𝑁 − ((𝑀 + 1) − 1)) / (𝑀 + 1))) = ((𝑁C𝑀) · ((𝑁 − 𝑀) / (𝑀 + 1)))) |
36 | 30, 35 | eqtrd 2794 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁C(𝑀 + 1)) = ((𝑁C𝑀) · ((𝑁 − 𝑀) / (𝑀 + 1)))) |
37 | 1 | nnred 11674 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℝ) |
38 | 5 | nnred 11674 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℝ) |
39 | 37, 38, 10 | ltled 10811 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
40 | 5, 6, 39 | bccl2d 39544 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁C𝑀) ∈ ℕ) |
41 | 40 | nncnd 11675 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁C𝑀) ∈ ℂ) |
42 | 5 | nncnd 11675 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℂ) |
43 | 42, 2 | subcld 11020 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℂ) |
44 | 21 | nnne0d 11709 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 + 1) ≠ 0) |
45 | 41, 43, 4, 44 | divassd 11474 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑁C𝑀) · (𝑁 − 𝑀)) / (𝑀 + 1)) = ((𝑁C𝑀) · ((𝑁 − 𝑀) / (𝑀 + 1)))) |
46 | 36, 45 | eqtr4d 2797 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁C(𝑀 + 1)) = (((𝑁C𝑀) · (𝑁 − 𝑀)) / (𝑀 + 1))) |
47 | 46 | eqcomd 2765 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑁C𝑀) · (𝑁 − 𝑀)) / (𝑀 + 1)) = (𝑁C(𝑀 + 1))) |
48 | 41, 43 | mulcld 10684 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁C𝑀) · (𝑁 − 𝑀)) ∈ ℂ) |
49 | 48, 17, 4, 44 | divmul2d 11472 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑁C𝑀) · (𝑁 − 𝑀)) / (𝑀 + 1)) = (𝑁C(𝑀 + 1)) ↔ ((𝑁C𝑀) · (𝑁 − 𝑀)) = ((𝑀 + 1) · (𝑁C(𝑀 + 1))))) |
50 | 47, 49 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁C𝑀) · (𝑁 − 𝑀)) = ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) |
51 | 50 | eqcomd 2765 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 + 1) · (𝑁C(𝑀 + 1))) = ((𝑁C𝑀) · (𝑁 − 𝑀))) |
52 | 41, 43 | mulcomd 10685 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁C𝑀) · (𝑁 − 𝑀)) = ((𝑁 − 𝑀) · (𝑁C𝑀))) |
53 | 51, 52 | eqtrd 2794 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 + 1) · (𝑁C(𝑀 + 1))) = ((𝑁 − 𝑀) · (𝑁C𝑀))) |
54 | 19, 53 | eqtrd 2794 |
. . . . . 6
⊢ (𝜑 → (((𝑀 + 1) · (𝑁C(𝑀 + 1))) / 1) = ((𝑁 − 𝑀) · (𝑁C𝑀))) |
55 | 43, 41 | mulcld 10684 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 𝑀) · (𝑁C𝑀)) ∈ ℂ) |
56 | 1 | nnne0d 11709 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ≠ 0) |
57 | 55, 2, 56 | divcan3d 11444 |
. . . . . 6
⊢ (𝜑 → ((𝑀 · ((𝑁 − 𝑀) · (𝑁C𝑀))) / 𝑀) = ((𝑁 − 𝑀) · (𝑁C𝑀))) |
58 | 54, 57 | eqtr4d 2797 |
. . . . 5
⊢ (𝜑 → (((𝑀 + 1) · (𝑁C(𝑀 + 1))) / 1) = ((𝑀 · ((𝑁 − 𝑀) · (𝑁C𝑀))) / 𝑀)) |
59 | 2, 43, 41 | mul12d 10872 |
. . . . . 6
⊢ (𝜑 → (𝑀 · ((𝑁 − 𝑀) · (𝑁C𝑀))) = ((𝑁 − 𝑀) · (𝑀 · (𝑁C𝑀)))) |
60 | 59 | oveq1d 7158 |
. . . . 5
⊢ (𝜑 → ((𝑀 · ((𝑁 − 𝑀) · (𝑁C𝑀))) / 𝑀) = (((𝑁 − 𝑀) · (𝑀 · (𝑁C𝑀))) / 𝑀)) |
61 | 58, 60 | eqtrd 2794 |
. . . 4
⊢ (𝜑 → (((𝑀 + 1) · (𝑁C(𝑀 + 1))) / 1) = (((𝑁 − 𝑀) · (𝑀 · (𝑁C𝑀))) / 𝑀)) |
62 | | 0ne1 11730 |
. . . . . . 7
⊢ 0 ≠
1 |
63 | 62 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≠ 1) |
64 | 63 | necomd 3004 |
. . . . 5
⊢ (𝜑 → 1 ≠ 0) |
65 | 16 | nnne0d 11709 |
. . . . . 6
⊢ (𝜑 → (𝑁C(𝑀 + 1)) ≠ 0) |
66 | 4, 17, 44, 65 | mulne0d 11315 |
. . . . 5
⊢ (𝜑 → ((𝑀 + 1) · (𝑁C(𝑀 + 1))) ≠ 0) |
67 | 2, 41 | mulcld 10684 |
. . . . . 6
⊢ (𝜑 → (𝑀 · (𝑁C𝑀)) ∈ ℂ) |
68 | 43, 67 | mulcld 10684 |
. . . . 5
⊢ (𝜑 → ((𝑁 − 𝑀) · (𝑀 · (𝑁C𝑀))) ∈ ℂ) |
69 | 37, 10 | gtned 10798 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ≠ 𝑀) |
70 | 42, 2, 69 | subne0d 11029 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 𝑀) ≠ 0) |
71 | 40 | nnne0d 11709 |
. . . . . . 7
⊢ (𝜑 → (𝑁C𝑀) ≠ 0) |
72 | 2, 41, 56, 71 | mulne0d 11315 |
. . . . . 6
⊢ (𝜑 → (𝑀 · (𝑁C𝑀)) ≠ 0) |
73 | 43, 67, 70, 72 | mulne0d 11315 |
. . . . 5
⊢ (𝜑 → ((𝑁 − 𝑀) · (𝑀 · (𝑁C𝑀))) ≠ 0) |
74 | 3, 64, 18, 66, 2, 56, 68, 73 | recbothd 39545 |
. . . 4
⊢ (𝜑 → ((1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = (𝑀 / ((𝑁 − 𝑀) · (𝑀 · (𝑁C𝑀)))) ↔ (((𝑀 + 1) · (𝑁C(𝑀 + 1))) / 1) = (((𝑁 − 𝑀) · (𝑀 · (𝑁C𝑀))) / 𝑀))) |
75 | 61, 74 | mpbird 260 |
. . 3
⊢ (𝜑 → (1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = (𝑀 / ((𝑁 − 𝑀) · (𝑀 · (𝑁C𝑀))))) |
76 | 2 | mulid1d 10681 |
. . . 4
⊢ (𝜑 → (𝑀 · 1) = 𝑀) |
77 | 76 | oveq1d 7158 |
. . 3
⊢ (𝜑 → ((𝑀 · 1) / ((𝑁 − 𝑀) · (𝑀 · (𝑁C𝑀)))) = (𝑀 / ((𝑁 − 𝑀) · (𝑀 · (𝑁C𝑀))))) |
78 | 75, 77 | eqtr4d 2797 |
. 2
⊢ (𝜑 → (1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = ((𝑀 · 1) / ((𝑁 − 𝑀) · (𝑀 · (𝑁C𝑀))))) |
79 | 2, 43, 3, 67, 70, 72 | divmuldivd 11480 |
. 2
⊢ (𝜑 → ((𝑀 / (𝑁 − 𝑀)) · (1 / (𝑀 · (𝑁C𝑀)))) = ((𝑀 · 1) / ((𝑁 − 𝑀) · (𝑀 · (𝑁C𝑀))))) |
80 | 78, 79 | eqtr4d 2797 |
1
⊢ (𝜑 → (1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = ((𝑀 / (𝑁 − 𝑀)) · (1 / (𝑀 · (𝑁C𝑀))))) |