Step | Hyp | Ref
| Expression |
1 | | reex 9648 |
. . . . . . 7
 |
2 | | mapdm0 37542 |
. . . . . . 7
       |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
     |
4 | 3 | a1i 11 |
. . . . 5

      |
5 | | oveq2 6316 |
. . . . 5

      |
6 | | ixpeq1 7551 |
. . . . . . 7


          
            |
7 | 6 | iuneq2d 4296 |
. . . . . 6

                          |
8 | | ixp0x 7568 |
. . . . . . . . . 10
              |
9 | 8 | a1i 11 |
. . . . . . . . 9
                |
10 | 9 | iuneq2i 4288 |
. . . . . . . 8
                |
11 | | 1nn 10642 |
. . . . . . . . . 10
 |
12 | 11 | ne0ii 3729 |
. . . . . . . . 9
 |
13 | | iunconst 4278 |
. . . . . . . . 9

       |
14 | 12, 13 | ax-mp 5 |
. . . . . . . 8
      |
15 | 10, 14 | eqtri 2493 |
. . . . . . 7
               |
16 | 15 | a1i 11 |
. . . . . 6

                |
17 | 7, 16 | eqtrd 2505 |
. . . . 5

                |
18 | 4, 5, 17 | 3eqtr4d 2515 |
. . . 4

                |
19 | | eqimss 3470 |
. . . 4
              
                |
20 | 18, 19 | syl 17 |
. . 3

   
 
          |
21 | 20 | adantl 473 |
. 2
 

                |
22 | | simpll 768 |
. . . . . 6
  

     |
23 | | simpr 468 |
. . . . . 6
  

       |
24 | | simplr 770 |
. . . . . 6
  

  
  |
25 | | rncoss 5101 |
. . . . . . . . . . 11
   |
26 | | absf 13477 |
. . . . . . . . . . . 12
     |
27 | | frn 5747 |
. . . . . . . . . . . 12
       |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . 11
 |
29 | 25, 28 | sstri 3427 |
. . . . . . . . . 10
   |
30 | 29 | a1i 11 |
. . . . . . . . 9
     
  
  |
31 | | ltso 9732 |
. . . . . . . . . . 11
 |
32 | 31 | a1i 11 |
. . . . . . . . . 10
     
   |
33 | 26 | a1i 11 |
. . . . . . . . . . . . 13
 

 
      |
34 | | elmapi 7511 |
. . . . . . . . . . . . . . 15
         |
35 | 34 | adantl 473 |
. . . . . . . . . . . . . 14
 

 
      |
36 | | ax-resscn 9614 |
. . . . . . . . . . . . . . 15
 |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
 

 
  |
38 | 35, 37 | fssd 5750 |
. . . . . . . . . . . . 13
 

 
      |
39 | | fco 5751 |
. . . . . . . . . . . . 13
                   |
40 | 33, 38, 39 | syl2anc 673 |
. . . . . . . . . . . 12
 

 
        |
41 | | hoicvr.3 |
. . . . . . . . . . . . 13
   |
42 | 41 | adantr 472 |
. . . . . . . . . . . 12
 

 
  |
43 | | rnffi 37513 |
. . . . . . . . . . . 12
       
     |
44 | 40, 42, 43 | syl2anc 673 |
. . . . . . . . . . 11
 

 
    |
45 | 44 | adantr 472 |
. . . . . . . . . 10
     
     |
46 | | frn 5747 |
. . . . . . . . . . . . . . . . . . . 20
    
  |
47 | 34, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
     |
48 | 26 | fdmi 5746 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
49 | 48 | eqcomi 2480 |
. . . . . . . . . . . . . . . . . . . . 21
 |
50 | 36, 49 | sseqtri 3450 |
. . . . . . . . . . . . . . . . . . . 20
 |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
     |
52 | 47, 51 | sstrd 3428 |
. . . . . . . . . . . . . . . . . 18
     |
53 | | dmcosseq 5102 |
. . . . . . . . . . . . . . . . . 18

    |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
55 | | fdm 5745 |
. . . . . . . . . . . . . . . . . 18
       |
56 | 34, 55 | syl 17 |
. . . . . . . . . . . . . . . . 17
  
  |
