Proof of Theorem relexpaddg
Step | Hyp | Ref
| Expression |
1 | | elnn0 10895 |
. . 3

    |
2 | | elnn0 10895 |
. . . . . . 7

    |
3 | | relexpaddnn 13191 |
. . . . . . . . . . 11
 
                |
4 | 3 | a1d 25 |
. . . . . . . . . 10
 
    
                 |
5 | 4 | 3exp 1230 |
. . . . . . . . 9
 
    
                   |
6 | 5 | com12 31 |
. . . . . . . 8
 
    
                   |
7 | | elnn1uz2 11258 |
. . . . . . . . . 10

        |
8 | | coires1 5360 |
. . . . . . . . . . . . . 14
                |
9 | | simpll 768 |
. . . . . . . . . . . . . . . . . . 19
             |
10 | | simplr 770 |
. . . . . . . . . . . . . . . . . . 19
             |
11 | 9, 10 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . 18
                 |
12 | | 1p0e1 10744 |
. . . . . . . . . . . . . . . . . 18
   |
13 | 11, 12 | syl6eq 2521 |
. . . . . . . . . . . . . . . . 17
               |
14 | | simprr 774 |
. . . . . . . . . . . . . . . . 17
             
   |
15 | 13, 14 | mpd 15 |
. . . . . . . . . . . . . . . 16
          
  |
16 | 9 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
                   |
17 | | simprl 772 |
. . . . . . . . . . . . . . . . . . 19
             |
18 | | relexp1g 13166 |
. . . . . . . . . . . . . . . . . . 19
      |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                |
20 | 16, 19 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
                |
21 | 20 | releqd 4924 |
. . . . . . . . . . . . . . . 16
                  |
22 | 15, 21 | mpbird 240 |
. . . . . . . . . . . . . . 15
          
     |
23 | | 1nn 10642 |
. . . . . . . . . . . . . . . . . 18
 |
24 | 9, 23 | syl6eqel 2557 |
. . . . . . . . . . . . . . . . 17
             |
25 | | relexpnndm 13181 |
. . . . . . . . . . . . . . . . 17
 
      |
26 | 24, 17, 25 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
          
  
  |
27 | | ssun1 3588 |
. . . . . . . . . . . . . . . 16
   |
28 | 26, 27 | syl6ss 3430 |
. . . . . . . . . . . . . . 15
          
       |
29 | | relssres 5148 |
. . . . . . . . . . . . . . 15
     
                 |
30 | 22, 28, 29 | syl2anc 673 |
. . . . . . . . . . . . . 14
                       |
31 | 8, 30 | syl5eq 2517 |
. . . . . . . . . . . . 13
                        |
32 | 10 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
                   |
33 | | relexp0g 13162 |
. . . . . . . . . . . . . . . 16
         |
34 | 17, 33 | syl 17 |
. . . . . . . . . . . . . . 15
                   |
35 | 32, 34 | eqtrd 2505 |
. . . . . . . . . . . . . 14
             
     |
36 | 35 | coeq2d 5002 |
. . . . . . . . . . . . 13
                             |
37 | 10 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
                 |
38 | | ax-1cn 9615 |
. . . . . . . . . . . . . . . . 17
 |
39 | 9, 38 | syl6eqel 2557 |
. . . . . . . . . . . . . . . 16
             |
40 | 39 | addid1d 9851 |
. . . . . . . . . . . . . . 15
               |
41 | 37, 40 | eqtrd 2505 |
. . . . . . . . . . . . . 14
               |
42 | 41 | oveq2d 6324 |
. . . . . . . . . . . . 13
                     |
43 | 31, 36, 42 | 3eqtr4d 2515 |
. . . . . . . . . . . 12
                          |
44 | 43 | exp43 623 |
. . . . . . . . . . 11
 
    
                   |
45 | | simp1 1030 |
. . . . . . . . . . . . . . . . 17
             |
46 | | simp3 1032 |
. . . . . . . . . . . . . . . . 17
         |
47 | | relexpuzrel 13192 |
. . . . . . . . . . . . . . . . 17
       
    |
48 | 45, 46, 47 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
       
    |
49 | | eluz2nn 11221 |
. . . . . . . . . . . . . . . . . . 19
    
  |
50 | 45, 49 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         |
51 | 50, 46, 25 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
       
    |
52 | 51, 27 | syl6ss 3430 |
. . . . . . . . . . . . . . . 16
       
      |
53 | 48, 52, 29 | syl2anc 673 |
. . . . . . . . . . . . . . 15
                   |
