Step | Hyp | Ref
| Expression |
1 | | sxbrsiga.0 |
. . . 4
     |
2 | | dya2ioc.1 |
. . . 4
 
                    |
3 | | dya2ioc.2 |
. . . 4
 
    |
4 | 1, 2, 3 | dya2iocucvr 29179 |
. . 3
    |
5 | | sxbrsigalem0 29166 |
. . 3
      
   
 
       |
6 | 4, 5 | eqtr4i 2496 |
. 2
       
   
 
     |
7 | | vex 3034 |
. . . . . 6
 |
8 | | vex 3034 |
. . . . . 6
 |
9 | 7, 8 | xpex 6614 |
. . . . 5
   |
10 | 3, 9 | elrnmpt2 6428 |
. . . 4

       |
11 | | simpr 468 |
. . . . . . 7
           |
12 | 1, 2 | dya2icobrsiga 29171 |
. . . . . . . . . . . . 13
𝔅ℝ |
13 | | brsigasspwrn 29081 |
. . . . . . . . . . . . 13
𝔅ℝ   |
14 | 12, 13 | sstri 3427 |
. . . . . . . . . . . 12
  |
15 | 14 | sseli 3414 |
. . . . . . . . . . 11

   |
16 | 15 | elpwid 3952 |
. . . . . . . . . 10
   |
17 | 14 | sseli 3414 |
. . . . . . . . . . 11
    |
18 | 17 | elpwid 3952 |
. . . . . . . . . 10

  |
19 | | xpinpreima2 28787 |
. . . . . . . . . 10
 
                         |
20 | 16, 18, 19 | syl2an 485 |
. . . . . . . . 9
 
                         |
21 | | reex 9648 |
. . . . . . . . . . . . . . . . 17
 |
22 | 21 | mptex 6152 |
. . . . . . . . . . . . . . . 16
        |
23 | 22 | rnex 6746 |
. . . . . . . . . . . . . . 15
        |
24 | 21 | mptex 6152 |
. . . . . . . . . . . . . . . 16
        |
25 | 24 | rnex 6746 |
. . . . . . . . . . . . . . 15
        |
26 | 23, 25 | unex 6608 |
. . . . . . . . . . . . . 14
     
   
 
     |
27 | 26 | a1i 11 |
. . . . . . . . . . . . 13
                  |
28 | 27 | sgsiga 29038 |
. . . . . . . . . . . 12
sigaGen      
   
 
      sigAlgebra |
29 | 28 | trud 1461 |
. . . . . . . . . . 11
sigaGen      
   
 
      sigAlgebra |
30 | 29 | a1i 11 |
. . . . . . . . . 10
 
 sigaGen                   sigAlgebra |
31 | | 1stpreima 28362 |
. . . . . . . . . . . . 13

             |
32 | 16, 31 | syl 17 |
. . . . . . . . . . . 12
              |
33 | | ovex 6336 |
. . . . . . . . . . . . . 14
                   |
34 | 2, 33 | elrnmpt2 6428 |
. . . . . . . . . . . . 13

                      |
35 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
                      
                    |
36 | 35 | xpeq1d 4862 |
. . . . . . . . . . . . . . . 16
                      
                        |
37 | | difxp1 5268 |
. . . . . . . . . . . . . . . . . . 19
                       
                       
   |
38 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
39 | 38 | zred 11063 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
40 | | 2rp 11330 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
42 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
43 | 41, 42 | rpexpcld 12477 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       |
44 | 39, 43 | rerpdivcld 11392 |
. . . . . . . . . . . . . . . . . . . . . 22
 
         |
45 | 44 | rexrd 9708 |
. . . . . . . . . . . . . . . . . . . . 21
 
         |
46 | | 1red 9676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
47 | 39, 46 | readdcld 9688 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
48 | 47, 43 | rerpdivcld 11392 |
. . . . . . . . . . . . . . . . . . . . . 22
 
           |
49 | 48 | rexrd 9708 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
50 | | pnfxr 11435 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
52 | 39 | lep1d 10560 |
. . . . . . . . . . . . . . . . . . . . . 22
 

    |
53 | 39, 47, 43, 52 | lediv1dd 11419 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
          |
54 | | pnfge 11455 |
. . . . . . . . . . . . . . . . . . . . . 22
        
          |
55 | 49, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
        
  |
