Step | Hyp | Ref
| Expression |
1 | | lncon.1 |
. . 3
   |
2 | | lncon.2 |
. . . 4
 
        
        |
3 | 2 | ralrimiva 2813 |
. . 3
         
        |
4 | | oveq1 6321 |
. . . . . 6
               |
5 | 4 | breq2d 4427 |
. . . . 5
         
             
         |
6 | 5 | ralbidv 2838 |
. . . 4
  
                                |
7 | 6 | rspcev 3161 |
. . 3
                 
         
        |
8 | 1, 3, 7 | syl2anc 671 |
. 2
          
        |
9 | | arch 10894 |
. . . . . 6
    |
10 | 9 | adantr 471 |
. . . . 5
                 
   |
11 | | nnre 10643 |
. . . . . . 7
   |
12 | | simplll 773 |
. . . . . . . . . . . 12
         |
13 | | simpllr 774 |
. . . . . . . . . . . 12
         |
14 | | normcl 26826 |
. . . . . . . . . . . . 13
       |
15 | 14 | adantl 472 |
. . . . . . . . . . . 12
             |
16 | | normge0 26827 |
. . . . . . . . . . . . 13
       |
17 | 16 | adantl 472 |
. . . . . . . . . . . 12
             |
18 | | ltle 9747 |
. . . . . . . . . . . . . 14
 
 
   |
19 | 18 | imp 435 |
. . . . . . . . . . . . 13
    
  |
20 | 19 | adantr 471 |
. . . . . . . . . . . 12
         |
21 | 12, 13, 15, 17, 20 | lemul1ad 10573 |
. . . . . . . . . . 11
                     |
22 | | lncon.4 |
. . . . . . . . . . . . 13
           |
23 | 22 | adantl 472 |
. . . . . . . . . . . 12
                 |
24 | | simpll 765 |
. . . . . . . . . . . . 13
    
  |
25 | | remulcl 9649 |
. . . . . . . . . . . . 13
               |
26 | 24, 14, 25 | syl2an 484 |
. . . . . . . . . . . 12
               |
27 | | simplr 767 |
. . . . . . . . . . . . 13
    
  |
28 | | remulcl 9649 |
. . . . . . . . . . . . 13
               |
29 | 27, 14, 28 | syl2an 484 |
. . . . . . . . . . . 12
               |
30 | | letr 9752 |
. . . . . . . . . . . 12
          
                     
     
     
                        |
31 | 23, 26, 29, 30 | syl3anc 1276 |
. . . . . . . . . . 11
                
     
     
                        |
32 | 21, 31 | mpan2d 685 |
. . . . . . . . . 10
               
     
                 |
33 | 32 | ralimdva 2807 |
. . . . . . . . 9
    
 
                                |
34 | 33 | impancom 446 |
. . . . . . . 8
            
       
                  |
35 | 34 | an32s 818 |
. . . . . . 7
                    
                  |
36 | 11, 35 | sylan2 481 |
. . . . . 6
                    
                  |
37 | 36 | reximdva 2873 |
. . . . 5
                 
 
         
         |
38 | 10, 37 | mpd 15 |
. . . 4
                 
         
        |
39 | 38 | rexlimiva 2886 |
. . 3
  
                                |
40 | | simprr 771 |
. . . . . . . 8
                   
    |
41 | | simpll 765 |
. . . . . . . . 9
                   
    |
42 | 41 | nnrpd 11367 |
. . . . . . . 8
                   
    |
43 | 40, 42 | rpdivcld 11386 |
. . . . . . 7
                   
      |
44 | | simprr 771 |
. . . . . . . . . . . . . 14
   
  
  |
45 | | simprll 777 |
. . . . . . . . . . . . . 14
   
  
  |
46 | | hvsubcl 26718 |
. . . . . . . . . . . . . 14
 
     |
47 | 44, 45, 46 | syl2anc 671 |
. . . . . . . . . . . . 13
   
       |
48 | | fveq2 5887 |
. . . . . . . . . . . . . . . 16
          
    |
49 | 48 | fveq2d 5891 |
. . . . . . . . . . . . . . 15
                       |
