Metamath Proof Explorer

Theorem 2np3bcnp1

Description: Part of induction step for 2ap1caineq . (Contributed by metakunt, 8-Jun-2024)

Ref Expression
Hypothesis 2np3bcnp1.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion 2np3bcnp1 ( 𝜑 → ( ( ( 2 · ( 𝑁 + 1 ) ) + 1 ) C ( 𝑁 + 1 ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) · ( 2 · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 2np3bcnp1.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
3 1 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
4 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
5 2 3 4 adddid ⊢ ( 𝜑 → ( 2 · ( 𝑁 + 1 ) ) = ( ( 2 · 𝑁 ) + ( 2 · 1 ) ) )
6 2t1e2 ⊢ ( 2 · 1 ) = 2
7 6 oveq2i ⊢ ( ( 2 · 𝑁 ) + ( 2 · 1 ) ) = ( ( 2 · 𝑁 ) + 2 )
8 5 7 eqtrdi ⊢ ( 𝜑 → ( 2 · ( 𝑁 + 1 ) ) = ( ( 2 · 𝑁 ) + 2 ) )
9 8 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( 𝑁 + 1 ) ) + 1 ) = ( ( ( 2 · 𝑁 ) + 2 ) + 1 ) )
10 2 3 mulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
11 10 2 4 addassd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 2 ) + 1 ) = ( ( 2 · 𝑁 ) + ( 2 + 1 ) ) )
12 9 11 eqtrd ⊢ ( 𝜑 → ( ( 2 · ( 𝑁 + 1 ) ) + 1 ) = ( ( 2 · 𝑁 ) + ( 2 + 1 ) ) )
13 2p1e3 ⊢ ( 2 + 1 ) = 3
14 13 a1i ⊢ ( 𝜑 → ( 2 + 1 ) = 3 )
15 14 oveq2d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + ( 2 + 1 ) ) = ( ( 2 · 𝑁 ) + 3 ) )
16 12 15 eqtrd ⊢ ( 𝜑 → ( ( 2 · ( 𝑁 + 1 ) ) + 1 ) = ( ( 2 · 𝑁 ) + 3 ) )
17 16 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑁 + 1 ) ) + 1 ) C ( 𝑁 + 1 ) ) = ( ( ( 2 · 𝑁 ) + 3 ) C ( 𝑁 + 1 ) ) )
18 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
19 2z ⊢ 2 ∈ ℤ
20 19 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
21 1 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
22 20 21 zmulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℤ )
23 3z ⊢ 3 ∈ ℤ
24 23 a1i ⊢ ( 𝜑 → 3 ∈ ℤ )
25 22 24 zaddcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 3 ) ∈ ℤ )
26 21 peano2zd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
27 1 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
28 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
29 1 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
30 0le1 ⊢ 0 ≤ 1
31 30 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
32 27 28 29 31 addge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑁 + 1 ) )
33 2re ⊢ 2 ∈ ℝ
34 33 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
35 34 27 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
36 3re ⊢ 3 ∈ ℝ
37 36 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
38 1le2 ⊢ 1 ≤ 2
39 38 a1i ⊢ ( 𝜑 → 1 ≤ 2 )
40 27 34 29 39 lemulge12d ⊢ ( 𝜑 → 𝑁 ≤ ( 2 · 𝑁 ) )
41 1le3 ⊢ 1 ≤ 3
42 41 a1i ⊢ ( 𝜑 → 1 ≤ 3 )
43 27 28 35 37 40 42 le2addd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≤ ( ( 2 · 𝑁 ) + 3 ) )
44 18 25 26 32 43 elfzd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 2 · 𝑁 ) + 3 ) ) )
45 bcval2 ⊢ ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 2 · 𝑁 ) + 3 ) ) → ( ( ( 2 · 𝑁 ) + 3 ) C ( 𝑁 + 1 ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 3 ) − ( 𝑁 + 1 ) ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) )
46 44 45 syl ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 3 ) C ( 𝑁 + 1 ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 3 ) − ( 𝑁 + 1 ) ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) )
47 37 recnd ⊢ ( 𝜑 → 3 ∈ ℂ )
48 10 47 3 4 addsub4d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 3 ) − ( 𝑁 + 1 ) ) = ( ( ( 2 · 𝑁 ) − 𝑁 ) + ( 3 − 1 ) ) )
49 2txmxeqx ⊢ ( 𝑁 ∈ ℂ → ( ( 2 · 𝑁 ) − 𝑁 ) = 𝑁 )
50 3 49 syl ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) − 𝑁 ) = 𝑁 )
51 3m1e2 ⊢ ( 3 − 1 ) = 2
52 51 a1i ⊢ ( 𝜑 → ( 3 − 1 ) = 2 )
53 50 52 oveq12d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) − 𝑁 ) + ( 3 − 1 ) ) = ( 𝑁 + 2 ) )
54 48 53 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 3 ) − ( 𝑁 + 1 ) ) = ( 𝑁 + 2 ) )
55 54 fveq2d ⊢ ( 𝜑 → ( ! ‘ ( ( ( 2 · 𝑁 ) + 3 ) − ( 𝑁 + 1 ) ) ) = ( ! ‘ ( 𝑁 + 2 ) ) )
56 55 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 3 ) − ( 𝑁 + 1 ) ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) = ( ( ! ‘ ( 𝑁 + 2 ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) )
57 56 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 3 ) − ( 𝑁 + 1 ) ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) / ( ( ! ‘ ( 𝑁 + 2 ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) )
58 2nn0 ⊢ 2 ∈ ℕ0
59 58 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
60 1 59 nn0addcld ⊢ ( 𝜑 → ( 𝑁 + 2 ) ∈ ℕ0 )
61 60 faccld ⊢ ( 𝜑 → ( ! ‘ ( 𝑁 + 2 ) ) ∈ ℕ )
62 61 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 𝑁 + 2 ) ) ∈ ℂ )
63 1nn0 ⊢ 1 ∈ ℕ0
64 63 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
65 1 64 nn0addcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
66 65 faccld ⊢ ( 𝜑 → ( ! ‘ ( 𝑁 + 1 ) ) ∈ ℕ )
67 66 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 𝑁 + 1 ) ) ∈ ℂ )
68 62 67 mulcomd ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑁 + 2 ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) = ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ ( 𝑁 + 2 ) ) ) )
69 68 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) / ( ( ! ‘ ( 𝑁 + 2 ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ ( 𝑁 + 2 ) ) ) ) )
70 10 4 2 addassd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) + 2 ) = ( ( 2 · 𝑁 ) + ( 1 + 2 ) ) )
71 1p2e3 ⊢ ( 1 + 2 ) = 3
72 71 oveq2i ⊢ ( ( 2 · 𝑁 ) + ( 1 + 2 ) ) = ( ( 2 · 𝑁 ) + 3 )
73 70 72 eqtrdi ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) + 2 ) = ( ( 2 · 𝑁 ) + 3 ) )
74 73 fveq2d ⊢ ( 𝜑 → ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) + 2 ) ) = ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) )
75 74 eqcomd ⊢ ( 𝜑 → ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) = ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) + 2 ) ) )
76 59 1 nn0mulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ0 )
77 76 64 nn0addcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ0 )
78 facp2 ⊢ ( ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ0 → ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) + 2 ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) + 2 ) ) ) )
79 77 78 syl ⊢ ( 𝜑 → ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) + 2 ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) + 2 ) ) ) )
80 75 79 eqtrd ⊢ ( 𝜑 → ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) + 2 ) ) ) )
81 10 4 4 addassd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) + 1 ) = ( ( 2 · 𝑁 ) + ( 1 + 1 ) ) )
82 1p1e2 ⊢ ( 1 + 1 ) = 2
83 82 a1i ⊢ ( 𝜑 → ( 1 + 1 ) = 2 )
84 83 oveq2d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + ( 1 + 1 ) ) = ( ( 2 · 𝑁 ) + 2 ) )
85 81 84 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) + 1 ) = ( ( 2 · 𝑁 ) + 2 ) )
86 71 a1i ⊢ ( 𝜑 → ( 1 + 2 ) = 3 )
87 86 oveq2d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + ( 1 + 2 ) ) = ( ( 2 · 𝑁 ) + 3 ) )
88 70 87 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) + 2 ) = ( ( 2 · 𝑁 ) + 3 ) )
89 85 88 oveq12d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) + 1 ) + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) + 2 ) ) = ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) )
90 89 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) + 2 ) ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ) )
91 80 90 eqtrd ⊢ ( 𝜑 → ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ) )
92 91 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ ( 𝑁 + 2 ) ) ) ) = ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ ( 𝑁 + 2 ) ) ) ) )
93 facp2 ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ ( 𝑁 + 2 ) ) = ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) )
94 1 93 syl ⊢ ( 𝜑 → ( ! ‘ ( 𝑁 + 2 ) ) = ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) )
95 94 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ ( 𝑁 + 2 ) ) ) = ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) )
96 95 oveq2d ⊢ ( 𝜑 → ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ ( 𝑁 + 2 ) ) ) ) = ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) ) )
97 1 faccld ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℕ )
98 97 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℂ )
99 3 4 addcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℂ )
100 3 2 addcld ⊢ ( 𝜑 → ( 𝑁 + 2 ) ∈ ℂ )
101 99 100 mulcld ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ∈ ℂ )
102 67 98 101 mulassd ⊢ ( 𝜑 → ( ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) = ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) )
103 102 eqcomd ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) = ( ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) )
104 103 oveq2d ⊢ ( 𝜑 → ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) ) = ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ) / ( ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) )
105 77 faccld ⊢ ( 𝜑 → ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
106 105 nncnd ⊢ ( 𝜑 → ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
107 67 98 mulcld ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) ∈ ℂ )
108 10 2 addcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 2 ) ∈ ℂ )
109 10 47 addcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 3 ) ∈ ℂ )
110 108 109 mulcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ∈ ℂ )
111 66 nnne0d ⊢ ( 𝜑 → ( ! ‘ ( 𝑁 + 1 ) ) ≠ 0 )
112 97 nnne0d ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ≠ 0 )
113 67 98 111 112 mulne0d ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) ≠ 0 )
114 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
115 27 28 readdcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ )
116 27 ltp1d ⊢ ( 𝜑 → 𝑁 < ( 𝑁 + 1 ) )
117 114 27 115 29 116 lelttrd ⊢ ( 𝜑 → 0 < ( 𝑁 + 1 ) )
118 114 117 ltned ⊢ ( 𝜑 → 0 ≠ ( 𝑁 + 1 ) )
119 118 necomd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≠ 0 )
120 27 34 readdcld ⊢ ( 𝜑 → ( 𝑁 + 2 ) ∈ ℝ )
121 2rp ⊢ 2 ∈ ℝ+
122 121 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
123 27 122 ltaddrpd ⊢ ( 𝜑 → 𝑁 < ( 𝑁 + 2 ) )
124 114 27 120 29 123 lelttrd ⊢ ( 𝜑 → 0 < ( 𝑁 + 2 ) )
125 114 124 ltned ⊢ ( 𝜑 → 0 ≠ ( 𝑁 + 2 ) )
126 125 necomd ⊢ ( 𝜑 → ( 𝑁 + 2 ) ≠ 0 )
127 99 100 119 126 mulne0d ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ≠ 0 )
128 106 107 110 101 113 127 divmuldivd ⊢ ( 𝜑 → ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) ) · ( ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) / ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) = ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ) / ( ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) )
129 128 eqcomd ⊢ ( 𝜑 → ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ) / ( ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) = ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) ) · ( ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) / ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) )
130 22 peano2zd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℤ )
131 35 28 readdcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
132 35 lep1d ⊢ ( 𝜑 → ( 2 · 𝑁 ) ≤ ( ( 2 · 𝑁 ) + 1 ) )
133 27 35 131 40 132 letrd ⊢ ( 𝜑 → 𝑁 ≤ ( ( 2 · 𝑁 ) + 1 ) )
134 18 130 21 29 133 elfzd ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... ( ( 2 · 𝑁 ) + 1 ) ) )
135 bcval2 ⊢ ( 𝑁 ∈ ( 0 ... ( ( 2 · 𝑁 ) + 1 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
136 134 135 syl ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
137 10 4 3 addsubd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) − 𝑁 ) = ( ( ( 2 · 𝑁 ) − 𝑁 ) + 1 ) )
138 50 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) − 𝑁 ) + 1 ) = ( 𝑁 + 1 ) )
139 137 138 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) − 𝑁 ) = ( 𝑁 + 1 ) )
140 139 fveq2d ⊢ ( 𝜑 → ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) − 𝑁 ) ) = ( ! ‘ ( 𝑁 + 1 ) ) )
141 140 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) = ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) )
142 141 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 1 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) ) )
143 136 142 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) = ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) ) )
144 143 eqcomd ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) )
145 108 99 109 100 119 126 divmuldivd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) + 2 ) / ( 𝑁 + 1 ) ) · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) = ( ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) / ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) )
146 145 eqcomd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) / ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) = ( ( ( ( 2 · 𝑁 ) + 2 ) / ( 𝑁 + 1 ) ) · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) )
147 8 eqcomd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 2 ) = ( 2 · ( 𝑁 + 1 ) ) )
148 147 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 2 ) / ( 𝑁 + 1 ) ) = ( ( 2 · ( 𝑁 + 1 ) ) / ( 𝑁 + 1 ) ) )
149 2 99 119 divcan4d ⊢ ( 𝜑 → ( ( 2 · ( 𝑁 + 1 ) ) / ( 𝑁 + 1 ) ) = 2 )
150 148 149 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 2 ) / ( 𝑁 + 1 ) ) = 2 )
151 eqidd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) = ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) )
152 150 151 oveq12d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) + 2 ) / ( 𝑁 + 1 ) ) · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) = ( 2 · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) )
153 146 152 eqtrd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) / ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) = ( 2 · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) )
154 144 153 oveq12d ⊢ ( 𝜑 → ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) ) · ( ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) / ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) · ( 2 · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) ) )
155 129 154 eqtrd ⊢ ( 𝜑 → ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ) / ( ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ 𝑁 ) ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) · ( 2 · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) ) )
156 104 155 eqtrd ⊢ ( 𝜑 → ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ( ! ‘ 𝑁 ) · ( ( 𝑁 + 1 ) · ( 𝑁 + 2 ) ) ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) · ( 2 · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) ) )
157 96 156 eqtrd ⊢ ( 𝜑 → ( ( ( ! ‘ ( ( 2 · 𝑁 ) + 1 ) ) · ( ( ( 2 · 𝑁 ) + 2 ) · ( ( 2 · 𝑁 ) + 3 ) ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ ( 𝑁 + 2 ) ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) · ( 2 · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) ) )
158 92 157 eqtrd ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) / ( ( ! ‘ ( 𝑁 + 1 ) ) · ( ! ‘ ( 𝑁 + 2 ) ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) · ( 2 · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) ) )
159 69 158 eqtrd ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) / ( ( ! ‘ ( 𝑁 + 2 ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) · ( 2 · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) ) )
160 57 159 eqtrd ⊢ ( 𝜑 → ( ( ! ‘ ( ( 2 · 𝑁 ) + 3 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) + 3 ) − ( 𝑁 + 1 ) ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) · ( 2 · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) ) )
161 46 160 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 3 ) C ( 𝑁 + 1 ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) · ( 2 · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) ) )
162 17 161 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑁 + 1 ) ) + 1 ) C ( 𝑁 + 1 ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) · ( 2 · ( ( ( 2 · 𝑁 ) + 3 ) / ( 𝑁 + 2 ) ) ) ) )