Metamath Proof Explorer

Theorem lcmineqlem18

Description: Technical lemma to shift factors in binomial coefficient. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypothesis lcmineqlem18.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion lcmineqlem18 ( 𝜑 → ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem18.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
3 2z ⊢ 2 ∈ ℤ
4 3 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
5 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
6 4 5 zmulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℤ )
7 6 peano2zd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℤ )
8 5 peano2zd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
9 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
10 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
11 1 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12 11 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
13 0le1 ⊢ 0 ≤ 1
14 13 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
15 9 10 12 14 addge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑁 + 1 ) )
16 9 10 readdcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ )
17 16 9 addge01d ⊢ ( 𝜑 → ( 0 ≤ 𝑁 ↔ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 𝑁 ) ) )
18 12 17 mpbid ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 𝑁 ) )
19 9 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
20 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
21 19 20 19 add32d ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) + 𝑁 ) = ( ( 𝑁 + 𝑁 ) + 1 ) )
22 19 2timesd ⊢ ( 𝜑 → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
23 22 oveq1d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) = ( ( 𝑁 + 𝑁 ) + 1 ) )
24 23 eqcomd ⊢ ( 𝜑 → ( ( 𝑁 + 𝑁 ) + 1 ) = ( ( 2 · 𝑁 ) + 1 ) )
25 21 24 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) + 𝑁 ) = ( ( 2 · 𝑁 ) + 1 ) )
26 18 25 breqtrd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≤ ( ( 2 · 𝑁 ) + 1 ) )
27 2 7 8 15 26 elfzd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 2 · 𝑁 ) + 1 ) ) )
28 bcval2 ⊢ ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 2 · 𝑁 ) + 1 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) − ( 𝑁 + 1 ) ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) )
29 27 28 syl ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) − ( 𝑁 + 1 ) ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) )
30 6 zcnd ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
31 30 20 19 20 addsub4d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) − ( 𝑁 + 1 ) ) = ( ( ( 2 · 𝑁 ) − 𝑁 ) + ( 1 − 1 ) ) )
32 22 oveq1d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) − 𝑁 ) = ( ( 𝑁 + 𝑁 ) − 𝑁 ) )
33 19 19 pncand ⊢ ( 𝜑 → ( ( 𝑁 + 𝑁 ) − 𝑁 ) = 𝑁 )
34 32 33 eqtrd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) − 𝑁 ) = 𝑁 )
35 1m1e0 ⊢ ( 1 − 1 ) = 0
36 35 a1i ⊢ ( 𝜑 → ( 1 − 1 ) = 0 )
37 34 36 oveq12d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) − 𝑁 ) + ( 1 − 1 ) ) = ( 𝑁 + 0 ) )
38 19 addid1d ⊢ ( 𝜑 → ( 𝑁 + 0 ) = 𝑁 )
39 37 38 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) − 𝑁 ) + ( 1 − 1 ) ) = 𝑁 )
40 31 39 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) − ( 𝑁 + 1 ) ) = 𝑁 )
41 40 fveq2d ⊢ ( 𝜑 → ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) − ( 𝑁 + 1 ) ) ) = ( ! ‘ 𝑁 ) )
42 41 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) − ( 𝑁 + 1 ) ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) = ( ( ! ‘ 𝑁 ) · ( ! ‘ ( 𝑁 + 1 ) ) ) )
43 42 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) − ( 𝑁 + 1 ) ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) )
44 29 43 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) )
45 faccl ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
46 11 45 syl ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℕ )
47 46 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℂ )
48 1nn0 ⊢ 1 ∈ ℕ0
49 48 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
50 11 49 nn0addcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
51 faccl ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ! ‘ ( 𝑁 + 1 ) ) ∈ ℕ )
52 50 51 syl ⊢ ( 𝜑 → ( ! ‘ ( 𝑁 + 1 ) ) ∈ ℕ )
53 52 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 𝑁 + 1 ) ) ∈ ℂ )
54 47 53 mulcomd ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) · ( ! ‘ ( 𝑁 + 1 ) ) ) = ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) )
55 facp1 ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )
56 11 55 syl ⊢ ( 𝜑 → ( ! ‘ ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )
57 19 20 addcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℂ )
58 47 57 mulcomd ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) = ( ( 𝑁 + 1 ) · ( ! ‘ 𝑁 ) ) )
59 56 58 eqtrd ⊢ ( 𝜑 → ( ! ‘ ( 𝑁 + 1 ) ) = ( ( 𝑁 + 1 ) · ( ! ‘ 𝑁 ) ) )
60 59 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) = ( ( ( 𝑁 + 1 ) · ( ! ‘ 𝑁 ) ) · ( ! ‘ 𝑁 ) ) )
61 57 47 47 mulassd ⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) · ( ! ‘ 𝑁 ) ) · ( ! ‘ 𝑁 ) ) = ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
62 60 61 eqtrd ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) = ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
63 54 62 eqtrd ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) · ( ! ‘ ( 𝑁 + 1 ) ) ) = ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
64 63 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
65 44 64 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
66 2nn0 ⊢ 2 ∈ ℕ0
67 66 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
68 67 11 nn0mulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ0 )
69 facp1 ⊢ ( ( 2 · 𝑁 ) ∈ ℕ0 → ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) = ( ( ! ‘ ( 2 · 𝑁 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) )
70 68 69 syl ⊢ ( 𝜑 → ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) = ( ( ! ‘ ( 2 · 𝑁 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) )
71 faccl ⊢ ( ( 2 · 𝑁 ) ∈ ℕ0 → ( ! ‘ ( 2 · 𝑁 ) ) ∈ ℕ )
72 68 71 syl ⊢ ( 𝜑 → ( ! ‘ ( 2 · 𝑁 ) ) ∈ ℕ )
73 72 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 2 · 𝑁 ) ) ∈ ℂ )
74 30 20 addcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
75 73 74 mulcomd ⊢ ( 𝜑 → ( ( ! ‘ ( 2 · 𝑁 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) )
76 70 75 eqtrd ⊢ ( 𝜑 → ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) )
77 76 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
78 65 77 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
79 78 oveq2d ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) ) = ( ( 𝑁 + 1 ) · ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) ) )
80 74 73 mulcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) ∈ ℂ )
81 47 47 mulcld ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ∈ ℂ )
82 57 81 mulcld ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ∈ ℂ )
83 1 peano2nnd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ )
84 83 nnne0d ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≠ 0 )
85 46 nnne0d ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ≠ 0 )
86 47 47 85 85 mulne0d ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ≠ 0 )
87 57 81 84 86 mulne0d ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ≠ 0 )
88 57 80 82 87 divassd ⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) = ( ( 𝑁 + 1 ) · ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) ) )
89 88 eqcomd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) ) = ( ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
90 79 89 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) ) = ( ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
91 57 57 80 81 84 86 divmuldivd ⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) / ( 𝑁 + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) = ( ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
92 91 eqcomd ⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) ) / ( ( 𝑁 + 1 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) = ( ( ( 𝑁 + 1 ) / ( 𝑁 + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
93 90 92 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) ) = ( ( ( 𝑁 + 1 ) / ( 𝑁 + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
94 57 84 dividd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) / ( 𝑁 + 1 ) ) = 1 )
95 94 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) / ( 𝑁 + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) = ( 1 · ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
96 80 81 86 divcld ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ∈ ℂ )
97 96 mulid2d ⊢ ( 𝜑 → ( 1 · ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
98 95 97 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) / ( 𝑁 + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
99 93 98 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
100 74 73 81 86 divassd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) + 1 ) · ( ! ‘ ( 2 · 𝑁 ) ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
101 99 100 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
102 9 9 addge01d ⊢ ( 𝜑 → ( 0 ≤ 𝑁 ↔ 𝑁 ≤ ( 𝑁 + 𝑁 ) ) )
103 22 breq2d ⊢ ( 𝜑 → ( 𝑁 ≤ ( 2 · 𝑁 ) ↔ 𝑁 ≤ ( 𝑁 + 𝑁 ) ) )
104 102 103 bitr4d ⊢ ( 𝜑 → ( 0 ≤ 𝑁 ↔ 𝑁 ≤ ( 2 · 𝑁 ) ) )
105 12 104 mpbid ⊢ ( 𝜑 → 𝑁 ≤ ( 2 · 𝑁 ) )
106 2 6 5 12 105 elfzd ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) )
107 bcval2 ⊢ ( 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) → ( ( 2 · 𝑁 ) C 𝑁 ) = ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ ( ( 2 · 𝑁 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
108 106 107 syl ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) = ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ ( ( 2 · 𝑁 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
109 34 fveq2d ⊢ ( 𝜑 → ( ! ‘ ( ( 2 · 𝑁 ) − 𝑁 ) ) = ( ! ‘ 𝑁 ) )
110 109 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) = ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) )
111 110 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ ( ( 2 · 𝑁 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) = ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
112 108 111 eqtrd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) = ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
113 112 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) )
114 113 eqcomd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) · ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) )
115 101 114 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) )