Metamath Proof Explorer

Theorem iserodd

Description: Collect the odd terms in a sequence. (Contributed by Mario Carneiro, 7-Apr-2015) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Hypotheses iserodd.f 
|- ( ( ph /\ k e. NN0 ) -> C e. CC )
iserodd.h 
|- ( n = ( ( 2 x. k ) + 1 ) -> B = C )
Assertion iserodd 
|- ( ph -> ( seq 0 ( + , ( k e. NN0 |-> C ) ) ~~> A <-> seq 1 ( + , ( n e. NN |-> if ( 2 || n , 0 , B ) ) ) ~~> A ) )

Proof

Step Hyp Ref Expression
1 iserodd.f 
 |-  ( ( ph /\ k e. NN0 ) -> C e. CC )
2 iserodd.h 
 |-  ( n = ( ( 2 x. k ) + 1 ) -> B = C )
3 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 0zd 
 |-  ( ph -> 0 e. ZZ )
6 1zzd 
 |-  ( ph -> 1 e. ZZ )
7 2nn0 
 |-  2 e. NN0
8 7 a1i 
 |-  ( ph -> 2 e. NN0 )
9 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ m e. NN0 ) -> ( 2 x. m ) e. NN0 )
10 8 9 sylan 
 |-  ( ( ph /\ m e. NN0 ) -> ( 2 x. m ) e. NN0 )
11 nn0p1nn 
 |-  ( ( 2 x. m ) e. NN0 -> ( ( 2 x. m ) + 1 ) e. NN )
12 10 11 syl 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( 2 x. m ) + 1 ) e. NN )
13 12 fmpttd 
 |-  ( ph -> ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) : NN0 --> NN )
14 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ i e. NN0 ) -> ( 2 x. i ) e. NN0 )
15 8 14 sylan 
 |-  ( ( ph /\ i e. NN0 ) -> ( 2 x. i ) e. NN0 )
16 15 nn0red 
 |-  ( ( ph /\ i e. NN0 ) -> ( 2 x. i ) e. RR )
17 peano2nn0 
 |-  ( i e. NN0 -> ( i + 1 ) e. NN0 )
18 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ ( i + 1 ) e. NN0 ) -> ( 2 x. ( i + 1 ) ) e. NN0 )
19 8 17 18 syl2an 
 |-  ( ( ph /\ i e. NN0 ) -> ( 2 x. ( i + 1 ) ) e. NN0 )
20 19 nn0red 
 |-  ( ( ph /\ i e. NN0 ) -> ( 2 x. ( i + 1 ) ) e. RR )
21 1red 
 |-  ( ( ph /\ i e. NN0 ) -> 1 e. RR )
22 nn0re 
 |-  ( i e. NN0 -> i e. RR )
23 22 adantl 
 |-  ( ( ph /\ i e. NN0 ) -> i e. RR )
24 23 ltp1d 
 |-  ( ( ph /\ i e. NN0 ) -> i < ( i + 1 ) )
25 1red 
 |-  ( i e. NN0 -> 1 e. RR )
26 22 25 readdcld 
 |-  ( i e. NN0 -> ( i + 1 ) e. RR )
27 2rp 
 |-  2 e. RR+
28 27 a1i 
 |-  ( i e. NN0 -> 2 e. RR+ )
29 22 26 28 ltmul2d 
 |-  ( i e. NN0 -> ( i < ( i + 1 ) <-> ( 2 x. i ) < ( 2 x. ( i + 1 ) ) ) )
30 29 adantl 
 |-  ( ( ph /\ i e. NN0 ) -> ( i < ( i + 1 ) <-> ( 2 x. i ) < ( 2 x. ( i + 1 ) ) ) )
31 24 30 mpbid 
 |-  ( ( ph /\ i e. NN0 ) -> ( 2 x. i ) < ( 2 x. ( i + 1 ) ) )
32 16 20 21 31 ltadd1dd 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( 2 x. i ) + 1 ) < ( ( 2 x. ( i + 1 ) ) + 1 ) )
33 oveq2 
 |-  ( m = i -> ( 2 x. m ) = ( 2 x. i ) )
34 33 oveq1d 
 |-  ( m = i -> ( ( 2 x. m ) + 1 ) = ( ( 2 x. i ) + 1 ) )
35 eqid 
 |-  ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) = ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) )
36 ovex 
 |-  ( ( 2 x. i ) + 1 ) e. _V
37 34 35 36 fvmpt 
 |-  ( i e. NN0 -> ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` i ) = ( ( 2 x. i ) + 1 ) )
38 37 adantl 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` i ) = ( ( 2 x. i ) + 1 ) )
39 17 adantl 
 |-  ( ( ph /\ i e. NN0 ) -> ( i + 1 ) e. NN0 )