54 | 8, 53 | syl5eq 2517 |
. . . . . . . . . . . . . 14
                    |
55 | | simp2 1031 |
. . . . . . . . . . . . . . . . 17
         |
56 | 55 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
               |
57 | 46, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
               |
58 | 56, 57 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
               |
59 | 58 | coeq2d 5002 |
. . . . . . . . . . . . . 14
                         |
60 | 55 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
       
     |
61 | | eluzelcn 11194 |
. . . . . . . . . . . . . . . . . 18
    
  |
62 | 45, 61 | syl 17 |
. . . . . . . . . . . . . . . . 17
         |
63 | 62 | addid1d 9851 |
. . . . . . . . . . . . . . . 16
       
   |
64 | 60, 63 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
       
   |
65 | 64 | oveq2d 6324 |
. . . . . . . . . . . . . 14
                 |
66 | 54, 59, 65 | 3eqtr4d 2515 |
. . . . . . . . . . . . 13
                      |
67 | 66 | a1d 25 |
. . . . . . . . . . . 12
          
                 |
68 | 67 | 3exp 1230 |
. . . . . . . . . . 11
    
 
   
                   |
69 | 44, 68 | jaoi 386 |
. . . . . . . . . 10
        
                       |
70 | 7, 69 | sylbi 200 |
. . . . . . . . 9
 
    
                   |
71 | 70 | com12 31 |
. . . . . . . 8
 
    
                   |
72 | 6, 71 | jaoi 386 |
. . . . . . 7
 
 

                       |
73 | 2, 72 | sylbi 200 |
. . . . . 6

 
   
                   |
74 | 73 | com12 31 |
. . . . 5
 

   
                   |
75 | 74 | 3impd 1247 |
. . . 4
     
 
                |
76 | | elnn1uz2 11258 |
. . . . . . . . 9

        |
77 | | coires1 5360 |
. . . . . . . . . . . . . . 15
         
 
    |
78 | | relcnv 5213 |
. . . . . . . . . . . . . . . . 17
  |
79 | | ssun1 3588 |
. . . . . . . . . . . . . . . . 17
  
   |
80 | 78, 79 | pm3.2i 462 |
. . . . . . . . . . . . . . . 16
 
  
    |
81 | | relssres 5148 |
. . . . . . . . . . . . . . . 16
   
 
             |
82 | 80, 81 | mp1i 13 |
. . . . . . . . . . . . . . 15
                     |
83 | 77, 82 | syl5eq 2517 |
. . . . . . . . . . . . . 14
            
 
       |
84 | | cnvco 5025 |
. . . . . . . . . . . . . . 15
               
    |
85 | | simplr 770 |
. . . . . . . . . . . . . . . . . . 19
             |
86 | | 1nn0 10909 |
. . . . . . . . . . . . . . . . . . 19
 |
87 | 85, 86 | syl6eqel 2557 |
. . . . . . . . . . . . . . . . . 18
             |
88 | | simprl 772 |
. . . . . . . . . . . . . . . . . 18
             |
89 | | relexpcnv 13175 |
. . . . . . . . . . . . . . . . . 18
 
      
    |
90 | 87, 88, 89 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
                     |
91 | 85 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
                     |
92 | | cnvexg 6758 |
. . . . . . . . . . . . . . . . . . 19
 
  |
93 | 88, 92 | syl 17 |
. . . . . . . . . . . . . . . . . 18
              |
94 | | relexp1g 13166 |
. . . . . . . . . . . . . . . . . 18
   
     |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . 17
                  |
96 | 90, 91, 95 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . 16
                  |
97 | | simpll 768 |
. . . . . . . . . . . . . . . . . . 19
             |
98 | | 0nn0 10908 |
. . . . . . . . . . . . . . . . . . 19
 |
99 | 97, 98 | syl6eqel 2557 |
. . . . . . . . . . . . . . . . . 18
             |
100 | | relexpcnv 13175 |
. . . . . . . . . . . . . . . . . 18
 
      
    |
101 | 99, 88, 100 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
                     |
102 | 97 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
                     |
103 | | relexp0g 13162 |
. . . . . . . . . . . . . . . . . 18
   
 
       |
104 | 93, 103 | syl 17 |
. . . . . . . . . . . . . . . . 17
                
     |
105 | 101, 102,
104 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . 16
                
     |
106 | 96, 105 | coeq12d 5004 |
. . . . . . . . . . . . . . 15
                      
 
      |
