Proof of Theorem fldivp1
Step | Hyp | Ref
| Expression |
1 | | nnz 9261 |
. . . . . . . . 9
   |
2 | | nnne0 8936 |
. . . . . . . . 9
   |
3 | | peano2z 9278 |
. . . . . . . . . 10
 
   |
4 | 3 | adantr 276 |
. . . . . . . . 9
 
     |
5 | | dvdsval2 11781 |
. . . . . . . . 9
  
   
        |
6 | 1, 2, 4, 5 | syl2an23an 1299 |
. . . . . . . 8
 
  
        |
7 | 6 | biimpa 296 |
. . . . . . 7
    
 
 
    |
8 | | flid 10270 |
. . . . . . 7
                   |
9 | 7, 8 | syl 14 |
. . . . . 6
    
 
              |
10 | | nnm1nn0 9206 |
. . . . . . . . . 10
 
   |
11 | 10 | nn0red 9219 |
. . . . . . . . 9
 
   |
12 | 10 | nn0ge0d 9221 |
. . . . . . . . 9
     |
13 | | nnre 8915 |
. . . . . . . . 9
   |
14 | | nngt0 8933 |
. . . . . . . . 9
   |
15 | | divge0 8819 |
. . . . . . . . 9
    
     
 
    |
16 | 11, 12, 13, 14, 15 | syl22anc 1239 |
. . . . . . . 8
       |
17 | 16 | ad2antlr 489 |
. . . . . . 7
    
 
      |
18 | 13 | ltm1d 8878 |
. . . . . . . . . 10
 
   |
19 | | nncn 8916 |
. . . . . . . . . . 11
   |
20 | 19 | mulid1d 7965 |
. . . . . . . . . 10
 
   |
21 | 18, 20 | breqtrrd 4028 |
. . . . . . . . 9
 
     |
22 | | 1red 7963 |
. . . . . . . . . 10
   |
23 | | ltdivmul 8822 |
. . . . . . . . . 10
   

              |
24 | 11, 22, 13, 14, 23 | syl112anc 1242 |
. . . . . . . . 9
     
       |
25 | 21, 24 | mpbird 167 |
. . . . . . . 8
       |
26 | 25 | ad2antlr 489 |
. . . . . . 7
    
 
 
    |
27 | 10 | nn0zd 9362 |
. . . . . . . . . 10
 
   |
28 | | znq 9613 |
. . . . . . . . . 10
   
       |
29 | 27, 28 | mpancom 422 |
. . . . . . . . 9
       |
30 | 29 | ad2antlr 489 |
. . . . . . . 8
    
 
 
    |
31 | | flqbi2 10277 |
. . . . . . . 8
                                  
 
      |
32 | 7, 30, 31 | syl2anc 411 |
. . . . . . 7
    
 
                       
 
      |
33 | 17, 26, 32 | mpbir2and 944 |
. . . . . 6
    
 
                    |
34 | 9, 33 | eqtr4d 2213 |
. . . . 5
    
 
                        |
35 | | zcn 9247 |
. . . . . . . . . 10
   |
36 | 35 | adantr 276 |
. . . . . . . . 9
 
   |
37 | 19 | adantl 277 |
. . . . . . . . 9
 
   |
38 | | nnap0 8937 |
. . . . . . . . . 10
 #   |
39 | 38 | adantl 277 |
. . . . . . . . 9
 
 #   |
40 | 36, 37, 37, 39 | divdirapd 8775 |
. . . . . . . 8
 
             |
41 | | ax-1cn 7895 |
. . . . . . . . . . . 12
 |
42 | 41 | a1i 9 |
. . . . . . . . . . 11
 
   |
43 | 36, 42, 37 | ppncand 8298 |
. . . . . . . . . 10
 
           |
44 | 43 | oveq1d 5884 |
. . . . . . . . 9
 
               |
45 | 4 | zcnd 9365 |
. . . . . . . . . 10
 
     |
46 | | subcl 8146 |
. . . . . . . . . . . 12
 
     |
47 | 19, 41, 46 | sylancl 413 |
. . . . . . . . . . 11
 
   |
48 | 47 | adantl 277 |
. . . . . . . . . 10
 
     |
49 | 45, 48, 37, 39 | divdirapd 8775 |
. . . . . . . . 9
 
                     |
50 | 44, 49 | eqtr3d 2212 |
. . . . . . . 8
 
                 |
51 | 37, 39 | dividapd 8732 |
. . . . . . . . 9
 
     |
52 | 51 | oveq2d 5885 |
. . . . . . . 8
 
             |
53 | 40, 50, 52 | 3eqtr3d 2218 |
. . . . . . 7
 
                 |
54 | 53 | fveq2d 5515 |
. . . . . 6
 
                         |
