Step | Hyp | Ref
| Expression |
1 | | fzfid 12218 |
. . . . . . . . . 10
      
     
   
         
       
            |
2 | | simpl21 1092 |
. . . . . . . . . . . . 13
       
             
             
                 |
3 | | fveere 24980 |
. . . . . . . . . . . . 13
     
           |
4 | 2, 3 | sylancom 678 |
. . . . . . . . . . . 12
       
             
             
                 |
5 | | simpl22 1093 |
. . . . . . . . . . . . 13
       
             
             
                 |
6 | | fveere 24980 |
. . . . . . . . . . . . 13
     
           |
7 | 5, 6 | sylancom 678 |
. . . . . . . . . . . 12
       
             
             
                 |
8 | 4, 7 | resubcld 10075 |
. . . . . . . . . . 11
       
             
             
                       |
9 | 8 | resqcld 12474 |
. . . . . . . . . 10
       
             
             
                           |
10 | 1, 9 | fsumrecl 13849 |
. . . . . . . . 9
      
     
   
         
       
                            |
11 | 10 | recnd 9695 |
. . . . . . . 8
      
     
   
         
       
                            |
12 | 11 | adantr 471 |
. . . . . . 7
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                            |
13 | | simpl32 1096 |
. . . . . . . . . . . . 13
       
             
             
                 |
14 | | fveere 24980 |
. . . . . . . . . . . . 13
     
           |
15 | 13, 14 | sylancom 678 |
. . . . . . . . . . . 12
       
             
             
                 |
16 | | simpl33 1097 |
. . . . . . . . . . . . 13
       
             
             
                 |
17 | | fveere 24980 |
. . . . . . . . . . . . 13
     
           |
18 | 16, 17 | sylancom 678 |
. . . . . . . . . . . 12
       
             
             
                 |
19 | 15, 18 | resubcld 10075 |
. . . . . . . . . . 11
       
             
             
                       |
20 | 19 | resqcld 12474 |
. . . . . . . . . 10
       
             
             
                           |
21 | 1, 20 | fsumrecl 13849 |
. . . . . . . . 9
      
     
   
         
       
                            |
22 | 21 | recnd 9695 |
. . . . . . . 8
      
     
   
         
       
                            |
23 | 22 | adantr 471 |
. . . . . . 7
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                            |
24 | | 0re 9669 |
. . . . . . . . . . . . 13
 |
25 | | 1re 9668 |
. . . . . . . . . . . . 13
 |
26 | 24, 25 | elicc2i 11729 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif) 

   |
27 | 26 | simp1bi 1029 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
28 | 27 | recnd 9695 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
29 | 28 | ad2antrr 737 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     
                         
                           
  |
30 | 29 | 3ad2ant1 1035 |
. . . . . . . 8
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr    
  |
31 | 30 | adantl 472 |
. . . . . . 7
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr        |
32 | | simpl11 1089 |
. . . . . . . 8
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr        |
33 | | simp12 1045 |
. . . . . . . . . 10
      
     
   
         
       
            |
34 | | simp13 1046 |
. . . . . . . . . 10
      
     
   
         
       
            |
35 | | simp21 1047 |
. . . . . . . . . 10
      
     
   
         
       
            |
36 | 33, 34, 35 | 3jca 1194 |
. . . . . . . . 9
      
     
   
         
       
      
       
       |
37 | 36 | adantr 471 |
. . . . . . . 8
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr      
       
       |
38 | | simprrl 779 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     
                         
                           
                            |
39 | 38 | 3ad2ant1 1035 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr    
                            |
40 | 39 | adantl 472 |
. . . . . . . 8
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                                  |
41 | | simp1rl 1079 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr    
  |
42 | 41 | adantl 472 |
. . . . . . . 8
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr        |
43 | | ax5seglem4 25011 |
. . . . . . . 8
                  
                            |
44 | 32, 37, 40, 42, 43 | syl211anc 1282 |
. . . . . . 7
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr        |
45 | | simpr3r 1076 |
. . . . . . . . . . 11
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr         Cgr     |
46 | | simpl13 1091 |
. . . . . . . . . . . 12
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr            |
47 | | simpl22 1093 |
. . . . . . . . . . . 12
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr            |
48 | | simpl31 1095 |
. . . . . . . . . . . 12
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr            |
49 | | simpl33 1097 |
. . . . . . . . . . . 12
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr            |
50 | | brcgr 24979 |
. . . . . . . . . . . 12
                           Cgr   
                                          |
51 | 46, 47, 48, 49, 50 | syl22anc 1277 |
. . . . . . . . . . 11
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr          Cgr 
 
                                          |
52 | 45, 51 | mpbid 215 |
. . . . . . . . . 10
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                          
                     |
53 | | simp23 1049 |
. . . . . . . . . . . . . . . 16
      
     
   
         
       
            |
54 | | simp31 1050 |
. . . . . . . . . . . . . . . 16
      
     
   
         
       
            |
