Step | Hyp | Ref
| Expression |
1 | | finnc 6243 |
. . 3
Spac
Fin Nc
Spac Nn |
2 | | risset 2661 |
. . . 4
Nc Spac
Nn Nn Nc Spac |
3 | | nchoicelem13 6301 |
. . . . . . 7
NC 1c c Nc
Spac |
4 | 3 | ad2antlr 707 |
. . . . . 6
c We NC NC Nn 1c c Nc Spac |
5 | | 1cnc 6139 |
. . . . . . . 8
1c
NC |
6 | | fvex 5339 |
. . . . . . . . 9
Spac |
7 | 6 | ncelncsi 6121 |
. . . . . . . 8
Nc Spac
NC |
8 | | dflec2 6210 |
. . . . . . . 8
1c NC Nc Spac
NC 1c c Nc Spac
NC Nc Spac
1c |
9 | 5, 7, 8 | mp2an 653 |
. . . . . . 7
1c c Nc Spac
NC Nc Spac
1c |
10 | | eqtr 2370 |
. . . . . . . . . . . 12
Nc Spac
Nc Spac
1c 1c |
11 | 10 | ancoms 439 |
. . . . . . . . . . 11
Nc Spac 1c Nc Spac
1c |
12 | | eqtr2 2371 |
. . . . . . . . . . . . 13
Nc Spac
1c Nc Spac 1c |
13 | 12 | ex 423 |
. . . . . . . . . . . 12
Nc Spac 1c Nc Spac
1c |
14 | 13 | adantl 452 |
. . . . . . . . . . 11
Nc Spac 1c Nc Spac
1c Nc Spac
1c |
15 | 11, 14 | jcai 522 |
. . . . . . . . . 10
Nc Spac 1c Nc Spac
1c Nc Spac
1c |
16 | | addceq2 4384 |
. . . . . . . . . . . . . . . . . 18
1c
1c |
17 | | addccom 4406 |
. . . . . . . . . . . . . . . . . 18
1c
1c
|
18 | 16, 17 | syl6eq 2401 |
. . . . . . . . . . . . . . . . 17
1c
1c
|
19 | 18 | eqeq2d 2364 |
. . . . . . . . . . . . . . . 16
1c 1c |
20 | 19 | rspcev 2955 |
. . . . . . . . . . . . . . 15
1c NC 1c
NC |
21 | 5, 20 | mpan 651 |
. . . . . . . . . . . . . 14
1c
NC |
22 | | nnnc 6146 |
. . . . . . . . . . . . . . . 16
Nn NC |
23 | | dflec2 6210 |
. . . . . . . . . . . . . . . 16
NC NC c
NC |
24 | 22, 23 | sylan2 460 |
. . . . . . . . . . . . . . 15
NC Nn c
NC |
25 | 24 | ancoms 439 |
. . . . . . . . . . . . . 14
Nn NC c
NC |
26 | 21, 25 | syl5ibr 212 |
. . . . . . . . . . . . 13
Nn NC 1c c |
27 | 26 | adantll 694 |
. . . . . . . . . . . 12
c We NC
NC Nn
NC 1c c |
28 | | nclenn 6249 |
. . . . . . . . . . . . . . 15
NC Nn c Nn |
29 | 28 | 3expia 1153 |
. . . . . . . . . . . . . 14
NC Nn c
Nn |
30 | 29 | ancoms 439 |
. . . . . . . . . . . . 13
Nn NC c
Nn |
31 | 30 | adantll 694 |
. . . . . . . . . . . 12
c We NC
NC Nn
NC c
Nn |
32 | | nchoicelem16 6304 |
. . . . . . . . . . . . . . . . . 18
c We NC NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
33 | | addceq2 4384 |
. . . . . . . . . . . . . . . . . . . . . . 23
0c 1c 1c 0c |
34 | | addcid1 4405 |
. . . . . . . . . . . . . . . . . . . . . . 23
1c
0c
1c |
35 | 33, 34 | syl6eq 2401 |
. . . . . . . . . . . . . . . . . . . . . 22
0c 1c 1c |
36 | 35 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . 21
0c Nc Spac
1c
Nc Spac 1c |
37 | 36 | imbi1d 308 |
. . . . . . . . . . . . . . . . . . . 20
0c Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac
1c Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
38 | 37 | ralbidv 2634 |
. . . . . . . . . . . . . . . . . . 19
0c NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c
NC Nc Spac
1c Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
39 | 38 | imbi2d 307 |
. . . . . . . . . . . . . . . . . 18
0c c We NC NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c c We NC NC Nc Spac
1c Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
40 | | addceq2 4384 |
. . . . . . . . . . . . . . . . . . . . . 22
1c
1c |
41 | 40 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . 21
Nc Spac 1c Nc Spac
1c |
42 | 41 | imbi1d 308 |
. . . . . . . . . . . . . . . . . . . 20
Nc Spac
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
43 | 42 | ralbidv 2634 |
. . . . . . . . . . . . . . . . . . 19
NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c
NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
44 | 43 | imbi2d 307 |
. . . . . . . . . . . . . . . . . 18
c We NC NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c c We NC NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
45 | | addceq2 4384 |
. . . . . . . . . . . . . . . . . . . . . . 23
1c 1c 1c
1c |
46 | 45 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . . 22
1c Nc Spac
1c
Nc Spac 1c
1c |
47 | 46 | imbi1d 308 |
. . . . . . . . . . . . . . . . . . . . 21
1c Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac
1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
48 | 47 | ralbidv 2634 |
. . . . . . . . . . . . . . . . . . . 20
1c NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c
NC Nc Spac
1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
49 | | fveq2 5328 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Spac Spac
|
50 | 49 | nceqd 6110 |
. . . . . . . . . . . . . . . . . . . . . . 23
Nc Spac
Nc Spac |
51 | 50 | eqeq1d 2361 |
. . . . . . . . . . . . . . . . . . . . . 22
Nc Spac 1c
1c Nc Spac
1c
1c |
52 | | tceq 6158 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Tc
Tc |
53 | 52 | fveq2d 5332 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Spac Tc Spac Tc |
54 | 53 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . 23
Spac Tc
Fin Spac Tc
Fin |
55 | 53 | nceqd 6110 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nc Spac Tc
Nc Spac Tc |
56 | | tceq 6158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Nc Spac
Nc Spac
Tc Nc Spac Tc Nc Spac |
57 | 50, 56 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Tc Nc Spac Tc Nc Spac |
58 | 57 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Tc Nc Spac
1c
Tc Nc Spac
1c |
59 | 55, 58 | eqeq12d 2367 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nc Spac Tc Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
1c |
60 | 57 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Tc Nc Spac
2c
Tc Nc Spac
2c |
61 | 55, 60 | eqeq12d 2367 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nc Spac Tc Tc Nc Spac
2c
Nc Spac Tc
Tc Nc Spac
2c |
62 | 59, 61 | orbi12d 690 |
. . . . . . . . . . . . . . . . . . . . . . 23
Nc Spac
Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
63 | 54, 62 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . . . . 22
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Spac
Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
64 | 51, 63 | imbi12d 311 |
. . . . . . . . . . . . . . . . . . . . 21
Nc Spac
1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac
1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
65 | 64 | cbvralv 2835 |
. . . . . . . . . . . . . . . . . . . 20
NC Nc Spac
1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c
NC Nc Spac
1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
66 | 48, 65 | syl6bb 252 |
. . . . . . . . . . . . . . . . . . 19
1c NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c
NC Nc Spac
1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
67 | 66 | imbi2d 307 |
. . . . . . . . . . . . . . . . . 18
1c c We NC NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c c We NC NC Nc Spac
1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
68 | | addceq2 4384 |
. . . . . . . . . . . . . . . . . . . . . 22
1c
1c |
69 | 68 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . 21
Nc Spac 1c Nc Spac
1c |
70 | 69 | imbi1d 308 |
. . . . . . . . . . . . . . . . . . . 20
Nc Spac
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
71 | 70 | ralbidv 2634 |
. . . . . . . . . . . . . . . . . . 19
NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c
NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
72 | 71 | imbi2d 307 |
. . . . . . . . . . . . . . . . . 18
c We NC NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c c We NC NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
73 | | nchoicelem14 6302 |
. . . . . . . . . . . . . . . . . . . . . 22
NC Nc Spac
1c
↑c 0c NC |
74 | 73 | ex 423 |
. . . . . . . . . . . . . . . . . . . . 21
NC Nc Spac
1c ↑c
0c
NC |
75 | 74 | adantl 452 |
. . . . . . . . . . . . . . . . . . . 20
c We NC NC Nc Spac
1c
↑c 0c NC |
76 | | nchoicelem9 6297 |
. . . . . . . . . . . . . . . . . . . . . . 23
c We NC NC ↑c
0c
NC Nc Spac Tc
2c
Nc Spac Tc
3c |
77 | | id 19 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nc Spac Tc
2c
Nc Spac Tc
2c |
78 | | 2nnc 6167 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
2c
Nn |
79 | 77, 78 | syl6eqel 2441 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nc Spac Tc
2c
Nc Spac Tc
Nn |
80 | | id 19 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nc Spac Tc
3c
Nc Spac Tc
3c |
81 | | 2p1e3c 6156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
2c
1c
3c |
82 | | peano2 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2c Nn 2c 1c
Nn |
83 | 78, 82 | ax-mp 8 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
2c
1c
Nn |
84 | 81, 83 | eqeltrri 2424 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
3c
Nn |
85 | 80, 84 | syl6eqel 2441 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nc Spac Tc
3c
Nc Spac Tc
Nn |
86 | 79, 85 | jaoi 368 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nc Spac Tc 2c Nc Spac
Tc
3c
Nc Spac Tc
Nn |
87 | | finnc 6243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Spac
Tc
Fin Nc Spac Tc Nn |
88 | 86, 87 | sylibr 203 |
. . . . . . . . . . . . . . . . . . . . . . 23
Nc Spac Tc 2c Nc Spac
Tc
3c
Spac Tc Fin |
89 | 76, 88 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . 22
c We NC NC ↑c
0c
NC Spac Tc Fin |
90 | | 1p1e2c 6155 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
1c
1c
2c |
91 | 90 | eqeq2i 2363 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nc Spac Tc
1c 1c Nc Spac Tc 2c |
92 | | addccom 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
1c
2c
2c 1c |
93 | 92, 81 | eqtri 2373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
1c
2c
3c |
94 | 93 | eqeq2i 2363 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nc Spac Tc
1c 2c Nc Spac Tc 3c |
95 | 91, 94 | orbi12i 507 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nc Spac Tc 1c 1c Nc Spac Tc
1c 2c Nc Spac Tc
2c
Nc Spac Tc
3c |
96 | 76, 95 | sylibr 203 |
. . . . . . . . . . . . . . . . . . . . . . 23
c We NC NC ↑c
0c
NC Nc Spac Tc
1c 1c Nc Spac
Tc
1c 2c |
97 | | nchoicelem3 6291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
NC ↑c
0c
NC Spac |
98 | 97 | nceqd 6110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
NC ↑c
0c
NC Nc Spac
Nc |
99 | | df1c3g 6141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
NC 1c Nc |
100 | 99 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
NC ↑c
0c
NC
1c
Nc |
101 | 98, 100 | eqtr4d 2388 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
NC ↑c
0c
NC Nc Spac
1c |
102 | | tceq 6158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Nc Spac
1c
Tc Nc Spac Tc 1c |
103 | 101, 102 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
NC ↑c
0c
NC Tc Nc Spac Tc 1c |
104 | | tc1c 6165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Tc 1c 1c |
105 | 103, 104 | syl6eq 2401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
NC ↑c
0c
NC Tc Nc Spac 1c |
106 | 105 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
NC ↑c
0c
NC Tc Nc Spac
1c
1c 1c |
107 | 106 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
NC ↑c
0c
NC Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
1c 1c |
108 | 105 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
NC ↑c
0c
NC Tc Nc Spac
2c
1c 2c |
109 | 108 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
NC ↑c
0c
NC Nc Spac Tc
Tc Nc Spac
2c
Nc Spac Tc
1c 2c |
110 | 107, 109 | orbi12d 690 |
. . . . . . . . . . . . . . . . . . . . . . . 24
NC ↑c
0c
NC Nc Spac Tc Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac Tc
1c 1c Nc Spac
Tc
1c 2c |
111 | 110 | 3adant1 973 |
. . . . . . . . . . . . . . . . . . . . . . 23
c We NC NC ↑c
0c
NC Nc Spac Tc Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac Tc
1c 1c Nc Spac
Tc
1c 2c |
112 | 96, 111 | mpbird 223 |
. . . . . . . . . . . . . . . . . . . . . 22
c We NC NC ↑c
0c
NC Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
113 | 89, 112 | jca 518 |
. . . . . . . . . . . . . . . . . . . . 21
c We NC NC ↑c
0c
NC Spac
Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
114 | 113 | 3expia 1153 |
. . . . . . . . . . . . . . . . . . . 20
c We NC NC
↑c 0c NC Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
115 | 75, 114 | syld 40 |
. . . . . . . . . . . . . . . . . . 19
c We NC NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
116 | 115 | ralrimiva 2697 |
. . . . . . . . . . . . . . . . . 18
c We
NC NC Nc Spac
1c Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
117 | | addccom 4406 |
. . . . . . . . . . . . . . . . . . . . . . . 24
1c 1c
1c
1c |
118 | 117 | eqeq2i 2363 |
. . . . . . . . . . . . . . . . . . . . . . 23
Nc Spac
1c
1c Nc Spac
1c
1c |
119 | | nchoicelem13 6301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
NC 1c c Nc
Spac |
120 | 119 | ad2antrl 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c 1c c Nc Spac |
121 | | simp2 956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nn |
122 | | simpr 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
NC Nc Spac
1c
1c Nc Spac
1c
1c |
123 | | simpr 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Nn Nc Spac
1c
1c Nc Spac
1c
1c |
124 | | 0cnsuc 4401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
1c 0c |
125 | | peano2 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
Nn
1c
Nn |
126 | | peano1 4402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
0c
Nn |
127 | | 1cnnc 4408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
1c
Nn |
128 | | addccan1 4560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
1c
Nn 0c Nn 1c Nn 1c 1c
0c
1c
1c
0c |
129 | 126, 127,
128 | mp3an23 1269 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
1c
Nn
1c
1c
0c 1c
1c
0c |
130 | 125, 129 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Nn 1c 1c 0c
1c
1c
0c |
131 | 130 | necon3bid 2551 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Nn 1c 1c 0c
1c
1c 0c |
132 | 124, 131 | mpbiri 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Nn 1c 1c 0c 1c |
133 | | addcid2 4407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
0c
1c
1c |
134 | 133 | neeq2i 2527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
1c
1c
0c 1c
1c
1c
1c |
135 | 132, 134 | sylib 188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Nn 1c 1c 1c |
136 | 135 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Nn Nc Spac
1c
1c
1c
1c
1c |
137 | 123, 136 | eqnetrd 2534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Nn Nc Spac
1c
1c Nc Spac
1c |
138 | 121, 122,
137 | syl2an 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c Nc Spac 1c |
139 | 138 | necomd 2599 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c 1c Nc Spac |
140 | | brltc 6114 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
1c c Nc Spac
1c
c Nc Spac
1c Nc Spac |
141 | 120, 139,
140 | sylanbrc 645 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c 1c c Nc Spac |
142 | | nchoicelem15 6303 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
NC 1c c Nc Spac
↑c 0c NC |
143 | 142 | ex 423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
NC 1c c Nc Spac ↑c 0c NC |
144 | 143 | ad2antrl 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c 1c c Nc Spac ↑c 0c NC |
145 | | df-3an 936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
NC Nc Spac
1c
1c
↑c 0c NC NC Nc Spac
1c
1c ↑c 0c NC |
146 | | ceclnn1 6189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
2c Nn NC
↑c 0c NC 2c ↑c
NC |
147 | 78, 146 | mp3an1 1264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
NC ↑c
0c
NC 2c
↑c NC |
148 | 147 | 3adant2 974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
NC Nc Spac
1c
1c
↑c 0c NC 2c ↑c NC |
149 | 148 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c
↑c 0c NC 2c ↑c
NC |
150 | | fveq2 5328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
2c ↑c Spac Spac
2c
↑c |
151 | 150 | nceqd 6110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
2c ↑c Nc Spac
Nc Spac 2c ↑c |
152 | 151 | eqeq1d 2361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
2c ↑c Nc Spac
1c
Nc Spac 2c ↑c 1c |
153 | | tceq 6158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
2c ↑c Tc Tc 2c
↑c |
154 | 153 | fveq2d 5332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
2c ↑c Spac Tc Spac Tc 2c
↑c |
155 | 154 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
2c ↑c Spac Tc Fin Spac
Tc 2c ↑c Fin |
156 | 154 | nceqd 6110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
2c ↑c Nc Spac Tc
Nc Spac Tc 2c ↑c |
157 | | tceq 6158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
Nc Spac
Nc Spac 2c ↑c Tc Nc Spac Tc Nc Spac 2c ↑c |
158 | 151, 157 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
2c ↑c Tc Nc Spac
Tc Nc Spac 2c ↑c |
159 | 158 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
2c ↑c Tc Nc Spac
1c
Tc Nc Spac 2c ↑c
1c |
160 | 156, 159 | eqeq12d 2367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
2c ↑c Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
1c |
161 | 158 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
2c ↑c Tc Nc Spac
2c
Tc Nc Spac 2c ↑c
2c |
162 | 156, 161 | eqeq12d 2367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
2c ↑c Nc Spac Tc
Tc Nc Spac
2c
Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
2c |
163 | 160, 162 | orbi12d 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
2c ↑c Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
1c
Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
2c |
164 | 155, 163 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
2c ↑c Spac
Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Spac
Tc 2c ↑c Fin Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
1c
Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
2c |
165 | 152, 164 | imbi12d 311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
2c ↑c Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac 2c
↑c 1c Spac Tc 2c ↑c Fin Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
1c
Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
2c |
166 | 165 | rspccva 2954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c 2c ↑c
NC Nc Spac 2c ↑c 1c Spac Tc 2c
↑c Fin Nc Spac Tc 2c
↑c Tc Nc Spac 2c ↑c
1c
Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
2c |
167 | | tce2 6236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
NC ↑c
0c
NC Tc 2c ↑c 2c ↑c Tc |
168 | 167 | fveq2d 5332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
NC ↑c
0c
NC Spac Tc 2c
↑c Spac 2c ↑c Tc |
169 | 168 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
NC ↑c
0c
NC Spac
Tc 2c ↑c Fin Spac 2c ↑c Tc Fin |
170 | 168 | nceqd 6110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
NC ↑c
0c
NC Nc Spac Tc 2c ↑c Nc Spac 2c ↑c Tc |
171 | 170 | eqeq1d 2361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
NC ↑c
0c
NC Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
1c
Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
1c |
172 | 170 | eqeq1d 2361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
NC ↑c
0c
NC Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
2c
Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
2c |
173 | 171, 172 | orbi12d 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
NC ↑c
0c
NC Nc Spac Tc 2c
↑c Tc Nc Spac 2c ↑c
1c
Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
2c Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
1c
Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
2c |
174 | 169, 173 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
NC ↑c
0c
NC Spac Tc 2c ↑c Fin Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
1c
Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
2c Spac
2c
↑c Tc Fin Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
1c
Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
2c |
175 | 174 | imbi2d 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
NC ↑c
0c
NC Nc Spac 2c ↑c
1c
Spac Tc 2c ↑c Fin Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
1c
Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
2c Nc Spac 2c
↑c 1c Spac 2c
↑c Tc Fin Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
1c
Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
2c |
176 | 175 | 3adant2 974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
NC Nc Spac
1c
1c
↑c 0c NC
Nc Spac 2c ↑c 1c Spac Tc 2c
↑c Fin Nc Spac Tc 2c
↑c Tc Nc Spac 2c ↑c
1c
Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
2c Nc Spac 2c
↑c 1c Spac 2c
↑c Tc Fin Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
1c
Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
2c |
177 | 176 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac 2c ↑c 1c Spac Tc 2c
↑c Fin Nc Spac Tc 2c
↑c Tc Nc Spac 2c ↑c
1c
Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
2c Nc Spac 2c
↑c 1c Spac 2c
↑c Tc Fin Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
1c
Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
2c |
178 | | nchoicelem7 6295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
NC ↑c
0c
NC Nc Spac
Nc Spac 2c ↑c
1c |
179 | 178 | 3adant2 974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
NC Nc Spac
1c
1c
↑c 0c NC Nc Spac Nc Spac 2c ↑c
1c |
180 | | simp2 956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
NC Nc Spac
1c
1c
↑c 0c NC Nc Spac
1c
1c |
181 | 179, 180 | eqtr3d 2387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
NC Nc Spac
1c
1c
↑c 0c NC Nc Spac
2c
↑c 1c 1c 1c |
182 | 181 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac 2c
↑c 1c 1c 1c |
183 | | nnnc 6146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
1c
Nn 1c NC |
184 | | fvex 5339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
Spac 2c ↑c
|
185 | 184 | ncelncsi 6121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
Nc Spac 2c ↑c NC |
186 | | peano4nc 6150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
Nc Spac 2c ↑c
NC 1c NC Nc Spac 2c ↑c
1c
1c
1c
Nc Spac 2c ↑c 1c |
187 | 185, 186 | mpan 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
1c
NC Nc Spac 2c ↑c
1c
1c
1c
Nc Spac 2c ↑c 1c |
188 | 125, 183,
187 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
Nn Nc Spac 2c ↑c
1c
1c
1c
Nc Spac 2c ↑c 1c |
189 | 188 | ad2antlr 707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac 2c ↑c
1c
1c
1c
Nc Spac 2c ↑c 1c |
190 | 182, 189 | mpbid 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac 2c ↑c
1c |
191 | | addccom 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
1c
1c
|
192 | 190, 191 | syl6eq 2401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac 2c ↑c
1c |
193 | | peano2 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
Nc Spac 2c ↑c Tc Nn Nc Spac 2c ↑c Tc
1c
Nn |
194 | | tccl 6160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
NC Tc NC |
195 | | te0c 6237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
NC Tc ↑c
0c
NC |
196 | | nchoicelem7 6295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
Tc NC Tc ↑c 0c NC Nc Spac Tc Nc Spac 2c ↑c Tc
1c |
197 | 194, 195,
196 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
NC Nc Spac Tc Nc Spac 2c ↑c Tc
1c |
198 | 197 | 3ad2ant1 976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
NC Nc Spac
1c
1c
↑c 0c NC Nc Spac Tc Nc Spac 2c ↑c Tc
1c |
199 | 198 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac Tc Nc Spac 2c ↑c Tc
1c |
200 | 199 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac Tc
Nn Nc Spac 2c
↑c Tc
1c
Nn |
201 | 193, 200 | syl5ibr 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac 2c
↑c Tc Nn Nc Spac Tc
Nn |
202 | | finnc 6243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
Spac
2c
↑c Tc Fin Nc Spac 2c ↑c Tc Nn |
203 | | finnc 6243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
Spac
Tc
Fin Nc Spac Tc Nn |
204 | 201, 202,
203 | 3imtr4g 261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Spac 2c ↑c Tc Fin Spac Tc Fin |
205 | | addceq1 4383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
1c
Nc Spac 2c ↑c Tc
1c
Tc Nc Spac 2c ↑c
1c
1c |
206 | | tceq 6158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
Nc Spac
Nc Spac 2c ↑c
1c
Tc Nc Spac Tc Nc Spac
2c
↑c 1c |
207 | 178, 206 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
NC ↑c
0c
NC Tc Nc Spac Tc Nc Spac
2c
↑c 1c |
208 | 207 | 3adant2 974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
NC Nc Spac
1c
1c
↑c 0c NC Tc
Nc Spac
Tc Nc Spac
2c
↑c 1c |
209 | 208 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Tc Nc Spac
Tc Nc Spac
2c
↑c 1c |
210 | | tcdi 6164 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
Nc Spac 2c ↑c
NC 1c NC Tc Nc Spac 2c ↑c
1c
Tc Nc Spac 2c ↑c
Tc 1c |
211 | 185, 5, 210 | mp2an 653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
Tc Nc Spac
2c
↑c 1c
Tc Nc Spac 2c ↑c
Tc 1c |
212 | 104 | addceq2i 4387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
Tc Nc Spac 2c ↑c
Tc 1c
Tc Nc Spac 2c ↑c
1c |
213 | 211, 212 | eqtri 2373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
Tc Nc Spac
2c
↑c 1c
Tc Nc Spac 2c ↑c
1c |
214 | 209, 213 | syl6eq 2401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Tc Nc Spac
Tc Nc Spac 2c ↑c
1c |
215 | 214 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Tc Nc Spac
1c
Tc Nc Spac 2c ↑c
1c
1c |
216 | 199, 215 | eqeq12d 2367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac Tc
Tc Nc Spac
1c
Nc Spac 2c ↑c Tc
1c
Tc Nc Spac 2c ↑c
1c
1c |
217 | 205, 216 | syl5ibr 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac 2c
↑c Tc Tc Nc Spac 2c ↑c
1c
Nc Spac Tc
Tc Nc Spac
1c |
218 | | addceq1 4383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
2c
Nc Spac 2c ↑c Tc
1c
Tc Nc Spac 2c ↑c
2c
1c |
219 | 214 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Tc Nc Spac
2c
Tc Nc Spac 2c ↑c
1c
2c |
220 | | addc32 4416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
Tc Nc Spac 2c ↑c
1c
2c
Tc Nc Spac 2c ↑c
2c
1c |
221 | 219, 220 | syl6eq 2401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Tc Nc Spac
2c
Tc Nc Spac 2c ↑c
2c
1c |
222 | 199, 221 | eqeq12d 2367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac Tc
Tc Nc Spac
2c
Nc Spac 2c ↑c Tc
1c
Tc Nc Spac 2c ↑c
2c
1c |
223 | 218, 222 | syl5ibr 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac 2c
↑c Tc Tc Nc Spac 2c ↑c
2c
Nc Spac Tc
Tc Nc Spac
2c |
224 | 217, 223 | orim12d 811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
1c
Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
2c Nc Spac Tc Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
225 | 204, 224 | anim12d 546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Spac 2c ↑c Tc Fin Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
1c
Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
2c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
226 | 192, 225 | embantd 50 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac 2c ↑c 1c Spac 2c ↑c Tc Fin Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
1c
Nc Spac 2c ↑c Tc Tc Nc Spac 2c ↑c
2c Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
227 | 177, 226 | sylbid 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC Nc Spac 2c ↑c 1c Spac Tc 2c
↑c Fin Nc Spac Tc 2c
↑c Tc Nc Spac 2c ↑c
1c
Nc Spac Tc 2c ↑c Tc Nc Spac 2c ↑c
2c Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
228 | 166, 227 | syl5 28 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC NC Nc Spac 1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c 2c ↑c
NC Spac
Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
229 | 228 | exp4b 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
c We NC Nn NC Nc Spac
1c
1c
↑c 0c NC NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c 2c ↑c
NC Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
230 | 229 | com23 72 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
c We NC Nn
NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c
↑c 0c NC 2c ↑c
NC Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
231 | 230 | 3impia 1148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c
↑c 0c NC 2c ↑c
NC Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
232 | 231 | imp 418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c
↑c 0c NC 2c ↑c
NC Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
233 | 149, 232 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c
↑c 0c NC Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
234 | 145, 233 | sylan2br 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c ↑c 0c NC Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
235 | 234 | expr 598 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c
↑c 0c NC Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
236 | 144, 235 | syld 40 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c 1c c Nc Spac Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
237 | 141, 236 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
238 | 237 | expr 598 |
. . . . . . . . . . . . . . . . . . . . . . 23
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c 1c Spac
Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
239 | 118, 238 | syl5bi 208 |
. . . . . . . . . . . . . . . . . . . . . 22
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
240 | 239 | ralrimiva 2697 |
. . . . . . . . . . . . . . . . . . . . 21
c We NC Nn NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac 1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
241 | 240 | 3exp 1150 |
. . . . . . . . . . . . . . . . . . . 20
c We
NC Nn NC Nc Spac 1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
242 | 241 | com12 27 |
. . . . . . . . . . . . . . . . . . 19
Nn c We NC NC Nc Spac 1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
243 | 242 | a2d 23 |
. . . . . . . . . . . . . . . . . 18
Nn c We NC NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c c We
NC NC Nc Spac
1c
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
244 | 32, 39, 44, 67, 72, 116, 243 | finds 4411 |
. . . . . . . . . . . . . . . . 17
Nn c We NC NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
245 | | fveq2 5328 |
. . . . . . . . . . . . . . . . . . . . 21
Spac Spac
|
246 | 245 | nceqd 6110 |
. . . . . . . . . . . . . . . . . . . 20
Nc Spac
Nc Spac |
247 | 246 | eqeq1d 2361 |
. . . . . . . . . . . . . . . . . . 19
Nc Spac 1c Nc Spac
1c |
248 | | tceq 6158 |
. . . . . . . . . . . . . . . . . . . . . 22
Tc
Tc |
249 | 248 | fveq2d 5332 |
. . . . . . . . . . . . . . . . . . . . 21
Spac Tc Spac Tc |
250 | 249 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . 20
Spac Tc
Fin Spac Tc
Fin |
251 | 249 | nceqd 6110 |
. . . . . . . . . . . . . . . . . . . . . 22
Nc Spac Tc
Nc Spac Tc |
252 | | tceq 6158 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nc Spac
Nc Spac
Tc Nc Spac Tc Nc Spac |
253 | 246, 252 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
Tc Nc Spac Tc Nc Spac |
254 | 253 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . . . . 22
Tc Nc Spac
1c
Tc Nc Spac
1c |
255 | 251, 254 | eqeq12d 2367 |
. . . . . . . . . . . . . . . . . . . . 21
Nc Spac Tc Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
1c |
256 | 253 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . . . . 22
Tc Nc Spac
2c
Tc Nc Spac
2c |
257 | 251, 256 | eqeq12d 2367 |
. . . . . . . . . . . . . . . . . . . . 21
Nc Spac Tc Tc Nc Spac
2c
Nc Spac Tc
Tc Nc Spac
2c |
258 | 255, 257 | orbi12d 690 |
. . . . . . . . . . . . . . . . . . . 20
Nc Spac
Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
259 | 250, 258 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . 19
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Spac
Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
260 | 247, 259 | imbi12d 311 |
. . . . . . . . . . . . . . . . . 18
Nc Spac
1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
261 | 260 | rspccv 2952 |
. . . . . . . . . . . . . . . . 17
NC Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c NC Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
262 | 244, 261 | syl6com 31 |
. . . . . . . . . . . . . . . 16
c We
NC Nn NC Nc Spac 1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
263 | 262 | com23 72 |
. . . . . . . . . . . . . . 15
c We
NC NC Nn Nc Spac 1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
264 | 263 | imp 418 |
. . . . . . . . . . . . . 14
c We NC NC Nn Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
265 | 264 | adantr 451 |
. . . . . . . . . . . . 13
c We NC NC Nn
Nn Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
266 | 265 | adantr 451 |
. . . . . . . . . . . 12
c We NC
NC Nn
NC Nn Nc Spac
1c
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
267 | 27, 31, 266 | 3syld 51 |
. . . . . . . . . . 11
c We NC
NC Nn
NC 1c Nc Spac 1c Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
268 | 267 | imp3a 420 |
. . . . . . . . . 10
c We NC
NC Nn
NC 1c Nc Spac
1c
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
269 | 15, 268 | syl5 28 |
. . . . . . . . 9
c We NC
NC Nn
NC Nc Spac 1c Nc Spac
Spac
Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
270 | 269 | exp3a 425 |
. . . . . . . 8
c We NC
NC Nn
NC Nc Spac
1c
Nc Spac
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
271 | 270 | rexlimdva 2738 |
. . . . . . 7
c We NC NC Nn NC Nc Spac 1c
Nc Spac
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
272 | 9, 271 | syl5bi 208 |
. . . . . 6
c We NC NC Nn 1c c Nc Spac
Nc Spac
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
273 | 4, 272 | mpd 14 |
. . . . 5
c We NC NC Nn
Nc Spac
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
274 | 273 | rexlimdva 2738 |
. . . 4
c We NC NC
Nn Nc Spac
Spac Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
275 | 2, 274 | syl5bi 208 |
. . 3
c We NC NC Nc Spac
Nn Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
276 | 1, 275 | syl5bi 208 |
. 2
c We NC NC Spac
Fin
Spac Tc Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
277 | 276 | 3impia 1148 |
1
c We NC NC Spac Fin Spac
Tc
Fin Nc Spac Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |