Proof of Theorem modfzo0difsn
Step | Hyp | Ref
| Expression |
1 | | eldifi 3257 |
. . . 4
   ..^     ..^   |
2 | | elfzoelz 10120 |
. . . 4
  ..^
  |
3 | 1, 2 | syl 14 |
. . 3
   ..^      |
4 | | elfzoelz 10120 |
. . 3
  ..^
  |
5 | | zdcle 9305 |
. . . 4
 
 DECID   |
6 | | exmiddc 836 |
. . . 4
DECID 
   |
7 | 5, 6 | syl 14 |
. . 3
 
     |
8 | 3, 4, 7 | syl2anr 290 |
. 2
   ..^   ..^         |
9 | | zleloe 9276 |
. . . . . 6
 
  
    |
10 | 3, 4, 9 | syl2anr 290 |
. . . . 5
   ..^   ..^      
    |
11 | | elfzo0 10155 |
. . . . . . . . . . . . 13
  ..^ 
   |
12 | | elfzo0 10155 |
. . . . . . . . . . . . . . . 16
  ..^ 
   |
13 | | nn0cn 9162 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
14 | 13 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . 22
  
  |
15 | 14 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
  |
16 | | nn0cn 9162 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
17 | 16 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
18 | 17 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
  |
19 | | nncn 8903 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
20 | 19 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
21 | 20 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
  |
22 | 15, 18, 21 | subadd23d 8267 |
. . . . . . . . . . . . . . . . . . . 20
    
 
 
        |
23 | | simpl 109 |
. . . . . . . . . . . . . . . . . . . . 21
  
  |
24 | | nn0z 9249 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
25 | | nnz 9248 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
26 | | znnsub 9280 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       |
27 | 24, 25, 26 | syl2an 289 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
28 | 27 | biimp3a 1345 |
. . . . . . . . . . . . . . . . . . . . 21
 
 
   |
29 | | nn0nnaddcl 9183 |
. . . . . . . . . . . . . . . . . . . . 21
  
   
    |
30 | 23, 28, 29 | syl2anr 290 |
. . . . . . . . . . . . . . . . . . . 20
    
 
      |
31 | 22, 30 | eqeltrd 2254 |
. . . . . . . . . . . . . . . . . . 19
    
 
 
    |
32 | 31 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
   

          |
33 | | simp2 998 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
34 | 33 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
    
 
  |
35 | 34 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
   

   
  |
36 | | nn0re 9161 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
37 | 36 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
  |
38 | 37 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
  |
39 | | nn0re 9161 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
40 | 39 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
41 | 40 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
  |
42 | 38, 41 | sublt0d 8504 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
 

   |
43 | 42 | bicomd 141 |
. . . . . . . . . . . . . . . . . . . 20
    
 
      |
44 | 43 | biimpa 296 |
. . . . . . . . . . . . . . . . . . 19
   

     
  |
45 | | resubcl 8198 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
46 | 37, 40, 45 | syl2anr 290 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
    |
47 | | nnre 8902 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
48 | 47 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
49 | 48 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
  |
50 | 46, 49 | jca 306 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
 
    |
51 | 50 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
   

          |
52 | | ltaddnegr 8359 |
. . . . . . . . . . . . . . . . . . . 20
   
           |
53 | 51, 52 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
   

              |
54 | 44, 53 | mpbid 147 |
. . . . . . . . . . . . . . . . . 18
   

       
  |
55 | | elfzo1 10163 |
. . . . . . . . . . . . . . . . . 18
      ..^             |
56 | 32, 35, 54, 55 | syl3anbrc 1181 |
. . . . . . . . . . . . . . . . 17
   

         ..^   |
57 | 56 | exp31 364 |
. . . . . . . . . . . . . . . 16
 
    
 
   ..^     |
58 | 12, 57 | sylbi 121 |
. . . . . . . . . . . . . . 15
  ..^
 
       ..^     |
59 | 58 | com12 30 |
. . . . . . . . . . . . . 14
     ..^       ..^     |
60 | 59 | 3adant2 1016 |
. . . . . . . . . . . . 13
 
 
 ..^       ..^     |
61 | 11, 60 | sylbi 121 |
. . . . . . . . . . . 12
  ..^
  ..^ 
 
   ..^     |
62 | 1, 61 | syl 14 |
. . . . . . . . . . 11
   ..^    
 ..^       ..^     |
63 | 62 | impcom 125 |
. . . . . . . . . 10
   ..^   ..^           ..^    |
64 | 63 | impcom 125 |
. . . . . . . . 9
  
 ..^
  ..^     
 
   ..^   |
65 | | oveq1 5875 |
. . . . . . . . . . . 12
               |