50 | | fveq2 5887 |
. . . . . . . . . . . . . . . 16
               |
51 | 50 | oveq2d 6330 |
. . . . . . . . . . . . . . 15
                   |
52 | 49, 51 | breq12d 4428 |
. . . . . . . . . . . . . 14
           
               
           |
53 | 52 | rspcva 3159 |
. . . . . . . . . . . . 13
                   
                    |
54 | 47, 53 | sylan 478 |
. . . . . . . . . . . 12
    
                  
                    |
55 | 54 | an32s 818 |
. . . . . . . . . . 11
                     
                      |
56 | 49 | eleq1d 2523 |
. . . . . . . . . . . . . . 15
           
             |
57 | 56, 22 | vtoclga 3124 |
. . . . . . . . . . . . . 14
               |
58 | 47, 57 | syl 17 |
. . . . . . . . . . . . 13
   
               |
59 | 11 | adantr 471 |
. . . . . . . . . . . . . 14
   
  
  |
60 | | normcl 26826 |
. . . . . . . . . . . . . . 15
           |
61 | 47, 60 | syl 17 |
. . . . . . . . . . . . . 14
   
           |
62 | | remulcl 9649 |
. . . . . . . . . . . . . 14
                   |
63 | 59, 61, 62 | syl2anc 671 |
. . . . . . . . . . . . 13
   
             |
64 | | simprlr 778 |
. . . . . . . . . . . . . 14
   
     |
65 | 64 | rpred 11369 |
. . . . . . . . . . . . 13
   
     |
66 | | lelttr 9749 |
. . . . . . . . . . . . 13
                                
                              |
67 | 58, 63, 65, 66 | syl3anc 1276 |
. . . . . . . . . . . 12
   
           
                                 |
68 | 67 | adantlr 726 |
. . . . . . . . . . 11
                     
             
                              |
69 | 55, 68 | mpand 686 |
. . . . . . . . . 10
                     
                        |
70 | | nnrp 11339 |
. . . . . . . . . . . . . 14
   |
71 | 70 | rpregt0d 11375 |
. . . . . . . . . . . . 13
     |
72 | 71 | adantr 471 |
. . . . . . . . . . . 12
   
       |
73 | | ltmuldiv2 10506 |
. . . . . . . . . . . 12
                   
           |
74 | 61, 65, 72, 73 | syl3anc 1276 |
. . . . . . . . . . 11
   
           
           |
75 | 74 | adantlr 726 |
. . . . . . . . . 10
                     
          
           |
76 | | lncon.5 |
. . . . . . . . . . . . . 14
 
                     |
77 | 44, 45, 76 | syl2anc 671 |
. . . . . . . . . . . . 13
   
                       |
78 | 77 | adantlr 726 |
. . . . . . . . . . . 12
                     
                      |
79 | 78 | fveq2d 5891 |
. . . . . . . . . . 11
                     
                              |
80 | 79 | breq1d 4425 |
. . . . . . . . . 10
                     
            
                   |
81 | 69, 75, 80 | 3imtr3d 275 |
. . . . . . . . 9
                     
          
                   |
82 | 81 | anassrs 658 |
. . . . . . . 8
            
       
                               |
83 | 82 | ralrimiva 2813 |
. . . . . . 7
                   
                               |
84 | | breq2 4419 |
. . . . . . . . . 10
                     |
85 | 84 | imbi1d 323 |
. . . . . . . . 9
                                                         |
86 | 85 | ralbidv 2838 |
. . . . . . . 8
    
                        
                             |
87 | 86 | rspcev 3161 |
. . . . . . 7
    
        
                                              |
88 | 43, 83, 87 | syl2anc 671 |
. . . . . 6
                   
          
                   |
89 | 88 | ralrimivva 2820 |
. . . . 5
                 
          
                   |
90 | 89 | rexlimiva 2886 |
. . . 4
  
                                            |
91 | | lncon.3 |
. . . 4

          
                   |
92 | 90, 91 | sylibr 217 |
. . 3
  
                |
93 | 39, 92 | syl 17 |
. 2
  
                |
94 | 8, 93 | impbii 192 |
1

         
        |