Step | Hyp | Ref
| Expression |
1 | | lcmineqlem13.1 |
. 2
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 |
2 | | lcmineqlem13.2 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℕ) |
3 | 2 | nnzd 12110 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
4 | | nnge1 11687 |
. . . . 5
⊢ (𝑀 ∈ ℕ → 1 ≤
𝑀) |
5 | 2, 4 | syl 17 |
. . . 4
⊢ (𝜑 → 1 ≤ 𝑀) |
6 | | lcmineqlem13.4 |
. . . 4
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
7 | 3, 5, 6 | 3jca 1126 |
. . 3
⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 1 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁)) |
8 | | oveq1 7150 |
. . . . . . . . 9
⊢ (𝑖 = 1 → (𝑖 − 1) = (1 − 1)) |
9 | 8 | oveq2d 7159 |
. . . . . . . 8
⊢ (𝑖 = 1 → (𝑥↑(𝑖 − 1)) = (𝑥↑(1 − 1))) |
10 | | oveq2 7151 |
. . . . . . . . 9
⊢ (𝑖 = 1 → (𝑁 − 𝑖) = (𝑁 − 1)) |
11 | 10 | oveq2d 7159 |
. . . . . . . 8
⊢ (𝑖 = 1 → ((1 − 𝑥)↑(𝑁 − 𝑖)) = ((1 − 𝑥)↑(𝑁 − 1))) |
12 | 9, 11 | oveq12d 7161 |
. . . . . . 7
⊢ (𝑖 = 1 → ((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) = ((𝑥↑(1 − 1)) · ((1 −
𝑥)↑(𝑁 − 1)))) |
13 | 12 | adantr 485 |
. . . . . 6
⊢ ((𝑖 = 1 ∧ 𝑥 ∈ (0[,]1)) → ((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) = ((𝑥↑(1 − 1)) · ((1 −
𝑥)↑(𝑁 − 1)))) |
14 | 13 | itgeq2dv 24466 |
. . . . 5
⊢ (𝑖 = 1 → ∫(0[,]1)((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) d𝑥 = ∫(0[,]1)((𝑥↑(1 − 1)) · ((1 −
𝑥)↑(𝑁 − 1))) d𝑥) |
15 | | id 22 |
. . . . . . 7
⊢ (𝑖 = 1 → 𝑖 = 1) |
16 | | oveq2 7151 |
. . . . . . 7
⊢ (𝑖 = 1 → (𝑁C𝑖) = (𝑁C1)) |
17 | 15, 16 | oveq12d 7161 |
. . . . . 6
⊢ (𝑖 = 1 → (𝑖 · (𝑁C𝑖)) = (1 · (𝑁C1))) |
18 | 17 | oveq2d 7159 |
. . . . 5
⊢ (𝑖 = 1 → (1 / (𝑖 · (𝑁C𝑖))) = (1 / (1 · (𝑁C1)))) |
19 | 14, 18 | eqeq12d 2775 |
. . . 4
⊢ (𝑖 = 1 → (∫(0[,]1)((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) d𝑥 = (1 / (𝑖 · (𝑁C𝑖))) ↔ ∫(0[,]1)((𝑥↑(1 − 1)) · ((1 −
𝑥)↑(𝑁 − 1))) d𝑥 = (1 / (1 · (𝑁C1))))) |
20 | | oveq1 7150 |
. . . . . . . . 9
⊢ (𝑖 = 𝑚 → (𝑖 − 1) = (𝑚 − 1)) |
21 | 20 | oveq2d 7159 |
. . . . . . . 8
⊢ (𝑖 = 𝑚 → (𝑥↑(𝑖 − 1)) = (𝑥↑(𝑚 − 1))) |
22 | | oveq2 7151 |
. . . . . . . . 9
⊢ (𝑖 = 𝑚 → (𝑁 − 𝑖) = (𝑁 − 𝑚)) |
23 | 22 | oveq2d 7159 |
. . . . . . . 8
⊢ (𝑖 = 𝑚 → ((1 − 𝑥)↑(𝑁 − 𝑖)) = ((1 − 𝑥)↑(𝑁 − 𝑚))) |
24 | 21, 23 | oveq12d 7161 |
. . . . . . 7
⊢ (𝑖 = 𝑚 → ((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) = ((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚)))) |
25 | 24 | adantr 485 |
. . . . . 6
⊢ ((𝑖 = 𝑚 ∧ 𝑥 ∈ (0[,]1)) → ((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) = ((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚)))) |
26 | 25 | itgeq2dv 24466 |
. . . . 5
⊢ (𝑖 = 𝑚 → ∫(0[,]1)((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) d𝑥 = ∫(0[,]1)((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚))) d𝑥) |
27 | | id 22 |
. . . . . . 7
⊢ (𝑖 = 𝑚 → 𝑖 = 𝑚) |
28 | | oveq2 7151 |
. . . . . . 7
⊢ (𝑖 = 𝑚 → (𝑁C𝑖) = (𝑁C𝑚)) |
29 | 27, 28 | oveq12d 7161 |
. . . . . 6
⊢ (𝑖 = 𝑚 → (𝑖 · (𝑁C𝑖)) = (𝑚 · (𝑁C𝑚))) |
30 | 29 | oveq2d 7159 |
. . . . 5
⊢ (𝑖 = 𝑚 → (1 / (𝑖 · (𝑁C𝑖))) = (1 / (𝑚 · (𝑁C𝑚)))) |
31 | 26, 30 | eqeq12d 2775 |
. . . 4
⊢ (𝑖 = 𝑚 → (∫(0[,]1)((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) d𝑥 = (1 / (𝑖 · (𝑁C𝑖))) ↔ ∫(0[,]1)((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚))) d𝑥 = (1 / (𝑚 · (𝑁C𝑚))))) |
32 | | oveq1 7150 |
. . . . . . . . 9
⊢ (𝑖 = (𝑚 + 1) → (𝑖 − 1) = ((𝑚 + 1) − 1)) |
33 | 32 | oveq2d 7159 |
. . . . . . . 8
⊢ (𝑖 = (𝑚 + 1) → (𝑥↑(𝑖 − 1)) = (𝑥↑((𝑚 + 1) − 1))) |
34 | | oveq2 7151 |
. . . . . . . . 9
⊢ (𝑖 = (𝑚 + 1) → (𝑁 − 𝑖) = (𝑁 − (𝑚 + 1))) |
35 | 34 | oveq2d 7159 |
. . . . . . . 8
⊢ (𝑖 = (𝑚 + 1) → ((1 − 𝑥)↑(𝑁 − 𝑖)) = ((1 − 𝑥)↑(𝑁 − (𝑚 + 1)))) |
36 | 33, 35 | oveq12d 7161 |
. . . . . . 7
⊢ (𝑖 = (𝑚 + 1) → ((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) = ((𝑥↑((𝑚 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑚 + 1))))) |
37 | 36 | adantr 485 |
. . . . . 6
⊢ ((𝑖 = (𝑚 + 1) ∧ 𝑥 ∈ (0[,]1)) → ((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) = ((𝑥↑((𝑚 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑚 + 1))))) |
38 | 37 | itgeq2dv 24466 |
. . . . 5
⊢ (𝑖 = (𝑚 + 1) → ∫(0[,]1)((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) d𝑥 = ∫(0[,]1)((𝑥↑((𝑚 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑚 + 1)))) d𝑥) |
39 | | id 22 |
. . . . . . 7
⊢ (𝑖 = (𝑚 + 1) → 𝑖 = (𝑚 + 1)) |
40 | | oveq2 7151 |
. . . . . . 7
⊢ (𝑖 = (𝑚 + 1) → (𝑁C𝑖) = (𝑁C(𝑚 + 1))) |
41 | 39, 40 | oveq12d 7161 |
. . . . . 6
⊢ (𝑖 = (𝑚 + 1) → (𝑖 · (𝑁C𝑖)) = ((𝑚 + 1) · (𝑁C(𝑚 + 1)))) |
42 | 41 | oveq2d 7159 |
. . . . 5
⊢ (𝑖 = (𝑚 + 1) → (1 / (𝑖 · (𝑁C𝑖))) = (1 / ((𝑚 + 1) · (𝑁C(𝑚 + 1))))) |
43 | 38, 42 | eqeq12d 2775 |
. . . 4
⊢ (𝑖 = (𝑚 + 1) → (∫(0[,]1)((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) d𝑥 = (1 / (𝑖 · (𝑁C𝑖))) ↔ ∫(0[,]1)((𝑥↑((𝑚 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑚 + 1)))) d𝑥 = (1 / ((𝑚 + 1) · (𝑁C(𝑚 + 1)))))) |
44 | | oveq1 7150 |
. . . . . . . . 9
⊢ (𝑖 = 𝑀 → (𝑖 − 1) = (𝑀 − 1)) |
45 | 44 | oveq2d 7159 |
. . . . . . . 8
⊢ (𝑖 = 𝑀 → (𝑥↑(𝑖 − 1)) = (𝑥↑(𝑀 − 1))) |
46 | | oveq2 7151 |
. . . . . . . . 9
⊢ (𝑖 = 𝑀 → (𝑁 − 𝑖) = (𝑁 − 𝑀)) |
47 | 46 | oveq2d 7159 |
. . . . . . . 8
⊢ (𝑖 = 𝑀 → ((1 − 𝑥)↑(𝑁 − 𝑖)) = ((1 − 𝑥)↑(𝑁 − 𝑀))) |
48 | 45, 47 | oveq12d 7161 |
. . . . . . 7
⊢ (𝑖 = 𝑀 → ((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) = ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) |
49 | 48 | adantr 485 |
. . . . . 6
⊢ ((𝑖 = 𝑀 ∧ 𝑥 ∈ (0[,]1)) → ((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) = ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) |
50 | 49 | itgeq2dv 24466 |
. . . . 5
⊢ (𝑖 = 𝑀 → ∫(0[,]1)((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) d𝑥 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) |
51 | | id 22 |
. . . . . . 7
⊢ (𝑖 = 𝑀 → 𝑖 = 𝑀) |
52 | | oveq2 7151 |
. . . . . . 7
⊢ (𝑖 = 𝑀 → (𝑁C𝑖) = (𝑁C𝑀)) |
53 | 51, 52 | oveq12d 7161 |
. . . . . 6
⊢ (𝑖 = 𝑀 → (𝑖 · (𝑁C𝑖)) = (𝑀 · (𝑁C𝑀))) |
54 | 53 | oveq2d 7159 |
. . . . 5
⊢ (𝑖 = 𝑀 → (1 / (𝑖 · (𝑁C𝑖))) = (1 / (𝑀 · (𝑁C𝑀)))) |
55 | 50, 54 | eqeq12d 2775 |
. . . 4
⊢ (𝑖 = 𝑀 → (∫(0[,]1)((𝑥↑(𝑖 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑖))) d𝑥 = (1 / (𝑖 · (𝑁C𝑖))) ↔ ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 = (1 / (𝑀 · (𝑁C𝑀))))) |
56 | | lcmineqlem13.3 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
57 | 56 | lcmineqlem12 39592 |
. . . 4
⊢ (𝜑 → ∫(0[,]1)((𝑥↑(1 − 1)) ·
((1 − 𝑥)↑(𝑁 − 1))) d𝑥 = (1 / (1 · (𝑁C1)))) |
58 | | elnnz1 12032 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ ↔ (𝑚 ∈ ℤ ∧ 1 ≤
𝑚)) |
59 | 58 | biimpri 231 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℤ ∧ 1 ≤
𝑚) → 𝑚 ∈
ℕ) |
60 | 59 | 3adant3 1130 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℤ ∧ 1 ≤
𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ ℕ) |
61 | 60 | adantl 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁)) → 𝑚 ∈ ℕ) |
62 | 56 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁)) → 𝑁 ∈ ℕ) |
63 | | simpr3 1194 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁)) → 𝑚 < 𝑁) |
64 | 61, 62, 63 | lcmineqlem10 39590 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁)) → ∫(0[,]1)((𝑥↑((𝑚 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑚 + 1)))) d𝑥 = ((𝑚 / (𝑁 − 𝑚)) · ∫(0[,]1)((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚))) d𝑥)) |
65 | 64 | 3adant3 1130 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁) ∧ ∫(0[,]1)((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚))) d𝑥 = (1 / (𝑚 · (𝑁C𝑚)))) → ∫(0[,]1)((𝑥↑((𝑚 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑚 + 1)))) d𝑥 = ((𝑚 / (𝑁 − 𝑚)) · ∫(0[,]1)((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚))) d𝑥)) |
66 | | oveq2 7151 |
. . . . . . 7
⊢
(∫(0[,]1)((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚))) d𝑥 = (1 / (𝑚 · (𝑁C𝑚))) → ((𝑚 / (𝑁 − 𝑚)) · ∫(0[,]1)((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚))) d𝑥) = ((𝑚 / (𝑁 − 𝑚)) · (1 / (𝑚 · (𝑁C𝑚))))) |
67 | 66 | 3ad2ant3 1133 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁) ∧ ∫(0[,]1)((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚))) d𝑥 = (1 / (𝑚 · (𝑁C𝑚)))) → ((𝑚 / (𝑁 − 𝑚)) · ∫(0[,]1)((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚))) d𝑥) = ((𝑚 / (𝑁 − 𝑚)) · (1 / (𝑚 · (𝑁C𝑚))))) |
68 | 65, 67 | eqtrd 2794 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁) ∧ ∫(0[,]1)((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚))) d𝑥 = (1 / (𝑚 · (𝑁C𝑚)))) → ∫(0[,]1)((𝑥↑((𝑚 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑚 + 1)))) d𝑥 = ((𝑚 / (𝑁 − 𝑚)) · (1 / (𝑚 · (𝑁C𝑚))))) |
69 | 61, 62, 63 | lcmineqlem11 39591 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁)) → (1 / ((𝑚 + 1) · (𝑁C(𝑚 + 1)))) = ((𝑚 / (𝑁 − 𝑚)) · (1 / (𝑚 · (𝑁C𝑚))))) |
70 | 69 | 3adant3 1130 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁) ∧ ∫(0[,]1)((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚))) d𝑥 = (1 / (𝑚 · (𝑁C𝑚)))) → (1 / ((𝑚 + 1) · (𝑁C(𝑚 + 1)))) = ((𝑚 / (𝑁 − 𝑚)) · (1 / (𝑚 · (𝑁C𝑚))))) |
71 | 68, 70 | eqtr4d 2797 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁) ∧ ∫(0[,]1)((𝑥↑(𝑚 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑚))) d𝑥 = (1 / (𝑚 · (𝑁C𝑚)))) → ∫(0[,]1)((𝑥↑((𝑚 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑚 + 1)))) d𝑥 = (1 / ((𝑚 + 1) · (𝑁C(𝑚 + 1))))) |
72 | | 1zzd 12037 |
. . . 4
⊢ (𝜑 → 1 ∈
ℤ) |
73 | 56 | nnzd 12110 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
74 | 56 | nnge1d 11707 |
. . . 4
⊢ (𝜑 → 1 ≤ 𝑁) |
75 | 19, 31, 43, 55, 57, 71, 72, 73, 74 | fzindd 39528 |
. . 3
⊢ ((𝜑 ∧ (𝑀 ∈ ℤ ∧ 1 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁)) → ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 = (1 / (𝑀 · (𝑁C𝑀)))) |
76 | 7, 75 | mpdan 687 |
. 2
⊢ (𝜑 → ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 = (1 / (𝑀 · (𝑁C𝑀)))) |
77 | 1, 76 | syl5eq 2806 |
1
⊢ (𝜑 → 𝐹 = (1 / (𝑀 · (𝑁C𝑀)))) |