Detailed syntax breakdown of Definition df-lgs
Step | Hyp | Ref
| Expression |
1 | | clgs 14065 |
. 2
![/ /](solidus.gif) ![L L](subcl.gif) |
2 | | va |
. . 3
![a a](_a.gif) |
3 | | vn |
. . 3
![n n](_n.gif) |
4 | | cz 9242 |
. . 3
![ZZ ZZ](bbz.gif) |
5 | 3 | cv 1352 |
. . . . 5
![n n](_n.gif) |
6 | | cc0 7802 |
. . . . 5
![0 0](0.gif) |
7 | 5, 6 | wceq 1353 |
. . . 4
![0 0](0.gif) |
8 | 2 | cv 1352 |
. . . . . . 7
![a a](_a.gif) |
9 | | c2 8959 |
. . . . . . 7
![2 2](2.gif) |
10 | | cexp 10505 |
. . . . . . 7
![^ ^](uparrow.gif) |
11 | 8, 9, 10 | co 5869 |
. . . . . 6
![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) |
12 | | c1 7803 |
. . . . . 6
![1 1](1.gif) |
13 | 11, 12 | wceq 1353 |
. . . . 5
![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![1 1](1.gif) |
14 | 13, 12, 6 | cif 3534 |
. . . 4
![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![1 1](1.gif) ![1 1](1.gif) ![0 0](0.gif) ![) )](rp.gif) |
15 | | clt 7982 |
. . . . . . . 8
![< <](lt.gif) |
16 | 5, 6, 15 | wbr 4000 |
. . . . . . 7
![0 0](0.gif) |
17 | 8, 6, 15 | wbr 4000 |
. . . . . . 7
![0 0](0.gif) |
18 | 16, 17 | wa 104 |
. . . . . 6
![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) |
19 | 12 | cneg 8119 |
. . . . . 6
![-u -u](shortminus.gif) ![1 1](1.gif) |
20 | 18, 19, 12 | cif 3534 |
. . . . 5
![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif)
![0 0](0.gif) ![)
)](rp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) |
21 | | cabs 10990 |
. . . . . . 7
![abs abs](_abs.gif) |
22 | 5, 21 | cfv 5212 |
. . . . . 6
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) |
23 | | cmul 7807 |
. . . . . . 7
![x. x.](cdot.gif) |
24 | | vm |
. . . . . . . 8
![m m](_m.gif) |
25 | | cn 8908 |
. . . . . . . 8
![NN NN](bbn.gif) |
26 | 24 | cv 1352 |
. . . . . . . . . 10
![m m](_m.gif) |
27 | | cprime 12090 |
. . . . . . . . . 10
![Prime Prime](bbp.gif) |
28 | 26, 27 | wcel 2148 |
. . . . . . . . 9
![Prime
Prime](bbp.gif) |
29 | 26, 9 | wceq 1353 |
. . . . . . . . . . 11
![2 2](2.gif) |
30 | | cdvds 11778 |
. . . . . . . . . . . . 13
![|| ||](parallel.gif) |
31 | 9, 8, 30 | wbr 4000 |
. . . . . . . . . . . 12
![a a](_a.gif) |
32 | | c8 8965 |
. . . . . . . . . . . . . . 15
![8 8](8.gif) |
33 | | cmo 10308 |
. . . . . . . . . . . . . . 15
![mod mod](_mod.gif) |
34 | 8, 32, 33 | co 5869 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![8 8](8.gif) ![) )](rp.gif) |
35 | | c7 8964 |
. . . . . . . . . . . . . . 15
![7 7](7.gif) |
36 | 12, 35 | cpr 3592 |
. . . . . . . . . . . . . 14
![{ {](lbrace.gif) ![1 1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) |
37 | 34, 36 | wcel 2148 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![8 8](8.gif) ![{
{](lbrace.gif) ![1 1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) |
38 | 37, 12, 19 | cif 3534 |
. . . . . . . . . . . 12
![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![8 8](8.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) ![1
1](1.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![)
)](rp.gif) |
39 | 31, 6, 38 | cif 3534 |
. . . . . . . . . . 11
![if if](_if.gif) ![( (](lp.gif) ![a a](_a.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![8 8](8.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) ![1
1](1.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) |
40 | | cmin 8118 |
. . . . . . . . . . . . . . . . 17
![- -](minus.gif) |
41 | 26, 12, 40 | co 5869 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) |
42 | | cdiv 8618 |
. . . . . . . . . . . . . . . 16
![/ /](solidus.gif) |
43 | 41, 9, 42 | co 5869 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) |
44 | 8, 43, 10 | co 5869 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
45 | | caddc 7805 |
. . . . . . . . . . . . . 14
![+ +](plus.gif) |
46 | 44, 12, 45 | co 5869 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) |
47 | 46, 26, 33 | co 5869 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![m m](_m.gif) ![) )](rp.gif) |
48 | 47, 12, 40 | co 5869 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![2 2](2.gif) ![)
)](rp.gif) ![1 1](1.gif) ![m m](_m.gif) ![1 1](1.gif) ![) )](rp.gif) |
49 | 29, 39, 48 | cif 3534 |
. . . . . . . . . 10
![if if](_if.gif) ![( (](lp.gif) ![2 2](2.gif) ![if if](_if.gif) ![( (](lp.gif) ![a a](_a.gif)
![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![8 8](8.gif) ![{ {](lbrace.gif) ![1
1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) ![1 1](1.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![m m](_m.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
50 | | cpc 12267 |
. . . . . . . . . . 11
![pCnt pCnt](_pcnt.gif) |
51 | 26, 5, 50 | co 5869 |
. . . . . . . . . 10
![( (](lp.gif) ![n n](_n.gif) ![) )](rp.gif) |
52 | 49, 51, 10 | co 5869 |
. . . . . . . . 9
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![2 2](2.gif) ![if if](_if.gif) ![( (](lp.gif) ![a a](_a.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![8 8](8.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) ![1 1](1.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![m m](_m.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![(
(](lp.gif) ![n n](_n.gif) ![)
)](rp.gif) ![) )](rp.gif) |
53 | 28, 52, 12 | cif 3534 |
. . . . . . . 8
![if if](_if.gif) ![( (](lp.gif) ![Prime Prime](bbp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![2 2](2.gif) ![if if](_if.gif) ![( (](lp.gif) ![a a](_a.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![8 8](8.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) ![1
1](1.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2
2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![m m](_m.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) |
54 | 24, 25, 53 | cmpt 4061 |
. . . . . . 7
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![Prime Prime](bbp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![2 2](2.gif) ![if if](_if.gif) ![( (](lp.gif) ![a a](_a.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![8 8](8.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) ![1
1](1.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2
2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![m m](_m.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
55 | 23, 54, 12 | cseq 10431 |
. . . . . 6
![seq seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![Prime Prime](bbp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![2 2](2.gif) ![if if](_if.gif) ![( (](lp.gif) ![a a](_a.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![8 8](8.gif) ![{ {](lbrace.gif) ![1
1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) ![1 1](1.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![m m](_m.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![( (](lp.gif)
![n n](_n.gif) ![) )](rp.gif) ![)
)](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
56 | 22, 55 | cfv 5212 |
. . . . 5
![seq seq](_seq.gif) ![1 1](1.gif) ![(
(](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![Prime Prime](bbp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![2 2](2.gif) ![if if](_if.gif) ![( (](lp.gif) ![a a](_a.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![8 8](8.gif) ![{ {](lbrace.gif) ![1
1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) ![1 1](1.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![m m](_m.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![( (](lp.gif)
![n n](_n.gif) ![) )](rp.gif) ![)
)](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) |
57 | 20, 56, 23 | co 5869 |
. . . 4
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![1 1](1.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![Prime Prime](bbp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![2 2](2.gif) ![if if](_if.gif) ![( (](lp.gif) ![a a](_a.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![8 8](8.gif) ![{ {](lbrace.gif) ![1
1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) ![1 1](1.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![m m](_m.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![( (](lp.gif)
![n n](_n.gif) ![) )](rp.gif) ![)
)](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
58 | 7, 14, 57 | cif 3534 |
. . 3
![if if](_if.gif) ![( (](lp.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![1 1](1.gif) ![1 1](1.gif) ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![1 1](1.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![Prime Prime](bbp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![2 2](2.gif) ![if if](_if.gif) ![( (](lp.gif) ![a a](_a.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![8 8](8.gif) ![{ {](lbrace.gif) ![1
1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) ![1 1](1.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![m m](_m.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![( (](lp.gif)
![n n](_n.gif) ![) )](rp.gif) ![)
)](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
59 | 2, 3, 4, 4, 58 | cmpo 5871 |
. 2
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![if if](_if.gif) ![( (](lp.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![1 1](1.gif) ![1 1](1.gif) ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![1 1](1.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![Prime Prime](bbp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![2 2](2.gif) ![if if](_if.gif) ![( (](lp.gif) ![a a](_a.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![8 8](8.gif) ![{ {](lbrace.gif) ![1
1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) ![1 1](1.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![m m](_m.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![( (](lp.gif)
![n n](_n.gif) ![) )](rp.gif) ![)
)](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
60 | 1, 59 | wceq 1353 |
1
![/ /](solidus.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![if if](_if.gif) ![( (](lp.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![1 1](1.gif) ![1 1](1.gif) ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![1 1](1.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![Prime Prime](bbp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![2 2](2.gif) ![if if](_if.gif) ![( (](lp.gif) ![a a](_a.gif) ![0 0](0.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![8 8](8.gif) ![{ {](lbrace.gif) ![1
1](1.gif) ![7 7](7.gif) ![} }](rbrace.gif) ![1 1](1.gif) ![-u -u](shortminus.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![m m](_m.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![( (](lp.gif)
![n n](_n.gif) ![) )](rp.gif) ![)
)](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |