Metamath Proof Explorer


Theorem poimirlem4

Description: Lemma for poimir connecting the admissible faces on the back face of the ( M + 1 ) -cube to admissible simplices in the M -cube. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 φ N
poimirlem4.1 φ K
poimirlem4.2 φ M 0
poimirlem4.3 φ M < N
Assertion poimirlem4 φ s 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M | i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M × 0 M + 1 N × 0 / p B s 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 | i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st s M + 1 = 0 2 nd s M + 1 = M + 1

Proof

Step Hyp Ref Expression
1 poimir.0 φ N
2 poimirlem4.1 φ K
3 poimirlem4.2 φ M 0
4 poimirlem4.3 φ M < N
5 1 adantr φ t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M N
6 2 adantr φ t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M K
7 3 adantr φ t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M M 0
8 4 adantr φ t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M M < N
9 xp1st t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M 1 st t 0 ..^ K 1 M
10 elmapi 1 st t 0 ..^ K 1 M 1 st t : 1 M 0 ..^ K
11 9 10 syl t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M 1 st t : 1 M 0 ..^ K
12 11 adantl φ t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M 1 st t : 1 M 0 ..^ K
13 xp2nd t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M 2 nd t f | f : 1 M 1-1 onto 1 M
14 fvex 2 nd t V
15 f1oeq1 f = 2 nd t f : 1 M 1-1 onto 1 M 2 nd t : 1 M 1-1 onto 1 M
16 14 15 elab 2 nd t f | f : 1 M 1-1 onto 1 M 2 nd t : 1 M 1-1 onto 1 M
17 13 16 sylib t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M 2 nd t : 1 M 1-1 onto 1 M
18 17 adantl φ t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M 2 nd t : 1 M 1-1 onto 1 M
19 5 6 7 8 12 18 poimirlem3 φ t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M i 0 M j 0 M i = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 M × 0 M + 1 N × 0 / p B 1 st t M + 1 0 2 nd t M + 1 M + 1 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 i 0 M j 0 M i = 1 st t M + 1 0 + f 2 nd t M + 1 M + 1 1 j × 1 2 nd t M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st t M + 1 0 M + 1 = 0 2 nd t M + 1 M + 1 M + 1 = M + 1
20 fvex 1 st t V
21 snex M + 1 0 V
22 20 21 unex 1 st t M + 1 0 V
23 snex M + 1 M + 1 V
24 14 23 unex 2 nd t M + 1 M + 1 V
25 22 24 op1std s = 1 st t M + 1 0 2 nd t M + 1 M + 1 1 st s = 1 st t M + 1 0
26 22 24 op2ndd s = 1 st t M + 1 0 2 nd t M + 1 M + 1 2 nd s = 2 nd t M + 1 M + 1
27 26 imaeq1d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 2 nd s 1 j = 2 nd t M + 1 M + 1 1 j
28 27 xpeq1d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 2 nd s 1 j × 1 = 2 nd t M + 1 M + 1 1 j × 1
29 26 imaeq1d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 2 nd s j + 1 M + 1 = 2 nd t M + 1 M + 1 j + 1 M + 1
30 29 xpeq1d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 2 nd s j + 1 M + 1 × 0 = 2 nd t M + 1 M + 1 j + 1 M + 1 × 0
31 28 30 uneq12d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 = 2 nd t M + 1 M + 1 1 j × 1 2 nd t M + 1 M + 1 j + 1 M + 1 × 0
32 25 31 oveq12d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 = 1 st t M + 1 0 + f 2 nd t M + 1 M + 1 1 j × 1 2 nd t M + 1 M + 1 j + 1 M + 1 × 0
33 32 uneq1d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 = 1 st t M + 1 0 + f 2 nd t M + 1 M + 1 1 j × 1 2 nd t M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0
34 33 csbeq1d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B = 1 st t M + 1 0 + f 2 nd t M + 1 M + 1 1 j × 1 2 nd t M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B
35 34 eqeq2d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B i = 1 st t M + 1 0 + f 2 nd t M + 1 M + 1 1 j × 1 2 nd t M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B
36 35 rexbidv s = 1 st t M + 1 0 2 nd t M + 1 M + 1 j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B j 0 M i = 1 st t M + 1 0 + f 2 nd t M + 1 M + 1 1 j × 1 2 nd t M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B
37 36 ralbidv s = 1 st t M + 1 0 2 nd t M + 1 M + 1 i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B i 0 M j 0 M i = 1 st t M + 1 0 + f 2 nd t M + 1 M + 1 1 j × 1 2 nd t M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B
38 25 fveq1d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 1 st s M + 1 = 1 st t M + 1 0 M + 1
39 38 eqeq1d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 1 st s M + 1 = 0 1 st t M + 1 0 M + 1 = 0
40 26 fveq1d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 2 nd s M + 1 = 2 nd t M + 1 M + 1 M + 1
41 40 eqeq1d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 2 nd s M + 1 = M + 1 2 nd t M + 1 M + 1 M + 1 = M + 1
42 37 39 41 3anbi123d s = 1 st t M + 1 0 2 nd t M + 1 M + 1 i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st s M + 1 = 0 2 nd s M + 1 = M + 1 i 0 M j 0 M i = 1 st t M + 1 0 + f 2 nd t M + 1 M + 1 1 j × 1 2 nd t M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st t M + 1 0 M + 1 = 0 2 nd t M + 1 M + 1 M + 1 = M + 1
43 42 elrab 1 st t M + 1 0 2 nd t M + 1 M + 1 s 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 | i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st s M + 1 = 0 2 nd s M + 1 = M + 1 1 st t M + 1 0 2 nd t M + 1 M + 1 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 i 0 M j 0 M i = 1 st t M + 1 0 + f 2 nd t M + 1 M + 1 1 j × 1 2 nd t M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st t M + 1 0 M + 1 = 0 2 nd t M + 1 M + 1 M + 1 = M + 1
44 19 43 syl6ibr φ t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M i 0 M j 0 M i = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 M × 0 M + 1 N × 0 / p B 1 st t M + 1 0 2 nd t M + 1 M + 1 s 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 | i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st s M + 1 = 0 2 nd s M + 1 = M + 1
45 44 ralrimiva φ t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M i 0 M j 0 M i = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 M × 0 M + 1 N × 0 / p B 1 st t M + 1 0 2 nd t M + 1 M + 1 s 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 | i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st s M + 1 = 0 2 nd s M + 1 = M + 1
46 fveq2 s = t 1 st s = 1 st t
47 fveq2 s = t 2 nd s = 2 nd t
48 47 imaeq1d s = t 2 nd s 1 j = 2 nd t 1 j
49 48 xpeq1d s = t 2 nd s 1 j × 1 = 2 nd t 1 j × 1
50 47 imaeq1d s = t 2 nd s j + 1 M = 2 nd t j + 1 M
51 50 xpeq1d s = t 2 nd s j + 1 M × 0 = 2 nd t j + 1 M × 0
52 49 51 uneq12d s = t 2 nd s 1 j × 1 2 nd s j + 1 M × 0 = 2 nd t 1 j × 1 2 nd t j + 1 M × 0
53 46 52 oveq12d s = t 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M × 0 = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 M × 0
54 53 uneq1d s = t 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M × 0 M + 1 N × 0 = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 M × 0 M + 1 N × 0
55 54 csbeq1d s = t 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M × 0 M + 1 N × 0 / p B = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 M × 0 M + 1 N × 0 / p B
56 55 eqeq2d s = t i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M × 0 M + 1 N × 0 / p B i = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 M × 0 M + 1 N × 0 / p B
57 56 rexbidv s = t j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M × 0 M + 1 N × 0 / p B j 0 M i = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 M × 0 M + 1 N × 0 / p B
58 57 ralbidv s = t i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M × 0 M + 1 N × 0 / p B i 0 M j 0 M i = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 M × 0 M + 1 N × 0 / p B
59 58 ralrab t s 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M | i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M × 0 M + 1 N × 0 / p B 1 st t M + 1 0 2 nd t M + 1 M + 1 s 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 | i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st s M + 1 = 0 2 nd s M + 1 = M + 1 t 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M i 0 M j 0 M i = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 M × 0 M + 1 N × 0 / p B 1 st t M + 1 0 2 nd t M + 1 M + 1 s 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 | i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st s M + 1 = 0 2 nd s M + 1 = M + 1
60 45 59 sylibr φ t s 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M | i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M × 0 M + 1 N × 0 / p B 1 st t M + 1 0 2 nd t M + 1 M + 1 s 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 | i 0 M j 0 M i = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st s M + 1 = 0 2 nd s M + 1 = M + 1
61 xp1st k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k 0 ..^ K 1 M + 1
62 elmapi 1 st k 0 ..^ K 1 M + 1 1 st k : 1 M + 1 0 ..^ K
63 61 62 syl k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k : 1 M + 1 0 ..^ K
64 fzssp1 1 M 1 M + 1
65 fssres 1 st k : 1 M + 1 0 ..^ K 1 M 1 M + 1 1 st k 1 M : 1 M 0 ..^ K
66 63 64 65 sylancl k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k 1 M : 1 M 0 ..^ K
67 ovex 0 ..^ K V
68 ovex 1 M V
69 67 68 elmap 1 st k 1 M 0 ..^ K 1 M 1 st k 1 M : 1 M 0 ..^ K
70 66 69 sylibr k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k 1 M 0 ..^ K 1 M
71 70 ad2antlr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 1 st k 1 M 0 ..^ K 1 M
72 xp2nd k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k f | f : 1 M + 1 1-1 onto 1 M + 1
73 fvex 2 nd k V
74 f1oeq1 f = 2 nd k f : 1 M + 1 1-1 onto 1 M + 1 2 nd k : 1 M + 1 1-1 onto 1 M + 1
75 73 74 elab 2 nd k f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k : 1 M + 1 1-1 onto 1 M + 1
76 72 75 sylib k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k : 1 M + 1 1-1 onto 1 M + 1
77 f1of1 2 nd k : 1 M + 1 1-1 onto 1 M + 1 2 nd k : 1 M + 1 1-1 1 M + 1
78 76 77 syl k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k : 1 M + 1 1-1 1 M + 1
79 f1ores 2 nd k : 1 M + 1 1-1 1 M + 1 1 M 1 M + 1 2 nd k 1 M : 1 M 1-1 onto 2 nd k 1 M
80 78 64 79 sylancl k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k 1 M : 1 M 1-1 onto 2 nd k 1 M
81 80 ad2antlr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k 1 M : 1 M 1-1 onto 2 nd k 1 M
82 dff1o3 2 nd k : 1 M + 1 1-1 onto 1 M + 1 2 nd k : 1 M + 1 onto 1 M + 1 Fun 2 nd k -1
83 82 simprbi 2 nd k : 1 M + 1 1-1 onto 1 M + 1 Fun 2 nd k -1
84 imadif Fun 2 nd k -1 2 nd k 1 M + 1 M + 1 = 2 nd k 1 M + 1 2 nd k M + 1
85 76 83 84 3syl k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k 1 M + 1 M + 1 = 2 nd k 1 M + 1 2 nd k M + 1
86 85 ad2antlr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k 1 M + 1 M + 1 = 2 nd k 1 M + 1 2 nd k M + 1
87 f1ofo 2 nd k : 1 M + 1 1-1 onto 1 M + 1 2 nd k : 1 M + 1 onto 1 M + 1
88 foima 2 nd k : 1 M + 1 onto 1 M + 1 2 nd k 1 M + 1 = 1 M + 1
89 76 87 88 3syl k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k 1 M + 1 = 1 M + 1
90 89 ad2antlr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k 1 M + 1 = 1 M + 1
91 f1ofn 2 nd k : 1 M + 1 1-1 onto 1 M + 1 2 nd k Fn 1 M + 1
92 76 91 syl k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k Fn 1 M + 1
93 nn0p1nn M 0 M + 1
94 3 93 syl φ M + 1
95 elfz1end M + 1 M + 1 1 M + 1
96 94 95 sylib φ M + 1 1 M + 1
97 fnsnfv 2 nd k Fn 1 M + 1 M + 1 1 M + 1 2 nd k M + 1 = 2 nd k M + 1
98 92 96 97 syl2anr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = 2 nd k M + 1
99 sneq 2 nd k M + 1 = M + 1 2 nd k M + 1 = M + 1
100 98 99 sylan9req φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k M + 1 = M + 1
101 90 100 difeq12d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k 1 M + 1 2 nd k M + 1 = 1 M + 1 M + 1
102 86 101 eqtrd φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k 1 M + 1 M + 1 = 1 M + 1 M + 1
103 1z 1
104 nn0uz 0 = 0
105 1m1e0 1 1 = 0
106 105 fveq2i 1 1 = 0
107 104 106 eqtr4i 0 = 1 1
108 3 107 eleqtrdi φ M 1 1
109 fzsuc2 1 M 1 1 1 M + 1 = 1 M M + 1
110 103 108 109 sylancr φ 1 M + 1 = 1 M M + 1
111 110 difeq1d φ 1 M + 1 M + 1 = 1 M M + 1 M + 1
112 difun2 1 M M + 1 M + 1 = 1 M M + 1
113 111 112 syl6eq φ 1 M + 1 M + 1 = 1 M M + 1
114 3 nn0red φ M
115 ltp1 M M < M + 1
116 peano2re M M + 1
117 ltnle M M + 1 M < M + 1 ¬ M + 1 M
118 116 117 mpdan M M < M + 1 ¬ M + 1 M
119 115 118 mpbid M ¬ M + 1 M
120 114 119 syl φ ¬ M + 1 M
121 elfzle2 M + 1 1 M M + 1 M
122 120 121 nsyl φ ¬ M + 1 1 M
123 difsn ¬ M + 1 1 M 1 M M + 1 = 1 M
124 122 123 syl φ 1 M M + 1 = 1 M
125 113 124 eqtrd φ 1 M + 1 M + 1 = 1 M
126 125 imaeq2d φ 2 nd k 1 M + 1 M + 1 = 2 nd k 1 M
127 126 ad2antrr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k 1 M + 1 M + 1 = 2 nd k 1 M
128 125 ad2antrr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 1 M + 1 M + 1 = 1 M
129 102 127 128 3eqtr3d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k 1 M = 1 M
130 f1oeq3 2 nd k 1 M = 1 M 2 nd k 1 M : 1 M 1-1 onto 2 nd k 1 M 2 nd k 1 M : 1 M 1-1 onto 1 M
131 129 130 syl φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k 1 M : 1 M 1-1 onto 2 nd k 1 M 2 nd k 1 M : 1 M 1-1 onto 1 M
132 81 131 mpbid φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k 1 M : 1 M 1-1 onto 1 M
133 73 resex 2 nd k 1 M V
134 f1oeq1 f = 2 nd k 1 M f : 1 M 1-1 onto 1 M 2 nd k 1 M : 1 M 1-1 onto 1 M
135 133 134 elab 2 nd k 1 M f | f : 1 M 1-1 onto 1 M 2 nd k 1 M : 1 M 1-1 onto 1 M
136 132 135 sylibr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k 1 M f | f : 1 M 1-1 onto 1 M
137 opelxpi 1 st k 1 M 0 ..^ K 1 M 2 nd k 1 M f | f : 1 M 1-1 onto 1 M 1 st k 1 M 2 nd k 1 M 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M
138 71 136 137 syl2anc φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 1 st k 1 M 2 nd k 1 M 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M
139 138 3ad2antr3 φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 i 0 M j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 1 st k 1 M 2 nd k 1 M 0 ..^ K 1 M × f | f : 1 M 1-1 onto 1 M
140 3anass i 0 M j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 i 0 M j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st k M + 1 = 0 2 nd k M + 1 = M + 1
141 ancom i 0 M j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 i 0 M j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B
142 140 141 bitri i 0 M j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 i 0 M j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B
143 94 nnzd φ M + 1
144 uzid M + 1 M + 1 M + 1
145 peano2uz M + 1 M + 1 M + 1 + 1 M + 1
146 143 144 145 3syl φ M + 1 + 1 M + 1
147 3 nn0zd φ M
148 1 nnzd φ N
149 zltp1le M N M < N M + 1 N
150 peano2z M M + 1
151 eluz M + 1 N N M + 1 M + 1 N
152 150 151 sylan M N N M + 1 M + 1 N
153 149 152 bitr4d M N M < N N M + 1
154 147 148 153 syl2anc φ M < N N M + 1
155 4 154 mpbid φ N M + 1
156 fzsplit2 M + 1 + 1 M + 1 N M + 1 M + 1 N = M + 1 M + 1 M + 1 + 1 N
157 146 155 156 syl2anc φ M + 1 N = M + 1 M + 1 M + 1 + 1 N
158 fzsn M + 1 M + 1 M + 1 = M + 1
159 143 158 syl φ M + 1 M + 1 = M + 1
160 159 uneq1d φ M + 1 M + 1 M + 1 + 1 N = M + 1 M + 1 + 1 N
161 157 160 eqtrd φ M + 1 N = M + 1 M + 1 + 1 N
162 161 xpeq1d φ M + 1 N × 0 = M + 1 M + 1 + 1 N × 0
163 162 uneq2d φ n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 N × 0 = n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 M + 1 + 1 N × 0
164 xpundir M + 1 M + 1 + 1 N × 0 = M + 1 × 0 M + 1 + 1 N × 0
165 ovex M + 1 V
166 c0ex 0 V
167 165 166 xpsn M + 1 × 0 = M + 1 0
168 167 uneq1i M + 1 × 0 M + 1 + 1 N × 0 = M + 1 0 M + 1 + 1 N × 0
169 164 168 eqtri M + 1 M + 1 + 1 N × 0 = M + 1 0 M + 1 + 1 N × 0
170 169 uneq2i n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 M + 1 + 1 N × 0 = n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 0 M + 1 + 1 N × 0
171 unass n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 0 M + 1 + 1 N × 0 = n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 0 M + 1 + 1 N × 0
172 170 171 eqtr4i n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 M + 1 + 1 N × 0 = n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 0 M + 1 + 1 N × 0
173 163 172 syl6eq φ n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 N × 0 = n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 0 M + 1 + 1 N × 0
174 173 ad3antrrr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 N × 0 = n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 0 M + 1 + 1 N × 0
175 165 a1i φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M M + 1 V
176 166 a1i φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M 0 V
177 110 eqcomd φ 1 M M + 1 = 1 M + 1
178 177 ad3antrrr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M 1 M M + 1 = 1 M + 1
179 fveq2 n = M + 1 1 st k n = 1 st k M + 1
180 fveq2 n = M + 1 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n = 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1
181 179 180 oveq12d n = M + 1 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n = 1 st k M + 1 + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1
182 simplrl φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M 1 st k M + 1 = 0
183 imain Fun 2 nd k -1 2 nd k 1 j j + 1 M + 1 = 2 nd k 1 j 2 nd k j + 1 M + 1
184 76 83 183 3syl k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k 1 j j + 1 M + 1 = 2 nd k 1 j 2 nd k j + 1 M + 1
185 184 ad2antlr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k 1 j j + 1 M + 1 = 2 nd k 1 j 2 nd k j + 1 M + 1
186 elfznn0 j 0 M j 0
187 186 nn0red j 0 M j
188 187 ltp1d j 0 M j < j + 1
189 fzdisj j < j + 1 1 j j + 1 M + 1 =
190 188 189 syl j 0 M 1 j j + 1 M + 1 =
191 190 imaeq2d j 0 M 2 nd k 1 j j + 1 M + 1 = 2 nd k
192 ima0 2 nd k =
193 191 192 syl6eq j 0 M 2 nd k 1 j j + 1 M + 1 =
194 185 193 sylan9req φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 j 2 nd k j + 1 M + 1 =
195 simplr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k M + 1 = M + 1
196 92 ad2antlr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k Fn 1 M + 1
197 nn0p1nn j 0 j + 1
198 nnuz = 1
199 197 198 eleqtrdi j 0 j + 1 1
200 fzss1 j + 1 1 j + 1 M + 1 1 M + 1
201 186 199 200 3syl j 0 M j + 1 M + 1 1 M + 1
202 elfzuz3 j 0 M M j
203 eluzp1p1 M j M + 1 j + 1
204 eluzfz2 M + 1 j + 1 M + 1 j + 1 M + 1
205 202 203 204 3syl j 0 M M + 1 j + 1 M + 1
206 201 205 jca j 0 M j + 1 M + 1 1 M + 1 M + 1 j + 1 M + 1
207 fnfvima 2 nd k Fn 1 M + 1 j + 1 M + 1 1 M + 1 M + 1 j + 1 M + 1 2 nd k M + 1 2 nd k j + 1 M + 1
208 207 3expb 2 nd k Fn 1 M + 1 j + 1 M + 1 1 M + 1 M + 1 j + 1 M + 1 2 nd k M + 1 2 nd k j + 1 M + 1
209 196 206 208 syl2an φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k M + 1 2 nd k j + 1 M + 1
210 195 209 eqeltrrd φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M M + 1 2 nd k j + 1 M + 1
211 1ex 1 V
212 fnconstg 1 V 2 nd k 1 j × 1 Fn 2 nd k 1 j
213 211 212 ax-mp 2 nd k 1 j × 1 Fn 2 nd k 1 j
214 fnconstg 0 V 2 nd k j + 1 M + 1 × 0 Fn 2 nd k j + 1 M + 1
215 166 214 ax-mp 2 nd k j + 1 M + 1 × 0 Fn 2 nd k j + 1 M + 1
216 fvun2 2 nd k 1 j × 1 Fn 2 nd k 1 j 2 nd k j + 1 M + 1 × 0 Fn 2 nd k j + 1 M + 1 2 nd k 1 j 2 nd k j + 1 M + 1 = M + 1 2 nd k j + 1 M + 1 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 = 2 nd k j + 1 M + 1 × 0 M + 1
217 213 215 216 mp3an12 2 nd k 1 j 2 nd k j + 1 M + 1 = M + 1 2 nd k j + 1 M + 1 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 = 2 nd k j + 1 M + 1 × 0 M + 1
218 194 210 217 syl2anc φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 = 2 nd k j + 1 M + 1 × 0 M + 1
219 166 fvconst2 M + 1 2 nd k j + 1 M + 1 2 nd k j + 1 M + 1 × 0 M + 1 = 0
220 210 219 syl φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k j + 1 M + 1 × 0 M + 1 = 0
221 218 220 eqtrd φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 = 0
222 221 adantlrl φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 = 0
223 182 222 oveq12d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M 1 st k M + 1 + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 = 0 + 0
224 00id 0 + 0 = 0
225 223 224 syl6eq φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M 1 st k M + 1 + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 = 0
226 181 225 sylan9eqr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M n = M + 1 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n = 0
227 175 176 178 226 fmptapd φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 0 = n 1 M + 1 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n
228 227 uneq1d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 0 M + 1 + 1 N × 0 = n 1 M + 1 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 + 1 N × 0
229 174 228 eqtrd φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 N × 0 = n 1 M + 1 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 + 1 N × 0
230 elmapfn 1 st k 0 ..^ K 1 M + 1 1 st k Fn 1 M + 1
231 61 230 syl k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k Fn 1 M + 1
232 fnssres 1 st k Fn 1 M + 1 1 M 1 M + 1 1 st k 1 M Fn 1 M
233 231 64 232 sylancl k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k 1 M Fn 1 M
234 233 ad3antlr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 1 st k 1 M Fn 1 M
235 simplr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1
236 fnconstg 0 V 2 nd k j + 1 M × 0 Fn 2 nd k j + 1 M
237 166 236 ax-mp 2 nd k j + 1 M × 0 Fn 2 nd k j + 1 M
238 213 237 pm3.2i 2 nd k 1 j × 1 Fn 2 nd k 1 j 2 nd k j + 1 M × 0 Fn 2 nd k j + 1 M
239 imain Fun 2 nd k -1 2 nd k 1 j j + 1 M = 2 nd k 1 j 2 nd k j + 1 M
240 76 83 239 3syl k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k 1 j j + 1 M = 2 nd k 1 j 2 nd k j + 1 M
241 fzdisj j < j + 1 1 j j + 1 M =
242 188 241 syl j 0 M 1 j j + 1 M =
243 242 imaeq2d j 0 M 2 nd k 1 j j + 1 M = 2 nd k
244 243 192 syl6eq j 0 M 2 nd k 1 j j + 1 M =
245 240 244 sylan9req k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 2 nd k 1 j 2 nd k j + 1 M =
246 fnun 2 nd k 1 j × 1 Fn 2 nd k 1 j 2 nd k j + 1 M × 0 Fn 2 nd k j + 1 M 2 nd k 1 j 2 nd k j + 1 M = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 Fn 2 nd k 1 j 2 nd k j + 1 M
247 238 245 246 sylancr k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M × 0 Fn 2 nd k 1 j 2 nd k j + 1 M
248 235 247 sylan φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M × 0 Fn 2 nd k 1 j 2 nd k j + 1 M
249 101 adantr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 M + 1 2 nd k M + 1 = 1 M + 1 M + 1
250 85 ad3antlr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 M + 1 M + 1 = 2 nd k 1 M + 1 2 nd k M + 1
251 186 197 syl j 0 M j + 1
252 251 198 eleqtrdi j 0 M j + 1 1
253 fzsplit2 j + 1 1 M j 1 M = 1 j j + 1 M
254 252 202 253 syl2anc j 0 M 1 M = 1 j j + 1 M
255 128 254 sylan9eq φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 1 M + 1 M + 1 = 1 j j + 1 M
256 255 imaeq2d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 M + 1 M + 1 = 2 nd k 1 j j + 1 M
257 250 256 eqtr3d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 M + 1 2 nd k M + 1 = 2 nd k 1 j j + 1 M
258 125 ad3antrrr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 1 M + 1 M + 1 = 1 M
259 249 257 258 3eqtr3rd φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 1 M = 2 nd k 1 j j + 1 M
260 imaundi 2 nd k 1 j j + 1 M = 2 nd k 1 j 2 nd k j + 1 M
261 259 260 syl6eq φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 1 M = 2 nd k 1 j 2 nd k j + 1 M
262 261 fneq2d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M × 0 Fn 1 M 2 nd k 1 j × 1 2 nd k j + 1 M × 0 Fn 2 nd k 1 j 2 nd k j + 1 M
263 248 262 mpbird φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M × 0 Fn 1 M
264 fzss2 M j 1 j 1 M
265 resima2 1 j 1 M 2 nd k 1 M 1 j = 2 nd k 1 j
266 202 264 265 3syl j 0 M 2 nd k 1 M 1 j = 2 nd k 1 j
267 266 xpeq1d j 0 M 2 nd k 1 M 1 j × 1 = 2 nd k 1 j × 1
268 186 199 syl j 0 M j + 1 1
269 fzss1 j + 1 1 j + 1 M 1 M
270 resima2 j + 1 M 1 M 2 nd k 1 M j + 1 M = 2 nd k j + 1 M
271 268 269 270 3syl j 0 M 2 nd k 1 M j + 1 M = 2 nd k j + 1 M
272 271 xpeq1d j 0 M 2 nd k 1 M j + 1 M × 0 = 2 nd k j + 1 M × 0
273 267 272 uneq12d j 0 M 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 = 2 nd k 1 j × 1 2 nd k j + 1 M × 0
274 273 adantl φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 = 2 nd k 1 j × 1 2 nd k j + 1 M × 0
275 274 fneq1d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 Fn 1 M 2 nd k 1 j × 1 2 nd k j + 1 M × 0 Fn 1 M
276 263 275 mpbird φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 Fn 1 M
277 fzfid φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 1 M Fin
278 inidm 1 M 1 M = 1 M
279 fvres n 1 M 1 st k 1 M n = 1 st k n
280 279 adantl φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M n 1 M 1 st k 1 M n = 1 st k n
281 disjsn 1 M M + 1 = ¬ M + 1 1 M
282 122 281 sylibr φ 1 M M + 1 =
283 282 ad3antrrr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 1 M M + 1 =
284 263 283 jca φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M × 0 Fn 1 M 1 M M + 1 =
285 fnconstg 0 V M + 1 × 0 Fn M + 1
286 166 285 ax-mp M + 1 × 0 Fn M + 1
287 fvun1 2 nd k 1 j × 1 2 nd k j + 1 M × 0 Fn 1 M M + 1 × 0 Fn M + 1 1 M M + 1 = n 1 M 2 nd k 1 j × 1 2 nd k j + 1 M × 0 M + 1 × 0 n = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 n
288 286 287 mp3an2 2 nd k 1 j × 1 2 nd k j + 1 M × 0 Fn 1 M 1 M M + 1 = n 1 M 2 nd k 1 j × 1 2 nd k j + 1 M × 0 M + 1 × 0 n = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 n
289 288 anassrs 2 nd k 1 j × 1 2 nd k j + 1 M × 0 Fn 1 M 1 M M + 1 = n 1 M 2 nd k 1 j × 1 2 nd k j + 1 M × 0 M + 1 × 0 n = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 n
290 284 289 sylan φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M n 1 M 2 nd k 1 j × 1 2 nd k j + 1 M × 0 M + 1 × 0 n = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 n
291 251 nnzd j 0 M j + 1
292 186 nn0cnd j 0 M j
293 pncan1 j j + 1 - 1 = j
294 292 293 syl j 0 M j + 1 - 1 = j
295 294 fveq2d j 0 M j + 1 - 1 = j
296 202 295 eleqtrrd j 0 M M j + 1 - 1
297 fzsuc2 j + 1 M j + 1 - 1 j + 1 M + 1 = j + 1 M M + 1
298 291 296 297 syl2anc j 0 M j + 1 M + 1 = j + 1 M M + 1
299 298 imaeq2d j 0 M 2 nd k j + 1 M + 1 = 2 nd k j + 1 M M + 1
300 imaundi 2 nd k j + 1 M M + 1 = 2 nd k j + 1 M 2 nd k M + 1
301 299 300 syl6eq j 0 M 2 nd k j + 1 M + 1 = 2 nd k j + 1 M 2 nd k M + 1
302 301 xpeq1d j 0 M 2 nd k j + 1 M + 1 × 0 = 2 nd k j + 1 M 2 nd k M + 1 × 0
303 xpundir 2 nd k j + 1 M 2 nd k M + 1 × 0 = 2 nd k j + 1 M × 0 2 nd k M + 1 × 0
304 302 303 syl6eq j 0 M 2 nd k j + 1 M + 1 × 0 = 2 nd k j + 1 M × 0 2 nd k M + 1 × 0
305 304 uneq2d j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 2 nd k M + 1 × 0
306 unass 2 nd k 1 j × 1 2 nd k j + 1 M × 0 2 nd k M + 1 × 0 = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 2 nd k M + 1 × 0
307 305 306 syl6eqr j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 2 nd k M + 1 × 0
308 307 adantl φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 2 nd k M + 1 × 0
309 98 xpeq1d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 × 0 = 2 nd k M + 1 × 0
310 309 uneq2d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k 1 j × 1 2 nd k j + 1 M × 0 2 nd k M + 1 × 0 = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 2 nd k M + 1 × 0
311 310 adantr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M × 0 2 nd k M + 1 × 0 = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 2 nd k M + 1 × 0
312 308 311 eqtr4d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 2 nd k M + 1 × 0
313 99 xpeq1d 2 nd k M + 1 = M + 1 2 nd k M + 1 × 0 = M + 1 × 0
314 313 uneq2d 2 nd k M + 1 = M + 1 2 nd k 1 j × 1 2 nd k j + 1 M × 0 2 nd k M + 1 × 0 = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 M + 1 × 0
315 312 314 sylan9eq φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 2 nd k M + 1 = M + 1 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 M + 1 × 0
316 315 an32s φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 M + 1 × 0
317 316 fveq1d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 M + 1 × 0 n
318 317 adantr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M n 1 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 M + 1 × 0 n
319 273 fveq1d j 0 M 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 n = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 n
320 319 ad2antlr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M n 1 M 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 n = 2 nd k 1 j × 1 2 nd k j + 1 M × 0 n
321 290 318 320 3eqtr4rd φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M n 1 M 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 n = 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n
322 234 276 277 277 278 280 321 offval φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 1 st k 1 M + f 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 = n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n
323 322 uneq1d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 j 0 M 1 st k 1 M + f 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 M + 1 N × 0 = n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 N × 0
324 323 adantlrl φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M 1 st k 1 M + f 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 M + 1 N × 0 = n 1 M 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 N × 0
325 simplr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1
326 231 adantr k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 1 st k Fn 1 M + 1
327 213 215 pm3.2i 2 nd k 1 j × 1 Fn 2 nd k 1 j 2 nd k j + 1 M + 1 × 0 Fn 2 nd k j + 1 M + 1
328 184 193 sylan9req k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 2 nd k 1 j 2 nd k j + 1 M + 1 =
329 fnun 2 nd k 1 j × 1 Fn 2 nd k 1 j 2 nd k j + 1 M + 1 × 0 Fn 2 nd k j + 1 M + 1 2 nd k 1 j 2 nd k j + 1 M + 1 = 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 Fn 2 nd k 1 j 2 nd k j + 1 M + 1
330 327 328 329 sylancr k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 Fn 2 nd k 1 j 2 nd k j + 1 M + 1
331 peano2uz M j M + 1 j
332 202 331 syl j 0 M M + 1 j
333 fzsplit2 j + 1 1 M + 1 j 1 M + 1 = 1 j j + 1 M + 1
334 268 332 333 syl2anc j 0 M 1 M + 1 = 1 j j + 1 M + 1
335 334 imaeq2d j 0 M 2 nd k 1 M + 1 = 2 nd k 1 j j + 1 M + 1
336 imaundi 2 nd k 1 j j + 1 M + 1 = 2 nd k 1 j 2 nd k j + 1 M + 1
337 335 336 syl6req j 0 M 2 nd k 1 j 2 nd k j + 1 M + 1 = 2 nd k 1 M + 1
338 337 89 sylan9eqr k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 2 nd k 1 j 2 nd k j + 1 M + 1 = 1 M + 1
339 338 fneq2d k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 Fn 2 nd k 1 j 2 nd k j + 1 M + 1 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 Fn 1 M + 1
340 330 339 mpbid k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 Fn 1 M + 1
341 fzfid k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 1 M + 1 Fin
342 inidm 1 M + 1 1 M + 1 = 1 M + 1
343 eqidd k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M n 1 M + 1 1 st k n = 1 st k n
344 eqidd k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M n 1 M + 1 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n = 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n
345 326 340 341 341 342 343 344 offval k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 = n 1 M + 1 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n
346 345 uneq1d k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 j 0 M 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 = n 1 M + 1 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 + 1 N × 0
347 325 346 sylan φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 = n 1 M + 1 1 st k n + 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 n M + 1 + 1 N × 0
348 229 324 347 3eqtr4rd φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 = 1 st k 1 M + f 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 M + 1 N × 0
349 348 csbeq1d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B = 1 st k 1 M + f 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 M + 1 N × 0 / p B
350 349 eqeq2d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B i = 1 st k 1 M + f 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 M + 1 N × 0 / p B
351 350 rexbidva φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B j 0 M i = 1 st k 1 M + f 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 M + 1 N × 0 / p B
352 351 ralbidv φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 i 0 M j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B i 0 M j 0 M i = 1 st k 1 M + f 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 M + 1 N × 0 / p B
353 352 biimpd φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 i 0 M j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B i 0 M j 0 M i = 1 st k 1 M + f 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 M + 1 N × 0 / p B
354 353 impr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 i 0 M j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B i 0 M j 0 M i = 1 st k 1 M + f 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 M + 1 N × 0 / p B
355 142 354 sylan2b φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 i 0 M j 0 M i = 1 st k + f 2 nd k 1 j × 1 2 nd k j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 i 0 M j 0 M i = 1 st k 1 M + f 2 nd k 1 M 1 j × 1 2 nd k 1 M j + 1 M × 0 M + 1 N × 0 / p B
356 1st2nd2 k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 k = 1 st k 2 nd k
357 356 ad2antlr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 k = 1 st k 2 nd k
358 fnsnsplit 1 st k Fn 1 M + 1 M + 1 1 M + 1 1 st k = 1 st k 1 M + 1 M + 1 M + 1 1 st k M + 1
359 231 96 358 syl2anr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k = 1 st k 1 M + 1 M + 1 M + 1 1 st k M + 1
360 359 adantr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 1 st k = 1 st k 1 M + 1 M + 1 M + 1 1 st k M + 1
361 125 reseq2d φ 1 st k 1 M + 1 M + 1 = 1 st k 1 M
362 361 adantr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k 1 M + 1 M + 1 = 1 st k 1 M
363 opeq2 1 st k M + 1 = 0 M + 1 1 st k M + 1 = M + 1 0
364 363 sneqd 1 st k M + 1 = 0 M + 1 1 st k M + 1 = M + 1 0
365 uneq12 1 st k 1 M + 1 M + 1 = 1 st k 1 M M + 1 1 st k M + 1 = M + 1 0 1 st k 1 M + 1 M + 1 M + 1 1 st k M + 1 = 1 st k 1 M M + 1 0
366 362 364 365 syl2an φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 1 st k 1 M + 1 M + 1 M + 1 1 st k M + 1 = 1 st k 1 M M + 1 0
367 360 366 eqtrd φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 1 st k = 1 st k 1 M M + 1 0
368 367 adantrr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 1 st k = 1 st k 1 M M + 1 0
369 fnsnsplit 2 nd k Fn 1 M + 1 M + 1 1 M + 1 2 nd k = 2 nd k 1 M + 1 M + 1 M + 1 2 nd k M + 1
370 92 96 369 syl2anr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k = 2 nd k 1 M + 1 M + 1 M + 1 2 nd k M + 1
371 370 adantr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k = 2 nd k 1 M + 1 M + 1 M + 1 2 nd k M + 1
372 125 reseq2d φ 2 nd k 1 M + 1 M + 1 = 2 nd k 1 M
373 372 adantr φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k 1 M + 1 M + 1 = 2 nd k 1 M
374 opeq2 2 nd k M + 1 = M + 1 M + 1 2 nd k M + 1 = M + 1 M + 1
375 374 sneqd 2 nd k M + 1 = M + 1 M + 1 2 nd k M + 1 = M + 1 M + 1
376 uneq12 2 nd k 1 M + 1 M + 1 = 2 nd k 1 M M + 1 2 nd k M + 1 = M + 1 M + 1 2 nd k 1 M + 1 M + 1 M + 1 2 nd k M + 1 = 2 nd k 1 M M + 1 M + 1
377 373 375 376 syl2an φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k 1 M + 1 M + 1 M + 1 2 nd k M + 1 = 2 nd k 1 M M + 1 M + 1
378 371 377 eqtrd φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 2 nd k M + 1 = M + 1 2 nd k = 2 nd k 1 M M + 1 M + 1
379 378 adantrl φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M + 1 = 0 2 nd k M + 1 = M + 1 2 nd k = 2 nd k 1 M M + 1 M + 1
380 368 379 opeq12d φ k 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 1 st k M