Proof of Theorem bcpasc
Step | Hyp | Ref
| Expression |
1 | | peano2nn0 8869 |
. . . . . 6

    |
2 | | elfzp12 9720 |
. . . . . . 7
      
    
        
      |
3 | | nn0uz 9210 |
. . . . . . 7
     |
4 | 2, 3 | eleq2s 2194 |
. . . . . 6
  
      
      
      |
5 | 1, 4 | syl 14 |
. . . . 5

      
      
      |
6 | | 1p0e1 8694 |
. . . . . . . 8
   |
7 | | bcn0 10342 |
. . . . . . . . 9

    |
8 | | 0z 8917 |
. . . . . . . . . . 11
 |
9 | | 1z 8932 |
. . . . . . . . . . 11
 |
10 | | zsubcl 8947 |
. . . . . . . . . . 11
 
     |
11 | 8, 9, 10 | mp2an 420 |
. . . . . . . . . 10
   |
12 | | 0re 7638 |
. . . . . . . . . . . 12
 |
13 | | ltm1 8462 |
. . . . . . . . . . . 12
     |
14 | 12, 13 | ax-mp 7 |
. . . . . . . . . . 11
   |
15 | 14 | orci 691 |
. . . . . . . . . 10
       |
16 | | bcval4 10339 |
. . . . . . . . . 10
      
   
      |
17 | 11, 15, 16 | mp3an23 1275 |
. . . . . . . . 9

      |
18 | 7, 17 | oveq12d 5724 |
. . . . . . . 8

            |
19 | | bcn0 10342 |
. . . . . . . . 9
  
      |
20 | 1, 19 | syl 14 |
. . . . . . . 8

      |
21 | 6, 18, 20 | 3eqtr4a 2158 |
. . . . . . 7

              |
22 | | oveq2 5714 |
. . . . . . . . 9
       |
23 | | oveq1 5713 |
. . . . . . . . . 10
 
     |
24 | 23 | oveq2d 5722 |
. . . . . . . . 9
           |
25 | 22, 24 | oveq12d 5724 |
. . . . . . . 8
                   |
26 | | oveq2 5714 |
. . . . . . . 8
           |
27 | 25, 26 | eqeq12d 2114 |
. . . . . . 7
             
               |
28 | 21, 27 | syl5ibrcom 156 |
. . . . . 6

                |
29 | | simpr 109 |
. . . . . . . . 9
 
                   |
30 | | 0p1e1 8692 |
. . . . . . . . . 10
   |
31 | 30 | oveq1i 5716 |
. . . . . . . . 9
           
   |
32 | 29, 31 | syl6eleq 2192 |
. . . . . . . 8
 
                 |
33 | | nn0p1nn 8868 |
. . . . . . . . . . 11

    |
34 | | nnuz 9211 |
. . . . . . . . . . 11
     |
35 | 33, 34 | syl6eleq 2192 |
. . . . . . . . . 10

        |
36 | | fzm1 9721 |
. . . . . . . . . . 11
      
    
                 |
37 | 36 | biimpa 292 |
. . . . . . . . . 10
           
   
             |
38 | 35, 37 | sylan 279 |
. . . . . . . . 9
 
                     |
39 | | nn0cn 8839 |
. . . . . . . . . . . . . . 15

  |
40 | | ax-1cn 7588 |
. . . . . . . . . . . . . . 15
 |
41 | | pncan 7839 |
. . . . . . . . . . . . . . 15
 
       |
42 | 39, 40, 41 | sylancl 407 |
. . . . . . . . . . . . . 14

      |
43 | 42 | oveq2d 5722 |
. . . . . . . . . . . . 13

              |
44 | 43 | eleq2d 2169 |
. . . . . . . . . . . 12

        
       |
45 | 44 | biimpa 292 |
. . . . . . . . . . 11
 
               |
46 | | 1eluzge0 9219 |
. . . . . . . . . . . . . . 15
     |
47 | | fzss1 9684 |
. . . . . . . . . . . . . . 15
    
          |
48 | 46, 47 | ax-mp 7 |
. . . . . . . . . . . . . 14
         |
