Metamath Proof Explorer


Theorem poimirlem16

Description: Lemma for poimir establishing the vertices of the simplex of poimirlem17 . (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 φ N
poimirlem22.s S = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
poimirlem22.1 φ F : 0 N 1 0 K 1 N
poimirlem22.2 φ T S
poimirlem18.3 φ n 1 N p ran F p n K
poimirlem18.4 φ 2 nd T = 0
Assertion poimirlem16 φ F = y 0 N 1 n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 + f 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0

Proof

Step Hyp Ref Expression
1 poimir.0 φ N
2 poimirlem22.s S = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
3 poimirlem22.1 φ F : 0 N 1 0 K 1 N
4 poimirlem22.2 φ T S
5 poimirlem18.3 φ n 1 N p ran F p n K
6 poimirlem18.4 φ 2 nd T = 0
7 fveq2 t = T 2 nd t = 2 nd T
8 7 breq2d t = T y < 2 nd t y < 2 nd T
9 8 ifbid t = T if y < 2 nd t y y + 1 = if y < 2 nd T y y + 1
10 2fveq3 t = T 1 st 1 st t = 1 st 1 st T
11 2fveq3 t = T 2 nd 1 st t = 2 nd 1 st T
12 11 imaeq1d t = T 2 nd 1 st t 1 j = 2 nd 1 st T 1 j
13 12 xpeq1d t = T 2 nd 1 st t 1 j × 1 = 2 nd 1 st T 1 j × 1
14 11 imaeq1d t = T 2 nd 1 st t j + 1 N = 2 nd 1 st T j + 1 N
15 14 xpeq1d t = T 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T j + 1 N × 0
16 13 15 uneq12d t = T 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
17 10 16 oveq12d t = T 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
18 9 17 csbeq12dv t = T if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
19 18 mpteq2dv t = T y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
20 19 eqeq2d t = T F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 F = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
21 20 2 elrab2 T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N F = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
22 21 simprbi T S F = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
23 4 22 syl φ F = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
24 elrabi T t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
25 24 2 eleq2s T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
26 4 25 syl φ T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
27 xp1st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
28 26 27 syl φ 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
29 xp1st 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st 1 st T 0 ..^ K 1 N
30 28 29 syl φ 1 st 1 st T 0 ..^ K 1 N
31 elmapfn 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T Fn 1 N
32 30 31 syl φ 1 st 1 st T Fn 1 N
33 32 adantr φ y 0 N 1 1 st 1 st T Fn 1 N
34 1ex 1 V
35 fnconstg 1 V 2 nd 1 st T 1 y + 1 × 1 Fn 2 nd 1 st T 1 y + 1
36 34 35 ax-mp 2 nd 1 st T 1 y + 1 × 1 Fn 2 nd 1 st T 1 y + 1
37 c0ex 0 V
38 fnconstg 0 V 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T y + 1 + 1 N
39 37 38 ax-mp 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T y + 1 + 1 N
40 36 39 pm3.2i 2 nd 1 st T 1 y + 1 × 1 Fn 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T y + 1 + 1 N
41 xp2nd 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
42 28 41 syl φ 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
43 fvex 2 nd 1 st T V
44 f1oeq1 f = 2 nd 1 st T f : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1-1 onto 1 N
45 43 44 elab 2 nd 1 st T f | f : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1-1 onto 1 N
46 42 45 sylib φ 2 nd 1 st T : 1 N 1-1 onto 1 N
47 dff1o3 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N onto 1 N Fun 2 nd 1 st T -1
48 47 simprbi 2 nd 1 st T : 1 N 1-1 onto 1 N Fun 2 nd 1 st T -1
49 46 48 syl φ Fun 2 nd 1 st T -1
50 imain Fun 2 nd 1 st T -1 2 nd 1 st T 1 y + 1 y + 1 + 1 N = 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N
51 49 50 syl φ 2 nd 1 st T 1 y + 1 y + 1 + 1 N = 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N
52 elfznn0 y 0 N 1 y 0
53 nn0p1nn y 0 y + 1
54 52 53 syl y 0 N 1 y + 1
55 54 nnred y 0 N 1 y + 1
56 55 ltp1d y 0 N 1 y + 1 < y + 1 + 1
57 fzdisj y + 1 < y + 1 + 1 1 y + 1 y + 1 + 1 N =
58 56 57 syl y 0 N 1 1 y + 1 y + 1 + 1 N =
59 58 imaeq2d y 0 N 1 2 nd 1 st T 1 y + 1 y + 1 + 1 N = 2 nd 1 st T
60 ima0 2 nd 1 st T =
61 59 60 eqtrdi y 0 N 1 2 nd 1 st T 1 y + 1 y + 1 + 1 N =
62 51 61 sylan9req φ y 0 N 1 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N =
63 fnun 2 nd 1 st T 1 y + 1 × 1 Fn 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T y + 1 + 1 N 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N = 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N
64 40 62 63 sylancr φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N
65 imaundi 2 nd 1 st T 1 y + 1 y + 1 + 1 N = 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N
66 nnuz = 1
67 54 66 eleqtrdi y 0 N 1 y + 1 1
68 peano2uz y + 1 1 y + 1 + 1 1
69 67 68 syl y 0 N 1 y + 1 + 1 1
70 1 nncnd φ N
71 npcan1 N N - 1 + 1 = N
72 70 71 syl φ N - 1 + 1 = N
73 72 adantr φ y 0 N 1 N - 1 + 1 = N
74 elfzuz3 y 0 N 1 N 1 y
75 eluzp1p1 N 1 y N - 1 + 1 y + 1
76 74 75 syl y 0 N 1 N - 1 + 1 y + 1
77 76 adantl φ y 0 N 1 N - 1 + 1 y + 1
78 73 77 eqeltrrd φ y 0 N 1 N y + 1
79 fzsplit2 y + 1 + 1 1 N y + 1 1 N = 1 y + 1 y + 1 + 1 N
80 69 78 79 syl2an2 φ y 0 N 1 1 N = 1 y + 1 y + 1 + 1 N
81 80 imaeq2d φ y 0 N 1 2 nd 1 st T 1 N = 2 nd 1 st T 1 y + 1 y + 1 + 1 N
82 f1ofo 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N onto 1 N
83 foima 2 nd 1 st T : 1 N onto 1 N 2 nd 1 st T 1 N = 1 N
84 46 82 83 3syl φ 2 nd 1 st T 1 N = 1 N
85 84 adantr φ y 0 N 1 2 nd 1 st T 1 N = 1 N
86 81 85 eqtr3d φ y 0 N 1 2 nd 1 st T 1 y + 1 y + 1 + 1 N = 1 N
87 65 86 eqtr3id φ y 0 N 1 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N = 1 N
88 87 fneq2d φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 1 N
89 64 88 mpbid φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 1 N
90 ovexd φ y 0 N 1 1 N V
91 inidm 1 N 1 N = 1 N
92 eqidd φ y 0 N 1 n 1 N 1 st 1 st T n = 1 st 1 st T n
93 eqidd φ y 0 N 1 n 1 N 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n
94 33 89 90 90 91 92 93 offval φ y 0 N 1 1 st 1 st T + f 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 = n 1 N 1 st 1 st T n + 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n
95 oveq1 1 = if n = 2 nd 1 st T 1 1 0 1 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n = if n = 2 nd 1 st T 1 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
96 95 eqeq2d 1 = if n = 2 nd 1 st T 1 1 0 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 1 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = if n = 2 nd 1 st T 1 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
97 oveq1 0 = if n = 2 nd 1 st T 1 1 0 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n = if n = 2 nd 1 st T 1 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
98 97 eqeq2d 0 = if n = 2 nd 1 st T 1 1 0 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = if n = 2 nd 1 st T 1 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
99 1p0e1 1 + 0 = 1
100 99 eqcomi 1 = 1 + 0
101 f1ofn 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T Fn 1 N
102 46 101 syl φ 2 nd 1 st T Fn 1 N
103 102 adantr φ y 0 N 1 2 nd 1 st T Fn 1 N
104 fzss2 N y + 1 1 y + 1 1 N
105 78 104 syl φ y 0 N 1 1 y + 1 1 N
106 eluzfz1 y + 1 1 1 1 y + 1
107 67 106 syl y 0 N 1 1 1 y + 1
108 107 adantl φ y 0 N 1 1 1 y + 1
109 fnfvima 2 nd 1 st T Fn 1 N 1 y + 1 1 N 1 1 y + 1 2 nd 1 st T 1 2 nd 1 st T 1 y + 1
110 103 105 108 109 syl3anc φ y 0 N 1 2 nd 1 st T 1 2 nd 1 st T 1 y + 1
111 fvun1 2 nd 1 st T 1 y + 1 × 1 Fn 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T y + 1 + 1 N 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N = 2 nd 1 st T 1 2 nd 1 st T 1 y + 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 = 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T 1
112 36 39 111 mp3an12 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N = 2 nd 1 st T 1 2 nd 1 st T 1 y + 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 = 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T 1
113 62 110 112 syl2anc φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 = 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T 1
114 34 fvconst2 2 nd 1 st T 1 2 nd 1 st T 1 y + 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T 1 = 1
115 110 114 syl φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T 1 = 1
116 113 115 eqtrd φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 = 1
117 simpr φ n 1 N 1 n 1 N 1
118 1 nnzd φ N
119 peano2zm N N 1
120 118 119 syl φ N 1
121 1z 1
122 120 121 jctil φ 1 N 1
123 elfzelz n 1 N 1 n
124 123 121 jctir n 1 N 1 n 1
125 fzaddel 1 N 1 n 1 n 1 N 1 n + 1 1 + 1 N - 1 + 1
126 122 124 125 syl2an φ n 1 N 1 n 1 N 1 n + 1 1 + 1 N - 1 + 1
127 117 126 mpbid φ n 1 N 1 n + 1 1 + 1 N - 1 + 1
128 72 oveq2d φ 1 + 1 N - 1 + 1 = 1 + 1 N
129 128 adantr φ n 1 N 1 1 + 1 N - 1 + 1 = 1 + 1 N
130 127 129 eleqtrd φ n 1 N 1 n + 1 1 + 1 N
131 130 ralrimiva φ n 1 N 1 n + 1 1 + 1 N
132 simpr φ y 1 + 1 N y 1 + 1 N
133 peano2z 1 1 + 1
134 121 133 ax-mp 1 + 1
135 118 134 jctil φ 1 + 1 N
136 elfzelz y 1 + 1 N y
137 136 121 jctir y 1 + 1 N y 1
138 fzsubel 1 + 1 N y 1 y 1 + 1 N y 1 1 + 1 - 1 N 1
139 135 137 138 syl2an φ y 1 + 1 N y 1 + 1 N y 1 1 + 1 - 1 N 1
140 132 139 mpbid φ y 1 + 1 N y 1 1 + 1 - 1 N 1
141 ax-1cn 1
142 141 141 pncan3oi 1 + 1 - 1 = 1
143 142 oveq1i 1 + 1 - 1 N 1 = 1 N 1
144 140 143 eleqtrdi φ y 1 + 1 N y 1 1 N 1
145 136 zcnd y 1 + 1 N y
146 elfznn n 1 N 1 n
147 146 nncnd n 1 N 1 n
148 subadd2 y 1 n y 1 = n n + 1 = y
149 141 148 mp3an2 y n y 1 = n n + 1 = y
150 149 bicomd y n n + 1 = y y 1 = n
151 eqcom n + 1 = y y = n + 1
152 eqcom y 1 = n n = y 1
153 150 151 152 3bitr3g y n y = n + 1 n = y 1
154 145 147 153 syl2an y 1 + 1 N n 1 N 1 y = n + 1 n = y 1
155 154 ralrimiva y 1 + 1 N n 1 N 1 y = n + 1 n = y 1
156 155 adantl φ y 1 + 1 N n 1 N 1 y = n + 1 n = y 1
157 reu6i y 1 1 N 1 n 1 N 1 y = n + 1 n = y 1 ∃! n 1 N 1 y = n + 1
158 144 156 157 syl2anc φ y 1 + 1 N ∃! n 1 N 1 y = n + 1
159 158 ralrimiva φ y 1 + 1 N ∃! n 1 N 1 y = n + 1
160 eqid n 1 N 1 n + 1 = n 1 N 1 n + 1
161 160 f1ompt n 1 N 1 n + 1 : 1 N 1 1-1 onto 1 + 1 N n 1 N 1 n + 1 1 + 1 N y 1 + 1 N ∃! n 1 N 1 y = n + 1
162 131 159 161 sylanbrc φ n 1 N 1 n + 1 : 1 N 1 1-1 onto 1 + 1 N
163 f1osng N 1 V N 1 : N 1-1 onto 1
164 1 34 163 sylancl φ N 1 : N 1-1 onto 1
165 1 nnred φ N
166 165 ltm1d φ N 1 < N
167 120 zred φ N 1
168 167 165 ltnled φ N 1 < N ¬ N N 1
169 166 168 mpbid φ ¬ N N 1
170 elfzle2 N 1 N 1 N N 1
171 169 170 nsyl φ ¬ N 1 N 1
172 disjsn 1 N 1 N = ¬ N 1 N 1
173 171 172 sylibr φ 1 N 1 N =
174 1re 1
175 174 ltp1i 1 < 1 + 1
176 174 174 readdcli 1 + 1
177 174 176 ltnlei 1 < 1 + 1 ¬ 1 + 1 1
178 175 177 mpbi ¬ 1 + 1 1
179 elfzle1 1 1 + 1 N 1 + 1 1
180 178 179 mto ¬ 1 1 + 1 N
181 disjsn 1 + 1 N 1 = ¬ 1 1 + 1 N
182 180 181 mpbir 1 + 1 N 1 =
183 f1oun n 1 N 1 n + 1 : 1 N 1 1-1 onto 1 + 1 N N 1 : N 1-1 onto 1 1 N 1 N = 1 + 1 N 1 = n 1 N 1 n + 1 N 1 : 1 N 1 N 1-1 onto 1 + 1 N 1
184 182 183 mpanr2 n 1 N 1 n + 1 : 1 N 1 1-1 onto 1 + 1 N N 1 : N 1-1 onto 1 1 N 1 N = n 1 N 1 n + 1 N 1 : 1 N 1 N 1-1 onto 1 + 1 N 1
185 162 164 173 184 syl21anc φ n 1 N 1 n + 1 N 1 : 1 N 1 N 1-1 onto 1 + 1 N 1
186 34 a1i φ 1 V
187 1 66 eleqtrdi φ N 1
188 72 187 eqeltrd φ N - 1 + 1 1
189 uzid N 1 N 1 N 1
190 peano2uz N 1 N 1 N - 1 + 1 N 1
191 120 189 190 3syl φ N - 1 + 1 N 1
192 72 191 eqeltrrd φ N N 1
193 fzsplit2 N - 1 + 1 1 N N 1 1 N = 1 N 1 N - 1 + 1 N
194 188 192 193 syl2anc φ 1 N = 1 N 1 N - 1 + 1 N
195 72 oveq1d φ N - 1 + 1 N = N N
196 fzsn N N N = N
197 118 196 syl φ N N = N
198 195 197 eqtrd φ N - 1 + 1 N = N
199 198 uneq2d φ 1 N 1 N - 1 + 1 N = 1 N 1 N
200 194 199 eqtr2d φ 1 N 1 N = 1 N
201 iftrue n = N if n = N 1 n + 1 = 1
202 201 adantl φ n = N if n = N 1 n + 1 = 1
203 1 186 200 202 fmptapd φ n 1 N 1 if n = N 1 n + 1 N 1 = n 1 N if n = N 1 n + 1
204 eleq1 n = N n 1 N 1 N 1 N 1
205 204 notbid n = N ¬ n 1 N 1 ¬ N 1 N 1
206 171 205 syl5ibrcom φ n = N ¬ n 1 N 1
207 206 necon2ad φ n 1 N 1 n N
208 207 imp φ n 1 N 1 n N
209 ifnefalse n N if n = N 1 n + 1 = n + 1
210 208 209 syl φ n 1 N 1 if n = N 1 n + 1 = n + 1
211 210 mpteq2dva φ n 1 N 1 if n = N 1 n + 1 = n 1 N 1 n + 1
212 211 uneq1d φ n 1 N 1 if n = N 1 n + 1 N 1 = n 1 N 1 n + 1 N 1
213 203 212 eqtr3d φ n 1 N if n = N 1 n + 1 = n 1 N 1 n + 1 N 1
214 194 199 eqtrd φ 1 N = 1 N 1 N
215 uzid 1 1 1
216 peano2uz 1 1 1 + 1 1
217 121 215 216 mp2b 1 + 1 1
218 fzsplit2 1 + 1 1 N 1 1 N = 1 1 1 + 1 N
219 217 187 218 sylancr φ 1 N = 1 1 1 + 1 N
220 fzsn 1 1 1 = 1
221 121 220 ax-mp 1 1 = 1
222 221 uneq1i 1 1 1 + 1 N = 1 1 + 1 N
223 222 equncomi 1 1 1 + 1 N = 1 + 1 N 1
224 219 223 eqtrdi φ 1 N = 1 + 1 N 1
225 213 214 224 f1oeq123d φ n 1 N if n = N 1 n + 1 : 1 N 1-1 onto 1 N n 1 N 1 n + 1 N 1 : 1 N 1 N 1-1 onto 1 + 1 N 1
226 185 225 mpbird φ n 1 N if n = N 1 n + 1 : 1 N 1-1 onto 1 N
227 f1oco 2 nd 1 st T : 1 N 1-1 onto 1 N n 1 N if n = N 1 n + 1 : 1 N 1-1 onto 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 : 1 N 1-1 onto 1 N
228 46 226 227 syl2anc φ 2 nd 1 st T n 1 N if n = N 1 n + 1 : 1 N 1-1 onto 1 N
229 dff1o3 2 nd 1 st T n 1 N if n = N 1 n + 1 : 1 N 1-1 onto 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 : 1 N onto 1 N Fun 2 nd 1 st T n 1 N if n = N 1 n + 1 -1
230 229 simprbi 2 nd 1 st T n 1 N if n = N 1 n + 1 : 1 N 1-1 onto 1 N Fun 2 nd 1 st T n 1 N if n = N 1 n + 1 -1
231 228 230 syl φ Fun 2 nd 1 st T n 1 N if n = N 1 n + 1 -1
232 imain Fun 2 nd 1 st T n 1 N if n = N 1 n + 1 -1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y y + 1 N = 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N
233 231 232 syl φ 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y y + 1 N = 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N
234 52 nn0red y 0 N 1 y
235 234 ltp1d y 0 N 1 y < y + 1
236 fzdisj y < y + 1 1 y y + 1 N =
237 235 236 syl y 0 N 1 1 y y + 1 N =
238 237 imaeq2d y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y y + 1 N = 2 nd 1 st T n 1 N if n = N 1 n + 1
239 ima0 2 nd 1 st T n 1 N if n = N 1 n + 1 =
240 238 239 eqtrdi y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y y + 1 N =
241 233 240 sylan9req φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N =
242 imassrn n 1 N if n = N 1 n + 1 y + 1 N ran n 1 N if n = N 1 n + 1
243 f1of n 1 N if n = N 1 n + 1 : 1 N 1-1 onto 1 N n 1 N if n = N 1 n + 1 : 1 N 1 N
244 frn n 1 N if n = N 1 n + 1 : 1 N 1 N ran n 1 N if n = N 1 n + 1 1 N
245 226 243 244 3syl φ ran n 1 N if n = N 1 n + 1 1 N
246 242 245 sstrid φ n 1 N if n = N 1 n + 1 y + 1 N 1 N
247 246 adantr φ y 0 N 1 n 1 N if n = N 1 n + 1 y + 1 N 1 N
248 elfz1end N N 1 N
249 1 248 sylib φ N 1 N
250 eqid n 1 N if n = N 1 n + 1 = n 1 N if n = N 1 n + 1
251 201 250 34 fvmpt N 1 N n 1 N if n = N 1 n + 1 N = 1
252 249 251 syl φ n 1 N if n = N 1 n + 1 N = 1
253 252 adantr φ y 0 N 1 n 1 N if n = N 1 n + 1 N = 1
254 f1ofn n 1 N if n = N 1 n + 1 : 1 N 1-1 onto 1 N n 1 N if n = N 1 n + 1 Fn 1 N
255 226 254 syl φ n 1 N if n = N 1 n + 1 Fn 1 N
256 255 adantr φ y 0 N 1 n 1 N if n = N 1 n + 1 Fn 1 N
257 fzss1 y + 1 1 y + 1 N 1 N
258 67 257 syl y 0 N 1 y + 1 N 1 N
259 258 adantl φ y 0 N 1 y + 1 N 1 N
260 eluzfz2 N y + 1 N y + 1 N
261 78 260 syl φ y 0 N 1 N y + 1 N
262 fnfvima n 1 N if n = N 1 n + 1 Fn 1 N y + 1 N 1 N N y + 1 N n 1 N if n = N 1 n + 1 N n 1 N if n = N 1 n + 1 y + 1 N
263 256 259 261 262 syl3anc φ y 0 N 1 n 1 N if n = N 1 n + 1 N n 1 N if n = N 1 n + 1 y + 1 N
264 253 263 eqeltrrd φ y 0 N 1 1 n 1 N if n = N 1 n + 1 y + 1 N
265 fnfvima 2 nd 1 st T Fn 1 N n 1 N if n = N 1 n + 1 y + 1 N 1 N 1 n 1 N if n = N 1 n + 1 y + 1 N 2 nd 1 st T 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N
266 103 247 264 265 syl3anc φ y 0 N 1 2 nd 1 st T 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N
267 imaco 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N = 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N
268 266 267 eleqtrrdi φ y 0 N 1 2 nd 1 st T 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N
269 fnconstg 1 V 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 Fn 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y
270 34 269 ax-mp 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 Fn 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y
271 fnconstg 0 V 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 Fn 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N
272 37 271 ax-mp 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 Fn 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N
273 fvun2 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 Fn 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 Fn 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N = 2 nd 1 st T 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1 = 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1
274 270 272 273 mp3an12 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N = 2 nd 1 st T 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1 = 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1
275 241 268 274 syl2anc φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1 = 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1
276 37 fvconst2 2 nd 1 st T 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1 = 0
277 268 276 syl φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1 = 0
278 275 277 eqtrd φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1 = 0
279 278 oveq2d φ y 0 N 1 1 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1 = 1 + 0
280 100 116 279 3eqtr4a φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 = 1 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1
281 fveq2 n = 2 nd 1 st T 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1
282 fveq2 n = 2 nd 1 st T 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n = 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1
283 282 oveq2d n = 2 nd 1 st T 1 1 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n = 1 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1
284 281 283 eqeq12d n = 2 nd 1 st T 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 1 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 = 1 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 2 nd 1 st T 1
285 280 284 syl5ibrcom φ y 0 N 1 n = 2 nd 1 st T 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 1 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
286 285 imp φ y 0 N 1 n = 2 nd 1 st T 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 1 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
287 286 adantlr φ y 0 N 1 n 1 N n = 2 nd 1 st T 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 1 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
288 eldifsn n 1 N 2 nd 1 st T 1 n 1 N n 2 nd 1 st T 1
289 df-ne n 2 nd 1 st T 1 ¬ n = 2 nd 1 st T 1
290 289 anbi2i n 1 N n 2 nd 1 st T 1 n 1 N ¬ n = 2 nd 1 st T 1
291 288 290 bitri n 1 N 2 nd 1 st T 1 n 1 N ¬ n = 2 nd 1 st T 1
292 fnconstg 1 V 2 nd 1 st T 1 + 1 y + 1 × 1 Fn 2 nd 1 st T 1 + 1 y + 1
293 34 292 ax-mp 2 nd 1 st T 1 + 1 y + 1 × 1 Fn 2 nd 1 st T 1 + 1 y + 1
294 293 39 pm3.2i 2 nd 1 st T 1 + 1 y + 1 × 1 Fn 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T y + 1 + 1 N
295 imain Fun 2 nd 1 st T -1 2 nd 1 st T 1 + 1 y + 1 y + 1 + 1 N = 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T y + 1 + 1 N
296 49 295 syl φ 2 nd 1 st T 1 + 1 y + 1 y + 1 + 1 N = 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T y + 1 + 1 N
297 fzdisj y + 1 < y + 1 + 1 1 + 1 y + 1 y + 1 + 1 N =
298 56 297 syl y 0 N 1 1 + 1 y + 1 y + 1 + 1 N =
299 298 imaeq2d y 0 N 1 2 nd 1 st T 1 + 1 y + 1 y + 1 + 1 N = 2 nd 1 st T
300 299 60 eqtrdi y 0 N 1 2 nd 1 st T 1 + 1 y + 1 y + 1 + 1 N =
301 296 300 sylan9req φ y 0 N 1 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T y + 1 + 1 N =
302 fnun 2 nd 1 st T 1 + 1 y + 1 × 1 Fn 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T y + 1 + 1 N 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T y + 1 + 1 N = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T y + 1 + 1 N
303 294 301 302 sylancr φ y 0 N 1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T y + 1 + 1 N
304 imaundi 2 nd 1 st T 1 + 1 y + 1 y + 1 + 1 N = 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T y + 1 + 1 N
305 fzpred N 1 1 N = 1 1 + 1 N
306 187 305 syl φ 1 N = 1 1 + 1 N
307 uncom 1 1 + 1 N = 1 + 1 N 1
308 306 307 eqtrdi φ 1 N = 1 + 1 N 1
309 308 difeq1d φ 1 N 1 = 1 + 1 N 1 1
310 difun2 1 + 1 N 1 1 = 1 + 1 N 1
311 disj3 1 + 1 N 1 = 1 + 1 N = 1 + 1 N 1
312 182 311 mpbi 1 + 1 N = 1 + 1 N 1
313 310 312 eqtr4i 1 + 1 N 1 1 = 1 + 1 N
314 309 313 eqtrdi φ 1 N 1 = 1 + 1 N
315 314 adantr φ y 0 N 1 1 N 1 = 1 + 1 N
316 eluzp1p1 y + 1 1 y + 1 + 1 1 + 1
317 67 316 syl y 0 N 1 y + 1 + 1 1 + 1
318 fzsplit2 y + 1 + 1 1 + 1 N y + 1 1 + 1 N = 1 + 1 y + 1 y + 1 + 1 N
319 317 78 318 syl2an2 φ y 0 N 1 1 + 1 N = 1 + 1 y + 1 y + 1 + 1 N
320 315 319 eqtrd φ y 0 N 1 1 N 1 = 1 + 1 y + 1 y + 1 + 1 N
321 320 imaeq2d φ y 0 N 1 2 nd 1 st T 1 N 1 = 2 nd 1 st T 1 + 1 y + 1 y + 1 + 1 N
322 imadif Fun 2 nd 1 st T -1 2 nd 1 st T 1 N 1 = 2 nd 1 st T 1 N 2 nd 1 st T 1
323 49 322 syl φ 2 nd 1 st T 1 N 1 = 2 nd 1 st T 1 N 2 nd 1 st T 1
324 eluzfz1 N 1 1 1 N
325 187 324 syl φ 1 1 N
326 fnsnfv 2 nd 1 st T Fn 1 N 1 1 N 2 nd 1 st T 1 = 2 nd 1 st T 1
327 102 325 326 syl2anc φ 2 nd 1 st T 1 = 2 nd 1 st T 1
328 327 eqcomd φ 2 nd 1 st T 1 = 2 nd 1 st T 1
329 84 328 difeq12d φ 2 nd 1 st T 1 N 2 nd 1 st T 1 = 1 N 2 nd 1 st T 1
330 323 329 eqtrd φ 2 nd 1 st T 1 N 1 = 1 N 2 nd 1 st T 1
331 330 adantr φ y 0 N 1 2 nd 1 st T 1 N 1 = 1 N 2 nd 1 st T 1
332 321 331 eqtr3d φ y 0 N 1 2 nd 1 st T 1 + 1 y + 1 y + 1 + 1 N = 1 N 2 nd 1 st T 1
333 304 332 eqtr3id φ y 0 N 1 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T y + 1 + 1 N = 1 N 2 nd 1 st T 1
334 333 fneq2d φ y 0 N 1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T y + 1 + 1 N 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 1 N 2 nd 1 st T 1
335 303 334 mpbid φ y 0 N 1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 1 N 2 nd 1 st T 1
336 disjdifr 1 N 2 nd 1 st T 1 2 nd 1 st T 1 =
337 fnconstg 1 V 2 nd 1 st T 1 × 1 Fn 2 nd 1 st T 1
338 34 337 ax-mp 2 nd 1 st T 1 × 1 Fn 2 nd 1 st T 1
339 fvun1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 1 N 2 nd 1 st T 1 2 nd 1 st T 1 × 1 Fn 2 nd 1 st T 1 1 N 2 nd 1 st T 1 2 nd 1 st T 1 = n 1 N 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 1 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n
340 338 339 mp3an2 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 1 N 2 nd 1 st T 1 1 N 2 nd 1 st T 1 2 nd 1 st T 1 = n 1 N 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 1 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n
341 fnconstg 0 V 2 nd 1 st T 1 × 0 Fn 2 nd 1 st T 1
342 37 341 ax-mp 2 nd 1 st T 1 × 0 Fn 2 nd 1 st T 1
343 fvun1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 1 N 2 nd 1 st T 1 2 nd 1 st T 1 × 0 Fn 2 nd 1 st T 1 1 N 2 nd 1 st T 1 2 nd 1 st T 1 = n 1 N 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 0 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n
344 342 343 mp3an2 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 1 N 2 nd 1 st T 1 1 N 2 nd 1 st T 1 2 nd 1 st T 1 = n 1 N 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 0 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n
345 340 344 eqtr4d 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 1 N 2 nd 1 st T 1 1 N 2 nd 1 st T 1 2 nd 1 st T 1 = n 1 N 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 1 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 0 n
346 336 345 mpanr1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 Fn 1 N 2 nd 1 st T 1 n 1 N 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 1 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 0 n
347 335 346 sylan φ y 0 N 1 n 1 N 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 1 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 0 n
348 291 347 sylan2br φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 1 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 0 n
349 348 anassrs φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 1 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 0 n
350 fzpred y + 1 1 1 y + 1 = 1 1 + 1 y + 1
351 67 350 syl y 0 N 1 1 y + 1 = 1 1 + 1 y + 1
352 351 imaeq2d y 0 N 1 2 nd 1 st T 1 y + 1 = 2 nd 1 st T 1 1 + 1 y + 1
353 352 adantl φ y 0 N 1 2 nd 1 st T 1 y + 1 = 2 nd 1 st T 1 1 + 1 y + 1
354 327 uneq1d φ 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1 = 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1
355 uncom 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T 1 = 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1
356 imaundi 2 nd 1 st T 1 1 + 1 y + 1 = 2 nd 1 st T 1 2 nd 1 st T 1 + 1 y + 1
357 354 355 356 3eqtr4g φ 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T 1 = 2 nd 1 st T 1 1 + 1 y + 1
358 357 adantr φ y 0 N 1 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T 1 = 2 nd 1 st T 1 1 + 1 y + 1
359 353 358 eqtr4d φ y 0 N 1 2 nd 1 st T 1 y + 1 = 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T 1
360 359 xpeq1d φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 = 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T 1 × 1
361 xpundir 2 nd 1 st T 1 + 1 y + 1 2 nd 1 st T 1 × 1 = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T 1 × 1
362 360 361 eqtrdi φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T 1 × 1
363 362 uneq1d φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T 1 × 1 2 nd 1 st T y + 1 + 1 N × 0
364 un23 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 1
365 363 364 eqtrdi φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 1
366 365 fveq1d φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 1 n
367 366 ad2antrr φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 1 n
368 imaco 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y = 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y
369 df-ima n 1 N if n = N 1 n + 1 1 y = ran n 1 N if n = N 1 n + 1 1 y
370 peano2uz N 1 y N - 1 + 1 y
371 74 370 syl y 0 N 1 N - 1 + 1 y
372 371 adantl φ y 0 N 1 N - 1 + 1 y
373 73 372 eqeltrrd φ y 0 N 1 N y
374 fzss2 N y 1 y 1 N
375 373 374 syl φ y 0 N 1 1 y 1 N
376 375 resmptd φ y 0 N 1 n 1 N if n = N 1 n + 1 1 y = n 1 y if n = N 1 n + 1
377 fzss2 N 1 y 1 y 1 N 1
378 74 377 syl y 0 N 1 1 y 1 N 1
379 378 adantl φ y 0 N 1 1 y 1 N 1
380 171 adantr φ y 0 N 1 ¬ N 1 N 1
381 379 380 ssneldd φ y 0 N 1 ¬ N 1 y
382 eleq1 n = N n 1 y N 1 y
383 382 notbid n = N ¬ n 1 y ¬ N 1 y
384 381 383 syl5ibrcom φ y 0 N 1 n = N ¬ n 1 y
385 384 necon2ad φ y 0 N 1 n 1 y n N
386 385 imp φ y 0 N 1 n 1 y n N
387 386 209 syl φ y 0 N 1 n 1 y if n = N 1 n + 1 = n + 1
388 387 mpteq2dva φ y 0 N 1 n 1 y if n = N 1 n + 1 = n 1 y n + 1
389 376 388 eqtrd φ y 0 N 1 n 1 N if n = N 1 n + 1 1 y = n 1 y n + 1
390 389 rneqd φ y 0 N 1 ran n 1 N if n = N 1 n + 1 1 y = ran n 1 y n + 1
391 369 390 syl5eq φ y 0 N 1 n 1 N if n = N 1 n + 1 1 y = ran n 1 y n + 1
392 eqid n 1 y n + 1 = n 1 y n + 1
393 392 elrnmpt j V j ran n 1 y n + 1 n 1 y j = n + 1
394 393 elv j ran n 1 y n + 1 n 1 y j = n + 1
395 elfzelz y 0 N 1 y
396 395 adantl φ y 0 N 1 y
397 simpr y n 1 y n 1 y
398 121 jctl y 1 y
399 elfzelz n 1 y n
400 399 121 jctir n 1 y n 1
401 fzaddel 1 y n 1 n 1 y n + 1 1 + 1 y + 1
402 398 400 401 syl2an y n 1 y n 1 y n + 1 1 + 1 y + 1
403 397 402 mpbid y n 1 y n + 1 1 + 1 y + 1
404 eleq1 j = n + 1 j 1 + 1 y + 1 n + 1 1 + 1 y + 1
405 403 404 syl5ibrcom y n 1 y j = n + 1 j 1 + 1 y + 1
406 405 rexlimdva y n 1 y j = n + 1 j 1 + 1 y + 1
407 elfzelz j 1 + 1 y + 1 j
408 407 zcnd j 1 + 1 y + 1 j
409 npcan1 j j - 1 + 1 = j
410 408 409 syl j 1 + 1 y + 1 j - 1 + 1 = j
411 410 eleq1d j 1 + 1 y + 1 j - 1 + 1 1 + 1 y + 1 j 1 + 1 y + 1
412 411 ibir j 1 + 1 y + 1 j - 1 + 1 1 + 1 y + 1
413 412 adantl y j 1 + 1 y + 1 j - 1 + 1 1 + 1 y + 1
414 peano2zm j j 1
415 407 414 syl j 1 + 1 y + 1 j 1
416 415 121 jctir j 1 + 1 y + 1 j 1 1
417 fzaddel 1 y j 1 1 j 1 1 y j - 1 + 1 1 + 1 y + 1
418 398 416 417 syl2an y j 1 + 1 y + 1 j 1 1 y j - 1 + 1 1 + 1 y + 1
419 413 418 mpbird y j 1 + 1 y + 1 j 1 1 y
420 408 adantl y j 1 + 1 y + 1 j
421 409 eqcomd j j = j - 1 + 1
422 420 421 syl y j 1 + 1 y + 1 j = j - 1 + 1
423 oveq1 n = j 1 n + 1 = j - 1 + 1
424 423 rspceeqv j 1 1 y j = j - 1 + 1 n 1 y j = n + 1
425 419 422 424 syl2anc y j 1 + 1 y + 1 n 1 y j = n + 1
426 425 ex y j 1 + 1 y + 1 n 1 y j = n + 1
427 406 426 impbid y n 1 y j = n + 1 j 1 + 1 y + 1
428 396 427 syl φ y 0 N 1 n 1 y j = n + 1 j 1 + 1 y + 1
429 394 428 syl5bb φ y 0 N 1 j ran n 1 y n + 1 j 1 + 1 y + 1
430 429 eqrdv φ y 0 N 1 ran n 1 y n + 1 = 1 + 1 y + 1
431 391 430 eqtrd φ y 0 N 1 n 1 N if n = N 1 n + 1 1 y = 1 + 1 y + 1
432 431 imaeq2d φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y = 2 nd 1 st T 1 + 1 y + 1
433 368 432 syl5eq φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y = 2 nd 1 st T 1 + 1 y + 1
434 433 xpeq1d φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 = 2 nd 1 st T 1 + 1 y + 1 × 1
435 imaundi 2 nd 1 st T n 1 N if n = N 1 n + 1 N y + 1 N 1 = 2 nd 1 st T n 1 N if n = N 1 n + 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 1
436 imaco 2 nd 1 st T n 1 N if n = N 1 n + 1 N = 2 nd 1 st T n 1 N if n = N 1 n + 1 N
437 imaco 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 1 = 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 1
438 436 437 uneq12i 2 nd 1 st T n 1 N if n = N 1 n + 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 1 = 2 nd 1 st T n 1 N if n = N 1 n + 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 1
439 435 438 eqtri 2 nd 1 st T n 1 N if n = N 1 n + 1 N y + 1 N 1 = 2 nd 1 st T n 1 N if n = N 1 n + 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 1
440 192 adantr φ y 0 N 1 N N 1
441 fzsplit2 N - 1 + 1 y + 1 N N 1 y + 1 N = y + 1 N 1 N - 1 + 1 N
442 76 440 441 syl2an2 φ y 0 N 1 y + 1 N = y + 1 N 1 N - 1 + 1 N
443 198 uneq2d φ y + 1 N 1 N - 1 + 1 N = y + 1 N 1 N
444 443 adantr φ y 0 N 1 y + 1 N 1 N - 1 + 1 N = y + 1 N 1 N
445 442 444 eqtrd φ y 0 N 1 y + 1 N = y + 1 N 1 N
446 uncom y + 1 N 1 N = N y + 1 N 1
447 445 446 eqtrdi φ y 0 N 1 y + 1 N = N y + 1 N 1
448 447 imaeq2d φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N = 2 nd 1 st T n 1 N if n = N 1 n + 1 N y + 1 N 1
449 252 sneqd φ n 1 N if n = N 1 n + 1 N = 1
450 fnsnfv n 1 N if n = N 1 n + 1 Fn 1 N N 1 N n 1 N if n = N 1 n + 1 N = n 1 N if n = N 1 n + 1 N
451 255 249 450 syl2anc φ n 1 N if n = N 1 n + 1 N = n 1 N if n = N 1 n + 1 N
452 449 451 eqtr3d φ 1 = n 1 N if n = N 1 n + 1 N
453 452 imaeq2d φ 2 nd 1 st T 1 = 2 nd 1 st T n 1 N if n = N 1 n + 1 N
454 327 453 eqtrd φ 2 nd 1 st T 1 = 2 nd 1 st T n 1 N if n = N 1 n + 1 N
455 454 adantr φ y 0 N 1 2 nd 1 st T 1 = 2 nd 1 st T n 1 N if n = N 1 n + 1 N
456 df-ima n 1 N if n = N 1 n + 1 y + 1 N 1 = ran n 1 N if n = N 1 n + 1 y + 1 N 1
457 fzss1 y + 1 1 y + 1 N 1 1 N 1
458 67 457 syl y 0 N 1 y + 1 N 1 1 N 1
459 fzss2 N N 1 1 N 1 1 N
460 192 459 syl φ 1 N 1 1 N
461 458 460 sylan9ssr φ y 0 N 1 y + 1 N 1 1 N
462 461 resmptd φ y 0 N 1 n 1 N if n = N 1 n + 1 y + 1 N 1 = n y + 1 N 1 if n = N 1 n + 1
463 elfzle2 N y + 1 N 1 N N 1
464 169 463 nsyl φ ¬ N y + 1 N 1
465 eleq1 n = N n y + 1 N 1 N y + 1 N 1
466 465 notbid n = N ¬ n y + 1 N 1 ¬ N y + 1 N 1
467 464 466 syl5ibrcom φ n = N ¬ n y + 1 N 1
468 467 con2d φ n y + 1 N 1 ¬ n = N
469 468 imp φ n y + 1 N 1 ¬ n = N
470 469 iffalsed φ n y + 1 N 1 if n = N 1 n + 1 = n + 1
471 470 mpteq2dva φ n y + 1 N 1 if n = N 1 n + 1 = n y + 1 N 1 n + 1
472 471 adantr φ y 0 N 1 n y + 1 N 1 if n = N 1 n + 1 = n y + 1 N 1 n + 1
473 462 472 eqtrd φ y 0 N 1 n 1 N if n = N 1 n + 1 y + 1 N 1 = n y + 1 N 1 n + 1
474 473 rneqd φ y 0 N 1 ran n 1 N if n = N 1 n + 1 y + 1 N 1 = ran n y + 1 N 1 n + 1
475 456 474 syl5eq φ y 0 N 1 n 1 N if n = N 1 n + 1 y + 1 N 1 = ran n y + 1 N 1 n + 1
476 elfzelz j y + 1 + 1 N - 1 + 1 j
477 476 zcnd j y + 1 + 1 N - 1 + 1 j
478 477 409 syl j y + 1 + 1 N - 1 + 1 j - 1 + 1 = j
479 478 eleq1d j y + 1 + 1 N - 1 + 1 j - 1 + 1 y + 1 + 1 N - 1 + 1 j y + 1 + 1 N - 1 + 1
480 479 ibir j y + 1 + 1 N - 1 + 1 j - 1 + 1 y + 1 + 1 N - 1 + 1
481 480 adantl φ y 0 N 1 j y + 1 + 1 N - 1 + 1 j - 1 + 1 y + 1 + 1 N - 1 + 1
482 54 nnzd y 0 N 1 y + 1
483 120 482 anim12ci φ y 0 N 1 y + 1 N 1
484 476 414 syl j y + 1 + 1 N - 1 + 1 j 1
485 484 121 jctir j y + 1 + 1 N - 1 + 1 j 1 1
486 fzaddel y + 1 N 1 j 1 1 j 1 y + 1 N 1 j - 1 + 1 y + 1 + 1 N - 1 + 1
487 483 485 486 syl2an φ y 0 N 1 j y + 1 + 1 N - 1 + 1 j 1 y + 1 N 1 j - 1 + 1 y + 1 + 1 N - 1 + 1
488 481 487 mpbird φ y 0 N 1 j y + 1 + 1 N - 1 + 1 j 1 y + 1 N 1
489 477 421 syl j y + 1 + 1 N - 1 + 1 j = j - 1 + 1
490 489 adantl φ y 0 N 1 j y + 1 + 1 N - 1 + 1 j = j - 1 + 1
491 423 rspceeqv j 1 y + 1 N 1 j = j - 1 + 1 n y + 1 N 1 j = n + 1
492 488 490 491 syl2anc φ y 0 N 1 j y + 1 + 1 N - 1 + 1 n y + 1 N 1 j = n + 1
493 492 ex φ y 0 N 1 j y + 1 + 1 N - 1 + 1 n y + 1 N 1 j = n + 1
494 simpr φ y 0 N 1 n y + 1 N 1 n y + 1 N 1
495 elfzelz n y + 1 N 1 n
496 495 121 jctir n y + 1 N 1 n 1
497 fzaddel y + 1 N 1 n 1 n y + 1 N 1 n + 1 y + 1 + 1 N - 1 + 1
498 483 496 497 syl2an φ y 0 N 1 n y + 1 N 1 n y + 1 N 1 n + 1 y + 1 + 1 N - 1 + 1
499 494 498 mpbid φ y 0 N 1 n y + 1 N 1 n + 1 y + 1 + 1 N - 1 + 1
500 eleq1 j = n + 1 j y + 1 + 1 N - 1 + 1 n + 1 y + 1 + 1 N - 1 + 1
501 499 500 syl5ibrcom φ y 0 N 1 n y + 1 N 1 j = n + 1 j y + 1 + 1 N - 1 + 1
502 501 rexlimdva φ y 0 N 1 n y + 1 N 1 j = n + 1 j y + 1 + 1 N - 1 + 1
503 493 502 impbid φ y 0 N 1 j y + 1 + 1 N - 1 + 1 n y + 1 N 1 j = n + 1
504 eqid n y + 1 N 1 n + 1 = n y + 1 N 1 n + 1
505 504 elrnmpt j V j ran n y + 1 N 1 n + 1 n y + 1 N 1 j = n + 1
506 505 elv j ran n y + 1 N 1 n + 1 n y + 1 N 1 j = n + 1
507 503 506 bitr4di φ y 0 N 1 j y + 1 + 1 N - 1 + 1 j ran n y + 1 N 1 n + 1
508 507 eqrdv φ y 0 N 1 y + 1 + 1 N - 1 + 1 = ran n y + 1 N 1 n + 1
509 72 oveq2d φ y + 1 + 1 N - 1 + 1 = y + 1 + 1 N
510 509 adantr φ y 0 N 1 y + 1 + 1 N - 1 + 1 = y + 1 + 1 N
511 475 508 510 3eqtr2rd φ y 0 N 1 y + 1 + 1 N = n 1 N if n = N 1 n + 1 y + 1 N 1
512 511 imaeq2d φ y 0 N 1 2 nd 1 st T y + 1 + 1 N = 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 1
513 455 512 uneq12d φ y 0 N 1 2 nd 1 st T 1 2 nd 1 st T y + 1 + 1 N = 2 nd 1 st T n 1 N if n = N 1 n + 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 1
514 439 448 513 3eqtr4a φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N = 2 nd 1 st T 1 2 nd 1 st T y + 1 + 1 N
515 514 xpeq1d φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 = 2 nd 1 st T 1 2 nd 1 st T y + 1 + 1 N × 0
516 xpundir 2 nd 1 st T 1 2 nd 1 st T y + 1 + 1 N × 0 = 2 nd 1 st T 1 × 0 2 nd 1 st T y + 1 + 1 N × 0
517 515 516 eqtrdi φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 = 2 nd 1 st T 1 × 0 2 nd 1 st T y + 1 + 1 N × 0
518 434 517 uneq12d φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T 1 × 0 2 nd 1 st T y + 1 + 1 N × 0
519 unass 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T 1 × 0 2 nd 1 st T y + 1 + 1 N × 0 = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T 1 × 0 2 nd 1 st T y + 1 + 1 N × 0
520 un23 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T 1 × 0 2 nd 1 st T y + 1 + 1 N × 0 = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 0
521 519 520 eqtr3i 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T 1 × 0 2 nd 1 st T y + 1 + 1 N × 0 = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 0
522 518 521 eqtrdi φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 0
523 522 fveq1d φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 0 n
524 523 ad2antrr φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n = 2 nd 1 st T 1 + 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 2 nd 1 st T 1 × 0 n
525 349 367 524 3eqtr4d φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
526 snssi 1 1
527 141 526 ax-mp 1
528 0cn 0
529 snssi 0 0
530 528 529 ax-mp 0
531 527 530 unssi 1 0
532 34 fconst 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 : 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 1
533 37 fconst 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 : 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 0
534 532 533 pm3.2i 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 : 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 : 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 0
535 fun 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 : 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 : 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 0 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N = 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 : 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 1 0
536 534 241 535 sylancr φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 : 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 1 0
537 imaundi 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y y + 1 N = 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N
538 fzsplit2 y + 1 1 N y 1 N = 1 y y + 1 N
539 67 373 538 syl2an2 φ y 0 N 1 1 N = 1 y y + 1 N
540 539 imaeq2d φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 N = 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y y + 1 N
541 f1ofo 2 nd 1 st T n 1 N if n = N 1 n + 1 : 1 N 1-1 onto 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 : 1 N onto 1 N
542 foima 2 nd 1 st T n 1 N if n = N 1 n + 1 : 1 N onto 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 1 N = 1 N
543 228 541 542 3syl φ 2 nd 1 st T n 1 N if n = N 1 n + 1 1 N = 1 N
544 543 adantr φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 N = 1 N
545 540 544 eqtr3d φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y y + 1 N = 1 N
546 537 545 eqtr3id φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N = 1 N
547 546 feq2d φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 : 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N 1 0 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 : 1 N 1 0
548 536 547 mpbid φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 : 1 N 1 0
549 548 ffvelrnda φ y 0 N 1 n 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n 1 0
550 531 549 sseldi φ y 0 N 1 n 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
551 550 addid2d φ y 0 N 1 n 1 N 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n = 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
552 551 adantr φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n = 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
553 525 552 eqtr4d φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
554 96 98 287 553 ifbothda φ y 0 N 1 n 1 N 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = if n = 2 nd 1 st T 1 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
555 554 oveq2d φ y 0 N 1 n 1 N 1 st 1 st T n + 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
556 elmapi 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T : 1 N 0 ..^ K
557 30 556 syl φ 1 st 1 st T : 1 N 0 ..^ K
558 557 ffvelrnda φ n 1 N 1 st 1 st T n 0 ..^ K
559 elfzonn0 1 st 1 st T n 0 ..^ K 1 st 1 st T n 0
560 558 559 syl φ n 1 N 1 st 1 st T n 0
561 560 nn0cnd φ n 1 N 1 st 1 st T n
562 561 adantlr φ y 0 N 1 n 1 N 1 st 1 st T n
563 141 528 ifcli if n = 2 nd 1 st T 1 1 0
564 563 a1i φ y 0 N 1 n 1 N if n = 2 nd 1 st T 1 1 0
565 562 564 550 addassd φ y 0 N 1 n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n = 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
566 555 565 eqtr4d φ y 0 N 1 n 1 N 1 st 1 st T n + 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
567 566 mpteq2dva φ y 0 N 1 n 1 N 1 st 1 st T n + 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 n = n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
568 94 567 eqtrd φ y 0 N 1 1 st 1 st T + f 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0 = n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
569 6 adantr φ y 0 N 1 2 nd T = 0
570 elfzle1 y 0 N 1 0 y
571 570 adantl φ y 0 N 1 0 y
572 569 571 eqbrtrd φ y 0 N 1 2 nd T y
573 0re 0
574 6 573 eqeltrdi φ 2 nd T
575 lenlt 2 nd T y 2 nd T y ¬ y < 2 nd T
576 574 234 575 syl2an φ y 0 N 1 2 nd T y ¬ y < 2 nd T
577 572 576 mpbid φ y 0 N 1 ¬ y < 2 nd T
578 577 iffalsed φ y 0 N 1 if y < 2 nd T y y + 1 = y + 1
579 578 csbeq1d φ y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
580 ovex y + 1 V
581 oveq2 j = y + 1 1 j = 1 y + 1
582 581 imaeq2d j = y + 1 2 nd 1 st T 1 j = 2 nd 1 st T 1 y + 1
583 582 xpeq1d j = y + 1 2 nd 1 st T 1 j × 1 = 2 nd 1 st T 1 y + 1 × 1
584 oveq1 j = y + 1 j + 1 = y + 1 + 1
585 584 oveq1d j = y + 1 j + 1 N = y + 1 + 1 N
586 585 imaeq2d j = y + 1 2 nd 1 st T j + 1 N = 2 nd 1 st T y + 1 + 1 N
587 586 xpeq1d j = y + 1 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T y + 1 + 1 N × 0
588 583 587 uneq12d j = y + 1 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0
589 588 oveq2d j = y + 1 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 1 st 1 st T + f 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0
590 580 589 csbie y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 1 st 1 st T + f 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0
591 579 590 eqtrdi φ y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 1 st 1 st T + f 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T y + 1 + 1 N × 0
592 ovexd φ y 0 N 1 n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 V
593 fvexd φ y 0 N 1 n 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n V
594 eqidd φ y 0 N 1 n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 = n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0
595 548 ffnd φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 Fn 1 N
596 nfcv _ n 2 nd 1 st T
597 nfmpt1 _ n n 1 N if n = N 1 n + 1
598 596 597 nfco _ n 2 nd 1 st T n 1 N if n = N 1 n + 1
599 nfcv _ n 1 y
600 598 599 nfima _ n 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y
601 nfcv _ n 1
602 600 601 nfxp _ n 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1
603 nfcv _ n y + 1 N
604 598 603 nfima _ n 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N
605 nfcv _ n 0
606 604 605 nfxp _ n 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0
607 602 606 nfun _ n 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0
608 607 dffn5f 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 Fn 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 = n 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
609 595 608 sylib φ y 0 N 1 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 = n 1 N 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
610 90 592 593 594 609 offval2 φ y 0 N 1 n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 + f 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 = n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 + 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 n
611 568 591 610 3eqtr4rd φ y 0 N 1 n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 + f 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 = if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
612 611 mpteq2dva φ y 0 N 1 n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 + f 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0 = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
613 23 612 eqtr4d φ F = y 0 N 1 n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 + f 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0