Proof of Theorem relexpaddss
Step | Hyp | Ref
| Expression |
1 | | elnn0 10899 |
. . 3

    |
2 | | elnn0 10899 |
. . . . . 6

    |
3 | 2 | biimpi 199 |
. . . . 5

    |
4 | | relexpaddnn 13162 |
. . . . . . . 8
 
                |
5 | | eqimss 3495 |
. . . . . . . 8
                      
      |
6 | 4, 5 | syl 17 |
. . . . . . 7
 
        
       |
7 | 6 | 3exp 1214 |
. . . . . 6
 
        
         |
8 | | elnn1uz2 11263 |
. . . . . . 7

        |
9 | | relco 5351 |
. . . . . . . . . . . . . 14
      |
10 | | dfrel2 5304 |
. . . . . . . . . . . . . . 15
                    |
11 | 10 | biimpi 199 |
. . . . . . . . . . . . . 14
     
       
      |
12 | 9, 11 | ax-mp 5 |
. . . . . . . . . . . . 13
       
     |
13 | | cnvco 5038 |
. . . . . . . . . . . . . . . . 17
        
     |
14 | | cnvresid 5674 |
. . . . . . . . . . . . . . . . . 18

       |
15 | 14 | coeq2i 5013 |
. . . . . . . . . . . . . . . . 17
  
     
     |
16 | | coires1 5371 |
. . . . . . . . . . . . . . . . 17
            |
17 | 13, 15, 16 | 3eqtri 2487 |
. . . . . . . . . . . . . . . 16
       
    |
18 | | eqimss 3495 |
. . . . . . . . . . . . . . . 16
        
  
     
       |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . . 15
     
      |
20 | | cnvss 5025 |
. . . . . . . . . . . . . . 15
      
           
  
     |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . 14
      
  
    |
22 | | resss 5146 |
. . . . . . . . . . . . . . 15
 
  
  |
23 | | cnvss 5025 |
. . . . . . . . . . . . . . 15
  
      
  
    |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . 14
  
      |
25 | 21, 24 | sstri 3452 |
. . . . . . . . . . . . 13
      
   |
26 | 12, 25 | eqsstr3i 3474 |
. . . . . . . . . . . 12

       |
27 | | cnvcnvss 5308 |
. . . . . . . . . . . 12
   |
28 | 26, 27 | sstri 3452 |
. . . . . . . . . . 11

     |
29 | 28 | a1i 11 |
. . . . . . . . . 10
          |
30 | | simp1 1014 |
. . . . . . . . . . . . 13
     |
31 | 30 | oveq2d 6330 |
. . . . . . . . . . . 12
           |
32 | | relexp0g 13133 |
. . . . . . . . . . . . 13
         |
33 | 32 | 3ad2ant3 1037 |
. . . . . . . . . . . 12
           |
34 | 31, 33 | eqtrd 2495 |
. . . . . . . . . . 11
     
     |
35 | | simp2 1015 |
. . . . . . . . . . . . 13
     |
36 | 35 | oveq2d 6330 |
. . . . . . . . . . . 12
           |
37 | | relexp1g 13137 |
. . . . . . . . . . . . 13
      |
38 | 37 | 3ad2ant3 1037 |
. . . . . . . . . . . 12
        |
39 | 36, 38 | eqtrd 2495 |
. . . . . . . . . . 11
        |
40 | 34, 39 | coeq12d 5017 |
. . . . . . . . . 10
                  |
41 | 30, 35 | oveq12d 6332 |
. . . . . . . . . . . . 13
         |
42 | | 1cnd 9684 |
. . . . . . . . . . . . . 14
     |
43 | 42 | addid2d 9859 |
. . . . . . . . . . . . 13
       |
44 | 41, 43 | eqtrd 2495 |
. . . . . . . . . . . 12
       |
45 | 44 | oveq2d 6330 |
. . . . . . . . . . 11
             |
46 | 45, 38 | eqtrd 2495 |
. . . . . . . . . 10
          |
47 | 29, 40, 46 | 3sstr4d 3486 |
. . . . . . . . 9
           
      |
48 | 47 | 3exp 1214 |
. . . . . . . 8
 
        
         |
49 | | coires1 5371 |
. . . . . . . . . . . . . 14
  
        
      |
50 | | simp2 1015 |
. . . . . . . . . . . . . . . 16
             |
51 | | cnvexg 6765 |
. . . . . . . . . . . . . . . . 17
 
  |
52 | 51 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . 16
       
  |
53 | | relexpuzrel 13163 |
. . . . . . . . . . . . . . . 16
      
       |
54 | 50, 52, 53 | syl2anc 671 |
. . . . . . . . . . . . . . 15
        
    |
55 | | eluz2nn 11225 |
. . . . . . . . . . . . . . . . . 18
    
  |
56 | 50, 55 | syl 17 |
. . . . . . . . . . . . . . . . 17
         |
57 | | relexpnndm 13152 |
. . . . . . . . . . . . . . . . 17
  

   
   |
58 | 56, 52, 57 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
        
     |
59 | | df-rn 4863 |
. . . . . . . . . . . . . . . . 17
  |
60 | | ssun2 3609 |
. . . . . . . . . . . . . . . . 17
   |
61 | 59, 60 | eqsstr3i 3474 |
. . . . . . . . . . . . . . . 16
    |
62 | 58, 61 | syl6ss 3455 |
. . . . . . . . . . . . . . 15
        
      |
63 | | relssres 5160 |
. . . . . . . . . . . . . . 15
         
  
  
      
    |
64 | 54, 62, 63 | syl2anc 671 |
. . . . . . . . . . . . . 14
                
    |
65 | 49, 64 | syl5eq 2507 |
. . . . . . . . . . . . 13
                      |
66 | | cnvco 5038 |
. . . . . . . . . . . . . 14
              
     |
67 | | eluzge2nn0 11226 |
. . . . . . . . . . . . . . . . 17
    
  |
68 | 50, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
         |
69 | | simp3 1016 |
. . . . . . . . . . . . . . . 16
         |
70 | | relexpcnv 13146 |
. . . . . . . . . . . . . . . 16
 
      
    |
71 | 68, 69, 70 | syl2anc 671 |
. . . . . . . . . . . . . . 15
        
   
    |
72 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
       
  
     |
73 | 71, 72 | coeq12d 5017 |
. . . . . . . . . . . . . 14
            
               |
74 | 66, 73 | syl5eq 2507 |
. . . . . . . . . . . . 13
                  
        |
75 | 65, 74, 71 | 3eqtr4d 2505 |
. . . . . . . . . . . 12
                      |
76 | | relco 5351 |
. . . . . . . . . . . . 13
         |
77 | | relexpuzrel 13163 |
. . . . . . . . . . . . . 14
       
    |
78 | 77 | 3adant1 1032 |
. . . . . . . . . . . . 13
       
    |
79 | | cnveqb 5309 |
. . . . . . . . . . . . 13
                         
                |
80 | 76, 78, 79 | sylancr 674 |
. . . . . . . . . . . 12
                                   |
81 | 75, 80 | mpbird 240 |
. . . . . . . . . . 11
                    |
82 | | simp1 1014 |
. . . . . . . . . . . . . 14
         |
83 | 82 | oveq2d 6330 |
. . . . . . . . . . . . 13
               |
84 | 32 | 3ad2ant3 1037 |
. . . . . . . . . . . . 13
               |
85 | 83, 84 | eqtrd 2495 |
. . . . . . . . . . . 12
               |
86 | 85 | coeq1d 5014 |
. . . . . . . . . . 11
               
         |
87 | 82 | oveq1d 6329 |
. . . . . . . . . . . . 13
       
     |
88 | | eluzelcn 11198 |
. . . . . . . . . . . . . . 15
    
  |
89 | 50, 88 | syl 17 |
. . . . . . . . . . . . . 14
         |
