Metamath Proof Explorer

Theorem lcmineqlem13

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

Ref Expression
Hypotheses lcmineqlem13.1 ⊢F=∫01xM−1⁢1−xN−Mdx
lcmineqlem13.2 ⊢φ→M∈ℕ
lcmineqlem13.3 ⊢φ→N∈ℕ
lcmineqlem13.4 ⊢φ→M≤N
Assertion lcmineqlem13 ⊢φ→F=1M⁢(NM)

Proof

Step Hyp Ref Expression
1 lcmineqlem13.1 ⊢F=∫01xM−1⁢1−xN−Mdx
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→xi−1=x1−1
11 oveq2 ⊢i=1→N−i=N−1
12 11 oveq2d ⊢i=1→1−xN−i=1−xN−1
13 10 12 oveq12d ⊢i=1→xi−1⁢1−xN−i=x1−1⁢1−xN−1
14 13 adantr ⊢i=1∧x∈01→xi−1⁢1−xN−i=x1−1⁢1−xN−1
15 14 itgeq2dv ⊢i=1→∫01xi−1⁢1−xN−idx=∫01x1−1⁢1−xN−1dx
16 id ⊢i=1→i=1
17 oveq2 ⊢i=1→(Ni)=(N1)
18 16 17 oveq12d ⊢i=1→i⁢(Ni)=1⁢(N1)
19 18 oveq2d ⊢i=1→1i⁢(Ni)=11⁢(N1)
20 15 19 eqeq12d ⊢i=1→∫01xi−1⁢1−xN−idx=1i⁢(Ni)↔∫01x1−1⁢1−xN−1dx=11⁢(N1)
21 oveq1 ⊢i=m→i−1=m−1
22 21 oveq2d ⊢i=m→xi−1=xm−1
23 oveq2 ⊢i=m→N−i=N−m
24 23 oveq2d ⊢i=m→1−xN−i=1−xN−m
25 22 24 oveq12d ⊢i=m→xi−1⁢1−xN−i=xm−1⁢1−xN−m
26 25 adantr ⊢i=m∧x∈01→xi−1⁢1−xN−i=xm−1⁢1−xN−m
27 26 itgeq2dv ⊢i=m→∫01xi−1⁢1−xN−idx=∫01xm−1⁢1−xN−mdx
28 id ⊢i=m→i=m
29 oveq2 ⊢i=m→(Ni)=(Nm)
30 28 29 oveq12d ⊢i=m→i⁢(Ni)=m⁢(Nm)
31 30 oveq2d ⊢i=m→1i⁢(Ni)=1m⁢(Nm)
32 27 31 eqeq12d ⊢i=m→∫01xi−1⁢1−xN−idx=1i⁢(Ni)↔∫01xm−1⁢1−xN−mdx=1m⁢(Nm)
33 oveq1 ⊢i=m+1→i−1=m+1-1
34 33 oveq2d ⊢i=m+1→xi−1=xm+1-1
35 oveq2 ⊢i=m+1→N−i=N−m+1
36 35 oveq2d ⊢i=m+1→1−xN−i=1−xN−m+1
37 34 36 oveq12d ⊢i=m+1→xi−1⁢1−xN−i=xm+1-1⁢1−xN−m+1
38 37 adantr ⊢i=m+1∧x∈01→xi−1⁢1−xN−i=xm+1-1⁢1−xN−m+1
39 38 itgeq2dv ⊢i=m+1→∫01xi−1⁢1−xN−idx=∫01xm+1-1⁢1−xN−m+1dx
40 id ⊢i=m+1→i=m+1
41 oveq2 ⊢i=m+1→(Ni)=(Nm+1)
42 40 41 oveq12d ⊢i=m+1→i⁢(Ni)=m+1⁢(Nm+1)
43 42 oveq2d ⊢i=m+1→1i⁢(Ni)=1m+1⁢(Nm+1)
44 39 43 eqeq12d ⊢i=m+1→∫01xi−1⁢1−xN−idx=1i⁢(Ni)↔∫01xm+1-1⁢1−xN−m+1dx=1m+1⁢(Nm+1)
45 oveq1 ⊢i=M→i−1=M−1
46 45 oveq2d ⊢i=M→xi−1=xM−1
47 oveq2 ⊢i=M→N−i=N−M
48 47 oveq2d ⊢i=M→1−xN−i=1−xN−M
49 46 48 oveq12d ⊢i=M→xi−1⁢1−xN−i=xM−1⁢1−xN−M
50 49 adantr ⊢i=M∧x∈01→xi−1⁢1−xN−i=xM−1⁢1−xN−M
51 50 itgeq2dv ⊢i=M→∫01xi−1⁢1−xN−idx=∫01xM−1⁢1−xN−Mdx
52 id ⊢i=M→i=M
53 oveq2 ⊢i=M→(Ni)=(NM)
54 52 53 oveq12d ⊢i=M→i⁢(Ni)=M⁢(NM)
55 54 oveq2d ⊢i=M→1i⁢(Ni)=1M⁢(NM)
56 51 55 eqeq12d ⊢i=M→∫01xi−1⁢1−xN−idx=1i⁢(Ni)↔∫01xM−1⁢1−xN−Mdx=1M⁢(NM)
57 3 lcmineqlem12 ⊢φ→∫01x1−1⁢1−xN−1dx=11⁢(N1)
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→∫01xm+1-1⁢1−xN−m+1dx=mN−m⁢∫01xm−1⁢1−xN−mdx
65 64 3adant3 ⊢φ∧m∈ℤ∧1≤m∧m<N∧∫01xm−1⁢1−xN−mdx=1m⁢(Nm)→∫01xm+1-1⁢1−xN−m+1dx=mN−m⁢∫01xm−1⁢1−xN−mdx
66 oveq2 ⊢∫01xm−1⁢1−xN−mdx=1m⁢(Nm)→mN−m⁢∫01xm−1⁢1−xN−mdx=mN−m⁢1m⁢(Nm)
67 66 3ad2ant3 ⊢φ∧m∈ℤ∧1≤m∧m<N∧∫01xm−1⁢1−xN−mdx=1m⁢(Nm)→mN−m⁢∫01xm−1⁢1−xN−mdx=mN−m⁢1m⁢(Nm)
68 65 67 eqtrd ⊢φ∧m∈ℤ∧1≤m∧m<N∧∫01xm−1⁢1−xN−mdx=1m⁢(Nm)→∫01xm+1-1⁢1−xN−m+1dx=mN−m⁢1m⁢(Nm)
69 61 62 63 lcmineqlem11 ⊢φ∧m∈ℤ∧1≤m∧m<N→1m+1⁢(Nm+1)=mN−m⁢1m⁢(Nm)
70 69 3adant3 ⊢φ∧m∈ℤ∧1≤m∧m<N∧∫01xm−1⁢1−xN−mdx=1m⁢(Nm)→1m+1⁢(Nm+1)=mN−m⁢1m⁢(Nm)
71 68 70 eqtr4d ⊢φ∧m∈ℤ∧1≤m∧m<N∧∫01xm−1⁢1−xN−mdx=1m⁢(Nm)→∫01xm+1-1⁢1−xN−m+1dx=1m+1⁢(Nm+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→∫01xM−1⁢1−xN−Mdx=1M⁢(NM)
76 8 75 mpdan ⊢φ→∫01xM−1⁢1−xN−Mdx=1M⁢(NM)
77 1 76 eqtrid ⊢φ→F=1M⁢(NM)