Proof of Theorem diophrw
Step | Hyp | Ref
| Expression |
1 | | simpr 463 |
. . . . . . . . . 10
                  |
2 | | nn0ex 10875 |
. . . . . . . . . . 11
 |
3 | | simp1 1008 |
. . . . . . . . . . . 12
      
  
  |
4 | 3 | adantr 467 |
. . . . . . . . . . 11
                |
5 | | elmapg 7485 |
. . . . . . . . . . 11
 
           |
6 | 2, 4, 5 | sylancr 669 |
. . . . . . . . . 10
                
       |
7 | 1, 6 | mpbid 214 |
. . . . . . . . 9
                    |
8 | 7 | adantr 467 |
. . . . . . . 8
   
   
                         
      |
9 | | simp2 1009 |
. . . . . . . . . 10
      
  
      |
10 | | f1f 5779 |
. . . . . . . . . 10
           |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
      
  
      |
12 | 11 | ad2antrr 732 |
. . . . . . . 8
   
   
                         
      |
13 | | fco 5739 |
. . . . . . . 8
                   |
14 | 8, 12, 13 | syl2anc 667 |
. . . . . . 7
   
   
                         
        |
15 | | f1dmex 6763 |
. . . . . . . . . 10
     
   |
16 | 9, 3, 15 | syl2anc 667 |
. . . . . . . . 9
      
  
  |
17 | 16 | ad2antrr 732 |
. . . . . . . 8
   
   
                         
  |
18 | | elmapg 7485 |
. . . . . . . 8
 
               |
19 | 2, 17, 18 | sylancr 669 |
. . . . . . 7
   
   
                         
    
         |
20 | 14, 19 | mpbird 236 |
. . . . . 6
   
   
                         
      |
21 | | simprl 764 |
. . . . . . 7
   
   
                         
    |
22 | | resco 5339 |
. . . . . . . 8
         |
23 | | simpll3 1049 |
. . . . . . . . . 10
   
   
                         
 
   |
24 | 23 | coeq2d 4997 |
. . . . . . . . 9
   
   
                         
         |
25 | | coires1 5353 |
. . . . . . . . 9
      |
26 | 24, 25 | syl6eq 2501 |
. . . . . . . 8
   
   
                         
        |
27 | 22, 26 | syl5eq 2497 |
. . . . . . 7
   
   
                         
    
   |
28 | 21, 27 | eqtr4d 2488 |
. . . . . 6
   
   
                         
      |
29 | | simpll1 1047 |
. . . . . . . . . 10
   
   
                         
  |
30 | | oveq2 6298 |
. . . . . . . . . . . 12
       |
31 | | oveq2 6298 |
. . . . . . . . . . . 12
       |
32 | 30, 31 | sseq12d 3461 |
. . . . . . . . . . 11
  

 
       |
33 | | zex 10946 |
. . . . . . . . . . . 12
 |
34 | | nn0ssz 10958 |
. . . . . . . . . . . 12
 |
35 | | mapss 7514 |
. . . . . . . . . . . 12
     
   |
36 | 33, 34, 35 | mp2an 678 |
. . . . . . . . . . 11
  
  |
37 | 32, 36 | vtoclg 3107 |
. . . . . . . . . 10
   
   |
38 | 29, 37 | syl 17 |
. . . . . . . . 9
   
   
                         
      |
39 | | simplr 762 |
. . . . . . . . 9
   
   
                         
    |
40 | 38, 39 | sseldd 3433 |
. . . . . . . 8
   
   
                         

   |
41 | | coeq1 4992 |
. . . . . . . . . 10
       |
42 | 41 | fveq2d 5869 |
. . . . . . . . 9
               |
43 | | eqid 2451 |
. . . . . . . . 9
                     |
44 | | fvex 5875 |
. . . . . . . . 9
       |
45 | 42, 43, 44 | fvmpt 5948 |
. . . . . . . 8
                         |
46 | 40, 45 | syl 17 |
. . . . . . 7
   
   
                         
                      |
47 | | simprr 766 |
. . . . . . 7
   
   
                         
                |
48 | 46, 47 | eqtr3d 2487 |
. . . . . 6
   
   
                         
        |
49 | | reseq1 5099 |
. . . . . . . . 9
           |
50 | 49 | eqeq2d 2461 |
. . . . . . . 8
     
       |
51 | | fveq2 5865 |
. . . . . . . . 9
               |
52 | 51 | eqeq1d 2453 |
. . . . . . . 8
                 |
