Step | Hyp | Ref
| Expression |
1 | | nncdiv3lem2 6276 |
. 2
![{](lbrace.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
2 | | eqeq1 2359 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
0c
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | eqeq1 2359 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | eqeq1 2359 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
5 | 2, 3, 4 | 3orbi123d 1251 |
. . 3
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
0c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | 5 | rexbidv 2635 |
. 2
![(](lp.gif) 0c ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![E.](exists.gif) Nn 0c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
0c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | eqeq1 2359 |
. . . 4
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | | eqeq1 2359 |
. . . 4
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | eqeq1 2359 |
. . . 4
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 7, 8, 9 | 3orbi123d 1251 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 10 | rexbidv 2635 |
. 2
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | eqeq1 2359 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | eqeq1 2359 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | eqeq1 2359 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 12, 13, 14 | 3orbi123d 1251 |
. . 3
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 15 | rexbidv 2635 |
. 2
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | | eqeq1 2359 |
. . . 4
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | eqeq1 2359 |
. . . 4
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | eqeq1 2359 |
. . . 4
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 17, 18, 19 | 3orbi123d 1251 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 20 | rexbidv 2635 |
. 2
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | | peano1 4402 |
. . 3
0c
Nn |
23 | | addcid1 4405 |
. . . . 5
![(](lp.gif) 0c 0c 0c
0c
0c![)](rp.gif) |
24 | | addcid2 4407 |
. . . . 5
0c
0c
0c |
25 | 23, 24 | eqtr2i 2374 |
. . . 4
0c
![(](lp.gif) 0c 0c 0c![)](rp.gif) |
26 | | 3mix1 1124 |
. . . 4
0c ![(](lp.gif) 0c 0c 0c 0c ![(](lp.gif) 0c 0c 0c
0c
![(](lp.gif) ![(](lp.gif) 0c 0c 0c
1c
0c
![(](lp.gif) ![(](lp.gif) 0c 0c 0c
2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 25, 26 | ax-mp 5 |
. . 3
0c ![(](lp.gif) 0c 0c 0c
0c
![(](lp.gif) ![(](lp.gif) 0c 0c 0c
1c
0c
![(](lp.gif) ![(](lp.gif) 0c 0c 0c
2c![)](rp.gif) ![)](rp.gif) |
28 | | addceq12 4385 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
0c 0c ![(](lp.gif)
![n](_n.gif)
0c
0c![)](rp.gif) ![)](rp.gif) |
29 | 28 | anidms 626 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif) ![n](_n.gif)
0c
0c![)](rp.gif) ![)](rp.gif) |
30 | | id 19 |
. . . . . . 7
![(](lp.gif) 0c
0c![)](rp.gif) |
31 | 29, 30 | addceq12d 4391 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
![(](lp.gif) 0c 0c 0c![)](rp.gif) ![)](rp.gif) |
32 | 31 | eqeq2d 2364 |
. . . . 5
![(](lp.gif) 0c 0c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 0c ![(](lp.gif) 0c 0c 0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 31 | addceq1d 4389 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) 0c 0c 0c
1c![)](rp.gif) ![)](rp.gif) |
34 | 33 | eqeq2d 2364 |
. . . . 5
![(](lp.gif) 0c 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
0c
![(](lp.gif) ![(](lp.gif) 0c 0c 0c
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 31 | addceq1d 4389 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![(](lp.gif) ![(](lp.gif) 0c 0c 0c
2c![)](rp.gif) ![)](rp.gif) |
36 | 35 | eqeq2d 2364 |
. . . . 5
![(](lp.gif) 0c 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
0c
![(](lp.gif) ![(](lp.gif) 0c 0c 0c
2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 32, 34, 36 | 3orbi123d 1251 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
0c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) 0c ![(](lp.gif) 0c
0c
0c
0c
![(](lp.gif) ![(](lp.gif) 0c 0c 0c
1c
0c
![(](lp.gif) ![(](lp.gif) 0c 0c 0c
2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 37 | rspcev 2955 |
. . 3
![(](lp.gif) 0c Nn 0c ![(](lp.gif) 0c 0c 0c
0c
![(](lp.gif) ![(](lp.gif) 0c 0c 0c
1c
0c
![(](lp.gif) ![(](lp.gif) 0c 0c 0c
2c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif)
Nn 0c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
0c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 22, 27, 38 | mp2an 653 |
. 2
![E.](exists.gif) Nn 0c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
0c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
40 | | addceq1 4383 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
41 | 40 | reximi 2721 |
. . . . 5
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
42 | 41 | a1i 10 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![E.](exists.gif) Nn ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
43 | | addceq1 4383 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
1c![)](rp.gif) ![)](rp.gif) |
44 | | addcass 4415 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c 1c![)](rp.gif) ![)](rp.gif) |
45 | | 1p1e2c 6155 |
. . . . . . . . 9
1c
1c
2c |
46 | 45 | addceq2i 4387 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) |
47 | 44, 46 | eqtri 2373 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) |
48 | 43, 47 | syl6eq 2401 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
49 | 48 | reximi 2721 |
. . . . 5
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
50 | 49 | a1i 10 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | | peano2 4403 |
. . . . . . . . 9
![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) |
52 | | addc32 4416 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
2c
![n](_n.gif) ![)](rp.gif) |
53 | 45 | addceq2i 4387 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 2c![)](rp.gif) |
54 | | addc4 4417 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
55 | 53, 54 | eqtr3i 2375 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 2c
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
56 | 55 | addceq1i 4386 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 2c ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) |
57 | 52, 56 | eqtri 2373 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) |
58 | 57 | addceq1i 4386 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) 1c![)](rp.gif) |
59 | | addcass 4415 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
60 | 58, 59 | eqtri 2373 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
61 | | addceq12 4385 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
62 | 61 | anidms 626 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
63 | | id 19 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
64 | 62, 63 | addceq12d 4391 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![a](_a.gif)
![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
65 | 64 | eqeq2d 2364 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c 1c
![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
66 | 65 | rspcev 2955 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
1c
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
67 | 51, 60, 66 | sylancl 643 |
. . . . . . . 8
![(](lp.gif) Nn ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
1c
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
68 | | addceq1 4383 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c![)](rp.gif) ![)](rp.gif) |
69 | 68 | eqeq1d 2361 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
70 | 69 | rexbidv 2635 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c
1c
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
71 | 67, 70 | syl5ibrcom 213 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
72 | 71 | rexlimiv 2732 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
73 | | addceq12 4385 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![(](lp.gif) ![a](_a.gif)
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
74 | 73 | anidms 626 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
75 | | id 19 |
. . . . . . . . 9
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) |
76 | 74, 75 | addceq12d 4391 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
77 | 76 | eqeq2d 2364 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
78 | 77 | cbvrexv 2836 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
79 | 72, 78 | sylib 188 |
. . . . 5
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
80 | 79 | a1i 10 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
81 | 42, 50, 80 | 3orim123d 1260 |
. . 3
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
82 | | df-3or 935 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
83 | 82 | rexbii 2639 |
. . . 4
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
84 | | r19.43 2766 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
85 | 84 | orbi1i 506 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
86 | | r19.43 2766 |
. . . . 5
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
87 | | df-3or 935 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
88 | 85, 86, 87 | 3bitr4i 268 |
. . . 4
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
89 | 83, 88 | bitri 240 |
. . 3
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
90 | | df-3or 935 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
91 | 90 | rexbii 2639 |
. . . 4
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
92 | | r19.43 2766 |
. . . . 5
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
93 | | r19.43 2766 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
94 | 93 | orbi1i 506 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
95 | | df-3or 935 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
96 | | 3orrot 940 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
97 | 94, 95, 96 | 3bitr2i 264 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
98 | 92, 97 | bitri 240 |
. . . 4
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
99 | 91, 98 | bitri 240 |
. . 3
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
100 | 81, 89, 99 | 3imtr4g 261 |
. 2
![(](lp.gif) Nn ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
101 | 1, 6, 11, 16, 21, 39, 100 | finds 4411 |
1
![(](lp.gif) Nn ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |