Step | Hyp | Ref
| Expression |
1 | | breq1 4006 |
. . . . 5
  #
#    |
2 | 1 | elrab 2893 |
. . . 4
  #   #    |
3 | | divrecap 8644 |
. . . . 5
 
#          |
4 | 3 | 3expb 1204 |
. . . 4
   #           |
5 | 2, 4 | sylan2b 287 |
. . 3
 
 #           |
6 | 5 | mpoeq3ia 5939 |
. 2
   #      
 #        |
7 | | addcncntop.j |
. . . . . 6
      |
8 | 7 | cntoptopon 14002 |
. . . . 5
TopOn   |
9 | 8 | a1i 9 |
. . . 4
TopOn    |
10 | | divcnap.k |
. . . . 5

↾t  #
   |
11 | | ssrab2 3240 |
. . . . . 6
 # 
 |
12 | | resttopon 13641 |
. . . . . 6
  TopOn 
 # 
 
↾t  #
  TopOn 
#
    |
13 | 9, 11, 12 | sylancl 413 |
. . . . 5

↾t  #
  TopOn 
#
    |
14 | 10, 13 | eqeltrid 2264 |
. . . 4
TopOn  #
    |
15 | 9, 14 | cnmpt1st 13758 |
. . . 4
 
 #         |
16 | 9, 14 | cnmpt2nd 13759 |
. . . . 5
 
 #         |
17 | | eqid 2177 |
. . . . . . . 8
  #       #      |
18 | | breq1 4006 |
. . . . . . . . . 10
  #
#    |
19 | 18 | elrab 2893 |
. . . . . . . . 9
  #   #    |
20 | | recclap 8635 |
. . . . . . . . 9
  #      |
21 | 19, 20 | sylbi 121 |
. . . . . . . 8
  # 
    |
22 | 17, 21 | fmpti 5668 |
. . . . . . 7
  #        #
    |
23 | | breq1 4006 |
. . . . . . . . . . 11
  #
#    |
24 | 23 | elrab 2893 |
. . . . . . . . . 10
  #   #    |
25 | | eqid 2177 |
. . . . . . . . . . . 12
inf                   inf                    |
26 | 25 | reccn2ap 11320 |
. . . . . . . . . . 11
  #
    #
                     |
27 | 26 | 3expa 1203 |
. . . . . . . . . 10
   # 
 
  #
                     |
28 | 24, 27 | sylanb 284 |
. . . . . . . . 9
   #  
   #
                     |
29 | | ovres 6013 |
. . . . . . . . . . . . . . 15
   #   #
 
   
  #   #             |
30 | | elrabi 2890 |
. . . . . . . . . . . . . . . 16
  # 
  |
31 | | elrabi 2890 |
. . . . . . . . . . . . . . . 16
  # 
  |
32 | | eqid 2177 |
. . . . . . . . . . . . . . . . . 18

  |
33 | 32 | cnmetdval 13999 |
. . . . . . . . . . . . . . . . 17
 
   
          |
34 | | abssub 11109 |
. . . . . . . . . . . . . . . . 17
 
               |
35 | 33, 34 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
 
   
          |
36 | 30, 31, 35 | syl2an 289 |
. . . . . . . . . . . . . . 15
   #   #
 
  
          |
37 | 29, 36 | eqtrd 2210 |
. . . . . . . . . . . . . 14
   #   #
 
   
  #   #              |
38 | 37 | breq1d 4013 |
. . . . . . . . . . . . 13
   #   #
 
    
 
#
  #
    
         |
39 | 24 | simprbi 275 |
. . . . . . . . . . . . . . . . . 18
  # 
#   |
40 | 30, 39 | recclapd 8737 |
. . . . . . . . . . . . . . . . 17
  # 
    |
41 | | oveq2 5882 |
. . . . . . . . . . . . . . . . . 18
       |
42 | 41, 17 | fvmptg 5592 |
. . . . . . . . . . . . . . . . 17
   #        #            |
43 | 40, 42 | mpdan 421 |
. . . . . . . . . . . . . . . 16
  # 
   #            |
44 | | breq1 4006 |
. . . . . . . . . . . . . . . . . . . 20
  #
