Proof of Theorem diophrw
Step | Hyp | Ref
| Expression |
1 | | simpr 468 |
. . . . . . . . . 10
                  |
2 | | nn0ex 10899 |
. . . . . . . . . . 11
 |
3 | | simp1 1030 |
. . . . . . . . . . . 12
      
  
  |
4 | 3 | adantr 472 |
. . . . . . . . . . 11
                |
5 | | elmapg 7503 |
. . . . . . . . . . 11
 
           |
6 | 2, 4, 5 | sylancr 676 |
. . . . . . . . . 10
                
       |
7 | 1, 6 | mpbid 215 |
. . . . . . . . 9
                    |
8 | 7 | adantr 472 |
. . . . . . . 8
   
   
                         
      |
9 | | simp2 1031 |
. . . . . . . . . 10
      
  
      |
10 | | f1f 5792 |
. . . . . . . . . 10
           |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
      
  
      |
12 | 11 | ad2antrr 740 |
. . . . . . . 8
   
   
                         
      |
13 | | fco 5751 |
. . . . . . . 8
                   |
14 | 8, 12, 13 | syl2anc 673 |
. . . . . . 7
   
   
                         
        |
15 | | f1dmex 6782 |
. . . . . . . . . 10
     
   |
16 | 9, 3, 15 | syl2anc 673 |
. . . . . . . . 9
      
  
  |
17 | 16 | ad2antrr 740 |
. . . . . . . 8
   
   
                         
  |
18 | | elmapg 7503 |
. . . . . . . 8
 
               |
19 | 2, 17, 18 | sylancr 676 |
. . . . . . 7
   
   
                         
    
         |
20 | 14, 19 | mpbird 240 |
. . . . . 6
   
   
                         
      |
21 | | simprl 772 |
. . . . . . 7
   
   
                         
    |
22 | | resco 5346 |
. . . . . . . 8
         |
23 | | simpll3 1071 |
. . . . . . . . . 10
   
   
                         
 
   |
24 | 23 | coeq2d 5002 |
. . . . . . . . 9
   
   
                         
         |
25 | | coires1 5360 |
. . . . . . . . 9
      |
26 | 24, 25 | syl6eq 2521 |
. . . . . . . 8
   
   
                         
        |
27 | 22, 26 | syl5eq 2517 |
. . . . . . 7
   
   
                         
    
   |
28 | 21, 27 | eqtr4d 2508 |
. . . . . 6
   
   
                         
      |
29 | | simpll1 1069 |
. . . . . . . . . 10
   
   
                         
  |
30 | | oveq2 6316 |
. . . . . . . . . . . 12
       |
31 | | oveq2 6316 |
. . . . . . . . . . . 12
       |
32 | 30, 31 | sseq12d 3447 |
. . . . . . . . . . 11
  

 
       |
33 | | zex 10970 |
. . . . . . . . . . . 12
 |
34 | | nn0ssz 10982 |
. . . . . . . . . . . 12
 |
35 | | mapss 7532 |
. . . . . . . . . . . 12
     
   |
36 | 33, 34, 35 | mp2an 686 |
. . . . . . . . . . 11
  
  |
37 | 32, 36 | vtoclg 3093 |
. . . . . . . . . 10
   
   |
38 | 29, 37 | syl 17 |
. . . . . . . . 9
   
   
                         
      |
39 | | simplr 770 |
. . . . . . . . 9
   
   
                         
    |
40 | 38, 39 | sseldd 3419 |
. . . . . . . 8
   
   
                         

   |
41 | | coeq1 4997 |
. . . . . . . . . 10
       |
42 | 41 | fveq2d 5883 |
. . . . . . . . 9
               |
43 | | eqid 2471 |
. . . . . . . . 9
                     |
44 | | fvex 5889 |
. . . . . . . . 9
       |
45 | 42, 43, 44 | fvmpt 5963 |
. . . . . . . 8
                         |
46 | 40, 45 | syl 17 |
. . . . . . 7
   
   
                         
                      |
47 | | simprr 774 |
. . . . . . 7
   
   
                         
                |
48 | 46, 47 | eqtr3d 2507 |
. . . . . 6
   
   
                         
        |
49 | | reseq1 5105 |
. . . . . . . . 9
           |
50 | 49 | eqeq2d 2481 |
. . . . . . . 8
     
       |
51 | | fveq2 5879 |
. . . . . . . . 9
               |
52 | 51 | eqeq1d 2473 |
. . . . . . . 8
                 |
