Step | Hyp | Ref
| Expression |
1 | | simprl 755 |
. . . 4
  
 
  |
2 | | eleq1 2523 |
. . . . . . . 8
 
   |
3 | 2 | anbi1d 704 |
. . . . . . 7
   

    |
4 | 3 | anbi2d 703 |
. . . . . 6
     
 
     |
5 | | oveq2 6198 |
. . . . . . . 8
             |
6 | 5 | coeq2d 5100 |
. . . . . . 7
                           |
7 | | oveq2 6198 |
. . . . . . . 8
 
     |
8 | 7 | oveq2d 6206 |
. . . . . . 7
                 |
9 | 6, 8 | eqeq12d 2473 |
. . . . . 6
                    
                      |
10 | 4, 9 | imbi12d 320 |
. . . . 5
   
  
                     

 
                       |
11 | | eleq1 2523 |
. . . . . . . 8
 
   |
12 | 11 | anbi1d 704 |
. . . . . . 7
   
     |
13 | 12 | anbi2d 703 |
. . . . . 6
     
 
     |
14 | | oveq2 6198 |
. . . . . . . 8
             |
15 | 14 | coeq2d 5100 |
. . . . . . 7
                           |
16 | | oveq2 6198 |
. . . . . . . 8
 
     |
17 | 16 | oveq2d 6206 |
. . . . . . 7
                 |
18 | 15, 17 | eqeq12d 2473 |
. . . . . 6
                    
                      |
19 | 13, 18 | imbi12d 320 |
. . . . 5
   
  
                     
  
                       |
20 | | eleq1 2523 |
. . . . . . . 8
   
     |
21 | 20 | anbi1d 704 |
. . . . . . 7
     
  
    |
22 | 21 | anbi2d 703 |
. . . . . 6
       
   
     |
23 | | oveq2 6198 |
. . . . . . . 8
                 |
24 | 23 | coeq2d 5100 |
. . . . . . 7
                               |
25 | | oveq2 6198 |
. . . . . . . 8
   
  
    |
26 | 25 | oveq2d 6206 |
. . . . . . 7
               
     |
27 | 24, 26 | eqeq12d 2473 |
. . . . . 6
                      
                   
      |
28 | 22, 27 | imbi12d 320 |
. . . . 5
     
  
                     
  
 
                   
       |
29 | | eleq1 2523 |
. . . . . . . 8
 
   |
30 | 29 | anbi1d 704 |
. . . . . . 7
   
     |
31 | 30 | anbi2d 703 |
. . . . . 6
     
 
     |
32 | | oveq2 6198 |
. . . . . . . 8
             |
33 | 32 | coeq2d 5100 |
. . . . . . 7
                           |
34 | | oveq2 6198 |
. . . . . . . 8
 
     |
35 | 34 | oveq2d 6206 |
. . . . . . 7
                 |
36 | 33, 35 | eqeq12d 2473 |
. . . . . 6
                    
                      |
37 | 31, 36 | imbi12d 320 |
. . . . 5
   
  
                     
  
                       |
38 | | nn0cn 10690 |
. . . . . . 7

  |
39 | 38 | adantr 465 |
. . . . . 6
    
  |
40 | | addid1 9650 |
. . . . . . . 8
 
   |
41 | 40 | adantr 465 |
. . . . . . 7
  
        |
42 | | simprrr 764 |
. . . . . . . . . 10
  
      |
43 | | relexpadd.1 |
. . . . . . . . . . 11
   |
44 | | relexpadd.2 |
. . . . . . . . . . 11
   |
45 | 43, 44 | relexp0 27465 |
. . . . . . . . . 10
     
     |
46 | 42, 45 | syl 16 |
. . . . . . . . 9
  
              |
47 | | coeq2 5096 |
. . . . . . . . . 10
                                 |
48 | | coires1 5453 |
. . . . . . . . . . 11
               
    |
49 | | simprl 755 |
. . . . . . . . . . . . 13
  
      |
50 | 43, 44 | relexpdm 27471 |
. . . . . . . . . . . . 13
            |
51 | 42, 49, 50 | sylc 60 |
. . . . . . . . . . . 12
  
   
         |
52 | 42 | adantl 466 |
. . . . . . . . . . . . . 14
         

       |
53 | | simprrl 763 |
. . . . . . . . . . . . . 14
         

       |
54 | 43, 44 | relexprel 27470 |
. . . . . . . . . . . . . 14
          |
55 | 52, 53, 54 | sylc 60 |
. . . . . . . . . . . . 13
         

    
       |
56 | | relssres 5245 |
. . . . . . . . . . . . . 14
                               |
57 | 56 | adantrr 716 |
. . . . . . . . . . . . 13
               

     
                |
58 | 55, 57 | mpancom 669 |
. . . . . . . . . . . 12
         

                     |
59 | 51, 58 | mpancom 669 |
. . . . . . . . . . 11
  
                    |
60 | 48, 59 | syl5eq 2504 |
. . . . . . . . . 10
  
                     |
61 | 47, 60 | sylan9eq 2512 |
. . . . . . . . 9
      
  
 
                        |