90 | 89 | addid2d 9859 |
. . . . . . . . . . . . 13
           |
91 | 87, 90 | eqtrd 2495 |
. . . . . . . . . . . 12
       
   |
92 | 91 | oveq2d 6330 |
. . . . . . . . . . 11
                 |
93 | 81, 86, 92 | 3eqtr4d 2505 |
. . . . . . . . . 10
                      |
94 | 93, 5 | syl 17 |
. . . . . . . . 9
              
       |
95 | 94 | 3exp 1214 |
. . . . . . . 8
 
    
       
         |
96 | 48, 95 | jaod 386 |
. . . . . . 7
        
        
        |
97 | 8, 96 | syl5bi 225 |
. . . . . 6
 
        
         |
98 | 7, 97 | jaoi 385 |
. . . . 5
 
 

       
         |
99 | 3, 98 | syl 17 |
. . . 4

 
       
         |
100 | | elnn1uz2 11263 |
. . . . . . . 8

        |
101 | 100 | biimpi 199 |
. . . . . . 7
 
       |
102 | | coires1 5371 |
. . . . . . . . . . . 12
          |
103 | | resss 5146 |
. . . . . . . . . . . 12
     |
104 | 102, 103 | eqsstri 3473 |
. . . . . . . . . . 11
      |
105 | 104 | a1i 11 |
. . . . . . . . . 10
   
      |
106 | | simp1 1014 |
. . . . . . . . . . . . 13
     |
107 | 106 | oveq2d 6330 |
. . . . . . . . . . . 12
           |
108 | 37 | 3ad2ant3 1037 |
. . . . . . . . . . . 12
        |
109 | 107, 108 | eqtrd 2495 |
. . . . . . . . . . 11
        |
110 | | simp2 1015 |
. . . . . . . . . . . . 13
     |
111 | 110 | oveq2d 6330 |
. . . . . . . . . . . 12
           |
112 | 32 | 3ad2ant3 1037 |
. . . . . . . . . . . 12
           |
113 | 111, 112 | eqtrd 2495 |
. . . . . . . . . . 11
     
     |
114 | 109, 113 | coeq12d 5017 |
. . . . . . . . . 10
                  |
115 | 106, 110 | oveq12d 6332 |
. . . . . . . . . . . . 13
         |
116 | | 1cnd 9684 |
. . . . . . . . . . . . . 14
     |
117 | 116 | addid1d 9858 |
. . . . . . . . . . . . 13
       |
118 | 115, 117 | eqtrd 2495 |
. . . . . . . . . . . 12
       |
119 | 118 | oveq2d 6330 |
. . . . . . . . . . 11
             |
120 | 119, 108 | eqtrd 2495 |
. . . . . . . . . 10
          |
121 | 105, 114,
120 | 3sstr4d 3486 |
. . . . . . . . 9
           
      |
122 | 121 | 3exp 1214 |
. . . . . . . 8
 
        
         |
123 | | coires1 5371 |
. . . . . . . . . . . 12
                |
124 | | relexpuzrel 13163 |
. . . . . . . . . . . . . 14
       
    |
125 | 124 | 3adant2 1033 |
. . . . . . . . . . . . 13
       
    |
126 | | simp1 1014 |
. . . . . . . . . . . . . . . 16
             |
127 | | eluz2nn 11225 |
. . . . . . . . . . . . . . . 16
    
  |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . 15
         |
129 | | simp3 1016 |
. . . . . . . . . . . . . . 15
         |
130 | | relexpnndm 13152 |
. . . . . . . . . . . . . . 15
 
      |
131 | 128, 129,
130 | syl2anc 671 |
. . . . . . . . . . . . . 14
       
    |
132 | | ssun1 3608 |
. . . . . . . . . . . . . 14
   |
133 | 131, 132 | syl6ss 3455 |
. . . . . . . . . . . . 13
       
      |
134 | | relssres 5160 |
. . . . . . . . . . . . 13
     
                 |
