Step | Hyp | Ref
| Expression |
1 | | nmembers1lem1 6268 |
. 2
Nn 1c c c Tc Tc
|
2 | | breq2 4643 |
. . . . 5
0c c c 0c |
3 | 2 | anbi2d 684 |
. . . 4
0c 1c c c 1c c c 0c |
4 | 3 | rabbidv 2851 |
. . 3
0c Nn 1c c c
Nn 1c c c 0c |
5 | | tceq 6158 |
. . . 4
0c Tc Tc
0c |
6 | | tceq 6158 |
. . . 4
Tc
Tc 0c Tc Tc
Tc Tc
0c |
7 | 5, 6 | syl 15 |
. . 3
0c Tc Tc
Tc Tc 0c |
8 | 4, 7 | eleq12d 2421 |
. 2
0c Nn 1c c
c Tc Tc
Nn 1c c c
0c Tc Tc
0c |
9 | | breq2 4643 |
. . . . 5
c c |
10 | 9 | anbi2d 684 |
. . . 4
1c c c 1c c c |
11 | 10 | rabbidv 2851 |
. . 3
Nn 1c c c
Nn 1c c c |
12 | | tceq 6158 |
. . . 4
Tc
Tc |
13 | | tceq 6158 |
. . . 4
Tc
Tc Tc Tc
Tc Tc |
14 | 12, 13 | syl 15 |
. . 3
Tc Tc
Tc Tc
|
15 | 11, 14 | eleq12d 2421 |
. 2
Nn 1c c c Tc Tc
Nn 1c c c Tc Tc
|
16 | | breq2 4643 |
. . . . 5
1c c c
1c |
17 | 16 | anbi2d 684 |
. . . 4
1c 1c c c 1c c c
1c |
18 | 17 | rabbidv 2851 |
. . 3
1c Nn 1c c c
Nn 1c c c
1c |
19 | | tceq 6158 |
. . . 4
1c Tc Tc 1c |
20 | | tceq 6158 |
. . . 4
Tc
Tc
1c
Tc Tc
Tc Tc
1c |
21 | 19, 20 | syl 15 |
. . 3
1c Tc Tc
Tc Tc
1c |
22 | 18, 21 | eleq12d 2421 |
. 2
1c Nn 1c c
c Tc Tc
Nn 1c c c 1c Tc Tc
1c |
23 | | breq2 4643 |
. . . . 5
c c |
24 | 23 | anbi2d 684 |
. . . 4
1c c c 1c c c |
25 | 24 | rabbidv 2851 |
. . 3
Nn 1c c c
Nn 1c c c |
26 | | tceq 6158 |
. . . 4
Tc
Tc |
27 | | tceq 6158 |
. . . 4
Tc
Tc Tc Tc
Tc Tc |
28 | 26, 27 | syl 15 |
. . 3
Tc Tc
Tc Tc
|
29 | 25, 28 | eleq12d 2421 |
. 2
Nn 1c c c Tc Tc
Nn 1c c c Tc Tc
|
30 | | nmembers1lem2 6269 |
. . 3
Nn 1c c c
0c
0c |
31 | | tc0c 6163 |
. . . . 5
Tc 0c 0c |
32 | | tceq 6158 |
. . . . 5
Tc 0c 0c Tc Tc
0c
Tc 0c |
33 | 31, 32 | ax-mp 5 |
. . . 4
Tc Tc
0c
Tc 0c |
34 | 33, 31 | eqtri 2373 |
. . 3
Tc Tc
0c
0c |
35 | 30, 34 | eleqtrri 2426 |
. 2
Nn 1c c c
0c Tc Tc
0c |
36 | | nntccl 6170 |
. . . 4
Nn Tc Nn |
37 | | nntccl 6170 |
. . . 4
Tc
Nn Tc Tc
Nn |
38 | 36, 37 | syl 15 |
. . 3
Nn Tc Tc
Nn |
39 | | nmembers1lem3 6270 |
. . . 4
Nn Tc Tc
Nn
Nn 1c c c Tc Tc
Nn 1c c c
1c Tc Tc 1c |
40 | | nnnc 6146 |
. . . . . . 7
Nn NC |
41 | | 1cnc 6139 |
. . . . . . . . . . 11
1c
NC |
42 | | tcdi 6164 |
. . . . . . . . . . 11
NC 1c NC Tc
1c
Tc Tc 1c |
43 | 41, 42 | mpan2 652 |
. . . . . . . . . 10
NC Tc 1c
Tc Tc 1c |
44 | | tc1c 6165 |
. . . . . . . . . . 11
Tc 1c 1c |
45 | 44 | addceq2i 4387 |
. . . . . . . . . 10
Tc Tc 1c Tc 1c |
46 | 43, 45 | syl6eq 2401 |
. . . . . . . . 9
NC Tc 1c
Tc 1c |
47 | | tceq 6158 |
. . . . . . . . 9
Tc
1c
Tc 1c Tc Tc
1c
Tc Tc 1c |
48 | 46, 47 | syl 15 |
. . . . . . . 8
NC Tc Tc
1c
Tc Tc 1c |
49 | | tccl 6160 |
. . . . . . . . . 10
NC Tc NC |
50 | | tcdi 6164 |
. . . . . . . . . . 11
Tc NC 1c
NC Tc Tc 1c
Tc Tc Tc 1c |
51 | 41, 50 | mpan2 652 |
. . . . . . . . . 10
Tc
NC Tc Tc 1c Tc Tc
Tc 1c |
52 | 49, 51 | syl 15 |
. . . . . . . . 9
NC Tc Tc 1c Tc Tc
Tc 1c |
53 | 44 | addceq2i 4387 |
. . . . . . . . 9
Tc Tc
Tc 1c
Tc Tc 1c |
54 | 52, 53 | syl6eq 2401 |
. . . . . . . 8
NC Tc Tc 1c Tc Tc
1c |
55 | 48, 54 | eqtrd 2385 |
. . . . . . 7
NC Tc Tc
1c
Tc Tc
1c |
56 | 40, 55 | syl 15 |
. . . . . 6
Nn Tc Tc
1c
Tc Tc
1c |
57 | 56 | eleq2d 2420 |
. . . . 5
Nn Nn 1c c
c 1c Tc Tc
1c Nn 1c c c
1c Tc Tc 1c |
58 | 57 | adantr 451 |
. . . 4
Nn Tc Tc
Nn
Nn 1c c c
1c Tc Tc
1c Nn 1c c c
1c Tc Tc 1c |
59 | 39, 58 | sylibrd 225 |
. . 3
Nn Tc Tc
Nn
Nn 1c c c Tc Tc
Nn 1c c c
1c Tc Tc
1c |
60 | 38, 59 | mpdan 649 |
. 2
Nn Nn 1c c
c Tc Tc
Nn 1c c c
1c Tc Tc
1c |
61 | 1, 8, 15, 22, 29, 35, 60 | finds 4411 |
1
Nn Nn 1c c c Tc Tc
|