Step | Hyp | Ref
| Expression |
1 | | vdwlem9.v |
. . . . 5
   |
2 | | vdwlem9.w |
. . . . 5
   |
3 | | vdw.r |
. . . . 5
   |
4 | | vdwlem9.h |
. . . . 5
               |
5 | | vdwlem9.f |
. . . . 5
                         |
6 | 1, 2, 3, 4, 5 | vdwlem4 14989 |
. . . 4
                 |
7 | | ovex 6348 |
. . . . 5
       |
8 | | ovex 6348 |
. . . . 5
     |
9 | 7, 8 | elmap 7531 |
. . . 4
            
                |
10 | 6, 9 | sylibr 217 |
. . 3
               |
11 | | vdwlem9.a |
. . 3
               MonoAP   |
12 | | breq2 4422 |
. . . 4
  MonoAP
MonoAP    |
13 | 12 | rspcv 3158 |
. . 3
              
             MonoAP
MonoAP    |
14 | 10, 11, 13 | sylc 62 |
. 2
 MonoAP   |
15 | | vdwlem9.k |
. . . . . 6
       |
16 | | eluz2nn 11231 |
. . . . . 6
    
  |
17 | 15, 16 | syl 17 |
. . . . 5
   |
18 | 17 | nnnn0d 10959 |
. . . 4
   |
19 | 8, 18, 6 | vdwmc 14983 |
. . 3
  MonoAP
  
   AP              |
20 | | vdwlem9.g |
. . . . . . . . 9
             PolyAP   MonoAP    |
21 | 20 | adantr 471 |
. . . . . . . 8
 
 
   AP                         PolyAP   MonoAP    |
22 | | simprr 771 |
. . . . . . . . . . . 12
 
 
   AP               AP             |
23 | 17 | adantr 471 |
. . . . . . . . . . . . 13
 
 
   AP               |
24 | | simprll 777 |
. . . . . . . . . . . . 13
 
 
   AP               |
25 | | simprlr 778 |
. . . . . . . . . . . . 13
 
 
   AP               |
26 | | vdwapid1 14980 |
. . . . . . . . . . . . 13
 
   AP      |
27 | 23, 24, 25, 26 | syl3anc 1276 |
. . . . . . . . . . . 12
 
 
   AP               AP      |
28 | 22, 27 | sseldd 3445 |
. . . . . . . . . . 11
 
 
   AP                      |
29 | | ffn 5755 |
. . . . . . . . . . . . . 14
              
      |
30 | 6, 29 | syl 17 |
. . . . . . . . . . . . 13
       |
31 | 30 | adantr 471 |
. . . . . . . . . . . 12
 
 
   AP                   |
32 | | fniniseg 6031 |
. . . . . . . . . . . 12
            
    
        |
33 | 31, 32 | syl 17 |
. . . . . . . . . . 11
 
 
   AP                    
    
        |
34 | 28, 33 | mpbid 215 |
. . . . . . . . . 10
 
 
   AP                         |
35 | 34 | simprd 469 |
. . . . . . . . 9
 
 
   AP                   |
36 | 6 | adantr 471 |
. . . . . . . . . 10
 
 
   AP                             |
37 | 34 | simpld 465 |
. . . . . . . . . 10
 
 
   AP                   |
38 | 36, 37 | ffvelrnd 6051 |
. . . . . . . . 9
 
 
   AP                         |
39 | 35, 38 | eqeltrrd 2541 |
. . . . . . . 8
 
 
   AP                     |
40 | | rsp 2766 |
. . . . . . . 8
 
         
 PolyAP   MonoAP
            PolyAP

 MonoAP     |
41 | 21, 39, 40 | sylc 62 |
. . . . . . 7
 
 
   AP                 PolyAP   MonoAP
   |
42 | 1 | adantr 471 |
. . . . . . . . . 10
 
 
   AP               |
43 | 2 | adantr 471 |
. . . . . . . . . 10
 
 
   AP               |
44 | 3 | adantr 471 |
. . . . . . . . . 10
 
 
   AP               |
45 | 4 | adantr 471 |
. . . . . . . . . 10
 
 
   AP                           |
46 | | vdwlem9.m |
. . . . . . . . . . 11
   |
47 | 46 | adantr 471 |
. . . . . . . . . 10
 
 
   AP               |
48 | | ovex 6348 |
. . . . . . . . . . . 12
     |
49 | | elmapg 7516 |
. . . . . . . . . . . 12
                         |
50 | 44, 48, 49 | sylancl 673 |
. . . . . . . . . . 11
 
 
   AP                   
           |
51 | 39, 50 | mpbid 215 |
. . . . . . . . . 10
 
 
   AP                       |
