Proof of Theorem dvfsumlem1
Step | Hyp | Ref
| Expression |
1 | | dvfsum.s |
. . . . . . . . . 10
    |
2 | | ioossre 11721 |
. . . . . . . . . 10
    |
3 | 1, 2 | eqsstri 3448 |
. . . . . . . . 9
 |
4 | | dvfsumlem1.2 |
. . . . . . . . 9
   |
5 | 3, 4 | sseldi 3416 |
. . . . . . . 8
   |
6 | | dvfsumlem1.1 |
. . . . . . . . . 10
   |
7 | 3, 6 | sseldi 3416 |
. . . . . . . . 9
   |
8 | 7 | flcld 12067 |
. . . . . . . 8
       |
9 | | reflcl 12065 |
. . . . . . . . . 10
       |
10 | 7, 9 | syl 17 |
. . . . . . . . 9
       |
11 | | flle 12068 |
. . . . . . . . . 10
       |
12 | 7, 11 | syl 17 |
. . . . . . . . 9
    
  |
13 | | dvfsumlem1.4 |
. . . . . . . . 9

  |
14 | 10, 7, 5, 12, 13 | letrd 9809 |
. . . . . . . 8
    
  |
15 | | flbi 12084 |
. . . . . . . . 9
                    
          |
16 | 15 | baibd 923 |
. . . . . . . 8
            
        
         |
17 | 5, 8, 14, 16 | syl21anc 1291 |
. . . . . . 7
         
         |
18 | 17 | biimpar 493 |
. . . . . 6
 
      
          |
19 | 18 | oveq2d 6324 |
. . . . 5
 
      
              |
20 | 19 | oveq1d 6323 |
. . . 4
 
      
 
       ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)    |
21 | 18 | oveq2d 6324 |
. . . . . 6
 
      
                  |
22 | 21 | sumeq1d 13844 |
. . . . 5
 
      
                      |
23 | 22 | oveq1d 6323 |
. . . 4
 
      
 
           ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)    |
24 | 20, 23 | oveq12d 6326 |
. . 3
 
      
          ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)     |
25 | | simpr 468 |
. . . . . . . . . . 11
 
               |
26 | 7 | adantr 472 |
. . . . . . . . . . . . 13
 
         |
27 | 26 | flcld 12067 |
. . . . . . . . . . . 12
 
             |
28 | 27 | peano2zd 11066 |
. . . . . . . . . . 11
 
               |
29 | 25, 28 | eqeltrd 2549 |
. . . . . . . . . 10
 
         |
30 | | flid 12077 |
. . . . . . . . . 10
       |
31 | 29, 30 | syl 17 |
. . . . . . . . 9
 
             |
32 | 31, 25 | eqtrd 2505 |
. . . . . . . 8
 
                   |
33 | 32 | oveq2d 6324 |
. . . . . . 7
 
       
               |
34 | 33 | oveq1d 6323 |
. . . . . 6
 
                ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)    |
35 | 5 | recnd 9687 |
. . . . . . . . . 10
   |
36 | 10 | recnd 9687 |
. . . . . . . . . 10
       |
37 | 35, 36 | subcld 10005 |
. . . . . . . . 9
         |
38 | | 1cnd 9677 |
. . . . . . . . 9
   |
39 | 3 | a1i 11 |
. . . . . . . . . . . . 13

  |
40 | | dvfsum.a |
. . . . . . . . . . . . 13
 
   |
41 | | dvfsum.b1 |
. . . . . . . . . . . . 13
 
   |
42 | | dvfsum.b3 |
. . . . . . . . . . . . 13
         |
43 | 39, 40, 41, 42 | dvmptrecl 23055 |
. . . . . . . . . . . 12
 
   |
44 | 43 | recnd 9687 |
. . . . . . . . . . 11
 
   |
45 | 44 | ralrimiva 2809 |
. . . . . . . . . 10
 
  |
46 | | nfcsb1v 3365 |
. . . . . . . . . . . 12
  
 ![]_ ]_](_urbrack.gif)  |
47 | 46 | nfel1 2626 |
. . . . . . . . . . 11
  
 ![]_ ]_](_urbrack.gif)
 |
48 | | csbeq1a 3358 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)   |
49 | 48 | eleq1d 2533 |
. . . . . . . . . . 11
 
  ![]_ ]_](_urbrack.gif)    |
50 | 47, 49 | rspc 3130 |
. . . . . . . . . 10
  
  ![]_ ]_](_urbrack.gif)
   |
51 | 4, 45, 50 | sylc 61 |
. . . . . . . . 9
   ![]_ ]_](_urbrack.gif)
  |
52 | 37, 38, 51 | subdird 10096 |
. . . . . . . 8
            ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     |
53 | 35, 36, 38 | subsub4d 10036 |
. . . . . . . . 9
                   |
54 | 53 | oveq1d 6323 |
. . . . . . . 8
            ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)    |
55 | 51 | mulid2d 9679 |
. . . . . . . . 9
    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
56 | 55 | oveq2d 6324 |
. . . . . . . 8
           ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