#    |
45 | 44 | elrab 2893 |
. . . . . . . . . . . . . . . . . . 19
  #   #    |
46 | 45 | simprbi 275 |
. . . . . . . . . . . . . . . . . 18
  # 
#   |
47 | 31, 46 | recclapd 8737 |
. . . . . . . . . . . . . . . . 17
  # 
    |
48 | | oveq2 5882 |
. . . . . . . . . . . . . . . . . 18
       |
49 | 48, 17 | fvmptg 5592 |
. . . . . . . . . . . . . . . . 17
   #        #            |
50 | 47, 49 | mpdan 421 |
. . . . . . . . . . . . . . . 16
  # 
   #            |
51 | 43, 50 | oveqan12d 5893 |
. . . . . . . . . . . . . . 15
   #   #
 
    #              #
                   |
52 | 32 | cnmetdval 13999 |
. . . . . . . . . . . . . . . . 17
                            |
53 | | abssub 11109 |
. . . . . . . . . . . . . . . . 17
                             |
54 | 52, 53 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
                            |
55 | 40, 47, 54 | syl2an 289 |
. . . . . . . . . . . . . . 15
   #   #
 
                     |
56 | 51, 55 | eqtrd 2210 |
. . . . . . . . . . . . . 14
   #   #
 
    #              #
                    |
57 | 56 | breq1d 4013 |
. . . . . . . . . . . . 13
   #   #
 
     #
             #                      |
58 | 38, 57 | imbi12d 234 |
. . . . . . . . . . . 12
   #   #
 
        #   #          #         
    #         
      
              |
59 | 58 | ralbidva 2473 |
. . . . . . . . . . 11
  # 
 
 #      
  #   #          #         
    #         
  #
                      |
60 | 59 | rexbidv 2478 |
. . . . . . . . . 10
  # 
 
  #
        #   #          #         
    #         
   #
                      |
61 | 60 | adantr 276 |
. . . . . . . . 9
   #  
    #
        #   #          #         
    #         
   #
                      |
62 | 28, 61 | mpbird 167 |
. . . . . . . 8
   #  
   #
        #   #          #         
    #            |
63 | 62 | rgen2 2563 |
. . . . . . 7
  #
  
   #
        #   #          #         
    #           |
64 | | cnxmet 14001 |
. . . . . . . . 9

      |
65 | | xmetres2 13849 |
. . . . . . . . 9
  
      #    
 
#
  #
        #     |
66 | 64, 11, 65 | mp2an 426 |
. . . . . . . 8
    #   #        
#
   |
67 | | eqid 2177 |
. . . . . . . . . . . 12
    #   #     
  #   #     |
68 | | eqid 2177 |
. . . . . . . . . . . 12
    
  #   #         
  #   #      |
69 | 67, 7, 68 | metrest 13976 |
. . . . . . . . . . 11
  
      #    ↾t  #       
 
#
  #
      |
70 | 64, 11, 69 | mp2an 426 |
. . . . . . . . . 10
 ↾t  #          #
  #
     |
71 | 10, 70 | eqtri 2198 |
. . . . . . . . 9
       #
  #
     |
72 | 71, 7 | metcn 13984 |
. . . . . . . 8
   
  #   #         #
 
          #      
   #        #
     #
  
   #
        #   #          #         
    #              |
73 | 66, 64, 72 | mp2an 426 |
. . . . . . 7
   #          #        #
     #
  
   #
        #   #          #         
    #             |
74 | 22, 63, 73 | mpbir2an 942 |
. . . . . 6
  #        |
75 | 74 | a1i 9 |
. . . . 5
  #         |
76 | | oveq2 5882 |
. . . . 5
       |
77 | 9, 14, 16, 14, 75, 76 | cnmpt21 13761 |
. . . 4
 
 #           |
78 | 7 | mulcncntop 14024 |
. . . . 5
     |
79 | 78 | a1i 9 |
. . . 4
      |
80 | 9, 14, 15, 77, 79 | cnmpt22f 13765 |
. . 3
 
 #             |
81 | 80 | mptru 1362 |
. 2
   #            |
82 | 6, 81 | eqeltri 2250 |
1
   #          |