57 | 54, 56 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
       |
58 | 57 | adantr 472 |
. . . . . . . . . . . . . . 15
   
     |
59 | | neqne 2651 |
. . . . . . . . . . . . . . . 16
   |
60 | 59 | adantl 473 |
. . . . . . . . . . . . . . 15
   
   |
61 | 58, 60 | eqnetrd 2710 |
. . . . . . . . . . . . . 14
   
     |
62 | 61 | neneqd 2648 |
. . . . . . . . . . . . 13
   
     |
63 | | dm0rn0 5057 |
. . . . . . . . . . . . 13
  
    |
64 | 62, 63 | sylnib 311 |
. . . . . . . . . . . 12
   
     |
65 | 64 | neqned 2650 |
. . . . . . . . . . 11
   
     |
66 | 65 | adantll 728 |
. . . . . . . . . 10
     
     |
67 | | fisupcl 8003 |
. . . . . . . . . 10
                    |
68 | 32, 45, 66, 30, 67 | syl13anc 1294 |
. . . . . . . . 9
     
           |
69 | 30, 68 | sseldd 3419 |
. . . . . . . 8
     
         |
70 | | arch 10890 |
. . . . . . . 8
      
         |
71 | 69, 70 | syl 17 |
. . . . . . 7
     
 
        |
72 | 35 | ffnd 5740 |
. . . . . . . . . . . . 13
 

 
  |
73 | 72 | ad2antrr 740 |
. . . . . . . . . . . 12
   
  
          |
74 | 73 | adantlr 729 |
. . . . . . . . . . 11
        
       
  |
75 | | simplll 776 |
. . . . . . . . . . . . . . . 16
                
      |
76 | | id 22 |
. . . . . . . . . . . . . . . . 17
   |
77 | 76 | ad3antlr 745 |
. . . . . . . . . . . . . . . 16
                
  |
78 | | simplr 770 |
. . . . . . . . . . . . . . . 16
                
        |
79 | | simpr 468 |
. . . . . . . . . . . . . . . 16
                
  |
80 | | simp2 1031 |
. . . . . . . . . . . . . . . . . 18
               |
81 | | zssre 10968 |
. . . . . . . . . . . . . . . . . . . . 21
 |
82 | | ressxr 9702 |
. . . . . . . . . . . . . . . . . . . . 21
 |
83 | 81, 82 | sstri 3427 |
. . . . . . . . . . . . . . . . . . . 20
 |
84 | | nnnegz 10964 |
. . . . . . . . . . . . . . . . . . . 20
    |
85 | 83, 84 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . 19
    |
86 | 85 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
    |
87 | 80, 86 | sylan 479 |
. . . . . . . . . . . . . . . . 17
   
  
      
    |
88 | 76 | nnxrd 37426 |
. . . . . . . . . . . . . . . . . . 19
   |
89 | 88 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
   |
90 | 80, 89 | sylan 479 |
. . . . . . . . . . . . . . . . 17
   
  
      
   |
91 | 34 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . 20
   
      
      |
92 | 82 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   
      
  |
93 | 91, 92 | fssd 5750 |
. . . . . . . . . . . . . . . . . . 19
   
      
      |
94 | 93 | 3adant1l 1284 |
. . . . . . . . . . . . . . . . . 18
                   |
95 | 94 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . 17
   
  
      
       |
96 | | nnre 10638 |
. . . . . . . . . . . . . . . . . . . . 21
   |
97 | 96 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
98 | 97 | 3ad2antl2 1193 |
. . . . . . . . . . . . . . . . . . 19
   
  
      
   |
99 | 98 | renegcld 10067 |
. . . . . . . . . . . . . . . . . 18
   
  
      
    |
100 | 35 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . 19
             |
101 | 100 | 3ad2antl1 1192 |
. . . . . . . . . . . . . . . . . 18
   
  
      
       |
102 | 101 | renegcld 10067 |
. . . . . . . . . . . . . . . . . . . . 21
   
  
      
        |
103 | | simpll 768 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
104 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
105 | | n0i 3727 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
106 | 105 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
  |
107 | 103, 104,
106, 69 | syl21anc 1291 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
108 | 107 | 3ad2antl1 1192 |
. . . . . . . . . . . . . . . . . . . . 21
   
  
      
         |
109 | 34 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
       |
110 | 36, 109 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
       |
111 | 110 | abscld 13575 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
           |
112 | 111 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
113 | 112 | 3ad2antl1 1192 |
. . . . . . . . . . . . . . . . . . . . . 22
   
  
      
           |
114 | 109 | renegcld 10067 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
        |
115 | 114 | leabsd 13553 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
                 |
116 | 110 | absnegd 13588 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
                    |
117 | 115, 116 | breqtrd 4420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
                |
118 | 117 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
                      |
119 | 118 | 3ad2antl1 1192 |
. . . . . . . . . . . . . . . . . . . . . 22
   
  
      
                |
120 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
  
      
     |
121 | 106, 66 | syldan 478 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
122 | 121 | 3ad2antl1 1192 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
  
      
     |
123 | | fimaxre2 10574 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              |
124 | 29, 44, 123 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

 
       |
125 | 124 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              |
126 | 125 | 3ad2antl1 1192 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
  
      
        |
127 | | elmapfun 7513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
128 | 127 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
   |
129 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
   |
130 | 56 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     |
131 | 130 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
   |
132 | 129, 131 | eleqtrd 2551 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
   |
133 | | fvco 5956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                   |
134 | 128, 132,
133 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                 |
135 | 134 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
                 |
136 | | absfun 37660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 |
137 | 136 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
138 | | funco 5627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

    |
139 | 137, 127,
138 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
140 | 139 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
     |
141 | 110, 49 | syl6eleq 2559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
       |
142 | | dmfco 5954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             |
143 | 128, 132,
142 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
           |
144 | 141, 143 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
     |
145 | | fvelrn 6030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 |
146 | 140, 144,
145 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
           |
147 | 135, 146 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
             |
148 | 147 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
149 | 148 | 3ad2antl1 1192 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
  
      
             |
150 | | suprub 10592 |
. . . . . . . . . . . . . . . . . . . . . . 23
                               
        |
151 | 120, 122,
126, 149, 150 | syl31anc 1295 |
. . . . . . . . . . . . . . . . . . . . . 22
   
  
      
                 |
152 | 102, 113,
108, 119, 151 | letrd 9809 |
. . . . . . . . . . . . . . . . . . . . 21
   
  
      
              |
153 | | simpl3 1035 |
. . . . . . . . . . . . . . . . . . . . 21
   
  
      
         |
154 | 102, 108,
98, 152, 153 | lelttrd 9810 |
. . . . . . . . . . . . . . . . . . . 20
   
  
      
        |
155 | 102, 98 | ltnegd 10212 |
. . . . . . . . . . . . . . . . . . . 20
   
  
      
      
          |
156 | 154, 155 | mpbid 215 |
. . . . . . . . . . . . . . . . . . 19
   
  
      
          |
157 | 36, 101 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . 20
   
  
      
       |
158 | 157 | negnegd 9996 |
. . . . . . . . . . . . . . . . . . 19
   
  
      
             |
159 | 156, 158 | breqtrd 4420 |
. . . . . . . . . . . . . . . . . 18
   
  
      
        |
160 | 99, 101, 159 | ltled 9800 |
. . . . . . . . . . . . . . . . 17
   
  
      
        |
161 | 101 | leabsd 13553 |
. . . . . . . . . . . . . . . . . . 19
   
  
      
               |
162 | 101, 113,
108, 161, 151 | letrd 9809 |
. . . . . . . . . . . . . . . . . 18
   
  
      
             |
163 | 101, 108,
98, 162, 153 | lelttrd 9810 |
. . . . . . . . . . . . . . . . 17
   
  
      
       |
164 | 87, 90, 95, 160, 163 | elicod 11710 |
. . . . . . . . . . . . . . . 16
   
  
      
            |
165 | 75, 77, 78, 79, 164 | syl31anc 1295 |
. . . . . . . . . . . . . . 15
                
           |
166 | 165 | adantlllr 37424 |
. . . . . . . . . . . . . 14
     

          
            |
167 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

  |
168 | | mptexg 6151 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
169 | 41, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
  |
