Proof of Theorem lgsdilem
Step | Hyp | Ref
| Expression |
1 | | simplrr 536 |
. . . . . . . . . . 11
           |
2 | 1 | biantrud 304 |
. . . . . . . . . 10
          
    |
3 | | 0z 9253 |
. . . . . . . . . . 11
 |
4 | | simpl2 1001 |
. . . . . . . . . . . 12
  
 
    |
5 | 4 | adantr 276 |
. . . . . . . . . . 11
        
  |
6 | | zltlen 9320 |
. . . . . . . . . . 11
 
  
    |
7 | 3, 5, 6 | sylancr 414 |
. . . . . . . . . 10
          
    |
8 | | simpl1 1000 |
. . . . . . . . . . . . . . . . 17
  
 
    |
9 | 8 | zred 9364 |
. . . . . . . . . . . . . . . 16
  
 
    |
10 | 9 | adantr 276 |
. . . . . . . . . . . . . . 15
        
  |
11 | 10 | renegcld 8327 |
. . . . . . . . . . . . . 14
            |
12 | 11 | recnd 7976 |
. . . . . . . . . . . . 13
            |
13 | 12 | mul01d 8340 |
. . . . . . . . . . . 12
              |
14 | 10 | recnd 7976 |
. . . . . . . . . . . . 13
        
  |
15 | 4 | zred 9364 |
. . . . . . . . . . . . . . 15
  
 
    |
16 | 15 | adantr 276 |
. . . . . . . . . . . . . 14
        
  |
17 | 16 | recnd 7976 |
. . . . . . . . . . . . 13
        
  |
18 | 14, 17 | mulneg1d 8358 |
. . . . . . . . . . . 12
             
   |
19 | 13, 18 | breq12d 4013 |
. . . . . . . . . . 11
                 
    |
20 | | 0red 7949 |
. . . . . . . . . . . 12
           |
21 | 9 | lt0neg1d 8462 |
. . . . . . . . . . . . 13
  
 
  
    |
22 | 21 | biimpa 296 |
. . . . . . . . . . . 12
        
   |
23 | | ltmul2 8802 |
. . . . . . . . . . . 12
 
               |
24 | 20, 16, 11, 22, 23 | syl112anc 1242 |
. . . . . . . . . . 11
              
    |
25 | 9, 15 | remulcld 7978 |
. . . . . . . . . . . . 13
  
 
  
   |
26 | 25 | adantr 276 |
. . . . . . . . . . . 12
             |
27 | 26 | lt0neg1d 8462 |
. . . . . . . . . . 11
                  |
28 | 19, 24, 27 | 3bitr4d 220 |
. . . . . . . . . 10
               |
29 | 2, 7, 28 | 3bitr2rd 217 |
. . . . . . . . 9
               |
30 | | 0re 7948 |
. . . . . . . . . 10
 |
31 | | lenlt 8023 |
. . . . . . . . . 10
 
     |
32 | 30, 16, 31 | sylancr 414 |
. . . . . . . . 9
             |
33 | 29, 32 | bitrd 188 |
. . . . . . . 8
               |
34 | 33 | ifbid 3555 |
. . . . . . 7
                         |
35 | | zdclt 9319 |
. . . . . . . . . . 11
 
 DECID   |
36 | 3, 35 | mpan2 425 |
. . . . . . . . . 10

DECID
  |
37 | | oveq2 5877 |
. . . . . . . . . . . . 13
                       |
38 | | neg1mulneg1e1 9120 |
. . . . . . . . . . . . 13
     |
39 | 37, 38 | eqtrdi 2226 |
. . . . . . . . . . . 12
                   |
40 | | oveq2 5877 |
. . . . . . . . . . . . 13
          
          |
41 | | ax-1cn 7895 |
. . . . . . . . . . . . . 14
 |
42 | 41 | mulm1i 8350 |
. . . . . . . . . . . . 13
     |
43 | 40, 42 | eqtrdi 2226 |
. . . . . . . . . . . 12
          
        |
44 | 39, 43 | ifsbdc 3546 |
. . . . . . . . . . 11
DECID
                 |
45 | | ifnotdc 3570 |
. . . . . . . . . . 11
DECID
 
            |
46 | 44, 45 | eqtr4d 2213 |
. . . . . . . . . 10
DECID
                 |
47 | 36, 46 | syl 14 |
. . . . . . . . 9
                  |
48 | 47 | 3ad2ant2 1019 |
. . . . . . . 8
 
                  |
49 | 48 | ad2antrr 488 |
. . . . . . 7
            
             |
50 | 34, 49 | eqtr4d 2213 |
. . . . . 6
                            |
51 | | iftrue 3539 |
. . . . . . . 8
  
       |
52 | 51 | adantl 277 |
. . . . . . 7
                  |
53 | 52 | oveq1d 5884 |
. . . . . 6
                                  |
54 | 50, 53 | eqtr4d 2213 |
. . . . 5
                                 |
55 | | iffalse 3542 |
. . . . . . . 8
         |
56 | 55 | adantl 277 |
. . . . . . 7
       

        |