52 | 15 | adantr 471 |
. . . . . . . . . 10
 
 
   AP                   |
53 | 42, 43, 44, 45, 5, 47, 51, 52, 24, 25, 22 | vdwlem7 14992 |
. . . . . . . . 9
 
 
   AP                 PolyAP   
   PolyAP 
 MonoAP     |
54 | | olc 390 |
. . . . . . . . . 10
   MonoAP
      PolyAP 
 MonoAP    |
55 | 54 | a1i 11 |
. . . . . . . . 9
 
 
   AP                MonoAP       PolyAP   MonoAP     |
56 | 53, 55 | jaod 386 |
. . . . . . . 8
 
 
   AP                  PolyAP   MonoAP 
      PolyAP 
 MonoAP     |
57 | | oveq1 6327 |
. . . . . . . . . . . . . . . . . . 19
       |
58 | 57 | oveq1d 6335 |
. . . . . . . . . . . . . . . . . 18
           |
59 | 58 | oveq2d 6336 |
. . . . . . . . . . . . . . . . 17
 
             |
60 | 59 | oveq2d 6336 |
. . . . . . . . . . . . . . . 16
                   |
61 | 60 | fveq2d 5896 |
. . . . . . . . . . . . . . 15
                           |
62 | 61 | mpteq2dv 4506 |
. . . . . . . . . . . . . 14
                                       |
63 | 48 | mptex 6166 |
. . . . . . . . . . . . . 14
                   |
64 | 62, 5, 63 | fvmpt 5976 |
. . . . . . . . . . . . 13
                             |
65 | 37, 64 | syl 17 |
. . . . . . . . . . . 12
 
 
   AP                                     |
66 | 65, 35 | eqtr3d 2498 |
. . . . . . . . . . 11
 
 
   AP                                 |
67 | 66 | breq2d 4430 |
. . . . . . . . . 10
 
 
   AP                MonoAP                  
  MonoAP    |
68 | 18 | adantr 471 |
. . . . . . . . . . . 12
 
 
   AP               |
69 | | peano2nn0 10944 |
. . . . . . . . . . . 12

    |
70 | 68, 69 | syl 17 |
. . . . . . . . . . 11
 
 
   AP             
   |
71 | | nnm1nn0 10945 |
. . . . . . . . . . . . . 14
     |
72 | 24, 71 | syl 17 |
. . . . . . . . . . . . 13
 
 
   AP                 |
73 | | nn0nnaddcl 10935 |
. . . . . . . . . . . . 13
   
       |
74 | 72, 42, 73 | syl2anc 671 |
. . . . . . . . . . . 12
 
 
   AP                   |
75 | 43, 74 | nnmulcld 10690 |
. . . . . . . . . . 11
 
 
   AP             
       |
76 | 24, 42 | nnaddcld 10689 |
. . . . . . . . . . . . . . 15
 
 
   AP                 |
77 | 43, 76 | nnmulcld 10690 |
. . . . . . . . . . . . . 14
 
 
   AP             
     |
78 | 77 | nnzd 11073 |
. . . . . . . . . . . . 13
 
 
   AP             
     |
79 | | 2nn 10801 |
. . . . . . . . . . . . . . . . 17
 |
80 | | nnmulcl 10665 |
. . . . . . . . . . . . . . . . 17
 
     |
81 | 79, 1, 80 | sylancr 674 |
. . . . . . . . . . . . . . . 16
     |
82 | 2, 81 | nnmulcld 10690 |
. . . . . . . . . . . . . . 15
       |
83 | 82 | nnzd 11073 |
. . . . . . . . . . . . . 14
       |
84 | 83 | adantr 471 |
. . . . . . . . . . . . 13
 
 
   AP             
     |
85 | 24 | nnred 10657 |
. . . . . . . . . . . . . . . 16
 
 
   AP               |
86 | 42 | nnred 10657 |
. . . . . . . . . . . . . . . 16
 
 
   AP               |
87 | | elfzle2 11838 |
. . . . . . . . . . . . . . . . 17
       |
88 | 37, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
 
 
   AP               |
89 | 85, 86, 86, 88 | leadd1dd 10260 |
. . . . . . . . . . . . . . 15
 
 
   AP                   |
90 | 42 | nncnd 10658 |
. . . . . . . . . . . . . . . 16
 
 
   AP               |
91 | 90 | 2timesd 10889 |
. . . . . . . . . . . . . . 15
 
 
   AP                   |
92 | 89, 91 | breqtrrd 4445 |
. . . . . . . . . . . . . 14
 
 
   AP                   |
93 | 76 | nnred 10657 |
. . . . . . . . . . . . . . 15
 
 
   AP                 |
94 | 81 | nnred 10657 |
. . . . . . . . . . . . . . . 16
     |
