Proof of Theorem metnrmlem3OLD
Step | Hyp | Ref
| Expression |
1 | | metnrmlemOLD.g |
. . . 4
             |
2 | | metdscnOLD.j |
. . . 4
     |
3 | | metnrmlemOLD.1 |
. . . 4
        |
4 | | metnrmlemOLD.3 |
. . . 4
       |
5 | | metnrmlemOLD.2 |
. . . 4
       |
6 | | incom 3616 |
. . . . 5
     |
7 | | metnrmlemOLD.4 |
. . . . 5
     |
8 | 6, 7 | syl5eq 2517 |
. . . 4
     |
9 | | metnrmlemOLD.v |
. . . 4
                         |
10 | 1, 2, 3, 4, 5, 8, 9 | metnrmlem2OLD 21970 |
. . 3
 
   |
11 | 10 | simpld 466 |
. 2
   |
12 | | metdscnOLD.f |
. . . 4
             |
13 | | metnrmlemOLD.u |
. . . 4
                         |
14 | 12, 2, 3, 5, 4, 7, 13 | metnrmlem2OLD 21970 |
. . 3
 
   |
15 | 14 | simpld 466 |
. 2
   |
16 | 10 | simprd 470 |
. 2

  |
17 | 14 | simprd 470 |
. 2

  |
18 | 9 | ineq1i 3621 |
. . . 4
                             |
19 | | iunin1 4334 |
. . . 4

          
                                         |
20 | 18, 19 | eqtr4i 2496 |
. . 3
                             |
21 | 13 | ineq2i 3622 |
. . . . . . . 8
          
                                      
                         |
22 | | iunin2 4333 |
. . . . . . . 8

          
                                                             
                         |
23 | 21, 22 | eqtr4i 2496 |
. . . . . . 7
          
              
                                 
               |
24 | 3 | adantr 472 |
. . . . . . . . . . . 12
 

 
       |
25 | | eqid 2471 |
. . . . . . . . . . . . . . . . 17
   |
26 | 25 | cldss 20121 |
. . . . . . . . . . . . . . . 16
    
   |
27 | 5, 26 | syl 17 |
. . . . . . . . . . . . . . 15

   |
28 | 2 | mopnuni 21534 |
. . . . . . . . . . . . . . . 16
         |
29 | 3, 28 | syl 17 |
. . . . . . . . . . . . . . 15
    |
30 | 27, 29 | sseqtr4d 3455 |
. . . . . . . . . . . . . 14

  |
31 | 30 | sselda 3418 |
. . . . . . . . . . . . 13
 
   |
32 | 31 | adantrr 731 |
. . . . . . . . . . . 12
 

    |
33 | 25 | cldss 20121 |
. . . . . . . . . . . . . . . 16
    
   |
34 | 4, 33 | syl 17 |
. . . . . . . . . . . . . . 15

   |
35 | 34, 29 | sseqtr4d 3455 |
. . . . . . . . . . . . . 14

  |
36 | 35 | sselda 3418 |
. . . . . . . . . . . . 13
 
   |
37 | 36 | adantrl 730 |
. . . . . . . . . . . 12
 

    |
38 | 1, 2, 3, 4, 5, 8 | metnrmlem1aOLD 21968 |
. . . . . . . . . . . . . . . 16
 
 
                    |
39 | 38 | simprd 470 |
. . . . . . . . . . . . . . 15
 
                |
40 | 39 | adantrr 731 |
. . . . . . . . . . . . . 14
 

                 |
41 | 40 | rphalfcld 11376 |
. . . . . . . . . . . . 13
 

                   |
42 | 41 | rpxrd 11365 |
. . . . . . . . . . . 12
 

                   |
43 | 12, 2, 3, 5, 4, 7 | metnrmlem1aOLD 21968 |
. . . . . . . . . . . . . . . 16
 
 
                    |
44 | 43 | adantrl 730 |
. . . . . . . . . . . . . . 15
 

                       |
45 | 44 | simprd 470 |
. . . . . . . . . . . . . 14
 

                 |
46 | 45 | rphalfcld 11376 |
. . . . . . . . . . . . 13
 

                   |
47 | 46 | rpxrd 11365 |
. . . . . . . . . . . 12
 

                   |
48 | 40 | rpred 11364 |
. . . . . . . . . . . . . . . 16
 

                 |
49 | 48 | rehalfcld 10882 |
. . . . . . . . . . . . . . 15
 

                   |
50 | 45 | rpred 11364 |
. . . . . . . . . . . . . . . 16
 

                 |
51 | 50 | rehalfcld 10882 |
. . . . . . . . . . . . . . 15
 

                   |
52 | | rexadd 11548 |
. . . . . . . . . . . . . . 15
                                                                                                      |
53 | 49, 51, 52 | syl2anc 673 |
. . . . . . . . . . . . . 14
 

     
                                  
                              |
54 | 48 | recnd 9687 |
. . . . . . . . . . . . . . 15
 

                 |
55 | 50 | recnd 9687 |
. . . . . . . . . . . . . . 15
 

                 |
56 | | 2cnd 10704 |
. . . . . . . . . . . . . . 15
 

    |
57 | | 2ne0 10724 |
. . . . . . . . . . . . . . . 16
 |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . 15
 

    |
59 | 54, 55, 56, 58 | divdird 10443 |
. . . . . . . . . . . . . 14
 

     
                                                            |
60 | 53, 59 | eqtr4d 2508 |
. . . . . . . . . . . . 13
 

     
                                  
                            |