53 | 50, 52 | anbi12d 725 |
. . . . . . 7
     
                     |
54 | 53 | rspcev 3136 |
. . . . . 6
                        
        |
55 | 20, 28, 48, 54 | syl12anc 1290 |
. . . . 5
   
   
                         
              |
56 | 55 | ex 441 |
. . . 4
                
               
               |
57 | 56 | rexlimdva 2871 |
. . 3
      
  
 
                          
         |
58 | | simpr 468 |
. . . . . . . . . . . 12
                  |
59 | 16 | adantr 472 |
. . . . . . . . . . . . 13
                |
60 | | elmapg 7503 |
. . . . . . . . . . . . 13
 
           |
61 | 2, 59, 60 | sylancr 676 |
. . . . . . . . . . . 12
                
       |
62 | 58, 61 | mpbid 215 |
. . . . . . . . . . 11
                    |
63 | 62 | adantr 472 |
. . . . . . . . . 10
   
   
                      |
64 | 9 | ad2antrr 740 |
. . . . . . . . . . 11
   
   
                      |
65 | | f1cnv 5851 |
. . . . . . . . . . 11
            |
66 | | f1of 5828 |
. . . . . . . . . . 11
             |
67 | 64, 65, 66 | 3syl 18 |
. . . . . . . . . 10
   
   
                       |
68 | | fco 5751 |
. . . . . . . . . 10
                     |
69 | 63, 67, 68 | syl2anc 673 |
. . . . . . . . 9
   
   
                         |
70 | | c0ex 9655 |
. . . . . . . . . . 11
 |
71 | 70 | fconst 5782 |
. . . . . . . . . 10
               |
72 | 71 | a1i 11 |
. . . . . . . . 9
   
   
                 
              |
73 | | disjdif 3830 |
. . . . . . . . . 10

    |
74 | 73 | a1i 11 |
. . . . . . . . 9
   
   
                      |
75 | | fun 5758 |
. . . . . . . . 9
                         
                  
          |
76 | 69, 72, 74, 75 | syl21anc 1291 |
. . . . . . . 8
   
   
                     
        
          |
77 | | frn 5747 |
. . . . . . . . . . . 12
    
  |
78 | 9, 10, 77 | 3syl 18 |
. . . . . . . . . . 11
      
  
  |
79 | 78 | ad2antrr 740 |
. . . . . . . . . 10
   
   
               
  |
80 | | undif 3839 |
. . . . . . . . . 10

      |
81 | 79, 80 | sylib 201 |
. . . . . . . . 9
   
   
                      |
82 | | 0nn0 10908 |
. . . . . . . . . . . 12
 |
83 | | snssi 4107 |
. . . . . . . . . . . 12

 
  |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . . . 11
 
 |
85 | | ssequn2 3598 |
. . . . . . . . . . 11
  
      |
86 | 84, 85 | mpbi 213 |
. . . . . . . . . 10
     |
87 | 86 | a1i 11 |
. . . . . . . . 9
   
   
                      |
88 | 81, 87 | feq23d 5734 |
. . . . . . . 8
   
   
                               
             
            |
89 | 76, 88 | mpbid 215 |
. . . . . . 7
   
   
                     
           |
90 | | elmapg 7503 |
. . . . . . . . 9
 
       
      
                  |
91 | 2, 3, 90 | sylancr 676 |
. . . . . . . 8
      
  
                   
            |
92 | 91 | ad2antrr 740 |
. . . . . . 7
   
   
                                   
            |
93 | 89, 92 | mpbird 240 |
. . . . . 6
   
   
                     
         |
94 | | simprl 772 |
. . . . . . 7
   
   
                
   |
95 | | resundir 5125 |
. . . . . . . . . 10
                             |
96 | | resco 5346 |
. . . . . . . . . . . 12
       
   |
97 | | cnvresid 5663 |
. . . . . . . . . . . . . . 15


  |
98 | | simpl2 1034 |
. . . . . . . . . . . . . . . . 17
                    |
99 | | df-f1 5594 |
. . . . . . . . . . . . . . . . . 18
    
         |
100 | 99 | simprbi 471 |
. . . . . . . . . . . . . . . . 17
        |
101 | | funcnvres 5662 |
. . . . . . . . . . . . . . . . 17
 
 
          |
102 | 98, 100, 101 | 3syl 18 |
. . . . . . . . . . . . . . . 16
               
          |
103 | | simpl3 1035 |
. . . . . . . . . . . . . . . . 17
                   |
