Step | Hyp | Ref
| Expression |
1 | | n0 3560 |
. . 3
  

    |
2 | | nncaddccl 4420 |
. . . . . . . 8
  Nn Nn   Nn  |
3 | | tfincl 4493 |
. . . . . . . 8
   Nn Tfin   Nn  |
4 | 2, 3 | syl 15 |
. . . . . . 7
  Nn Nn Tfin 

Nn  |
5 | 4 | 3adant3 975 |
. . . . . 6
  Nn Nn    Tfin 

Nn  |
6 | | tfincl 4493 |
. . . . . . . 8
 Nn Tfin Nn  |
7 | | tfincl 4493 |
. . . . . . . 8
 Nn Tfin Nn  |
8 | | nncaddccl 4420 |
. . . . . . . 8
 Tfin
Nn Tfin
Nn Tfin Tfin 
Nn  |
9 | 6, 7, 8 | syl2an 463 |
. . . . . . 7
  Nn Nn Tfin Tfin 
Nn  |
10 | 9 | 3adant3 975 |
. . . . . 6
  Nn Nn    Tfin Tfin 
Nn  |
11 | 2 | 3adant3 975 |
. . . . . . 7
  Nn Nn      Nn  |
12 | | simp3 957 |
. . . . . . 7
  Nn Nn        |
13 | | tfinpw1 4495 |
. . . . . . 7
   
Nn
   1
Tfin 
   |
14 | 11, 12, 13 | syl2anc 642 |
. . . . . 6
  Nn Nn    1 Tfin
    |
15 | | eladdc 4399 |
. . . . . . . 8
  
          |
16 | | simplll 734 |
. . . . . . . . . . . . 13
    Nn Nn 
 
  
Nn  |
17 | | simplrl 736 |
. . . . . . . . . . . . 13
    Nn Nn 
 
  
  |
18 | | tfinpw1 4495 |
. . . . . . . . . . . . 13
  Nn  1
Tfin   |
19 | 16, 17, 18 | syl2anc 642 |
. . . . . . . . . . . 12
    Nn Nn 
 
  
1 Tfin
  |
20 | | simpllr 735 |
. . . . . . . . . . . . 13
    Nn Nn 
 
  
Nn  |
21 | | simplrr 737 |
. . . . . . . . . . . . 13
    Nn Nn 
 
  
  |
22 | | tfinpw1 4495 |
. . . . . . . . . . . . 13
  Nn  1
Tfin   |
23 | 20, 21, 22 | syl2anc 642 |
. . . . . . . . . . . 12
    Nn Nn 
 
  
1 Tfin
  |
24 | | pw1eq 4144 |
. . . . . . . . . . . . . 14
  
1   1   |
25 | | pw1in 4165 |
. . . . . . . . . . . . . 14
1    1
1   |
26 | | pw10 4162 |
. . . . . . . . . . . . . 14
1  |
27 | 24, 25, 26 | 3eqtr3g 2408 |
. . . . . . . . . . . . 13
  
 1 1    |
28 | 27 | adantl 452 |
. . . . . . . . . . . 12
    Nn Nn 
 
  
 1 1    |
29 | | eladdci 4400 |
. . . . . . . . . . . 12
  1
Tfin 1
Tfin  1 1    1 1  Tfin
Tfin    |
30 | 19, 23, 28, 29 | syl3anc 1182 |
. . . . . . . . . . 11
    Nn Nn 
 
  
 1 1  Tfin Tfin    |
31 | | pw1eq 4144 |
. . . . . . . . . . . . 13
   1 1     |
32 | | pw1un 4164 |
. . . . . . . . . . . . 13
1    1
1   |
33 | 31, 32 | syl6eq 2401 |
. . . . . . . . . . . 12
   1  1 1    |
34 | 33 | eleq1d 2419 |
. . . . . . . . . . 11
    1 Tfin Tfin   1
1  Tfin Tfin     |
35 | 30, 34 | syl5ibrcom 213 |
. . . . . . . . . 10
    Nn Nn 
 
  

  1 Tfin Tfin     |
36 | 35 | expimpd 586 |
. . . . . . . . 9
   Nn Nn           1
Tfin Tfin     |
37 | 36 | rexlimdvva 2746 |
. . . . . . . 8
  Nn Nn  
       1
Tfin Tfin     |
38 | 15, 37 | syl5bi 208 |
. . . . . . 7
  Nn Nn   
1 Tfin Tfin     |
39 | 38 | 3impia 1148 |
. . . . . 6
  Nn Nn    1 Tfin Tfin    |
40 | | nnceleq 4431 |
. . . . . 6
  Tfin   Nn Tfin Tfin 
Nn  1
Tfin   1
Tfin Tfin    Tfin 

Tfin Tfin    |
41 | 5, 10, 14, 39, 40 | syl22anc 1183 |
. . . . 5
  Nn Nn    Tfin 

Tfin Tfin    |
42 | 41 | 3expia 1153 |
. . . 4
  Nn Nn   
Tfin 

Tfin Tfin     |
43 | 42 | exlimdv 1636 |
. . 3
  Nn Nn  
  Tfin
  Tfin
Tfin     |
44 | 1, 43 | syl5bi 208 |
. 2
  Nn Nn   
Tfin 

Tfin Tfin     |
45 | 44 | 3impia 1148 |
1
  Nn Nn  
 Tfin   Tfin
Tfin    |