Metamath Proof Explorer


Theorem lcmineqlem12

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

Ref Expression
Hypothesis lcmineqlem12.1 φ N
Assertion lcmineqlem12 φ 0 1 t 1 1 1 t N 1 dt = 1 1 ( N 1 )

Proof

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