Metamath Proof Explorer


Theorem lcmineqlem13

Description: Induction proof for lcm integral. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses lcmineqlem13.1 F = 0 1 x M 1 1 x N M dx
lcmineqlem13.2 φ M
lcmineqlem13.3 φ N
lcmineqlem13.4 φ M N
Assertion lcmineqlem13 φ F = 1 M ( N M)

Proof

Step Hyp Ref Expression
1 lcmineqlem13.1 F = 0 1 x M 1 1 x N M dx
2 lcmineqlem13.2 φ M
3 lcmineqlem13.3 φ N
4 lcmineqlem13.4 φ M N
5 2 nnzd φ M
6 nnge1 M 1 M
7 2 6 syl φ 1 M
8 5 7 4 3jca φ M 1 M M N
9 oveq1 i = 1 i 1 = 1 1
10 9 oveq2d i = 1 x i 1 = x 1 1
11 oveq2 i = 1 N i = N 1
12 11 oveq2d i = 1 1 x N i = 1 x N 1
13 10 12 oveq12d i = 1 x i 1 1 x N i = x 1 1 1 x N 1
14 13 adantr i = 1 x 0 1 x i 1 1 x N i = x 1 1 1 x N 1
15 14 itgeq2dv i = 1 0 1 x i 1 1 x N i dx = 0 1 x 1 1 1 x N 1 dx
16 id i = 1 i = 1
17 oveq2 i = 1 ( N i) = ( N 1 )
18 16 17 oveq12d i = 1 i ( N i) = 1 ( N 1 )
19 18 oveq2d i = 1 1 i ( N i) = 1 1 ( N 1 )
20 15 19 eqeq12d i = 1 0 1 x i 1 1 x N i dx = 1 i ( N i) 0 1 x 1 1 1 x N 1 dx = 1 1 ( N 1 )
21 oveq1 i = m i 1 = m 1
22 21 oveq2d i = m x i 1 = x m 1
23 oveq2 i = m N i = N m
24 23 oveq2d i = m 1 x N i = 1 x N m
25 22 24 oveq12d i = m x i 1 1 x N i = x m 1 1 x N m
26 25 adantr i = m x 0 1 x i 1 1 x N i = x m 1 1 x N m
27 26 itgeq2dv i = m 0 1 x i 1 1 x N i dx = 0 1 x m 1 1 x N m dx
28 id i = m i = m
29 oveq2 i = m ( N i) = ( N m)
30 28 29 oveq12d i = m i ( N i) = m ( N m)
31 30 oveq2d i = m 1 i ( N i) = 1 m ( N m)
32 27 31 eqeq12d i = m 0 1 x i 1 1 x N i dx = 1 i ( N i) 0 1 x m 1 1 x N m dx = 1 m ( N m)
33 oveq1 i = m + 1 i 1 = m + 1 - 1
34 33 oveq2d i = m + 1 x i 1 = x m + 1 - 1
35 oveq2 i = m + 1 N i = N m + 1
36 35 oveq2d i = m + 1 1 x N i = 1 x N m + 1
37 34 36 oveq12d i = m + 1 x i 1 1 x N i = x m + 1 - 1 1 x N m + 1
38 37 adantr i = m + 1 x 0 1 x i 1 1 x N i = x m + 1 - 1 1 x N m + 1
39 38 itgeq2dv i = m + 1 0 1 x i 1 1 x N i dx = 0 1 x m + 1 - 1 1 x N m + 1 dx
40 id i = m + 1 i = m + 1
41 oveq2 i = m + 1 ( N i) = ( N m + 1 )
42 40 41 oveq12d i = m + 1 i ( N i) = m + 1 ( N m + 1 )
43 42 oveq2d i = m + 1 1 i ( N i) = 1 m + 1 ( N m + 1 )
44 39 43 eqeq12d i = m + 1 0 1 x i 1 1 x N i dx = 1 i ( N i) 0 1 x m + 1 - 1 1 x N m + 1 dx = 1 m + 1 ( N m + 1 )
45 oveq1 i = M i 1 = M 1
46 45 oveq2d i = M x i 1 = x M 1
47 oveq2 i = M N i = N M
48 47 oveq2d i = M 1 x N i = 1 x N M
49 46 48 oveq12d i = M x i 1 1 x N i = x M 1 1 x N M
50 49 adantr i = M x 0 1 x i 1 1 x N i = x M 1 1 x N M
51 50 itgeq2dv i = M 0 1 x i 1 1 x N i dx = 0 1 x M 1 1 x N M dx
52 id i = M i = M
53 oveq2 i = M ( N i) = ( N M)
54 52 53 oveq12d i = M i ( N i) = M ( N M)
55 54 oveq2d i = M 1 i ( N i) = 1 M ( N M)
56 51 55 eqeq12d i = M 0 1 x i 1 1 x N i dx = 1 i ( N i) 0 1 x M 1 1 x N M dx = 1 M ( N M)
57 3 lcmineqlem12 φ 0 1 x 1 1 1 x N 1 dx = 1 1 ( N 1 )
58 elnnz1 m m 1 m
59 58 biimpri m 1 m m
60 59 3adant3 m 1 m m < N m
61 60 adantl φ m 1 m m < N m
62 3 adantr φ m 1 m m < N N
63 simpr3 φ m 1 m m < N m < N
64 61 62 63 lcmineqlem10 φ m 1 m m < N 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
65 64 3adant3 φ m 1 m m < N 0 1 x m 1 1 x N m dx = 1 m ( N m) 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
66 oveq2 0 1 x m 1 1 x N m dx = 1 m ( N m) m N m 0 1 x m 1 1 x N m dx = m N m 1 m ( N m)
67 66 3ad2ant3 φ m 1 m m < N 0 1 x m 1 1 x N m dx = 1 m ( N m) m N m 0 1 x m 1 1 x N m dx = m N m 1 m ( N m)
68 65 67 eqtrd φ m 1 m m < N 0 1 x m 1 1 x N m dx = 1 m ( N m) 0 1 x m + 1 - 1 1 x N m + 1 dx = m N m 1 m ( N m)
69 61 62 63 lcmineqlem11 φ m 1 m m < N 1 m + 1 ( N m + 1 ) = m N m 1 m ( N m)
70 69 3adant3 φ m 1 m m < N 0 1 x m 1 1 x N m dx = 1 m ( N m) 1 m + 1 ( N m + 1 ) = m N m 1 m ( N m)
71 68 70 eqtr4d φ m 1 m m < N 0 1 x m 1 1 x N m dx = 1 m ( N m) 0 1 x m + 1 - 1 1 x N m + 1 dx = 1 m + 1 ( N m + 1 )
72 1zzd φ 1
73 3 nnzd φ N
74 3 nnge1d φ 1 N
75 20 32 44 56 57 71 72 73 74 fzindd φ M 1 M M N 0 1 x M 1 1 x N M dx = 1 M ( N M)
76 8 75 mpdan φ 0 1 x M 1 1 x N M dx = 1 M ( N M)
77 1 76 syl5eq φ F = 1 M ( N M)