Step | Hyp | Ref
| Expression |
1 | | zssre 9085 |
. . . 4
![RR RR](bbr.gif) |
2 | | infssuzledc.a |
. . . . . . . . . 10
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) |
3 | | infssuzledc.s |
. . . . . . . . . . 11
![{ {](lbrace.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) |
4 | 3 | eleq2i 2207 |
. . . . . . . . . 10
![( (](lp.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
5 | 2, 4 | sylib 121 |
. . . . . . . . 9
![( (](lp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
6 | | elrabi 2841 |
. . . . . . . . 9
![( (](lp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![)
)](rp.gif) |
7 | 5, 6 | syl 14 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | | eluzelz 9359 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
9 | 7, 8 | syl 14 |
. . . . . . 7
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
10 | 9 | znegcld 9199 |
. . . . . 6
![( (](lp.gif) ![-u
-u](shortminus.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
11 | | negeq 7979 |
. . . . . . 7
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
12 | 11 | eleq1d 2209 |
. . . . . 6
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | 9 | zcnd 9198 |
. . . . . . . 8
![( (](lp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
14 | 13 | negnegd 8088 |
. . . . . . 7
![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
15 | 14, 2 | eqeltrd 2217 |
. . . . . 6
![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![)
)](rp.gif) |
16 | | simpr 109 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![-u
-u](shortminus.gif) ![m m](_m.gif) ![) )](rp.gif) |
17 | 9 | adantr 274 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
18 | 17 | zred 9197 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
19 | | eluzelz 9359 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
20 | 19 | adantl 275 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
21 | 20 | zred 9197 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
22 | | eluzle 9362 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif)
![-u -u](shortminus.gif) ![m m](_m.gif) ![) )](rp.gif) |
23 | 22 | adantl 275 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif)
![-u -u](shortminus.gif) ![m m](_m.gif) ![) )](rp.gif) |
24 | 18, 21, 23 | lenegcon1d 8313 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif)
![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
25 | 24 | adantr 274 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
26 | 16, 25 | jca 304 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 20 | znegcld 9199 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif)
![-u -u](shortminus.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
28 | 27 | adantr 274 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![-u -u](shortminus.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
29 | | infssuzledc.m |
. . . . . . . . . . . 12
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
30 | 29 | ad2antrr 480 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
31 | 9 | ad2antrr 480 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
32 | | elfz 9827 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![A A](_ca.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | 28, 30, 31, 32 | syl3anc 1217 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![A A](_ca.gif)
![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | 26, 33 | mpbird 166 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
35 | | infssuzledc.dc |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![A A](_ca.gif) ![) )](rp.gif)
DECID ![ps ps](_psi.gif) ![) )](rp.gif) |
36 | 35 | ralrimiva 2508 |
. . . . . . . . . 10
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![A A](_ca.gif) DECID ![ps ps](_psi.gif) ![) )](rp.gif) |
37 | 36 | ad2antrr 480 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![A A](_ca.gif) DECID ![ps
ps](_psi.gif) ![) )](rp.gif) |
38 | | nfsbc1v 2931 |
. . . . . . . . . . 11
![F/ F/](finv.gif) ![n n](_n.gif) ![[. [.](_dlbrack.gif) ![-u -u](shortminus.gif) ![n n](_n.gif) ![]. ].](_drbrack.gif) ![ps ps](_psi.gif) |
39 | 38 | nfdc 1638 |
. . . . . . . . . 10
![F/ F/](finv.gif) DECID ![[. [.](_dlbrack.gif) ![-u -u](shortminus.gif) ![n n](_n.gif) ![]. ].](_drbrack.gif) ![ps ps](_psi.gif) |
40 | | sbceq1a 2922 |
. . . . . . . . . . 11
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![[.
[.](_dlbrack.gif) ![-u -u](shortminus.gif) ![n n](_n.gif) ![]. ].](_drbrack.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
41 | 40 | dcbid 824 |
. . . . . . . . . 10
![( (](lp.gif) ![-u -u](shortminus.gif) DECID DECID ![[. [.](_dlbrack.gif) ![-u -u](shortminus.gif) ![n n](_n.gif) ![]. ].](_drbrack.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
42 | 39, 41 | rspc 2787 |
. . . . . . . . 9
![( (](lp.gif) ![-u -u](shortminus.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![A A](_ca.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![A A](_ca.gif) DECID DECID ![[. [.](_dlbrack.gif) ![-u -u](shortminus.gif) ![n n](_n.gif) ![]. ].](_drbrack.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
43 | 34, 37, 42 | sylc 62 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif)
DECID ![[. [.](_dlbrack.gif) ![-u -u](shortminus.gif) ![n n](_n.gif) ![]. ].](_drbrack.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
44 | 3 | eleq2i 2207 |
. . . . . . . . . 10
![( (](lp.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif) ![{
{](lbrace.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
45 | | nfcv 2282 |
. . . . . . . . . . . 12
![F/_ F/_](_finvbar.gif) ![n n](_n.gif) ![(
(](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) |
46 | 45 | elrabsf 2951 |
. . . . . . . . . . 11
![( (](lp.gif) ![-u -u](shortminus.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![ps ps](_psi.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![[. [.](_dlbrack.gif) ![-u -u](shortminus.gif) ![n n](_n.gif) ![]. ].](_drbrack.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
47 | | elfzuz 9833 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![-u -u](shortminus.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![A A](_ca.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![)
)](rp.gif) |
48 | 34, 47 | syl 14 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![)
)](rp.gif) |
49 | 48 | biantrurd 303 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![-u -u](shortminus.gif) ![n n](_n.gif) ![]. ].](_drbrack.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![[. [.](_dlbrack.gif) ![-u -u](shortminus.gif) ![n n](_n.gif) ![]. ].](_drbrack.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
50 | 46, 49 | bitr4id 198 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![ps ps](_psi.gif)
![[. [.](_dlbrack.gif) ![-u -u](shortminus.gif) ![n n](_n.gif) ![]. ].](_drbrack.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
51 | 44, 50 | syl5bb 191 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![( (](lp.gif) ![-u -u](shortminus.gif)
![[. [.](_dlbrack.gif) ![-u -u](shortminus.gif) ![n n](_n.gif) ![]. ].](_drbrack.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
52 | 51 | dcbid 824 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) DECID ![-u -u](shortminus.gif)
DECID ![[. [.](_dlbrack.gif) ![-u -u](shortminus.gif)
![n n](_n.gif) ![]. ].](_drbrack.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | 43, 52 | mpbird 166 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![m m](_m.gif)
DECID ![-u -u](shortminus.gif) ![S S](_cs.gif) ![)
)](rp.gif) |
54 | | simpr 109 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u
-u](shortminus.gif) ![m m](_m.gif)
![-u -u](shortminus.gif) ![m m](_m.gif) ![)
)](rp.gif) |
55 | | elrabi 2841 |
. . . . . . . . . . . 12
![( (](lp.gif) ![-u -u](shortminus.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![ps ps](_psi.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![)
)](rp.gif) |
56 | | eluzle 9362 |
. . . . . . . . . . . 12
![( (](lp.gif) ![-u -u](shortminus.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![-u
-u](shortminus.gif) ![m m](_m.gif) ![) )](rp.gif) |
57 | 55, 56 | syl 14 |
. . . . . . . . . . 11
![( (](lp.gif) ![-u -u](shortminus.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![ps ps](_psi.gif) ![-u
-u](shortminus.gif) ![m m](_m.gif) ![) )](rp.gif) |
58 | 57, 3 | eleq2s 2235 |
. . . . . . . . . 10
![( (](lp.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif) ![m m](_m.gif) ![) )](rp.gif) |
59 | 54, 58 | nsyl 618 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u
-u](shortminus.gif) ![m m](_m.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![)
)](rp.gif) |
60 | 59 | olcd 724 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u
-u](shortminus.gif) ![m m](_m.gif) ![(
(](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![)
)](rp.gif) ![) )](rp.gif) |
61 | | df-dc 821 |
. . . . . . . 8
DECID ![-u -u](shortminus.gif)
![( (](lp.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
62 | 60, 61 | sylibr 133 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u
-u](shortminus.gif) ![m m](_m.gif) DECID ![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) |
63 | 29 | adantr 274 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
64 | | zdcle 9151 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![ZZ ZZ](bbz.gif) DECID
![-u -u](shortminus.gif) ![m m](_m.gif) ![) )](rp.gif) |
65 | 63, 27, 64 | syl2anc 409 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif)
DECID
![-u -u](shortminus.gif) ![m m](_m.gif) ![)
)](rp.gif) |
66 | | exmiddc 822 |
. . . . . . . 8
DECID ![-u -u](shortminus.gif)
![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) |
67 | 65, 66 | syl 14 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) |
68 | 53, 62, 67 | mpjaodan 788 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif)
DECID ![-u -u](shortminus.gif) ![S S](_cs.gif) ![)
)](rp.gif) |
69 | | eluzle 9362 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif)
![A A](_ca.gif) ![) )](rp.gif) |
70 | 7, 69 | syl 14 |
. . . . . . . . . 10
![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) |
71 | 29 | zred 9197 |
. . . . . . . . . . 11
![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
72 | 9 | zred 9197 |
. . . . . . . . . . 11
![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
73 | 71, 72 | lenegd 8310 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
74 | 70, 73 | mpbid 146 |
. . . . . . . . 9
![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif) ![M M](_cm.gif) ![)
)](rp.gif) |
75 | 29 | znegcld 9199 |
. . . . . . . . . 10
![( (](lp.gif) ![-u
-u](shortminus.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
76 | | eluz 9363 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif) ![M M](_cm.gif) ![)
)](rp.gif) ![) )](rp.gif) |
77 | 10, 75, 76 | syl2anc 409 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif) ![M M](_cm.gif) ![)
)](rp.gif) ![) )](rp.gif) |
78 | 74, 77 | mpbird 166 |
. . . . . . . 8
![( (](lp.gif) ![-u
-u](shortminus.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
79 | | peano2uz 9405 |
. . . . . . . 8
![( (](lp.gif) ![-u -u](shortminus.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
80 | 78, 79 | syl 14 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
81 | 71 | ad2antrr 480 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
82 | 81 | renegcld 8166 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![-u -u](shortminus.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
83 | | peano2re 7922 |
. . . . . . . . . . . 12
![( (](lp.gif) ![-u -u](shortminus.gif)
![( (](lp.gif) ![-u
-u](shortminus.gif) ![1 1](1.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
84 | 82, 83 | syl 14 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
85 | | eluzelz 9359 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
86 | 85 | ad2antlr 481 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
87 | 86 | zred 9197 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
88 | | eluzle 9362 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![m m](_m.gif) ![) )](rp.gif) |
89 | 88 | ad2antlr 481 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![m m](_m.gif) ![) )](rp.gif) |
90 | 55, 3 | eleq2s 2235 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
91 | 90 | adantl 275 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![-u -u](shortminus.gif) ![S S](_cs.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![)
)](rp.gif) |
92 | 91, 56 | syl 14 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![-u -u](shortminus.gif) ![S S](_cs.gif) ![-u
-u](shortminus.gif) ![m m](_m.gif) ![) )](rp.gif) |
93 | 92 | adantlr 469 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![-u
-u](shortminus.gif) ![m m](_m.gif) ![) )](rp.gif) |
94 | 81, 87, 93 | lenegcon2d 8314 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![-u
-u](shortminus.gif) ![M M](_cm.gif) ![) )](rp.gif) |
95 | 84, 87, 82, 89, 94 | letrd 7910 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![-u -u](shortminus.gif) ![M M](_cm.gif) ![) )](rp.gif) |
96 | 75 | ad2antrr 480 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![-u -u](shortminus.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
97 | | zltp1le 9132 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![-u -u](shortminus.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
98 | 96, 96, 97 | syl2anc 409 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![1 1](1.gif)
![-u -u](shortminus.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
99 | 95, 98 | mpbird 166 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![M M](_cm.gif) ![) )](rp.gif) |
100 | 82 | ltnrd 7899 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![M M](_cm.gif) ![)
)](rp.gif) |
101 | 99, 100 | pm2.65da 651 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif)
![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) |
102 | 101 | ralrimiva 2508 |
. . . . . . 7
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![)
)](rp.gif) |
103 | | fveq2 5429 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![(
(](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![j j](_j.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
104 | 103 | raleqdv 2635 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![(
(](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![j j](_j.gif) ![-u -u](shortminus.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
105 | 104 | rspcev 2793 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![j j](_j.gif) ![-u -u](shortminus.gif)
![S S](_cs.gif) ![)
)](rp.gif) |
106 | 80, 102, 105 | syl2anc 409 |
. . . . . 6
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![j j](_j.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) |
107 | 10, 12, 15, 68, 106 | zsupcllemex 11675 |
. . . . 5
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif)
![A. A.](forall.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![z
z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
108 | | zre 9082 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
109 | 108 | anim1i 338 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
110 | | elrabi 2841 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![-u -u](shortminus.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![ps ps](_psi.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![)
)](rp.gif) |
111 | 110, 3 | eleq2s 2235 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
112 | | eluzelz 9359 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![-u -u](shortminus.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![-u -u](shortminus.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
113 | 111, 112 | syl 14 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
114 | 113 | adantl 275 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![-u -u](shortminus.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
115 | | recn 7777 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
116 | | znegclb 9111 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif)
![-u -u](shortminus.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![) )](rp.gif) |
117 | 115, 116 | syl 14 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif)
![-u -u](shortminus.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![) )](rp.gif) |
118 | 117 | adantr 274 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![) )](rp.gif) |
119 | 114, 118 | mpbird 166 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
120 | | simpr 109 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![)
)](rp.gif) |
121 | 119, 120 | jca 304 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
122 | 109, 121 | impbii 125 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![(
(](lp.gif) ![-u -u](shortminus.gif)
![S S](_cs.gif) ![)
)](rp.gif) ![) )](rp.gif) |
123 | | negeq 7979 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![b b](_b.gif) ![) )](rp.gif) |
124 | 123 | eleq1d 2209 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
125 | 124 | elrab 2844 |
. . . . . . . . . . 11
![( (](lp.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
126 | 124 | elrab 2844 |
. . . . . . . . . . 11
![( (](lp.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
127 | 122, 125,
126 | 3bitr4i 211 |
. . . . . . . . . 10
![( (](lp.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif)
![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
128 | 127 | a1i 9 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
129 | 128 | eqrdv 2138 |
. . . . . . . 8
![( (](lp.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif)
![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
130 | 129 | raleqdv 2635 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![{
{](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
131 | 129 | rexeqdv 2636 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![{
{](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![z
z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) |
132 | 131 | imbi2d 229 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![z z](_z.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
133 | 132 | ralbidv 2438 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![z z](_z.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif)
![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
134 | 130, 133 | anbi12d 465 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif)
![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif)
![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
135 | 134 | rexbidv 2439 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif)
![z z](_z.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif)
![A. A.](forall.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![z
z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
136 | 107, 135 | mpbid 146 |
. . . 4
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif)
![A. A.](forall.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![z
z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
137 | | ssrexv 3167 |
. . . 4
![( (](lp.gif)
![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![z z](_z.gif) ![)
)](rp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif)
![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
138 | 1, 136, 137 | mpsyl 65 |
. . 3
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif)
![A. A.](forall.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![z
z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
139 | | ssrab2 3187 |
. . . 4
![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![RR RR](bbr.gif) |
140 | 139 | a1i 9 |
. . 3
![( (](lp.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
141 | 138, 140 | supinfneg 9417 |
. 2
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![A. A.](forall.gif)
![( (](lp.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![} }](rbrace.gif) ![y y](_y.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
142 | | elrabi 2841 |
. . . . . . 7
![( (](lp.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
143 | | elrabi 2841 |
. . . . . . . . 9
![( (](lp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![)
)](rp.gif) |
144 | 143, 3 | eleq2s 2235 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![)
)](rp.gif) |
145 | | eluzelre 9360 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
146 | 144, 145 | syl 14 |
. . . . . . 7
![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
147 | | negeq 7979 |
. . . . . . . . . 10
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![a a](_a.gif) ![) )](rp.gif) |
148 | 147 | eleq1d 2209 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif)
![-u -u](shortminus.gif) ![{
{](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
149 | 148 | elrab3 2845 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif)
![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![) )](rp.gif) |
150 | | negeq 7979 |
. . . . . . . . . . 11
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![a a](_a.gif) ![) )](rp.gif) |
151 | 150 | eleq1d 2209 |
. . . . . . . . . 10
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
152 | 151 | elrab 2844 |
. . . . . . . . 9
![( (](lp.gif) ![-u -u](shortminus.gif)
![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
153 | | renegcl 8047 |
. . . . . . . . . 10
![( (](lp.gif) ![-u -u](shortminus.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
154 | 153 | biantrurd 303 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif)
![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
155 | 152, 154 | bitr4id 198 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif)
![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
156 | | recn 7777 |
. . . . . . . . . 10
![( (](lp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
157 | 156 | negnegd 8088 |
. . . . . . . . 9
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![a a](_a.gif) ![) )](rp.gif) |
158 | 157 | eleq1d 2209 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif)
![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
159 | 149, 155,
158 | 3bitrd 213 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif)
![S S](_cs.gif) ![)
)](rp.gif) ![) )](rp.gif) |
160 | 142, 146,
159 | pm5.21nii 694 |
. . . . . 6
![( (](lp.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif)
![S S](_cs.gif) ![)
)](rp.gif) |
161 | 160 | eqriv 2137 |
. . . . 5
![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif)
![S S](_cs.gif) |
162 | 161 | raleqi 2633 |
. . . 4
![( (](lp.gif) ![A. A.](forall.gif)
![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif)
![A. A.](forall.gif)
![x x](_x.gif) ![) )](rp.gif) |
163 | 161 | rexeqi 2634 |
. . . . . 6
![( (](lp.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![} }](rbrace.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![) )](rp.gif) |
164 | 163 | imbi2i 225 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![} }](rbrace.gif) ![y y](_y.gif) ![( (](lp.gif)
![E. E.](exists.gif)
![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
165 | 164 | ralbii 2444 |
. . . 4
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![} }](rbrace.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![E. E.](exists.gif)
![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
166 | 162, 165 | anbi12i 456 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![A. A.](forall.gif)
![( (](lp.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![} }](rbrace.gif) ![y y](_y.gif) ![)
)](rp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif)
![E. E.](exists.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
167 | 166 | rexbii 2445 |
. 2
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif)
![A. A.](forall.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![S S](_cs.gif) ![} }](rbrace.gif) ![} }](rbrace.gif) ![y y](_y.gif) ![)
)](rp.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif) ![( (](lp.gif)
![E. E.](exists.gif)
![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
168 | 141, 167 | sylib 121 |
1
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |