Proof of Theorem bcpasc
Step | Hyp | Ref
| Expression |
1 | | peano2nn0 8328 |
. . . . . 6
|
2 | | elfzp12 9116 |
. . . . . . 7
|
3 | | nn0uz 8653 |
. . . . . . 7
|
4 | 2, 3 | eleq2s 2173 |
. . . . . 6
|
5 | 1, 4 | syl 14 |
. . . . 5
|
6 | | 1p0e1 8154 |
. . . . . . . 8
|
7 | | bcn0 9682 |
. . . . . . . . 9
|
8 | | 0z 8362 |
. . . . . . . . . . 11
|
9 | | 1z 8377 |
. . . . . . . . . . 11
|
10 | | zsubcl 8392 |
. . . . . . . . . . 11
|
11 | 8, 9, 10 | mp2an 416 |
. . . . . . . . . 10
|
12 | | 0re 7119 |
. . . . . . . . . . . 12
|
13 | | ltm1 7924 |
. . . . . . . . . . . 12
|
14 | 12, 13 | ax-mp 7 |
. . . . . . . . . . 11
|
15 | 14 | orci 682 |
. . . . . . . . . 10
|
16 | | bcval4 9679 |
. . . . . . . . . 10
|
17 | 11, 15, 16 | mp3an23 1260 |
. . . . . . . . 9
|
18 | 7, 17 | oveq12d 5550 |
. . . . . . . 8
|
19 | | bcn0 9682 |
. . . . . . . . 9
|
20 | 1, 19 | syl 14 |
. . . . . . . 8
|
21 | 6, 18, 20 | 3eqtr4a 2139 |
. . . . . . 7
|
22 | | oveq2 5540 |
. . . . . . . . 9
|
23 | | oveq1 5539 |
. . . . . . . . . 10
|
24 | 23 | oveq2d 5548 |
. . . . . . . . 9
|
25 | 22, 24 | oveq12d 5550 |
. . . . . . . 8
|
26 | | oveq2 5540 |
. . . . . . . 8
|
27 | 25, 26 | eqeq12d 2095 |
. . . . . . 7
|
28 | 21, 27 | syl5ibrcom 155 |
. . . . . 6
|
29 | | simpr 108 |
. . . . . . . . 9
|
30 | | 0p1e1 8153 |
. . . . . . . . . 10
|
31 | 30 | oveq1i 5542 |
. . . . . . . . 9
|
32 | 29, 31 | syl6eleq 2171 |
. . . . . . . 8
|
33 | | nn0p1nn 8327 |
. . . . . . . . . . 11
|
34 | | nnuz 8654 |
. . . . . . . . . . 11
|
35 | 33, 34 | syl6eleq 2171 |
. . . . . . . . . 10
|
36 | | fzm1 9117 |
. . . . . . . . . . 11
|
37 | 36 | biimpa 290 |
. . . . . . . . . 10
|
38 | 35, 37 | sylan 277 |
. . . . . . . . 9
|
39 | | nn0cn 8298 |
. . . . . . . . . . . . . . 15
|
40 | | ax-1cn 7069 |
. . . . . . . . . . . . . . 15
|
41 | | pncan 7314 |
. . . . . . . . . . . . . . 15
|
42 | 39, 40, 41 | sylancl 404 |
. . . . . . . . . . . . . 14
|
43 | 42 | oveq2d 5548 |
. . . . . . . . . . . . 13
|
44 | 43 | eleq2d 2148 |
. . . . . . . . . . . 12
|
45 | 44 | biimpa 290 |
. . . . . . . . . . 11
|
46 | | 1eluzge0 8662 |
. . . . . . . . . . . . . . 15
|
47 | | fzss1 9081 |
. . . . . . . . . . . . . . 15
|
48 | 46, 47 | ax-mp 7 |
. . . . . . . . . . . . . 14
|
49 | 48 | sseli 2995 |
. . . . . . . . . . . . 13
|
50 | | bcp1n 9688 |
. . . . . . . . . . . . 13
|
51 | 49, 50 | syl 14 |
. . . . . . . . . . . 12
|
52 | | bcrpcl 9680 |
. . . . . . . . . . . . . . . . 17
|
53 | 49, 52 | syl 14 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | rpcnd 8775 |
. . . . . . . . . . . . . . 15
|
55 | | elfzuz2 9048 |
. . . . . . . . . . . . . . . . . 18
|
56 | 55, 34 | syl6eleqr 2172 |
. . . . . . . . . . . . . . . . 17
|
57 | 56 | peano2nnd 8054 |
. . . . . . . . . . . . . . . 16
|
58 | 57 | nncnd 8053 |
. . . . . . . . . . . . . . 15
|
59 | 56 | nncnd 8053 |
. . . . . . . . . . . . . . . . . 18
|
60 | | 1cnd 7135 |
. . . . . . . . . . . . . . . . . 18
|
61 | | elfzelz 9045 |
. . . . . . . . . . . . . . . . . . 19
|
62 | 61 | zcnd 8470 |
. . . . . . . . . . . . . . . . . 18
|
63 | 59, 60, 62 | addsubd 7440 |
. . . . . . . . . . . . . . . . 17
|
64 | | fznn0sub 9075 |
. . . . . . . . . . . . . . . . . 18
|
65 | | nn0p1nn 8327 |
. . . . . . . . . . . . . . . . . 18
|
66 | 64, 65 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
67 | 63, 66 | eqeltrd 2155 |
. . . . . . . . . . . . . . . 16
|
68 | 67 | nncnd 8053 |
. . . . . . . . . . . . . . 15
|
69 | 67 | nnap0d 8084 |
. . . . . . . . . . . . . . 15
# |
70 | 54, 58, 68, 69 | div12apd 7913 |
. . . . . . . . . . . . . 14
|
71 | 67 | nnrpd 8772 |
. . . . . . . . . . . . . . . . 17
|
72 | 53, 71 | rpdivcld 8791 |
. . . . . . . . . . . . . . . 16
|
73 | 72 | rpcnd 8775 |
. . . . . . . . . . . . . . 15
|
74 | 58, 73 | mulcomd 7140 |
. . . . . . . . . . . . . 14
|
75 | 70, 74 | eqtrd 2113 |
. . . . . . . . . . . . 13
|
76 | 58, 62 | npcand 7423 |
. . . . . . . . . . . . . 14
|
77 | 76 | oveq2d 5548 |
. . . . . . . . . . . . 13
|
78 | 73, 68, 62 | adddid 7143 |
. . . . . . . . . . . . 13
|
79 | 75, 77, 78 | 3eqtr2d 2119 |
. . . . . . . . . . . 12
|
80 | 54, 68, 69 | divcanap1d 7878 |
. . . . . . . . . . . . 13
|
81 | | elfznn 9073 |
. . . . . . . . . . . . . . . 16
|
82 | 81 | nnap0d 8084 |
. . . . . . . . . . . . . . 15
# |
83 | 54, 68, 62, 69, 82 | divdivap2d 7909 |
. . . . . . . . . . . . . 14
|
84 | | bcm1k 9687 |
. . . . . . . . . . . . . . . 16
|
85 | 59, 62, 60 | subsub3d 7449 |
. . . . . . . . . . . . . . . . . 18
|
86 | 85 | oveq1d 5547 |
. . . . . . . . . . . . . . . . 17
|
87 | 86 | oveq2d 5548 |
. . . . . . . . . . . . . . . 16
|
88 | 84, 87 | eqtrd 2113 |
. . . . . . . . . . . . . . 15
|
89 | | fzelp1 9091 |
. . . . . . . . . . . . . . . . . . . 20
|
90 | 57 | nnzd 8468 |
. . . . . . . . . . . . . . . . . . . . 21
|
91 | | elfzm1b 9115 |
. . . . . . . . . . . . . . . . . . . . 21
|
92 | 61, 90, 91 | syl2anc 403 |
. . . . . . . . . . . . . . . . . . . 20
|
93 | 89, 92 | mpbid 145 |
. . . . . . . . . . . . . . . . . . 19
|
94 | 59, 40, 41 | sylancl 404 |
. . . . . . . . . . . . . . . . . . . 20
|
95 | 94 | oveq2d 5548 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 93, 95 | eleqtrd 2157 |
. . . . . . . . . . . . . . . . . 18
|
97 | | bcrpcl 9680 |
. . . . . . . . . . . . . . . . . 18
|
98 | 96, 97 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
99 | 98 | rpcnd 8775 |
. . . . . . . . . . . . . . . 16
|
100 | 81 | nnrpd 8772 |
. . . . . . . . . . . . . . . . . 18
|
101 | 71, 100 | rpdivcld 8791 |
. . . . . . . . . . . . . . . . 17
|
102 | 101 | rpcnd 8775 |
. . . . . . . . . . . . . . . 16
|
103 | 68, 62, 69, 82 | divap0d 7893 |
. . . . . . . . . . . . . . . 16
# |
104 | 54, 99, 102, 103 | divmulap3d 7911 |
. . . . . . . . . . . . . . 15
|
105 | 88, 104 | mpbird 165 |
. . . . . . . . . . . . . 14
|
106 | 54, 62, 68, 69 | div23apd 7914 |
. . . . . . . . . . . . . 14
|
107 | 83, 105, 106 | 3eqtr3rd 2122 |
. . . . . . . . . . . . 13
|
108 | 80, 107 | oveq12d 5550 |
. . . . . . . . . . . 12
|
109 | 51, 79, 108 | 3eqtrrd 2118 |
. . . . . . . . . . 11
|
110 | 45, 109 | syl 14 |
. . . . . . . . . 10
|
111 | | oveq2 5540 |
. . . . . . . . . . . . 13
|
112 | 33 | nnzd 8468 |
. . . . . . . . . . . . . 14
|
113 | | nn0re 8297 |
. . . . . . . . . . . . . . . 16
|
114 | 113 | ltp1d 8008 |
. . . . . . . . . . . . . . 15
|
115 | 114 | olcd 685 |
. . . . . . . . . . . . . 14
|
116 | | bcval4 9679 |
. . . . . . . . . . . . . 14
|
117 | 112, 115,
116 | mpd3an23 1270 |
. . . . . . . . . . . . 13
|
118 | 111, 117 | sylan9eqr 2135 |
. . . . . . . . . . . 12
|
119 | | oveq1 5539 |
. . . . . . . . . . . . . . 15
|
120 | 119, 42 | sylan9eqr 2135 |
. . . . . . . . . . . . . 14
|
121 | 120 | oveq2d 5548 |
. . . . . . . . . . . . 13
|
122 | | bcnn 9684 |
. . . . . . . . . . . . . 14
|
123 | 122 | adantr 270 |
. . . . . . . . . . . . 13
|
124 | 121, 123 | eqtrd 2113 |
. . . . . . . . . . . 12
|
125 | 118, 124 | oveq12d 5550 |
. . . . . . . . . . 11
|
126 | | oveq2 5540 |
. . . . . . . . . . . 12
|
127 | | bcnn 9684 |
. . . . . . . . . . . . 13
|
128 | 1, 127 | syl 14 |
. . . . . . . . . . . 12
|
129 | 126, 128 | sylan9eqr 2135 |
. . . . . . . . . . 11
|
130 | 30, 125, 129 | 3eqtr4a 2139 |
. . . . . . . . . 10
|
131 | 110, 130 | jaodan 743 |
. . . . . . . . 9
|
132 | 38, 131 | syldan 276 |
. . . . . . . 8
|
133 | 32, 132 | syldan 276 |
. . . . . . 7
|
134 | 133 | ex 113 |
. . . . . 6
|
135 | 28, 134 | jaod 669 |
. . . . 5
|
136 | 5, 135 | sylbid 148 |
. . . 4
|
137 | 136 | imp 122 |
. . 3
|
138 | 137 | adantlr 460 |
. 2
|
139 | | 00id 7249 |
. . 3
|
140 | | fzelp1 9091 |
. . . . . 6
|
141 | 140 | con3i 594 |
. . . . 5
|
142 | | bcval3 9678 |
. . . . . 6
|
143 | 142 | 3expa 1138 |
. . . . 5
|
144 | 141, 143 | sylan2 280 |
. . . 4
|
145 | | simpll 495 |
. . . . 5
|
146 | | simplr 496 |
. . . . . 6
|
147 | | peano2zm 8389 |
. . . . . 6
|
148 | 146, 147 | syl 14 |
. . . . 5
|
149 | 39 | adantr 270 |
. . . . . . . . . 10
|
150 | 149, 40, 41 | sylancl 404 |
. . . . . . . . 9
|
151 | 150 | oveq2d 5548 |
. . . . . . . 8
|
152 | 151 | eleq2d 2148 |
. . . . . . 7
|
153 | | id 19 |
. . . . . . . . 9
|
154 | 1 | nn0zd 8467 |
. . . . . . . . 9
|
155 | 153, 154,
91 | syl2anr 284 |
. . . . . . . 8
|
156 | | fzp1ss 9090 |
. . . . . . . . . . 11
|
157 | 8, 156 | ax-mp 7 |
. . . . . . . . . 10
|
158 | 31, 157 | eqsstr3i 3030 |
. . . . . . . . 9
|
159 | 158 | sseli 2995 |
. . . . . . . 8
|
160 | 155, 159 | syl6bir 162 |
. . . . . . 7
|
161 | 152, 160 | sylbird 168 |
. . . . . 6
|
162 | 161 | con3dimp 596 |
. . . . 5
|
163 | | bcval3 9678 |
. . . . 5
|
164 | 145, 148,
162, 163 | syl3anc 1169 |
. . . 4
|
165 | 144, 164 | oveq12d 5550 |
. . 3
|
166 | 145, 1 | syl 14 |
. . . 4
|
167 | | simpr 108 |
. . . 4
|
168 | | bcval3 9678 |
. . . 4
|
169 | 166, 146,
167, 168 | syl3anc 1169 |
. . 3
|
170 | 139, 165,
169 | 3eqtr4a 2139 |
. 2
|
171 | | simpr 108 |
. . 3
|
172 | | 0zd 8363 |
. . 3
|
173 | 112 | adantr 270 |
. . 3
|
174 | | fzdcel 9059 |
. . . 4
DECID
|
175 | | exmiddc 777 |
. . . 4
DECID
|
176 | 174, 175 | syl 14 |
. . 3
|
177 | 171, 172,
173, 176 | syl3anc 1169 |
. 2
|
178 | 138, 170,
177 | mpjaodan 744 |
1
|