Step | Hyp | Ref
| Expression |
1 | | peano2nn0 10934 |
. . . . 5

    |
2 | | vdwapval 15002 |
. . . . 5
   
    AP     
                 |
3 | 1, 2 | syl3an1 1325 |
. . . 4
 
    AP     
                 |
4 | | simp1 1030 |
. . . . . . . . . . . . 13
 
   |
5 | 4 | nn0cnd 10951 |
. . . . . . . . . . . 12
 
   |
6 | | ax-1cn 9615 |
. . . . . . . . . . . 12
 |
7 | | pncan 9901 |
. . . . . . . . . . . 12
 
       |
8 | 5, 6, 7 | sylancl 675 |
. . . . . . . . . . 11
 
       |
9 | 8 | oveq2d 6324 |
. . . . . . . . . 10
 
               |
10 | 9 | eleq2d 2534 |
. . . . . . . . 9
 
         
       |
11 | | nn0uz 11217 |
. . . . . . . . . . 11
     |
12 | 4, 11 | syl6eleq 2559 |
. . . . . . . . . 10
 
       |
13 | | elfzp12 11899 |
. . . . . . . . . 10
    
                |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
 
     
           |
15 | 10, 14 | bitrd 261 |
. . . . . . . 8
 
         
           |
16 | 15 | anbi1d 719 |
. . . . . . 7
 
                          
      |
17 | | andir 885 |
. . . . . . 7
              
             

       |
18 | 16, 17 | syl6bb 269 |
. . . . . 6
 
                   
                   |
19 | 18 | exbidv 1776 |
. . . . 5
 
                 
               
         |
20 | | df-rex 2762 |
. . . . 5
            
 
                  |
21 | | 19.43 1753 |
. . . . . 6
      
               
                 

       |
22 | 21 | bicomi 207 |
. . . . 5
      
             
         
                  |
23 | 19, 20, 22 | 3bitr4g 296 |
. . . 4
 
  
          
 
                 

        |
24 | 3, 23 | bitrd 261 |
. . 3
 
    AP     
                 

        |
25 | | nncn 10639 |
. . . . . . . . . . 11
   |
26 | 25 | 3ad2ant3 1053 |
. . . . . . . . . 10
 
   |
27 | 26 | mul02d 9849 |
. . . . . . . . 9
 
     |
28 | 27 | oveq2d 6324 |
. . . . . . . 8
 
 
       |
29 | | nncn 10639 |
. . . . . . . . . 10
   |
30 | 29 | 3ad2ant2 1052 |
. . . . . . . . 9
 
   |
31 | 30 | addid1d 9851 |
. . . . . . . 8
 
 
   |
32 | 28, 31 | eqtrd 2505 |
. . . . . . 7
 
 
     |
33 | 32 | eqeq2d 2481 |
. . . . . 6
 
     
   |
34 | | c0ex 9655 |
. . . . . . 7
 |
35 | | oveq1 6315 |
. . . . . . . . 9
       |
36 | 35 | oveq2d 6324 |
. . . . . . . 8
 
         |
37 | 36 | eqeq2d 2481 |
. . . . . . 7
     

      |
38 | 34, 37 | ceqsexv 3070 |
. . . . . 6
        

     |
39 | | elsn 3973 |
. . . . . 6
     |
40 | 33, 38, 39 | 3bitr4g 296 |
. . . . 5
 
         
     |
41 | | simpr 468 |
. . . . . . . . . . . . . 14
  

      
        |
42 | | 0p1e1 10743 |
. . . . . . . . . . . . . . 15
   |
43 | 42 | oveq1i 6318 |
. . . . . . . . . . . . . 14
           |
44 | 41, 43 | syl6eleq 2559 |
. . . . . . . . . . . . 13
  

      
      |
45 | | 1zzd 10992 |
. . . . . . . . . . . . . 14
  

      
  |
46 | 4 | adantr 472 |
. . . . . . . . . . . . . . 15
  

      
  |
47 | 46 | nn0zd 11061 |
. . . . . . . . . . . . . 14
  

      
  |
48 | | elfzelz 11826 |
. . . . . . . . . . . . . . 15
         |
49 | 48 | adantl 473 |
. . . . . . . . . . . . . 14
  

      
  |