49 | 48 | sseli 3043 |
. . . . . . . . . . . . 13
           |
50 | | bcp1n 10348 |
. . . . . . . . . . . . 13
                       |
51 | 49, 50 | syl 14 |
. . . . . . . . . . . 12
                       |
52 | | bcrpcl 10340 |
. . . . . . . . . . . . . . . . 17
         |
53 | 49, 52 | syl 14 |
. . . . . . . . . . . . . . . 16
         |
54 | 53 | rpcnd 9332 |
. . . . . . . . . . . . . . 15
         |
55 | | elfzuz2 9650 |
. . . . . . . . . . . . . . . . . 18
           |
56 | 55, 34 | syl6eleqr 2193 |
. . . . . . . . . . . . . . . . 17
       |
57 | 56 | peano2nnd 8593 |
. . . . . . . . . . . . . . . 16
     
   |
58 | 57 | nncnd 8592 |
. . . . . . . . . . . . . . 15
     
   |
59 | 56 | nncnd 8592 |
. . . . . . . . . . . . . . . . . 18
       |
60 | | 1cnd 7654 |
. . . . . . . . . . . . . . . . . 18
       |
61 | | elfzelz 9647 |
. . . . . . . . . . . . . . . . . . 19
       |
62 | 61 | zcnd 9026 |
. . . . . . . . . . . . . . . . . 18
       |
63 | 59, 60, 62 | addsubd 7965 |
. . . . . . . . . . . . . . . . 17
               |
64 | | fznn0sub 9678 |
. . . . . . . . . . . . . . . . . 18
     
   |
65 | | nn0p1nn 8868 |
. . . . . . . . . . . . . . . . . 18
  
      |
66 | 64, 65 | syl 14 |
. . . . . . . . . . . . . . . . 17
           |
67 | 63, 66 | eqeltrd 2176 |
. . . . . . . . . . . . . . . 16
           |
68 | 67 | nncnd 8592 |
. . . . . . . . . . . . . . 15
           |
69 | 67 | nnap0d 8624 |
. . . . . . . . . . . . . . 15
         #   |
70 | 54, 58, 68, 69 | div12apd 8448 |
. . . . . . . . . . . . . 14
                               |
71 | 67 | nnrpd 9329 |
. . . . . . . . . . . . . . . . 17
           |
72 | 53, 71 | rpdivcld 9348 |
. . . . . . . . . . . . . . . 16
               |
73 | 72 | rpcnd 9332 |
. . . . . . . . . . . . . . 15
               |
74 | 58, 73 | mulcomd 7659 |
. . . . . . . . . . . . . 14
                               |
75 | 70, 74 | eqtrd 2132 |
. . . . . . . . . . . . 13
                               |
76 | 58, 62 | npcand 7948 |
. . . . . . . . . . . . . 14
               |
77 | 76 | oveq2d 5722 |
. . . . . . . . . . . . 13
                                   |
78 | 73, 68, 62 | adddid 7662 |
. . . . . . . . . . . . 13
                                                 |
79 | 75, 77, 78 | 3eqtr2d 2138 |
. . . . . . . . . . . 12
                                             |
80 | 54, 68, 69 | divcanap1d 8412 |
. . . . . . . . . . . . 13
                       |
81 | | elfznn 9675 |
. . . . . . . . . . . . . . . 16
       |
82 | 81 | nnap0d 8624 |
. . . . . . . . . . . . . . 15
     #   |
83 | 54, 68, 62, 69, 82 | divdivap2d 8444 |
. . . . . . . . . . . . . 14
                           |
84 | | bcm1k 10347 |
. . . . . . . . . . . . . . . 16
         
    
      |
85 | 59, 62, 60 | subsub3d 7974 |
. . . . . . . . . . . . . . . . . 18
     
         |
86 | 85 | oveq1d 5721 |
. . . . . . . . . . . . . . . . 17
       
           |
87 | 86 | oveq2d 5722 |
. . . . . . . . . . . . . . . 16
       
                       |
