Step | Hyp | Ref
| Expression |
1 | | iftrue 3539 |
. . . . . . . . 9
  
       |
2 | 1 | adantl 277 |
. . . . . . . 8
              |
3 | 2 | oveq1d 5884 |
. . . . . . 7
                                  |
4 | | simpl2 1001 |
. . . . . . . . 9
    
  |
5 | | 0z 9253 |
. . . . . . . . . . 11
 |
6 | | zdclt 9319 |
. . . . . . . . . . 11
 
 DECID   |
7 | 5, 6 | mpan2 425 |
. . . . . . . . . 10

DECID
  |
8 | | oveq2 5877 |
. . . . . . . . . . . 12
                       |
9 | | neg1mulneg1e1 9120 |
. . . . . . . . . . . 12
     |
10 | 8, 9 | eqtrdi 2226 |
. . . . . . . . . . 11
                   |
11 | | oveq2 5877 |
. . . . . . . . . . . 12
          
          |
12 | | ax-1cn 7895 |
. . . . . . . . . . . . 13
 |
13 | 12 | mulm1i 8350 |
. . . . . . . . . . . 12
     |
14 | 11, 13 | eqtrdi 2226 |
. . . . . . . . . . 11
          
        |
15 | 10, 14 | ifsbdc 3546 |
. . . . . . . . . 10
DECID
                 |
16 | 7, 15 | syl 14 |
. . . . . . . . 9
                  |
17 | 4, 16 | syl 14 |
. . . . . . . 8
        
             |
18 | | simpr 110 |
. . . . . . . . . . 11
       |
19 | 18 | biantrud 304 |
. . . . . . . . . 10
           |
20 | 19 | ifbid 3555 |
. . . . . . . . 9
             
       |
21 | 20 | oveq2d 5885 |
. . . . . . . 8
        
                  |
22 | | simpl3 1002 |
. . . . . . . . . . . . 13
       |
23 | 22 | necomd 2433 |
. . . . . . . . . . . 12
       |
24 | | zltlen 9320 |
. . . . . . . . . . . . 13
 
  
    |
25 | 4, 5, 24 | sylancl 413 |
. . . . . . . . . . . 12
      
    |
26 | 23, 25 | mpbiran2d 442 |
. . . . . . . . . . 11
         |
27 | 4 | zred 9364 |
. . . . . . . . . . . 12
    
  |
28 | 27 | le0neg1d 8464 |
. . . . . . . . . . 11
          |
29 | | 0re 7948 |
. . . . . . . . . . . 12
 |
30 | 27 | renegcld 8327 |
. . . . . . . . . . . 12
        |
31 | | lenlt 8023 |
. . . . . . . . . . . 12
     
    |
32 | 29, 30, 31 | sylancr 414 |
. . . . . . . . . . 11
       
   |
33 | 26, 28, 32 | 3bitrd 214 |
. . . . . . . . . 10
      
   |
34 | 33 | ifbid 3555 |
. . . . . . . . 9
                    |
35 | | znegcl 9273 |
. . . . . . . . . . . 12
    |
36 | | zdclt 9319 |
. . . . . . . . . . . 12
    DECID 
  |
37 | 35, 5, 36 | sylancl 413 |
. . . . . . . . . . 11

DECID    |
38 | | ifnotdc 3570 |
. . . . . . . . . . 11
DECID 
                |
39 | 37, 38 | syl 14 |
. . . . . . . . . 10
  
              |
40 | 4, 39 | syl 14 |
. . . . . . . . 9
                     |
41 | 34, 40 | eqtrd 2210 |
. . . . . . . 8
                    |
42 | 17, 21, 41 | 3eqtr3d 2218 |
. . . . . . 7
                         |
43 | 18 | biantrud 304 |
. . . . . . . 8
        
    |
44 | 43 | ifbid 3555 |
. . . . . . 7
                       |
45 | 3, 42, 44 | 3eqtrd 2214 |
. . . . . 6
                                |
46 | | 1t1e1 9060 |
. . . . . . 7
   |
47 | | iffalse 3542 |
. . . . . . . . 9
         |
48 | 47 | adantl 277 |
. . . . . . . 8
   

        |
49 | | simpr 110 |
. . . . . . . . . 10
   

  |
50 | 49 | intnand 931 |
. . . . . . . . 9
   

    |
51 | 50 | iffalsed 3544 |
. . . . . . . 8
   

  
       |
52 | 48, 51 | oveq12d 5887 |
. . . . . . 7
   

  
      
          |
53 | 49 | intnand 931 |
. . . . . . . 8
   

     |
54 | 53 | iffalsed 3544 |
. . . . . . 7
   

   
       |
