Step | Hyp | Ref
| Expression |
1 | | itgulm.z |
. . . . 5
     |
2 | | itgulm.m |
. . . . . 6
   |
3 | 2 | adantr 472 |
. . . . 5
 

  |
4 | | itgulm.f |
. . . . . . . 8
        |
5 | | ffn 5739 |
. . . . . . . 8
     
  |
6 | 4, 5 | syl 17 |
. . . . . . 7
   |
7 | | itgulm.u |
. . . . . . 7
          |
8 | | ulmf2 23418 |
. . . . . . 7
              
   |
9 | 6, 7, 8 | syl2anc 673 |
. . . . . 6
         |
10 | 9 | adantr 472 |
. . . . 5
 

        |
11 | | eqidd 2472 |
. . . . 5
    
 
                  |
12 | | eqidd 2472 |
. . . . 5
               |
13 | 7 | adantr 472 |
. . . . 5
 

         |
14 | | simpr 468 |
. . . . . 6
 

  |
15 | | itgulm.s |
. . . . . . . 8
       |
16 | 15 | adantr 472 |
. . . . . . 7
 

      |
17 | | ulmcl 23415 |
. . . . . . . . . . . 12
              |
18 | | fdm 5745 |
. . . . . . . . . . . 12
       |
19 | 7, 17, 18 | 3syl 18 |
. . . . . . . . . . 11
   |
20 | 1, 2, 4, 7, 15 | iblulm 23441 |
. . . . . . . . . . . 12
    |
21 | | iblmbf 22804 |
. . . . . . . . . . . 12
  MblFn |
22 | | mbfdm 22663 |
. . . . . . . . . . . 12
 MblFn
  |
23 | 20, 21, 22 | 3syl 18 |
. . . . . . . . . . 11
   |
24 | 19, 23 | eqeltrrd 2550 |
. . . . . . . . . 10
   |
25 | | mblss 22563 |
. . . . . . . . . 10
   |
26 | | ovolge0 22512 |
. . . . . . . . . 10

       |
27 | 24, 25, 26 | 3syl 18 |
. . . . . . . . 9

       |
28 | | mblvol 22562 |
. . . . . . . . . 10
            |
29 | 24, 28 | syl 17 |
. . . . . . . . 9
            |
30 | 27, 29 | breqtrrd 4422 |
. . . . . . . 8

      |
31 | 30 | adantr 472 |
. . . . . . 7
 

      |
32 | 16, 31 | ge0p1rpd 11391 |
. . . . . 6
 

        |
33 | 14, 32 | rpdivcld 11381 |
. . . . 5
 

          |
34 | 1, 3, 10, 11, 12, 13, 33 | ulmi 23420 |
. . . 4
 


      
                            |
35 | 1 | uztrn2 11200 |
. . . . . . . 8
 
    
  |
36 | 9 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . 16
 
         |
37 | | elmapi 7511 |
. . . . . . . . . . . . . . . 16
                 |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . 15
 
           |
39 | 38 | ffvelrnda 6037 |
. . . . . . . . . . . . . 14
               |
40 | 39 | adantllr 733 |
. . . . . . . . . . . . 13
   



          |
41 | 40 | adantlrr 735 |
. . . . . . . . . . . 12
   
 
                            
           |
42 | 38 | feqmptd 5932 |
. . . . . . . . . . . . . 14
 
                 |
43 | 4 | ffvelrnda 6037 |
. . . . . . . . . . . . . 14
 
        |
44 | 42, 43 | eqeltrrd 2550 |
. . . . . . . . . . . . 13
 
              |
45 | 44 | ad2ant2r 761 |
. . . . . . . . . . . 12
                                               |
46 | 7, 17 | syl 17 |
. . . . . . . . . . . . . . 15
       |
47 | 46 | ffvelrnda 6037 |
. . . . . . . . . . . . . 14
 
       |
