Step | Hyp | Ref
| Expression |
1 | | nnltp1c 6262 |
. . . . . . . . . . . 12
Nn c
1c |
2 | | nnnc 6146 |
. . . . . . . . . . . . 13
Nn NC |
3 | | peano2 4403 |
. . . . . . . . . . . . . 14
Nn
1c
Nn |
4 | | nnnc 6146 |
. . . . . . . . . . . . . 14
1c
Nn 1c NC |
5 | 3, 4 | syl 15 |
. . . . . . . . . . . . 13
Nn
1c
NC |
6 | | ltlenlec 6207 |
. . . . . . . . . . . . 13
NC 1c NC c 1c c 1c 1c c |
7 | 2, 5, 6 | syl2anc 642 |
. . . . . . . . . . . 12
Nn c 1c c 1c 1c c |
8 | 1, 7 | mpbid 201 |
. . . . . . . . . . 11
Nn c 1c 1c c |
9 | 8 | simprd 449 |
. . . . . . . . . 10
Nn 1c c |
10 | 9 | adantr 451 |
. . . . . . . . 9
Nn Nn 1c c |
11 | 10 | intnand 882 |
. . . . . . . 8
Nn Nn 1c c
1c
1c c |
12 | 11 | a1d 22 |
. . . . . . 7
Nn Nn
1c
Nn 1c c 1c 1c c |
13 | | breq2 4643 |
. . . . . . . . . . 11
1c 1c c 1c c
1c |
14 | | breq1 4642 |
. . . . . . . . . . 11
1c c 1c c |
15 | 13, 14 | anbi12d 691 |
. . . . . . . . . 10
1c 1c c c 1c c
1c
1c c |
16 | 15 | elrab 2994 |
. . . . . . . . 9
1c
Nn 1c c c 1c
Nn 1c c
1c
1c c |
17 | 16 | notbii 287 |
. . . . . . . 8
1c
Nn 1c c c
1c
Nn 1c c
1c
1c c |
18 | | imnan 411 |
. . . . . . . 8
1c
Nn 1c c 1c 1c c
1c
Nn 1c c
1c
1c c |
19 | 17, 18 | bitr4i 243 |
. . . . . . 7
1c
Nn 1c c c 1c
Nn 1c c
1c
1c c |
20 | 12, 19 | sylibr 203 |
. . . . . 6
Nn Nn 1c Nn 1c c c |
21 | 3 | adantr 451 |
. . . . . . 7
Nn Nn 1c
Nn |
22 | | elcomplg 3218 |
. . . . . . 7
1c
Nn 1c
∼ Nn 1c c
c 1c
Nn 1c c c |
23 | 21, 22 | syl 15 |
. . . . . 6
Nn Nn
1c
∼ Nn 1c c c 1c
Nn 1c c c |
24 | 20, 23 | mpbird 223 |
. . . . 5
Nn Nn 1c
∼ Nn 1c c
c |
25 | | nnnc 6146 |
. . . . . . . . . . . . . 14
Nn NC |
26 | | ncslesuc 6267 |
. . . . . . . . . . . . . 14
NC NC c
1c
c
1c |
27 | 25, 2, 26 | syl2an 463 |
. . . . . . . . . . . . 13
Nn Nn c
1c
c
1c |
28 | 27 | expcom 424 |
. . . . . . . . . . . 12
Nn Nn c
1c
c
1c |
29 | 28 | adantrd 454 |
. . . . . . . . . . 11
Nn Nn 1c
c c 1c c
1c |
30 | 29 | adantr 451 |
. . . . . . . . . 10
Nn Nn Nn 1c c
c
1c
c
1c |
31 | 30 | pm5.32d 620 |
. . . . . . . . 9
Nn Nn Nn 1c c
c
1c Nn 1c c
c
1c |
32 | | anass 630 |
. . . . . . . . 9
Nn 1c c
c
1c Nn 1c c c
1c |
33 | | andi 837 |
. . . . . . . . . 10
Nn 1c c
c
1c Nn 1c c
c
Nn 1c c
1c |
34 | | anass 630 |
. . . . . . . . . . 11
Nn 1c c
c
Nn 1c c c |
35 | 34 | orbi1i 506 |
. . . . . . . . . 10
Nn 1c
c
c Nn 1c c
1c Nn 1c c c
Nn 1c c
1c |
36 | 33, 35 | bitri 240 |
. . . . . . . . 9
Nn 1c c
c
1c Nn 1c c c
Nn 1c c
1c |
37 | 31, 32, 36 | 3bitr3g 278 |
. . . . . . . 8
Nn Nn Nn 1c c c
1c Nn 1c c c
Nn 1c c
1c |
38 | | 1cnc 6139 |
. . . . . . . . . . . . . . . 16
1c
NC |
39 | | addlecncs 6209 |
. . . . . . . . . . . . . . . 16
1c NC NC 1c c 1c |
40 | 38, 2, 39 | sylancr 644 |
. . . . . . . . . . . . . . 15
Nn 1c c 1c |
41 | | addccom 4406 |
. . . . . . . . . . . . . . 15
1c
1c
|
42 | 40, 41 | syl6breqr 4679 |
. . . . . . . . . . . . . 14
Nn 1c c
1c |
43 | 3, 42 | jca 518 |
. . . . . . . . . . . . 13
Nn 1c Nn 1c c
1c |
44 | | eleq1 2413 |
. . . . . . . . . . . . . 14
1c Nn
1c
Nn |
45 | | breq2 4643 |
. . . . . . . . . . . . . 14
1c 1c c 1c c
1c |
46 | 44, 45 | anbi12d 691 |
. . . . . . . . . . . . 13
1c Nn 1c
c 1c Nn 1c c
1c |
47 | 43, 46 | syl5ibrcom 213 |
. . . . . . . . . . . 12
Nn
1c
Nn 1c c |
48 | 47 | adantr 451 |
. . . . . . . . . . 11
Nn Nn 1c Nn 1c c |
49 | 48 | pm4.71rd 616 |
. . . . . . . . . 10
Nn Nn 1c Nn 1c c
1c |
50 | 49 | bicomd 192 |
. . . . . . . . 9
Nn Nn Nn 1c c
1c
1c |
51 | 50 | orbi2d 682 |
. . . . . . . 8
Nn Nn Nn 1c c c
Nn 1c c
1c Nn 1c c c
1c |
52 | 37, 51 | bitrd 244 |
. . . . . . 7
Nn Nn Nn 1c c c
1c Nn 1c c c
1c |
53 | | breq2 4643 |
. . . . . . . . 9
1c c 1c c |
54 | | breq1 4642 |
. . . . . . . . 9
c
1c
c
1c |
55 | 53, 54 | anbi12d 691 |
. . . . . . . 8
1c c c 1c
1c
c c
1c |
56 | 55 | elrab 2994 |
. . . . . . 7
Nn 1c c
c 1c Nn 1c c c
1c |
57 | | elun 3220 |
. . . . . . . 8
Nn 1c c c 1c Nn 1c c
c
1c |
58 | | breq1 4642 |
. . . . . . . . . . 11
c c |
59 | 53, 58 | anbi12d 691 |
. . . . . . . . . 10
1c c c 1c c c |
60 | 59 | elrab 2994 |
. . . . . . . . 9
Nn 1c c
c Nn 1c c
c |
61 | | elsn 3748 |
. . . . . . . . 9
1c
1c |
62 | 60, 61 | orbi12i 507 |
. . . . . . . 8
Nn 1c c c
1c Nn 1c c c
1c |
63 | 57, 62 | bitri 240 |
. . . . . . 7
Nn 1c c c 1c Nn 1c c c
1c |
64 | 52, 56, 63 | 3bitr4g 279 |
. . . . . 6
Nn Nn Nn 1c c
c 1c Nn 1c c
c 1c |
65 | 64 | eqrdv 2351 |
. . . . 5
Nn Nn Nn 1c c c 1c Nn 1c c c
1c |
66 | | sneq 3744 |
. . . . . . . 8
1c
1c |
67 | 66 | uneq2d 3418 |
. . . . . . 7
1c Nn 1c c
c
Nn 1c c c
1c |
68 | 67 | eqeq2d 2364 |
. . . . . 6
1c Nn 1c c
c 1c Nn 1c c c Nn 1c c c 1c Nn 1c c c
1c |
69 | 68 | rspcev 2955 |
. . . . 5
1c
∼ Nn 1c c c Nn 1c c c 1c Nn 1c c c
1c ∼ Nn 1c c c Nn 1c c
c 1c Nn 1c c c |
70 | 24, 65, 69 | syl2anc 642 |
. . . 4
Nn Nn ∼ Nn 1c c c Nn 1c c c 1c Nn 1c c c |
71 | | compleq 3243 |
. . . . . 6
Nn 1c c
c ∼
∼ Nn 1c c c |
72 | | uneq1 3411 |
. . . . . . 7
Nn 1c c
c
Nn 1c c c |
73 | 72 | eqeq2d 2364 |
. . . . . 6
Nn 1c c
c
Nn 1c c c
1c
Nn 1c c c 1c Nn 1c c c |
74 | 71, 73 | rexeqbidv 2820 |
. . . . 5
Nn 1c c
c
∼ Nn 1c c c 1c
∼ Nn 1c c c Nn 1c c c 1c Nn 1c c c |
75 | 74 | rspcev 2955 |
. . . 4
Nn 1c c c ∼ Nn 1c c c Nn 1c c
c 1c Nn 1c c c
∼
Nn 1c c c
1c
|
76 | 70, 75 | sylan2 460 |
. . 3
Nn 1c c c Nn Nn
∼ Nn 1c c
c 1c |
77 | | elsuc 4413 |
. . 3
Nn 1c c c
1c
1c
∼ Nn 1c c c
1c
|
78 | 76, 77 | sylibr 203 |
. 2
Nn 1c c c Nn Nn
Nn 1c c c
1c
1c |
79 | 78 | expcom 424 |
1
Nn Nn
Nn 1c c c Nn 1c c c
1c
1c |