Metamath Proof Explorer

Theorem lcmineqlem12

Description: Base case for induction. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypothesis lcmineqlem12.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion lcmineqlem12 ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑡 ↑ ( 1 − 1 ) ) · ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) ) d 𝑡 = ( 1 / ( 1 · ( 𝑁 C 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem12.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 elunitcn ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) → 𝑡 ∈ ℂ )
3 1m1e0 ⊢ ( 1 − 1 ) = 0
4 3 oveq2i ⊢ ( 𝑡 ↑ ( 1 − 1 ) ) = ( 𝑡 ↑ 0 )
5 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → 𝑡 ∈ ℂ )
6 5 exp0d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 𝑡 ↑ 0 ) = 1 )
7 4 6 eqtrid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 𝑡 ↑ ( 1 − 1 ) ) = 1 )
8 7 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( ( 𝑡 ↑ ( 1 − 1 ) ) · ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) ) = ( 1 · ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) ) )
9 1cnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → 1 ∈ ℂ )
10 9 5 subcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 1 − 𝑡 ) ∈ ℂ )
11 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
12 1 11 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ℕ0 )
14 10 13 expcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
15 14 mullidd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 1 · ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) ) = ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) )
16 8 15 eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( ( 𝑡 ↑ ( 1 − 1 ) ) · ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) ) = ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) )
17 2 16 sylan2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 ↑ ( 1 − 1 ) ) · ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) ) = ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) )
18 17 itgeq2dv ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑡 ↑ ( 1 − 1 ) ) · ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) ) d 𝑡 = ∫ ( 0 [,] 1 ) ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) d 𝑡 )
19 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
20 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
21 2 14 sylan2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
22 19 20 21 itgioo ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) d 𝑡 = ∫ ( 0 [,] 1 ) ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) d 𝑡 )
23 eqidd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) = ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
24 oveq2 ⊢ ( 𝑥 = 𝑡 → ( 1 − 𝑥 ) = ( 1 − 𝑡 ) )
25 24 oveq1d ⊢ ( 𝑥 = 𝑡 → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) = ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑡 ) → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) = ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) )
27 26 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) ∧ 𝑥 = 𝑡 ) → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) = ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) )
28 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ( 0 (,) 1 ) )
29 1cnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 1 ∈ ℂ )
30 elioore ⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → 𝑡 ∈ ℝ )
31 recn ⊢ ( 𝑡 ∈ ℝ → 𝑡 ∈ ℂ )
32 28 30 31 3syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ℂ )
33 29 32 subcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 − 𝑡 ) ∈ ℂ )
34 12 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 − 1 ) ∈ ℕ0 )
35 33 34 expcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
36 23 27 28 35 fvmptd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ‘ 𝑡 ) = ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) )
37 36 itgeq2dv ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ‘ 𝑡 ) d 𝑡 = ∫ ( 0 (,) 1 ) ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) d 𝑡 )
38 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
39 38 a1i ⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
40 1cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℂ )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
42 40 41 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 1 − 𝑥 ) ∈ ℂ )
43 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
44 1 43 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
46 42 45 expcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 1 − 𝑥 ) ↑ 𝑁 ) ∈ ℂ )
47 45 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑁 ∈ ℂ )
48 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ℕ0 )
49 42 48 expcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
50 47 49 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ℂ )
51 40 negcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → - 1 ∈ ℂ )
52 50 51 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) ∈ ℂ )
53 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
54 44 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
55 53 54 expcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ 𝑁 ) ∈ ℂ )
56 54 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑁 ∈ ℂ )
57 12 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ℕ0 )
58 53 57 expcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
59 56 58 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑁 · ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) ∈ ℂ )
60 0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 0 ∈ ℂ )
61 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
62 39 61 dvmptc ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ 1 ) ) = ( 𝑥 ∈ ℂ ↦ 0 ) )
63 39 dvmptid ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ 1 ) )
64 39 40 60 62 41 40 63 dvmptsub ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 0 − 1 ) ) )
65 df-neg ⊢ - 1 = ( 0 − 1 )
66 65 a1i ⊢ ( 𝜑 → - 1 = ( 0 − 1 ) )
67 66 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ - 1 ) = ( 𝑥 ∈ ℂ ↦ ( 0 − 1 ) ) )
68 64 67 eqtr4d ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ - 1 ) )
69 dvexp ⊢ ( 𝑁 ∈ ℕ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑁 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑁 · ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) ) )
70 1 69 syl ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑁 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑁 · ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) ) )
71 oveq1 ⊢ ( 𝑦 = ( 1 − 𝑥 ) → ( 𝑦 ↑ 𝑁 ) = ( ( 1 − 𝑥 ) ↑ 𝑁 ) )
72 oveq1 ⊢ ( 𝑦 = ( 1 − 𝑥 ) → ( 𝑦 ↑ ( 𝑁 − 1 ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
73 72 oveq2d ⊢ ( 𝑦 = ( 1 − 𝑥 ) → ( 𝑁 · ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) = ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
74 39 39 42 51 55 59 68 70 71 73 dvmptco ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) ) )
75 61 negcld ⊢ ( 𝜑 → - 1 ∈ ℂ )
76 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
77 1 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
78 75 76 77 divcld ⊢ ( 𝜑 → ( - 1 / 𝑁 ) ∈ ℂ )
79 39 46 52 74 78 dvmptcmul ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( - 1 / 𝑁 ) · ( ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) ) ) )
80 78 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( - 1 / 𝑁 ) ∈ ℂ )
81 80 50 51 mulassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( - 1 / 𝑁 ) · ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) · - 1 ) = ( ( - 1 / 𝑁 ) · ( ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) ) )
82 81 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( - 1 / 𝑁 ) · ( ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) ) = ( ( ( - 1 / 𝑁 ) · ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) · - 1 ) )
83 80 47 49 mulassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( - 1 / 𝑁 ) · 𝑁 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) = ( ( - 1 / 𝑁 ) · ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) )
84 83 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( ( - 1 / 𝑁 ) · 𝑁 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) = ( ( ( - 1 / 𝑁 ) · ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) · - 1 ) )
85 84 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( - 1 / 𝑁 ) · ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) · - 1 ) = ( ( ( ( - 1 / 𝑁 ) · 𝑁 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) )
86 82 85 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( - 1 / 𝑁 ) · ( ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) ) = ( ( ( ( - 1 / 𝑁 ) · 𝑁 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) )
87 77 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑁 ≠ 0 )
88 51 47 87 divcan1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( - 1 / 𝑁 ) · 𝑁 ) = - 1 )
89 88 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( - 1 / 𝑁 ) · 𝑁 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) = ( - 1 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
90 89 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( ( - 1 / 𝑁 ) · 𝑁 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) = ( ( - 1 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) )
91 86 90 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( - 1 / 𝑁 ) · ( ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) ) = ( ( - 1 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) )
92 51 51 49 mul32d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( - 1 · - 1 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) = ( ( - 1 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) )
93 92 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( - 1 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) = ( ( - 1 · - 1 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
94 91 93 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( - 1 / 𝑁 ) · ( ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) ) = ( ( - 1 · - 1 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
95 40 40 mul2negd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( - 1 · - 1 ) = ( 1 · 1 ) )
96 1t1e1 ⊢ ( 1 · 1 ) = 1
97 95 96 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( - 1 · - 1 ) = 1 )
98 97 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( - 1 · - 1 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) = ( 1 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
99 49 mullidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 1 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
100 98 99 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( - 1 · - 1 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
101 94 100 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( - 1 / 𝑁 ) · ( ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
102 101 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( - 1 / 𝑁 ) · ( ( 𝑁 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · - 1 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
103 79 102 eqtrd ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
104 80 46 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ∈ ℂ )
105 103 104 49 resdvopclptsd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ) = ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
106 105 fveq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ) ‘ 𝑡 ) = ( ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ‘ 𝑡 ) )
107 106 ralrimivw ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 0 (,) 1 ) ( ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ) ‘ 𝑡 ) = ( ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ‘ 𝑡 ) )
108 itgeq2 ⊢ ( ∀ 𝑡 ∈ ( 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 ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ) ‘ 𝑡 ) d 𝑡 = ∫ ( 0 (,) 1 ) ( ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ‘ 𝑡 ) d 𝑡 )
110 0le1 ⊢ 0 ≤ 1
111 110 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
112 nfv ⊢ Ⅎ 𝑥 𝜑
113 ax-1cn ⊢ 1 ∈ ℂ
114 ssid ⊢ ℂ ⊆ ℂ
115 cncfmptc ⊢ ( ( 1 ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℂ ↦ 1 ) ∈ ( ℂ –cn→ ℂ ) )
116 113 114 114 115 mp3an ⊢ ( 𝑥 ∈ ℂ ↦ 1 ) ∈ ( ℂ –cn→ ℂ )
117 116 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 1 ) ∈ ( ℂ –cn→ ℂ ) )
118 cncfmptid ⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ℂ –cn→ ℂ ) )
119 114 114 118 mp2an ⊢ ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ℂ –cn→ ℂ )
120 119 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ℂ –cn→ ℂ ) )
121 117 120 subcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
122 expcncf ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
123 12 122 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
124 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
125 112 121 123 124 72 cncfcompt2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
126 125 resopunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) )
127 105 eleq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) ↔ ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) ) )
128 126 127 mpbird ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) )
129 ioossicc ⊢ ( 0 (,) 1 ) ⊆ ( 0 [,] 1 )
130 129 a1i ⊢ ( 𝜑 → ( 0 (,) 1 ) ⊆ ( 0 [,] 1 ) )
131 ioombl ⊢ ( 0 (,) 1 ) ∈ dom vol
132 131 a1i ⊢ ( 𝜑 → ( 0 (,) 1 ) ∈ dom vol )
133 elunitcn ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → 𝑥 ∈ ℂ )
134 133 49 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
135 114 a1i ⊢ ( 𝜑 → ℂ ⊆ ℂ )
136 112 121 123 135 72 cncfcompt2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
137 136 resclunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
138 19 20 137 3jca ⊢ ( 𝜑 → ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) )
139 cnicciblnc ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ 𝐿1 )
140 138 139 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ 𝐿1 )
141 130 132 134 140 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ 𝐿1 )
142 105 141 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ) ∈ 𝐿1 )
143 cncfmptc ⊢ ( ( ( - 1 / 𝑁 ) ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℂ ↦ ( - 1 / 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
144 114 114 143 mp3an23 ⊢ ( ( - 1 / 𝑁 ) ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( - 1 / 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
145 78 144 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( - 1 / 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
146 145 resclunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( - 1 / 𝑁 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
147 expcncf ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
148 44 147 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
149 112 121 148 124 71 cncfcompt2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
150 149 resclunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
151 146 150 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
152 19 20 111 128 142 151 ftc2 ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ) ‘ 𝑡 ) d 𝑡 = ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ‘ 1 ) − ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ‘ 0 ) ) )
153 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) )
154 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → 𝑥 = 1 )
155 154 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( 1 − 𝑥 ) = ( 1 − 1 ) )
156 155 3 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( 1 − 𝑥 ) = 0 )
157 156 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( ( 1 − 𝑥 ) ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
158 0exp ⊢ ( 𝑁 ∈ ℕ → ( 0 ↑ 𝑁 ) = 0 )
159 1 158 syl ⊢ ( 𝜑 → ( 0 ↑ 𝑁 ) = 0 )
160 159 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( 0 ↑ 𝑁 ) = 0 )
161 157 160 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( ( 1 − 𝑥 ) ↑ 𝑁 ) = 0 )
162 161 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) = ( ( - 1 / 𝑁 ) · 0 ) )
163 78 mul01d ⊢ ( 𝜑 → ( ( - 1 / 𝑁 ) · 0 ) = 0 )
164 163 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( ( - 1 / 𝑁 ) · 0 ) = 0 )
165 162 164 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) = 0 )
166 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
167 166 a1i ⊢ ( 𝜑 → 1 ∈ ( 0 [,] 1 ) )
168 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
169 153 165 167 168 fvmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ‘ 1 ) = 0 )
170 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → 𝑥 = 0 )
171 170 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( 1 − 𝑥 ) = ( 1 − 0 ) )
172 1m0e1 ⊢ ( 1 − 0 ) = 1
173 171 172 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( 1 − 𝑥 ) = 1 )
174 173 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( ( 1 − 𝑥 ) ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) )
175 44 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
176 1exp ⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )
177 175 176 syl ⊢ ( 𝜑 → ( 1 ↑ 𝑁 ) = 1 )
178 177 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( 1 ↑ 𝑁 ) = 1 )
179 174 178 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( ( 1 − 𝑥 ) ↑ 𝑁 ) = 1 )
180 179 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) = ( ( - 1 / 𝑁 ) · 1 ) )
181 78 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( - 1 / 𝑁 ) ∈ ℂ )
182 181 mulridd ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( ( - 1 / 𝑁 ) · 1 ) = ( - 1 / 𝑁 ) )
183 180 182 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) = ( - 1 / 𝑁 ) )
184 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
185 184 a1i ⊢ ( 𝜑 → 0 ∈ ( 0 [,] 1 ) )
186 153 183 185 78 fvmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ‘ 0 ) = ( - 1 / 𝑁 ) )
187 169 186 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ‘ 1 ) − ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ‘ 0 ) ) = ( 0 − ( - 1 / 𝑁 ) ) )
188 152 187 eqtrd ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ) ‘ 𝑡 ) d 𝑡 = ( 0 − ( - 1 / 𝑁 ) ) )
189 df-neg ⊢ - - ( 1 / 𝑁 ) = ( 0 − - ( 1 / 𝑁 ) )
190 189 a1i ⊢ ( 𝜑 → - - ( 1 / 𝑁 ) = ( 0 − - ( 1 / 𝑁 ) ) )
191 61 76 77 divnegd ⊢ ( 𝜑 → - ( 1 / 𝑁 ) = ( - 1 / 𝑁 ) )
192 191 oveq2d ⊢ ( 𝜑 → ( 0 − - ( 1 / 𝑁 ) ) = ( 0 − ( - 1 / 𝑁 ) ) )
193 190 192 eqtr2d ⊢ ( 𝜑 → ( 0 − ( - 1 / 𝑁 ) ) = - - ( 1 / 𝑁 ) )
194 76 77 reccld ⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℂ )
195 194 negnegd ⊢ ( 𝜑 → - - ( 1 / 𝑁 ) = ( 1 / 𝑁 ) )
196 193 195 eqtrd ⊢ ( 𝜑 → ( 0 − ( - 1 / 𝑁 ) ) = ( 1 / 𝑁 ) )
197 188 196 eqtrd ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( - 1 / 𝑁 ) · ( ( 1 − 𝑥 ) ↑ 𝑁 ) ) ) ) ‘ 𝑡 ) d 𝑡 = ( 1 / 𝑁 ) )
198 109 197 eqtr3d ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ‘ 𝑡 ) d 𝑡 = ( 1 / 𝑁 ) )
199 37 198 eqtr3d ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) d 𝑡 = ( 1 / 𝑁 ) )
200 22 199 eqtr3d ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) d 𝑡 = ( 1 / 𝑁 ) )
201 bcn1 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 1 ) = 𝑁 )
202 44 201 syl ⊢ ( 𝜑 → ( 𝑁 C 1 ) = 𝑁 )
203 202 oveq2d ⊢ ( 𝜑 → ( 1 · ( 𝑁 C 1 ) ) = ( 1 · 𝑁 ) )
204 76 mullidd ⊢ ( 𝜑 → ( 1 · 𝑁 ) = 𝑁 )
205 203 204 eqtrd ⊢ ( 𝜑 → ( 1 · ( 𝑁 C 1 ) ) = 𝑁 )
206 205 oveq2d ⊢ ( 𝜑 → ( 1 / ( 1 · ( 𝑁 C 1 ) ) ) = ( 1 / 𝑁 ) )
207 200 206 eqtr4d ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) d 𝑡 = ( 1 / ( 1 · ( 𝑁 C 1 ) ) ) )
208 18 207 eqtrd ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑡 ↑ ( 1 − 1 ) ) · ( ( 1 − 𝑡 ) ↑ ( 𝑁 − 1 ) ) ) d 𝑡 = ( 1 / ( 1 · ( 𝑁 C 1 ) ) ) )