56 | | difico 28440 |
. . . . . . . . . . . . . . . . . . . . 21
                        
               
 
                                          |
57 | 45, 49, 51, 53, 55, 56 | syl32anc 1300 |
. . . . . . . . . . . . . . . . . . . 20
 
          
                                |
58 | 57 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . 19
 
                        
                      |
59 | 37, 58 | syl5reqr 2520 |
. . . . . . . . . . . . . . . . . 18
 
                    
                       
    |
60 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 
 sigaGen      
   
 
      sigAlgebra |
61 | | ssun1 3588 |
. . . . . . . . . . . . . . . . . . . . 21
                        |
62 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
63 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
            |
64 | 63 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                     
   |
65 | 64 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 

  
 
                         |
66 | 65 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 

            
         

  
    |
67 | 44, 62, 66 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . 22
 
           

  
    |
68 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
   |
69 | | ovex 6336 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    |
70 | 69, 21 | xpex 6614 |
. . . . . . . . . . . . . . . . . . . . . . 23
      |
71 | 68, 70 | elrnmpti 5091 |
. . . . . . . . . . . . . . . . . . . . . 22
                  
                   |
72 | 67, 71 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . 21
 
          

         |
73 | 61, 72 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . 20
 
          

     
   
 
      |
74 | | elsigagen 29043 |
. . . . . . . . . . . . . . . . . . . 20
                                             
           sigaGen                    |
75 | 26, 73, 74 | sylancr 676 |
. . . . . . . . . . . . . . . . . . 19
 
          

sigaGen      
   
 
       |
76 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . 23
                           |
77 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          
              |
78 | 77 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                         
   |
79 | 78 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     

  
 
                             |
80 | 79 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     

              
           

  
    |
81 | 48, 76, 80 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . 22
 
             

  
    |
82 | 68, 70 | elrnmpti 5091 |
. . . . . . . . . . . . . . . . . . . . . 22
                    
                     |
83 | 81, 82 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . 21
 
            

         |
84 | 61, 83 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . 20
 
            

     
   
 
      |
85 | | elsigagen 29043 |
. . . . . . . . . . . . . . . . . . . 20
                                               
             sigaGen                    |
86 | 26, 84, 85 | sylancr 676 |
. . . . . . . . . . . . . . . . . . 19
 
            

sigaGen      
   
 
       |
87 | | difelsiga 29029 |
. . . . . . . . . . . . . . . . . . 19
  sigaGen      
   
 
      sigAlgebra            sigaGen      
   
 
                  sigaGen                             
               sigaGen      
   
 
       |
88 | 60, 75, 86, 87 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
 
                           sigaGen      
   
 
       |
89 | 59, 88 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . 17
 
                    
sigaGen      
   
 
       |
90 | 89 | adantr 472 |
. . . . . . . . . . . . . . . 16
                      
                    sigaGen      
   
 
       |
91 | 36, 90 | eqeltrd 2549 |
. . . . . . . . . . . . . . 15
                      
  sigaGen                    |
92 | 91 | ex 441 |
. . . . . . . . . . . . . 14
 
                     
sigaGen                     |
93 | 92 | rexlimivv 2876 |
. . . . . . . . . . . . 13
  
                    sigaGen      
   
 
       |
94 | 34, 93 | sylbi 200 |
. . . . . . . . . . . 12
  
sigaGen      
   
 
       |
95 | 32, 94 | eqeltrd 2549 |
. . . . . . . . . . 11
          sigaGen      
   
 
       |
96 | 95 | adantr 472 |
. . . . . . . . . 10
 
          sigaGen      
   
 
       |
97 | | 2ndpreima 28363 |
. . . . . . . . . . . . 13

             |
98 | 18, 97 | syl 17 |
. . . . . . . . . . . 12
              |
99 | 2, 33 | elrnmpt2 6428 |
. . . . . . . . . . . . 13

                      |
100 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
                      
                    |
101 | 100 | xpeq2d 4863 |
. . . . . . . . . . . . . . . 16
                      
                        |
102 | | difxp2 5269 |
. . . . . . . . . . . . . . . . . . 19
                                                   |
103 | 57 | xpeq2d 4863 |
. . . . . . . . . . . . . . . . . . 19
 
                                               |
104 | 102, 103 | syl5reqr 2520 |
. . . . . . . . . . . . . . . . . 18
 
                                                 |