88 | 84, 87 | eqtrd 2132 |
. . . . . . . . . . . . . . 15
         
           |
89 | | fzelp1 9695 |
. . . . . . . . . . . . . . . . . . . 20
        
    |
90 | 57 | nnzd 9024 |
. . . . . . . . . . . . . . . . . . . . 21
     
   |
91 | | elfzm1b 9719 |
. . . . . . . . . . . . . . . . . . . . 21
  
      
               |
92 | 61, 90, 91 | syl2anc 406 |
. . . . . . . . . . . . . . . . . . . 20
     
     
             |
93 | 89, 92 | mpbid 146 |
. . . . . . . . . . . . . . . . . . 19
     
           |
94 | 59, 40, 41 | sylancl 407 |
. . . . . . . . . . . . . . . . . . . 20
           |
95 | 94 | oveq2d 5722 |
. . . . . . . . . . . . . . . . . . 19
                   |
96 | 93, 95 | eleqtrd 2178 |
. . . . . . . . . . . . . . . . . 18
     
       |
97 | | bcrpcl 10340 |
. . . . . . . . . . . . . . . . . 18
             |
98 | 96, 97 | syl 14 |
. . . . . . . . . . . . . . . . 17
           |
99 | 98 | rpcnd 9332 |
. . . . . . . . . . . . . . . 16
           |
100 | 81 | nnrpd 9329 |
. . . . . . . . . . . . . . . . . 18
       |
101 | 71, 100 | rpdivcld 9348 |
. . . . . . . . . . . . . . . . 17
             |
102 | 101 | rpcnd 9332 |
. . . . . . . . . . . . . . . 16
             |
103 | 68, 62, 69, 82 | divap0d 8427 |
. . . . . . . . . . . . . . . 16
           #   |
104 | 54, 99, 102, 103 | divmulap3d 8446 |
. . . . . . . . . . . . . . 15
                   
    
            |
105 | 88, 104 | mpbird 166 |
. . . . . . . . . . . . . 14
                
    |
106 | 54, 62, 68, 69 | div23apd 8449 |
. . . . . . . . . . . . . 14
                           |
107 | 83, 105, 106 | 3eqtr3rd 2141 |
. . . . . . . . . . . . 13
                
    |
108 | 80, 107 | oveq12d 5724 |
. . . . . . . . . . . 12
                                   
     |
109 | 51, 79, 108 | 3eqtrrd 2137 |
. . . . . . . . . . 11
                   |
110 | 45, 109 | syl 14 |
. . . . . . . . . 10
 
             
         |
111 | | oveq2 5714 |
. . . . . . . . . . . . 13
      
    |
112 | 33 | nnzd 9024 |
. . . . . . . . . . . . . 14

    |
113 | | nn0re 8838 |
. . . . . . . . . . . . . . . 16

  |
114 | 113 | ltp1d 8546 |
. . . . . . . . . . . . . . 15

    |
115 | 114 | olcd 694 |
. . . . . . . . . . . . . 14

        |
116 | | bcval4 10339 |
. . . . . . . . . . . . . 14
  
   
   
      |
117 | 112, 115,
116 | mpd3an23 1285 |
. . . . . . . . . . . . 13

      |
118 | 111, 117 | sylan9eqr 2154 |
. . . . . . . . . . . 12
 
       |
119 | | oveq1 5713 |
. . . . . . . . . . . . . . 15
   
       |
120 | 119, 42 | sylan9eqr 2154 |
. . . . . . . . . . . . . 14
 
       |
121 | 120 | oveq2d 5722 |
. . . . . . . . . . . . 13
 
    
      |
122 | | bcnn 10344 |
. . . . . . . . . . . . . 14

    |
123 | 122 | adantr 272 |
. . . . . . . . . . . . 13
 
       |
124 | 121, 123 | eqtrd 2132 |
. . . . . . . . . . . 12
 
    
    |
125 | 118, 124 | oveq12d 5724 |
. . . . . . . . . . 11
 
       
       |
126 | | oveq2 5714 |
. . . . . . . . . . . 12
               |
