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 ) ) ) )