50 | | fzsubel 11860 |
. . . . . . . . . . . . . 14
                         |
51 | 45, 47, 49, 45, 50 | syl22anc 1293 |
. . . . . . . . . . . . 13
  

      
                  |
52 | 44, 51 | mpbid 215 |
. . . . . . . . . . . 12
  

      
       
    |
53 | | 1m1e0 10700 |
. . . . . . . . . . . . 13
   |
54 | 53 | oveq1i 6318 |
. . . . . . . . . . . 12
           
   |
55 | 52, 54 | syl6eleq 2559 |
. . . . . . . . . . 11
  

      
     
    |
56 | 49 | zcnd 11064 |
. . . . . . . . . . . . . . . . 17
  

      
  |
57 | | 1cnd 9677 |
. . . . . . . . . . . . . . . . 17
  

      
  |
58 | 26 | adantr 472 |
. . . . . . . . . . . . . . . . 17
  

      
  |
59 | 56, 57, 58 | subdird 10096 |
. . . . . . . . . . . . . . . 16
  

      
            |
60 | 58 | mulid2d 9679 |
. . . . . . . . . . . . . . . . 17
  

      
    |
61 | 60 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
  

      
            |
62 | 59, 61 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
  

      
          |
63 | 62 | oveq2d 6324 |
. . . . . . . . . . . . . 14
  

      
              |
64 | 56, 58 | mulcld 9681 |
. . . . . . . . . . . . . . 15
  

      
    |
65 | 58, 64 | pncan3d 10008 |
. . . . . . . . . . . . . 14
  

      
          |
66 | 63, 65 | eqtr2d 2506 |
. . . . . . . . . . . . 13
  

      
          |
67 | 66 | oveq2d 6324 |
. . . . . . . . . . . 12
  

      
              |
68 | 30 | adantr 472 |
. . . . . . . . . . . . 13
  

      
  |
69 | | subcl 9894 |
. . . . . . . . . . . . . . 15
 
     |
70 | 56, 6, 69 | sylancl 675 |
. . . . . . . . . . . . . 14
  

      
    |
71 | 70, 58 | mulcld 9681 |
. . . . . . . . . . . . 13
  

      
      |
72 | 68, 58, 71 | addassd 9683 |
. . . . . . . . . . . 12
  

      
 
                |
73 | 67, 72 | eqtr4d 2508 |
. . . . . . . . . . 11
  

      
              |
74 | | oveq1 6315 |
. . . . . . . . . . . . . 14
           |
75 | 74 | oveq2d 6324 |
. . . . . . . . . . . . 13
                   |
76 | 75 | eqeq2d 2481 |
. . . . . . . . . . . 12
             
               |
77 | 76 | rspcev 3136 |
. . . . . . . . . . 11
          
                                |
78 | 55, 73, 77 | syl2anc 673 |
. . . . . . . . . 10
  

      
    
    
          |
79 | | eqeq1 2475 |
. . . . . . . . . . 11
  
        
             |
80 | 79 | rexbidv 2892 |
. . . . . . . . . 10
  
   
            
    
    
           |
81 | 78, 80 | syl5ibrcom 230 |
. . . . . . . . 9
  

      
  
      
            |
82 | 81 | expimpd 614 |
. . . . . . . 8
 
             
    
            |
83 | 82 | exlimdv 1787 |
. . . . . . 7
 
          

        
            |
84 | | simpr 468 |
. . . . . . . . . . . 12
  

               |
85 | | 0zd 10973 |
. . . . . . . . . . . . 13
  

         |
86 | 4 | adantr 472 |
. . . . . . . . . . . . . . 15
  

         |
87 | 86 | nn0zd 11061 |
. . . . . . . . . . . . . 14
  

         |
88 | | peano2zm 11004 |
. . . . . . . . . . . . . 14
 
   |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . 13
  

           |
90 | | elfzelz 11826 |
. . . . . . . . . . . . . 14
         |
91 | 90 | adantl 473 |
. . . . . . . . . . . . 13
  

         |
92 | | 1zzd 10992 |
. . . . . . . . . . . . 13
  

         |
93 | | fzaddel 11859 |
. . . . . . . . . . . . 13
                               |