66 | 2 | zcnd 9352 |
. . . . . . . . . . . . . . . . . . . . . 22
  ..^
  |
67 | 66 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^ 
 
  |
68 | 16 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
69 | 68 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^ 
 
  |
70 | 19 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
71 | 70 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^ 
 
  |
72 | 67, 69, 71 | 3jca 1177 |
. . . . . . . . . . . . . . . . . . . 20
   ..^ 
  
   |
73 | 72 | ex 115 |
. . . . . . . . . . . . . . . . . . 19
  ..^
 
 
    |
74 | 1, 73 | syl 14 |
. . . . . . . . . . . . . . . . . 18
   ..^            |
75 | 74 | com12 30 |
. . . . . . . . . . . . . . . . 17
 
    ..^   
     |
76 | 75 | 3adant3 1017 |
. . . . . . . . . . . . . . . 16
 
 
  ..^    
    |
77 | 12, 76 | sylbi 121 |
. . . . . . . . . . . . . . 15
  ..^
   ..^    
    |
78 | 77 | imp 124 |
. . . . . . . . . . . . . 14
   ..^   ..^     
   |
79 | 78 | adantl 277 |
. . . . . . . . . . . . 13
  
 ..^
  ..^     
    |
80 | | nppcan 8156 |
. . . . . . . . . . . . 13
 
           |
81 | 79, 80 | syl 14 |
. . . . . . . . . . . 12
  
 ..^
  ..^     
          |
82 | 65, 81 | sylan9eqr 2232 |
. . . . . . . . . . 11
     ..^
  ..^                 |
83 | 82 | oveq1d 5883 |
. . . . . . . . . 10
     ..^
  ..^             
       |
84 | 83 | eqeq2d 2189 |
. . . . . . . . 9
     ..^
  ..^           
   
       |
85 | 11 | biimpi 120 |
. . . . . . . . . . . . . 14
  ..^
    |
86 | 85 | a1d 22 |
. . . . . . . . . . . . 13
  ..^
  ..^ 
    |
87 | 1, 86 | syl 14 |
. . . . . . . . . . . 12
   ..^    
 ..^ 
    |
88 | 87 | impcom 125 |
. . . . . . . . . . 11
   ..^   ..^         |
89 | 88 | adantl 277 |
. . . . . . . . . 10
  
 ..^
  ..^     
    |
90 | | addmodidr 10346 |
. . . . . . . . . . 11
 
   
   |
91 | 90 | eqcomd 2183 |
. . . . . . . . . 10
 
       |
92 | 89, 91 | syl 14 |
. . . . . . . . 9
  
 ..^
  ..^     
      |
93 | 64, 84, 92 | rspcedvd 2847 |
. . . . . . . 8
  
 ..^
  ..^     
  ..^        |
94 | 93 | ex 115 |
. . . . . . 7
    ..^
  ..^       ..^         |
95 | | eldifsn 3718 |
. . . . . . . . . 10
   ..^   
  ..^    |
96 | | eqneqall 2357 |
. . . . . . . . . . . 12
    ..^         |
97 | 96 | com12 30 |
. . . . . . . . . . 11
 
  ..^         |
98 | 97 | adantl 277 |
. . . . . . . . . 10
   ..^  
  ..^         |
99 | 95, 98 | sylbi 121 |
. . . . . . . . 9
   ..^    
  ..^         |
100 | 99 | adantl 277 |
. . . . . . . 8
   ..^   ..^        ..^         |
101 | 100 | com12 30 |
. . . . . . 7
    ..^
  ..^       ..^         |
102 | 94, 101 | jaoi 716 |
. . . . . 6
 
    ..^   ..^       ..^         |
103 | 102 | com12 30 |
. . . . 5
   ..^   ..^          ..^         |
104 | 10, 103 | sylbid 150 |
. . . 4
   ..^   ..^        ..^         |
105 | 104 | com12 30 |
. . 3
    ..^
  ..^       ..^         |
106 | | zltnle 9275 |
. . . . . . . . . 10
 
 
   |
107 | 4, 3, 106 | syl2an 289 |
. . . . . . . . 9
   ..^   ..^     
   |
108 | 107 | bicomd 141 |
. . . . . . . 8
   ..^   ..^         |
109 | 24 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . 18
 
   |
110 | | nn0z 9249 |
. . . . . . . . . . . . . . . . . . 19

  |
111 | 110 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
  
  |
112 | | znnsub 9280 |
. . . . . . . . . . . . . . . . . 18
 
       |
113 | 109, 111,
112 | syl2anr 290 |
. . . . . . . . . . . . . . . . 17
    
  
     |
