Step | Hyp | Ref
| Expression |
1 | | opklefing 4449 |
. . . 4
  Nn Nn     fin  Nn      |
2 | 1 | 3adant3 975 |
. . 3
  Nn Nn Nn     fin  Nn      |
3 | | addcnnul 4454 |
. . . . . . . . . 10
  

   |
4 | 3 | simpld 445 |
. . . . . . . . 9
  
  |
5 | 4 | a1i 10 |
. . . . . . . 8
   Nn Nn Nn   
   |
6 | | nncaddccl 4420 |
. . . . . . . . . . . . . 14
  Nn Nn   Nn  |
7 | 6 | 3adant1 973 |
. . . . . . . . . . . . 13
  Nn Nn Nn   Nn  |
8 | | addcass 4416 |
. . . . . . . . . . . . . . 15
         |
9 | | addceq1 4384 |
. . . . . . . . . . . . . . 15
              1c      1c  |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . . . 14
     1c   
 
1c |
11 | 10 | a1i 10 |
. . . . . . . . . . . . 13
  Nn Nn Nn      1c   
 
1c  |
12 | | addceq2 4385 |
. . . . . . . . . . . . . . . 16
  
        |
13 | | addceq1 4384 |
. . . . . . . . . . . . . . . 16
    
 
 
 1c      1c  |
14 | 12, 13 | syl 15 |
. . . . . . . . . . . . . . 15
  
 
 1c      1c  |
15 | 14 | eqeq2d 2364 |
. . . . . . . . . . . . . 14
  
    
 1c    1c      1c      1c   |
16 | 15 | rspcev 2956 |
. . . . . . . . . . . . 13
   
Nn      1c      1c  Nn      1c   
1c  |
17 | 7, 11, 16 | syl2anc 642 |
. . . . . . . . . . . 12
  Nn Nn Nn  Nn    
 1c    1c  |
18 | | eqeq1 2359 |
. . . . . . . . . . . . 13
     
1c

   1c    
 1c    1c   |
19 | 18 | rexbidv 2636 |
. . . . . . . . . . . 12
     
1c
 
Nn    1c  Nn      1c    1c   |
20 | 17, 19 | syl5ibrcom 213 |
. . . . . . . . . . 11
  Nn Nn Nn      
1c
 Nn   
1c   |
21 | 20 | 3expa 1151 |
. . . . . . . . . 10
   Nn Nn Nn 
     1c  Nn    1c   |
22 | 21 | adantllr 699 |
. . . . . . . . 9
    Nn Nn
Nn Nn 
     1c  Nn    1c   |
23 | 22 | rexlimdva 2739 |
. . . . . . . 8
   Nn Nn Nn   Nn      1c  Nn    1c   |
24 | 5, 23 | anim12d 546 |
. . . . . . 7
   Nn Nn Nn    

Nn      1c   Nn    1c    |
25 | | addcexg 4394 |
. . . . . . . . 9
  Nn Nn     |
26 | 25 | adantlr 695 |
. . . . . . . 8
   Nn Nn Nn 

  |
27 | | simplr 731 |
. . . . . . . 8
   Nn Nn Nn
Nn  |
28 | | opkltfing 4450 |
. . . . . . . 8
   
Nn       fin   

Nn      1c    |
29 | 26, 27, 28 | syl2anc 642 |
. . . . . . 7
   Nn Nn Nn       fin   

Nn      1c    |
30 | | opkltfing 4450 |
. . . . . . . 8
  Nn Nn     fin 
 Nn   
1c    |
31 | 30 | adantr 451 |
. . . . . . 7
   Nn Nn Nn     fin  
Nn    1c    |
32 | 24, 29, 31 | 3imtr4d 259 |
. . . . . 6
   Nn Nn Nn       fin    fin   |
33 | | opkeq1 4060 |
. . . . . . . 8
  
          |
34 | 33 | eleq1d 2419 |
. . . . . . 7
  
    fin    
 fin   |
35 | 34 | imbi1d 308 |
. . . . . 6
  
     fin    fin       fin    fin    |
36 | 32, 35 | syl5ibrcom 213 |
. . . . 5
   Nn Nn Nn 
      fin    fin    |
37 | 36 | rexlimdva 2739 |
. . . 4
  Nn Nn  
Nn       fin    fin    |
38 | 37 | 3adant2 974 |
. . 3
  Nn Nn Nn  
Nn       fin    fin    |
39 | 2, 38 | sylbid 206 |
. 2
  Nn Nn Nn     fin     fin    fin    |
40 | 39 | imp3a 420 |
1
  Nn Nn Nn      fin    fin    fin   |