Step | Hyp | Ref
| Expression |
1 | | elncs 6120 |
. . . . 5
 NC  Nc   |
2 | | elncs 6120 |
. . . . 5
 NC  Nc   |
3 | 1, 2 | anbi12i 678 |
. . . 4
  NC NC  
Nc 
Nc    |
4 | | eeanv 1913 |
. . . 4
      Nc Nc   
Nc 
Nc    |
5 | 3, 4 | bitr4i 243 |
. . 3
  NC NC      Nc Nc    |
6 | | vex 2863 |
. . . . . . . 8
 |
7 | | vex 2863 |
. . . . . . . 8
 |
8 | 6, 7 | mucnc 6132 |
. . . . . . 7
Nc ·c Nc  Nc 
  |
9 | | df0c2 6138 |
. . . . . . 7
0c
Nc  |
10 | 8, 9 | eqeq12i 2366 |
. . . . . 6
 Nc
·c Nc 
0c Nc   Nc   |
11 | 6, 7 | xpex 5116 |
. . . . . . . . 9
   |
12 | 11 | eqnc 6128 |
. . . . . . . 8
Nc  
Nc     |
13 | | en0 6043 |
. . . . . . . 8
    
  |
14 | 12, 13 | bitri 240 |
. . . . . . 7
Nc  
Nc  
  |
15 | | xpeq0 5047 |
. . . . . . . 8
  
    |
16 | | nceq 6109 |
. . . . . . . . 9

Nc Nc   |
17 | | nceq 6109 |
. . . . . . . . 9

Nc Nc   |
18 | 16, 17 | orim12i 502 |
. . . . . . . 8
   Nc Nc Nc Nc    |
19 | 15, 18 | sylbi 187 |
. . . . . . 7
  
Nc Nc Nc Nc    |
20 | 14, 19 | sylbi 187 |
. . . . . 6
Nc  
Nc Nc Nc Nc
Nc    |
21 | 10, 20 | sylbi 187 |
. . . . 5
 Nc
·c Nc 
0c Nc Nc Nc
Nc    |
22 | | oveq12 5533 |
. . . . . . 7
  Nc Nc  
·c  Nc
·c Nc    |
23 | 22 | eqeq1d 2361 |
. . . . . 6
  Nc Nc   
·c  0c Nc ·c Nc  0c  |
24 | | eqeq1 2359 |
. . . . . . . . 9
 Nc  0c Nc
0c  |
25 | 24 | adantr 451 |
. . . . . . . 8
  Nc Nc   0c Nc
0c  |
26 | 9 | eqeq2i 2363 |
. . . . . . . 8
Nc
0c Nc Nc   |
27 | 25, 26 | syl6bb 252 |
. . . . . . 7
  Nc Nc   0c Nc Nc    |
28 | | eqeq1 2359 |
. . . . . . . . 9
 Nc  0c Nc
0c  |
29 | 9 | eqeq2i 2363 |
. . . . . . . . 9
Nc
0c Nc Nc   |
30 | 28, 29 | syl6bb 252 |
. . . . . . . 8
 Nc  0c Nc Nc    |
31 | 30 | adantl 452 |
. . . . . . 7
  Nc Nc   0c Nc Nc    |
32 | 27, 31 | orbi12d 690 |
. . . . . 6
  Nc Nc    0c
0c
Nc Nc Nc
Nc     |
33 | 23, 32 | imbi12d 311 |
. . . . 5
  Nc Nc     ·c 
0c  0c
0c  Nc
·c Nc 
0c Nc Nc Nc
Nc      |
34 | 21, 33 | mpbiri 224 |
. . . 4
  Nc Nc   
·c  0c 
0c 0c   |
35 | 34 | exlimivv 1635 |
. . 3
      Nc Nc   
·c  0c 
0c 0c   |
36 | 5, 35 | sylbi 187 |
. 2
  NC NC   ·c 
0c

0c 0c   |
37 | | 0cnc 6139 |
. . . . . . 7
0c
NC |
38 | | muccom 6135 |
. . . . . . 7
 0c NC NC 0c ·c 
 ·c
0c  |
39 | 37, 38 | mpan 651 |
. . . . . 6
 NC 0c ·c 
 ·c
0c  |
40 | | muc0 6143 |
. . . . . 6
 NC 
·c 0c 0c |
41 | 39, 40 | eqtrd 2385 |
. . . . 5
 NC 0c ·c 
0c |
42 | | oveq1 5531 |
. . . . . 6
 0c 
·c  0c ·c
   |
43 | 42 | eqeq1d 2361 |
. . . . 5
 0c  
·c  0c 0c
·c  0c  |
44 | 41, 43 | syl5ibrcom 213 |
. . . 4
 NC  0c  ·c 
0c  |
45 | 44 | adantl 452 |
. . 3
  NC NC  0c 
·c  0c  |
46 | | muc0 6143 |
. . . . 5
 NC 
·c 0c 0c |
47 | | oveq2 5532 |
. . . . . 6
 0c 
·c   ·c 0c  |
48 | 47 | eqeq1d 2361 |
. . . . 5
 0c  
·c  0c  ·c
0c
0c  |
49 | 46, 48 | syl5ibrcom 213 |
. . . 4
 NC  0c  ·c 
0c  |
50 | 49 | adantr 451 |
. . 3
  NC NC  0c 
·c  0c  |
51 | 45, 50 | jaod 369 |
. 2
  NC NC  
0c 0c 
·c  0c  |
52 | 36, 51 | impbid 183 |
1
  NC NC   ·c 
0c
 0c
0c   |