61 | 1, 2, 3, 4, 5, 8 | metnrmlem1OLD 21969 |
. . . . . . . . . . . . . . . . . 18
 

              
      |
62 | 61 | ancom2s 819 |
. . . . . . . . . . . . . . . . 17
 

              
      |
63 | | xmetsym 21440 |
. . . . . . . . . . . . . . . . . 18
      

          |
64 | 24, 37, 32, 63 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
 

            |
65 | 62, 64 | breqtrd 4420 |
. . . . . . . . . . . . . . . 16
 

              
      |
66 | 12, 2, 3, 5, 4, 7 | metnrmlem1OLD 21969 |
. . . . . . . . . . . . . . . 16
 

              
      |
67 | 40 | rpxrd 11365 |
. . . . . . . . . . . . . . . . 17
 

                 |
68 | 45 | rpxrd 11365 |
. . . . . . . . . . . . . . . . 17
 

                 |
69 | | xmetcl 21424 |
. . . . . . . . . . . . . . . . . 18
      

      |
70 | 24, 32, 37, 69 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
 

        |
71 | | xle2add 11570 |
. . . . . . . . . . . . . . . . 17
               
 
                          
                
                                                               |
72 | 67, 68, 70, 70, 71 | syl22anc 1293 |
. . . . . . . . . . . . . . . 16
 

     
                
                                                               |
73 | 65, 66, 72 | mp2and 693 |
. . . . . . . . . . . . . . 15
 

                                                |
74 | 48, 50 | readdcld 9688 |
. . . . . . . . . . . . . . . . . 18
 

                                |
75 | 74 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
 

                                |
76 | 75, 56, 58 | divcan2d 10407 |
. . . . . . . . . . . . . . . 16
 

                                                                |
77 | | 2re 10701 |
. . . . . . . . . . . . . . . . 17
 |
78 | 74 | rehalfcld 10882 |
. . . . . . . . . . . . . . . . 17
 

     
                            |
79 | | rexmul 11582 |
. . . . . . . . . . . . . . . . 17
     
                                               
                  
                             |
80 | 77, 78, 79 | sylancr 676 |
. . . . . . . . . . . . . . . 16
 

         
                                                             |
81 | | rexadd 11548 |
. . . . . . . . . . . . . . . . 17
                               
                              
                           |
82 | 48, 50, 81 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
 

                                   
                           |
83 | 76, 80, 82 | 3eqtr4d 2515 |
. . . . . . . . . . . . . . 15
 

         
                                                            |
84 | | x2times 11610 |
. . . . . . . . . . . . . . . 16
    
                        |
85 | 70, 84 | syl 17 |
. . . . . . . . . . . . . . 15
 

                          |
86 | 73, 83, 85 | 3brtr4d 4426 |
. . . . . . . . . . . . . 14
 

         
                                      |
87 | 78 | rexrd 9708 |
. . . . . . . . . . . . . . 15
 

     
                            |
88 | | 2rp 11330 |
. . . . . . . . . . . . . . . 16
 |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . 15
 

    |
90 | | xlemul2 11602 |
. . . . . . . . . . . . . . 15
     
                                   
                                     
                                       |
91 | 87, 70, 89, 90 | syl3anc 1292 |
. . . . . . . . . . . . . 14
 

                   
                                     
                          |
92 | 86, 91 | mpbird 240 |
. . . . . . . . . . . . 13
 

     
                                |
93 | 60, 92 | eqbrtrd 4416 |
. . . . . . . . . . . 12
 

     
                                     |
94 | | bldisj 21491 |
. . . . . . . . . . . 12
       

               
              
                                                                                           |
95 | 24, 32, 37, 42, 47, 93, 94 | syl33anc 1307 |
. . . . . . . . . . 11
 

                                                    |
96 | | eqimss 3470 |
. . . . . . . . . . 11
                                  
             
          
                                       |
97 | 95, 96 | syl 17 |
. . . . . . . . . 10
 

                                                    |
98 | 97 | anassrs 660 |
. . . . . . . . 9
                                      
                |
99 | 98 | ralrimiva 2809 |
. . . . . . . 8
 
 
          
                                       |
100 | | iunss 4310 |
. . . . . . . 8
 
                                 
                                                                 |
101 | 99, 100 | sylibr 217 |
. . . . . . 7
 
 
          
                                       |
102 | 23, 101 | syl5eqss 3462 |
. . . . . 6
 
                            |
103 | 102 | ralrimiva 2809 |
. . . . 5
                             |
104 | | iunss 4310 |
. . . . 5
 
                                                     |
105 | 103, 104 | sylibr 217 |
. . . 4
                             |
106 | | ss0 3768 |
. . . 4
 
                        
           
                |
107 | 105, 106 | syl 17 |
. . 3
                             |
108 | 20, 107 | syl5eq 2517 |
. 2
     |
109 | | sseq2 3440 |
. . . 4
 
   |
110 | | ineq1 3618 |
. . . . 5
 
     |
111 | 110 | eqeq1d 2473 |
. . . 4
   
     |
112 | 109, 111 | 3anbi13d 1367 |
. . 3
  
  
       |
113 | | sseq2 3440 |
. . . 4
 
   |
114 | | ineq2 3619 |
. . . . 5
       |
115 | 114 | eqeq1d 2473 |
. . . 4
   
     |
116 | 113, 115 | 3anbi23d 1368 |
. . 3
  

 
       |
117 | 112, 116 | rspc2ev 3149 |
. 2
 

    

      |
118 | 11, 15, 16, 17, 108, 117 | syl113anc 1304 |
1
  


    |