Proof of Theorem bcpasc
Step | Hyp | Ref
| Expression |
1 | | peano2nn0 9041 |
. . . . . 6
![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![NN0
NN0](_bbn0.gif) ![) )](rp.gif) |
2 | | elfzp12 9910 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![0 0](0.gif)
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
3 | | nn0uz 9384 |
. . . . . . 7
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![0 0](0.gif) ![) )](rp.gif) |
4 | 2, 3 | eleq2s 2235 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | 1, 4 | syl 14 |
. . . . 5
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | | 1p0e1 8860 |
. . . . . . . 8
![( (](lp.gif) ![0 0](0.gif) ![1 1](1.gif) |
7 | | bcn0 10533 |
. . . . . . . . 9
![( (](lp.gif)
![( (](lp.gif) ![0 0](0.gif) ![1 1](1.gif) ![) )](rp.gif) |
8 | | 0z 9089 |
. . . . . . . . . . 11
![ZZ ZZ](bbz.gif) |
9 | | 1z 9104 |
. . . . . . . . . . 11
![ZZ ZZ](bbz.gif) |
10 | | zsubcl 9119 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![1 1](1.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
11 | 8, 9, 10 | mp2an 423 |
. . . . . . . . . 10
![( (](lp.gif) ![1 1](1.gif) ![ZZ ZZ](bbz.gif) |
12 | | 0re 7790 |
. . . . . . . . . . . 12
![RR RR](bbr.gif) |
13 | | ltm1 8628 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![0 0](0.gif) ![) )](rp.gif) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . 11
![( (](lp.gif) ![1 1](1.gif) ![0 0](0.gif) |
15 | 14 | orci 721 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | | bcval4 10530 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
17 | 11, 15, 16 | mp3an23 1308 |
. . . . . . . . 9
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
18 | 7, 17 | oveq12d 5800 |
. . . . . . . 8
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | | bcn0 10533 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![0 0](0.gif) ![1 1](1.gif) ![) )](rp.gif) |
20 | 1, 19 | syl 14 |
. . . . . . . 8
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![0 0](0.gif) ![1 1](1.gif) ![) )](rp.gif) |
21 | 6, 18, 20 | 3eqtr4a 2199 |
. . . . . . 7
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![0 0](0.gif) ![)
)](rp.gif) ![) )](rp.gif) |
22 | | oveq2 5790 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![0 0](0.gif) ![)
)](rp.gif) ![) )](rp.gif) |
23 | | oveq1 5789 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
24 | 23 | oveq2d 5798 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
25 | 22, 24 | oveq12d 5800 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | | oveq2 5790 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 25, 26 | eqeq12d 2155 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif)
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | 21, 27 | syl5ibrcom 156 |
. . . . . 6
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | | simpr 109 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | | 0p1e1 8858 |
. . . . . . . . . 10
![( (](lp.gif) ![1 1](1.gif) ![1 1](1.gif) |
31 | 30 | oveq1i 5792 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
32 | 29, 31 | eleqtrdi 2233 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | | nn0p1nn 9040 |
. . . . . . . . . . 11
![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
34 | | nnuz 9385 |
. . . . . . . . . . 11
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![1 1](1.gif) ![) )](rp.gif) |
35 | 33, 34 | eleqtrdi 2233 |
. . . . . . . . . 10
![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![1 1](1.gif) ![) )](rp.gif) ![)
)](rp.gif) |
36 | | fzm1 9911 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 36 | biimpa 294 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![1
1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1
1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 35, 37 | sylan 281 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | | nn0cn 9011 |
. . . . . . . . . . . . . . 15
![( (](lp.gif)
![CC CC](bbc.gif) ![) )](rp.gif) |
40 | | ax-1cn 7737 |
. . . . . . . . . . . . . . 15
![CC CC](bbc.gif) |
41 | | pncan 7992 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![1 1](1.gif) ![N N](_cn.gif) ![) )](rp.gif) |
42 | 39, 40, 41 | sylancl 410 |
. . . . . . . . . . . . . 14
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![N N](_cn.gif) ![) )](rp.gif) |
43 | 42 | oveq2d 5798 |
. . . . . . . . . . . . 13
![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1
1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![)
)](rp.gif) ![) )](rp.gif) |
44 | 43 | eleq2d 2210 |
. . . . . . . . . . . 12
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![1 1](1.gif) ![) )](rp.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
45 | 44 | biimpa 294 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
46 | | 1eluzge0 9396 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![0 0](0.gif) ![) )](rp.gif) |
47 | | fzss1 9874 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![0 0](0.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![)
)](rp.gif) ![) )](rp.gif) |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![)
)](rp.gif) |
49 | 48 | sseli 3098 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![)
)](rp.gif) ![) )](rp.gif) |
50 | | bcp1n 10539 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
51 | 49, 50 | syl 14 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
52 | | bcrpcl 10531 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![K K](_ck.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
53 | 49, 52 | syl 14 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![K K](_ck.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
54 | 53 | rpcnd 9515 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![K K](_ck.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
55 | | elfzuz2 9840 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![1 1](1.gif) ![) )](rp.gif) ![)
)](rp.gif) |
56 | 55, 34 | eleqtrrdi 2234 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
57 | 56 | peano2nnd 8759 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif)
![1 1](1.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
58 | 57 | nncnd 8758 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif)
![1 1](1.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
59 | 56 | nncnd 8758 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
60 | | 1cnd 7806 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
61 | | elfzelz 9837 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
62 | 61 | zcnd 9198 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
63 | 59, 60, 62 | addsubd 8118 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
64 | | fznn0sub 9868 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif)
![K K](_ck.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
65 | | nn0p1nn 9040 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif)
![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![1 1](1.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
66 | 64, 65 | syl 14 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![1 1](1.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
67 | 63, 66 | eqeltrd 2217 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
68 | 67 | nncnd 8758 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
69 | 67 | nnap0d 8790 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) # ![0 0](0.gif) ![) )](rp.gif) |
70 | 54, 58, 68, 69 | div12apd 8611 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
71 | 67 | nnrpd 9511 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
72 | 53, 71 | rpdivcld 9531 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
73 | 72 | rpcnd 9515 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
74 | 58, 73 | mulcomd 7811 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
75 | 70, 74 | eqtrd 2173 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
76 | 58, 62 | npcand 8101 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
77 | 76 | oveq2d 5798 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
78 | 73, 68, 62 | adddid 7814 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![K K](_ck.gif) ![)
)](rp.gif) ![K K](_ck.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
79 | 75, 77, 78 | 3eqtr2d 2179 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![K K](_ck.gif) ![)
)](rp.gif) ![K K](_ck.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
80 | 54, 68, 69 | divcanap1d 8575 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
81 | | elfznn 9865 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
82 | 81 | nnap0d 8790 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) # ![0 0](0.gif) ![) )](rp.gif) |
83 | 54, 68, 62, 69, 82 | divdivap2d 8607 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![K K](_ck.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
84 | | bcm1k 10538 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
85 | 59, 62, 60 | subsub3d 8127 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
86 | 85 | oveq1d 5797 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
87 | 86 | oveq2d 5798 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
88 | 84, 87 | eqtrd 2173 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
89 | | fzelp1 9885 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
90 | 57 | nnzd 9196 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif)
![1 1](1.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
91 | | elfzm1b 9909 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![1
1](1.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
92 | 61, 90, 91 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif)
![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
93 | 89, 92 | mpbid 146 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
94 | 59, 40, 41 | sylancl 410 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![N N](_cn.gif) ![) )](rp.gif) |
95 | 94 | oveq2d 5798 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![0
0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1
1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![)
)](rp.gif) ![) )](rp.gif) |
96 | 93, 95 | eleqtrd 2219 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
97 | | bcrpcl 10531 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
98 | 96, 97 | syl 14 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
99 | 98 | rpcnd 9515 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
100 | 81 | nnrpd 9511 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
101 | 71, 100 | rpdivcld 9531 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
102 | 101 | rpcnd 9515 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
103 | 68, 62, 69, 82 | divap0d 8590 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) # ![0 0](0.gif) ![) )](rp.gif) |
104 | 54, 99, 102, 103 | divmulap3d 8609 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif)
![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
105 | 88, 104 | mpbird 166 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
106 | 54, 62, 68, 69 | div23apd 8612 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
107 | 83, 105, 106 | 3eqtr3rd 2182 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
108 | 80, 107 | oveq12d 5800 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![K K](_ck.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
109 | 51, 79, 108 | 3eqtrrd 2178 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
110 | 45, 109 | syl 14 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
111 | | oveq2 5790 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
112 | 33 | nnzd 9196 |
. . . . . . . . . . . . . 14
![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
113 | | nn0re 9010 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
114 | 113 | ltp1d 8712 |
. . . . . . . . . . . . . . 15
![( (](lp.gif)
![(
(](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
115 | 114 | olcd 724 |
. . . . . . . . . . . . . 14
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
116 | | bcval4 10530 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
117 | 112, 115,
116 | mpd3an23 1318 |
. . . . . . . . . . . . 13
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
118 | 111, 117 | sylan9eqr 2195 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![0 0](0.gif) ![) )](rp.gif) |
119 | | oveq1 5789 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
120 | 119, 42 | sylan9eqr 2195 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![1
1](1.gif) ![N N](_cn.gif) ![) )](rp.gif) |
121 | 120 | oveq2d 5798 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![)
)](rp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
122 | | bcnn 10535 |
. . . . . . . . . . . . . 14
![( (](lp.gif)
![( (](lp.gif) ![N N](_cn.gif) ![1 1](1.gif) ![) )](rp.gif) |
123 | 122 | adantr 274 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![1 1](1.gif) ![) )](rp.gif) |
124 | 121, 123 | eqtrd 2173 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![)
)](rp.gif) ![1 1](1.gif) ![) )](rp.gif) |
125 | 118, 124 | oveq12d 5800 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
126 | | oveq2 5790 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
127 | | bcnn 10535 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) |
128 | 1, 127 | syl 14 |
. . . . . . . . . . . 12
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) |
129 | 126, 128 | sylan9eqr 2195 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![1 1](1.gif) ![) )](rp.gif) |
130 | 30, 125, 129 | 3eqtr4a 2199 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
131 | 110, 130 | jaodan 787 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1
1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
132 | 38, 131 | syldan 280 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
133 | 32, 132 | syldan 280 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
134 | 133 | ex 114 |
. . . . . 6
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
135 | 28, 134 | jaod 707 |
. . . . 5
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
136 | 5, 135 | sylbid 149 |
. . . 4
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
137 | 136 | imp 123 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
138 | 137 | adantlr 469 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
139 | | 00id 7927 |
. . 3
![( (](lp.gif) ![0 0](0.gif) ![0 0](0.gif) |
140 | | fzelp1 9885 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
141 | 140 | con3i 622 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif)
![( (](lp.gif) ![0
0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
142 | | bcval3 10529 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![0 0](0.gif) ![) )](rp.gif) |
143 | 142 | 3expa 1182 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![)
)](rp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![0 0](0.gif) ![) )](rp.gif) |
144 | 141, 143 | sylan2 284 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![0 0](0.gif) ![) )](rp.gif) |
145 | | simpll 519 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
146 | | simplr 520 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
147 | | peano2zm 9116 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
148 | 146, 147 | syl 14 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![1 1](1.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
149 | 39 | adantr 274 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
150 | 149, 40, 41 | sylancl 410 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![1 1](1.gif) ![N N](_cn.gif) ![) )](rp.gif) |
151 | 150 | oveq2d 5798 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
152 | 151 | eleq2d 2210 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
153 | | id 19 |
. . . . . . . . 9
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
154 | 1 | nn0zd 9195 |
. . . . . . . . 9
![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
155 | 153, 154,
91 | syl2anr 288 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
156 | | fzp1ss 9884 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
157 | 8, 156 | ax-mp 5 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
158 | 31, 157 | eqsstrri 3135 |
. . . . . . . . 9
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
159 | 158 | sseli 3098 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
160 | 155, 159 | syl6bir 163 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
161 | 152, 160 | sylbird 169 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
162 | 161 | con3dimp 625 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
163 | | bcval3 10529 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![)
)](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
164 | 145, 148,
162, 163 | syl3anc 1217 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
165 | 144, 164 | oveq12d 5800 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
166 | 145, 1 | syl 14 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![1 1](1.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
167 | | simpr 109 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
168 | | bcval3 10529 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![0 0](0.gif) ![) )](rp.gif) |
169 | 166, 146,
167, 168 | syl3anc 1217 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![0 0](0.gif) ![) )](rp.gif) |
170 | 139, 165,
169 | 3eqtr4a 2199 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
171 | | simpr 109 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
172 | | 0zd 9090 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
173 | 112 | adantr 274 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![1 1](1.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
174 | | fzdcel 9851 |
. . . 4
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif)
![1 1](1.gif) ![ZZ ZZ](bbz.gif) DECID ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
175 | | exmiddc 822 |
. . . 4
DECID ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
176 | 174, 175 | syl 14 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif)
![1 1](1.gif) ![ZZ ZZ](bbz.gif) ![(
(](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
177 | 171, 172,
173, 176 | syl3anc 1217 |
. 2
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
178 | 138, 170,
177 | mpjaodan 788 |
1
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |