Step | Hyp | Ref
| Expression |
1 | | itg2mono.1 |
. . . . . . . 8
                 |
2 | | itg2mono.2 |
. . . . . . . . 9
 

    MblFn |
3 | 2 | adantlr 729 |
. . . . . . . 8
          
 

    MblFn |
4 | | itg2mono.3 |
. . . . . . . . 9
 

             |
5 | 4 | adantlr 729 |
. . . . . . . 8
          
 

             |
6 | | itg2mono.4 |
. . . . . . . . 9
 

    
        |
7 | 6 | adantlr 729 |
. . . . . . . 8
          
 

    
        |
8 | | itg2mono.5 |
. . . . . . . . 9
 

            |
9 | 8 | adantlr 729 |
. . . . . . . 8
          
 

            |
10 | | itg2mono.6 |
. . . . . . . 8
               |
11 | | simprll 780 |
. . . . . . . 8
 
            |
12 | | simprlr 781 |
. . . . . . . 8
 
             |
13 | | simprr 774 |
. . . . . . . 8
 
         
      |
14 | 1, 3, 5, 7, 9, 10,
11, 12, 13 | itg2monolem3 22789 |
. . . . . . 7
 
             
  |
15 | 14 | expr 626 |
. . . . . 6
 


 
            |
16 | 15 | pm2.18d 115 |
. . . . 5
 


 
      |
17 | 16 | expr 626 |
. . . 4
 
      
   |
18 | 17 | ralrimiva 2809 |
. . 3
            |
19 | | rge0ssre 11766 |
. . . . . . . . . . . . 13
    |
20 | | fss 5749 |
. . . . . . . . . . . . 13
                           |
21 | 4, 19, 20 | sylancl 675 |
. . . . . . . . . . . 12
 

          |
22 | 21 | ffvelrnda 6037 |
. . . . . . . . . . 11
               |
23 | 22 | an32s 821 |
. . . . . . . . . 10
               |
24 | | eqid 2471 |
. . . . . . . . . 10
                     |
25 | 23, 24 | fmptd 6061 |
. . . . . . . . 9
 

                |
26 | | frn 5747 |
. . . . . . . . 9
                           |
27 | 25, 26 | syl 17 |
. . . . . . . 8
 

         
  |
28 | | 1nn 10642 |
. . . . . . . . . . 11
 |
29 | 24, 23 | dmmptd 5718 |
. . . . . . . . . . 11
 

            |
30 | 28, 29 | syl5eleqr 2556 |
. . . . . . . . . 10
 

            |
31 | | ne0i 3728 |
. . . . . . . . . 10
          
            |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
 

            |
33 | | dm0rn0 5057 |
. . . . . . . . . 10
           
           |
34 | 33 | necon3bii 2695 |
. . . . . . . . 9
          
            |
35 | 32, 34 | sylib 201 |
. . . . . . . 8
 

            |
36 | | ffn 5739 |
. . . . . . . . . . . . 13
                           |
37 | 25, 36 | syl 17 |
. . . . . . . . . . . 12
 

            |
38 | | breq1 4398 |
. . . . . . . . . . . . 13
                             
   |
39 | 38 | ralrn 6040 |
. . . . . . . . . . . 12
             
                            |
40 | 37, 39 | syl 17 |
. . . . . . . . . . 11
 

 
          
                  |
41 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
           |
42 | 41 | fveq1d 5881 |
. . . . . . . . . . . . . . 15
                   |
43 | | fvex 5889 |
. . . . . . . . . . . . . . 15
         |
44 | 42, 24, 43 | fvmpt 5963 |
. . . . . . . . . . . . . 14
                         |
45 | 44 | breq1d 4405 |
. . . . . . . . . . . . 13
                           |
46 | 45 | ralbiia 2822 |
. . . . . . . . . . . 12
 
             
           |
47 | 42 | breq1d 4405 |
. . . . . . . . . . . . 13
         
           |
48 | 47 | cbvralv 3005 |
. . . . . . . . . . . 12
 
                
  |
49 | 46, 48 | bitr4i 260 |
. . . . . . . . . . 11
 
             
           |
50 | 40, 49 | syl6bb 269 |
. . . . . . . . . 10
 

 
          
            |
51 | 50 | rexbidv 2892 |
. . . . . . . . 9
 

  
          
             |
52 | 8, 51 | mpbird 240 |
. . . . . . . 8
 

               |
53 | | suprcl 10591 |
. . . . . . . 8
                                                    |
