Proof of Theorem lcmineqlem10
Step | Hyp | Ref
| Expression |
1 | | lcmineqlem10.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | nncnd 11675 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℂ) |
3 | | lcmineqlem10.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℕ) |
4 | 3 | nncnd 11675 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℂ) |
5 | 2, 4 | subcld 11020 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℂ) |
6 | | elunitcn 12885 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈
ℂ) |
7 | 3 | nnnn0d 11979 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
8 | | expcl 13482 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ (𝑥↑𝑀) ∈
ℂ) |
9 | 7, 8 | sylan2 596 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝜑) → (𝑥↑𝑀) ∈ ℂ) |
10 | 9 | ancoms 463 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑥↑𝑀) ∈ ℂ) |
11 | 6, 10 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → (𝑥↑𝑀) ∈ ℂ) |
12 | | 1cnd 10659 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 1 ∈
ℂ) |
13 | | simpr 489 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) |
14 | 12, 13 | subcld 11020 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (1 − 𝑥) ∈
ℂ) |
15 | | lcmineqlem10.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 < 𝑁) |
16 | 3 | nnzd 12110 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℤ) |
17 | 1 | nnzd 12110 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℤ) |
18 | | znnsub 12052 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ)) |
19 | 16, 17, 18 | syl2anc 588 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ)) |
20 | 15, 19 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ) |
21 | | nnm1nn0 11960 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 − 𝑀) ∈ ℕ → ((𝑁 − 𝑀) − 1) ∈
ℕ0) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 − 𝑀) − 1) ∈
ℕ0) |
23 | 22 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑁 − 𝑀) − 1) ∈
ℕ0) |
24 | 14, 23 | expcld 13545 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)) ∈
ℂ) |
25 | 6, 24 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)) ∈
ℂ) |
26 | 11, 25 | mulcld 10684 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) ∈
ℂ) |
27 | | 0red 10667 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) |
28 | | 1red 10665 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
29 | | expcncf 23612 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
→ (𝑥 ∈ ℂ
↦ (𝑥↑𝑀)) ∈ (ℂ–cn→ℂ)) |
30 | 7, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑀)) ∈ (ℂ–cn→ℂ)) |
31 | | 1nn 11670 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ |
32 | 31 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℕ) |
33 | 20 | nnge1d 11707 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ≤ (𝑁 − 𝑀)) |
34 | 32, 20, 33 | lcmineqlem9 39589 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) ∈ (ℂ–cn→ℂ)) |
35 | 30, 34 | mulcncf 24131 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) ∈ (ℂ–cn→ℂ)) |
36 | 35 | resclunitintvd 39579 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) ∈ ((0[,]1)–cn→ℂ)) |
37 | | cnicciblnc 24527 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑥 ∈ (0[,]1) ↦ ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) ∈ ((0[,]1)–cn→ℂ)) → (𝑥 ∈ (0[,]1) ↦ ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) ∈
𝐿1) |
38 | 27, 28, 36, 37 | syl3anc 1369 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) ∈
𝐿1) |
39 | 26, 38 | itgcl 24468 |
. . . . . . . 8
⊢ (𝜑 → ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥 ∈ ℂ) |
40 | 5, 39 | mulneg1d 11116 |
. . . . . . 7
⊢ (𝜑 → (-(𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) = -((𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥)) |
41 | 5 | negcld 11007 |
. . . . . . . . . . . 12
⊢ (𝜑 → -(𝑁 − 𝑀) ∈ ℂ) |
42 | 41, 26, 38 | itgmulc2 24518 |
. . . . . . . . . . 11
⊢ (𝜑 → (-(𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) = ∫(0[,]1)(-(𝑁 − 𝑀) · ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) d𝑥) |
43 | 2 | adantr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑁 ∈ ℂ) |
44 | 4 | adantr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑀 ∈ ℂ) |
45 | 43, 44 | subcld 11020 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑁 − 𝑀) ∈ ℂ) |
46 | 45 | negcld 11007 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → -(𝑁 − 𝑀) ∈ ℂ) |
47 | 10, 46, 24 | mul12d 10872 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) = (-(𝑁 − 𝑀) · ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) |
48 | 6, 47 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) = (-(𝑁 − 𝑀) · ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) |
49 | 48 | itgeq2dv 24466 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∫(0[,]1)((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) d𝑥 = ∫(0[,]1)(-(𝑁 − 𝑀) · ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) d𝑥) |
50 | 2 | adantr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → 𝑁 ∈ ℂ) |
51 | 4 | adantr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → 𝑀 ∈ ℂ) |
52 | 50, 51 | subcld 11020 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → (𝑁 − 𝑀) ∈ ℂ) |
53 | 52 | negcld 11007 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → -(𝑁 − 𝑀) ∈ ℂ) |
54 | 53, 25 | mulcld 10684 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) ∈
ℂ) |
55 | 11, 54 | mulcld 10684 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) ∈
ℂ) |
56 | 27, 28, 55 | itgioo 24500 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∫(0(,)1)((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) d𝑥 = ∫(0[,]1)((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) d𝑥) |
57 | | 0le1 11186 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≤
1 |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ 1) |
59 | 30 | resclunitintvd 39579 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ (𝑥↑𝑀)) ∈ ((0[,]1)–cn→ℂ)) |
60 | 3 | nnred 11674 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℝ) |
61 | 1 | nnred 11674 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℝ) |
62 | | ltle 10752 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁)) |
63 | 60, 61, 62 | syl2anc 588 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁)) |
64 | 15, 63 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
65 | 3, 1, 64 | lcmineqlem9 39589 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀))) ∈ (ℂ–cn→ℂ)) |
66 | 65 | resclunitintvd 39579 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((1 − 𝑥)↑(𝑁 − 𝑀))) ∈ ((0[,]1)–cn→ℂ)) |
67 | | ssid 3910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℂ
⊆ ℂ |
68 | | cncfmptc 23598 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℂ ∧ ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ ℂ ↦ 𝑀) ∈ (ℂ–cn→ℂ)) |
69 | 67, 67, 68 | mp3an23 1451 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℂ → (𝑥 ∈ ℂ ↦ 𝑀) ∈ (ℂ–cn→ℂ)) |
70 | 4, 69 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝑀) ∈ (ℂ–cn→ℂ)) |
71 | 70 | resopunitintvd 39578 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ 𝑀) ∈ ((0(,)1)–cn→ℂ)) |
72 | | nnm1nn0 11960 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℕ0) |
73 | | expcncf 23612 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 − 1) ∈
ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 − 1))) ∈ (ℂ–cn→ℂ)) |
74 | 3, 72, 73 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 − 1))) ∈ (ℂ–cn→ℂ)) |
75 | 74 | resopunitintvd 39578 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ (𝑥↑(𝑀 − 1))) ∈ ((0(,)1)–cn→ℂ)) |
76 | 71, 75 | mulcncf 24131 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ (𝑀 · (𝑥↑(𝑀 − 1)))) ∈ ((0(,)1)–cn→ℂ)) |
77 | | cncfmptc 23598 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((-(𝑁 − 𝑀) ∈ ℂ ∧ ℂ ⊆
ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ ℂ ↦ -(𝑁 − 𝑀)) ∈ (ℂ–cn→ℂ)) |
78 | 67, 67, 77 | mp3an23 1451 |
. . . . . . . . . . . . . . . . . . 19
⊢ (-(𝑁 − 𝑀) ∈ ℂ → (𝑥 ∈ ℂ ↦ -(𝑁 − 𝑀)) ∈ (ℂ–cn→ℂ)) |
79 | 41, 78 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ -(𝑁 − 𝑀)) ∈ (ℂ–cn→ℂ)) |
80 | 79 | resopunitintvd 39578 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ -(𝑁 − 𝑀)) ∈ ((0(,)1)–cn→ℂ)) |
81 | 34 | resopunitintvd 39578 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) ∈ ((0(,)1)–cn→ℂ)) |
82 | 80, 81 | mulcncf 24131 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) ∈ ((0(,)1)–cn→ℂ)) |
83 | | ioossicc 12850 |
. . . . . . . . . . . . . . . . . 18
⊢ (0(,)1)
⊆ (0[,]1) |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (0(,)1) ⊆
(0[,]1)) |
85 | | ioombl 24250 |
. . . . . . . . . . . . . . . . . 18
⊢ (0(,)1)
∈ dom vol |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (0(,)1) ∈ dom
vol) |
87 | 79, 34 | mulcncf 24131 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) ∈ (ℂ–cn→ℂ)) |
88 | 30, 87 | mulcncf 24131 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) ∈ (ℂ–cn→ℂ)) |
89 | 88 | resclunitintvd 39579 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) ∈ ((0[,]1)–cn→ℂ)) |
90 | | cnicciblnc 24527 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑥 ∈ (0[,]1) ↦ ((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) ∈ ((0[,]1)–cn→ℂ)) → (𝑥 ∈ (0[,]1) ↦ ((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) ∈
𝐿1) |
91 | 27, 28, 89, 90 | syl3anc 1369 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) ∈
𝐿1) |
92 | 84, 86, 55, 91 | iblss 24489 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ ((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) ∈
𝐿1) |
93 | 3, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑀 − 1) ∈
ℕ0) |
94 | | expcl 13482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℂ ∧ (𝑀 − 1) ∈
ℕ0) → (𝑥↑(𝑀 − 1)) ∈
ℂ) |
95 | 93, 94 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝜑) → (𝑥↑(𝑀 − 1)) ∈
ℂ) |
96 | 95 | ancoms 463 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑥↑(𝑀 − 1)) ∈
ℂ) |
97 | 6, 96 | sylan2 596 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → (𝑥↑(𝑀 − 1)) ∈
ℂ) |
98 | 51, 97 | mulcld 10684 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → (𝑀 · (𝑥↑(𝑀 − 1))) ∈
ℂ) |
99 | 20 | nnnn0d 11979 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑁 − 𝑀) ∈
ℕ0) |
100 | 99 | adantr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑁 − 𝑀) ∈
ℕ0) |
101 | 14, 100 | expcld 13545 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((1 − 𝑥)↑(𝑁 − 𝑀)) ∈ ℂ) |
102 | 6, 101 | sylan2 596 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((1 − 𝑥)↑(𝑁 − 𝑀)) ∈ ℂ) |
103 | 98, 102 | mulcld 10684 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) ∈ ℂ) |
104 | 70, 74 | mulcncf 24131 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑀 · (𝑥↑(𝑀 − 1)))) ∈ (ℂ–cn→ℂ)) |
105 | 104, 65 | mulcncf 24131 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) ∈ (ℂ–cn→ℂ)) |
106 | 105 | resclunitintvd 39579 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) ∈ ((0[,]1)–cn→ℂ)) |
107 | | cnicciblnc 24527 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑥 ∈ (0[,]1) ↦ ((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) ∈ ((0[,]1)–cn→ℂ)) → (𝑥 ∈ (0[,]1) ↦ ((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) ∈
𝐿1) |
108 | 27, 28, 106, 107 | syl3anc 1369 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) ∈
𝐿1) |
109 | 84, 86, 103, 108 | iblss 24489 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ ((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) ∈
𝐿1) |
110 | | dvexp 24637 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑𝑀))) = (𝑥 ∈ ℂ ↦ (𝑀 · (𝑥↑(𝑀 − 1))))) |
111 | 3, 110 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑𝑀))) = (𝑥 ∈ ℂ ↦ (𝑀 · (𝑥↑(𝑀 − 1))))) |
112 | 44, 96 | mulcld 10684 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑀 · (𝑥↑(𝑀 − 1))) ∈
ℂ) |
113 | 111, 10, 112 | resdvopclptsd 39580 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]1) ↦ (𝑥↑𝑀))) = (𝑥 ∈ (0(,)1) ↦ (𝑀 · (𝑥↑(𝑀 − 1))))) |
114 | 3, 1, 15 | lcmineqlem8 39588 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((1
− 𝑥)↑(𝑁 − 𝑀)))) = (𝑥 ∈ ℂ ↦ (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) |
115 | 46, 24 | mulcld 10684 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) ∈
ℂ) |
116 | 114, 101,
115 | resdvopclptsd 39580 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]1) ↦ ((1
− 𝑥)↑(𝑁 − 𝑀)))) = (𝑥 ∈ (0(,)1) ↦ (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) |
117 | | oveq1 7150 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 0 → (𝑥↑𝑀) = (0↑𝑀)) |
118 | 117 | adantl 486 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑥↑𝑀) = (0↑𝑀)) |
119 | 3 | 0expd 13538 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (0↑𝑀) = 0) |
120 | 119 | adantr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 = 0) → (0↑𝑀) = 0) |
121 | 118, 120 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑥↑𝑀) = 0) |
122 | 121 | oveq1d 7158 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 = 0) → ((𝑥↑𝑀) · ((1 − 𝑥)↑(𝑁 − 𝑀))) = (0 · ((1 − 𝑥)↑(𝑁 − 𝑀)))) |
123 | | 0cn 10656 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℂ |
124 | | eleq1 2838 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 0 → (𝑥 ∈ ℂ ↔ 0 ∈
ℂ)) |
125 | 123, 124 | mpbiri 261 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → 𝑥 ∈ ℂ) |
126 | 101 | mul02d 10861 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (0 · ((1
− 𝑥)↑(𝑁 − 𝑀))) = 0) |
127 | 125, 126 | sylan2 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 = 0) → (0 · ((1 − 𝑥)↑(𝑁 − 𝑀))) = 0) |
128 | 122, 127 | eqtrd 2794 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 = 0) → ((𝑥↑𝑀) · ((1 − 𝑥)↑(𝑁 − 𝑀))) = 0) |
129 | | oveq2 7151 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 1 → (1 − 𝑥) = (1 −
1)) |
130 | | 1m1e0 11731 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1
− 1) = 0 |
131 | 129, 130 | eqtrdi 2810 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 1 → (1 − 𝑥) = 0) |
132 | 131 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 1 → ((1 − 𝑥)↑(𝑁 − 𝑀)) = (0↑(𝑁 − 𝑀))) |
133 | 132 | adantl 486 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 = 1) → ((1 − 𝑥)↑(𝑁 − 𝑀)) = (0↑(𝑁 − 𝑀))) |
134 | 20 | 0expd 13538 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (0↑(𝑁 − 𝑀)) = 0) |
135 | 134 | adantr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 = 1) → (0↑(𝑁 − 𝑀)) = 0) |
136 | 133, 135 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 = 1) → ((1 − 𝑥)↑(𝑁 − 𝑀)) = 0) |
137 | 136 | oveq2d 7159 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 = 1) → ((𝑥↑𝑀) · ((1 − 𝑥)↑(𝑁 − 𝑀))) = ((𝑥↑𝑀) · 0)) |
138 | | ax-1cn 10618 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
139 | | eleq1 2838 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 1 → (𝑥 ∈ ℂ ↔ 1 ∈
ℂ)) |
140 | 138, 139 | mpbiri 261 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 1 → 𝑥 ∈ ℂ) |
141 | 10 | mul01d 10862 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑥↑𝑀) · 0) = 0) |
142 | 140, 141 | sylan2 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 = 1) → ((𝑥↑𝑀) · 0) = 0) |
143 | 137, 142 | eqtrd 2794 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 = 1) → ((𝑥↑𝑀) · ((1 − 𝑥)↑(𝑁 − 𝑀))) = 0) |
144 | 27, 28, 58, 59, 66, 76, 82, 92, 109, 113, 116, 128, 143 | itgparts 24731 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∫(0(,)1)((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) d𝑥 = ((0 − 0) − ∫(0(,)1)((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |
145 | 56, 144 | eqtr3d 2796 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∫(0[,]1)((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) d𝑥 = ((0 − 0) − ∫(0(,)1)((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |
146 | 27, 28, 103 | itgioo 24500 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∫(0(,)1)((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 = ∫(0[,]1)((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) |
147 | 146 | oveq2d 7159 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((0 − 0) −
∫(0(,)1)((𝑀 ·
(𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) = ((0 − 0) −
∫(0[,]1)((𝑀 ·
(𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |
148 | 145, 147 | eqtrd 2794 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∫(0[,]1)((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) d𝑥 = ((0 − 0) − ∫(0[,]1)((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |
149 | | 0m0e0 11779 |
. . . . . . . . . . . . . 14
⊢ (0
− 0) = 0 |
150 | 149 | oveq1i 7153 |
. . . . . . . . . . . . 13
⊢ ((0
− 0) − ∫(0[,]1)((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) = (0 − ∫(0[,]1)((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) |
151 | 148, 150 | eqtrdi 2810 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∫(0[,]1)((𝑥↑𝑀) · (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) d𝑥 = (0 − ∫(0[,]1)((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |
152 | 49, 151 | eqtr3d 2796 |
. . . . . . . . . . 11
⊢ (𝜑 → ∫(0[,]1)(-(𝑁 − 𝑀) · ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)))) d𝑥 = (0 − ∫(0[,]1)((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |
153 | 42, 152 | eqtrd 2794 |
. . . . . . . . . 10
⊢ (𝜑 → (-(𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) = (0 − ∫(0[,]1)((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |
154 | 44, 96, 101 | mulassd 10687 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) = (𝑀 · ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))))) |
155 | 6, 154 | sylan2 596 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) = (𝑀 · ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))))) |
156 | 155 | itgeq2dv 24466 |
. . . . . . . . . . 11
⊢ (𝜑 → ∫(0[,]1)((𝑀 · (𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 = ∫(0[,]1)(𝑀 · ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) d𝑥) |
157 | 156 | oveq2d 7159 |
. . . . . . . . . 10
⊢ (𝜑 → (0 −
∫(0[,]1)((𝑀 ·
(𝑥↑(𝑀 − 1))) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) = (0 − ∫(0[,]1)(𝑀 · ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) d𝑥)) |
158 | 153, 157 | eqtrd 2794 |
. . . . . . . . 9
⊢ (𝜑 → (-(𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) = (0 − ∫(0[,]1)(𝑀 · ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) d𝑥)) |
159 | 97, 102 | mulcld 10684 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) ∈ ℂ) |
160 | 74, 65 | mulcncf 24131 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) ∈ (ℂ–cn→ℂ)) |
161 | 160 | resclunitintvd 39579 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) ∈ ((0[,]1)–cn→ℂ)) |
162 | | cnicciblnc 24527 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑥 ∈ (0[,]1) ↦ ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) ∈ ((0[,]1)–cn→ℂ)) → (𝑥 ∈ (0[,]1) ↦ ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) ∈
𝐿1) |
163 | 27, 28, 161, 162 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) ∈
𝐿1) |
164 | 4, 159, 163 | itgmulc2 24518 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) = ∫(0[,]1)(𝑀 · ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) d𝑥) |
165 | 164 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝜑 → (0 − (𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) = (0 − ∫(0[,]1)(𝑀 · ((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀)))) d𝑥)) |
166 | 158, 165 | eqtr4d 2797 |
. . . . . . . 8
⊢ (𝜑 → (-(𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) = (0 − (𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥))) |
167 | | df-neg 10896 |
. . . . . . . 8
⊢ -(𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) = (0 − (𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |
168 | 166, 167 | eqtr4di 2812 |
. . . . . . 7
⊢ (𝜑 → (-(𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) = -(𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |
169 | 40, 168 | eqtr3d 2796 |
. . . . . 6
⊢ (𝜑 → -((𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) = -(𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |
170 | 5, 39 | mulcld 10684 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) ∈ ℂ) |
171 | 159, 163 | itgcl 24468 |
. . . . . . . 8
⊢ (𝜑 → ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 ∈ ℂ) |
172 | 4, 171 | mulcld 10684 |
. . . . . . 7
⊢ (𝜑 → (𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) ∈ ℂ) |
173 | 170, 172 | neg11ad 11016 |
. . . . . 6
⊢ (𝜑 → (-((𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) = -(𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) ↔ ((𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) = (𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥))) |
174 | 169, 173 | mpbid 235 |
. . . . 5
⊢ (𝜑 → ((𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) = (𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |
175 | 20 | nnne0d 11709 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 𝑀) ≠ 0) |
176 | 172, 5, 39, 175 | divmuld 11461 |
. . . . 5
⊢ (𝜑 → (((𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) / (𝑁 − 𝑀)) = ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥 ↔ ((𝑁 − 𝑀) · ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) = (𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥))) |
177 | 174, 176 | mpbird 260 |
. . . 4
⊢ (𝜑 → ((𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) / (𝑁 − 𝑀)) = ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥) |
178 | 138 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
179 | 4, 178 | pncand 11021 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) |
180 | 179 | eqcomd 2765 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 = ((𝑀 + 1) − 1)) |
181 | 180 | oveq2d 7159 |
. . . . . . 7
⊢ (𝜑 → (𝑥↑𝑀) = (𝑥↑((𝑀 + 1) − 1))) |
182 | 2, 4, 178 | subsub4d 11051 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 𝑀) − 1) = (𝑁 − (𝑀 + 1))) |
183 | 182 | oveq2d 7159 |
. . . . . . 7
⊢ (𝜑 → ((1 − 𝑥)↑((𝑁 − 𝑀) − 1)) = ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) |
184 | 181, 183 | oveq12d 7161 |
. . . . . 6
⊢ (𝜑 → ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) = ((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1))))) |
185 | 184 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) = ((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1))))) |
186 | 185 | itgeq2dv 24466 |
. . . 4
⊢ (𝜑 → ∫(0[,]1)((𝑥↑𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))) d𝑥 = ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥) |
187 | 177, 186 | eqtrd 2794 |
. . 3
⊢ (𝜑 → ((𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) / (𝑁 − 𝑀)) = ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥) |
188 | 187 | eqcomd 2765 |
. 2
⊢ (𝜑 → ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥 = ((𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) / (𝑁 − 𝑀))) |
189 | 4, 171, 5, 175 | div23d 11476 |
. 2
⊢ (𝜑 → ((𝑀 · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥) / (𝑁 − 𝑀)) = ((𝑀 / (𝑁 − 𝑀)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |
190 | 188, 189 | eqtrd 2794 |
1
⊢ (𝜑 → ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥 = ((𝑀 / (𝑁 − 𝑀)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) |