48 | 47 | adantlr 729 |
. . . . . . . . . . . . 13
           |
49 | 48 | adantlr 729 |
. . . . . . . . . . . 12
   
 
                            
       |
50 | 46 | feqmptd 5932 |
. . . . . . . . . . . . . 14
         |
51 | 50, 20 | eqeltrrd 2550 |
. . . . . . . . . . . . 13
          |
52 | 51 | ad2antrr 740 |
. . . . . . . . . . . 12
                                           |
53 | 41, 45, 49, 52 | itgsub 22862 |
. . . . . . . . . . 11
                                                              
          |
54 | 53 | fveq2d 5883 |
. . . . . . . . . 10
                                                                                 |
55 | 41, 49 | subcld 10005 |
. . . . . . . . . . . . 13
   
 
                            
                 |
56 | 41, 45, 49, 52 | iblsub 22858 |
. . . . . . . . . . . . 13
                                                     |
57 | 55, 56 | itgcl 22820 |
. . . . . . . . . . . 12
                                                     |
58 | 57 | abscld 13575 |
. . . . . . . . . . 11
                                                         |
59 | 55 | abscld 13575 |
. . . . . . . . . . . 12
   
 
                            
                     |
60 | 55, 56 | iblabs 22865 |
. . . . . . . . . . . 12
                                                         |
61 | 59, 60 | itgrecl 22834 |
. . . . . . . . . . 11
                                                         |
62 | | rpre 11331 |
. . . . . . . . . . . 12

  |
63 | 62 | ad2antlr 741 |
. . . . . . . . . . 11
                                    |
64 | 55, 56 | itgabs 22871 |
. . . . . . . . . . 11
                                                                              |
65 | 33 | adantr 472 |
. . . . . . . . . . . . . 14
                                            |
66 | 65 | rpred 11364 |
. . . . . . . . . . . . 13
                                            |
67 | 15 | ad2antrr 740 |
. . . . . . . . . . . . 13
                                        |
68 | 66, 67 | remulcld 9689 |
. . . . . . . . . . . 12
                                                  |
69 | | fconstmpt 4883 |
. . . . . . . . . . . . . . 15
                       |
70 | 24 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
                                 
  |
71 | 65 | rpcnd 11366 |
. . . . . . . . . . . . . . . 16
                                            |
72 | | iblconst 22854 |
. . . . . . . . . . . . . . . 16
                              |
73 | 70, 67, 71, 72 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
                                                 |
74 | 69, 73 | syl5eqelr 2554 |
. . . . . . . . . . . . . 14
                                               |
75 | 66 | adantr 472 |
. . . . . . . . . . . . . 14
   
 
                            
           |
76 | | simprr 774 |
. . . . . . . . . . . . . . . 16
                                  
                            |
77 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . 20
                   |
78 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . 20
           |
79 | 77, 78 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . 19
                               |
80 | 79 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . 18
                                       |
81 | 80 | breq1d 4405 |
. . . . . . . . . . . . . . . . 17
                           
                             |
82 | 81 | rspccva 3135 |
. . . . . . . . . . . . . . . 16
                                                          |
83 | 76, 82 | sylan 479 |
. . . . . . . . . . . . . . 15
   
 
                            
                             |
84 | 59, 75, 83 | ltled 9800 |
. . . . . . . . . . . . . 14
   
 
                            
                  
          |
85 | 60, 74, 59, 75, 84 | itgle 22846 |
. . . . . . . . . . . . 13
                                                                    |
86 | | itgconst 22855 |
. . . . . . . . . . . . . 14
                                          |
87 | 70, 67, 71, 86 | syl3anc 1292 |
. . . . . . . . . . . . 13
                                                             |
88 | 85, 87 | breqtrd 4420 |
. . . . . . . . . . . 12
                                                                       |
89 | 63 | recnd 9687 |
. . . . . . . . . . . . . 14
                                    |
