| Step | Hyp | Ref
| Expression |
| 1 | | elunitcn 13508 |
. . . 4
⊢ (𝑡 ∈ (0[,]1) → 𝑡 ∈
ℂ) |
| 2 | | 1m1e0 12338 |
. . . . . . . 8
⊢ (1
− 1) = 0 |
| 3 | 2 | oveq2i 7442 |
. . . . . . 7
⊢ (𝑡↑(1 − 1)) = (𝑡↑0) |
| 4 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → 𝑡 ∈ ℂ) |
| 5 | 4 | exp0d 14180 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (𝑡↑0) = 1) |
| 6 | 3, 5 | eqtrid 2789 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (𝑡↑(1 − 1)) = 1) |
| 7 | 6 | oveq1d 7446 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → ((𝑡↑(1 − 1)) · ((1 −
𝑡)↑(𝑁 − 1))) = (1 · ((1 −
𝑡)↑(𝑁 − 1)))) |
| 8 | | 1cnd 11256 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → 1 ∈
ℂ) |
| 9 | 8, 4 | subcld 11620 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈
ℂ) |
| 10 | | lcmineqlem12.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 11 | | nnm1nn0 12567 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
| 12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
| 13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (𝑁 − 1) ∈
ℕ0) |
| 14 | 9, 13 | expcld 14186 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → ((1 − 𝑡)↑(𝑁 − 1)) ∈
ℂ) |
| 15 | 14 | mullidd 11279 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → (1 · ((1
− 𝑡)↑(𝑁 − 1))) = ((1 −
𝑡)↑(𝑁 − 1))) |
| 16 | 7, 15 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ℂ) → ((𝑡↑(1 − 1)) · ((1 −
𝑡)↑(𝑁 − 1))) = ((1 − 𝑡)↑(𝑁 − 1))) |
| 17 | 1, 16 | sylan2 593 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((𝑡↑(1 − 1)) · ((1 −
𝑡)↑(𝑁 − 1))) = ((1 − 𝑡)↑(𝑁 − 1))) |
| 18 | 17 | itgeq2dv 25817 |
. 2
⊢ (𝜑 → ∫(0[,]1)((𝑡↑(1 − 1)) ·
((1 − 𝑡)↑(𝑁 − 1))) d𝑡 = ∫(0[,]1)((1 − 𝑡)↑(𝑁 − 1)) d𝑡) |
| 19 | | 0red 11264 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℝ) |
| 20 | | 1red 11262 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
| 21 | 1, 14 | sylan2 593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((1 − 𝑡)↑(𝑁 − 1)) ∈
ℂ) |
| 22 | 19, 20, 21 | itgioo 25851 |
. . . 4
⊢ (𝜑 → ∫(0(,)1)((1 −
𝑡)↑(𝑁 − 1)) d𝑡 = ∫(0[,]1)((1 − 𝑡)↑(𝑁 − 1)) d𝑡) |
| 23 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑(𝑁 − 1))) = (𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑(𝑁 − 1)))) |
| 24 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑡 → (1 − 𝑥) = (1 − 𝑡)) |
| 25 | 24 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑥 = 𝑡 → ((1 − 𝑥)↑(𝑁 − 1)) = ((1 − 𝑡)↑(𝑁 − 1))) |
| 26 | 25 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑡) → ((1 − 𝑥)↑(𝑁 − 1)) = ((1 − 𝑡)↑(𝑁 − 1))) |
| 27 | 26 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑥 = 𝑡) → ((1 − 𝑥)↑(𝑁 − 1)) = ((1 − 𝑡)↑(𝑁 − 1))) |
| 28 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0(,)1)) |
| 29 | | 1cnd 11256 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 1 ∈
ℂ) |
| 30 | | elioore 13417 |
. . . . . . . . . 10
⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈
ℝ) |
| 31 | | recn 11245 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℝ → 𝑡 ∈
ℂ) |
| 32 | 28, 30, 31 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ) |
| 33 | 29, 32 | subcld 11620 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈
ℂ) |
| 34 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 − 1) ∈
ℕ0) |
| 35 | 33, 34 | expcld 14186 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡)↑(𝑁 − 1)) ∈
ℂ) |
| 36 | 23, 27, 28, 35 | fvmptd 7023 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑(𝑁 − 1)))‘𝑡) = ((1 − 𝑡)↑(𝑁 − 1))) |
| 37 | 36 | itgeq2dv 25817 |
. . . . 5
⊢ (𝜑 → ∫(0(,)1)((𝑥 ∈ (0(,)1) ↦ ((1
− 𝑥)↑(𝑁 − 1)))‘𝑡) d𝑡 = ∫(0(,)1)((1 − 𝑡)↑(𝑁 − 1)) d𝑡) |
| 38 | | cnelprrecn 11248 |
. . . . . . . . . . . . 13
⊢ ℂ
∈ {ℝ, ℂ} |
| 39 | 38 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
| 40 | | 1cnd 11256 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 1 ∈
ℂ) |
| 41 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) |
| 42 | 40, 41 | subcld 11620 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (1 − 𝑥) ∈
ℂ) |
| 43 | | nnnn0 12533 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 44 | 10, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑁 ∈
ℕ0) |
| 46 | 42, 45 | expcld 14186 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((1 − 𝑥)↑𝑁) ∈ ℂ) |
| 47 | 45 | nn0cnd 12589 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑁 ∈ ℂ) |
| 48 | 12 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑁 − 1) ∈
ℕ0) |
| 49 | 42, 48 | expcld 14186 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((1 − 𝑥)↑(𝑁 − 1)) ∈
ℂ) |
| 50 | 47, 49 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑁 · ((1 − 𝑥)↑(𝑁 − 1))) ∈
ℂ) |
| 51 | 40 | negcld 11607 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → -1 ∈
ℂ) |
| 52 | 50, 51 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑁 · ((1 − 𝑥)↑(𝑁 − 1))) · -1) ∈
ℂ) |
| 53 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ) |
| 54 | 44 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑁 ∈
ℕ0) |
| 55 | 53, 54 | expcld 14186 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦↑𝑁) ∈ ℂ) |
| 56 | 54 | nn0cnd 12589 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑁 ∈ ℂ) |
| 57 | 12 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑁 − 1) ∈
ℕ0) |
| 58 | 53, 57 | expcld 14186 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦↑(𝑁 − 1)) ∈
ℂ) |
| 59 | 56, 58 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑁 · (𝑦↑(𝑁 − 1))) ∈
ℂ) |
| 60 | | 0cnd 11254 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 0 ∈
ℂ) |
| 61 | | 1cnd 11256 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℂ) |
| 62 | 39, 61 | dvmptc 25996 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 1)) =
(𝑥 ∈ ℂ ↦
0)) |
| 63 | 39 | dvmptid 25995 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1)) |
| 64 | 39, 40, 60, 62, 41, 40, 63 | dvmptsub 26005 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (1
− 𝑥))) = (𝑥 ∈ ℂ ↦ (0
− 1))) |
| 65 | | df-neg 11495 |
. . . . . . . . . . . . . . . 16
⊢ -1 = (0
− 1) |
| 66 | 65 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → -1 = (0 −
1)) |
| 67 | 66 | mpteq2dv 5244 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ -1) = (𝑥 ∈ ℂ ↦ (0
− 1))) |
| 68 | 64, 67 | eqtr4d 2780 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (1
− 𝑥))) = (𝑥 ∈ ℂ ↦
-1)) |
| 69 | | dvexp 25991 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑𝑁))) = (𝑦 ∈ ℂ ↦ (𝑁 · (𝑦↑(𝑁 − 1))))) |
| 70 | 10, 69 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑𝑁))) = (𝑦 ∈ ℂ ↦ (𝑁 · (𝑦↑(𝑁 − 1))))) |
| 71 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (1 − 𝑥) → (𝑦↑𝑁) = ((1 − 𝑥)↑𝑁)) |
| 72 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (1 − 𝑥) → (𝑦↑(𝑁 − 1)) = ((1 − 𝑥)↑(𝑁 − 1))) |
| 73 | 72 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (1 − 𝑥) → (𝑁 · (𝑦↑(𝑁 − 1))) = (𝑁 · ((1 − 𝑥)↑(𝑁 − 1)))) |
| 74 | 39, 39, 42, 51, 55, 59, 68, 70, 71, 73 | dvmptco 26010 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((1
− 𝑥)↑𝑁))) = (𝑥 ∈ ℂ ↦ ((𝑁 · ((1 − 𝑥)↑(𝑁 − 1))) ·
-1))) |
| 75 | 61 | negcld 11607 |
. . . . . . . . . . . . 13
⊢ (𝜑 → -1 ∈
ℂ) |
| 76 | 10 | nncnd 12282 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 77 | 10 | nnne0d 12316 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ≠ 0) |
| 78 | 75, 76, 77 | divcld 12043 |
. . . . . . . . . . . 12
⊢ (𝜑 → (-1 / 𝑁) ∈ ℂ) |
| 79 | 39, 46, 52, 74, 78 | dvmptcmul 26002 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((-1 /
𝑁) · ((1 −
𝑥)↑𝑁)))) = (𝑥 ∈ ℂ ↦ ((-1 / 𝑁) · ((𝑁 · ((1 − 𝑥)↑(𝑁 − 1))) ·
-1)))) |
| 80 | 78 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (-1 / 𝑁) ∈
ℂ) |
| 81 | 80, 50, 51 | mulassd 11284 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((-1 / 𝑁) · (𝑁 · ((1 − 𝑥)↑(𝑁 − 1)))) · -1) = ((-1 / 𝑁) · ((𝑁 · ((1 − 𝑥)↑(𝑁 − 1))) ·
-1))) |
| 82 | 81 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((-1 / 𝑁) · ((𝑁 · ((1 − 𝑥)↑(𝑁 − 1))) · -1)) = (((-1 / 𝑁) · (𝑁 · ((1 − 𝑥)↑(𝑁 − 1)))) ·
-1)) |
| 83 | 80, 47, 49 | mulassd 11284 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((-1 / 𝑁) · 𝑁) · ((1 − 𝑥)↑(𝑁 − 1))) = ((-1 / 𝑁) · (𝑁 · ((1 − 𝑥)↑(𝑁 − 1))))) |
| 84 | 83 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((((-1 / 𝑁) · 𝑁) · ((1 − 𝑥)↑(𝑁 − 1))) · -1) = (((-1 / 𝑁) · (𝑁 · ((1 − 𝑥)↑(𝑁 − 1)))) ·
-1)) |
| 85 | 84 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((-1 / 𝑁) · (𝑁 · ((1 − 𝑥)↑(𝑁 − 1)))) · -1) = ((((-1 / 𝑁) · 𝑁) · ((1 − 𝑥)↑(𝑁 − 1))) · -1)) |
| 86 | 82, 85 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((-1 / 𝑁) · ((𝑁 · ((1 − 𝑥)↑(𝑁 − 1))) · -1)) = ((((-1 / 𝑁) · 𝑁) · ((1 − 𝑥)↑(𝑁 − 1))) · -1)) |
| 87 | 77 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑁 ≠ 0) |
| 88 | 51, 47, 87 | divcan1d 12044 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((-1 / 𝑁) · 𝑁) = -1) |
| 89 | 88 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((-1 / 𝑁) · 𝑁) · ((1 − 𝑥)↑(𝑁 − 1))) = (-1 · ((1 −
𝑥)↑(𝑁 − 1)))) |
| 90 | 89 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((((-1 / 𝑁) · 𝑁) · ((1 − 𝑥)↑(𝑁 − 1))) · -1) = ((-1 ·
((1 − 𝑥)↑(𝑁 − 1))) ·
-1)) |
| 91 | 86, 90 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((-1 / 𝑁) · ((𝑁 · ((1 − 𝑥)↑(𝑁 − 1))) · -1)) = ((-1 ·
((1 − 𝑥)↑(𝑁 − 1))) ·
-1)) |
| 92 | 51, 51, 49 | mul32d 11471 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((-1 · -1)
· ((1 − 𝑥)↑(𝑁 − 1))) = ((-1 · ((1 −
𝑥)↑(𝑁 − 1))) · -1)) |
| 93 | 92 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((-1 · ((1
− 𝑥)↑(𝑁 − 1))) · -1) =
((-1 · -1) · ((1 − 𝑥)↑(𝑁 − 1)))) |
| 94 | 91, 93 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((-1 / 𝑁) · ((𝑁 · ((1 − 𝑥)↑(𝑁 − 1))) · -1)) = ((-1 ·
-1) · ((1 − 𝑥)↑(𝑁 − 1)))) |
| 95 | 40, 40 | mul2negd 11718 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (-1 · -1) = (1
· 1)) |
| 96 | | 1t1e1 12428 |
. . . . . . . . . . . . . . . 16
⊢ (1
· 1) = 1 |
| 97 | 95, 96 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (-1 · -1) =
1) |
| 98 | 97 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((-1 · -1)
· ((1 − 𝑥)↑(𝑁 − 1))) = (1 · ((1 −
𝑥)↑(𝑁 − 1)))) |
| 99 | 49 | mullidd 11279 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (1 · ((1
− 𝑥)↑(𝑁 − 1))) = ((1 −
𝑥)↑(𝑁 − 1))) |
| 100 | 98, 99 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((-1 · -1)
· ((1 − 𝑥)↑(𝑁 − 1))) = ((1 − 𝑥)↑(𝑁 − 1))) |
| 101 | 94, 100 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((-1 / 𝑁) · ((𝑁 · ((1 − 𝑥)↑(𝑁 − 1))) · -1)) = ((1 −
𝑥)↑(𝑁 − 1))) |
| 102 | 101 | mpteq2dva 5242 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((-1 / 𝑁) · ((𝑁 · ((1 − 𝑥)↑(𝑁 − 1))) · -1))) = (𝑥 ∈ ℂ ↦ ((1
− 𝑥)↑(𝑁 − 1)))) |
| 103 | 79, 102 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((-1 /
𝑁) · ((1 −
𝑥)↑𝑁)))) = (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 1)))) |
| 104 | 80, 46 | mulcld 11281 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁)) ∈ ℂ) |
| 105 | 103, 104,
49 | resdvopclptsd 42029 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]1) ↦ ((-1 /
𝑁) · ((1 −
𝑥)↑𝑁)))) = (𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑(𝑁 − 1)))) |
| 106 | 105 | fveq1d 6908 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (0[,]1) ↦ ((-1 /
𝑁) · ((1 −
𝑥)↑𝑁))))‘𝑡) = ((𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑(𝑁 − 1)))‘𝑡)) |
| 107 | 106 | ralrimivw 3150 |
. . . . . . 7
⊢ (𝜑 → ∀𝑡 ∈ (0(,)1)((ℝ D (𝑥 ∈ (0[,]1) ↦ ((-1 /
𝑁) · ((1 −
𝑥)↑𝑁))))‘𝑡) = ((𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑(𝑁 − 1)))‘𝑡)) |
| 108 | | itgeq2 25813 |
. . . . . . 7
⊢
(∀𝑡 ∈
(0(,)1)((ℝ D (𝑥
∈ (0[,]1) ↦ ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁))))‘𝑡) = ((𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑(𝑁 − 1)))‘𝑡) → ∫(0(,)1)((ℝ D (𝑥 ∈ (0[,]1) ↦ ((-1 /
𝑁) · ((1 −
𝑥)↑𝑁))))‘𝑡) d𝑡 = ∫(0(,)1)((𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑(𝑁 − 1)))‘𝑡) d𝑡) |
| 109 | 107, 108 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∫(0(,)1)((ℝ D
(𝑥 ∈ (0[,]1) ↦
((-1 / 𝑁) · ((1
− 𝑥)↑𝑁))))‘𝑡) d𝑡 = ∫(0(,)1)((𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑(𝑁 − 1)))‘𝑡) d𝑡) |
| 110 | | 0le1 11786 |
. . . . . . . . . 10
⊢ 0 ≤
1 |
| 111 | 110 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 1) |
| 112 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝜑 |
| 113 | | ax-1cn 11213 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
| 114 | | ssid 4006 |
. . . . . . . . . . . . . . 15
⊢ ℂ
⊆ ℂ |
| 115 | | cncfmptc 24938 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ)
→ (𝑥 ∈ ℂ
↦ 1) ∈ (ℂ–cn→ℂ)) |
| 116 | 113, 114,
114, 115 | mp3an 1463 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ ↦ 1)
∈ (ℂ–cn→ℂ) |
| 117 | 116 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 1) ∈
(ℂ–cn→ℂ)) |
| 118 | | cncfmptid 24939 |
. . . . . . . . . . . . . . 15
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ ℂ ↦ 𝑥) ∈ (ℂ–cn→ℂ)) |
| 119 | 114, 114,
118 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ ↦ 𝑥) ∈ (ℂ–cn→ℂ) |
| 120 | 119 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝑥) ∈ (ℂ–cn→ℂ)) |
| 121 | 117, 120 | subcncf 25479 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 − 𝑥)) ∈ (ℂ–cn→ℂ)) |
| 122 | | expcncf 24953 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈
ℕ0 → (𝑦 ∈ ℂ ↦ (𝑦↑(𝑁 − 1))) ∈ (ℂ–cn→ℂ)) |
| 123 | 12, 122 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑(𝑁 − 1))) ∈ (ℂ–cn→ℂ)) |
| 124 | | ssidd 4007 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ⊆
ℂ) |
| 125 | 112, 121,
123, 124, 72 | cncfcompt2 24934 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 1))) ∈ (ℂ–cn→ℂ)) |
| 126 | 125 | resopunitintvd 42027 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑(𝑁 − 1))) ∈ ((0(,)1)–cn→ℂ)) |
| 127 | 105 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (0[,]1) ↦ ((-1 /
𝑁) · ((1 −
𝑥)↑𝑁)))) ∈ ((0(,)1)–cn→ℂ) ↔ (𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑(𝑁 − 1))) ∈ ((0(,)1)–cn→ℂ))) |
| 128 | 126, 127 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]1) ↦ ((-1 /
𝑁) · ((1 −
𝑥)↑𝑁)))) ∈ ((0(,)1)–cn→ℂ)) |
| 129 | | ioossicc 13473 |
. . . . . . . . . . . 12
⊢ (0(,)1)
⊆ (0[,]1) |
| 130 | 129 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (0(,)1) ⊆
(0[,]1)) |
| 131 | | ioombl 25600 |
. . . . . . . . . . . 12
⊢ (0(,)1)
∈ dom vol |
| 132 | 131 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (0(,)1) ∈ dom
vol) |
| 133 | | elunitcn 13508 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈
ℂ) |
| 134 | 133, 49 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((1 − 𝑥)↑(𝑁 − 1)) ∈
ℂ) |
| 135 | 114 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ℂ ⊆
ℂ) |
| 136 | 112, 121,
123, 135, 72 | cncfcompt2 24934 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 1))) ∈ (ℂ–cn→ℂ)) |
| 137 | 136 | resclunitintvd 42028 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((1 − 𝑥)↑(𝑁 − 1))) ∈ ((0[,]1)–cn→ℂ)) |
| 138 | 19, 20, 137 | 3jca 1129 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ∈ ℝ ∧ 1
∈ ℝ ∧ (𝑥
∈ (0[,]1) ↦ ((1 − 𝑥)↑(𝑁 − 1))) ∈ ((0[,]1)–cn→ℂ))) |
| 139 | | cnicciblnc 25878 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑥 ∈ (0[,]1) ↦ ((1 − 𝑥)↑(𝑁 − 1))) ∈ ((0[,]1)–cn→ℂ)) → (𝑥 ∈ (0[,]1) ↦ ((1 − 𝑥)↑(𝑁 − 1))) ∈
𝐿1) |
| 140 | 138, 139 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((1 − 𝑥)↑(𝑁 − 1))) ∈
𝐿1) |
| 141 | 130, 132,
134, 140 | iblss 25840 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ ((1 − 𝑥)↑(𝑁 − 1))) ∈
𝐿1) |
| 142 | 105, 141 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]1) ↦ ((-1 /
𝑁) · ((1 −
𝑥)↑𝑁)))) ∈
𝐿1) |
| 143 | | cncfmptc 24938 |
. . . . . . . . . . . . 13
⊢ (((-1 /
𝑁) ∈ ℂ ∧
ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ ℂ ↦ (-1 /
𝑁)) ∈
(ℂ–cn→ℂ)) |
| 144 | 114, 114,
143 | mp3an23 1455 |
. . . . . . . . . . . 12
⊢ ((-1 /
𝑁) ∈ ℂ →
(𝑥 ∈ ℂ ↦
(-1 / 𝑁)) ∈
(ℂ–cn→ℂ)) |
| 145 | 78, 144 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (-1 / 𝑁)) ∈ (ℂ–cn→ℂ)) |
| 146 | 145 | resclunitintvd 42028 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ (-1 / 𝑁)) ∈ ((0[,]1)–cn→ℂ)) |
| 147 | | expcncf 24953 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑦 ∈ ℂ
↦ (𝑦↑𝑁)) ∈ (ℂ–cn→ℂ)) |
| 148 | 44, 147 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑𝑁)) ∈ (ℂ–cn→ℂ)) |
| 149 | 112, 121,
148, 124, 71 | cncfcompt2 24934 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑𝑁)) ∈ (ℂ–cn→ℂ)) |
| 150 | 149 | resclunitintvd 42028 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((1 − 𝑥)↑𝑁)) ∈ ((0[,]1)–cn→ℂ)) |
| 151 | 146, 150 | mulcncf 25480 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁))) ∈ ((0[,]1)–cn→ℂ)) |
| 152 | 19, 20, 111, 128, 142, 151 | ftc2 26085 |
. . . . . . . 8
⊢ (𝜑 → ∫(0(,)1)((ℝ D
(𝑥 ∈ (0[,]1) ↦
((-1 / 𝑁) · ((1
− 𝑥)↑𝑁))))‘𝑡) d𝑡 = (((𝑥 ∈ (0[,]1) ↦ ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁)))‘1) − ((𝑥 ∈ (0[,]1) ↦ ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁)))‘0))) |
| 153 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁))) = (𝑥 ∈ (0[,]1) ↦ ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁)))) |
| 154 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 = 1) → 𝑥 = 1) |
| 155 | 154 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 = 1) → (1 − 𝑥) = (1 − 1)) |
| 156 | 155, 2 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = 1) → (1 − 𝑥) = 0) |
| 157 | 156 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = 1) → ((1 − 𝑥)↑𝑁) = (0↑𝑁)) |
| 158 | | 0exp 14138 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ →
(0↑𝑁) =
0) |
| 159 | 10, 158 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0↑𝑁) = 0) |
| 160 | 159 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = 1) → (0↑𝑁) = 0) |
| 161 | 157, 160 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 = 1) → ((1 − 𝑥)↑𝑁) = 0) |
| 162 | 161 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 1) → ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁)) = ((-1 / 𝑁) · 0)) |
| 163 | 78 | mul01d 11460 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((-1 / 𝑁) · 0) = 0) |
| 164 | 163 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 1) → ((-1 / 𝑁) · 0) = 0) |
| 165 | 162, 164 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 1) → ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁)) = 0) |
| 166 | | 1elunit 13510 |
. . . . . . . . . . 11
⊢ 1 ∈
(0[,]1) |
| 167 | 166 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
(0[,]1)) |
| 168 | | 0cnd 11254 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℂ) |
| 169 | 153, 165,
167, 168 | fvmptd 7023 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ (0[,]1) ↦ ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁)))‘1) = 0) |
| 170 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 = 0) → 𝑥 = 0) |
| 171 | 170 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 = 0) → (1 − 𝑥) = (1 − 0)) |
| 172 | | 1m0e1 12387 |
. . . . . . . . . . . . . . 15
⊢ (1
− 0) = 1 |
| 173 | 171, 172 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = 0) → (1 − 𝑥) = 1) |
| 174 | 173 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = 0) → ((1 − 𝑥)↑𝑁) = (1↑𝑁)) |
| 175 | 44 | nn0zd 12639 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 176 | | 1exp 14132 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ →
(1↑𝑁) =
1) |
| 177 | 175, 176 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1↑𝑁) = 1) |
| 178 | 177 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = 0) → (1↑𝑁) = 1) |
| 179 | 174, 178 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 = 0) → ((1 − 𝑥)↑𝑁) = 1) |
| 180 | 179 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 0) → ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁)) = ((-1 / 𝑁) · 1)) |
| 181 | 78 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 = 0) → (-1 / 𝑁) ∈ ℂ) |
| 182 | 181 | mulridd 11278 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 0) → ((-1 / 𝑁) · 1) = (-1 / 𝑁)) |
| 183 | 180, 182 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 0) → ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁)) = (-1 / 𝑁)) |
| 184 | | 0elunit 13509 |
. . . . . . . . . . 11
⊢ 0 ∈
(0[,]1) |
| 185 | 184 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
(0[,]1)) |
| 186 | 153, 183,
185, 78 | fvmptd 7023 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ (0[,]1) ↦ ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁)))‘0) = (-1 / 𝑁)) |
| 187 | 169, 186 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝜑 → (((𝑥 ∈ (0[,]1) ↦ ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁)))‘1) − ((𝑥 ∈ (0[,]1) ↦ ((-1 / 𝑁) · ((1 − 𝑥)↑𝑁)))‘0)) = (0 − (-1 / 𝑁))) |
| 188 | 152, 187 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ∫(0(,)1)((ℝ D
(𝑥 ∈ (0[,]1) ↦
((-1 / 𝑁) · ((1
− 𝑥)↑𝑁))))‘𝑡) d𝑡 = (0 − (-1 / 𝑁))) |
| 189 | | df-neg 11495 |
. . . . . . . . . 10
⊢ --(1 /
𝑁) = (0 − -(1 / 𝑁)) |
| 190 | 189 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → --(1 / 𝑁) = (0 − -(1 / 𝑁))) |
| 191 | 61, 76, 77 | divnegd 12056 |
. . . . . . . . . 10
⊢ (𝜑 → -(1 / 𝑁) = (-1 / 𝑁)) |
| 192 | 191 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (0 − -(1 / 𝑁)) = (0 − (-1 / 𝑁))) |
| 193 | 190, 192 | eqtr2d 2778 |
. . . . . . . 8
⊢ (𝜑 → (0 − (-1 / 𝑁)) = --(1 / 𝑁)) |
| 194 | 76, 77 | reccld 12036 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 𝑁) ∈ ℂ) |
| 195 | 194 | negnegd 11611 |
. . . . . . . 8
⊢ (𝜑 → --(1 / 𝑁) = (1 / 𝑁)) |
| 196 | 193, 195 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → (0 − (-1 / 𝑁)) = (1 / 𝑁)) |
| 197 | 188, 196 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ∫(0(,)1)((ℝ D
(𝑥 ∈ (0[,]1) ↦
((-1 / 𝑁) · ((1
− 𝑥)↑𝑁))))‘𝑡) d𝑡 = (1 / 𝑁)) |
| 198 | 109, 197 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → ∫(0(,)1)((𝑥 ∈ (0(,)1) ↦ ((1
− 𝑥)↑(𝑁 − 1)))‘𝑡) d𝑡 = (1 / 𝑁)) |
| 199 | 37, 198 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → ∫(0(,)1)((1 −
𝑡)↑(𝑁 − 1)) d𝑡 = (1 / 𝑁)) |
| 200 | 22, 199 | eqtr3d 2779 |
. . 3
⊢ (𝜑 → ∫(0[,]1)((1 −
𝑡)↑(𝑁 − 1)) d𝑡 = (1 / 𝑁)) |
| 201 | | bcn1 14352 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁C1) = 𝑁) |
| 202 | 44, 201 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑁C1) = 𝑁) |
| 203 | 202 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (1 · (𝑁C1)) = (1 · 𝑁)) |
| 204 | 76 | mullidd 11279 |
. . . . 5
⊢ (𝜑 → (1 · 𝑁) = 𝑁) |
| 205 | 203, 204 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (1 · (𝑁C1)) = 𝑁) |
| 206 | 205 | oveq2d 7447 |
. . 3
⊢ (𝜑 → (1 / (1 · (𝑁C1))) = (1 / 𝑁)) |
| 207 | 200, 206 | eqtr4d 2780 |
. 2
⊢ (𝜑 → ∫(0[,]1)((1 −
𝑡)↑(𝑁 − 1)) d𝑡 = (1 / (1 · (𝑁C1)))) |
| 208 | 18, 207 | eqtrd 2777 |
1
⊢ (𝜑 → ∫(0[,]1)((𝑡↑(1 − 1)) ·
((1 − 𝑡)↑(𝑁 − 1))) d𝑡 = (1 / (1 · (𝑁C1)))) |