Step | Hyp | Ref
| Expression |
1 | | nmlno0lem.u |
. . . . . . . . . . . . . . 15
 |
2 | | nmlno0lem.1 |
. . . . . . . . . . . . . . . 16
     |
3 | | nmlno0lem.k |
. . . . . . . . . . . . . . . 16
 CV   |
4 | 2, 3 | nvcl 26288 |
. . . . . . . . . . . . . . 15
         |
5 | 1, 4 | mpan 676 |
. . . . . . . . . . . . . 14
       |
6 | 5 | recnd 9669 |
. . . . . . . . . . . . 13
       |
7 | 6 | adantr 467 |
. . . . . . . . . . . 12
             |
8 | | nmlno0lem.p |
. . . . . . . . . . . . . . . . 17
     |
9 | 2, 8, 3 | nvz 26298 |
. . . . . . . . . . . . . . . 16
           |
10 | 1, 9 | mpan 676 |
. . . . . . . . . . . . . . 15
         |
11 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
           |
12 | | nmlno0lem.w |
. . . . . . . . . . . . . . . . 17
 |
13 | | nmlno0lem.l |
. . . . . . . . . . . . . . . . 17
 |
14 | | nmlno0lem.2 |
. . . . . . . . . . . . . . . . . 18
     |
15 | | nmlno0lem.q |
. . . . . . . . . . . . . . . . . 18
     |
16 | | nmlno0.7 |
. . . . . . . . . . . . . . . . . 18
   |
17 | 2, 14, 8, 15, 16 | lno0 26397 |
. . . . . . . . . . . . . . . . 17
 
       |
18 | 1, 12, 13, 17 | mp3an 1364 |
. . . . . . . . . . . . . . . 16
     |
19 | 11, 18 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
       |
20 | 10, 19 | syl6bi 232 |
. . . . . . . . . . . . . 14
             |
21 | 20 | necon3d 2645 |
. . . . . . . . . . . . 13
             |
22 | 21 | imp 431 |
. . . . . . . . . . . 12
             |
23 | 7, 22 | recne0d 10377 |
. . . . . . . . . . 11
               |
24 | | simpr 463 |
. . . . . . . . . . 11
             |
25 | 7, 22 | reccld 10376 |
. . . . . . . . . . . . . 14
               |
26 | 2, 14, 16 | lnof 26396 |
. . . . . . . . . . . . . . . . 17
 
       |
27 | 1, 12, 13, 26 | mp3an 1364 |
. . . . . . . . . . . . . . . 16
     |
28 | 27 | ffvelrni 6021 |
. . . . . . . . . . . . . . 15
       |
29 | 28 | adantr 467 |
. . . . . . . . . . . . . 14
             |
30 | | nmlno0lem.s |
. . . . . . . . . . . . . . . 16
      |
31 | 14, 30, 15 | nvmul0or 26273 |
. . . . . . . . . . . . . . 15
                           
               |
32 | 12, 31 | mp3an1 1351 |
. . . . . . . . . . . . . 14
                                           |
33 | 25, 29, 32 | syl2anc 667 |
. . . . . . . . . . . . 13
                                     |
34 | 33 | necon3abid 2660 |
. . . . . . . . . . . 12
                                     |
35 | | neanior 2716 |
. . . . . . . . . . . 12
                           |
36 | 34, 35 | syl6bbr 267 |
. . . . . . . . . . 11
                                     |
37 | 23, 24, 36 | mpbir2and 933 |
. . . . . . . . . 10
                       |
38 | 14, 30 | nvscl 26247 |
. . . . . . . . . . . . 13
                             |
39 | 12, 38 | mp3an1 1351 |
. . . . . . . . . . . 12
                             |
40 | 25, 29, 39 | syl2anc 667 |
. . . . . . . . . . 11
                       |
41 | | nmlno0lem.m |
. . . . . . . . . . . 12
 CV   |
42 | 14, 15, 41 | nvgt0 26304 |
. . . . . . . . . . 11
                                                     |
43 | 12, 40, 42 | sylancr 669 |
. . . . . . . . . 10
                                           |
44 | 37, 43 | mpbid 214 |
. . . . . . . . 9
      
                    |
45 | 44 | ex 436 |
. . . . . . . 8
     
                     |
46 | 45 | adantl 468 |
. . . . . . 7
           
                     |
47 | 14, 41 | nmosetre 26405 |
. . . . . . . . . . . . . 14
        
    
            |
48 | 12, 27, 47 | mp2an 678 |
. . . . . . . . . . . . 13
      
           |
49 | | ressxr 9684 |
. . . . . . . . . . . . 13
 |
50 | 48, 49 | sstri 3441 |
. . . . . . . . . . . 12
      
           |
51 | | simpl 459 |
. . . . . . . . . . . . . . 15
      
  |
52 | | nmlno0lem.r |
. . . . . . . . . . . . . . . . 17
      |
53 | 2, 52 | nvscl 26247 |
. . . . . . . . . . . . . . . 16
                     |
54 | 1, 53 | mp3an1 1351 |
. . . . . . . . . . . . . . 15
       
             |
55 | 25, 51, 54 | syl2anc 667 |
. . . . . . . . . . . . . 14
                   |
56 | 19 | necon3i 2656 |
. . . . . . . . . . . . . . . . 17
       |
57 | 2, 52, 8, 3 | nv1 26305 |
. . . . . . . . . . . . . . . . . 18
 
                 |
58 | 1, 57 | mp3an1 1351 |
. . . . . . . . . . . . . . . . 17
                   |
59 | 56, 58 | sylan2 477 |
. . . . . . . . . . . . . . . 16
                       |
