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 eqtrid ⊢ φ → F = 1 M ⁢ ( N M)