104 | 103 | cnveqd 5015 |
. . . . . . . . . . . . . . . 16
               
     |
105 | | df-ima 4852 |
. . . . . . . . . . . . . . . . . 18
       |
106 | 103 | rneqd 5068 |
. . . . . . . . . . . . . . . . . . 19
              
    |
107 | | rnresi 5187 |
. . . . . . . . . . . . . . . . . . 19
  |
108 | 106, 107 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . 18
              
   |
109 | 105, 108 | syl5eq 2517 |
. . . . . . . . . . . . . . . . 17
                    |
110 | 109 | reseq2d 5111 |
. . . . . . . . . . . . . . . 16
               
          |
111 | 102, 104,
110 | 3eqtr3d 2513 |
. . . . . . . . . . . . . . 15
              
      |
112 | 97, 111 | syl5reqr 2520 |
. . . . . . . . . . . . . 14
               
    |
113 | 112 | coeq2d 5002 |
. . . . . . . . . . . . 13
                
       |
114 | | coires1 5360 |
. . . . . . . . . . . . 13
      |
115 | 113, 114 | syl6eq 2521 |
. . . . . . . . . . . 12
                
      |
116 | 96, 115 | syl5eq 2517 |
. . . . . . . . . . 11
                       |
117 | | dmres 5131 |
. . . . . . . . . . . . 13
                 |
118 | 70 | snnz 4081 |
. . . . . . . . . . . . . . . 16
   |
119 | | dmxp 5059 |
. . . . . . . . . . . . . . . 16
             |
120 | 118, 119 | ax-mp 5 |
. . . . . . . . . . . . . . 15
         |
121 | 120 | ineq2i 3622 |
. . . . . . . . . . . . . 14

        
   |
122 | | inss1 3643 |
. . . . . . . . . . . . . . . 16
   |
123 | 106, 107 | syl6req 2522 |
. . . . . . . . . . . . . . . . 17
                  |
124 | | resss 5134 |
. . . . . . . . . . . . . . . . . 18
   |
125 | | rnss 5069 |
. . . . . . . . . . . . . . . . . 18
 

    |
126 | 124, 125 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
              

  |
127 | 123, 126 | eqsstrd 3452 |
. . . . . . . . . . . . . . . 16
                |
128 | 122, 127 | syl5ss 3429 |
. . . . . . . . . . . . . . 15
                  |
129 | | inssdif0 3746 |
. . . . . . . . . . . . . . 15
  
      |
130 | 128, 129 | sylib 201 |
. . . . . . . . . . . . . 14
                    |
131 | 121, 130 | syl5eq 2517 |
. . . . . . . . . . . . 13
              
         |
132 | 117, 131 | syl5eq 2517 |
. . . . . . . . . . . 12
                
       |
133 | | relres 5138 |
. . . . . . . . . . . . 13
         |
134 | | reldm0 5058 |
. . . . . . . . . . . . 13
   
        
       
        |
135 | 133, 134 | ax-mp 5 |
. . . . . . . . . . . 12
           
       |
136 | 132, 135 | sylibr 217 |
. . . . . . . . . . 11
                        |
137 | 116, 136 | uneq12d 3580 |
. . . . . . . . . 10
                              
    |
138 | 95, 137 | syl5eq 2517 |
. . . . . . . . 9
                                 |
139 | | un0 3762 |
. . . . . . . . 9
 
  
  |
140 | 138, 139 | syl6req 2522 |
. . . . . . . 8
                      
    
   |
141 | 140 | adantr 472 |
. . . . . . 7
   
   
                                 |
142 | 94, 141 | eqtrd 2505 |
. . . . . 6
   
   
                               |
143 | | fss 5749 |
. . . . . . . . . . . . . 14
             |
144 | 62, 34, 143 | sylancl 675 |
. . . . . . . . . . . . 13
                    |
145 | 144 | adantr 472 |
. . . . . . . . . . . 12
   
   
                      |
146 | | fco 5751 |
. . . . . . . . . . . 12
                     |
147 | 145, 67, 146 | syl2anc 673 |
. . . . . . . . . . 11
   
   
                         |
148 | | fun 5758 |
. . . . . . . . . . 11
                         
                  
          |
149 | 147, 72, 74, 148 | syl21anc 1291 |
. . . . . . . . . 10
   
   
                     
        
          |
150 | | 0z 10972 |
. . . . . . . . . . . . . 14
 |
151 | | snssi 4107 |
. . . . . . . . . . . . . 14
  
  |