55 | | simp32 1051 |
. . . . . . . . . . . . . . . 16
      
     
   
         
       
            |
56 | 53, 54, 55 | 3jca 1194 |
. . . . . . . . . . . . . . 15
      
     
   
         
       
      
       
       |
57 | 36, 56 | jca 539 |
. . . . . . . . . . . . . 14
      
     
   
         
       
                             
        |
58 | 57 | adantr 471 |
. . . . . . . . . . . . 13
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                             
        |
59 | | simpr1l 1071 |
. . . . . . . . . . . . 13
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr         ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     |
60 | | simprrr 780 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     
                         
                           
                            |
61 | 60 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr    
                            |
62 | 61 | adantl 472 |
. . . . . . . . . . . . . 14
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                                  |
63 | 40, 62 | jca 539 |
. . . . . . . . . . . . 13
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr       
                         
                            |
64 | | simpr2l 1073 |
. . . . . . . . . . . . 13
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr         Cgr     |
65 | | simpr2r 1074 |
. . . . . . . . . . . . 13
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr         Cgr     |
66 | | ax5seglem6 25013 |
. . . . . . . . . . . . 13
        
                 
       
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
  |
67 | 32, 58, 42, 59, 63, 64, 65, 66 | syl232anc 1303 |
. . . . . . . . . . . 12
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr        |
68 | 67 | oveq2d 6331 |
. . . . . . . . . . 11
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr            |
69 | 56 | adantr 471 |
. . . . . . . . . . . . . 14
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr      
       
       |
70 | | ax5seglem3 25010 |
. . . . . . . . . . . . . 14
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                    
                     |
71 | 32, 37, 69, 59, 63, 64, 65, 70 | syl322anc 1304 |
. . . . . . . . . . . . 13
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                          
                     |
72 | 67, 71 | oveq12d 6333 |
. . . . . . . . . . . 12
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                             
                      |
73 | | simpr3l 1075 |
. . . . . . . . . . . . 13
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr         Cgr     |
74 | | simpl12 1090 |
. . . . . . . . . . . . . 14
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr            |
75 | | simpl23 1094 |
. . . . . . . . . . . . . 14
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr            |
76 | | brcgr 24979 |
. . . . . . . . . . . . . 14
                           Cgr   
                                          |
77 | 74, 47, 75, 49, 76 | syl22anc 1277 |
. . . . . . . . . . . . 13
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr          Cgr 
 
                                          |
78 | 73, 77 | mpbid 215 |
. . . . . . . . . . . 12
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                          
                     |
79 | 72, 78 | oveq12d 6333 |
. . . . . . . . . . 11
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr        
                                                                                       |
80 | 68, 79 | oveq12d 6333 |
. . . . . . . . . 10
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                                                                                                        |
81 | 52, 80 | oveq12d 6333 |
. . . . . . . . 9
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                                                                             
                                                                      |
82 | 33, 34 | jca 539 |
. . . . . . . . . . . 12
      
     
   
         
       
      
           |
83 | | simp22 1048 |
. . . . . . . . . . . 12
      
     
   
         
       
            |
84 | 82, 35, 83 | jca32 542 |
. . . . . . . . . . 11
      
     
   
         
       
                              |
85 | 84 | adantr 471 |
. . . . . . . . . 10
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                              |
86 | | simp1ll 1077 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr    
  ![[,] [,]](_icc.gif)    |
87 | 86 | adantl 472 |
. . . . . . . . . 10
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr        ![[,] [,]](_icc.gif)    |
88 | | ax5seglem9 25016 |
. . . . . . . . . 10
        
                    ![[,] [,]](_icc.gif) 
                                                                                                                          |
89 | 32, 85, 87, 40, 88 | syl22anc 1277 |
. . . . . . . . 9
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                                                                                                    |
90 | | 3simpc 1013 |
. . . . . . . . . . . . 13
     
         
           |
91 | 90 | 3ad2ant3 1037 |
. . . . . . . . . . . 12
      
     
   
         
       
      
           |
92 | 53, 54, 91 | jca31 541 |
. . . . . . . . . . 11
      
     
   
         
       
                              |
93 | 92 | adantr 471 |
. . . . . . . . . 10
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                              |
94 | | simp1lr 1078 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr    
  ![[,] [,]](_icc.gif)    |
95 | 94 | adantl 472 |
. . . . . . . . . 10
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr        ![[,] [,]](_icc.gif)    |
96 | | ax5seglem9 25016 |
. . . . . . . . . 10
        
                    ![[,] [,]](_icc.gif) 
                                                                                                                          |
97 | 32, 93, 95, 62, 96 | syl22anc 1277 |
. . . . . . . . 9
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
    Cgr 
      Cgr      Cgr                                                                                                    |
98 | 81, 89, 97 | 3eqtr4d 2506 |
. . . . . . . 8
       
             
             
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     
                         
                              
 Cgr 
   |