60 | | 1re 9642 |
. . . . . . . . . . . . . . . 16
 |
61 | 59, 60 | syl6eqel 2537 |
. . . . . . . . . . . . . . 15
                       |
62 | | eqle 9736 |
. . . . . . . . . . . . . . 15
                                            
  |
63 | 61, 59, 62 | syl2anc 667 |
. . . . . . . . . . . . . 14
                    
  |
64 | 1, 12, 13 | 3pm3.2i 1186 |
. . . . . . . . . . . . . . . . . 18

  |
65 | 2, 52, 30, 16 | lnomul 26401 |
. . . . . . . . . . . . . . . . . 18
  
       
 
                              |
66 | 64, 65 | mpan 676 |
. . . . . . . . . . . . . . . . 17
       
                               |
67 | 25, 51, 66 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
                                     |
68 | 67 | eqcomd 2457 |
. . . . . . . . . . . . . . 15
                                     |
69 | 68 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                                             |
70 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
                               |
71 | 70 | breq1d 4412 |
. . . . . . . . . . . . . . . 16
               
                 |
72 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
                               |
73 | 72 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
                                       |
74 | 73 | eqeq2d 2461 |
. . . . . . . . . . . . . . . 16
                                     
                                       |
75 | 71, 74 | anbi12d 717 |
. . . . . . . . . . . . . . 15
                                                                                                   |
76 | 75 | rspcev 3150 |
. . . . . . . . . . . . . 14
                                                                

                                  |
77 | 55, 63, 69, 76 | syl12anc 1266 |
. . . . . . . . . . . . 13
       
                                  |
78 | | fvex 5875 |
. . . . . . . . . . . . . 14
                   |
79 | | eqeq1 2455 |
. . . . . . . . . . . . . . . 16
                           
                             |
80 | 79 | anbi2d 710 |
. . . . . . . . . . . . . . 15
                        
                                            |
81 | 80 | rexbidv 2901 |
. . . . . . . . . . . . . 14
                    
    
         
                                   |
82 | 78, 81 | elab 3185 |
. . . . . . . . . . . . 13
                         
                                             |
83 | 77, 82 | sylibr 216 |
. . . . . . . . . . . 12
                               
            |
84 | | supxrub 11610 |
. . . . . . . . . . . 12
   
    
                             
    
          
                     
    
              |
85 | 50, 83, 84 | sylancr 669 |
. . . . . . . . . . 11
                        
   
    
              |
86 | 85 | adantll 720 |
. . . . . . . . . 10
       
    
                     
    
              |
87 | | nmlno0.3 |
. . . . . . . . . . . . . . 15
      |
88 | 2, 14, 3, 41, 87 | nmooval 26404 |
. . . . . . . . . . . . . 14
 
                 
              |
89 | 1, 12, 27, 88 | mp3an 1364 |
. . . . . . . . . . . . 13
            
             |
90 | 89 | eqeq1i 2456 |
. . . . . . . . . . . 12
    
   
    
              |
91 | 90 | biimpi 198 |
. . . . . . . . . . 11
        
    
              |
92 | 91 | ad2antrr 732 |
. . . . . . . . . 10
       
    
   
    
              |
93 | 86, 92 | breqtrd 4427 |
. . . . . . . . 9
       
    
                    |
94 | 14, 41 | nvcl 26288 |
. . . . . . . . . . . 12
                                     |
95 | 12, 40, 94 | sylancr 669 |
. . . . . . . . . . 11
                           |
96 | | 0re 9643 |
. . . . . . . . . . 11
 |
97 | | lenlt 9712 |
. . . . . . . . . . 11
                   
                                         |
98 | 95, 96, 97 | sylancl 668 |
. . . . . . . . . 10
                                               |
99 | 98 | adantll 720 |
. . . . . . . . 9
       
    
                  
                     |
100 | 93, 99 | mpbid 214 |
. . . . . . . 8
       
    
                    |
101 | 100 | ex 436 |
. . . . . . 7
           
                     |
102 | 46, 101 | pm2.65d 179 |
. . . . . 6
      
      |
103 | | nne 2628 |
. . . . . 6
    
      |
104 | 102, 103 | sylib 200 |
. . . . 5
             |
105 | | nmlno0.0 |
. . . . . . . 8
   |
106 | 2, 15, 105 | 0oval 26429 |
. . . . . . 7
 
       |
107 | 1, 12, 106 | mp3an12 1354 |
. . . . . 6
       |
108 | 107 | adantl 468 |
. . . . 5
             |
109 | 104, 108 | eqtr4d 2488 |
. . . 4
                 |
110 | 109 | ralrimiva 2802 |
. . 3
     
          |
111 | | ffn 5728 |
. . . . 5
    
  |
112 | 27, 111 | ax-mp 5 |
. . . 4
 |
113 | 2, 14, 105 | 0oo 26430 |
. . . . . 6
         |
114 | 1, 12, 113 | mp2an 678 |
. . . . 5
     |
115 | | ffn 5728 |
. . . . 5
    
  |
116 | 114, 115 | ax-mp 5 |
. . . 4
 |
117 | | eqfnfv 5976 |
. . . 4
 
  
           |
118 | 112, 116,
117 | mp2an 678 |
. . 3


          |
119 | 110, 118 | sylibr 216 |
. 2
       |
120 | | fveq2 5865 |
. . 3
           |
121 | 87, 105 | nmoo0 26432 |
. . . 4
         |
122 | 1, 12, 121 | mp2an 678 |
. . 3
     |
123 | 120, 122 | syl6eq 2501 |
. 2
       |
124 | 119, 123 | impbii 191 |
1
    
  |