Step | Hyp | Ref
| Expression |
1 | | climc 14506 |
. 2
lim |
2 | | vf |
. . 3
 |
3 | | vx |
. . 3
 |
4 | | cc 7826 |
. . . 4
 |
5 | | cpm 6666 |
. . . 4
 |
6 | 4, 4, 5 | co 5890 |
. . 3
   |
7 | 2 | cv 1362 |
. . . . . . . 8
 |
8 | 7 | cdm 4640 |
. . . . . . 7
 |
9 | 8, 4, 7 | wf 5226 |
. . . . . 6
     |
10 | 8, 4 | wss 3143 |
. . . . . 6
 |
11 | 9, 10 | wa 104 |
. . . . 5
    
  |
12 | 3 | cv 1362 |
. . . . . . 7
 |
13 | 12, 4 | wcel 2159 |
. . . . . 6
 |
14 | | vz |
. . . . . . . . . . . . 13
 |
15 | 14 | cv 1362 |
. . . . . . . . . . . 12
 |
16 | | cap 8555 |
. . . . . . . . . . . 12
# |
17 | 15, 12, 16 | wbr 4017 |
. . . . . . . . . . 11
#  |
18 | | cmin 8145 |
. . . . . . . . . . . . . 14
 |
19 | 15, 12, 18 | co 5890 |
. . . . . . . . . . . . 13
   |
20 | | cabs 11023 |
. . . . . . . . . . . . 13
 |
21 | 19, 20 | cfv 5230 |
. . . . . . . . . . . 12
       |
22 | | vd |
. . . . . . . . . . . . 13
 |
23 | 22 | cv 1362 |
. . . . . . . . . . . 12
 |
24 | | clt 8009 |
. . . . . . . . . . . 12
 |
25 | 21, 23, 24 | wbr 4017 |
. . . . . . . . . . 11
       |
26 | 17, 25 | wa 104 |
. . . . . . . . . 10
 #         |
27 | 15, 7 | cfv 5230 |
. . . . . . . . . . . . 13
     |
28 | | vy |
. . . . . . . . . . . . . 14
 |
29 | 28 | cv 1362 |
. . . . . . . . . . . . 13
 |
30 | 27, 29, 18 | co 5890 |
. . . . . . . . . . . 12
       |
31 | 30, 20 | cfv 5230 |
. . . . . . . . . . 11
           |
32 | | ve |
. . . . . . . . . . . 12
 |
33 | 32 | cv 1362 |
. . . . . . . . . . 11
 |
34 | 31, 33, 24 | wbr 4017 |
. . . . . . . . . 10
           |
35 | 26, 34 | wi 4 |
. . . . . . . . 9
  #                    |
36 | 35, 14, 8 | wral 2467 |
. . . . . . . 8
    #                    |
37 | | crp 9670 |
. . . . . . . 8
 |
38 | 36, 22, 37 | wrex 2468 |
. . . . . . 7
     #                    |
39 | 38, 32, 37 | wral 2467 |
. . . . . 6
      #       
            |
40 | 13, 39 | wa 104 |
. . . . 5
 
     #                     |
41 | 11, 40 | wa 104 |
. . . 4
      
       #                      |
42 | 41, 28, 4 | crab 2471 |
. . 3
               #                       |
43 | 2, 3, 6, 4, 42 | cmpo 5892 |
. 2
           
       #                        |
44 | 1, 43 | wceq 1363 |
1
lim  
 
      

       #                        |