135 | 125, 133,
134 | syl2anc 671 |
. . . . . . . . . . . 12
                   |
136 | 123, 135 | syl5eq 2507 |
. . . . . . . . . . 11
                    |
137 | | simp2 1015 |
. . . . . . . . . . . . . 14
         |
138 | 137 | oveq2d 6330 |
. . . . . . . . . . . . 13
               |
139 | 32 | 3ad2ant3 1037 |
. . . . . . . . . . . . 13
               |
140 | 138, 139 | eqtrd 2495 |
. . . . . . . . . . . 12
               |
141 | 140 | coeq2d 5015 |
. . . . . . . . . . 11
                         |
142 | 137 | oveq2d 6330 |
. . . . . . . . . . . . 13
       
     |
143 | | eluzelcn 11198 |
. . . . . . . . . . . . . . 15
    
  |
144 | 126, 143 | syl 17 |
. . . . . . . . . . . . . 14
         |
145 | 144 | addid1d 9858 |
. . . . . . . . . . . . 13
       
   |
146 | 142, 145 | eqtrd 2495 |
. . . . . . . . . . . 12
       
   |
147 | 146 | oveq2d 6330 |
. . . . . . . . . . 11
                 |
148 | 136, 141,
147 | 3eqtr4d 2505 |
. . . . . . . . . 10
                      |
149 | 148, 5 | syl 17 |
. . . . . . . . 9
              
       |
150 | 149 | 3exp 1214 |
. . . . . . . 8
    
 
       
         |
151 | 122, 150 | jaoi 385 |
. . . . . . 7
        
        
        |
152 | 101, 151 | syl 17 |
. . . . . 6
 
        
         |
153 | | coires1 5371 |
. . . . . . . . . 10

               |
154 | | resres 5135 |
. . . . . . . . . 10

  
           |
155 | | inidm 3652 |
. . . . . . . . . . 11
         |
156 | 155 | reseq2i 5120 |
. . . . . . . . . 10
           |
157 | 153, 154,
156 | 3eqtri 2487 |
. . . . . . . . 9

           |
158 | | simp1 1014 |
. . . . . . . . . . . 12
     |
159 | 158 | oveq2d 6330 |
. . . . . . . . . . 11
           |
160 | 32 | 3ad2ant3 1037 |
. . . . . . . . . . 11
           |
161 | 159, 160 | eqtrd 2495 |
. . . . . . . . . 10
     
     |
162 | | simp2 1015 |
. . . . . . . . . . . 12
     |
163 | 162 | oveq2d 6330 |
. . . . . . . . . . 11
           |
164 | 163, 160 | eqtrd 2495 |
. . . . . . . . . 10
     
     |
165 | 161, 164 | coeq12d 5017 |
. . . . . . . . 9
                     |
166 | 158, 162 | oveq12d 6332 |
. . . . . . . . . . . 12
         |
167 | | 00id 9833 |
. . . . . . . . . . . . 13
   |
168 | 167 | a1i 11 |
. . . . . . . . . . . 12
       |
169 | 166, 168 | eqtrd 2495 |
. . . . . . . . . . 11
       |
170 | 169 | oveq2d 6330 |
. . . . . . . . . 10
             |
171 | 170, 160 | eqtrd 2495 |
. . . . . . . . 9
             |
172 | 157, 165,
171 | 3eqtr4a 2521 |
. . . . . . . 8
                  |
173 | 172, 5 | syl 17 |
. . . . . . 7
           
      |
174 | 173 | 3exp 1214 |
. . . . . 6
 
        
         |
175 | 152, 174 | jaoi 385 |
. . . . 5
 
 

       
         |
176 | 3, 175 | syl 17 |
. . . 4

 
       
         |
177 | 99, 176 | jaod 386 |
. . 3

 
 
        
        |
178 | 1, 177 | syl5bi 225 |
. 2


        
         |
179 | 178 | 3imp 1208 |
1
 
        
       |