Step | Hyp | Ref
| Expression |
1 | | elsuc 4413 |
. 2
⊢ (℘1A ∈ (M +c 1c) ↔
∃b ∈ M ∃x ∈ ∼ b℘1A = (b ∪
{x})) |
2 | | vex 2862 |
. . . . . 6
⊢ b ∈
V |
3 | | vex 2862 |
. . . . . 6
⊢ x ∈
V |
4 | 2, 3 | pw1eqadj 4332 |
. . . . 5
⊢ (℘1A = (b ∪
{x}) ↔ ∃y∃z(A = (y ∪
{z}) ∧
b = ℘1y ∧ x = {z})) |
5 | | eleq1 2413 |
. . . . . . . . . . . 12
⊢ (b = ℘1y → (b
∈ M
↔ ℘1y ∈ M)) |
6 | 5 | adantr 451 |
. . . . . . . . . . 11
⊢ ((b = ℘1y ∧ x = {z}) →
(b ∈
M ↔ ℘1y ∈ M)) |
7 | | compleq 3243 |
. . . . . . . . . . . . 13
⊢ (b = ℘1y → ∼ b
= ∼ ℘1y) |
8 | | eleq12 2415 |
. . . . . . . . . . . . . 14
⊢ ((x = {z} ∧ ∼ b =
∼ ℘1y) → (x
∈ ∼ b
↔ {z} ∈ ∼ ℘1y)) |
9 | | snex 4111 |
. . . . . . . . . . . . . . . 16
⊢ {z} ∈
V |
10 | 9 | elcompl 3225 |
. . . . . . . . . . . . . . 15
⊢ ({z} ∈ ∼ ℘1y ↔ ¬ {z} ∈ ℘1y) |
11 | | snelpw1 4146 |
. . . . . . . . . . . . . . 15
⊢ ({z} ∈ ℘1y ↔ z ∈ y) |
12 | 10, 11 | xchbinx 301 |
. . . . . . . . . . . . . 14
⊢ ({z} ∈ ∼ ℘1y ↔ ¬ z
∈ y) |
13 | 8, 12 | syl6bb 252 |
. . . . . . . . . . . . 13
⊢ ((x = {z} ∧ ∼ b =
∼ ℘1y) → (x
∈ ∼ b
↔ ¬ z ∈ y)) |
14 | 7, 13 | sylan2 460 |
. . . . . . . . . . . 12
⊢ ((x = {z} ∧ b = ℘1y) → (x
∈ ∼ b
↔ ¬ z ∈ y)) |
15 | 14 | ancoms 439 |
. . . . . . . . . . 11
⊢ ((b = ℘1y ∧ x = {z}) →
(x ∈
∼ b ↔ ¬ z ∈ y)) |
16 | 6, 15 | anbi12d 691 |
. . . . . . . . . 10
⊢ ((b = ℘1y ∧ x = {z}) →
((b ∈
M ∧
x ∈ ∼
b) ↔ (℘1y ∈ M ∧ ¬ z ∈ y))) |
17 | 16 | anbi2d 684 |
. . . . . . . . 9
⊢ ((b = ℘1y ∧ x = {z}) →
((M ∈
Nn ∧ (b ∈ M ∧ x ∈ ∼ b)) ↔ (M
∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y)))) |
18 | | ncfinlower 4483 |
. . . . . . . . . . . 12
⊢ ((M ∈ Nn ∧ ℘1y ∈ M ∧ ℘1y ∈ M) → ∃k ∈ Nn (y ∈ k ∧ y ∈ k)) |
19 | 18 | 3anidm23 1241 |
. . . . . . . . . . 11
⊢ ((M ∈ Nn ∧ ℘1y ∈ M) → ∃k ∈ Nn (y ∈ k ∧ y ∈ k)) |
20 | 19 | adantrr 697 |
. . . . . . . . . 10
⊢ ((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y)) → ∃k ∈ Nn (y ∈ k ∧ y ∈ k)) |
21 | | simp3l 983 |
. . . . . . . . . . . . . . 15
⊢ ((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) → k
∈ Nn
) |
22 | | simp3rr 1029 |
. . . . . . . . . . . . . . 15
⊢ ((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) → y
∈ k) |
23 | | nnpweq 4523 |
. . . . . . . . . . . . . . 15
⊢ ((k ∈ Nn ∧ y ∈ k ∧ y ∈ k) → ∃n ∈ Nn (℘y ∈ n ∧ ℘y ∈ n)) |
24 | 21, 22, 22, 23 | syl3anc 1182 |
. . . . . . . . . . . . . 14
⊢ ((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) → ∃n ∈ Nn (℘y ∈ n ∧ ℘y ∈ n)) |
25 | | simpl1 958 |
. . . . . . . . . . . . . . . . . 18
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → M
∈ Nn
) |
26 | | simprl 732 |
. . . . . . . . . . . . . . . . . 18
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → n
∈ Nn
) |
27 | | simpl2l 1008 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → ℘1y ∈ M) |
28 | | simprrr 741 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → ℘y ∈ n) |
29 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . 20
⊢ y ∈
V |
30 | | pw1eq 4143 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (a = y →
℘1a = ℘1y) |
31 | 30 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (a = y →
(℘1a ∈ M ↔ ℘1y ∈ M)) |
32 | | pweq 3725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (a = y →
℘a =
℘y) |
33 | 32 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (a = y →
(℘a
∈ n
↔ ℘y ∈ n)) |
34 | 31, 33 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (a = y →
((℘1a ∈ M ∧ ℘a ∈ n) ↔
(℘1y ∈ M ∧ ℘y ∈ n))) |
35 | 29, 34 | spcev 2946 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((℘1y ∈ M ∧ ℘y ∈ n) →
∃a(℘1a ∈ M ∧ ℘a ∈ n)) |
36 | 27, 28, 35 | syl2anc 642 |
. . . . . . . . . . . . . . . . . 18
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → ∃a(℘1a ∈ M ∧ ℘a ∈ n)) |
37 | | df-sfin 4446 |
. . . . . . . . . . . . . . . . . 18
⊢ ( Sfin (M,
n) ↔ (M ∈ Nn ∧ n ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ n))) |
38 | 25, 26, 36, 37 | syl3anbrc 1136 |
. . . . . . . . . . . . . . . . 17
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → Sfin (M,
n)) |
39 | | peano2 4403 |
. . . . . . . . . . . . . . . . . . 19
⊢ (M ∈ Nn → (M
+c 1c) ∈
Nn ) |
40 | 25, 39 | syl 15 |
. . . . . . . . . . . . . . . . . 18
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → (M
+c 1c) ∈
Nn ) |
41 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((n ∈ Nn ∧ n ∈ Nn ) → (n
+c n) ∈ Nn
) |
42 | 41 | anidms 626 |
. . . . . . . . . . . . . . . . . . 19
⊢ (n ∈ Nn → (n
+c n) ∈ Nn
) |
43 | 26, 42 | syl 15 |
. . . . . . . . . . . . . . . . . 18
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → (n
+c n) ∈ Nn
) |
44 | | pw1un 4163 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℘1(y ∪ {z}) =
(℘1y ∪ ℘1{z}) |
45 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ z ∈
V |
46 | 45 | pw1sn 4165 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℘1{z} = {{z}} |
47 | 46 | uneq2i 3415 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (℘1y ∪ ℘1{z}) = (℘1y ∪ {{z}}) |
48 | 44, 47 | eqtri 2373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℘1(y ∪ {z}) =
(℘1y ∪ {{z}}) |
49 | | simpl2r 1009 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → ¬ z ∈ y) |
50 | 49, 11 | sylnibr 296 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → ¬ {z} ∈ ℘1y) |
51 | 9 | elsuci 4414 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((℘1y ∈ M ∧ ¬ {z} ∈ ℘1y) → (℘1y ∪ {{z}})
∈ (M
+c 1c)) |
52 | 27, 50, 51 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → (℘1y ∪ {{z}})
∈ (M
+c 1c)) |
53 | 48, 52 | syl5eqel 2437 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → ℘1(y ∪ {z})
∈ (M
+c 1c)) |
54 | | simpl3l 1010 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → k
∈ Nn
) |
55 | 22 | adantr 451 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → y
∈ k) |
56 | 45 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (z ∈ ∼ y ↔ ¬ z
∈ y) |
57 | 49, 56 | sylibr 203 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → z
∈ ∼ y) |
58 | | nnadjoinpw 4521 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ (y ∈ k ∧ z ∈ ∼ y) ∧ ℘y ∈ n) →
℘(y
∪ {z}) ∈ (n
+c n)) |
59 | 54, 26, 55, 57, 28, 58 | syl221anc 1193 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → ℘(y ∪
{z}) ∈
(n +c n)) |
60 | 29, 9 | unex 4106 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (y ∪ {z})
∈ V |
61 | | pw1eq 4143 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (a = (y ∪
{z}) → ℘1a = ℘1(y ∪ {z})) |
62 | 61 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (a = (y ∪
{z}) → (℘1a ∈ (M +c 1c) ↔
℘1(y ∪ {z})
∈ (M
+c 1c))) |
63 | | pweq 3725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (a = (y ∪
{z}) → ℘a = ℘(y ∪
{z})) |
64 | 63 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (a = (y ∪
{z}) → (℘a ∈ (n
+c n) ↔ ℘(y ∪
{z}) ∈
(n +c n))) |
65 | 62, 64 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (a = (y ∪
{z}) → ((℘1a ∈ (M +c 1c) ∧ ℘a ∈ (n +c n)) ↔ (℘1(y ∪ {z})
∈ (M
+c 1c) ∧
℘(y
∪ {z}) ∈ (n
+c n)))) |
66 | 60, 65 | spcev 2946 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((℘1(y ∪ {z})
∈ (M
+c 1c) ∧
℘(y
∪ {z}) ∈ (n
+c n)) → ∃a(℘1a ∈ (M +c 1c) ∧ ℘a ∈ (n +c n))) |
67 | 53, 59, 66 | syl2anc 642 |
. . . . . . . . . . . . . . . . . 18
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → ∃a(℘1a ∈ (M +c 1c) ∧ ℘a ∈ (n +c n))) |
68 | | df-sfin 4446 |
. . . . . . . . . . . . . . . . . 18
⊢ ( Sfin ((M
+c 1c), (n +c n)) ↔ ((M
+c 1c) ∈
Nn ∧ (n +c n) ∈ Nn ∧ ∃a(℘1a ∈ (M +c 1c) ∧ ℘a ∈ (n +c n)))) |
69 | 40, 43, 67, 68 | syl3anbrc 1136 |
. . . . . . . . . . . . . . . . 17
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → Sfin ((M
+c 1c), (n +c n))) |
70 | 38, 69 | jca 518 |
. . . . . . . . . . . . . . . 16
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (℘y ∈ n ∧ ℘y ∈ n))) → ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n)))) |
71 | 70 | expr 598 |
. . . . . . . . . . . . . . 15
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ n ∈ Nn ) → ((℘y ∈ n ∧ ℘y ∈ n) → ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n))))) |
72 | 71 | reximdva 2726 |
. . . . . . . . . . . . . 14
⊢ ((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) → (∃n ∈ Nn (℘y ∈ n ∧ ℘y ∈ n) → ∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n))))) |
73 | 24, 72 | mpd 14 |
. . . . . . . . . . . . 13
⊢ ((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) → ∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n)))) |
74 | 73 | 3expa 1151 |
. . . . . . . . . . . 12
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y)) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) → ∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n)))) |
75 | 74 | expr 598 |
. . . . . . . . . . 11
⊢ (((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y)) ∧ k ∈ Nn ) → ((y
∈ k ∧ y ∈ k) →
∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n))))) |
76 | 75 | rexlimdva 2738 |
. . . . . . . . . 10
⊢ ((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y)) → (∃k ∈ Nn (y ∈ k ∧ y ∈ k) → ∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n))))) |
77 | 20, 76 | mpd 14 |
. . . . . . . . 9
⊢ ((M ∈ Nn ∧ (℘1y ∈ M ∧ ¬ z ∈ y)) → ∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n)))) |
78 | 17, 77 | syl6bi 219 |
. . . . . . . 8
⊢ ((b = ℘1y ∧ x = {z}) →
((M ∈
Nn ∧ (b ∈ M ∧ x ∈ ∼ b)) → ∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n))))) |
79 | 78 | 3adant1 973 |
. . . . . . 7
⊢ ((A = (y ∪
{z}) ∧
b = ℘1y ∧ x = {z}) →
((M ∈
Nn ∧ (b ∈ M ∧ x ∈ ∼ b)) → ∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n))))) |
80 | 79 | com12 27 |
. . . . . 6
⊢ ((M ∈ Nn ∧ (b ∈ M ∧ x ∈ ∼ b)) → ((A =
(y ∪ {z}) ∧ b = ℘1y ∧ x = {z}) →
∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n))))) |
81 | 80 | exlimdvv 1637 |
. . . . 5
⊢ ((M ∈ Nn ∧ (b ∈ M ∧ x ∈ ∼ b)) → (∃y∃z(A = (y ∪
{z}) ∧
b = ℘1y ∧ x = {z}) →
∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n))))) |
82 | 4, 81 | syl5bi 208 |
. . . 4
⊢ ((M ∈ Nn ∧ (b ∈ M ∧ x ∈ ∼ b)) → (℘1A = (b ∪
{x}) → ∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n))))) |
83 | 82 | rexlimdvva 2745 |
. . 3
⊢ (M ∈ Nn → (∃b ∈ M ∃x ∈ ∼ b℘1A = (b ∪
{x}) → ∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n))))) |
84 | 83 | imp 418 |
. 2
⊢ ((M ∈ Nn ∧ ∃b ∈ M ∃x ∈ ∼ b℘1A = (b ∪
{x})) → ∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n)))) |
85 | 1, 84 | sylan2b 461 |
1
⊢ ((M ∈ Nn ∧ ℘1A ∈ (M +c 1c)) →
∃n ∈ Nn ( Sfin (M,
n) ∧ Sfin ((M
+c 1c), (n +c n)))) |