55 | 46, 52, 54 | 3eqtr4a 2236 |
. . . . . 6
   

  
      
         
       |
56 | | simp1 997 |
. . . . . . . 8
 
   |
57 | | zdclt 9319 |
. . . . . . . 8
 
 DECID   |
58 | 56, 5, 57 | sylancl 413 |
. . . . . . 7
 

DECID
  |
59 | | exmiddc 836 |
. . . . . . 7
DECID
    |
60 | 58, 59 | syl 14 |
. . . . . 6
 
     |
61 | 45, 55, 60 | mpjaodan 798 |
. . . . 5
 
          
         
       |
62 | 61 | eqcomd 2183 |
. . . 4
 
                   
        |
63 | | simpr 110 |
. . . . . . . . . . 11
   

  |
64 | | simpl2 1001 |
. . . . . . . . . . . 12
   

  |
65 | | zq 9615 |
. . . . . . . . . . . 12
   |
66 | 64, 65 | syl 14 |
. . . . . . . . . . 11
   

  |
67 | | pcneg 12307 |
. . . . . . . . . . 11
   
      |
68 | 63, 66, 67 | syl2anc 411 |
. . . . . . . . . 10
   
        |
69 | 68 | oveq2d 5885 |
. . . . . . . . 9
   
                   
    |
70 | 69 | adantlr 477 |
. . . . . . . 8
              
               |
71 | | prmdc 12113 |
. . . . . . . . 9

DECID
  |
72 | 71 | adantl 277 |
. . . . . . . 8
   
 DECID   |
73 | 70, 72 | ifeq1dadc 3564 |
. . . . . . 7
   
   
                              |
74 | 73 | mpteq2dva 4090 |
. . . . . 6
 
                                      |
75 | 74 | seqeq3d 10439 |
. . . . 5
 
                                            |
76 | | zcn 9247 |
. . . . . . 7
   |
77 | 76 | 3ad2ant2 1019 |
. . . . . 6
 
   |
78 | 77 | absnegd 11182 |
. . . . 5
 
            |
79 | 75, 78 | fveq12d 5518 |
. . . 4
 
                                                           |
80 | 62, 79 | oveq12d 5887 |
. . 3
 
                                                   
                                    |
81 | | neg1cn 9013 |
. . . . . 6
  |
82 | 81 | a1i 9 |
. . . . 5
 
    |
83 | 12 | a1i 9 |
. . . . 5
 
   |
84 | 82, 83, 58 | ifcldcd 3569 |
. . . 4
 
  
      |
85 | 7 | 3ad2ant2 1019 |
. . . . . 6
 

DECID
  |
86 | | dcan2 934 |
. . . . . 6
DECID
DECID
DECID 
    |
87 | 85, 58, 86 | sylc 62 |
. . . . 5
 

DECID 
   |
88 | 82, 83, 87 | ifcldcd 3569 |
. . . 4
 
           |
89 | | nnuz 9552 |
. . . . . . 7
     |
90 | | 1zzd 9269 |
. . . . . . 7
 
   |
91 | | eqid 2177 |
. . . . . . . . 9
           
                
      |
92 | 91 | lgsfcl3 14089 |
. . . . . . . 8
 
                        |
93 | 92 | ffvelcdmda 5647 |
. . . . . . 7
   
                        |
94 | | zmulcl 9295 |
. . . . . . . 8
 
     |
95 | 94 | adantl 277 |
. . . . . . 7
    
 
    |
96 | 89, 90, 93, 95 | seqf 10447 |
. . . . . 6
 
                           |
97 | | nnabscl 11093 |
. . . . . . 7
         |
98 | 97 | 3adant1 1015 |
. . . . . 6
 
       |
99 | 96, 98 | ffvelcdmd 5648 |
. . . . 5
 
                              |
100 | 99 | zcnd 9365 |
. . . 4
 
                              |
101 | 84, 88, 100 | mulassd 7971 |
. . 3
 
                                                                                             |
102 | 80, 101 | eqtrd 2210 |
. 2
 
                                                   
                  
                 |
103 | 35 | 3ad2ant2 1019 |
. . 3
 
    |
104 | | simp3 999 |
. . . 4
 
   |
105 | 77, 104 | negne0d 8256 |
. . 3
 
    |
106 | | eqid 2177 |
. . . 4
           
                 
       |
107 | 106 | lgsval4 14088 |
. . 3
              
                  
                  |
108 | 56, 103, 105, 107 | syl3anc 1238 |
. 2
 
                                                |
109 | 91 | lgsval4 14088 |
. . 3
 
        
                  
                |
110 | 109 | oveq2d 5885 |
. 2
 
                                                            |
111 | 102, 108,
110 | 3eqtr4d 2220 |
1
 
                    |