170 | 169 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

        |
171 | | hoicvr.2 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
172 | 171 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
    
             |
173 | 167, 170,
172 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

            |
174 | 173 | fveq1d 5881 |
. . . . . . . . . . . . . . . . . . . . . 22
 

                    |
175 | 174 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . . . . 21
 

                    |
176 | | eqidd 2472 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
177 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
178 | 177 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
    
      |
179 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
180 | | opex 4664 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
181 | 180 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
182 | 176, 178,
179, 181 | fvmptd 5969 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
183 | 182 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . . . . . . . 21
 

                |
184 | 175, 183 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . 20
 

              |
185 | 184 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
 

                      |
186 | | negex 9893 |
. . . . . . . . . . . . . . . . . . . . 21
  |
187 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . 21
 |
188 | 186, 187 | op1st 6820 |
. . . . . . . . . . . . . . . . . . . 20
       
  |
189 | 188 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 

       
   |
190 | 185, 189 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . 18
 

               |
191 | 184 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
 

                      |
192 | 186, 187 | op2nd 6821 |
. . . . . . . . . . . . . . . . . . . 20
       
 |
193 | 192 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 

       
  |
194 | 191, 193 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . 18
 

              |
195 | 190, 194 | oveq12d 6326 |
. . . . . . . . . . . . . . . . 17
 

                                   |
196 | 195 | eqcomd 2477 |
. . . . . . . . . . . . . . . 16
 

                                   |
197 | 196 | 3adant1r 1285 |
. . . . . . . . . . . . . . 15
                                          |
198 | 197 | ad5ant135 1280 |
. . . . . . . . . . . . . 14
     

          
                                    |
199 | 166, 198 | eleqtrd 2551 |
. . . . . . . . . . . . 13
     

          
                                   |
200 | 81, 84 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . . 21
    |
201 | | opelxpi 4871 |
. . . . . . . . . . . . . . . . . . . . 21
            |
202 | 200, 96, 201 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . 20
         |
203 | 202 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . 19
             |
204 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . 19
             |
205 | 203, 204 | fmptd 6061 |
. . . . . . . . . . . . . . . . . 18
 

              |
206 | 173 | feq1d 5724 |
. . . . . . . . . . . . . . . . . 18
 

          

              |
207 | 205, 206 | mpbird 240 |
. . . . . . . . . . . . . . . . 17
 

            |
208 | 207 | ad4ant14 1259 |
. . . . . . . . . . . . . . . 16
   
  

             |
209 | 208 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
     

          
             |
210 | | simpr 468 |
. . . . . . . . . . . . . . 15
     

          
   |
211 | 209, 210 | fvovco 37540 |
. . . . . . . . . . . . . 14
     

          
  
                                      |
212 | 211 | eqcomd 2477 |
. . . . . . . . . . . . 13
     

          
                                         |
213 | 199, 212 | eleqtrd 2551 |
. . . . . . . . . . . 12
     

          
                 |
214 | 213 | ralrimiva 2809 |
. . . . . . . . . . 11
        
       

                |
215 | 74, 214 | jca 541 |
. . . . . . . . . 10
        
       


                 |
216 | | vex 3034 |
. . . . . . . . . . 11
 |
217 | 216 | elixp 7547 |
. . . . . . . . . 10
             
                 |
218 | 215, 217 | sylibr 217 |
. . . . . . . . 9
        
       
             |
219 | 218 | ex 441 |
. . . . . . . 8
   
  

        
             |
220 | 219 | reximdva 2858 |
. . . . . . 7
     
         
              |
221 | 71, 220 | mpd 15 |
. . . . . 6
     
 
             |
222 | 22, 23, 24, 221 | syl21anc 1291 |
. . . . 5
  

   
             |
223 | | eliun 4274 |
. . . . 5
             
             |
224 | 222, 223 | sylibr 217 |
. . . 4
  

                 |
225 | 224 | ralrimiva 2809 |
. . 3
 
     

            |
226 | | dfss3 3408 |
. . 3
                                 |
227 | 225, 226 | sylibr 217 |
. 2
 
    
 
          |
228 | 21, 227 | pm2.61dan 808 |
1
  
              |