Metamath Proof Explorer

Theorem lcmineqlem10

Description: Induction step of lcmineqlem13 (deduction form). (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses lcmineqlem10.1 ⊢φ→M∈ℕ
lcmineqlem10.2 ⊢φ→N∈ℕ
lcmineqlem10.3 ⊢φ→M<N
Assertion lcmineqlem10 ⊢φ→∫01xM+1-1⁢1−xN−M+1dx=MN−M⁢∫01xM−1⁢1−xN−Mdx

Proof

Step Hyp Ref Expression
1 lcmineqlem10.1 ⊢φ→M∈ℕ
2 lcmineqlem10.2 ⊢φ→N∈ℕ
3 lcmineqlem10.3 ⊢φ→M<N
4 2 nncnd ⊢φ→N∈ℂ
5 1 nncnd ⊢φ→M∈ℂ
6 4 5 subcld ⊢φ→N−M∈ℂ
7 elunitcn ⊢x∈01→x∈ℂ
8 1 nnnn0d ⊢φ→M∈ℕ0
9 expcl ⊢x∈ℂ∧M∈ℕ0→xM∈ℂ
10 8 9 sylan2 ⊢x∈ℂ∧φ→xM∈ℂ
11 10 ancoms ⊢φ∧x∈ℂ→xM∈ℂ
12 7 11 sylan2 ⊢φ∧x∈01→xM∈ℂ
13 1cnd ⊢φ∧x∈ℂ→1∈ℂ
14 simpr ⊢φ∧x∈ℂ→x∈ℂ
15 13 14 subcld ⊢φ∧x∈ℂ→1−x∈ℂ
16 1 nnzd ⊢φ→M∈ℤ
17 2 nnzd ⊢φ→N∈ℤ
18 znnsub ⊢M∈ℤ∧N∈ℤ→M<N↔N−M∈ℕ
19 16 17 18 syl2anc ⊢φ→M<N↔N−M∈ℕ
20 3 19 mpbid ⊢φ→N−M∈ℕ
21 nnm1nn0 ⊢N−M∈ℕ→N-M-1∈ℕ0
22 20 21 syl ⊢φ→N-M-1∈ℕ0
23 22 adantr ⊢φ∧x∈ℂ→N-M-1∈ℕ0
24 15 23 expcld ⊢φ∧x∈ℂ→1−xN-M-1∈ℂ
25 7 24 sylan2 ⊢φ∧x∈01→1−xN-M-1∈ℂ
26 12 25 mulcld ⊢φ∧x∈01→xM⁢1−xN-M-1∈ℂ
27 0red ⊢φ→0∈ℝ
28 1red ⊢φ→1∈ℝ
29 expcncf ⊢M∈ℕ0→x∈ℂ⟼xM:ℂ⟶cnℂ
30 8 29 syl ⊢φ→x∈ℂ⟼xM:ℂ⟶cnℂ
31 1nn ⊢1∈ℕ
32 31 a1i ⊢φ→1∈ℕ
33 20 nnge1d ⊢φ→1≤N−M
34 32 20 33 lcmineqlem9 ⊢φ→x∈ℂ⟼1−xN-M-1:ℂ⟶cnℂ
35 30 34 mulcncf ⊢φ→x∈ℂ⟼xM⁢1−xN-M-1:ℂ⟶cnℂ
36 35 resclunitintvd ⊢φ→x∈01⟼xM⁢1−xN-M-1:01⟶cnℂ
37 cnicciblnc ⊢0∈ℝ∧1∈ℝ∧x∈01⟼xM⁢1−xN-M-1:01⟶cnℂ→x∈01⟼xM⁢1−xN-M-1∈𝐿1
38 27 28 36 37 syl3anc ⊢φ→x∈01⟼xM⁢1−xN-M-1∈𝐿1
39 26 38 itgcl ⊢φ→∫01xM⁢1−xN-M-1dx∈ℂ
40 6 39 mulneg1d ⊢φ→−N−M⁢∫01xM⁢1−xN-M-1dx=−N−M⁢∫01xM⁢1−xN-M-1dx
41 6 negcld ⊢φ→−N−M∈ℂ
42 41 26 38 itgmulc2 ⊢φ→−N−M⁢∫01xM⁢1−xN-M-1dx=∫01−N−M⁢xM⁢1−xN-M-1dx
43 4 adantr ⊢φ∧x∈ℂ→N∈ℂ
44 5 adantr ⊢φ∧x∈ℂ→M∈ℂ
45 43 44 subcld ⊢φ∧x∈ℂ→N−M∈ℂ
46 45 negcld ⊢φ∧x∈ℂ→−N−M∈ℂ
47 11 46 24 mul12d ⊢φ∧x∈ℂ→xM⁢−N−M⁢1−xN-M-1=−N−M⁢xM⁢1−xN-M-1
48 7 47 sylan2 ⊢φ∧x∈01→xM⁢−N−M⁢1−xN-M-1=−N−M⁢xM⁢1−xN-M-1
49 48 itgeq2dv ⊢φ→∫01xM⁢−N−M⁢1−xN-M-1dx=∫01−N−M⁢xM⁢1−xN-M-1dx
50 4 adantr ⊢φ∧x∈01→N∈ℂ
51 5 adantr ⊢φ∧x∈01→M∈ℂ
52 50 51 subcld ⊢φ∧x∈01→N−M∈ℂ
53 52 negcld ⊢φ∧x∈01→−N−M∈ℂ
54 53 25 mulcld ⊢φ∧x∈01→−N−M⁢1−xN-M-1∈ℂ
55 12 54 mulcld ⊢φ∧x∈01→xM⁢−N−M⁢1−xN-M-1∈ℂ
56 27 28 55 itgioo ⊢φ→∫01xM⁢−N−M⁢1−xN-M-1dx=∫01xM⁢−N−M⁢1−xN-M-1dx
57 0le1 ⊢0≤1
58 57 a1i ⊢φ→0≤1
59 30 resclunitintvd ⊢φ→x∈01⟼xM:01⟶cnℂ
60 1 nnred ⊢φ→M∈ℝ
61 2 nnred ⊢φ→N∈ℝ
62 ltle ⊢M∈ℝ∧N∈ℝ→M<N→M≤N
63 60 61 62 syl2anc ⊢φ→M<N→M≤N
64 3 63 mpd ⊢φ→M≤N
65 1 2 64 lcmineqlem9 ⊢φ→x∈ℂ⟼1−xN−M:ℂ⟶cnℂ
66 65 resclunitintvd ⊢φ→x∈01⟼1−xN−M:01⟶cnℂ
67 ssid ⊢ℂ⊆ℂ
68 cncfmptc ⊢M∈ℂ∧ℂ⊆ℂ∧ℂ⊆ℂ→x∈ℂ⟼M:ℂ⟶cnℂ
69 67 67 68 mp3an23 ⊢M∈ℂ→x∈ℂ⟼M:ℂ⟶cnℂ
70 5 69 syl ⊢φ→x∈ℂ⟼M:ℂ⟶cnℂ
71 70 resopunitintvd ⊢φ→x∈01⟼M:01⟶cnℂ
72 nnm1nn0 ⊢M∈ℕ→M−1∈ℕ0
73 expcncf ⊢M−1∈ℕ0→x∈ℂ⟼xM−1:ℂ⟶cnℂ
74 1 72 73 3syl ⊢φ→x∈ℂ⟼xM−1:ℂ⟶cnℂ
75 74 resopunitintvd ⊢φ→x∈01⟼xM−1:01⟶cnℂ
76 71 75 mulcncf ⊢φ→x∈01⟼M⁢xM−1:01⟶cnℂ
77 cncfmptc ⊢−N−M∈ℂ∧ℂ⊆ℂ∧ℂ⊆ℂ→x∈ℂ⟼−N−M:ℂ⟶cnℂ
78 67 67 77 mp3an23 ⊢−N−M∈ℂ→x∈ℂ⟼−N−M:ℂ⟶cnℂ
79 41 78 syl ⊢φ→x∈ℂ⟼−N−M:ℂ⟶cnℂ
80 79 resopunitintvd ⊢φ→x∈01⟼−N−M:01⟶cnℂ
81 34 resopunitintvd ⊢φ→x∈01⟼1−xN-M-1:01⟶cnℂ
82 80 81 mulcncf ⊢φ→x∈01⟼−N−M⁢1−xN-M-1:01⟶cnℂ
83 ioossicc ⊢01⊆01
84 83 a1i ⊢φ→01⊆01
85 ioombl ⊢01∈dom⁡vol
86 85 a1i ⊢φ→01∈dom⁡vol
87 79 34 mulcncf ⊢φ→x∈ℂ⟼−N−M⁢1−xN-M-1:ℂ⟶cnℂ
88 30 87 mulcncf ⊢φ→x∈ℂ⟼xM⁢−N−M⁢1−xN-M-1:ℂ⟶cnℂ
89 88 resclunitintvd ⊢φ→x∈01⟼xM⁢−N−M⁢1−xN-M-1:01⟶cnℂ
90 cnicciblnc ⊢0∈ℝ∧1∈ℝ∧x∈01⟼xM⁢−N−M⁢1−xN-M-1:01⟶cnℂ→x∈01⟼xM⁢−N−M⁢1−xN-M-1∈𝐿1
91 27 28 89 90 syl3anc ⊢φ→x∈01⟼xM⁢−N−M⁢1−xN-M-1∈𝐿1
92 84 86 55 91 iblss ⊢φ→x∈01⟼xM⁢−N−M⁢1−xN-M-1∈𝐿1
93 1 72 syl ⊢φ→M−1∈ℕ0
94 expcl ⊢x∈ℂ∧M−1∈ℕ0→xM−1∈ℂ
95 93 94 sylan2 ⊢x∈ℂ∧φ→xM−1∈ℂ
96 95 ancoms ⊢φ∧x∈ℂ→xM−1∈ℂ
97 7 96 sylan2 ⊢φ∧x∈01→xM−1∈ℂ
98 51 97 mulcld ⊢φ∧x∈01→M⁢xM−1∈ℂ
99 20 nnnn0d ⊢φ→N−M∈ℕ0
100 99 adantr ⊢φ∧x∈ℂ→N−M∈ℕ0
101 15 100 expcld ⊢φ∧x∈ℂ→1−xN−M∈ℂ
102 7 101 sylan2 ⊢φ∧x∈01→1−xN−M∈ℂ
103 98 102 mulcld ⊢φ∧x∈01→M⁢xM−1⁢1−xN−M∈ℂ
104 70 74 mulcncf ⊢φ→x∈ℂ⟼M⁢xM−1:ℂ⟶cnℂ
105 104 65 mulcncf ⊢φ→x∈ℂ⟼M⁢xM−1⁢1−xN−M:ℂ⟶cnℂ
106 105 resclunitintvd ⊢φ→x∈01⟼M⁢xM−1⁢1−xN−M:01⟶cnℂ
107 cnicciblnc ⊢0∈ℝ∧1∈ℝ∧x∈01⟼M⁢xM−1⁢1−xN−M:01⟶cnℂ→x∈01⟼M⁢xM−1⁢1−xN−M∈𝐿1
108 27 28 106 107 syl3anc ⊢φ→x∈01⟼M⁢xM−1⁢1−xN−M∈𝐿1
109 84 86 103 108 iblss ⊢φ→x∈01⟼M⁢xM−1⁢1−xN−M∈𝐿1
110 dvexp ⊢M∈ℕ→dx∈ℂxMdℂx=x∈ℂ⟼M⁢xM−1
111 1 110 syl ⊢φ→dx∈ℂxMdℂx=x∈ℂ⟼M⁢xM−1
112 44 96 mulcld ⊢φ∧x∈ℂ→M⁢xM−1∈ℂ
113 111 11 112 resdvopclptsd ⊢φ→dx∈01xMdℝx=x∈01⟼M⁢xM−1
114 1 2 3 lcmineqlem8 ⊢φ→dx∈ℂ1−xN−Mdℂx=x∈ℂ⟼−N−M⁢1−xN-M-1
115 46 24 mulcld ⊢φ∧x∈ℂ→−N−M⁢1−xN-M-1∈ℂ
116 114 101 115 resdvopclptsd ⊢φ→dx∈011−xN−Mdℝx=x∈01⟼−N−M⁢1−xN-M-1
117 oveq1 ⊢x=0→xM=0M
118 117 adantl ⊢φ∧x=0→xM=0M
119 1 0expd ⊢φ→0M=0
120 119 adantr ⊢φ∧x=0→0M=0
121 118 120 eqtrd ⊢φ∧x=0→xM=0
122 121 oveq1d ⊢φ∧x=0→xM⁢1−xN−M=0⋅1−xN−M
123 0cn ⊢0∈ℂ
124 eleq1 ⊢x=0→x∈ℂ↔0∈ℂ
125 123 124 mpbiri ⊢x=0→x∈ℂ
126 101 mul02d ⊢φ∧x∈ℂ→0⋅1−xN−M=0
127 125 126 sylan2 ⊢φ∧x=0→0⋅1−xN−M=0
128 122 127 eqtrd ⊢φ∧x=0→xM⁢1−xN−M=0
129 oveq2 ⊢x=1→1−x=1−1
130 1m1e0 ⊢1−1=0
131 129 130 eqtrdi ⊢x=1→1−x=0
132 131 oveq1d ⊢x=1→1−xN−M=0N−M
133 132 adantl ⊢φ∧x=1→1−xN−M=0N−M
134 20 0expd ⊢φ→0N−M=0
135 134 adantr ⊢φ∧x=1→0N−M=0
136 133 135 eqtrd ⊢φ∧x=1→1−xN−M=0
137 136 oveq2d ⊢φ∧x=1→xM⁢1−xN−M=xM⋅0
138 ax-1cn ⊢1∈ℂ
139 eleq1 ⊢x=1→x∈ℂ↔1∈ℂ
140 138 139 mpbiri ⊢x=1→x∈ℂ
141 11 mul01d ⊢φ∧x∈ℂ→xM⋅0=0
142 140 141 sylan2 ⊢φ∧x=1→xM⋅0=0
143 137 142 eqtrd ⊢φ∧x=1→xM⁢1−xN−M=0
144 27 28 58 59 66 76 82 92 109 113 116 128 143 itgparts ⊢φ→∫01xM⁢−N−M⁢1−xN-M-1dx=0-0-∫01M⁢xM−1⁢1−xN−Mdx
145 56 144 eqtr3d ⊢φ→∫01xM⁢−N−M⁢1−xN-M-1dx=0-0-∫01M⁢xM−1⁢1−xN−Mdx
146 27 28 103 itgioo ⊢φ→∫01M⁢xM−1⁢1−xN−Mdx=∫01M⁢xM−1⁢1−xN−Mdx
147 146 oveq2d ⊢φ→0-0-∫01M⁢xM−1⁢1−xN−Mdx=0-0-∫01M⁢xM−1⁢1−xN−Mdx
148 145 147 eqtrd ⊢φ→∫01xM⁢−N−M⁢1−xN-M-1dx=0-0-∫01M⁢xM−1⁢1−xN−Mdx
149 0m0e0 ⊢0−0=0
150 149 oveq1i ⊢0-0-∫01M⁢xM−1⁢1−xN−Mdx=0−∫01M⁢xM−1⁢1−xN−Mdx
151 148 150 eqtrdi ⊢φ→∫01xM⁢−N−M⁢1−xN-M-1dx=0−∫01M⁢xM−1⁢1−xN−Mdx
152 49 151 eqtr3d ⊢φ→∫01−N−M⁢xM⁢1−xN-M-1dx=0−∫01M⁢xM−1⁢1−xN−Mdx
153 42 152 eqtrd ⊢φ→−N−M⁢∫01xM⁢1−xN-M-1dx=0−∫01M⁢xM−1⁢1−xN−Mdx
154 44 96 101 mulassd ⊢φ∧x∈ℂ→M⁢xM−1⁢1−xN−M=M⁢xM−1⁢1−xN−M
155 7 154 sylan2 ⊢φ∧x∈01→M⁢xM−1⁢1−xN−M=M⁢xM−1⁢1−xN−M
156 155 itgeq2dv ⊢φ→∫01M⁢xM−1⁢1−xN−Mdx=∫01M⁢xM−1⁢1−xN−Mdx
157 156 oveq2d ⊢φ→0−∫01M⁢xM−1⁢1−xN−Mdx=0−∫01M⁢xM−1⁢1−xN−Mdx
158 153 157 eqtrd ⊢φ→−N−M⁢∫01xM⁢1−xN-M-1dx=0−∫01M⁢xM−1⁢1−xN−Mdx
159 97 102 mulcld ⊢φ∧x∈01→xM−1⁢1−xN−M∈ℂ
160 74 65 mulcncf ⊢φ→x∈ℂ⟼xM−1⁢1−xN−M:ℂ⟶cnℂ
161 160 resclunitintvd ⊢φ→x∈01⟼xM−1⁢1−xN−M:01⟶cnℂ
162 cnicciblnc ⊢0∈ℝ∧1∈ℝ∧x∈01⟼xM−1⁢1−xN−M:01⟶cnℂ→x∈01⟼xM−1⁢1−xN−M∈𝐿1
163 27 28 161 162 syl3anc ⊢φ→x∈01⟼xM−1⁢1−xN−M∈𝐿1
164 5 159 163 itgmulc2 ⊢φ→M⁢∫01xM−1⁢1−xN−Mdx=∫01M⁢xM−1⁢1−xN−Mdx
165 164 oveq2d ⊢φ→0−M⁢∫01xM−1⁢1−xN−Mdx=0−∫01M⁢xM−1⁢1−xN−Mdx
166 158 165 eqtr4d ⊢φ→−N−M⁢∫01xM⁢1−xN-M-1dx=0−M⁢∫01xM−1⁢1−xN−Mdx
167 df-neg ⊢−M⁢∫01xM−1⁢1−xN−Mdx=0−M⁢∫01xM−1⁢1−xN−Mdx
168 166 167 eqtr4di ⊢φ→−N−M⁢∫01xM⁢1−xN-M-1dx=−M⁢∫01xM−1⁢1−xN−Mdx
169 40 168 eqtr3d ⊢φ→−N−M⁢∫01xM⁢1−xN-M-1dx=−M⁢∫01xM−1⁢1−xN−Mdx
170 6 39 mulcld ⊢φ→N−M⁢∫01xM⁢1−xN-M-1dx∈ℂ
171 159 163 itgcl ⊢φ→∫01xM−1⁢1−xN−Mdx∈ℂ
172 5 171 mulcld ⊢φ→M⁢∫01xM−1⁢1−xN−Mdx∈ℂ
173 170 172 neg11ad ⊢φ→−N−M⁢∫01xM⁢1−xN-M-1dx=−M⁢∫01xM−1⁢1−xN−Mdx↔N−M⁢∫01xM⁢1−xN-M-1dx=M⁢∫01xM−1⁢1−xN−Mdx
174 169 173 mpbid ⊢φ→N−M⁢∫01xM⁢1−xN-M-1dx=M⁢∫01xM−1⁢1−xN−Mdx
175 20 nnne0d ⊢φ→N−M≠0
176 172 6 39 175 divmuld ⊢φ→M⁢∫01xM−1⁢1−xN−MdxN−M=∫01xM⁢1−xN-M-1dx↔N−M⁢∫01xM⁢1−xN-M-1dx=M⁢∫01xM−1⁢1−xN−Mdx
177 174 176 mpbird ⊢φ→M⁢∫01xM−1⁢1−xN−MdxN−M=∫01xM⁢1−xN-M-1dx
178 138 a1i ⊢φ→1∈ℂ
179 5 178 pncand ⊢φ→M+1-1=M
180 179 eqcomd ⊢φ→M=M+1-1
181 180 oveq2d ⊢φ→xM=xM+1-1
182 4 5 178 subsub4d ⊢φ→N-M-1=N−M+1
183 182 oveq2d ⊢φ→1−xN-M-1=1−xN−M+1
184 181 183 oveq12d ⊢φ→xM⁢1−xN-M-1=xM+1-1⁢1−xN−M+1
185 184 adantr ⊢φ∧x∈01→xM⁢1−xN-M-1=xM+1-1⁢1−xN−M+1
186 185 itgeq2dv ⊢φ→∫01xM⁢1−xN-M-1dx=∫01xM+1-1⁢1−xN−M+1dx
187 177 186 eqtrd ⊢φ→M⁢∫01xM−1⁢1−xN−MdxN−M=∫01xM+1-1⁢1−xN−M+1dx
188 187 eqcomd ⊢φ→∫01xM+1-1⁢1−xN−M+1dx=M⁢∫01xM−1⁢1−xN−MdxN−M
189 5 171 6 175 div23d ⊢φ→M⁢∫01xM−1⁢1−xN−MdxN−M=MN−M⁢∫01xM−1⁢1−xN−Mdx
190 188 189 eqtrd ⊢φ→∫01xM+1-1⁢1−xN−M+1dx=MN−M⁢∫01xM−1⁢1−xN−Mdx