53 | 50, 52 | anbi12d 717 |
. . . . . . 7
     
                     |
54 | 53 | rspcev 3150 |
. . . . . 6
                        
        |
55 | 20, 28, 48, 54 | syl12anc 1266 |
. . . . 5
   
   
                         
              |
56 | 55 | ex 436 |
. . . 4
                
               
               |
57 | 56 | rexlimdva 2879 |
. . 3
      
  
 
                          
         |
58 | | simpr 463 |
. . . . . . . . . . . 12
                  |
59 | 16 | adantr 467 |
. . . . . . . . . . . . 13
                |
60 | | elmapg 7485 |
. . . . . . . . . . . . 13
 
           |
61 | 2, 59, 60 | sylancr 669 |
. . . . . . . . . . . 12
                
       |
62 | 58, 61 | mpbid 214 |
. . . . . . . . . . 11
                    |
63 | 62 | adantr 467 |
. . . . . . . . . 10
   
   
                      |
64 | 9 | ad2antrr 732 |
. . . . . . . . . . 11
   
   
                      |
65 | | f1cnv 5837 |
. . . . . . . . . . 11
            |
66 | | f1of 5814 |
. . . . . . . . . . 11
             |
67 | 64, 65, 66 | 3syl 18 |
. . . . . . . . . 10
   
   
                       |
68 | | fco 5739 |
. . . . . . . . . 10
                     |
69 | 63, 67, 68 | syl2anc 667 |
. . . . . . . . 9
   
   
                         |
70 | | c0ex 9637 |
. . . . . . . . . . 11
 |
71 | 70 | fconst 5769 |
. . . . . . . . . 10
               |
72 | 71 | a1i 11 |
. . . . . . . . 9
   
   
                 
              |
73 | | disjdif 3839 |
. . . . . . . . . 10

    |
74 | 73 | a1i 11 |
. . . . . . . . 9
   
   
                      |
75 | | fun 5746 |
. . . . . . . . 9
                         
                  
          |
76 | 69, 72, 74, 75 | syl21anc 1267 |
. . . . . . . 8
   
   
                     
        
          |
77 | | frn 5735 |
. . . . . . . . . . . 12
    
  |
78 | 9, 10, 77 | 3syl 18 |
. . . . . . . . . . 11
      
  
  |
79 | 78 | ad2antrr 732 |
. . . . . . . . . 10
   
   
               
  |
80 | | undif 3848 |
. . . . . . . . . 10

      |
81 | 79, 80 | sylib 200 |
. . . . . . . . 9
   
   
                      |
82 | | 0nn0 10884 |
. . . . . . . . . . . 12
 |
83 | | snssi 4116 |
. . . . . . . . . . . 12

 
  |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . . . 11
 
 |
85 | | ssequn2 3607 |
. . . . . . . . . . 11
  
      |
86 | 84, 85 | mpbi 212 |
. . . . . . . . . 10
     |
87 | 86 | a1i 11 |
. . . . . . . . 9
   
   
                      |
88 | 81, 87 | feq23d 5723 |
. . . . . . . 8
   
   
                               
             
            |
89 | 76, 88 | mpbid 214 |
. . . . . . 7
   
   
                     
           |
90 | | elmapg 7485 |
. . . . . . . . 9
 
       
      
                  |
91 | 2, 3, 90 | sylancr 669 |
. . . . . . . 8
      
  
                   
            |
92 | 91 | ad2antrr 732 |
. . . . . . 7
   
   
                                   
            |
93 | 89, 92 | mpbird 236 |
. . . . . 6
   
   
                     
         |
94 | | simprl 764 |
. . . . . . 7
   
   
                
   |
95 | | resundir 5119 |
. . . . . . . . . 10
                             |
96 | | resco 5339 |
. . . . . . . . . . . 12
       
   |
97 | | cnvresid 5653 |
. . . . . . . . . . . . . . 15


  |
98 | | simpl2 1012 |
. . . . . . . . . . . . . . . . 17
                    |
99 | | df-f1 5587 |
. . . . . . . . . . . . . . . . . 18
    
         |
100 | 99 | simprbi 466 |
. . . . . . . . . . . . . . . . 17
        |
101 | | funcnvres 5652 |
. . . . . . . . . . . . . . . . 17
 
 
          |
102 | 98, 100, 101 | 3syl 18 |
. . . . . . . . . . . . . . . 16
               
          |
103 | | simpl3 1013 |
. . . . . . . . . . . . . . . . 17
                   |
