Proof of Theorem aaliou3lem7
Step | Hyp | Ref
| Expression |
1 | | peano2nn 10437 |
. . 3
 
   |
2 | | eqid 2451 |
. . . 4
    
                    
                    
                |
3 | | aaliou3lem.c |
. . . 4
            |
4 | 2, 3 | aaliou3lem3 21928 |
. . 3
                   
           
        
       |
5 | | 3simpc 987 |
. . 3
                 
           
        
    
 
   
                                   |
6 | 1, 4, 5 | 3syl 20 |
. 2
      
                                   |
7 | | nncn 10433 |
. . . . . . . . . . . 12
   |
8 | | ax-1cn 9443 |
. . . . . . . . . . . 12
 |
9 | | pncan 9719 |
. . . . . . . . . . . 12
 
       |
10 | 7, 8, 9 | sylancl 662 |
. . . . . . . . . . 11
       |
11 | 10 | oveq2d 6208 |
. . . . . . . . . 10
               |
12 | 11 | sumeq1d 13282 |
. . . . . . . . 9
               
           |
13 | 12 | oveq1d 6207 |
. . . . . . . 8
                              
                        |
14 | | nnuz 10999 |
. . . . . . . . 9
     |
15 | | eqid 2451 |
. . . . . . . . 9
   
         |
16 | | eqidd 2452 |
. . . . . . . . 9
 
           |
17 | | fveq2 5791 |
. . . . . . . . . . . . . 14
           |
18 | 17 | negeqd 9707 |
. . . . . . . . . . . . 13
             |
19 | 18 | oveq2d 6208 |
. . . . . . . . . . . 12
                     |
20 | | ovex 6217 |
. . . . . . . . . . . 12
          |
21 | 19, 3, 20 | fvmpt 5875 |
. . . . . . . . . . 11
                |
22 | | 2rp 11099 |
. . . . . . . . . . . . 13
 |
23 | | nnnn0 10689 |
. . . . . . . . . . . . . . . 16
   |
24 | | faccl 12164 |
. . . . . . . . . . . . . . . 16

      |
25 | 23, 24 | syl 16 |
. . . . . . . . . . . . . . 15
       |
26 | 25 | nnzd 10849 |
. . . . . . . . . . . . . 14
       |
27 | 26 | znegcld 10852 |
. . . . . . . . . . . . 13
        |
28 | | rpexpcl 11987 |
. . . . . . . . . . . . 13
                   |
29 | 22, 27, 28 | sylancr 663 |
. . . . . . . . . . . 12
            |
30 | 29 | rpcnd 11132 |
. . . . . . . . . . 11
            |
31 | 21, 30 | eqeltrd 2539 |
. . . . . . . . . 10
       |
32 | 31 | adantl 466 |
. . . . . . . . 9
 
       |
33 | | 1nn 10436 |
. . . . . . . . . 10
 |
34 | | eqid 2451 |
. . . . . . . . . . . 12
                                                   |
35 | 34, 3 | aaliou3lem3 21928 |
. . . . . . . . . . 11
             
         
              |
36 | 35 | simp1d 1000 |
. . . . . . . . . 10
     |
37 | 33, 36 | mp1i 12 |
. . . . . . . . 9
     |
38 | 14, 15, 1, 16, 32, 37 | isumsplit 13407 |
. . . . . . . 8
                                    |
39 | | oveq2 6200 |
. . . . . . . . . . 11
           |
40 | 39 | sumeq1d 13282 |
. . . . . . . . . 10
           
           |
41 | | aaliou3lem.e |
. . . . . . . . . 10
             |
42 | | sumex 13269 |
. . . . . . . . . 10
           |
43 | 40, 41, 42 | fvmpt 5875 |
. . . . . . . . 9
                 |
44 | 43 | oveq1d 6207 |
. . . . . . . 8
                                             |
45 | 13, 38, 44 | 3eqtr4rd 2503 |
. . . . . . 7
                   
      |
46 | | aaliou3lem.d |
. . . . . . 7
      |
47 | 45, 46 | syl6eqr 2510 |
. . . . . 6
                     |
48 | 3, 46, 41 | aaliou3lem4 21930 |
. . . . . . . . 9
 |
49 | 48 | recni 9501 |
. . . . . . . 8
 |
50 | 49 | a1i 11 |
. . . . . . 7
   |
51 | 3, 46, 41 | aaliou3lem5 21931 |
. . . . . . . 8
       |
52 | 51 | recnd 9515 |
. . . . . . 7
       |
53 | 4 | simp2d 1001 |
. . . . . . . . 9
                 |
54 | 1, 53 | syl 16 |
. . . . . . . 8
               |
55 | 54 | rpcnd 11132 |
. . . . . . 7
               |
56 | 50, 52, 55 | subaddd 9840 |
. . . . . 6
                                         |
57 | 47, 56 | mpbird 232 |
. . . . 5
 
                   |
58 | 57 | eqcomd 2459 |
. . . 4
                     |
59 | | eleq1 2523 |
. . . . 5
 
   
            
 
   
                |
60 | | breq1 4395 |
. . . . 5
 
   
            
 
   
                   
                      |
61 | 59, 60 | anbi12d 710 |
. . . 4
 
   
            
      
                                
 
          
        
        |
62 | 58, 61 | syl 16 |
. . 3
              
           
        
                 
        
        |
63 | 51 | adantr 465 |
. . . . . 6
         
                          |
64 | | simprl 755 |
. . . . . . 7
         
                            |
65 | | difrp 11127 |
. . . . . . . 8
     
               |
66 | 63, 48, 65 | sylancl 662 |
. . . . . . 7
         
                                  |
67 | 64, 66 | mpbird 232 |
. . . . . 6
         
                          |
68 | 63, 67 | ltned 9613 |
. . . . 5
         
                          |
69 | | nnnn0 10689 |
. . . . . . . . . . . . . . 15
   
   |
70 | | faccl 12164 |
. . . . . . . . . . . . . . 15
  
        |
71 | 1, 69, 70 | 3syl 20 |
. . . . . . . . . . . . . 14
         |
72 | 71 | nnzd 10849 |
. . . . . . . . . . . . 13
         |
73 | 72 | znegcld 10852 |
. . . . . . . . . . . 12
          |
74 | | rpexpcl 11987 |
. . . . . . . . . . . 12
                       |
75 | 22, 73, 74 | sylancr 663 |
. . . . . . . . . . 11
              |
76 | | rpmulcl 11115 |
. . . . . . . . . . 11
                             |
77 | 22, 75, 76 | sylancr 663 |
. . . . . . . . . 10
                |
78 | 77 | adantr 465 |
. . . . . . . . 9
         
                                   |
79 | 78 | rpred 11130 |
. . . . . . . 8
         
                                   |
80 | 63, 79 | resubcld 9879 |
. . . . . . 7
         
                                         |
81 | 48 | a1i 11 |
. . . . . . 7
         
                      |
82 | 63, 78 | ltsubrpd 11158 |
. . . . . . . 8
         
                                             |
83 | 80, 63, 81, 82, 67 | lttrd 9635 |
. . . . . . 7
         
                                         |
84 | 80, 81, 83 | ltled 9625 |
. . . . . 6
         
                                         |
85 | | simprr 756 |
. . . . . . 7
         
                         
        
      |
86 | 81, 63, 79 | lesubadd2d 10041 |
. . . . . . 7
         
                                       
             
        |
87 | 85, 86 | mpbid 210 |
. . . . . 6
         
                                 
       |
88 | 81, 63, 79 | absdifled 13025 |
. . . . . 6
         
                                                                             
         |
89 | 84, 87, 88 | mpbir2and 913 |
. . . . 5
         
                       
                     |
90 | 68, 89 | jca 532 |
. . . 4
         
                        
                          |
91 | 90 | ex 434 |
. . 3
         
                           
                       |
92 | 62, 91 | sylbid 215 |
. 2
              
           
        
    
                                |
93 | 6, 92 | mpd 15 |
1
                                |