57 | 56 | oveq1d 5884 |
. . . . . 6
       

  
                     |
58 | | neg1cn 9013 |
. . . . . . . . 9
  |
59 | 58 | a1i 9 |
. . . . . . . 8
       

   |
60 | 41 | a1i 9 |
. . . . . . . 8
       

  |
61 | 4 | adantr 276 |
. . . . . . . . 9
       

  |
62 | 61, 3, 35 | sylancl 413 |
. . . . . . . 8
       

DECID
  |
63 | 59, 60, 62 | ifcldcd 3569 |
. . . . . . 7
       

        |
64 | 63 | mulid2d 7966 |
. . . . . 6
       

                |
65 | 15 | adantr 276 |
. . . . . . . . 9
       

  |
66 | | 0red 7949 |
. . . . . . . . 9
       

  |
67 | 9 | adantr 276 |
. . . . . . . . 9
       

  |
68 | | simplrl 535 |
. . . . . . . . . . 11
       

  |
69 | 68 | neneqd 2368 |
. . . . . . . . . 10
       

  |
70 | | simpr 110 |
. . . . . . . . . . . 12
       

  |
71 | 8 | adantr 276 |
. . . . . . . . . . . . . . 15
       

  |
72 | | ztri3or 9285 |
. . . . . . . . . . . . . . 15
 
 
   |
73 | 71, 3, 72 | sylancl 413 |
. . . . . . . . . . . . . 14
       

    |
74 | | 3orass 981 |
. . . . . . . . . . . . . 14
         |
75 | 73, 74 | sylib 122 |
. . . . . . . . . . . . 13
       

      |
76 | 75 | orcomd 729 |
. . . . . . . . . . . 12
       

 
    |
77 | 70, 76 | ecased 1349 |
. . . . . . . . . . 11
       

    |
78 | 77 | orcomd 729 |
. . . . . . . . . 10
       

    |
79 | 69, 78 | ecased 1349 |
. . . . . . . . 9
       

  |
80 | | ltmul2 8802 |
. . . . . . . . 9
 

          |
81 | 65, 66, 67, 79, 80 | syl112anc 1242 |
. . . . . . . 8
       

   
    |
82 | 67 | recnd 7976 |
. . . . . . . . . 10
       

  |
83 | 82 | mul01d 8340 |
. . . . . . . . 9
       

    |
84 | 83 | breq2d 4012 |
. . . . . . . 8
       

 
        |
85 | 81, 84 | bitrd 188 |
. . . . . . 7
       

      |
86 | 85 | ifbid 3555 |
. . . . . 6
       

                |
87 | 57, 64, 86 | 3eqtrrd 2215 |
. . . . 5
       

   
                    |
88 | | zdclt 9319 |
. . . . . . 7
 
 DECID   |
89 | 8, 3, 88 | sylancl 413 |
. . . . . 6
  
 
 
DECID
  |
90 | | exmiddc 836 |
. . . . . 6
DECID
    |
91 | 89, 90 | syl 14 |
. . . . 5
  
 
      |
92 | 54, 87, 91 | mpjaodan 798 |
. . . 4
  
 
                          |
93 | 92 | adantr 276 |
. . 3
                                 |
94 | | simpr 110 |
. . . . 5
           |
95 | 94 | biantrurd 305 |
. . . 4
              
    |
96 | 95 | ifbid 3555 |
. . 3
                     
       |
97 | 94 | biantrurd 305 |
. . . . 5
               |
98 | 97 | ifbid 3555 |
. . . 4
                 
       |
99 | 94 | biantrurd 305 |
. . . . 5
               |
100 | 99 | ifbid 3555 |
. . . 4
                 
       |
101 | 98, 100 | oveq12d 5887 |
. . 3
                                           |
102 | 93, 96, 101 | 3eqtr3d 2218 |
. 2
                      
                |
103 | | simpr 110 |
. . . . . 6
       

  |
104 | 103 | intnanrd 932 |
. . . . 5
       

 
    |
105 | 104 | iffalsed 3544 |
. . . 4
       

    
       |
106 | | 1t1e1 9060 |
. . . 4
   |
107 | 105, 106 | eqtr4di 2228 |
. . 3
       

    
         |
108 | 103 | intnanrd 932 |
. . . . 5
       

    |
109 | 108 | iffalsed 3544 |
. . . 4
       

  
       |
110 | 103 | intnanrd 932 |
. . . . 5
       

    |
111 | 110 | iffalsed 3544 |
. . . 4
       

  
       |
112 | 109, 111 | oveq12d 5887 |
. . 3
       

                      |
113 | 107, 112 | eqtr4d 2213 |
. 2
       

    
                         |
114 | | simpl3 1002 |
. . . 4
  
 
    |
115 | | zdclt 9319 |
. . . 4
 
 DECID   |
116 | 114, 3, 115 | sylancl 413 |
. . 3
  
 
 
DECID
  |
117 | | exmiddc 836 |
. . 3
DECID
    |
118 | 116, 117 | syl 14 |
. 2
  
 
      |
119 | 102, 113,
118 | mpjaodan 798 |
1
  
 
               
                |