107 | 84, 106 | syl5eq 2517 |
. . . . . . . . . . . . . 14
                              |
108 | 99, 87 | nn0addcld 10953 |
. . . . . . . . . . . . . . . 16
               |
109 | | relexpcnv 13175 |
. . . . . . . . . . . . . . . 16
   
               |
110 | 108, 88, 109 | syl2anc 673 |
. . . . . . . . . . . . . . 15
                         |
111 | 97, 85 | oveq12d 6326 |
. . . . . . . . . . . . . . . . 17
                 |
112 | | 0p1e1 10743 |
. . . . . . . . . . . . . . . . 17
   |
113 | 111, 112 | syl6eq 2521 |
. . . . . . . . . . . . . . . 16
               |
114 | 113 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
                       |
115 | 110, 114,
95 | 3eqtrd 2509 |
. . . . . . . . . . . . . 14
                    |
116 | 83, 107, 115 | 3eqtr4d 2515 |
. . . . . . . . . . . . 13
                            |
117 | | relco 5340 |
. . . . . . . . . . . . . 14
         |
118 | | simprr 774 |
. . . . . . . . . . . . . . . 16
             
   |
119 | 113, 118 | mpd 15 |
. . . . . . . . . . . . . . 15
          
  |
120 | 113 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
                     |
121 | 88, 18 | syl 17 |
. . . . . . . . . . . . . . . . 17
                |
122 | 120, 121 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
                  |
123 | 122 | releqd 4924 |
. . . . . . . . . . . . . . 15
                    |
124 | 119, 123 | mpbird 240 |
. . . . . . . . . . . . . 14
          
       |
125 | | cnveqb 5298 |
. . . . . . . . . . . . . 14
                             
                  |
126 | 117, 124,
125 | sylancr 676 |
. . . . . . . . . . . . 13
                                           |
127 | 116, 126 | mpbird 240 |
. . . . . . . . . . . 12
                          |
128 | 127 | exp43 623 |
. . . . . . . . . . 11
 
    
                   |
129 | 128 | com12 31 |
. . . . . . . . . 10
 
    
                   |
130 | | coires1 5360 |
. . . . . . . . . . . . . . . . 17
  
   
               |
131 | | simp2 1031 |
. . . . . . . . . . . . . . . . . . 19
             |
132 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . . 20
         |
133 | 132, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
       
  |
134 | | relexpuzrel 13192 |
. . . . . . . . . . . . . . . . . . 19
      
       |
135 | 131, 133,
134 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
        
    |
136 | | eluz2nn 11221 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
137 | 131, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
         |
138 | | relexpnndm 13181 |
. . . . . . . . . . . . . . . . . . . 20
  

   
   |
139 | 137, 133,
138 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
        
     |
140 | 139, 79 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . 18
        
   
    |
141 | | relssres 5148 |
. . . . . . . . . . . . . . . . . 18
         
                     |
142 | 135, 140,
141 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
             
         |
143 | 130, 142 | syl5eq 2517 |
. . . . . . . . . . . . . . . 16
             
          |
144 | | simp1 1030 |
. . . . . . . . . . . . . . . . . . 19
         |
145 | 144 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
        
   
    |
146 | 133, 103 | syl 17 |
. . . . . . . . . . . . . . . . . 18
        
 
       |
147 | 145, 146 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
        
 
       |
148 | 147 | coeq2d 5002 |
. . . . . . . . . . . . . . . 16
             
         
      |
149 | 144 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
       
     |
150 | | eluzelcn 11194 |
. . . . . . . . . . . . . . . . . . . 20
    
  |
151 | 131, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
         |
152 | 151 | addid2d 9852 |
. . . . . . . . . . . . . . . . . 18
           |
153 | 149, 152 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
       
   |
154 | 153 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
        
     
    |
155 | 143, 148,
154 | 3eqtr4d 2515 |
. . . . . . . . . . . . . . 15
             
           |
156 | | nnnn0 10900 |
. . . . . . . . . . . . . . . . . . 19
   |
157 | 131, 136,
156 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
         |
158 | 157, 132,
89 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
        
   
    |
159 | 144, 98 | syl6eqel 2557 |
. . . . . . . . . . . . . . . . . 18
         |
160 | 159, 132,
100 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
        
   
    |
161 | 158, 160 | coeq12d 5004 |
. . . . . . . . . . . . . . . 16
             
               |
162 | 84, 161 | syl5eq 2517 |
. . . . . . . . . . . . . . 15
                  
   
     |
