Step | Hyp | Ref
| Expression |
1 | | eleq1 2517 |
. . . . . 6
 
   |
2 | 1 | anbi2d 710 |
. . . . 5
  

     |
3 | | csbeq1 3366 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
4 | 3 | fveq2d 5869 |
. . . . . 6
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
5 | | fveq2 5865 |
. . . . . . 7
           |
6 | 5 | csbeq1d 3370 |
. . . . . 6
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
7 | 4, 6 | eqeq12d 2466 |
. . . . 5
       ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)
     ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)    |
8 | 2, 7 | imbi12d 322 |
. . . 4
   
      ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif) 
        ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)     |
9 | | nfv 1761 |
. . . . . . . . . 10
  
  |
10 | | nfcsb1v 3379 |
. . . . . . . . . . 11
  
 ![]_ ]_](_urbrack.gif)  |
11 | 10 | nfel1 2606 |
. . . . . . . . . 10
  
 ![]_ ]_](_urbrack.gif)
 |
12 | 9, 11 | nfim 2003 |
. . . . . . . . 9
   
   ![]_ ]_](_urbrack.gif)
  |
13 | | eleq1 2517 |
. . . . . . . . . . 11
 
   |
14 | 13 | anbi2d 710 |
. . . . . . . . . 10
  

     |
15 | | csbeq1a 3372 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)   |
16 | 15 | eleq1d 2513 |
. . . . . . . . . 10
 
  ![]_ ]_](_urbrack.gif)    |
17 | 14, 16 | imbi12d 322 |
. . . . . . . . 9
   
   
   ![]_ ]_](_urbrack.gif)
    |
18 | | oddcomabszz.1 |
. . . . . . . . 9
 

  |
19 | 12, 17, 18 | chvar 2106 |
. . . . . . . 8
 

  ![]_ ]_](_urbrack.gif)   |
20 | 19 | adantr 467 |
. . . . . . 7
       ![]_ ]_](_urbrack.gif)   |
21 | | nfv 1761 |
. . . . . . . . . 10
  
  |
22 | | nfcv 2592 |
. . . . . . . . . . 11
   |
23 | | nfcv 2592 |
. . . . . . . . . . 11
  |
24 | 22, 23, 10 | nfbr 4447 |
. . . . . . . . . 10
 
  ![]_ ]_](_urbrack.gif)  |
25 | 21, 24 | nfim 2003 |
. . . . . . . . 9
   
   ![]_ ]_](_urbrack.gif)   |
26 | | breq2 4406 |
. . . . . . . . . . 11
 
   |
27 | 13, 26 | 3anbi23d 1342 |
. . . . . . . . . 10
  

     |
28 | 15 | breq2d 4414 |
. . . . . . . . . 10
 
  ![]_ ]_](_urbrack.gif)    |
29 | 27, 28 | imbi12d 322 |
. . . . . . . . 9
   
 
 

  ![]_ ]_](_urbrack.gif)     |
30 | | oddcomabszz.2 |
. . . . . . . . 9
 

  |
31 | 25, 29, 30 | chvar 2106 |
. . . . . . . 8
 

  ![]_ ]_](_urbrack.gif)   |
32 | 31 | 3expa 1208 |
. . . . . . 7
       ![]_ ]_](_urbrack.gif)   |
33 | 20, 32 | absidd 13484 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
34 | | zre 10941 |
. . . . . . . . 9
   |
35 | 34 | ad2antlr 733 |
. . . . . . . 8
       |
36 | | absid 13359 |
. . . . . . . 8
         |
37 | 35, 36 | sylancom 673 |
. . . . . . 7
           |
38 | 37 | csbeq1d 3370 |
. . . . . 6
           ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
39 | 33, 38 | eqtr4d 2488 |
. . . . 5
          ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)   |
40 | | nfv 1761 |
. . . . . . . 8
   
    ![]_ ]_](_urbrack.gif)
   ![]_ ]_](_urbrack.gif)   |
41 | | eleq1 2517 |
. . . . . . . . . 10
 
   |
42 | 41 | anbi2d 710 |
. . . . . . . . 9
  

     |
43 | | negex 9873 |
. . . . . . . . . . . 12
  |
44 | | oddcomabszz.5 |
. . . . . . . . . . . 12
    |
45 | 43, 44 | csbie 3389 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)  |
46 | | negeq 9867 |
. . . . . . . . . . . 12
     |
47 | 46 | csbeq1d 3370 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
48 | 45, 47 | syl5eqr 2499 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)   |
49 | | vex 3048 |
. . . . . . . . . . . . 13
 |
50 | | oddcomabszz.4 |
. . . . . . . . . . . . 13
   |
51 | 49, 50 | csbie 3389 |
. . . . . . . . . . . 12
  ![]_ ]_](_urbrack.gif)  |
52 | | csbeq1 3366 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
53 | 51, 52 | syl5eqr 2499 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)   |
54 | 53 | negeqd 9869 |
. . . . . . . . . 10
     ![]_ ]_](_urbrack.gif)   |
55 | 48, 54 | eqeq12d 2466 |
. . . . . . . . 9
 

   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
