Proof of Theorem bcpasc
Step | Hyp | Ref
| Expression |
1 | | peano2nn0 9010 |
. . . . . 6
|
2 | | elfzp12 9872 |
. . . . . . 7
|
3 | | nn0uz 9353 |
. . . . . . 7
|
4 | 2, 3 | eleq2s 2232 |
. . . . . 6
|
5 | 1, 4 | syl 14 |
. . . . 5
|
6 | | 1p0e1 8829 |
. . . . . . . 8
|
7 | | bcn0 10494 |
. . . . . . . . 9
|
8 | | 0z 9058 |
. . . . . . . . . . 11
|
9 | | 1z 9073 |
. . . . . . . . . . 11
|
10 | | zsubcl 9088 |
. . . . . . . . . . 11
|
11 | 8, 9, 10 | mp2an 422 |
. . . . . . . . . 10
|
12 | | 0re 7759 |
. . . . . . . . . . . 12
|
13 | | ltm1 8597 |
. . . . . . . . . . . 12
|
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . 11
|
15 | 14 | orci 720 |
. . . . . . . . . 10
|
16 | | bcval4 10491 |
. . . . . . . . . 10
|
17 | 11, 15, 16 | mp3an23 1307 |
. . . . . . . . 9
|
18 | 7, 17 | oveq12d 5785 |
. . . . . . . 8
|
19 | | bcn0 10494 |
. . . . . . . . 9
|
20 | 1, 19 | syl 14 |
. . . . . . . 8
|
21 | 6, 18, 20 | 3eqtr4a 2196 |
. . . . . . 7
|
22 | | oveq2 5775 |
. . . . . . . . 9
|
23 | | oveq1 5774 |
. . . . . . . . . 10
|
24 | 23 | oveq2d 5783 |
. . . . . . . . 9
|
25 | 22, 24 | oveq12d 5785 |
. . . . . . . 8
|
26 | | oveq2 5775 |
. . . . . . . 8
|
27 | 25, 26 | eqeq12d 2152 |
. . . . . . 7
|
28 | 21, 27 | syl5ibrcom 156 |
. . . . . 6
|
29 | | simpr 109 |
. . . . . . . . 9
|
30 | | 0p1e1 8827 |
. . . . . . . . . 10
|
31 | 30 | oveq1i 5777 |
. . . . . . . . 9
|
32 | 29, 31 | eleqtrdi 2230 |
. . . . . . . 8
|
33 | | nn0p1nn 9009 |
. . . . . . . . . . 11
|
34 | | nnuz 9354 |
. . . . . . . . . . 11
|
35 | 33, 34 | eleqtrdi 2230 |
. . . . . . . . . 10
|
36 | | fzm1 9873 |
. . . . . . . . . . 11
|
37 | 36 | biimpa 294 |
. . . . . . . . . 10
|
38 | 35, 37 | sylan 281 |
. . . . . . . . 9
|
39 | | nn0cn 8980 |
. . . . . . . . . . . . . . 15
|
40 | | ax-1cn 7706 |
. . . . . . . . . . . . . . 15
|
41 | | pncan 7961 |
. . . . . . . . . . . . . . 15
|
42 | 39, 40, 41 | sylancl 409 |
. . . . . . . . . . . . . 14
|
43 | 42 | oveq2d 5783 |
. . . . . . . . . . . . 13
|
44 | 43 | eleq2d 2207 |
. . . . . . . . . . . 12
|
45 | 44 | biimpa 294 |
. . . . . . . . . . 11
|
46 | | 1eluzge0 9362 |
. . . . . . . . . . . . . . 15
|
47 | | fzss1 9836 |
. . . . . . . . . . . . . . 15
|
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
49 | 48 | sseli 3088 |
. . . . . . . . . . . . 13
|
50 | | bcp1n 10500 |
. . . . . . . . . . . . 13
|
51 | 49, 50 | syl 14 |
. . . . . . . . . . . 12
|
52 | | bcrpcl 10492 |
. . . . . . . . . . . . . . . . 17
|
53 | 49, 52 | syl 14 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | rpcnd 9478 |
. . . . . . . . . . . . . . 15
|
55 | | elfzuz2 9802 |
. . . . . . . . . . . . . . . . . 18
|
56 | 55, 34 | eleqtrrdi 2231 |
. . . . . . . . . . . . . . . . 17
|
57 | 56 | peano2nnd 8728 |
. . . . . . . . . . . . . . . 16
|
58 | 57 | nncnd 8727 |
. . . . . . . . . . . . . . 15
|
59 | 56 | nncnd 8727 |
. . . . . . . . . . . . . . . . . 18
|
60 | | 1cnd 7775 |
. . . . . . . . . . . . . . . . . 18
|
61 | | elfzelz 9799 |
. . . . . . . . . . . . . . . . . . 19
|
62 | 61 | zcnd 9167 |
. . . . . . . . . . . . . . . . . 18
|
63 | 59, 60, 62 | addsubd 8087 |
. . . . . . . . . . . . . . . . 17
|
64 | | fznn0sub 9830 |
. . . . . . . . . . . . . . . . . 18
|
65 | | nn0p1nn 9009 |
. . . . . . . . . . . . . . . . . 18
|
66 | 64, 65 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
67 | 63, 66 | eqeltrd 2214 |
. . . . . . . . . . . . . . . 16
|
68 | 67 | nncnd 8727 |
. . . . . . . . . . . . . . 15
|
69 | 67 | nnap0d 8759 |
. . . . . . . . . . . . . . 15
# |
70 | 54, 58, 68, 69 | div12apd 8580 |
. . . . . . . . . . . . . 14
|
71 | 67 | nnrpd 9475 |
. . . . . . . . . . . . . . . . 17
|
72 | 53, 71 | rpdivcld 9494 |
. . . . . . . . . . . . . . . 16
|
73 | 72 | rpcnd 9478 |
. . . . . . . . . . . . . . 15
|
74 | 58, 73 | mulcomd 7780 |
. . . . . . . . . . . . . 14
|
75 | 70, 74 | eqtrd 2170 |
. . . . . . . . . . . . 13
|
76 | 58, 62 | npcand 8070 |
. . . . . . . . . . . . . 14
|
77 | 76 | oveq2d 5783 |
. . . . . . . . . . . . 13
|
78 | 73, 68, 62 | adddid 7783 |
. . . . . . . . . . . . 13
|
79 | 75, 77, 78 | 3eqtr2d 2176 |
. . . . . . . . . . . 12
|
80 | 54, 68, 69 | divcanap1d 8544 |
. . . . . . . . . . . . 13
|
81 | | elfznn 9827 |
. . . . . . . . . . . . . . . 16
|
82 | 81 | nnap0d 8759 |
. . . . . . . . . . . . . . 15
# |
83 | 54, 68, 62, 69, 82 | divdivap2d 8576 |
. . . . . . . . . . . . . 14
|
84 | | bcm1k 10499 |
. . . . . . . . . . . . . . . 16
|
85 | 59, 62, 60 | subsub3d 8096 |
. . . . . . . . . . . . . . . . . 18
|
86 | 85 | oveq1d 5782 |
. . . . . . . . . . . . . . . . 17
|
87 | 86 | oveq2d 5783 |
. . . . . . . . . . . . . . . 16
|
88 | 84, 87 | eqtrd 2170 |
. . . . . . . . . . . . . . 15
|
89 | | fzelp1 9847 |
. . . . . . . . . . . . . . . . . . . 20
|
90 | 57 | nnzd 9165 |
. . . . . . . . . . . . . . . . . . . . 21
|
91 | | elfzm1b 9871 |
. . . . . . . . . . . . . . . . . . . . 21
|
92 | 61, 90, 91 | syl2anc 408 |
. . . . . . . . . . . . . . . . . . . 20
|
93 | 89, 92 | mpbid 146 |
. . . . . . . . . . . . . . . . . . 19
|
94 | 59, 40, 41 | sylancl 409 |
. . . . . . . . . . . . . . . . . . . 20
|
95 | 94 | oveq2d 5783 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 93, 95 | eleqtrd 2216 |
. . . . . . . . . . . . . . . . . 18
|
97 | | bcrpcl 10492 |
. . . . . . . . . . . . . . . . . 18
|
98 | 96, 97 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
99 | 98 | rpcnd 9478 |
. . . . . . . . . . . . . . . 16
|
100 | 81 | nnrpd 9475 |
. . . . . . . . . . . . . . . . . 18
|
101 | 71, 100 | rpdivcld 9494 |
. . . . . . . . . . . . . . . . 17
|
102 | 101 | rpcnd 9478 |
. . . . . . . . . . . . . . . 16
|
103 | 68, 62, 69, 82 | divap0d 8559 |
. . . . . . . . . . . . . . . 16
# |
104 | 54, 99, 102, 103 | divmulap3d 8578 |
. . . . . . . . . . . . . . 15
|
105 | 88, 104 | mpbird 166 |
. . . . . . . . . . . . . 14
|
106 | 54, 62, 68, 69 | div23apd 8581 |
. . . . . . . . . . . . . 14
|
107 | 83, 105, 106 | 3eqtr3rd 2179 |
. . . . . . . . . . . . 13
|
108 | 80, 107 | oveq12d 5785 |
. . . . . . . . . . . 12
|
109 | 51, 79, 108 | 3eqtrrd 2175 |
. . . . . . . . . . 11
|
110 | 45, 109 | syl 14 |
. . . . . . . . . 10
|
111 | | oveq2 5775 |
. . . . . . . . . . . . 13
|
112 | 33 | nnzd 9165 |
. . . . . . . . . . . . . 14
|
113 | | nn0re 8979 |
. . . . . . . . . . . . . . . 16
|
114 | 113 | ltp1d 8681 |
. . . . . . . . . . . . . . 15
|
115 | 114 | olcd 723 |
. . . . . . . . . . . . . 14
|
116 | | bcval4 10491 |
. . . . . . . . . . . . . 14
|
117 | 112, 115,
116 | mpd3an23 1317 |
. . . . . . . . . . . . 13
|
118 | 111, 117 | sylan9eqr 2192 |
. . . . . . . . . . . 12
|
119 | | oveq1 5774 |
. . . . . . . . . . . . . . 15
|
120 | 119, 42 | sylan9eqr 2192 |
. . . . . . . . . . . . . 14
|
121 | 120 | oveq2d 5783 |
. . . . . . . . . . . . 13
|
122 | | bcnn 10496 |
. . . . . . . . . . . . . 14
|
123 | 122 | adantr 274 |
. . . . . . . . . . . . 13
|
124 | 121, 123 | eqtrd 2170 |
. . . . . . . . . . . 12
|
125 | 118, 124 | oveq12d 5785 |
. . . . . . . . . . 11
|
126 | | oveq2 5775 |
. . . . . . . . . . . 12
|
127 | | bcnn 10496 |
. . . . . . . . . . . . 13
|
128 | 1, 127 | syl 14 |
. . . . . . . . . . . 12
|
129 | 126, 128 | sylan9eqr 2192 |
. . . . . . . . . . 11
|
130 | 30, 125, 129 | 3eqtr4a 2196 |
. . . . . . . . . 10
|
131 | 110, 130 | jaodan 786 |
. . . . . . . . 9
|
132 | 38, 131 | syldan 280 |
. . . . . . . 8
|
133 | 32, 132 | syldan 280 |
. . . . . . 7
|
134 | 133 | ex 114 |
. . . . . 6
|
135 | 28, 134 | jaod 706 |
. . . . 5
|
136 | 5, 135 | sylbid 149 |
. . . 4
|
137 | 136 | imp 123 |
. . 3
|
138 | 137 | adantlr 468 |
. 2
|
139 | | 00id 7896 |
. . 3
|
140 | | fzelp1 9847 |
. . . . . 6
|
141 | 140 | con3i 621 |
. . . . 5
|
142 | | bcval3 10490 |
. . . . . 6
|
143 | 142 | 3expa 1181 |
. . . . 5
|
144 | 141, 143 | sylan2 284 |
. . . 4
|
145 | | simpll 518 |
. . . . 5
|
146 | | simplr 519 |
. . . . . 6
|
147 | | peano2zm 9085 |
. . . . . 6
|
148 | 146, 147 | syl 14 |
. . . . 5
|
149 | 39 | adantr 274 |
. . . . . . . . . 10
|
150 | 149, 40, 41 | sylancl 409 |
. . . . . . . . 9
|
151 | 150 | oveq2d 5783 |
. . . . . . . 8
|
152 | 151 | eleq2d 2207 |
. . . . . . 7
|
153 | | id 19 |
. . . . . . . . 9
|
154 | 1 | nn0zd 9164 |
. . . . . . . . 9
|
155 | 153, 154,
91 | syl2anr 288 |
. . . . . . . 8
|
156 | | fzp1ss 9846 |
. . . . . . . . . . 11
|
157 | 8, 156 | ax-mp 5 |
. . . . . . . . . 10
|
158 | 31, 157 | eqsstrri 3125 |
. . . . . . . . 9
|
159 | 158 | sseli 3088 |
. . . . . . . 8
|
160 | 155, 159 | syl6bir 163 |
. . . . . . 7
|
161 | 152, 160 | sylbird 169 |
. . . . . 6
|
162 | 161 | con3dimp 624 |
. . . . 5
|
163 | | bcval3 10490 |
. . . . 5
|
164 | 145, 148,
162, 163 | syl3anc 1216 |
. . . 4
|
165 | 144, 164 | oveq12d 5785 |
. . 3
|
166 | 145, 1 | syl 14 |
. . . 4
|
167 | | simpr 109 |
. . . 4
|
168 | | bcval3 10490 |
. . . 4
|
169 | 166, 146,
167, 168 | syl3anc 1216 |
. . 3
|
170 | 139, 165,
169 | 3eqtr4a 2196 |
. 2
|
171 | | simpr 109 |
. . 3
|
172 | | 0zd 9059 |
. . 3
|
173 | 112 | adantr 274 |
. . 3
|
174 | | fzdcel 9813 |
. . . 4
DECID
|
175 | | exmiddc 821 |
. . . 4
DECID
|
176 | 174, 175 | syl 14 |
. . 3
|
177 | 171, 172,
173, 176 | syl3anc 1216 |
. 2
|
178 | 138, 170,
177 | mpjaodan 787 |
1
|