40 oveq2 
 |-  ( m = ( i + 1 ) -> ( 2 x. m ) = ( 2 x. ( i + 1 ) ) )
41 40 oveq1d 
 |-  ( m = ( i + 1 ) -> ( ( 2 x. m ) + 1 ) = ( ( 2 x. ( i + 1 ) ) + 1 ) )
42 ovex 
 |-  ( ( 2 x. ( i + 1 ) ) + 1 ) e. _V
43 41 35 42 fvmpt 
 |-  ( ( i + 1 ) e. NN0 -> ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` ( i + 1 ) ) = ( ( 2 x. ( i + 1 ) ) + 1 ) )
44 39 43 syl 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` ( i + 1 ) ) = ( ( 2 x. ( i + 1 ) ) + 1 ) )
45 32 38 44 3brtr4d 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` i ) < ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` ( i + 1 ) ) )
46 eldifi 
 |-  ( n e. ( NN \ ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) -> n e. NN )
47 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
48 0cnd 
 |-  ( ( ( ph /\ n e. NN ) /\ 2 || n ) -> 0 e. CC )
49 nnz 
 |-  ( n e. NN -> n e. ZZ )
50 49 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. ZZ )
51 odd2np1 
 |-  ( n e. ZZ -> ( -. 2 || n <-> E. k e. ZZ ( ( 2 x. k ) + 1 ) = n ) )
52 50 51 syl 
 |-  ( ( ph /\ n e. NN ) -> ( -. 2 || n <-> E. k e. ZZ ( ( 2 x. k ) + 1 ) = n ) )
53 simprl 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> k e. ZZ )
54 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
55 54 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( n - 1 ) e. NN0 )
56 55 nn0red 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( n - 1 ) e. RR )
57 27 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> 2 e. RR+ )
58 55 nn0ge0d 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> 0 <_ ( n - 1 ) )
59 56 57 58 divge0d 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> 0 <_ ( ( n - 1 ) / 2 ) )
60 simprr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( ( 2 x. k ) + 1 ) = n )
61 60 oveq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( ( ( 2 x. k ) + 1 ) - 1 ) = ( n - 1 ) )
62 2cn 
 |-  2 e. CC
63 zcn 
 |-  ( k e. ZZ -> k e. CC )
64 63 ad2antrl 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> k e. CC )
65 mulcl 
 |-  ( ( 2 e. CC /\ k e. CC ) -> ( 2 x. k ) e. CC )
66 62 64 65 sylancr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( 2 x. k ) e. CC )
67 ax-1cn 
 |-  1 e. CC
68 pncan 
 |-  ( ( ( 2 x. k ) e. CC /\ 1 e. CC ) -> ( ( ( 2 x. k ) + 1 ) - 1 ) = ( 2 x. k ) )
69 66 67 68 sylancl 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( ( ( 2 x. k ) + 1 ) - 1 ) = ( 2 x. k ) )
70 61 69 eqtr3d 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( n - 1 ) = ( 2 x. k ) )
71 70 oveq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( ( n - 1 ) / 2 ) = ( ( 2 x. k ) / 2 ) )
72 2cnd 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> 2 e. CC )
73 2ne0 
 |-  2 =/= 0
74 73 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> 2 =/= 0 )
75 64 72 74 divcan3d 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( ( 2 x. k ) / 2 ) = k )
76 71 75 eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( ( n - 1 ) / 2 ) = k )
77 59 76 breqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> 0 <_ k )
78 elnn0z 
 |-  ( k e. NN0 <-> ( k e. ZZ /\ 0 <_ k ) )
79 53 77 78 sylanbrc 
 |-  ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> k e. NN0 )
80 79 ex 
 |-  ( ( ph /\ n e. NN ) -> ( ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) -> k e. NN0 ) )
81 simpr 
 |-  ( ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) -> ( ( 2 x. k ) + 1 ) = n )
82 81 eqcomd 
 |-  ( ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) -> n = ( ( 2 x. k ) + 1 ) )
83 80 82 jca2 
 |-  ( ( ph /\ n e. NN ) -> ( ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) -> ( k e. NN0 /\ n = ( ( 2 x. k ) + 1 ) ) ) )
84 83 reximdv2 
 |-  ( ( ph /\ n e. NN ) -> ( E. k e. ZZ ( ( 2 x. k ) + 1 ) = n -> E. k e. NN0 n = ( ( 2 x. k ) + 1 ) ) )
85 52 84 sylbid 
 |-  ( ( ph /\ n e. NN ) -> ( -. 2 || n -> E. k e. NN0 n = ( ( 2 x. k ) + 1 ) ) )
86 2 eleq1d 
 |-  ( n = ( ( 2 x. k ) + 1 ) -> ( B e. CC <-> C e. CC ) )