54 | 27, 35, 52, 53 | syl3anc 1292 |
. . . . . . 7
 

                |
55 | 54 | rexrd 9708 |
. . . . . 6
 

                |
56 | | 0red 9662 |
. . . . . . 7
 

  |
57 | 4 | ralrimiva 2809 |
. . . . . . . . . . 11
               |
58 | | fveq2 5879 |
. . . . . . . . . . . . 13
           |
59 | 58 | feq1d 5724 |
. . . . . . . . . . . 12
            
              |
60 | 59 | rspcv 3132 |
. . . . . . . . . . 11
  
                         |
61 | 28, 57, 60 | mpsyl 64 |
. . . . . . . . . 10
              |
62 | 61 | ffvelrnda 6037 |
. . . . . . . . 9
 

             |
63 | | elrege0 11764 |
. . . . . . . . 9
                    
           |
64 | 62, 63 | sylib 201 |
. . . . . . . 8
 

                    |
65 | 64 | simpld 466 |
. . . . . . 7
 

          |
66 | 64 | simprd 470 |
. . . . . . 7
 

          |
67 | 58 | fveq1d 5881 |
. . . . . . . . . . 11
                   |
68 | | fvex 5889 |
. . . . . . . . . . 11
         |
69 | 67, 24, 68 | fvmpt 5963 |
. . . . . . . . . 10
                         |
70 | 28, 69 | ax-mp 5 |
. . . . . . . . 9
                       |
71 | | fnfvelrn 6034 |
. . . . . . . . . 10
                                       |
72 | 37, 28, 71 | sylancl 675 |
. . . . . . . . 9
 

                          |
73 | 70, 72 | syl5eqelr 2554 |
. . . . . . . 8
 

                    |
74 | | suprub 10592 |
. . . . . . . 8
            
          
                                                        |
75 | 27, 35, 52, 73, 74 | syl31anc 1295 |
. . . . . . 7
 

                        |
76 | 56, 65, 54, 66, 75 | letrd 9809 |
. . . . . 6
 

                |
77 | | elxrge0 11767 |
. . . . . 6
                 
              
                 |
78 | 55, 76, 77 | sylanbrc 677 |
. . . . 5
 

                   |
79 | 78, 1 | fmptd 6061 |
. . . 4
          |
80 | | icossicc 11746 |
. . . . . . . . . 10
       |
81 | | fss 5749 |
. . . . . . . . . 10
                                 |
82 | 4, 80, 81 | sylancl 675 |
. . . . . . . . 9
 

             |
83 | | itg2cl 22769 |
. . . . . . . . 9
                      |
84 | 82, 83 | syl 17 |
. . . . . . . 8
 

          |
85 | | eqid 2471 |
. . . . . . . 8
                     |
86 | 84, 85 | fmptd 6061 |
. . . . . . 7
                 |
87 | | frn 5747 |
. . . . . . 7
                        
  |
88 | 86, 87 | syl 17 |
. . . . . 6
             |
89 | | supxrcl 11625 |
. . . . . 6
          
                |
90 | 88, 89 | syl 17 |
. . . . 5
                 |
91 | 10, 90 | syl5eqel 2553 |
. . . 4
   |
92 | | itg2leub 22771 |
. . . 4
        
     
   
        |
93 | 79, 91, 92 | syl2anc 673 |
. . 3
     
   
        |
94 | 18, 93 | mpbird 240 |
. 2
    
  |
95 | 41 | feq1d 5724 |
. . . . . . . . . . 11
            
              |
96 | 95 | cbvralv 3005 |
. . . . . . . . . 10
 
          
              |
97 | 57, 96 | sylib 201 |
. . . . . . . . 9
               |
98 | 97 | r19.21bi 2776 |
. . . . . . . 8
 

             |
99 | | fss 5749 |
. . . . . . . 8
                                 |
100 | 98, 80, 99 | sylancl 675 |
. . . . . . 7
 

             |
101 | 79 | adantr 472 |
. . . . . . 7
 

         |
102 | 27, 35, 52 | 3jca 1210 |
. . . . . . . . . . . . 13
 

                                     |
103 | 102 | adantlr 729 |
. . . . . . . . . . . 12
                                          |
104 | 44 | ad2antlr 741 |
. . . . . . . . . . . . 13
                             |
105 | 37 | adantlr 729 |
. . . . . . . . . . . . . 14
                 |
106 | | simplr 770 |
. . . . . . . . . . . . . 14
       |
