Step | Hyp | Ref
| Expression |
1 | | nmcex.2 |
. . 3
            
             |
2 | | nmcex.3 |
. . . . . . . . 9
           |
3 | | eleq1 2527 |
. . . . . . . . 9
        
            |
4 | 2, 3 | syl5ibrcom 230 |
. . . . . . . 8
         
   |
5 | 4 | imp 435 |
. . . . . . 7
 
        
  |
6 | 5 | adantrl 727 |
. . . . . 6
      
            |
7 | 6 | rexlimiva 2886 |
. . . . 5
                  |
8 | 7 | abssi 3515 |
. . . 4
      
           |
9 | | ax-hv0cl 26704 |
. . . . . . 7
 |
10 | | norm0 26829 |
. . . . . . . . 9
     |
11 | | 0le1 10164 |
. . . . . . . . 9
 |
12 | 10, 11 | eqbrtri 4435 |
. . . . . . . 8
     |
13 | | nmcex.4 |
. . . . . . . . 9
         |
14 | 13 | eqcomi 2470 |
. . . . . . . 8
         |
15 | 12, 14 | pm3.2i 461 |
. . . . . . 7
    
          |
16 | | fveq2 5887 |
. . . . . . . . . 10
           |
17 | 16 | breq1d 4425 |
. . . . . . . . 9
             |
18 | | fveq2 5887 |
. . . . . . . . . . 11
           |
19 | 18 | fveq2d 5891 |
. . . . . . . . . 10
                   |
20 | 19 | eqeq2d 2471 |
. . . . . . . . 9
         
           |
21 | 17, 20 | anbi12d 722 |
. . . . . . . 8
      
        
    
            |
22 | 21 | rspcev 3161 |
. . . . . . 7
                 
    
           |
23 | 9, 15, 22 | mp2an 683 |
. . . . . 6
     
          |
24 | | c0ex 9662 |
. . . . . . 7
 |
25 | | eqeq1 2465 |
. . . . . . . . 9
         
           |
26 | 25 | anbi2d 715 |
. . . . . . . 8
      
        
    
            |
27 | 26 | rexbidv 2912 |
. . . . . . 7
  
    
        
     
            |
28 | 24, 27 | elab 3196 |
. . . . . 6
       
          
    
           |
29 | 23, 28 | mpbir 214 |
. . . . 5
 
                |
30 | 29 | ne0ii 3749 |
. . . 4
      
           |
31 | | nmcex.1 |
. . . . 5
              
  |
32 | | 2rp 11335 |
. . . . . . . . . 10
 |
33 | | rpdivcl 11353 |
. . . . . . . . . 10
       |
34 | 32, 33 | mpan 681 |
. . . . . . . . 9

    |
35 | 34 | rpred 11369 |
. . . . . . . 8

    |
36 | 35 | adantr 471 |
. . . . . . 7
  
    
              |
37 | | rpre 11336 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
38 | 37 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
           |
39 | 38 | rehalfcld 10887 |
. . . . . . . . . . . . . . . . . . . 20
             |
40 | 39 | recnd 9694 |
. . . . . . . . . . . . . . . . . . 19
             |
41 | | simprl 769 |
. . . . . . . . . . . . . . . . . . 19
        
  |
42 | | hvmulcl 26714 |
. . . . . . . . . . . . . . . . . . 19
   
       |
43 | 40, 41, 42 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
               |
44 | | normcl 26826 |
. . . . . . . . . . . . . . . . . 18
               |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . 17
                   |
46 | | simprr 771 |
. . . . . . . . . . . . . . . . . . 19
               |
47 | | normcl 26826 |
. . . . . . . . . . . . . . . . . . . . 21
       |
48 | 47 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . 20
               |
49 | | 1red 9683 |
. . . . . . . . . . . . . . . . . . . 20
           |
50 | | rphalfcl 11355 |
. . . . . . . . . . . . . . . . . . . . 21

    |
51 | 50 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
             |
52 | 48, 49, 51 | lemul2d 11410 |
. . . . . . . . . . . . . . . . . . 19
             
               |
53 | 46, 52 | mpbid 215 |
. . . . . . . . . . . . . . . . . 18
                       |
54 | | rpcn 11338 |
. . . . . . . . . . . . . . . . . . . . 21
  
    |
55 | | norm-iii 26841 |
. . . . . . . . . . . . . . . . . . . . 21
   
                       |
56 | 54, 55 | sylan 478 |
. . . . . . . . . . . . . . . . . . . 20
                           |
57 | | rpre 11336 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
    |
58 | | rpge0 11342 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
    |
59 | 57, 58 | absidd 13532 |
. . . . . . . . . . . . . . . . . . . . . 22
  
          |
60 | 59 | oveq1d 6329 |
. . . . . . . . . . . . . . . . . . . . 21
  
                      |
61 | 60 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
                           |
62 | 56, 61 | eqtr2d 2496 |
. . . . . . . . . . . . . . . . . . 19
                       |
63 | 51, 41, 62 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
                           |
64 | 40 | mulid1d 9685 |
. . . . . . . . . . . . . . . . . 18
                 |
65 | 53, 63, 64 | 3brtr3d 4445 |
. . . . . . . . . . . . . . . . 17
                     |
66 | | rphalflt 11357 |
. . . . . . . . . . . . . . . . . 18

    |