90 | 67 | recnd 9687 |
. . . . . . . . . . . . . 14
                                        |
91 | 32 | adantr 472 |
. . . . . . . . . . . . . . 15
                                          |
92 | 91 | rpcnd 11366 |
. . . . . . . . . . . . . 14
                                          |
93 | 91 | rpne0d 11369 |
. . . . . . . . . . . . . 14
                                          |
94 | 89, 90, 92, 93 | div23d 10442 |
. . . . . . . . . . . . 13
                                                                |
95 | 67 | ltp1d 10559 |
. . . . . . . . . . . . . . 15
                                     
        |
96 | | peano2re 9824 |
. . . . . . . . . . . . . . . . 17
             |
97 | 67, 96 | syl 17 |
. . . . . . . . . . . . . . . 16
                                          |
98 | | rpgt0 11336 |
. . . . . . . . . . . . . . . . 17

  |
99 | 98 | ad2antlr 741 |
. . . . . . . . . . . . . . . 16
                                 
  |
100 | | ltmul2 10478 |
. . . . . . . . . . . . . . . 16
                                           |
101 | 67, 97, 63, 99, 100 | syl112anc 1296 |
. . . . . . . . . . . . . . 15
                                      
     
                 |
102 | 95, 101 | mpbid 215 |
. . . . . . . . . . . . . 14
                                                  |
103 | 63, 67 | remulcld 9689 |
. . . . . . . . . . . . . . 15
                                          |
104 | 103, 63, 91 | ltdivmul2d 11413 |
. . . . . . . . . . . . . 14
                                                
                 |
105 | 102, 104 | mpbird 240 |
. . . . . . . . . . . . 13
                                                  |
106 | 94, 105 | eqbrtrrd 4418 |
. . . . . . . . . . . 12
                                                  |
107 | 61, 68, 63, 88, 106 | lelttrd 9810 |
. . . . . . . . . . 11
                                                         |
108 | 58, 61, 63, 64, 107 | lelttrd 9810 |
. . . . . . . . . 10
                                                         |
109 | 54, 108 | eqbrtrrd 4418 |
. . . . . . . . 9
                                                            |
110 | 109 | expr 626 |
. . . . . . . 8
      
                         
              
            |
111 | 35, 110 | sylan2 482 |
. . . . . . 7
    
       
                                                     |
112 | 111 | anassrs 660 |
. . . . . 6
   


      
                                                     |
113 | 112 | ralimdva 2805 |
. . . . 5
      
     
                                                           |
114 | 113 | reximdva 2858 |
. . . 4
 

 

     
                           
                                |
115 | 34, 114 | mpd 15 |
. . 3
 


                                |
116 | 115 | ralrimiva 2809 |
. 2
   
                   
           |
117 | | fvex 5889 |
. . . . . 6
     |
118 | 1, 117 | eqeltri 2545 |
. . . . 5
 |
119 | 118 | mptex 6152 |
. . . 4
              |
120 | 119 | a1i 11 |
. . 3
                |
121 | | fveq2 5879 |
. . . . . . . 8
           |
122 | 121 | fveq1d 5881 |
. . . . . . 7
                   |
123 | 122 | adantr 472 |
. . . . . 6
 
                   |
124 | 123 | itgeq2dv 22818 |
. . . . 5
                         |
125 | | eqid 2471 |
. . . . 5
                           |
126 | | itgex 22807 |
. . . . 5
            |
127 | 124, 125,
126 | fvmpt 5963 |
. . . 4
                               |
128 | 127 | adantl 473 |
. . 3
 
                               |
129 | 47, 51 | itgcl 22820 |
. . 3
          |
130 | 39, 44 | itgcl 22820 |
. . 3
 
              |
131 | 1, 2, 120, 128, 129, 130 | clim2c 13646 |
. 2
                     
                                   |
132 | 116, 131 | mpbird 240 |
1
                       |