94 | 85, 89, 91, 92, 93 | syl22anc 1293 |
. . . . . . . . . . . 12
  

           
                 |
95 | 84, 94 | mpbid 215 |
. . . . . . . . . . 11
  

                     |
96 | 86 | nn0cnd 10951 |
. . . . . . . . . . . . 13
  

         |
97 | | npcan 9904 |
. . . . . . . . . . . . 13
 
       |
98 | 96, 6, 97 | sylancl 675 |
. . . . . . . . . . . 12
  

             |
99 | 98 | oveq2d 6324 |
. . . . . . . . . . 11
  

                         |
100 | 95, 99 | eleqtrd 2551 |
. . . . . . . . . 10
  

                 |
101 | 30 | adantr 472 |
. . . . . . . . . . . 12
  

         |
102 | 26 | adantr 472 |
. . . . . . . . . . . 12
  

         |
103 | 91 | zcnd 11064 |
. . . . . . . . . . . . 13
  

         |
104 | 103, 102 | mulcld 9681 |
. . . . . . . . . . . 12
  

           |
105 | 101, 102,
104 | addassd 9683 |
. . . . . . . . . . 11
  

                     |
106 | | 1cnd 9677 |
. . . . . . . . . . . . . 14
  

         |
107 | 103, 106,
102 | adddird 9686 |
. . . . . . . . . . . . 13
  

                   |
108 | 102, 104 | addcomd 9853 |
. . . . . . . . . . . . . 14
  

        
        |
109 | 102 | mulid2d 9679 |
. . . . . . . . . . . . . . 15
  

           |
110 | 109 | oveq2d 6324 |
. . . . . . . . . . . . . 14
  

                   |
111 | 108, 110 | eqtr4d 2508 |
. . . . . . . . . . . . 13
  

        
          |
112 | 107, 111 | eqtr4d 2508 |
. . . . . . . . . . . 12
  

                 |
113 | 112 | oveq2d 6324 |
. . . . . . . . . . 11
  

                     |
114 | 105, 113 | eqtr4d 2508 |
. . . . . . . . . 10
  

                     |
115 | | ovex 6336 |
. . . . . . . . . . 11
   |
116 | | eleq1 2537 |
. . . . . . . . . . . 12
         
           |
117 | | oveq1 6315 |
. . . . . . . . . . . . . 14
           |
118 | 117 | oveq2d 6324 |
. . . . . . . . . . . . 13
   
           |
119 | 118 | eqeq2d 2481 |
. . . . . . . . . . . 12
             
 
             |
120 | 116, 119 | anbi12d 725 |
. . . . . . . . . . 11
                              
 
              |
121 | 115, 120 | spcev 3127 |
. . . . . . . . . 10
                                       
     |
122 | 100, 114,
121 | syl2anc 673 |
. . . . . . . . 9
  

                       
     |
123 | | eqeq1 2475 |
. . . . . . . . . . 11
           
 
           |
124 | 123 | anbi2d 718 |
. . . . . . . . . 10
                          
 
            |
125 | 124 | exbidv 1776 |
. . . . . . . . 9
                

   
                       |
126 | 122, 125 | syl5ibrcom 230 |
. . . . . . . 8
  

             
                 |
127 | 126 | rexlimdva 2871 |
. . . . . . 7
 
  
                              |
128 | 83, 127 | impbid 195 |
. . . . . 6
 
          

   
    
            |
129 | | nnaddcl 10653 |
. . . . . . . 8
 
     |
130 | 129 | 3adant1 1048 |
. . . . . . 7
 
 
   |
131 | | vdwapval 15002 |
. . . . . . 7
  

      AP   
    
            |
132 | 130, 131 | syld3an2 1339 |
. . . . . 6
 
      AP   
    
            |
133 | 128, 132 | bitr4d 264 |
. . . . 5
 
          

   
    AP       |
134 | 40, 133 | orbi12d 724 |
. . . 4
 
                   
        
 
  AP        |
135 | | elun 3565 |
. . . 4
   
 
  AP    
  
 
  AP       |
136 | 134, 135 | syl6bbr 271 |
. . 3
 
                   
     
       AP        |
137 | 24, 136 | bitrd 261 |
. 2
 
    AP     
       AP        |
138 | 137 | eqrdv 2469 |
1
 
   AP             AP       |