56 | 42, 55 | imbi12d 322 |
. . . . . . . 8
   
         ![]_ ]_](_urbrack.gif)
   ![]_ ]_](_urbrack.gif)     |
57 | | oddcomabszz.3 |
. . . . . . . 8
 

   |
58 | 40, 56, 57 | chvar 2106 |
. . . . . . 7
 

   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
59 | 58 | adantr 467 |
. . . . . 6
        ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
60 | 34 | ad2antlr 733 |
. . . . . . . 8
       |
61 | | absnid 13361 |
. . . . . . . 8
          |
62 | 60, 61 | sylancom 673 |
. . . . . . 7
            |
63 | 62 | csbeq1d 3370 |
. . . . . 6
           ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
64 | 19 | adantr 467 |
. . . . . . 7
       ![]_ ]_](_urbrack.gif)   |
65 | | znegcl 10972 |
. . . . . . . . . . 11
    |
66 | | nfv 1761 |
. . . . . . . . . . . . . 14
  
    |
67 | | nfcsb1v 3379 |
. . . . . . . . . . . . . . 15
     ![]_ ]_](_urbrack.gif)  |
68 | 22, 23, 67 | nfbr 4447 |
. . . . . . . . . . . . . 14
 
   ![]_ ]_](_urbrack.gif)  |
69 | 66, 68 | nfim 2003 |
. . . . . . . . . . . . 13
      
   ![]_ ]_](_urbrack.gif)   |
70 | | negex 9873 |
. . . . . . . . . . . . 13
  |
71 | | eleq1 2517 |
. . . . . . . . . . . . . . 15
  
    |
72 | | breq2 4406 |
. . . . . . . . . . . . . . 15
  
    |
73 | 71, 72 | 3anbi23d 1342 |
. . . . . . . . . . . . . 14
   

 
     |
74 | | csbeq1a 3372 |
. . . . . . . . . . . . . . 15
     ![]_ ]_](_urbrack.gif)   |
75 | 74 | breq2d 4414 |
. . . . . . . . . . . . . 14
  
 
 ![]_ ]_](_urbrack.gif)    |
76 | 73, 75 | imbi12d 322 |
. . . . . . . . . . . . 13
    
 
  
     ![]_ ]_](_urbrack.gif)     |
77 | 69, 70, 76, 30 | vtoclf 3099 |
. . . . . . . . . . . 12
 
      ![]_ ]_](_urbrack.gif)   |
78 | 77 | 3expia 1210 |
. . . . . . . . . . 11
 
  

   ![]_ ]_](_urbrack.gif)    |
79 | 65, 78 | sylan2 477 |
. . . . . . . . . 10
 

     ![]_ ]_](_urbrack.gif)    |
80 | 58 | breq2d 4414 |
. . . . . . . . . 10
 

    ![]_ ]_](_urbrack.gif)
   ![]_ ]_](_urbrack.gif)    |
81 | 79, 80 | sylibd 218 |
. . . . . . . . 9
 

     ![]_ ]_](_urbrack.gif)    |
82 | 34 | adantl 468 |
. . . . . . . . . 10
 

  |
83 | 82 | le0neg1d 10185 |
. . . . . . . . 9
 


    |
84 | 19 | le0neg1d 10185 |
. . . . . . . . 9
 

   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
85 | 81, 83, 84 | 3imtr4d 272 |
. . . . . . . 8
 

   ![]_ ]_](_urbrack.gif)    |
86 | 85 | imp 431 |
. . . . . . 7
       ![]_ ]_](_urbrack.gif)   |
87 | 64, 86 | absnidd 13475 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
88 | 59, 63, 87 | 3eqtr4rd 2496 |
. . . . 5
          ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)   |
89 | | 0re 9643 |
. . . . . . 7
 |
90 | | letric 9734 |
. . . . . . 7
 
 
   |
91 | 89, 34, 90 | sylancr 669 |
. . . . . 6
 
   |
92 | 91 | adantl 468 |
. . . . 5
 

    |
93 | 39, 88, 92 | mpjaodan 795 |
. . . 4
 

     ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)   |
94 | 8, 93 | vtoclg 3107 |
. . 3
  
      ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)    |
95 | 94 | anabsi7 828 |
. 2
 

     ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)   |
96 | | nfcvd 2593 |
. . . . 5
     |
97 | | oddcomabszz.6 |
. . . . 5
   |
98 | 96, 97 | csbiegf 3387 |
. . . 4
   ![]_ ]_](_urbrack.gif)   |
99 | 98 | fveq2d 5869 |
. . 3
      ![]_ ]_](_urbrack.gif)        |
100 | 99 | adantl 468 |
. 2
 

     ![]_ ]_](_urbrack.gif)        |
101 | | fvex 5875 |
. . . 4
     |
102 | | oddcomabszz.7 |
. . . 4
    
  |
103 | 101, 102 | csbie 3389 |
. . 3
      ![]_ ]_](_urbrack.gif)  |
104 | 103 | a1i 11 |
. 2
 

      ![]_ ]_](_urbrack.gif)   |
105 | 95, 100, 104 | 3eqtr3d 2493 |
1
 

      |