105 | | ssun2 3589 |
. . . . . . . . . . . . . . . . . . . . 21
      
     
   
 
     |
106 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
107 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
            |
108 | 107 | xpeq2d 4863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                         |
109 | 108 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       
                         |
110 | 109 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
                      

                 |
111 | 44, 106, 110 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
                 |
112 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
 
    |
113 | | ovex 6336 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    |
114 | 21, 113 | xpex 6614 |
. . . . . . . . . . . . . . . . . . . . . . 23
      |
115 | 112, 114 | elrnmpti 5091 |
. . . . . . . . . . . . . . . . . . . . . 22
                  
                   |
116 | 111, 115 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . 21
 
                     |
117 | 105, 116 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . 20
 
                 
   
 
      |
118 | | elsigagen 29043 |
. . . . . . . . . . . . . . . . . . . 20
                                             
           sigaGen                    |
119 | 26, 117, 118 | sylancr 676 |
. . . . . . . . . . . . . . . . . . 19
 
            sigaGen      
   
 
       |
120 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . 23
                           |
121 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          
              |
122 | 121 | xpeq2d 4863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                             |
123 | 122 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           
                             |
124 | 123 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
                          

                   |
125 | 48, 120, 124 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
                   |
126 | 112, 114 | elrnmpti 5091 |
. . . . . . . . . . . . . . . . . . . . . 22
                    
                     |
127 | 125, 126 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . 21
 
                       |
128 | 105, 127 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . 20
 
                   
   
 
      |
129 | | elsigagen 29043 |
. . . . . . . . . . . . . . . . . . . 20
                                               
             sigaGen                    |
130 | 26, 128, 129 | sylancr 676 |
. . . . . . . . . . . . . . . . . . 19
 
              sigaGen      
   
 
       |
131 | | difelsiga 29029 |
. . . . . . . . . . . . . . . . . . 19
  sigaGen      
   
 
      sigAlgebra            sigaGen                               sigaGen                              
              sigaGen      
   
 
       |
132 | 60, 119, 130, 131 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
 
                           sigaGen      
   
 
       |
133 | 104, 132 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . 17
 
                     sigaGen      
   
 
       |
134 | 133 | adantr 472 |
. . . . . . . . . . . . . . . 16
                      
                    sigaGen                    |
135 | 101, 134 | eqeltrd 2549 |
. . . . . . . . . . . . . . 15
                      
  sigaGen                    |
136 | 135 | ex 441 |
. . . . . . . . . . . . . 14
 
                      sigaGen                     |
137 | 136 | rexlimivv 2876 |
. . . . . . . . . . . . 13
  
                    sigaGen      
   
 
       |
138 | 99, 137 | sylbi 200 |
. . . . . . . . . . . 12
   sigaGen      
   
 
       |
139 | 98, 138 | eqeltrd 2549 |
. . . . . . . . . . 11
          sigaGen      
   
 
       |
140 | 139 | adantl 473 |
. . . . . . . . . 10
 
          sigaGen      
   
 
       |
141 | | inelsiga 29031 |
. . . . . . . . . 10
  sigaGen      
   
 
      sigAlgebra          sigaGen      
   
 
       
      sigaGen                            
  
       sigaGen      
   
 
       |
142 | 30, 96, 140, 141 | syl3anc 1292 |
. . . . . . . . 9
 
          
  
       sigaGen      
   
 
       |
143 | 20, 142 | eqeltrd 2549 |
. . . . . . . 8
 
   sigaGen      
   
 
       |
144 | 143 | adantr 472 |
. . . . . . 7
         sigaGen      
   
 
       |
145 | 11, 144 | eqeltrd 2549 |
. . . . . 6
       sigaGen      
   
 
       |
146 | 145 | ex 441 |
. . . . 5
 
    sigaGen      
   
 
        |
147 | 146 | rexlimivv 2876 |
. . . 4
   
  sigaGen                    |
148 | 10, 147 | sylbi 200 |
. . 3
 sigaGen      
   
 
       |
149 | 148 | ssriv 3422 |
. 2
sigaGen      
   
 
      |
150 | | sigagenss2 29046 |
. 2
                    sigaGen                       
   
 
     sigaGen  sigaGen                    |
151 | 6, 149, 26, 150 | mp3an 1390 |
1
sigaGen 
sigaGen      
   
 
      |