104 | 103 | cnveqd 5010 |
. . . . . . . . . . . . . . . 16
               
     |
105 | | df-ima 4847 |
. . . . . . . . . . . . . . . . . 18
       |
106 | 103 | rneqd 5062 |
. . . . . . . . . . . . . . . . . . 19
              
    |
107 | | rnresi 5181 |
. . . . . . . . . . . . . . . . . . 19
  |
108 | 106, 107 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . 18
              
   |
109 | 105, 108 | syl5eq 2497 |
. . . . . . . . . . . . . . . . 17
                    |
110 | 109 | reseq2d 5105 |
. . . . . . . . . . . . . . . 16
               
          |
111 | 102, 104,
110 | 3eqtr3d 2493 |
. . . . . . . . . . . . . . 15
              
      |
112 | 97, 111 | syl5reqr 2500 |
. . . . . . . . . . . . . 14
               
    |
113 | 112 | coeq2d 4997 |
. . . . . . . . . . . . 13
                
       |
114 | | coires1 5353 |
. . . . . . . . . . . . 13
      |
115 | 113, 114 | syl6eq 2501 |
. . . . . . . . . . . 12
                
      |
116 | 96, 115 | syl5eq 2497 |
. . . . . . . . . . 11
                       |
117 | | dmres 5125 |
. . . . . . . . . . . . 13
                 |
118 | 70 | snnz 4090 |
. . . . . . . . . . . . . . . 16
   |
119 | | dmxp 5053 |
. . . . . . . . . . . . . . . 16
             |
120 | 118, 119 | ax-mp 5 |
. . . . . . . . . . . . . . 15
         |
121 | 120 | ineq2i 3631 |
. . . . . . . . . . . . . 14

        
   |
122 | | inss1 3652 |
. . . . . . . . . . . . . . . 16
   |
123 | 106, 107 | syl6req 2502 |
. . . . . . . . . . . . . . . . 17
                  |
124 | | resss 5128 |
. . . . . . . . . . . . . . . . . 18
   |
125 | | rnss 5063 |
. . . . . . . . . . . . . . . . . 18
 

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

  |
127 | 123, 126 | eqsstrd 3466 |
. . . . . . . . . . . . . . . 16
                |
128 | 122, 127 | syl5ss 3443 |
. . . . . . . . . . . . . . 15
                  |
129 | | inssdif0 3834 |
. . . . . . . . . . . . . . 15
  
      |
130 | 128, 129 | sylib 200 |
. . . . . . . . . . . . . 14
                    |
131 | 121, 130 | syl5eq 2497 |
. . . . . . . . . . . . 13
              
         |
132 | 117, 131 | syl5eq 2497 |
. . . . . . . . . . . 12
                
       |
133 | | relres 5132 |
. . . . . . . . . . . . 13
         |
134 | | reldm0 5052 |
. . . . . . . . . . . . 13
   
        
       
        |
135 | 133, 134 | ax-mp 5 |
. . . . . . . . . . . 12
           
       |
136 | 132, 135 | sylibr 216 |
. . . . . . . . . . 11
                        |
137 | 116, 136 | uneq12d 3589 |
. . . . . . . . . 10
                              
    |
138 | 95, 137 | syl5eq 2497 |
. . . . . . . . 9
                                 |
139 | | un0 3759 |
. . . . . . . . 9
 
  
  |
140 | 138, 139 | syl6req 2502 |
. . . . . . . 8
                      
    
   |
141 | 140 | adantr 467 |
. . . . . . 7
   
   
                                 |
142 | 94, 141 | eqtrd 2485 |
. . . . . 6
   
   
                               |
143 | | fss 5737 |
. . . . . . . . . . . . . 14
             |
144 | 62, 34, 143 | sylancl 668 |
. . . . . . . . . . . . 13
                    |
145 | 144 | adantr 467 |
. . . . . . . . . . . 12
   
   
                      |
146 | | fco 5739 |
. . . . . . . . . . . 12
                     |
147 | 145, 67, 146 | syl2anc 667 |
. . . . . . . . . . 11
   
   
                         |
148 | | fun 5746 |
. . . . . . . . . . 11
                         
                  
          |
149 | 147, 72, 74, 148 | syl21anc 1267 |
. . . . . . . . . 10
   
   
                     
        
          |
150 | | 0z 10948 |
. . . . . . . . . . . . . 14
 |
151 | | snssi 4116 |
. . . . . . . . . . . . . 14
  
  |