67 | 66 | adantr 471 |
. . . . . . . . . . . . . . . . 17
          
  |
68 | 45, 39, 38, 65, 67 | lelttrd 9818 |
. . . . . . . . . . . . . . . 16
                   |
69 | | fveq2 5887 |
. . . . . . . . . . . . . . . . . . . 20
                   |
70 | 69 | breq1d 4425 |
. . . . . . . . . . . . . . . . . . 19
                     |
71 | | fveq2 5887 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
72 | 71 | fveq2d 5891 |
. . . . . . . . . . . . . . . . . . . 20
                           |
73 | 72 | breq1d 4425 |
. . . . . . . . . . . . . . . . . . 19
             
               |
74 | 70, 73 | imbi12d 326 |
. . . . . . . . . . . . . . . . . 18
          
        
        
                |
75 | 74 | rspcv 3157 |
. . . . . . . . . . . . . . . . 17
      
    
                                  |
76 | 43, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
                       
                          |
77 | 68, 76 | mpid 42 |
. . . . . . . . . . . . . . 15
                       
                |
78 | 2 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . 18
                   |
79 | 78, 49, 51 | ltmuldiv2d 11414 |
. . . . . . . . . . . . . . . . 17
                                     |
80 | 51 | rprecred 11380 |
. . . . . . . . . . . . . . . . . 18
               |
81 | | ltle 9747 |
. . . . . . . . . . . . . . . . . 18
                           
               |
82 | 78, 80, 81 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
                             
       |
83 | 79, 82 | sylbid 223 |
. . . . . . . . . . . . . . . 16
                             
       |
84 | | nmcex.5 |
. . . . . . . . . . . . . . . . . 18
                               |
85 | 51, 41, 84 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
                                   |
86 | 85 | breq1d 4425 |
. . . . . . . . . . . . . . . 16
                                     |
87 | | rpcn 11338 |
. . . . . . . . . . . . . . . . . . 19

  |
88 | | rpne0 11345 |
. . . . . . . . . . . . . . . . . . 19

  |
89 | | 2cn 10707 |
. . . . . . . . . . . . . . . . . . . 20
 |
90 | | 2ne0 10729 |
. . . . . . . . . . . . . . . . . . . 20
 |
91 | | recdiv 10340 |
. . . . . . . . . . . . . . . . . . . 20
               |
92 | 89, 90, 91 | mpanr12 696 |
. . . . . . . . . . . . . . . . . . 19
           |
93 | 87, 88, 92 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18

        |
94 | 93 | adantr 471 |
. . . . . . . . . . . . . . . . 17
                 |
95 | 94 | breq2d 4427 |
. . . . . . . . . . . . . . . 16
                 
   
             |
96 | 83, 86, 95 | 3imtr3d 275 |
. . . . . . . . . . . . . . 15
                             
     |
97 | 77, 96 | syld 45 |
. . . . . . . . . . . . . 14
                       
        
     |
98 | 97 | imp 435 |
. . . . . . . . . . . . 13
               
                      |
99 | 98 | an32s 818 |
. . . . . . . . . . . 12
        
          
                  |
100 | 99 | anassrs 658 |
. . . . . . . . . . 11
                 
                    |
101 | | breq1 4418 |
. . . . . . . . . . 11
        
          
     |
102 | 100, 101 | syl5ibrcom 230 |
. . . . . . . . . 10
                 
                      |
103 | 102 | expimpd 612 |
. . . . . . . . 9
        
                
        
     |
104 | 103 | rexlimdva 2890 |
. . . . . . . 8
  
    
           
    
              |
105 | 104 | alrimiv 1783 |
. . . . . . 7
  
    
                  
              |
106 | | eqeq1 2465 |
. . . . . . . . . . . 12
         
           |
107 | 106 | anbi2d 715 |
. . . . . . . . . . 11
      
        
    
            |
108 | 107 | rexbidv 2912 |
. . . . . . . . . 10
  
    
        
     
            |
109 | 108 | ralab 3210 |
. . . . . . . . 9
 
      
          
        
            |
110 | | breq2 4419 |
. . . . . . . . . . 11
   
     |
111 | 110 | imbi2d 322 |
. . . . . . . . . 10
          
                
               |
112 | 111 | albidv 1777 |
. . . . . . . . 9
            
                                  |
113 | 109, 112 | syl5bb 265 |
. . . . . . . 8
    
      
          
        
               |
114 | 113 | rspcev 3161 |
. . . . . . 7
            
                
                  |
115 | 36, 105, 114 | syl2anc 671 |
. . . . . 6
  
    
             
                  |
116 | 115 | rexlimiva 2886 |
. . . . 5
               
         
          
  |
117 | 31, 116 | ax-mp 5 |
. . . 4
   
                 |
118 | | supxrre 11641 |
. . . 4
   
                     
             
                    
                         
              |
119 | 8, 30, 117, 118 | mp3an 1373 |
. . 3
  

                         
             |
120 | 1, 119 | eqtri 2483 |
. 2
            
             |
121 | | suprcl 10596 |
. . 3
   
                     
             
                    
                
  |
122 | 8, 30, 117, 121 | mp3an 1373 |
. 2
  

                
 |
123 | 120, 122 | eqeltri 2535 |
1
     |