127 | | bcnn 10344 |
. . . . . . . . . . . . 13
  
        |
128 | 1, 127 | syl 14 |
. . . . . . . . . . . 12

        |
129 | 126, 128 | sylan9eqr 2154 |
. . . . . . . . . . 11
 
         |
130 | 30, 125, 129 | 3eqtr4a 2158 |
. . . . . . . . . 10
 
       
         |
131 | 110, 130 | jaodan 752 |
. . . . . . . . 9
  
           
    
         |
132 | 38, 131 | syldan 278 |
. . . . . . . 8
 
           
         |
133 | 32, 132 | syldan 278 |
. . . . . . 7
 
             
         |
134 | 133 | ex 114 |
. . . . . 6

                        |
135 | 28, 134 | jaod 678 |
. . . . 5

               
          |
136 | 5, 135 | sylbid 149 |
. . . 4

                      |
137 | 136 | imp 123 |
. . 3
 
           
         |
138 | 137 | adantlr 464 |
. 2
          
    
         |
139 | | 00id 7774 |
. . 3
   |
140 | | fzelp1 9695 |
. . . . . 6
        
    |
141 | 140 | con3i 602 |
. . . . 5
      
      |
142 | | bcval3 10338 |
. . . . . 6
 
         |
143 | 142 | 3expa 1149 |
. . . . 5
             |
144 | 141, 143 | sylan2 282 |
. . . 4
       
       |
145 | | simpll 499 |
. . . . 5
       
     |
146 | | simplr 500 |
. . . . . 6
       
     |
147 | | peano2zm 8944 |
. . . . . 6
 
   |
148 | 146, 147 | syl 14 |
. . . . 5
       
   
   |
149 | 39 | adantr 272 |
. . . . . . . . . 10
 
   |
150 | 149, 40, 41 | sylancl 407 |
. . . . . . . . 9
 
       |
151 | 150 | oveq2d 5722 |
. . . . . . . 8
 
               |
152 | 151 | eleq2d 2169 |
. . . . . . 7
 
                     |
153 | | id 19 |
. . . . . . . . 9
   |
154 | 1 | nn0zd 9023 |
. . . . . . . . 9

    |
155 | 153, 154,
91 | syl2anr 286 |
. . . . . . . 8
 
                     |
156 | | fzp1ss 9694 |
. . . . . . . . . . 11
                 |
157 | 8, 156 | ax-mp 7 |
. . . . . . . . . 10
           
   |
158 | 31, 157 | eqsstr3i 3080 |
. . . . . . . . 9
         
   |
159 | 158 | sseli 3043 |
. . . . . . . 8
          
    |
160 | 155, 159 | syl6bir 163 |
. . . . . . 7
 
                     |
161 | 152, 160 | sylbird 169 |
. . . . . 6
 
                 |
162 | 161 | con3dimp 604 |
. . . . 5
       
   
       |
163 | | bcval3 10338 |
. . . . 5
  
         
    |
164 | 145, 148,
162, 163 | syl3anc 1184 |
. . . 4
       
         |
165 | 144, 164 | oveq12d 5724 |
. . 3
       
               |
166 | 145, 1 | syl 14 |
. . . 4
       
   
   |
167 | | simpr 109 |
. . . 4
       
  
        |
168 | | bcval3 10338 |
. . . 4
   
             |
169 | 166, 146,
167, 168 | syl3anc 1184 |
. . 3
       
         |
170 | 139, 165,
169 | 3eqtr4a 2158 |
. 2
       
                 |
171 | | simpr 109 |
. . 3
 
   |
172 | | 0zd 8918 |
. . 3
 
   |
173 | 112 | adantr 272 |
. . 3
 
     |
174 | | fzdcel 9661 |
. . . 4
 

  DECID    
    |
175 | | exmiddc 788 |
. . . 4
DECID    
 
    
     
     |
176 | 174, 175 | syl 14 |
. . 3
 

            
     |
177 | 171, 172,
173, 176 | syl3anc 1184 |
. 2
 
           
     |
178 | 138, 170,
177 | mpjaodan 753 |
1
 
               |