55 | 54 | adantr 276 |
. . . . 5
    
 
                        |
56 | | znq 9613 |
. . . . . . 7
 
     |
57 | | 1z 9268 |
. . . . . . 7
 |
58 | | flqaddz 10283 |
. . . . . . 7
   
                   |
59 | 56, 57, 58 | sylancl 413 |
. . . . . 6
 
                   |
60 | 59 | adantr 276 |
. . . . 5
    
 
                  |
61 | 34, 55, 60 | 3eqtrrd 2215 |
. . . 4
    
 
                  |
62 | | znq 9613 |
. . . . . . . . 9
   
       |
63 | 3, 62 | sylan 283 |
. . . . . . . 8
 
       |
64 | 63 | flqcld 10263 |
. . . . . . 7
 
           |
65 | 64 | zcnd 9365 |
. . . . . 6
 
           |
66 | 56 | flqcld 10263 |
. . . . . . 7
 
         |
67 | 66 | zcnd 9365 |
. . . . . 6
 
         |
68 | 65, 67, 42 | subaddd 8276 |
. . . . 5
 
                                     |
69 | 68 | adantr 276 |
. . . 4
    
 
                
                   |
70 | 61, 69 | mpbird 167 |
. . 3
    
 
                  |
71 | | iftrue 3539 |
. . . 4
    
       |
72 | 71 | adantl 277 |
. . 3
    
 
         |
73 | 70, 72 | eqtr4d 2213 |
. 2
    
 
                         |
74 | | zmodcl 10330 |
. . . . . . . . . . 11
   
       |
75 | 3, 74 | sylan 283 |
. . . . . . . . . 10
 
       |
76 | 75 | nn0red 9219 |
. . . . . . . . 9
 
       |
77 | | 1re 7947 |
. . . . . . . . 9
 |
78 | | resubcl 8211 |
. . . . . . . . 9
     
         |
79 | 76, 77, 78 | sylancl 413 |
. . . . . . . 8
 
         |
80 | 79 | adantr 276 |
. . . . . . 7
    
          |
81 | 75 | nn0zd 9362 |
. . . . . . . . . . . 12
 
       |
82 | | elnndc 9601 |
. . . . . . . . . . . 12
    
DECID       |
83 | 81, 82 | syl 14 |
. . . . . . . . . . 11
 
 DECID       |
84 | | elnn0 9167 |
. . . . . . . . . . . . . 14
    
            |
85 | 75, 84 | sylib 122 |
. . . . . . . . . . . . 13
 
             |
86 | 85 | ord 724 |
. . . . . . . . . . . 12
 
     
 
     |
87 | | id 19 |
. . . . . . . . . . . . 13
   |
88 | | dvdsval3 11782 |
. . . . . . . . . . . . 13
  
   
        |
89 | 87, 3, 88 | syl2anr 290 |
. . . . . . . . . . . 12
 
  
        |
90 | 86, 89 | sylibrd 169 |
. . . . . . . . . . 11
 
     

    |
91 | | con1dc 856 |
. . . . . . . . . . 11
DECID    
          

 
      |
92 | 83, 90, 91 | sylc 62 |
. . . . . . . . . 10
 
  

 
     |
93 | 92 | imp 124 |
. . . . . . . . 9
    
        |
94 | | nnm1nn0 9206 |
. . . . . . . . 9
             |
95 | 93, 94 | syl 14 |
. . . . . . . 8
    
          |
96 | 95 | nn0ge0d 9221 |
. . . . . . 7
    
          |
97 | 13, 14 | jca 306 |
. . . . . . . 8
 
   |
98 | 97 | ad2antlr 489 |
. . . . . . 7
    
  
   |
99 | | divge0 8819 |
. . . . . . 7
        
         
          |
100 | 80, 96, 98, 99 | syl21anc 1237 |
. . . . . 6
    
            |
101 | 13 | adantl 277 |
. . . . . . . . . 10
 
   |
102 | 76 | ltm1d 8878 |
. . . . . . . . . 10
 
             |
103 | | zq 9615 |
. . . . . . . . . . . . 13
   
   |
104 | 3, 103 | syl 14 |
. . . . . . . . . . . 12
 
   |
105 | 104 | adantr 276 |
. . . . . . . . . . 11
 
     |
106 | | nnq 9622 |
. . . . . . . . . . . 12
   |
107 | 106 | adantl 277 |
. . . . . . . . . . 11
 
   |
108 | 14 | adantl 277 |
. . . . . . . . . . 11
 
   |
109 | | modqlt 10319 |
. . . . . . . . . . 11
   
       |
110 | 105, 107,
108, 109 | syl3anc 1238 |
. . . . . . . . . 10
 
    
  |