152 | 150, 151 | ax-mp 5 |
. . . . . . . . . . . . 13
 
 |
153 | | ssequn2 3607 |
. . . . . . . . . . . . 13
         |
154 | 152, 153 | mpbi 212 |
. . . . . . . . . . . 12
     |
155 | 154 | a1i 11 |
. . . . . . . . . . 11
   
   
                      |
156 | 81, 155 | feq23d 5723 |
. . . . . . . . . 10
   
   
                               
             
            |
157 | 149, 156 | mpbid 214 |
. . . . . . . . 9
   
   
                     
           |
158 | | elmapg 7485 |
. . . . . . . . . . 11
 
       
      
                  |
159 | 33, 3, 158 | sylancr 669 |
. . . . . . . . . 10
      
  
                   
            |
160 | 159 | ad2antrr 732 |
. . . . . . . . 9
   
   
                                   
            |
161 | 157, 160 | mpbird 236 |
. . . . . . . 8
   
   
                     
         |
162 | | coeq1 4992 |
. . . . . . . . . 10
      
    
                 |
163 | 162 | fveq2d 5869 |
. . . . . . . . 9
      
    
                         |
164 | | fvex 5875 |
. . . . . . . . 9
                  |
165 | 163, 43, 164 | fvmpt 5948 |
. . . . . . . 8
             
                                  
         |
166 | 161, 165 | syl 17 |
. . . . . . 7
   
   
                                  
                         |
167 | | coundir 5337 |
. . . . . . . . 9
                             |
168 | | coass 5354 |
. . . . . . . . . . . 12
           |
169 | | f1cocnv1 5843 |
. . . . . . . . . . . . . 14
       
   |
170 | 169 | coeq2d 4997 |
. . . . . . . . . . . . 13
       
       |
171 | 64, 170 | syl 17 |
. . . . . . . . . . . 12
   
   
                          |
172 | 168, 171 | syl5eq 2497 |
. . . . . . . . . . 11
   
   
                          |
173 | 120 | ineq1i 3630 |
. . . . . . . . . . . . . 14
             |
174 | | incom 3625 |
. . . . . . . . . . . . . 14
  
      |
175 | 173, 174,
73 | 3eqtri 2477 |
. . . . . . . . . . . . 13
         |
176 | | coeq0 5344 |
. . . . . . . . . . . . 13
                   |
177 | 175, 176 | mpbir 213 |
. . . . . . . . . . . 12
         |
178 | 177 | a1i 11 |
. . . . . . . . . . 11
   
   
                          |
179 | 172, 178 | uneq12d 3589 |
. . . . . . . . . 10
   
   
                                      |
180 | | un0 3759 |
. . . . . . . . . . 11
    
    |
181 | | fcoi1 5757 |
. . . . . . . . . . . 12
          |
182 | 63, 181 | syl 17 |
. . . . . . . . . . 11
   
   
                     |
183 | 180, 182 | syl5eq 2497 |
. . . . . . . . . 10
   
   
                       |
184 | 179, 183 | eqtrd 2485 |
. . . . . . . . 9
   
   
                                 |
185 | 167, 184 | syl5eq 2497 |
. . . . . . . 8
   
   
                               |
186 | 185 | fveq2d 5869 |
. . . . . . 7
   
   
                         
             |
187 | | simprr 766 |
. . . . . . 7
   
   
                      |
188 | 166, 186,
187 | 3eqtrd 2489 |
. . . . . 6
   
   
                                  
        |
189 | | reseq1 5099 |
. . . . . . . . 9
      
    
                 |
190 | 189 | eqeq2d 2461 |
. . . . . . . 8
      
    
  
      
    
    |
191 | | fveq2 5865 |
. . . . . . . . 9
      
    
                                
        |
192 | 191 | eqeq1d 2453 |
. . . . . . . 8
      
    
                                           |
193 | 190, 192 | anbi12d 717 |
. . . . . . 7
      
    
                                                              |
194 | 193 | rspcev 3150 |
. . . . . 6
              
                                              
                  |
195 | 93, 142, 188, 194 | syl12anc 1266 |
. . . . 5
   
   
                     
                  |
196 | 195 | ex 436 |
. . . 4
                
           
                   |
197 | 196 | rexlimdva 2879 |
. . 3
      
  
 
           
                        |
198 | 57, 197 | impbid 194 |
. 2
      
  
 
                     
              |
199 | 198 | abbidv 2569 |
1
      
  
      
                                 |