57 | 52, 54, 56 | 3eqtr3d 2513 |
. . . . . . 7
            ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
58 | 57 | adantr 472 |
. . . . . 6
 
                  ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
59 | 34, 58 | eqtrd 2505 |
. . . . 5
 
                ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
60 | | dvfsum.m |
. . . . . . . . . . . 12
   |
61 | 8 | peano2zd 11066 |
. . . . . . . . . . . 12
         |
62 | 60 | zred 11063 |
. . . . . . . . . . . . . . . 16
   |
63 | | peano2rem 9961 |
. . . . . . . . . . . . . . . 16
 
   |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
     |
65 | | dvfsum.d |
. . . . . . . . . . . . . . 15
   |
66 | | dvfsum.md |
. . . . . . . . . . . . . . . 16

    |
67 | | 1red 9676 |
. . . . . . . . . . . . . . . . 17
   |
68 | 62, 67, 65 | lesubaddd 10231 |
. . . . . . . . . . . . . . . 16
         |
69 | 66, 68 | mpbird 240 |
. . . . . . . . . . . . . . 15
  
  |
70 | | dvfsumlem1.3 |
. . . . . . . . . . . . . . 15

  |
71 | 64, 65, 7, 69, 70 | letrd 9809 |
. . . . . . . . . . . . . 14
  
  |
72 | | peano2zm 11004 |
. . . . . . . . . . . . . . . 16
 
   |
73 | 60, 72 | syl 17 |
. . . . . . . . . . . . . . 15
     |
74 | | flge 12074 |
. . . . . . . . . . . . . . 15
  
      
       |
75 | 7, 73, 74 | syl2anc 673 |
. . . . . . . . . . . . . 14
             |
76 | 71, 75 | mpbid 215 |
. . . . . . . . . . . . 13
  
      |
77 | 62, 67, 10 | lesubaddd 10231 |
. . . . . . . . . . . . 13
       
         |
78 | 76, 77 | mpbid 215 |
. . . . . . . . . . . 12

        |
79 | | eluz2 11188 |
. . . . . . . . . . . 12
                           |
80 | 60, 61, 78, 79 | syl3anbrc 1214 |
. . . . . . . . . . 11
             |
81 | | dvfsum.b2 |
. . . . . . . . . . . . . 14
 
   |
82 | 81 | recnd 9687 |
. . . . . . . . . . . . 13
 
   |
83 | 82 | ralrimiva 2809 |
. . . . . . . . . . . 12
 
  |
84 | | elfzuz 11822 |
. . . . . . . . . . . . 13
                 |
85 | | dvfsum.z |
. . . . . . . . . . . . 13
     |
86 | 84, 85 | syl6eleqr 2560 |
. . . . . . . . . . . 12
             |
87 | | dvfsum.c |
. . . . . . . . . . . . . 14
   |
88 | 87 | eleq1d 2533 |
. . . . . . . . . . . . 13
 
   |
89 | 88 | rspccva 3135 |
. . . . . . . . . . . 12
  
   |
90 | 83, 86, 89 | syl2an 485 |
. . . . . . . . . . 11
 
          
  |
91 | | eqvisset 3039 |
. . . . . . . . . . . . 13
               |
92 | | eqeq2 2482 |
. . . . . . . . . . . . . . 15
       
         |
93 | 92 | biimpar 493 |
. . . . . . . . . . . . . 14
       
      
  |
94 | 93, 87 | syl 17 |
. . . . . . . . . . . . 13
       
      
  |
95 | 91, 94 | csbied 3376 |
. . . . . . . . . . . 12
               ![]_ ]_](_urbrack.gif)   |
96 | 95 | eqcomd 2477 |
. . . . . . . . . . 11
               ![]_ ]_](_urbrack.gif)   |
97 | 80, 90, 96 | fsumm1 13889 |
. . . . . . . . . 10
              
                     ![]_ ]_](_urbrack.gif)    |
98 | | ax-1cn 9615 |
. . . . . . . . . . . . . 14
 |
99 | | pncan 9901 |
. . . . . . . . . . . . . 14
     
               |
100 | 36, 98, 99 | sylancl 675 |
. . . . . . . . . . . . 13
               |
101 | 100 | oveq2d 6324 |
. . . . . . . . . . . 12
                       |
102 | 101 | sumeq1d 13844 |
. . . . . . . . . . 11
                           |
103 | 102 | oveq1d 6323 |
. . . . . . . . . 10
                        ![]_ ]_](_urbrack.gif)   
                 ![]_ ]_](_urbrack.gif)    |
104 | 97, 103 | eqtrd 2505 |
. . . . . . . . 9
              
                 ![]_ ]_](_urbrack.gif)    |
105 | 104 | adantr 472 |
. . . . . . . 8
 
                                      ![]_ ]_](_urbrack.gif)    |
106 | 32 | oveq2d 6324 |
. . . . . . . . 9
 
                           |
107 | 106 | sumeq1d 13844 |
. . . . . . . 8
 
                               |
108 | 25 | csbeq1d 3356 |
. . . . . . . . 9
 
         ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
