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 φ 0 1 x M + 1 - 1 1 x N M + 1 dx = M N M 0 1 x M 1 1 x N M dx

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 0 1 x
8 1 nnnn0d φ M 0
9 expcl x M 0 x M
10 8 9 sylan2 x φ x M
11 10 ancoms φ x x M
12 7 11 sylan2 φ x 0 1 x M
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 x N - M - 1
25 7 24 sylan2 φ x 0 1 1 x N - M - 1
26 12 25 mulcld φ x 0 1 x M 1 x N - M - 1
27 0red φ 0
28 1red φ 1
29 expcncf M 0 x x M : cn
30 8 29 syl φ x x M : cn
31 1nn 1
32 31 a1i φ 1
33 20 nnge1d φ 1 N M
34 32 20 33 lcmineqlem9 φ x 1 x N - M - 1 : cn
35 30 34 mulcncf φ x x M 1 x N - M - 1 : cn
36 35 resclunitintvd φ x 0 1 x M 1 x N - M - 1 : 0 1 cn
37 cnicciblnc 0 1 x 0 1 x M 1 x N - M - 1 : 0 1 cn x 0 1 x M 1 x N - M - 1 𝐿 1
38 27 28 36 37 syl3anc φ x 0 1 x M 1 x N - M - 1 𝐿 1
39 26 38 itgcl φ 0 1 x M 1 x N - M - 1 dx
40 6 39 mulneg1d φ N M 0 1 x M 1 x N - M - 1 dx = N M 0 1 x M 1 x N - M - 1 dx
41 6 negcld φ N M
42 41 26 38 itgmulc2 φ N M 0 1 x M 1 x N - M - 1 dx = 0 1 N M x M 1 x N - M - 1 dx
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 x M N M 1 x N - M - 1 = N M x M 1 x N - M - 1
48 7 47 sylan2 φ x 0 1 x M N M 1 x N - M - 1 = N M x M 1 x N - M - 1
49 48 itgeq2dv φ 0 1 x M N M 1 x N - M - 1 dx = 0 1 N M x M 1 x N - M - 1 dx
50 4 adantr φ x 0 1 N
51 5 adantr φ x 0 1 M
52 50 51 subcld φ x 0 1 N M
53 52 negcld φ x 0 1 N M
54 53 25 mulcld φ x 0 1 N M 1 x N - M - 1
55 12 54 mulcld φ x 0 1 x M N M 1 x N - M - 1
56 27 28 55 itgioo φ 0 1 x M N M 1 x N - M - 1 dx = 0 1 x M N M 1 x N - M - 1 dx
57 0le1 0 1
58 57 a1i φ 0 1
59 30 resclunitintvd φ x 0 1 x M : 0 1 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 x N M : cn
66 65 resclunitintvd φ x 0 1 1 x N M : 0 1 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 0 1 M : 0 1 cn
72 nnm1nn0 M M 1 0
73 expcncf M 1 0 x x M 1 : cn
74 1 72 73 3syl φ x x M 1 : cn
75 74 resopunitintvd φ x 0 1 x M 1 : 0 1 cn
76 71 75 mulcncf φ x 0 1 M x M 1 : 0 1 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 0 1 N M : 0 1 cn
81 34 resopunitintvd φ x 0 1 1 x N - M - 1 : 0 1 cn
82 80 81 mulcncf φ x 0 1 N M 1 x N - M - 1 : 0 1 cn
83 ioossicc 0 1 0 1
84 83 a1i φ 0 1 0 1
85 ioombl 0 1 dom vol
86 85 a1i φ 0 1 dom vol
87 79 34 mulcncf φ x N M 1 x N - M - 1 : cn
88 30 87 mulcncf φ x x M N M 1 x N - M - 1 : cn
89 88 resclunitintvd φ x 0 1 x M N M 1 x N - M - 1 : 0 1 cn
90 cnicciblnc 0 1 x 0 1 x M N M 1 x N - M - 1 : 0 1 cn x 0 1 x M N M 1 x N - M - 1 𝐿 1
91 27 28 89 90 syl3anc φ x 0 1 x M N M 1 x N - M - 1 𝐿 1
92 84 86 55 91 iblss φ x 0 1 x M N M 1 x N - M - 1 𝐿 1
93 1 72 syl φ M 1 0
94 expcl x M 1 0 x M 1
95 93 94 sylan2 x φ x M 1
96 95 ancoms φ x x M 1
97 7 96 sylan2 φ x 0 1 x M 1
98 51 97 mulcld φ x 0 1 M x M 1
99 20 nnnn0d φ N M 0
100 99 adantr φ x N M 0
101 15 100 expcld φ x 1 x N M
102 7 101 sylan2 φ x 0 1 1 x N M
103 98 102 mulcld φ x 0 1 M x M 1 1 x N M
104 70 74 mulcncf φ x M x M 1 : cn
105 104 65 mulcncf φ x M x M 1 1 x N M : cn
106 105 resclunitintvd φ x 0 1 M x M 1 1 x N M : 0 1 cn
107 cnicciblnc 0 1 x 0 1 M x M 1 1 x N M : 0 1 cn x 0 1 M x M 1 1 x N M 𝐿 1
108 27 28 106 107 syl3anc φ x 0 1 M x M 1 1 x N M 𝐿 1
109 84 86 103 108 iblss φ x 0 1 M x M 1 1 x N M 𝐿 1
110 dvexp M dx x M d x = x M x M 1
111 1 110 syl φ dx x M d x = x M x M 1
112 44 96 mulcld φ x M x M 1
113 111 11 112 resdvopclptsd φ dx 0 1 x M d x = x 0 1 M x M 1
114 1 2 3 lcmineqlem8 φ dx 1 x N M d x = x N M 1 x N - M - 1
115 46 24 mulcld φ x N M 1 x N - M - 1
116 114 101 115 resdvopclptsd φ dx 0 1 1 x N M d x = x 0 1 N M 1 x N - M - 1
117 oveq1 x = 0 x M = 0 M
118 117 adantl φ x = 0 x M = 0 M
119 1 0expd φ 0 M = 0
120 119 adantr φ x = 0 0 M = 0
121 118 120 eqtrd φ x = 0 x M = 0
122 121 oveq1d φ x = 0 x M 1 x N M = 0 1 x N M
123 0cn 0
124 eleq1 x = 0 x 0
125 123 124 mpbiri x = 0 x
126 101 mul02d φ x 0 1 x N M = 0
127 125 126 sylan2 φ x = 0 0 1 x N M = 0
128 122 127 eqtrd φ x = 0 x M 1 x N 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 x N M = 0 N M
133 132 adantl φ x = 1 1 x N M = 0 N M
134 20 0expd φ 0 N M = 0
135 134 adantr φ x = 1 0 N M = 0
136 133 135 eqtrd φ x = 1 1 x N M = 0
137 136 oveq2d φ x = 1 x M 1 x N M = x M 0
138 ax-1cn 1
139 eleq1 x = 1 x 1
140 138 139 mpbiri x = 1 x
141 11 mul01d φ x x M 0 = 0
142 140 141 sylan2 φ x = 1 x M 0 = 0
143 137 142 eqtrd φ x = 1 x M 1 x N M = 0
144 27 28 58 59 66 76 82 92 109 113 116 128 143 itgparts φ 0 1 x M N M 1 x N - M - 1 dx = 0 - 0 - 0 1 M x M 1 1 x N M dx
145 56 144 eqtr3d φ 0 1 x M N M 1 x N - M - 1 dx = 0 - 0 - 0 1 M x M 1 1 x N M dx
146 27 28 103 itgioo φ 0 1 M x M 1 1 x N M dx = 0 1 M x M 1 1 x N M dx
147 146 oveq2d φ 0 - 0 - 0 1 M x M 1 1 x N M dx = 0 - 0 - 0 1 M x M 1 1 x N M dx
148 145 147 eqtrd φ 0 1 x M N M 1 x N - M - 1 dx = 0 - 0 - 0 1 M x M 1 1 x N M dx
149 0m0e0 0 0 = 0
150 149 oveq1i 0 - 0 - 0 1 M x M 1 1 x N M dx = 0 0 1 M x M 1 1 x N M dx
151 148 150 eqtrdi φ 0 1 x M N M 1 x N - M - 1 dx = 0 0 1 M x M 1 1 x N M dx
152 49 151 eqtr3d φ 0 1 N M x M 1 x N - M - 1 dx = 0 0 1 M x M 1 1 x N M dx
153 42 152 eqtrd φ N M 0 1 x M 1 x N - M - 1 dx = 0 0 1 M x M 1 1 x N M dx
154 44 96 101 mulassd φ x M x M 1 1 x N M = M x M 1 1 x N M
155 7 154 sylan2 φ x 0 1 M x M 1 1 x N M = M x M 1 1 x N M
156 155 itgeq2dv φ 0 1 M x M 1 1 x N M dx = 0 1 M x M 1 1 x N M dx
157 156 oveq2d φ 0 0 1 M x M 1 1 x N M dx = 0 0 1 M x M 1 1 x N M dx
158 153 157 eqtrd φ N M 0 1 x M 1 x N - M - 1 dx = 0 0 1 M x M 1 1 x N M dx
159 97 102 mulcld φ x 0 1 x M 1 1 x N M
160 74 65 mulcncf φ x x M 1 1 x N M : cn
161 160 resclunitintvd φ x 0 1 x M 1 1 x N M : 0 1 cn
162 cnicciblnc 0 1 x 0 1 x M 1 1 x N M : 0 1 cn x 0 1 x M 1 1 x N M 𝐿 1
163 27 28 161 162 syl3anc φ x 0 1 x M 1 1 x N M 𝐿 1
164 5 159 163 itgmulc2 φ M 0 1 x M 1 1 x N M dx = 0 1 M x M 1 1 x N M dx
165 164 oveq2d φ 0 M 0 1 x M 1 1 x N M dx = 0 0 1 M x M 1 1 x N M dx
166 158 165 eqtr4d φ N M 0 1 x M 1 x N - M - 1 dx = 0 M 0 1 x M 1 1 x N M dx
167 df-neg M 0 1 x M 1 1 x N M dx = 0 M 0 1 x M 1 1 x N M dx
168 166 167 eqtr4di φ N M 0 1 x M 1 x N - M - 1 dx = M 0 1 x M 1 1 x N M dx
169 40 168 eqtr3d φ N M 0 1 x M 1 x N - M - 1 dx = M 0 1 x M 1 1 x N M dx
170 6 39 mulcld φ N M 0 1 x M 1 x N - M - 1 dx
171 159 163 itgcl φ 0 1 x M 1 1 x N M dx
172 5 171 mulcld φ M 0 1 x M 1 1 x N M dx
173 170 172 neg11ad φ N M 0 1 x M 1 x N - M - 1 dx = M 0 1 x M 1 1 x N M dx N M 0 1 x M 1 x N - M - 1 dx = M 0 1 x M 1 1 x N M dx
174 169 173 mpbid φ N M 0 1 x M 1 x N - M - 1 dx = M 0 1 x M 1 1 x N M dx
175 20 nnne0d φ N M 0
176 172 6 39 175 divmuld φ M 0 1 x M 1 1 x N M dx N M = 0 1 x M 1 x N - M - 1 dx N M 0 1 x M 1 x N - M - 1 dx = M 0 1 x M 1 1 x N M dx
177 174 176 mpbird φ M 0 1 x M 1 1 x N M dx N M = 0 1 x M 1 x N - M - 1 dx
178 138 a1i φ 1
179 5 178 pncand φ M + 1 - 1 = M
180 179 eqcomd φ M = M + 1 - 1
181 180 oveq2d φ x M = x M + 1 - 1
182 4 5 178 subsub4d φ N - M - 1 = N M + 1
183 182 oveq2d φ 1 x N - M - 1 = 1 x N M + 1
184 181 183 oveq12d φ x M 1 x N - M - 1 = x M + 1 - 1 1 x N M + 1
185 184 adantr φ x 0 1 x M 1 x N - M - 1 = x M + 1 - 1 1 x N M + 1
186 185 itgeq2dv φ 0 1 x M 1 x N - M - 1 dx = 0 1 x M + 1 - 1 1 x N M + 1 dx
187 177 186 eqtrd φ M 0 1 x M 1 1 x N M dx N M = 0 1 x M + 1 - 1 1 x N M + 1 dx
188 187 eqcomd φ 0 1 x M + 1 - 1 1 x N M + 1 dx = M 0 1 x M 1 1 x N M dx N M
189 5 171 6 175 div23d φ M 0 1 x M 1 1 x N M dx N M = M N M 0 1 x M 1 1 x N M dx
190 188 189 eqtrd φ 0 1 x M + 1 - 1 1 x N M + 1 dx = M N M 0 1 x M 1 1 x N M dx