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	eqtrid	⊢ ( 𝜑 → 𝐹 = ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) )