87 1 86 syl5ibrcom 
 |-  ( ( ph /\ k e. NN0 ) -> ( n = ( ( 2 x. k ) + 1 ) -> B e. CC ) )
88 87 rexlimdva 
 |-  ( ph -> ( E. k e. NN0 n = ( ( 2 x. k ) + 1 ) -> B e. CC ) )
89 88 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( E. k e. NN0 n = ( ( 2 x. k ) + 1 ) -> B e. CC ) )
90 85 89 syld 
 |-  ( ( ph /\ n e. NN ) -> ( -. 2 || n -> B e. CC ) )
91 90 imp 
 |-  ( ( ( ph /\ n e. NN ) /\ -. 2 || n ) -> B e. CC )
92 48 91 ifclda 
 |-  ( ( ph /\ n e. NN ) -> if ( 2 || n , 0 , B ) e. CC )
93 eqid 
 |-  ( n e. NN |-> if ( 2 || n , 0 , B ) ) = ( n e. NN |-> if ( 2 || n , 0 , B ) )
94 93 fvmpt2 
 |-  ( ( n e. NN /\ if ( 2 || n , 0 , B ) e. CC ) -> ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` n ) = if ( 2 || n , 0 , B ) )
95 47 92 94 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` n ) = if ( 2 || n , 0 , B ) )
96 46 95 sylan2 
 |-  ( ( ph /\ n e. ( NN \ ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) ) -> ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` n ) = if ( 2 || n , 0 , B ) )
97 eldif 
 |-  ( n e. ( NN \ ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) <-> ( n e. NN /\ -. n e. ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) )
98 oveq2 
 |-  ( m = k -> ( 2 x. m ) = ( 2 x. k ) )
99 98 oveq1d 
 |-  ( m = k -> ( ( 2 x. m ) + 1 ) = ( ( 2 x. k ) + 1 ) )
100 99 cbvmptv 
 |-  ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) = ( k e. NN0 |-> ( ( 2 x. k ) + 1 ) )
101 100 elrnmpt 
 |-  ( n e. _V -> ( n e. ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) <-> E. k e. NN0 n = ( ( 2 x. k ) + 1 ) ) )
102 101 elv 
 |-  ( n e. ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) <-> E. k e. NN0 n = ( ( 2 x. k ) + 1 ) )
103 85 102 imbitrrdi 
 |-  ( ( ph /\ n e. NN ) -> ( -. 2 || n -> n e. ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) )
104 103 con1d 
 |-  ( ( ph /\ n e. NN ) -> ( -. n e. ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) -> 2 || n ) )
105 104 impr 
 |-  ( ( ph /\ ( n e. NN /\ -. n e. ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) ) -> 2 || n )
106 97 105 sylan2b 
 |-  ( ( ph /\ n e. ( NN \ ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) ) -> 2 || n )
107 106 iftrued 
 |-  ( ( ph /\ n e. ( NN \ ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) ) -> if ( 2 || n , 0 , B ) = 0 )
108 96 107 eqtrd 
 |-  ( ( ph /\ n e. ( NN \ ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) ) -> ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` n ) = 0 )
109 108 ralrimiva 
 |-  ( ph -> A. n e. ( NN \ ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` n ) = 0 )
110 nfv 
 |-  F/ j ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` n ) = 0
111 nffvmpt1 
 |-  F/_ n ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` j )
112 111 nfeq1 
 |-  F/ n ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` j ) = 0
113 fveqeq2 
 |-  ( n = j -> ( ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` n ) = 0 <-> ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` j ) = 0 ) )
114 110 112 113 cbvralw 
 |-  ( A. n e. ( NN \ ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` n ) = 0 <-> A. j e. ( NN \ ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` j ) = 0 )
115 109 114 sylib 
 |-  ( ph -> A. j e. ( NN \ ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` j ) = 0 )
116 115 r19.21bi 
 |-  ( ( ph /\ j e. ( NN \ ran ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ) ) -> ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` j ) = 0 )
117 92 fmpttd 
 |-  ( ph -> ( n e. NN |-> if ( 2 || n , 0 , B ) ) : NN --> CC )
118 117 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` j ) e. CC )
119 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
120 eqid 
 |-  ( k e. NN0 |-> C ) = ( k e. NN0 |-> C )
121 120 fvmpt2 
 |-  ( ( k e. NN0 /\ C e. CC ) -> ( ( k e. NN0 |-> C ) ` k ) = C )
122 119 1 121 syl2anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( k e. NN0 |-> C ) ` k ) = C )
123 ovex 
 |-  ( ( 2 x. k ) + 1 ) e. _V
124 99 35 123 fvmpt 
 |-  ( k e. NN0 -> ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` k ) = ( ( 2 x. k ) + 1 ) )