62 | 46, 61 | mpancom 669 |
. . . . . . . 8
  
                       |
63 | | oveq2 6198 |
. . . . . . . . 9
                 |
64 | 63 | eqeq2d 2465 |
. . . . . . . 8
                      
                    |
65 | 62, 64 | syl5ibr 221 |
. . . . . . 7
                                |
66 | 41, 65 | mpcom 36 |
. . . . . 6
  
                         |
67 | 39, 66 | mpancom 669 |
. . . . 5
                          |
68 | | simprrl 763 |
. . . . . . . . . . . . 13
        
  
                          |
69 | | simprrr 764 |
. . . . . . . . . . . . . 14
                              
  
  |
70 | 69 | adantl 466 |
. . . . . . . . . . . . 13
        
  
                          |
71 | 43, 44 | relexpsucr 27466 |
. . . . . . . . . . . . 13
                   |
72 | 68, 70, 71 | sylc 60 |
. . . . . . . . . . . 12
        
  
                                        |
73 | | coeq2 5096 |
. . . . . . . . . . . . 13
                                             |
74 | 38 | adantr 465 |
. . . . . . . . . . . . . . . 16
        
  
                          |
75 | 70 | nn0cnd 10739 |
. . . . . . . . . . . . . . . 16
        
  
                          |
76 | | ax-1cn 9441 |
. . . . . . . . . . . . . . . . 17
 |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . 16
        
  
                          |
78 | 74, 75, 77 | addassd 9509 |
. . . . . . . . . . . . . . 15
        
  
                                  |
79 | 78 | eqcomd 2459 |
. . . . . . . . . . . . . 14
        
  
                         
        |
80 | | nn0addcl 10716 |
. . . . . . . . . . . . . . . . 17
 
     |
81 | 69, 80 | sylan2 474 |
. . . . . . . . . . . . . . . 16
        
  
                            |
82 | | coass 5454 |
. . . . . . . . . . . . . . . . . 18
                             |
83 | | simprl 755 |
. . . . . . . . . . . . . . . . . . . . 21
    
      
  
                        
  |
84 | 70 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . 21
    
      
  
                        
  |
85 | 68 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . 21
    
      
  
                        
  |
86 | 83, 84, 85 | jca32 535 |
. . . . . . . . . . . . . . . . . . . 20
    
      
  
                        
 
    |
87 | | simprrl 763 |
. . . . . . . . . . . . . . . . . . . . . 22
                              
  
 
                         |
88 | 87 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . 21
        
  
                         
                         |
89 | 88 | adantl 466 |
. . . . . . . . . . . . . . . . . . . 20
    
      
  
                        
 
                         |
90 | 86, 89 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
    
      
  
                        
                     |
91 | 90 | coeq1d 5099 |
. . . . . . . . . . . . . . . . . 18
    
      
  
                        
                         |
92 | 82, 91 | syl5eqr 2506 |
. . . . . . . . . . . . . . . . 17
    
      
  
                        
                         |
93 | | simpl 457 |
. . . . . . . . . . . . . . . . . 18
    
      
  
                        
    |
94 | 43, 44 | relexpsucr 27466 |
. . . . . . . . . . . . . . . . . 18
                         |
95 | 85, 93, 94 | sylc 60 |
. . . . . . . . . . . . . . . . 17
    
      
  
                        
                    |
96 | 92, 95 | eqtr4d 2495 |
. . . . . . . . . . . . . . . 16
    
      
  
                        
                         |
97 | 81, 96 | mpancom 669 |
. . . . . . . . . . . . . . 15
        
  
                                                 |
98 | | oveq2 6198 |
. . . . . . . . . . . . . . . 16
                             |
99 | 98 | eqeq2d 2465 |
. . . . . . . . . . . . . . 15
                                
                          |
100 | 97, 99 | syl5ibr 221 |
. . . . . . . . . . . . . 14
                 
  
                                           
      |
101 | 79, 100 | mpcom 36 |
. . . . . . . . . . . . 13
        
  
                                           
     |
102 | 73, 101 | sylan9eq 2512 |
. . . . . . . . . . . 12
               
   
    
                     
                              |
103 | 72, 102 | mpancom 669 |
. . . . . . . . . . 11
        
  
                                           
     |
104 | 103 | expcom 435 |
. . . . . . . . . 10
                              
  

                   
      |
105 | 104 | anassrs 648 |
. . . . . . . . 9
        
  
                      
                          |
106 | 105 | impcom 430 |
. . . . . . . 8
     
   
                                             
     |
107 | 106 | anassrs 648 |
. . . . . . 7
          
                                                  |
108 | 107 | expcom 435 |
. . . . . 6
   
  
                      
                               |
109 | 108 | expcom 435 |
. . . . 5

                           
  
 
                   
       |
110 | 10, 19, 28, 37, 67, 109 | nn0ind 10839 |
. . . 4

  
                        |
111 | 1, 110 | mpcom 36 |
. . 3
  
                       |
112 | 111 | anassrs 648 |
. 2
                          |
113 | 112 | expcom 435 |
1
  

                      |