107 | | fnfvelrn 6034 |
. . . . . . . . . . . . . 14
                                       |
108 | 105, 106,
107 | syl2anc 673 |
. . . . . . . . . . . . 13
                               |
109 | 104, 108 | eqeltrrd 2550 |
. . . . . . . . . . . 12
                         |
110 | | suprub 10592 |
. . . . . . . . . . . 12
            
          
                                                        |
111 | 103, 109,
110 | syl2anc 673 |
. . . . . . . . . . 11
                             |
112 | | simpr 468 |
. . . . . . . . . . . 12
       |
113 | | ltso 9732 |
. . . . . . . . . . . . 13
 |
114 | 113 | supex 7995 |
. . . . . . . . . . . 12
               |
115 | 1 | fvmpt2 5972 |
. . . . . . . . . . . 12
                                     |
116 | 112, 114,
115 | sylancl 675 |
. . . . . . . . . . 11
                         |
117 | 111, 116 | breqtrrd 4422 |
. . . . . . . . . 10
                   |
118 | 117 | ralrimiva 2809 |
. . . . . . . . 9
 

               |
119 | | fveq2 5879 |
. . . . . . . . . . 11
                   |
120 | | fveq2 5879 |
. . . . . . . . . . 11
           |
121 | 119, 120 | breq12d 4408 |
. . . . . . . . . 10
         
   
               |
122 | 121 | cbvralv 3005 |
. . . . . . . . 9
 
                    
      |
123 | 118, 122 | sylib 201 |
. . . . . . . 8
 

               |
124 | | ffn 5739 |
. . . . . . . . . 10
                  |
125 | 100, 124 | syl 17 |
. . . . . . . . 9
 

      |
126 | 54, 1 | fmptd 6061 |
. . . . . . . . . . 11
       |
127 | | ffn 5739 |
. . . . . . . . . . 11
       |
128 | 126, 127 | syl 17 |
. . . . . . . . . 10
   |
129 | 128 | adantr 472 |
. . . . . . . . 9
 

  |
130 | | reex 9648 |
. . . . . . . . . 10
 |
131 | 130 | a1i 11 |
. . . . . . . . 9
 

  |
132 | | inidm 3632 |
. . . . . . . . 9
   |
133 | | eqidd 2472 |
. . . . . . . . 9
                       |
134 | | eqidd 2472 |
. . . . . . . . 9
               |
135 | 125, 129,
131, 131, 132, 133, 134 | ofrfval 6558 |
. . . . . . . 8
 

                      |
136 | 123, 135 | mpbird 240 |
. . . . . . 7
 

    
  |
137 | | itg2le 22776 |
. . . . . . 7
                         
              |
138 | 100, 101,
136, 137 | syl3anc 1292 |
. . . . . 6
 

              |
139 | 138 | ralrimiva 2809 |
. . . . 5
                |
140 | | ffn 5739 |
. . . . . . . 8
                           |
141 | 86, 140 | syl 17 |
. . . . . . 7
             |
142 | | breq1 4398 |
. . . . . . . 8
               
   
                     |
143 | 142 | ralrn 6040 |
. . . . . . 7
             
             
                      |
144 | 141, 143 | syl 17 |
. . . . . 6
                  
             
       |
145 | 41 | fveq2d 5883 |
. . . . . . . . 9
                   |
146 | | fvex 5889 |
. . . . . . . . 9
         |
147 | 145, 85, 146 | fvmpt 5963 |
. . . . . . . 8
                         |
148 | 147 | breq1d 4405 |
. . . . . . 7
               
   
               |
149 | 148 | ralbiia 2822 |
. . . . . 6
 
                                 |
150 | 144, 149 | syl6bb 269 |
. . . . 5
                  
               |
151 | 139, 150 | mpbird 240 |
. . . 4
  
                |
152 | | itg2cl 22769 |
. . . . . 6
              |
153 | 79, 152 | syl 17 |
. . . . 5
       |
154 | | supxrleub 11637 |
. . . . 5
                               
    

                 |
155 | 88, 153, 154 | syl2anc 673 |
. . . 4
                     
                 |
156 | 151, 155 | mpbird 240 |
. . 3
                     |
157 | 10, 156 | syl5eqbr 4429 |
. 2

      |
158 | | xrletri3 11474 |
. . 3
           
             |
159 | 153, 91, 158 | syl2anc 673 |
. 2
     
             |
160 | 94, 157, 159 | mpbir2and 936 |
1
       |