125 124 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` k ) = ( ( 2 x. k ) + 1 ) )
126 125 fveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` k ) ) = ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( 2 x. k ) + 1 ) ) )
127 breq2 
 |-  ( n = ( ( 2 x. k ) + 1 ) -> ( 2 || n <-> 2 || ( ( 2 x. k ) + 1 ) ) )
128 127 2 ifbieq2d 
 |-  ( n = ( ( 2 x. k ) + 1 ) -> if ( 2 || n , 0 , B ) = if ( 2 || ( ( 2 x. k ) + 1 ) , 0 , C ) )
129 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ k e. NN0 ) -> ( 2 x. k ) e. NN0 )
130 8 129 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( 2 x. k ) e. NN0 )
131 nn0p1nn 
 |-  ( ( 2 x. k ) e. NN0 -> ( ( 2 x. k ) + 1 ) e. NN )
132 130 131 syl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( 2 x. k ) + 1 ) e. NN )
133 2z 
 |-  2 e. ZZ
134 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
135 134 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> k e. ZZ )
136 dvdsmul1 
 |-  ( ( 2 e. ZZ /\ k e. ZZ ) -> 2 || ( 2 x. k ) )
137 133 135 136 sylancr 
 |-  ( ( ph /\ k e. NN0 ) -> 2 || ( 2 x. k ) )
138 130 nn0zd 
 |-  ( ( ph /\ k e. NN0 ) -> ( 2 x. k ) e. ZZ )
139 2nn 
 |-  2 e. NN
140 139 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> 2 e. NN )
141 1lt2 
 |-  1 < 2
142 141 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> 1 < 2 )
143 ndvdsp1 
 |-  ( ( ( 2 x. k ) e. ZZ /\ 2 e. NN /\ 1 < 2 ) -> ( 2 || ( 2 x. k ) -> -. 2 || ( ( 2 x. k ) + 1 ) ) )
144 138 140 142 143 syl3anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( 2 || ( 2 x. k ) -> -. 2 || ( ( 2 x. k ) + 1 ) ) )
145 137 144 mpd 
 |-  ( ( ph /\ k e. NN0 ) -> -. 2 || ( ( 2 x. k ) + 1 ) )
146 145 iffalsed 
 |-  ( ( ph /\ k e. NN0 ) -> if ( 2 || ( ( 2 x. k ) + 1 ) , 0 , C ) = C )
147 146 1 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> if ( 2 || ( ( 2 x. k ) + 1 ) , 0 , C ) e. CC )
148 93 128 132 147 fvmptd3 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( 2 x. k ) + 1 ) ) = if ( 2 || ( ( 2 x. k ) + 1 ) , 0 , C ) )
149 126 148 146 3eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` k ) ) = C )
150 122 149 eqtr4d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( k e. NN0 |-> C ) ` k ) = ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` k ) ) )
151 150 ralrimiva 
 |-  ( ph -> A. k e. NN0 ( ( k e. NN0 |-> C ) ` k ) = ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` k ) ) )
152 nfv 
 |-  F/ i ( ( k e. NN0 |-> C ) ` k ) = ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` k ) )
153 nffvmpt1 
 |-  F/_ k ( ( k e. NN0 |-> C ) ` i )
154 153 nfeq1 
 |-  F/ k ( ( k e. NN0 |-> C ) ` i ) = ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` i ) )
155 fveq2 
 |-  ( k = i -> ( ( k e. NN0 |-> C ) ` k ) = ( ( k e. NN0 |-> C ) ` i ) )
156 2fveq3 
 |-  ( k = i -> ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` k ) ) = ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` i ) ) )
157 155 156 eqeq12d 
 |-  ( k = i -> ( ( ( k e. NN0 |-> C ) ` k ) = ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` k ) ) <-> ( ( k e. NN0 |-> C ) ` i ) = ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` i ) ) ) )
158 152 154 157 cbvralw 
 |-  ( A. k e. NN0 ( ( k e. NN0 |-> C ) ` k ) = ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` k ) ) <-> A. i e. NN0 ( ( k e. NN0 |-> C ) ` i ) = ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` i ) ) )
159 151 158 sylib 
 |-  ( ph -> A. i e. NN0 ( ( k e. NN0 |-> C ) ` i ) = ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` i ) ) )
160 159 r19.21bi 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( k e. NN0 |-> C ) ` i ) = ( ( n e. NN |-> if ( 2 || n , 0 , B ) ) ` ( ( m e. NN0 |-> ( ( 2 x. m ) + 1 ) ) ` i ) ) )
161 3 4 5 6 13 45 116 118 160 isercoll2 
 |-  ( ph -> ( seq 0 ( + , ( k e. NN0 |-> C ) ) ~~> A <-> seq 1 ( + , ( n e. NN |-> if ( 2 || n , 0 , B ) ) ) ~~> A ) )