163 | 159, 157 | nn0addcld 10953 |
. . . . . . . . . . . . . . . 16
       
   |
164 | 163, 132,
109 | syl2anc 673 |
. . . . . . . . . . . . . . 15
        
     
      |
165 | 155, 162,
164 | 3eqtr4d 2515 |
. . . . . . . . . . . . . 14
                        |
166 | 159 | nn0cnd 10951 |
. . . . . . . . . . . . . . . . . 18
         |
167 | 151, 166 | addcomd 9853 |
. . . . . . . . . . . . . . . . 17
       
     |
168 | | uzaddcl 11238 |
. . . . . . . . . . . . . . . . . 18
       
       |
169 | 131, 159,
168 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
       
       |
170 | 167, 169 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . 16
       
       |
171 | | relexpuzrel 13192 |
. . . . . . . . . . . . . . . 16
         
      |
172 | 170, 132,
171 | syl2anc 673 |
. . . . . . . . . . . . . . 15
       
      |
173 | 117, 172,
125 | sylancr 676 |
. . . . . . . . . . . . . 14
                                       |
174 | 165, 173 | mpbird 240 |
. . . . . . . . . . . . 13
                      |
175 | 174 | a1d 25 |
. . . . . . . . . . . 12
          
                 |
176 | 175 | 3exp 1230 |
. . . . . . . . . . 11
 
    
   
                   |
177 | 176 | com12 31 |
. . . . . . . . . 10
    
 
   
                   |
178 | 129, 177 | jaoi 386 |
. . . . . . . . 9
        
                       |
179 | 76, 178 | sylbi 200 |
. . . . . . . 8
 
    
                   |
180 | | coires1 5360 |
. . . . . . . . . . . . 13
                |
181 | | simp3 1032 |
. . . . . . . . . . . . . . 15
     |
182 | | relexp0rel 13177 |
. . . . . . . . . . . . . . 15
 
    |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . . . 14
  
     |
184 | 181, 33 | syl 17 |
. . . . . . . . . . . . . . . . 17
           |
185 | 184 | dmeqd 5042 |
. . . . . . . . . . . . . . . 16
  
        |
186 | | dmresi 5166 |
. . . . . . . . . . . . . . . 16
      |
187 | 185, 186 | syl6eq 2521 |
. . . . . . . . . . . . . . 15
  
       |
188 | | eqimss 3470 |
. . . . . . . . . . . . . . 15
     
       |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . . . 14
  
       |
190 | | relssres 5148 |
. . . . . . . . . . . . . 14
                       |
191 | 183, 189,
190 | syl2anc 673 |
. . . . . . . . . . . . 13
               |
192 | 180, 191 | syl5eq 2517 |
. . . . . . . . . . . 12
                |
193 | | simp1 1030 |
. . . . . . . . . . . . . 14
     |
194 | 193 | oveq2d 6324 |
. . . . . . . . . . . . 13
           |
195 | | simp2 1031 |
. . . . . . . . . . . . . . 15
     |
196 | 195 | oveq2d 6324 |
. . . . . . . . . . . . . 14
           |
197 | 196, 184 | eqtrd 2505 |
. . . . . . . . . . . . 13
     
     |
198 | 194, 197 | coeq12d 5004 |
. . . . . . . . . . . 12
                     |
199 | 193, 195 | oveq12d 6326 |
. . . . . . . . . . . . . 14
         |
200 | | 00id 9826 |
. . . . . . . . . . . . . 14
   |
201 | 199, 200 | syl6eq 2521 |
. . . . . . . . . . . . 13
       |
202 | 201 | oveq2d 6324 |
. . . . . . . . . . . 12
             |
203 | 192, 198,
202 | 3eqtr4d 2515 |
. . . . . . . . . . 11
                  |
204 | 203 | a1d 25 |
. . . . . . . . . 10
       
                |
205 | 204 | 3exp 1230 |
. . . . . . . . 9
 
    
                   |
206 | 205 | com12 31 |
. . . . . . . 8
 
    
                   |
207 | 179, 206 | jaoi 386 |
. . . . . . 7
 
 

                       |
208 | 2, 207 | sylbi 200 |
. . . . . 6

 
   
                   |
209 | 208 | com12 31 |
. . . . 5
 

   
                   |
210 | 209 | 3impd 1247 |
. . . 4
     
 
                |
211 | 75, 210 | jaoi 386 |
. . 3
 
  
                     |
212 | 1, 211 | sylbi 200 |
. 2

 
  
 
                |
213 | 212 | imp 436 |
1
  
  
                  |