111 | 79, 76, 101, 102, 110 | lttrd 8073 |
. . . . . . . . 9
 
         |
112 | 37 | mulid1d 7965 |
. . . . . . . . 9
 
     |
113 | 111, 112 | breqtrrd 4028 |
. . . . . . . 8
 
           |
114 | | 1red 7963 |
. . . . . . . . 9
 
   |
115 | | ltdivmul 8822 |
. . . . . . . . 9
       

                      |
116 | 79, 114, 101, 108, 115 | syl112anc 1242 |
. . . . . . . 8
 
                     |
117 | 113, 116 | mpbird 167 |
. . . . . . 7
 
        
  |
118 | 117 | adantr 276 |
. . . . . 6
    
            |
119 | | peano2zm 9280 |
. . . . . . . . . 10
             |
120 | 81, 119 | syl 14 |
. . . . . . . . 9
 
         |
121 | | znq 9613 |
. . . . . . . . 9
       
           |
122 | 120, 121 | sylancom 420 |
. . . . . . . 8
 
           |
123 | | flqbi2 10277 |
. . . . . . . 8
                                                          
            |
124 | 64, 122, 123 | syl2anc 411 |
. . . . . . 7
 
                                                     |
125 | 124 | adantr 276 |
. . . . . 6
    
                                
                     |
126 | 100, 118,
125 | mpbir2and 944 |
. . . . 5
    
                                  |
127 | | modqval 10310 |
. . . . . . . . . . . . 13
   
        
            |
128 | 105, 107,
108, 127 | syl3anc 1238 |
. . . . . . . . . . . 12
 
                     |
129 | 128 | oveq1d 5884 |
. . . . . . . . . . 11
 
                         |
130 | 37, 65 | mulcld 7968 |
. . . . . . . . . . . 12
 
             |
131 | 45, 42, 130 | sub32d 8290 |
. . . . . . . . . . 11
 
      
                            |
132 | | pncan 8153 |
. . . . . . . . . . . . 13
 
       |
133 | 36, 41, 132 | sylancl 413 |
. . . . . . . . . . . 12
 
       |
134 | 133 | oveq1d 5884 |
. . . . . . . . . . 11
 
      
           
            |
135 | 129, 131,
134 | 3eqtr2d 2216 |
. . . . . . . . . 10
 
                     |
136 | 135 | oveq1d 5884 |
. . . . . . . . 9
 
                         |
137 | 36, 130, 37, 39 | divsubdirapd 8776 |
. . . . . . . . 9
 
   
                             |
138 | 65, 37, 39 | divcanap3d 8741 |
. . . . . . . . . 10
 
                       |
139 | 138 | oveq2d 5885 |
. . . . . . . . 9
 
                               |
140 | 136, 137,
139 | 3eqtrrd 2215 |
. . . . . . . 8
 
                       |
141 | | zre 9246 |
. . . . . . . . . . 11
   |
142 | | nndivre 8944 |
. . . . . . . . . . 11
 
     |
143 | 141, 142 | sylan 283 |
. . . . . . . . . 10
 
     |
144 | 143 | recnd 7976 |
. . . . . . . . 9
 
     |
145 | | nndivre 8944 |
. . . . . . . . . . 11
       
           |
146 | 79, 145 | sylancom 420 |
. . . . . . . . . 10
 
           |
147 | 146 | recnd 7976 |
. . . . . . . . 9
 
           |
148 | 144, 65, 147 | subaddd 8276 |
. . . . . . . 8
 
                     
                       |
149 | 140, 148 | mpbid 147 |
. . . . . . 7
 
                       |
150 | 149 | adantr 276 |
. . . . . 6
    
                        |
151 | 150 | fveq2d 5515 |
. . . . 5
    
                                |
152 | 126, 151 | eqtr3d 2212 |
. . . 4
    
                  |
153 | 65, 67 | subeq0ad 8268 |
. . . . 5
 
                                   |
154 | 153 | adantr 276 |
. . . 4
    
                  
                 |
155 | 152, 154 | mpbird 167 |
. . 3
    
                    |
156 | | iffalse 3542 |
. . . 4
     
      |
157 | 156 | adantl 277 |
. . 3
    
   
       |
158 | 155, 157 | eqtr4d 2213 |
. 2
    
                           |
159 | | simpr 110 |
. . . 4
 
   |
160 | | dvdsdc 11789 |
. . . 4
  
  DECID
    |
161 | 159, 4, 160 | syl2anc 411 |
. . 3
 
 DECID     |
162 | | exmiddc 836 |
. . 3
DECID 

        |
163 | 161, 162 | syl 14 |
. 2
 
  
 
    |
164 | 73, 158, 163 | mpjaodan 798 |
1
 
                          |