Step | Hyp | Ref
| Expression |
1 | | prmind.5 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![et et](_eta.gif) ![) )](rp.gif) ![) )](rp.gif) |
2 | | oveq2 5790 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![n n](_n.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) |
3 | 2 | raleqdv 2635 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![n n](_n.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![1 1](1.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
4 | | oveq2 5790 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![n n](_n.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![)
)](rp.gif) ![) )](rp.gif) |
5 | 4 | raleqdv 2635 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![n n](_n.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | | oveq2 5790 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![n n](_n.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | 6 | raleqdv 2635 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![n n](_n.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | | oveq2 5790 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![n n](_n.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
9 | 8 | raleqdv 2635 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![n n](_n.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![A A](_ca.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
10 | | prmind.6 |
. . . . 5
![ps ps](_psi.gif) |
11 | | elfz1eq 9846 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) |
12 | | prmind.1 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | 11, 12 | syl 14 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![1 1](1.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
14 | 10, 13 | mpbiri 167 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![1 1](1.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
15 | 14 | rgen 2488 |
. . 3
![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![1 1](1.gif) ![)
)](rp.gif) ![ph ph](_varphi.gif) |
16 | | peano2nn 8756 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
17 | 16 | ad2antrr 480 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
18 | 17 | nncnd 8758 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
19 | | elfzuz 9833 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![) )](rp.gif) ![)
)](rp.gif) |
20 | 19 | ad2antrl 482 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | | eluz2nn 9388 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif)
![NN NN](bbn.gif) ![) )](rp.gif) |
22 | 20, 21 | syl 14 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![NN NN](bbn.gif) ![) )](rp.gif) |
23 | 22 | nncnd 8758 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![CC CC](bbc.gif) ![) )](rp.gif) |
24 | 22 | nnap0d 8790 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) # ![0 0](0.gif) ![) )](rp.gif) |
25 | 18, 23, 24 | divcanap2d 8576 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![)
)](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | | simprr 522 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 22 | nnzd 9196 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
28 | 22 | nnne0d 8789 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![0 0](0.gif) ![)
)](rp.gif) |
29 | 17 | nnzd 9196 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
30 | | dvdsval2 11532 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![ZZ ZZ](bbz.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | 27, 28, 29, 30 | syl3anc 1217 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![) )](rp.gif) |
32 | 26, 31 | mpbid 146 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![y
y](_y.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
33 | 23 | mulid2d 7808 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![y y](_y.gif) ![y y](_y.gif) ![) )](rp.gif) |
34 | | elfzle2 9839 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | 34 | ad2antrl 482 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
36 | | nncn 8752 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
37 | 36 | ad2antrr 480 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![CC CC](bbc.gif) ![) )](rp.gif) |
38 | | ax-1cn 7737 |
. . . . . . . . . . . . . . . . 17
![CC CC](bbc.gif) |
39 | | pncan 7992 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![k k](_k.gif) ![) )](rp.gif) |
40 | 37, 38, 39 | sylancl 410 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![1
1](1.gif) ![k k](_k.gif) ![) )](rp.gif) |
41 | 35, 40 | breqtrd 3962 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![k k](_k.gif) ![)
)](rp.gif) |
42 | | nnz 9097 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
43 | 42 | ad2antrr 480 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
44 | | zleltp1 9133 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
45 | 27, 43, 44 | syl2anc 409 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
46 | 41, 45 | mpbid 146 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
47 | 33, 46 | eqbrtrd 3958 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![y y](_y.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
48 | | 1red 7805 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![RR RR](bbr.gif) ![) )](rp.gif) |
49 | 17 | nnred 8757 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
50 | 22 | nnred 8757 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![RR RR](bbr.gif) ![) )](rp.gif) |
51 | 22 | nngt0d 8788 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![y y](_y.gif) ![)
)](rp.gif) |
52 | | ltmuldiv 8656 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | 48, 49, 50, 51, 52 | syl112anc 1221 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![y y](_y.gif) ![(
(](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
54 | 47, 53 | mpbid 146 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
55 | | eluz2b1 9422 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
56 | 32, 54, 55 | sylanbrc 414 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
57 | | prmind.2 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |
58 | | simplr 520 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![) )](rp.gif) |
59 | | fznn 9900 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif)
![( (](lp.gif) ![k
k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
60 | 43, 59 | syl 14 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![( (](lp.gif) ![k
k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
61 | 22, 41, 60 | mpbir2and 929 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) |
62 | 57, 58, 61 | rspcdva 2798 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![ch ch](_chi.gif) ![) )](rp.gif) |
63 | | vex 2692 |
. . . . . . . . . . . . . . 15
![_V
_V](rmcv.gif) |
64 | | prmind.3 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) |
65 | 63, 64 | sbcie 2947 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif)
![th th](_theta.gif) ![) )](rp.gif) |
66 | | dfsbcq 2915 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif)
![x x](_x.gif) ![]. ].](_drbrack.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
67 | 65, 66 | bitr3id 193 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![[.
[.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
68 | 64 | cbvralv 2657 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![th th](_theta.gif) ![) )](rp.gif) |
69 | 58, 68 | sylib 121 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![th th](_theta.gif) ![) )](rp.gif) |
70 | 17 | nnrpd 9511 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
71 | 22 | nnrpd 9511 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
72 | 70, 71 | rpdivcld 9531 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![y
y](_y.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
73 | 72 | rpgt0d 9516 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
74 | | elnnz 9088 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
75 | 32, 73, 74 | sylanbrc 414 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![y
y](_y.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
76 | 17 | nnap0d 8790 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) # ![0 0](0.gif) ![) )](rp.gif) |
77 | 18, 76 | dividapd 8570 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![(
(](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) |
78 | | eluz2gt1 9423 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif)
![y y](_y.gif) ![) )](rp.gif) |
79 | 20, 78 | syl 14 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![y y](_y.gif) ![)
)](rp.gif) |
80 | 77, 79 | eqbrtrd 3958 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![(
(](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![y y](_y.gif) ![)
)](rp.gif) |
81 | 17 | nngt0d 8788 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
82 | | ltdiv23 8674 |
. . . . . . . . . . . . . . . . 17
![( (](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) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![(
(](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
83 | 49, 49, 81, 50, 51, 82 | syl122anc 1226 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
84 | 80, 83 | mpbid 146 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
85 | | zleltp1 9133 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
86 | 32, 43, 85 | syl2anc 409 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
87 | 84, 86 | mpbird 166 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![y
y](_y.gif) ![k k](_k.gif) ![)
)](rp.gif) |
88 | | fznn 9900 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
89 | 43, 88 | syl 14 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![k
k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
90 | 75, 87, 89 | mpbir2and 929 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) |
91 | 67, 69, 90 | rspcdva 2798 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
92 | 62, 91 | jca 304 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
93 | 67 | anbi2d 460 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![(
(](lp.gif) ![th th](_theta.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
94 | | oveq2 5790 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
95 | 94 | sbceq1d 2918 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![z z](_z.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![) )](rp.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
96 | 93, 95 | imbi12d 233 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![th th](_theta.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![z z](_z.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif)
![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![) )](rp.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
97 | 96 | imbi2d 229 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif) ![(
(](lp.gif) ![( (](lp.gif) ![th th](_theta.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![z z](_z.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif) ![(
(](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![) )](rp.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
98 | | prmind2.8 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2
2](2.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![ta ta](_tau.gif) ![) )](rp.gif) ![) )](rp.gif) |
99 | 98 | ancoms 266 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2
2](2.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![ta ta](_tau.gif) ![) )](rp.gif) ![) )](rp.gif) |
100 | | eluzelz 9359 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
101 | 100 | adantl 275 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2
2](2.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![) )](rp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
102 | | eluzelz 9359 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
103 | 102 | adantr 274 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2
2](2.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![) )](rp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
104 | 101, 103 | zmulcld 9203 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2
2](2.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![) )](rp.gif)
![( (](lp.gif) ![z z](_z.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
105 | | prmind.4 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![ta ta](_tau.gif) ![) )](rp.gif) ![) )](rp.gif) |
106 | 105 | sbcieg 2945 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![z z](_z.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ta ta](_tau.gif) ![) )](rp.gif) ![) )](rp.gif) |
107 | 104, 106 | syl 14 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2
2](2.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![) )](rp.gif)
![( (](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![z z](_z.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ta ta](_tau.gif) ![) )](rp.gif) ![) )](rp.gif) |
108 | 99, 107 | sylibrd 168 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2
2](2.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![z z](_z.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
109 | 108 | ex 114 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif)
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![z z](_z.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
110 | 97, 109 | vtoclga 2755 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif)
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y
y](_y.gif) ![) )](rp.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
111 | 56, 20, 92, 110 | syl3c 63 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![y y](_y.gif) ![)
)](rp.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
112 | 25, 111 | sbceq1dd 2919 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.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) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
113 | 112 | rexlimdvaa 2553 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![2 2](2.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) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
114 | | ralnex 2427 |
. . . . . . . . 9
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![2 2](2.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1
1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![2 2](2.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) ![) )](rp.gif) ![) )](rp.gif) |
115 | | simpl 108 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
116 | | elnnuz 9386 |
. . . . . . . . . . . . . 14
![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![1 1](1.gif) ![) )](rp.gif) ![)
)](rp.gif) |
117 | 115, 116 | sylib 121 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
118 | | eluzp1p1 9375 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![1 1](1.gif)
![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
119 | 117, 118 | syl 14 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
120 | | df-2 8803 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) |
121 | 120 | fveq2i 5432 |
. . . . . . . . . . . 12
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2
2](2.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
122 | 119, 121 | eleqtrrdi 2234 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
123 | | isprm3 11835 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![2 2](2.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) |
124 | 123 | baibr 906 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![2 2](2.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![Prime
Prime](bbp.gif) ![) )](rp.gif) ![) )](rp.gif) |
125 | 122, 124 | syl 14 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![2 2](2.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) ![1 1](1.gif) ![Prime Prime](bbp.gif) ![) )](rp.gif) ![) )](rp.gif) |
126 | | simpr 109 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![) )](rp.gif) |
127 | 57 | cbvralv 2657 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) |
128 | 126, 127 | sylib 121 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) |
129 | 115 | nncnd 8758 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
130 | 129, 38, 39 | sylancl 410 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1
1](1.gif) ![k k](_k.gif) ![) )](rp.gif) |
131 | 130 | oveq2d 5798 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.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) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) |
132 | 131 | raleqdv 2635 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![A. A.](forall.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)
![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![)
)](rp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |
133 | 128, 132 | mpbird 166 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![A. A.](forall.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) ![ch ch](_chi.gif) ![) )](rp.gif) |
134 | | nfcv 2282 |
. . . . . . . . . . . 12
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![(
(](lp.gif) ![1 1](1.gif) ![) )](rp.gif) |
135 | | nfv 1509 |
. . . . . . . . . . . . 13
![F/ F/](finv.gif) ![x x](_x.gif) ![A. A.](forall.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) ![ch ch](_chi.gif) |
136 | | nfsbc1v 2931 |
. . . . . . . . . . . . 13
![F/ F/](finv.gif) ![x x](_x.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) |
137 | 135, 136 | nfim 1552 |
. . . . . . . . . . . 12
![F/ F/](finv.gif) ![x x](_x.gif) ![(
(](lp.gif) ![A. A.](forall.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) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
138 | | 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) |
139 | 138 | oveq2d 5798 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.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) ![) )](rp.gif) |
140 | 139 | raleqdv 2635 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![A. A.](forall.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) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |
141 | | sbceq1a 2922 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![[.
[.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
142 | 140, 141 | imbi12d 233 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![A. A.](forall.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)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
143 | | prmind2.7 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![ch ch](_chi.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) |
144 | 143 | ex 114 |
. . . . . . . . . . . 12
![( (](lp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
145 | 134, 137,
142, 144 | vtoclgaf 2754 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![( (](lp.gif) ![A. A.](forall.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) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
146 | 133, 145 | syl5com 29 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
147 | 125, 146 | sylbid 149 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![2 2](2.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
148 | 114, 147 | syl5bir 152 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![2 2](2.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) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
149 | | 2z 9106 |
. . . . . . . . . . 11
![ZZ ZZ](bbz.gif) |
150 | 149 | a1i 9 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
151 | 115 | nnzd 9196 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
152 | 151 | peano2zd 9200 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![1 1](1.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
153 | | 1zzd 9105 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
154 | 152, 153 | zsubcld 9202 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1
1](1.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
155 | 19, 21 | syl 14 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
156 | | dvdsdc 11537 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![ZZ ZZ](bbz.gif) DECID
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
157 | 155, 152,
156 | syl2anr 288 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![2 2](2.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif)
DECID
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
158 | 150, 154,
157 | exfzdc 10048 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) DECID ![E. E.](exists.gif)
![( (](lp.gif) ![2
2](2.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) ![) )](rp.gif) ![) )](rp.gif) |
159 | | exmiddc 822 |
. . . . . . . . 9
DECID ![E. E.](exists.gif) ![( (](lp.gif) ![2 2](2.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) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![2 2](2.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) ![E. E.](exists.gif) ![( (](lp.gif) ![2 2](2.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) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
160 | 158, 159 | syl 14 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![2 2](2.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) ![E. E.](exists.gif) ![( (](lp.gif) ![2 2](2.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) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
161 | 113, 148,
160 | mpjaod 708 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
162 | 161 | ex 114 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
163 | | ralsnsg 3568 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
164 | 16, 163 | syl 14 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1 1](1.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
165 | 162, 164 | sylibrd 168 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![(
(](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
166 | 165 | ancld 323 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![)
)](rp.gif)
![A. A.](forall.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
167 | | fzsuc 9880 |
. . . . . . 7
![( (](lp.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) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![{ {](lbrace.gif) ![(
(](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
168 | 116, 167 | sylbi 120 |
. . . . . 6
![( (](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) ![k k](_k.gif) ![{ {](lbrace.gif) ![(
(](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
169 | 168 | raleqdv 2635 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
170 | | ralunb 3262 |
. . . . 5
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![{
{](lbrace.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![)
)](rp.gif)
![A. A.](forall.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
171 | 169, 170 | syl6bb 195 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif)
![A. A.](forall.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
172 | 166, 171 | sylibrd 168 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![ph
ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
173 | 3, 5, 7, 9, 15, 172 | nnind 8760 |
. 2
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
174 | | elfz1end 9866 |
. . 3
![( (](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
175 | 174 | biimpi 119 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
176 | 1, 173, 175 | rspcdva 2798 |
1
![( (](lp.gif) ![et et](_eta.gif) ![) )](rp.gif) |