114 | 113 | biimpa 296 |
. . . . . . . . . . . . . . . 16
   
 
       |
115 | 33 | adantl 277 |
. . . . . . . . . . . . . . . . 17
    
    |
116 | 115 | adantr 276 |
. . . . . . . . . . . . . . . 16
   
 
  
  |
117 | | nn0ge0 9177 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
118 | 117 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
119 | 118 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
  
    |
120 | | subge02 8412 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
121 | 36, 40, 120 | syl2an 289 |
. . . . . . . . . . . . . . . . . . . . 21
  
    
   |
122 | 119, 121 | mpbid 147 |
. . . . . . . . . . . . . . . . . . . 20
  
      |
123 | 40 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
    |
124 | 36 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
    |
125 | 48 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
    |
126 | 123, 124,
125 | 3jca 1177 |
. . . . . . . . . . . . . . . . . . . . . 22
  
      |
127 | 45 | ancoms 268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
128 | 127 | 3adant3 1017 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
   |
129 | | simp2 998 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
130 | | simp3 999 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
131 | 128, 129,
130 | 3jca 1177 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   
   |
132 | 126, 131 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
  
        |
133 | | lelttr 8023 |
. . . . . . . . . . . . . . . . . . . . 21
   
    
      |
134 | 132, 133 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
  
       
    |
135 | 122, 134 | mpand 429 |
. . . . . . . . . . . . . . . . . . 19
  
  
     |
136 | 135 | impancom 260 |
. . . . . . . . . . . . . . . . . 18
    

     |
137 | 136 | imp 124 |
. . . . . . . . . . . . . . . . 17
    
  
   |
138 | 137 | adantr 276 |
. . . . . . . . . . . . . . . 16
   
 
    
  |
139 | 114, 116,
138 | 3jca 1177 |
. . . . . . . . . . . . . . 15
   
 
      

   |
140 | 139 | exp31 364 |
. . . . . . . . . . . . . 14
    


 
        |
141 | 140 | 3adant2 1016 |
. . . . . . . . . . . . 13
 
        

     |
142 | 11, 141 | sylbi 121 |
. . . . . . . . . . . 12
  ..^
 
    

      |
143 | 1, 142 | syl 14 |
. . . . . . . . . . 11
   ..^           

     |
144 | 143 | com12 30 |
. . . . . . . . . 10
 
 
  ..^        

     |
145 | 12, 144 | sylbi 121 |
. . . . . . . . 9
  ..^
   ..^       

      |
146 | 145 | imp 124 |
. . . . . . . 8
   ..^   ..^         

    |
147 | 108, 146 | sylbid 150 |
. . . . . . 7
   ..^   ..^               |
148 | 147 | impcom 125 |
. . . . . 6
    ..^
  ..^     
 
      |
149 | | elfzo1 10163 |
. . . . . 6
    ..^         |
150 | 148, 149 | sylibr 134 |
. . . . 5
    ..^
  ..^     
   ..^   |
151 | | oveq1 5875 |
. . . . . . . 8
           |
152 | 1, 66 | syl 14 |
. . . . . . . . . 10
   ..^      |
153 | 4 | zcnd 9352 |
. . . . . . . . . 10
  ..^
  |
154 | | npcan 8143 |
. . . . . . . . . 10
 
       |
155 | 152, 153,
154 | syl2anr 290 |
. . . . . . . . 9
   ..^   ..^           |
156 | 155 | adantl 277 |
. . . . . . . 8
    ..^
  ..^     
 
    |
157 | 151, 156 | sylan9eqr 2232 |
. . . . . . 7
     ..^   ..^     
       |
158 | 157 | oveq1d 5883 |
. . . . . 6
     ..^   ..^     
           |
159 | 158 | eqeq2d 2189 |
. . . . 5
     ..^   ..^     
      
      |
160 | | zmodidfzoimp 10327 |
. . . . . . . . 9
  ..^
    |
161 | 1, 160 | syl 14 |
. . . . . . . 8
   ..^        |
162 | 161 | adantl 277 |
. . . . . . 7
   ..^   ..^         |
163 | 162 | adantl 277 |
. . . . . 6
    ..^
  ..^     
    |
164 | 163 | eqcomd 2183 |
. . . . 5
    ..^
  ..^     

   |
165 | 150, 159,
164 | rspcedvd 2847 |
. . . 4
    ..^
  ..^     
  ..^        |
166 | 165 | ex 115 |
. . 3

   ..^
  ..^       ..^         |
167 | 105, 166 | jaoi 716 |
. 2
 
    ..^   ..^     
 ..^         |
168 | 8, 167 | mpcom 36 |
1
   ..^   ..^     
 ..^        |