109 | 108 | oveq2d 6324 |
. . . . . . . 8
 
                    ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)    |
110 | 105, 107,
109 | 3eqtr4d 2515 |
. . . . . . 7
 
                  
           ![]_ ]_](_urbrack.gif)    |
111 | 110 | oveq1d 6323 |
. . . . . 6
 
                    ![]_ ]_](_urbrack.gif)                ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
112 | | fzfid 12224 |
. . . . . . . . 9
           |
113 | | elfzuz 11822 |
. . . . . . . . . . 11
        
      |
114 | 113, 85 | syl6eleqr 2560 |
. . . . . . . . . 10
        
  |
115 | 83, 114, 89 | syl2an 485 |
. . . . . . . . 9
 
        
  |
116 | 112, 115 | fsumcl 13876 |
. . . . . . . 8
             |
117 | 40 | recnd 9687 |
. . . . . . . . . 10
 
   |
118 | 117 | ralrimiva 2809 |
. . . . . . . . 9
 
  |
119 | | nfcsb1v 3365 |
. . . . . . . . . . 11
  
 ![]_ ]_](_urbrack.gif)  |
120 | 119 | nfel1 2626 |
. . . . . . . . . 10
  
 ![]_ ]_](_urbrack.gif)
 |
121 | | csbeq1a 3358 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)   |
122 | 121 | eleq1d 2533 |
. . . . . . . . . 10
 
  ![]_ ]_](_urbrack.gif)    |
123 | 120, 122 | rspc 3130 |
. . . . . . . . 9
  
  ![]_ ]_](_urbrack.gif)
   |
124 | 4, 118, 123 | sylc 61 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)
  |
125 | 116, 51, 124 | addsubd 10026 |
. . . . . . 7
               ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)                ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
126 | 125 | adantr 472 |
. . . . . 6
 
                     ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)                ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
127 | 111, 126 | eqtrd 2505 |
. . . . 5
 
                    ![]_ ]_](_urbrack.gif)                ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
128 | 59, 127 | oveq12d 6326 |
. . . 4
 
                 ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)                ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)     |
129 | 37, 51 | mulcld 9681 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)    |
130 | 129 | adantr 472 |
. . . . 5
 
                ![]_ ]_](_urbrack.gif)    |
131 | 51 | adantr 472 |
. . . . 5
 
         ![]_ ]_](_urbrack.gif)   |
132 | 116, 124 | subcld 10005 |
. . . . . 6
              ![]_ ]_](_urbrack.gif)    |
133 | 132 | adantr 472 |
. . . . 5
 
                    ![]_ ]_](_urbrack.gif)    |
134 | 130, 131,
133 | nppcan3d 10032 |
. . . 4
 
                  ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)                ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)     |
135 | 128, 134 | eqtrd 2505 |
. . 3
 
                 ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)     |
136 | | dvfsumlem1.6 |
. . . 4

        |
137 | | peano2re 9824 |
. . . . . 6
             |
138 | 10, 137 | syl 17 |
. . . . 5
         |
139 | 5, 138 | leloed 9795 |
. . . 4
                         |
140 | 136, 139 | mpbid 215 |
. . 3
                 |
141 | 24, 135, 140 | mpjaodan 803 |
. 2
           ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)     |
142 | | ovex 6336 |
. . 3
          ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)    |
143 | | nfcv 2612 |
. . . 4
   |
144 | | nfcv 2612 |
. . . . . 6
         |
145 | | nfcv 2612 |
. . . . . 6
  |
146 | 144, 145,
46 | nfov 6334 |
. . . . 5
           ![]_ ]_](_urbrack.gif)   |
147 | | nfcv 2612 |
. . . . 5
  |
148 | | nfcv 2612 |
. . . . . 6
             |
149 | | nfcv 2612 |
. . . . . 6
  |
150 | 148, 149,
119 | nfov 6334 |
. . . . 5
               ![]_ ]_](_urbrack.gif)   |
151 | 146, 147,
150 | nfov 6334 |
. . . 4
            ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)    |
152 | | id 22 |
. . . . . . 7
   |
153 | | fveq2 5879 |
. . . . . . 7
           |
154 | 152, 153 | oveq12d 6326 |
. . . . . 6
               |
155 | 154, 48 | oveq12d 6326 |
. . . . 5
                  ![]_ ]_](_urbrack.gif)    |
156 | 153 | oveq2d 6324 |
. . . . . . 7
                   |
157 | 156 | sumeq1d 13844 |
. . . . . 6
                       |
158 | 157, 121 | oveq12d 6326 |
. . . . 5
                          ![]_ ]_](_urbrack.gif)    |
159 | 155, 158 | oveq12d 6326 |
. . . 4
                                 ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)     |
160 | | dvfsum.h |
. . . 4
                         |
161 | 143, 151,
159, 160 | fvmptf 5981 |
. . 3
            ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)                  ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)     |
162 | 4, 142, 161 | sylancl 675 |
. 2
               ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)     |
163 | 129, 124,
116 | subadd23d 10027 |
. 2
            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)  
                    ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)     |
164 | 141, 162,
163 | 3eqtr4d 2515 |
1
                ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)               |