lcmineqlem12

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

		Ref	Expression
	Hypothesis	lcmineqlem12.1	$⊢ φ \to N \in ℕ$
	Assertion	lcmineqlem12	$⊢ φ \to \int_{[0, 1]} t^{1 - 1} {(1 - t)}^{N - 1} d t = \frac{1}{1 (\binom{N}{1})}$

Proof

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

Metamath Proof Explorer

Theorem lcmineqlem12

Proof