152 | 150, 151 | ax-mp 5 |
. . . . . . . . . . . . 13
 
 |
153 | | ssequn2 3598 |
. . . . . . . . . . . . 13
         |
154 | 152, 153 | mpbi 213 |
. . . . . . . . . . . 12
     |
155 | 154 | a1i 11 |
. . . . . . . . . . 11
   
   
                      |
156 | 81, 155 | feq23d 5734 |
. . . . . . . . . 10
   
   
                               
             
            |
157 | 149, 156 | mpbid 215 |
. . . . . . . . 9
   
   
                     
           |
158 | | elmapg 7503 |
. . . . . . . . . . 11
 
       
      
                  |
159 | 33, 3, 158 | sylancr 676 |
. . . . . . . . . 10
      
  
                   
            |
160 | 159 | ad2antrr 740 |
. . . . . . . . 9
   
   
                                   
            |
161 | 157, 160 | mpbird 240 |
. . . . . . . 8
   
   
                     
         |
162 | | coeq1 4997 |
. . . . . . . . . 10
      
    
                 |
163 | 162 | fveq2d 5883 |
. . . . . . . . 9
      
    
                         |
164 | | fvex 5889 |
. . . . . . . . 9
                  |
165 | 163, 43, 164 | fvmpt 5963 |
. . . . . . . 8
             
                                  
         |
166 | 161, 165 | syl 17 |
. . . . . . 7
   
   
                                  
                         |
167 | | coundir 5344 |
. . . . . . . . 9
                             |
168 | | coass 5361 |
. . . . . . . . . . . 12
           |
169 | | f1cocnv1 5857 |
. . . . . . . . . . . . . 14
       
   |
170 | 169 | coeq2d 5002 |
. . . . . . . . . . . . 13
       
       |
171 | 64, 170 | syl 17 |
. . . . . . . . . . . 12
   
   
                          |
172 | 168, 171 | syl5eq 2517 |
. . . . . . . . . . 11
   
   
                          |
173 | 120 | ineq1i 3621 |
. . . . . . . . . . . . . 14
             |
174 | | incom 3616 |
. . . . . . . . . . . . . 14
  
      |
175 | 173, 174,
73 | 3eqtri 2497 |
. . . . . . . . . . . . 13
         |
176 | | coeq0 5351 |
. . . . . . . . . . . . 13
                   |
177 | 175, 176 | mpbir 214 |
. . . . . . . . . . . 12
         |
178 | 177 | a1i 11 |
. . . . . . . . . . 11
   
   
                          |
179 | 172, 178 | uneq12d 3580 |
. . . . . . . . . 10
   
   
                                      |
180 | | un0 3762 |
. . . . . . . . . . 11
    
    |
181 | | fcoi1 5769 |
. . . . . . . . . . . 12
          |
182 | 63, 181 | syl 17 |
. . . . . . . . . . 11
   
   
                     |
183 | 180, 182 | syl5eq 2517 |
. . . . . . . . . 10
   
   
                       |
184 | 179, 183 | eqtrd 2505 |
. . . . . . . . 9
   
   
                                 |
185 | 167, 184 | syl5eq 2517 |
. . . . . . . 8
   
   
                               |
186 | 185 | fveq2d 5883 |
. . . . . . 7
   
   
                         
             |
187 | | simprr 774 |
. . . . . . 7
   
   
                      |
188 | 166, 186,
187 | 3eqtrd 2509 |
. . . . . 6
   
   
                                  
        |
189 | | reseq1 5105 |
. . . . . . . . 9
      
    
                 |
190 | 189 | eqeq2d 2481 |
. . . . . . . 8
      
    
  
      
    
    |
191 | | fveq2 5879 |
. . . . . . . . 9
      
    
                                
        |
192 | 191 | eqeq1d 2473 |
. . . . . . . 8
      
    
                                           |
193 | 190, 192 | anbi12d 725 |
. . . . . . 7
      
    
                                                              |
194 | 193 | rspcev 3136 |
. . . . . 6
              
                                              
                  |
195 | 93, 142, 188, 194 | syl12anc 1290 |
. . . . 5
   
   
                     
                  |
196 | 195 | ex 441 |
. . . 4
                
           
                   |
197 | 196 | rexlimdva 2871 |
. . 3
      
  
 
           
                        |
198 | 57, 197 | impbid 195 |
. 2
      
  
 
                     
              |
199 | 198 | abbidv 2589 |
1
      
  
      
                                 |