Metamath Proof Explorer

Theorem lcmineqlem13

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

Ref Expression
Hypotheses lcmineqlem13.1 ⊢ 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥
lcmineqlem13.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
lcmineqlem13.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lcmineqlem13.4 ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
Assertion lcmineqlem13 ( 𝜑 → 𝐹 = ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem13.1 ⊢ 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥
2 lcmineqlem13.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 lcmineqlem13.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 lcmineqlem13.4 ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
5 2 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
6 nnge1 ⊢ ( 𝑀 ∈ ℕ → 1 ≤ 𝑀 )
7 2 6 syl ⊢ ( 𝜑 → 1 ≤ 𝑀 )
8 5 7 4 3jca ⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 1 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) )
9 oveq1 ⊢ ( 𝑖 = 1 → ( 𝑖 − 1 ) = ( 1 − 1 ) )
10 9 oveq2d ⊢ ( 𝑖 = 1 → ( 𝑥 ↑ ( 𝑖 − 1 ) ) = ( 𝑥 ↑ ( 1 − 1 ) ) )
11 oveq2 ⊢ ( 𝑖 = 1 → ( 𝑁 − 𝑖 ) = ( 𝑁 − 1 ) )
12 11 oveq2d ⊢ ( 𝑖 = 1 → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
13 10 12 oveq12d ⊢ ( 𝑖 = 1 → ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) = ( ( 𝑥 ↑ ( 1 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
14 13 adantr ⊢ ( ( 𝑖 = 1 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) = ( ( 𝑥 ↑ ( 1 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
15 14 itgeq2dv ⊢ ( 𝑖 = 1 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) d 𝑥 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 1 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) d 𝑥 )
16 id ⊢ ( 𝑖 = 1 → 𝑖 = 1 )
17 oveq2 ⊢ ( 𝑖 = 1 → ( 𝑁 C 𝑖 ) = ( 𝑁 C 1 ) )
18 16 17 oveq12d ⊢ ( 𝑖 = 1 → ( 𝑖 · ( 𝑁 C 𝑖 ) ) = ( 1 · ( 𝑁 C 1 ) ) )
19 18 oveq2d ⊢ ( 𝑖 = 1 → ( 1 / ( 𝑖 · ( 𝑁 C 𝑖 ) ) ) = ( 1 / ( 1 · ( 𝑁 C 1 ) ) ) )
20 15 19 eqeq12d ⊢ ( 𝑖 = 1 → ( ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) d 𝑥 = ( 1 / ( 𝑖 · ( 𝑁 C 𝑖 ) ) ) ↔ ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 1 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) d 𝑥 = ( 1 / ( 1 · ( 𝑁 C 1 ) ) ) ) )
21 oveq1 ⊢ ( 𝑖 = 𝑚 → ( 𝑖 − 1 ) = ( 𝑚 − 1 ) )
22 21 oveq2d ⊢ ( 𝑖 = 𝑚 → ( 𝑥 ↑ ( 𝑖 − 1 ) ) = ( 𝑥 ↑ ( 𝑚 − 1 ) ) )
23 oveq2 ⊢ ( 𝑖 = 𝑚 → ( 𝑁 − 𝑖 ) = ( 𝑁 − 𝑚 ) )
24 23 oveq2d ⊢ ( 𝑖 = 𝑚 → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) )
25 22 24 oveq12d ⊢ ( 𝑖 = 𝑚 → ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) = ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) )
26 25 adantr ⊢ ( ( 𝑖 = 𝑚 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) = ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) )
27 26 itgeq2dv ⊢ ( 𝑖 = 𝑚 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) d 𝑥 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) d 𝑥 )
28 id ⊢ ( 𝑖 = 𝑚 → 𝑖 = 𝑚 )
29 oveq2 ⊢ ( 𝑖 = 𝑚 → ( 𝑁 C 𝑖 ) = ( 𝑁 C 𝑚 ) )
30 28 29 oveq12d ⊢ ( 𝑖 = 𝑚 → ( 𝑖 · ( 𝑁 C 𝑖 ) ) = ( 𝑚 · ( 𝑁 C 𝑚 ) ) )
31 30 oveq2d ⊢ ( 𝑖 = 𝑚 → ( 1 / ( 𝑖 · ( 𝑁 C 𝑖 ) ) ) = ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) )
32 27 31 eqeq12d ⊢ ( 𝑖 = 𝑚 → ( ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) d 𝑥 = ( 1 / ( 𝑖 · ( 𝑁 C 𝑖 ) ) ) ↔ ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) d 𝑥 = ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) ) )
33 oveq1 ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( 𝑖 − 1 ) = ( ( 𝑚 + 1 ) − 1 ) )
34 33 oveq2d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( 𝑥 ↑ ( 𝑖 − 1 ) ) = ( 𝑥 ↑ ( ( 𝑚 + 1 ) − 1 ) ) )
35 oveq2 ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( 𝑁 − 𝑖 ) = ( 𝑁 − ( 𝑚 + 1 ) ) )
36 35 oveq2d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑚 + 1 ) ) ) )
37 34 36 oveq12d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) = ( ( 𝑥 ↑ ( ( 𝑚 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑚 + 1 ) ) ) ) )
38 37 adantr ⊢ ( ( 𝑖 = ( 𝑚 + 1 ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) = ( ( 𝑥 ↑ ( ( 𝑚 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑚 + 1 ) ) ) ) )
39 38 itgeq2dv ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) d 𝑥 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( ( 𝑚 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑚 + 1 ) ) ) ) d 𝑥 )
40 id ⊢ ( 𝑖 = ( 𝑚 + 1 ) → 𝑖 = ( 𝑚 + 1 ) )
41 oveq2 ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( 𝑁 C 𝑖 ) = ( 𝑁 C ( 𝑚 + 1 ) ) )
42 40 41 oveq12d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( 𝑖 · ( 𝑁 C 𝑖 ) ) = ( ( 𝑚 + 1 ) · ( 𝑁 C ( 𝑚 + 1 ) ) ) )
43 42 oveq2d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( 1 / ( 𝑖 · ( 𝑁 C 𝑖 ) ) ) = ( 1 / ( ( 𝑚 + 1 ) · ( 𝑁 C ( 𝑚 + 1 ) ) ) ) )
44 39 43 eqeq12d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) d 𝑥 = ( 1 / ( 𝑖 · ( 𝑁 C 𝑖 ) ) ) ↔ ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( ( 𝑚 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑚 + 1 ) ) ) ) d 𝑥 = ( 1 / ( ( 𝑚 + 1 ) · ( 𝑁 C ( 𝑚 + 1 ) ) ) ) ) )
45 oveq1 ⊢ ( 𝑖 = 𝑀 → ( 𝑖 − 1 ) = ( 𝑀 − 1 ) )
46 45 oveq2d ⊢ ( 𝑖 = 𝑀 → ( 𝑥 ↑ ( 𝑖 − 1 ) ) = ( 𝑥 ↑ ( 𝑀 − 1 ) ) )
47 oveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝑁 − 𝑖 ) = ( 𝑁 − 𝑀 ) )
48 47 oveq2d ⊢ ( 𝑖 = 𝑀 → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) )
49 46 48 oveq12d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) = ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) )
50 49 adantr ⊢ ( ( 𝑖 = 𝑀 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) = ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) )
51 50 itgeq2dv ⊢ ( 𝑖 = 𝑀 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) d 𝑥 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 )
52 id ⊢ ( 𝑖 = 𝑀 → 𝑖 = 𝑀 )
53 oveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝑁 C 𝑖 ) = ( 𝑁 C 𝑀 ) )
54 52 53 oveq12d ⊢ ( 𝑖 = 𝑀 → ( 𝑖 · ( 𝑁 C 𝑖 ) ) = ( 𝑀 · ( 𝑁 C 𝑀 ) ) )
55 54 oveq2d ⊢ ( 𝑖 = 𝑀 → ( 1 / ( 𝑖 · ( 𝑁 C 𝑖 ) ) ) = ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) )
56 51 55 eqeq12d ⊢ ( 𝑖 = 𝑀 → ( ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑖 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑖 ) ) ) d 𝑥 = ( 1 / ( 𝑖 · ( 𝑁 C 𝑖 ) ) ) ↔ ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 = ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) )
57 3 lcmineqlem12 ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 1 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) d 𝑥 = ( 1 / ( 1 · ( 𝑁 C 1 ) ) ) )
58 elnnz1 ⊢ ( 𝑚 ∈ ℕ ↔ ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ) )
59 58 biimpri ⊢ ( ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ) → 𝑚 ∈ ℕ )
60 59 3adant3 ⊢ ( ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) → 𝑚 ∈ ℕ )
61 60 adantl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) → 𝑚 ∈ ℕ )
62 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) → 𝑁 ∈ ℕ )
63 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) → 𝑚 < 𝑁 )
64 61 62 63 lcmineqlem10 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( ( 𝑚 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑚 + 1 ) ) ) ) d 𝑥 = ( ( 𝑚 / ( 𝑁 − 𝑚 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) d 𝑥 ) )
65 64 3adant3 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ∧ ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) d 𝑥 = ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) ) → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( ( 𝑚 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑚 + 1 ) ) ) ) d 𝑥 = ( ( 𝑚 / ( 𝑁 − 𝑚 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) d 𝑥 ) )
66 oveq2 ⊢ ( ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) d 𝑥 = ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) → ( ( 𝑚 / ( 𝑁 − 𝑚 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) d 𝑥 ) = ( ( 𝑚 / ( 𝑁 − 𝑚 ) ) · ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) ) )
67 66 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ∧ ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) d 𝑥 = ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) ) → ( ( 𝑚 / ( 𝑁 − 𝑚 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) d 𝑥 ) = ( ( 𝑚 / ( 𝑁 − 𝑚 ) ) · ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) ) )
68 65 67 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ∧ ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) d 𝑥 = ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) ) → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( ( 𝑚 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑚 + 1 ) ) ) ) d 𝑥 = ( ( 𝑚 / ( 𝑁 − 𝑚 ) ) · ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) ) )
69 61 62 63 lcmineqlem11 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) → ( 1 / ( ( 𝑚 + 1 ) · ( 𝑁 C ( 𝑚 + 1 ) ) ) ) = ( ( 𝑚 / ( 𝑁 − 𝑚 ) ) · ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) ) )
70 69 3adant3 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ∧ ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) d 𝑥 = ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) ) → ( 1 / ( ( 𝑚 + 1 ) · ( 𝑁 C ( 𝑚 + 1 ) ) ) ) = ( ( 𝑚 / ( 𝑁 − 𝑚 ) ) · ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) ) )
71 68 70 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ∧ ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑚 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑚 ) ) ) d 𝑥 = ( 1 / ( 𝑚 · ( 𝑁 C 𝑚 ) ) ) ) → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( ( 𝑚 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑚 + 1 ) ) ) ) d 𝑥 = ( 1 / ( ( 𝑚 + 1 ) · ( 𝑁 C ( 𝑚 + 1 ) ) ) ) )
72 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
73 3 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
74 3 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑁 )
75 20 32 44 56 57 71 72 73 74 fzindd ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ ℤ ∧ 1 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 = ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) )
76 8 75 mpdan ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 = ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) )
77 1 76 syl5eq ⊢ ( 𝜑 → 𝐹 = ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) )