Metamath Proof Explorer

Theorem 2np3bcnp1

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

Ref Expression
Hypothesis 2np3bcnp1.1 
|- ( ph -> N e. NN0 )
Assertion 2np3bcnp1 
|- ( ph -> ( ( ( 2 x. ( N + 1 ) ) + 1 ) _C ( N + 1 ) ) = ( ( ( ( 2 x. N ) + 1 ) _C N ) x. ( 2 x. ( ( ( 2 x. N ) + 3 ) / ( N + 2 ) ) ) ) )

Proof

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