95 | 94 | adantr 471 |
. . . . . . . . . . . . . . 15
 
 
   AP                 |
96 | 43 | nnred 10657 |
. . . . . . . . . . . . . . 15
 
 
   AP               |
97 | 43 | nngt0d 10686 |
. . . . . . . . . . . . . . 15
 
 
   AP               |
98 | | lemul2 10491 |
. . . . . . . . . . . . . . 15
      
 
    
    
      |
99 | 93, 95, 96, 97, 98 | syl112anc 1280 |
. . . . . . . . . . . . . 14
 
 
   AP               
 
    
      |
100 | 92, 99 | mpbid 215 |
. . . . . . . . . . . . 13
 
 
   AP             
         |
101 | | eluz2 11199 |
. . . . . . . . . . . . 13
        
             
  
       |
102 | 78, 84, 100, 101 | syl3anbrc 1198 |
. . . . . . . . . . . 12
 
 
   AP             
      
      |
103 | 43 | nncnd 10658 |
. . . . . . . . . . . . . . 15
 
 
   AP               |
104 | | 1cnd 9690 |
. . . . . . . . . . . . . . 15
 
 
   AP               |
105 | 72 | nn0cnd 10961 |
. . . . . . . . . . . . . . . 16
 
 
   AP                 |
106 | 105, 90 | addcld 9693 |
. . . . . . . . . . . . . . 15
 
 
   AP                   |
107 | 103, 104,
106 | adddid 9698 |
. . . . . . . . . . . . . 14
 
 
   AP             
                   |
108 | 104, 105,
90 | addassd 9696 |
. . . . . . . . . . . . . . . 16
 
 
   AP                           |
109 | | ax-1cn 9628 |
. . . . . . . . . . . . . . . . . 18
 |
110 | 24 | nncnd 10658 |
. . . . . . . . . . . . . . . . . 18
 
 
   AP               |
111 | | pncan3 9914 |
. . . . . . . . . . . . . . . . . 18
 
       |
112 | 109, 110,
111 | sylancr 674 |
. . . . . . . . . . . . . . . . 17
 
 
   AP                   |
113 | 112 | oveq1d 6335 |
. . . . . . . . . . . . . . . 16
 
 
   AP                       |
114 | 108, 113 | eqtr3d 2498 |
. . . . . . . . . . . . . . 15
 
 
   AP                       |
115 | 114 | oveq2d 6336 |
. . . . . . . . . . . . . 14
 
 
   AP             
             |
116 | 103 | mulid1d 9691 |
. . . . . . . . . . . . . . 15
 
 
   AP             
   |
117 | 116 | oveq1d 6335 |
. . . . . . . . . . . . . 14
 
 
   AP                        
        |
118 | 107, 115,
117 | 3eqtr3d 2504 |
. . . . . . . . . . . . 13
 
 
   AP             
             |
119 | 118 | fveq2d 5896 |
. . . . . . . . . . . 12
 
 
   AP                                   |
120 | 102, 119 | eleqtrd 2542 |
. . . . . . . . . . 11
 
 
   AP             
      
          |
121 | | oveq1 6327 |
. . . . . . . . . . . . 13
                   |
122 | 121 | fveq2d 5896 |
. . . . . . . . . . . 12
                           |
123 | 122 | cbvmptv 4511 |
. . . . . . . . . . 11
                                     |
124 | 44, 70, 43, 75, 45, 120, 123 | vdwlem2 14987 |
. . . . . . . . . 10
 
 
   AP                MonoAP                     MonoAP    |
125 | 67, 124 | sylbird 243 |
. . . . . . . . 9
 
 
   AP                MonoAP 
 MonoAP    |
126 | 125 | orim2d 856 |
. . . . . . . 8
 
 
   AP                    PolyAP   MonoAP 
      PolyAP 
 MonoAP     |
127 | 56, 126 | syld 45 |
. . . . . . 7
 
 
   AP                  PolyAP   MonoAP 
      PolyAP 
 MonoAP     |
128 | 41, 127 | mpd 15 |
. . . . . 6
 
 
   AP                   PolyAP   MonoAP    |
129 | 128 | expr 624 |
. . . . 5
 
      AP   
      
      PolyAP 
 MonoAP     |
130 | 129 | rexlimdvva 2898 |
. . . 4
      AP   
      
      PolyAP 
 MonoAP     |
131 | 130 | exlimdv 1790 |
. . 3
     
  AP                 PolyAP   MonoAP     |
132 | 19, 131 | sylbid 223 |
. 2
  MonoAP       PolyAP   MonoAP     |
133 | 14, 132 | mpd 15 |
1
       PolyAP   MonoAP    |