Metamath Proof Explorer


Theorem poimirlem17

Description: Lemma for poimir establishing existence for poimirlem18 . (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 poimirlem17 φ z S z T

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 1 2 3 4 5 6 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
8 elfznn0 y 0 N 1 y 0
9 8 nn0red y 0 N 1 y
10 9 adantl φ y 0 N 1 y
11 1 nnzd φ N
12 peano2zm N N 1
13 11 12 syl φ N 1
14 13 zred φ N 1
15 14 adantr φ y 0 N 1 N 1
16 1 nnred φ N
17 16 adantr φ y 0 N 1 N
18 elfzle2 y 0 N 1 y N 1
19 18 adantl φ y 0 N 1 y N 1
20 16 ltm1d φ N 1 < N
21 20 adantr φ y 0 N 1 N 1 < N
22 10 15 17 19 21 lelttrd φ y 0 N 1 y < N
23 22 adantlr φ t = 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 N y 0 N 1 y < N
24 fveq2 t = 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 N 2 nd t = 2 nd 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 N
25 opex 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 V
26 op2ndg 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 V N 2 nd 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 N = N
27 25 1 26 sylancr φ 2 nd 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 N = N
28 24 27 sylan9eqr φ t = 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 N 2 nd t = N
29 28 adantr φ t = 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 N y 0 N 1 2 nd t = N
30 23 29 breqtrrd φ t = 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 N y 0 N 1 y < 2 nd t
31 30 iftrued φ t = 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 N y 0 N 1 if y < 2 nd t y y + 1 = y
32 31 csbeq1d φ t = 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 N 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 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
33 vex y V
34 oveq2 j = y 1 j = 1 y
35 34 imaeq2d j = y 2 nd 1 st t 1 j = 2 nd 1 st t 1 y
36 35 xpeq1d j = y 2 nd 1 st t 1 j × 1 = 2 nd 1 st t 1 y × 1
37 oveq1 j = y j + 1 = y + 1
38 37 oveq1d j = y j + 1 N = y + 1 N
39 38 imaeq2d j = y 2 nd 1 st t j + 1 N = 2 nd 1 st t y + 1 N
40 39 xpeq1d j = y 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st t y + 1 N × 0
41 36 40 uneq12d j = y 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 2 nd 1 st t y + 1 N × 0
42 41 oveq2d j = y 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 2 nd 1 st t y + 1 N × 0
43 33 42 csbie y / 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 2 nd 1 st t y + 1 N × 0
44 2fveq3 t = 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 N 1 st 1 st t = 1 st 1 st 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 N
45 op1stg 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 V N 1 st 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 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
46 25 1 45 sylancr φ 1 st 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 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
47 46 fveq2d φ 1 st 1 st 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 N = 1 st 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
48 ovex 1 N V
49 48 mptex n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 V
50 fvex 2 nd 1 st T V
51 48 mptex n 1 N if n = N 1 n + 1 V
52 50 51 coex 2 nd 1 st T n 1 N if n = N 1 n + 1 V
53 49 52 op1st 1 st 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 = n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0
54 47 53 eqtrdi φ 1 st 1 st 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 N = n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0
55 44 54 sylan9eqr φ t = 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 N 1 st 1 st t = n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0
56 fveq2 t = 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 N 1 st t = 1 st 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 N
57 56 46 sylan9eqr φ t = 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 N 1 st t = 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
58 57 fveq2d φ t = 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 N 2 nd 1 st t = 2 nd 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
59 49 52 op2nd 2 nd 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 = 2 nd 1 st T n 1 N if n = N 1 n + 1
60 58 59 eqtrdi φ t = 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 N 2 nd 1 st t = 2 nd 1 st T n 1 N if n = N 1 n + 1
61 60 imaeq1d φ t = 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 N 2 nd 1 st t 1 y = 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y
62 61 xpeq1d φ t = 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 N 2 nd 1 st t 1 y × 1 = 2 nd 1 st T n 1 N if n = N 1 n + 1 1 y × 1
63 60 imaeq1d φ t = 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 N 2 nd 1 st t y + 1 N = 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N
64 63 xpeq1d φ t = 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 N 2 nd 1 st t y + 1 N × 0 = 2 nd 1 st T n 1 N if n = N 1 n + 1 y + 1 N × 0
65 62 64 uneq12d φ t = 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 N 2 nd 1 st t 1 y × 1 2 nd 1 st t y + 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
66 55 65 oveq12d φ t = 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 N 1 st 1 st t + f 2 nd 1 st t 1 y × 1 2 nd 1 st t y + 1 N × 0 = 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
67 43 66 syl5eq φ t = 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 N y / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 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
68 67 adantr φ t = 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 N y 0 N 1 y / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 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
69 32 68 eqtrd φ t = 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 N 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 = 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
70 69 mpteq2dva φ t = 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 N 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 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
71 70 eqeq2d φ t = 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 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 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
72 71 ex φ t = 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 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 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
73 72 alrimiv φ t t = 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 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 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
74 oveq2 1 = if n = 2 nd 1 st T 1 1 0 1 st 1 st T n + 1 = 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0
75 74 eleq1d 1 = if n = 2 nd 1 st T 1 1 0 1 st 1 st T n + 1 0 ..^ K 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 0 ..^ K
76 oveq2 0 = if n = 2 nd 1 st T 1 1 0 1 st 1 st T n + 0 = 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0
77 76 eleq1d 0 = if n = 2 nd 1 st T 1 1 0 1 st 1 st T n + 0 0 ..^ K 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 0 ..^ K
78 fveq2 n = 2 nd 1 st T 1 1 st 1 st T n = 1 st 1 st T 2 nd 1 st T 1
79 78 oveq1d n = 2 nd 1 st T 1 1 st 1 st T n + 1 = 1 st 1 st T 2 nd 1 st T 1 + 1
80 79 adantl φ n = 2 nd 1 st T 1 1 st 1 st T n + 1 = 1 st 1 st T 2 nd 1 st T 1 + 1
81 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
82 81 2 eleq2s T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
83 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
84 4 82 83 3syl φ 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
85 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
86 elmapi 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T : 1 N 0 ..^ K
87 84 85 86 3syl φ 1 st 1 st T : 1 N 0 ..^ K
88 4 82 syl φ T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
89 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
90 88 83 89 3syl φ 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
91 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
92 50 91 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
93 90 92 sylib φ 2 nd 1 st T : 1 N 1-1 onto 1 N
94 f1of 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1 N
95 93 94 syl φ 2 nd 1 st T : 1 N 1 N
96 nnuz = 1
97 1 96 eleqtrdi φ N 1
98 eluzfz1 N 1 1 1 N
99 97 98 syl φ 1 1 N
100 95 99 ffvelrnd φ 2 nd 1 st T 1 1 N
101 87 100 ffvelrnd φ 1 st 1 st T 2 nd 1 st T 1 0 ..^ K
102 elfzonn0 1 st 1 st T 2 nd 1 st T 1 0 ..^ K 1 st 1 st T 2 nd 1 st T 1 0
103 peano2nn0 1 st 1 st T 2 nd 1 st T 1 0 1 st 1 st T 2 nd 1 st T 1 + 1 0
104 101 102 103 3syl φ 1 st 1 st T 2 nd 1 st T 1 + 1 0
105 elfzo0 1 st 1 st T 2 nd 1 st T 1 0 ..^ K 1 st 1 st T 2 nd 1 st T 1 0 K 1 st 1 st T 2 nd 1 st T 1 < K
106 101 105 sylib φ 1 st 1 st T 2 nd 1 st T 1 0 K 1 st 1 st T 2 nd 1 st T 1 < K
107 106 simp2d φ K
108 104 nn0red φ 1 st 1 st T 2 nd 1 st T 1 + 1
109 107 nnred φ K
110 elfzolt2 1 st 1 st T 2 nd 1 st T 1 0 ..^ K 1 st 1 st T 2 nd 1 st T 1 < K
111 101 110 syl φ 1 st 1 st T 2 nd 1 st T 1 < K
112 101 102 syl φ 1 st 1 st T 2 nd 1 st T 1 0
113 112 nn0zd φ 1 st 1 st T 2 nd 1 st T 1
114 107 nnzd φ K
115 zltp1le 1 st 1 st T 2 nd 1 st T 1 K 1 st 1 st T 2 nd 1 st T 1 < K 1 st 1 st T 2 nd 1 st T 1 + 1 K
116 113 114 115 syl2anc φ 1 st 1 st T 2 nd 1 st T 1 < K 1 st 1 st T 2 nd 1 st T 1 + 1 K
117 111 116 mpbid φ 1 st 1 st T 2 nd 1 st T 1 + 1 K
118 fvex 2 nd 1 st T 1 V
119 eleq1 n = 2 nd 1 st T 1 n 1 N 2 nd 1 st T 1 1 N
120 119 anbi2d n = 2 nd 1 st T 1 φ n 1 N φ 2 nd 1 st T 1 1 N
121 fveq2 n = 2 nd 1 st T 1 p n = p 2 nd 1 st T 1
122 121 neeq1d n = 2 nd 1 st T 1 p n K p 2 nd 1 st T 1 K
123 122 rexbidv n = 2 nd 1 st T 1 p ran F p n K p ran F p 2 nd 1 st T 1 K
124 120 123 imbi12d n = 2 nd 1 st T 1 φ n 1 N p ran F p n K φ 2 nd 1 st T 1 1 N p ran F p 2 nd 1 st T 1 K
125 118 124 5 vtocl φ 2 nd 1 st T 1 1 N p ran F p 2 nd 1 st T 1 K
126 100 125 mpdan φ p ran F p 2 nd 1 st T 1 K
127 fveq1 p = 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 p 2 nd 1 st T 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 2 nd 1 st T 1
128 87 ffnd φ 1 st 1 st T Fn 1 N
129 128 adantr φ y 0 N 1 1 st 1 st T Fn 1 N
130 1ex 1 V
131 fnconstg 1 V 2 nd 1 st T 1 y + 1 × 1 Fn 2 nd 1 st T 1 y + 1
132 130 131 ax-mp 2 nd 1 st T 1 y + 1 × 1 Fn 2 nd 1 st T 1 y + 1
133 c0ex 0 V
134 fnconstg 0 V 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T y + 1 + 1 N
135 133 134 ax-mp 2 nd 1 st T y + 1 + 1 N × 0 Fn 2 nd 1 st T y + 1 + 1 N
136 132 135 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
137 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
138 137 simprbi 2 nd 1 st T : 1 N 1-1 onto 1 N Fun 2 nd 1 st T -1
139 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
140 93 138 139 3syl φ 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
141 nn0p1nn y 0 y + 1
142 8 141 syl y 0 N 1 y + 1
143 142 nnred y 0 N 1 y + 1
144 143 ltp1d y 0 N 1 y + 1 < y + 1 + 1
145 fzdisj y + 1 < y + 1 + 1 1 y + 1 y + 1 + 1 N =
146 145 imaeq2d y + 1 < y + 1 + 1 2 nd 1 st T 1 y + 1 y + 1 + 1 N = 2 nd 1 st T
147 ima0 2 nd 1 st T =
148 146 147 eqtrdi y + 1 < y + 1 + 1 2 nd 1 st T 1 y + 1 y + 1 + 1 N =
149 144 148 syl y 0 N 1 2 nd 1 st T 1 y + 1 y + 1 + 1 N =
150 140 149 sylan9req φ y 0 N 1 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N =
151 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
152 136 150 151 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
153 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
154 142 peano2nnd y 0 N 1 y + 1 + 1
155 154 96 eleqtrdi y 0 N 1 y + 1 + 1 1
156 1 nncnd φ N
157 npcan1 N N - 1 + 1 = N
158 156 157 syl φ N - 1 + 1 = N
159 158 adantr φ y 0 N 1 N - 1 + 1 = N
160 elfzuz3 y 0 N 1 N 1 y
161 eluzp1p1 N 1 y N - 1 + 1 y + 1
162 160 161 syl y 0 N 1 N - 1 + 1 y + 1
163 162 adantl φ y 0 N 1 N - 1 + 1 y + 1
164 159 163 eqeltrrd φ y 0 N 1 N y + 1
165 fzsplit2 y + 1 + 1 1 N y + 1 1 N = 1 y + 1 y + 1 + 1 N
166 155 164 165 syl2an2 φ y 0 N 1 1 N = 1 y + 1 y + 1 + 1 N
167 166 imaeq2d φ y 0 N 1 2 nd 1 st T 1 N = 2 nd 1 st T 1 y + 1 y + 1 + 1 N
168 f1ofo 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N onto 1 N
169 foima 2 nd 1 st T : 1 N onto 1 N 2 nd 1 st T 1 N = 1 N
170 93 168 169 3syl φ 2 nd 1 st T 1 N = 1 N
171 170 adantr φ y 0 N 1 2 nd 1 st T 1 N = 1 N
172 167 171 eqtr3d φ y 0 N 1 2 nd 1 st T 1 y + 1 y + 1 + 1 N = 1 N
173 153 172 eqtr3id φ y 0 N 1 2 nd 1 st T 1 y + 1 2 nd 1 st T y + 1 + 1 N = 1 N
174 173 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
175 152 174 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
176 48 a1i φ y 0 N 1 1 N V
177 inidm 1 N 1 N = 1 N
178 eqidd φ y 0 N 1 2 nd 1 st T 1 1 N 1 st 1 st T 2 nd 1 st T 1 = 1 st 1 st T 2 nd 1 st T 1
179 f1ofn 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T Fn 1 N
180 93 179 syl φ 2 nd 1 st T Fn 1 N
181 180 adantr φ y 0 N 1 2 nd 1 st T Fn 1 N
182 fzss2 N y + 1 1 y + 1 1 N
183 164 182 syl φ y 0 N 1 1 y + 1 1 N
184 142 96 eleqtrdi y 0 N 1 y + 1 1
185 eluzfz1 y + 1 1 1 1 y + 1
186 184 185 syl y 0 N 1 1 1 y + 1
187 186 adantl φ y 0 N 1 1 1 y + 1
188 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
189 181 183 187 188 syl3anc φ y 0 N 1 2 nd 1 st T 1 2 nd 1 st T 1 y + 1
190 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
191 132 135 190 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
192 150 189 191 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
193 130 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
194 189 193 syl φ y 0 N 1 2 nd 1 st T 1 y + 1 × 1 2 nd 1 st T 1 = 1
195 192 194 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
196 195 adantr φ y 0 N 1 2 nd 1 st T 1 1 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
197 129 175 176 176 177 178 196 ofval φ y 0 N 1 2 nd 1 st T 1 1 N 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 2 nd 1 st T 1 = 1 st 1 st T 2 nd 1 st T 1 + 1
198 100 197 mpidan φ 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 2 nd 1 st T 1 = 1 st 1 st T 2 nd 1 st T 1 + 1
199 127 198 sylan9eqr φ y 0 N 1 p = 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 p 2 nd 1 st T 1 = 1 st 1 st T 2 nd 1 st T 1 + 1
200 199 adantllr φ p ran F y 0 N 1 p = 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 p 2 nd 1 st T 1 = 1 st 1 st T 2 nd 1 st T 1 + 1
201 fveq2 t = T 2 nd t = 2 nd T
202 201 breq2d t = T y < 2 nd t y < 2 nd T
203 202 ifbid t = T if y < 2 nd t y y + 1 = if y < 2 nd T y y + 1
204 2fveq3 t = T 1 st 1 st t = 1 st 1 st T
205 2fveq3 t = T 2 nd 1 st t = 2 nd 1 st T
206 205 imaeq1d t = T 2 nd 1 st t 1 j = 2 nd 1 st T 1 j
207 206 xpeq1d t = T 2 nd 1 st t 1 j × 1 = 2 nd 1 st T 1 j × 1
208 205 imaeq1d t = T 2 nd 1 st t j + 1 N = 2 nd 1 st T j + 1 N
209 208 xpeq1d t = T 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T j + 1 N × 0
210 207 209 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
211 204 210 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
212 203 211 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
213 212 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
214 213 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
215 214 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
216 215 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
217 4 216 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
218 217 rneqd φ ran F = ran 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
219 218 eleq2d φ p ran F p ran 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
220 eqid 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
221 ovex 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 V
222 221 csbex 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 V
223 220 222 elrnmpti p ran 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 p = 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
224 219 223 bitrdi φ p ran F y 0 N 1 p = 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
225 6 adantr φ y 0 N 1 2 nd T = 0
226 elfzle1 y 0 N 1 0 y
227 226 adantl φ y 0 N 1 0 y
228 225 227 eqbrtrd φ y 0 N 1 2 nd T y
229 0re 0
230 6 229 eqeltrdi φ 2 nd T
231 lenlt 2 nd T y 2 nd T y ¬ y < 2 nd T
232 230 9 231 syl2an φ y 0 N 1 2 nd T y ¬ y < 2 nd T
233 228 232 mpbid φ y 0 N 1 ¬ y < 2 nd T
234 233 iffalsed φ y 0 N 1 if y < 2 nd T y y + 1 = y + 1
235 234 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
236 ovex y + 1 V
237 oveq2 j = y + 1 1 j = 1 y + 1
238 237 imaeq2d j = y + 1 2 nd 1 st T 1 j = 2 nd 1 st T 1 y + 1
239 238 xpeq1d j = y + 1 2 nd 1 st T 1 j × 1 = 2 nd 1 st T 1 y + 1 × 1
240 oveq1 j = y + 1 j + 1 = y + 1 + 1
241 240 oveq1d j = y + 1 j + 1 N = y + 1 + 1 N
242 241 imaeq2d j = y + 1 2 nd 1 st T j + 1 N = 2 nd 1 st T y + 1 + 1 N
243 242 xpeq1d j = y + 1 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T y + 1 + 1 N × 0
244 239 243 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
245 244 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
246 236 245 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
247 235 246 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
248 247 eqeq2d φ y 0 N 1 p = 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 p = 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
249 248 rexbidva φ y 0 N 1 p = 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 p = 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
250 224 249 bitrd φ p ran F y 0 N 1 p = 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
251 250 biimpa φ p ran F y 0 N 1 p = 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
252 200 251 r19.29a φ p ran F p 2 nd 1 st T 1 = 1 st 1 st T 2 nd 1 st T 1 + 1
253 eqtr3 p 2 nd 1 st T 1 = 1 st 1 st T 2 nd 1 st T 1 + 1 K = 1 st 1 st T 2 nd 1 st T 1 + 1 p 2 nd 1 st T 1 = K
254 253 ex p 2 nd 1 st T 1 = 1 st 1 st T 2 nd 1 st T 1 + 1 K = 1 st 1 st T 2 nd 1 st T 1 + 1 p 2 nd 1 st T 1 = K
255 252 254 syl φ p ran F K = 1 st 1 st T 2 nd 1 st T 1 + 1 p 2 nd 1 st T 1 = K
256 255 necon3d φ p ran F p 2 nd 1 st T 1 K K 1 st 1 st T 2 nd 1 st T 1 + 1
257 256 rexlimdva φ p ran F p 2 nd 1 st T 1 K K 1 st 1 st T 2 nd 1 st T 1 + 1
258 126 257 mpd φ K 1 st 1 st T 2 nd 1 st T 1 + 1
259 108 109 117 258 leneltd φ 1 st 1 st T 2 nd 1 st T 1 + 1 < K
260 elfzo0 1 st 1 st T 2 nd 1 st T 1 + 1 0 ..^ K 1 st 1 st T 2 nd 1 st T 1 + 1 0 K 1 st 1 st T 2 nd 1 st T 1 + 1 < K
261 104 107 259 260 syl3anbrc φ 1 st 1 st T 2 nd 1 st T 1 + 1 0 ..^ K
262 261 adantr φ n = 2 nd 1 st T 1 1 st 1 st T 2 nd 1 st T 1 + 1 0 ..^ K
263 80 262 eqeltrd φ n = 2 nd 1 st T 1 1 st 1 st T n + 1 0 ..^ K
264 263 adantlr φ n 1 N n = 2 nd 1 st T 1 1 st 1 st T n + 1 0 ..^ K
265 87 ffvelrnda φ n 1 N 1 st 1 st T n 0 ..^ K
266 elfzonn0 1 st 1 st T n 0 ..^ K 1 st 1 st T n 0
267 265 266 syl φ n 1 N 1 st 1 st T n 0
268 267 nn0cnd φ n 1 N 1 st 1 st T n
269 268 addid1d φ n 1 N 1 st 1 st T n + 0 = 1 st 1 st T n
270 269 265 eqeltrd φ n 1 N 1 st 1 st T n + 0 0 ..^ K
271 270 adantr φ n 1 N ¬ n = 2 nd 1 st T 1 1 st 1 st T n + 0 0 ..^ K
272 75 77 264 271 ifbothda φ n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 0 ..^ K
273 272 fmpttd φ n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 : 1 N 0 ..^ K
274 ovex 0 ..^ K V
275 274 48 elmap n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 0 ..^ K 1 N n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 : 1 N 0 ..^ K
276 273 275 sylibr φ n 1 N 1 st 1 st T n + if n = 2 nd 1 st T 1 1 0 0 ..^ K 1 N
277 simpr φ n 1 N 1 n 1 N 1
278 1z 1
279 13 278 jctil φ 1 N 1
280 elfzelz n 1 N 1 n
281 280 278 jctir n 1 N 1 n 1
282 fzaddel 1 N 1 n 1 n 1 N 1 n + 1 1 + 1 N - 1 + 1
283 279 281 282 syl2an φ n 1 N 1 n 1 N 1 n + 1 1 + 1 N - 1 + 1
284 277 283 mpbid φ n 1 N 1 n + 1 1 + 1 N - 1 + 1
285 158 oveq2d φ 1 + 1 N - 1 + 1 = 1 + 1 N
286 285 adantr φ n 1 N 1 1 + 1 N - 1 + 1 = 1 + 1 N
287 284 286 eleqtrd φ n 1 N 1 n + 1 1 + 1 N
288 287 ralrimiva φ n 1 N 1 n + 1 1 + 1 N
289 simpr φ y 1 + 1 N y 1 + 1 N
290 peano2z 1 1 + 1
291 278 290 ax-mp 1 + 1
292 11 291 jctil φ 1 + 1 N
293 elfzelz y 1 + 1 N y
294 293 278 jctir y 1 + 1 N y 1
295 fzsubel 1 + 1 N y 1 y 1 + 1 N y 1 1 + 1 - 1 N 1
296 292 294 295 syl2an φ y 1 + 1 N y 1 + 1 N y 1 1 + 1 - 1 N 1
297 289 296 mpbid φ y 1 + 1 N y 1 1 + 1 - 1 N 1
298 ax-1cn 1
299 298 298 pncan3oi 1 + 1 - 1 = 1
300 299 oveq1i 1 + 1 - 1 N 1 = 1 N 1
301 297 300 eleqtrdi φ y 1 + 1 N y 1 1 N 1
302 293 zcnd y 1 + 1 N y
303 elfznn n 1 N 1 n
304 303 nncnd n 1 N 1 n
305 subadd2 y 1 n y 1 = n n + 1 = y
306 298 305 mp3an2 y n y 1 = n n + 1 = y
307 306 bicomd y n n + 1 = y y 1 = n
308 eqcom y = n + 1 n + 1 = y
309 eqcom n = y 1 y 1 = n
310 307 308 309 3bitr4g y n y = n + 1 n = y 1
311 302 304 310 syl2an y 1 + 1 N n 1 N 1 y = n + 1 n = y 1
312 311 ralrimiva y 1 + 1 N n 1 N 1 y = n + 1 n = y 1
313 312 adantl φ y 1 + 1 N n 1 N 1 y = n + 1 n = y 1
314 reu6i y 1 1 N 1 n 1 N 1 y = n + 1 n = y 1 ∃! n 1 N 1 y = n + 1
315 301 313 314 syl2anc φ y 1 + 1 N ∃! n 1 N 1 y = n + 1
316 315 ralrimiva φ y 1 + 1 N ∃! n 1 N 1 y = n + 1
317 eqid n 1 N 1 n + 1 = n 1 N 1 n + 1
318 317 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
319 288 316 318 sylanbrc φ n 1 N 1 n + 1 : 1 N 1 1-1 onto 1 + 1 N
320 f1osng N 1 V N 1 : N 1-1 onto 1
321 1 130 320 sylancl φ N 1 : N 1-1 onto 1
322 14 16 ltnled φ N 1 < N ¬ N N 1
323 20 322 mpbid φ ¬ N N 1
324 elfzle2 N 1 N 1 N N 1
325 323 324 nsyl φ ¬ N 1 N 1
326 disjsn 1 N 1 N = ¬ N 1 N 1
327 325 326 sylibr φ 1 N 1 N =
328 1re 1
329 328 ltp1i 1 < 1 + 1
330 291 zrei 1 + 1
331 328 330 ltnlei 1 < 1 + 1 ¬ 1 + 1 1
332 329 331 mpbi ¬ 1 + 1 1
333 elfzle1 1 1 + 1 N 1 + 1 1
334 332 333 mto ¬ 1 1 + 1 N
335 disjsn 1 + 1 N 1 = ¬ 1 1 + 1 N
336 334 335 mpbir 1 + 1 N 1 =
337 336 a1i φ 1 + 1 N 1 =
338 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
339 319 321 327 337 338 syl22anc φ n 1 N 1 n + 1 N 1 : 1 N 1 N 1-1 onto 1 + 1 N 1
340 130 a1i φ 1 V
341 158 97 eqeltrd φ N - 1 + 1 1
342 uzid N 1 N 1 N 1
343 peano2uz N 1 N 1 N - 1 + 1 N 1
344 13 342 343 3syl φ N - 1 + 1 N 1
345 158 344 eqeltrrd φ N N 1
346 fzsplit2 N - 1 + 1 1 N N 1 1 N = 1 N 1 N - 1 + 1 N
347 341 345 346 syl2anc φ 1 N = 1 N 1 N - 1 + 1 N
348 158 oveq1d φ N - 1 + 1 N = N N
349 fzsn N N N = N
350 11 349 syl φ N N = N
351 348 350 eqtrd φ N - 1 + 1 N = N
352 351 uneq2d φ 1 N 1 N - 1 + 1 N = 1 N 1 N
353 347 352 eqtr2d φ 1 N 1 N = 1 N
354 iftrue n = N if n = N 1 n + 1 = 1
355 354 adantl φ n = N if n = N 1 n + 1 = 1
356 1 340 353 355 fmptapd φ n 1 N 1 if n = N 1 n + 1 N 1 = n 1 N if n = N 1 n + 1
357 eleq1 n = N n 1 N 1 N 1 N 1
358 357 notbid n = N ¬ n 1 N 1 ¬ N 1 N 1
359 325 358 syl5ibrcom φ n = N ¬ n 1 N 1
360 359 necon2ad φ n 1 N 1 n N
361 360 imp φ n 1 N 1 n N
362 ifnefalse n N if n = N 1 n + 1 = n + 1
363 361 362 syl φ n 1 N 1 if n = N 1 n + 1 = n + 1
364 363 mpteq2dva φ n 1 N 1 if n = N 1 n + 1 = n 1 N 1 n + 1
365 364 uneq1d φ n 1 N 1 if n = N 1 n + 1 N 1 = n 1 N 1 n + 1 N 1
366 356 365 eqtr3d φ n 1 N if n = N 1 n + 1 = n 1 N 1 n + 1 N 1
367 347 352 eqtrd φ 1 N = 1 N 1 N
368 uzid 1 1 1
369 peano2uz 1 1 1 + 1 1
370 278 368 369 mp2b 1 + 1 1
371 fzsplit2 1 + 1 1 N 1 1 N = 1 1 1 + 1 N
372 370 97 371 sylancr φ 1 N = 1 1 1 + 1 N
373 fzsn 1 1 1 = 1
374 278 373 ax-mp 1 1 = 1
375 374 uneq1i 1 1 1 + 1 N = 1 1 + 1 N
376 375 equncomi 1 1 1 + 1 N = 1 + 1 N 1
377 372 376 eqtrdi φ 1 N = 1 + 1 N 1
378 366 367 377 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
379 339 378 mpbird φ n 1 N if n = N 1 n + 1 : 1 N 1-1 onto 1 N
380 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
381 93 379 380 syl2anc φ 2 nd 1 st T n 1 N if n = N 1 n + 1 : 1 N 1-1 onto 1 N
382 f1oeq1 f = 2 nd 1 st T n 1 N if n = N 1 n + 1 f : 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
383 52 382 elab 2 nd 1 st T n 1 N if n = N 1 n + 1 f | f : 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
384 381 383 sylibr φ 2 nd 1 st T n 1 N if n = N 1 n + 1 f | f : 1 N 1-1 onto 1 N
385 276 384 opelxpd φ 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 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
386 1 nnnn0d φ N 0
387 nn0fz0 N 0 N 0 N
388 386 387 sylib φ N 0 N
389 385 388 opelxpd φ 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 N 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
390 elrab3t t t = 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 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 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 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 N 0 ..^ K 1 N × f | f : 1 N 1-1 onto 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 N 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 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
391 73 389 390 syl2anc φ 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 N 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 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
392 7 391 mpbird φ 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 N 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
393 392 2 eleqtrrdi φ 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 N S
394 fveqeq2 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 N = T 2 nd 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 N = N 2 nd T = N
395 27 394 syl5ibcom φ 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 N = T 2 nd T = N
396 1 nnne0d φ N 0
397 neeq1 2 nd T = N 2 nd T 0 N 0
398 396 397 syl5ibrcom φ 2 nd T = N 2 nd T 0
399 395 398 syld φ 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 N = T 2 nd T 0
400 399 necon2d φ 2 nd T = 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 N T
401 6 400 mpd φ 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 N T
402 neeq1 z = 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 N z T 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 N T
403 402 rspcev 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 N S 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 N T z S z T
404 393 401 403 syl2anc φ z S z T