Step | Hyp | Ref
| Expression |
1 | | dfevenfin2 4512 |
. . . 4
Evenfin ![{](lbrace.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![k](_k.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![}](rbrace.gif) |
2 | | dfoddfin2 4513 |
. . . 4
Oddfin ![{](lbrace.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![}](rbrace.gif) |
3 | 1, 2 | ineq12i 3455 |
. . 3
Evenfin Oddfin ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![k](_k.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![{](lbrace.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
4 | | inab 3522 |
. . 3
![(](lp.gif) ![{](lbrace.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![k](_k.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![{](lbrace.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![}](rbrace.gif)
![{](lbrace.gif)
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![k](_k.gif) ![(/)](varnothing.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
5 | 3, 4 | eqtri 2373 |
. 2
Evenfin Oddfin ![{](lbrace.gif)
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![k](_k.gif) ![(/)](varnothing.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
6 | | evenodddisjlem1 4515 |
. . . . . . . . 9
![{](lbrace.gif) ![(](lp.gif) ![(](lp.gif) ![j](_j.gif)
![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
7 | | addceq12 4385 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif)
0c 0c ![(](lp.gif)
![j](_j.gif)
0c
0c![)](rp.gif) ![)](rp.gif) |
8 | 7 | anidms 626 |
. . . . . . . . . . . 12
![(](lp.gif) 0c ![(](lp.gif) ![j](_j.gif)
0c
0c![)](rp.gif) ![)](rp.gif) |
9 | | addcid2 4407 |
. . . . . . . . . . . 12
0c
0c
0c |
10 | 8, 9 | syl6eq 2401 |
. . . . . . . . . . 11
![(](lp.gif) 0c ![(](lp.gif) ![j](_j.gif)
0c![)](rp.gif) |
11 | 10 | neeq1d 2529 |
. . . . . . . . . 10
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![j](_j.gif)
0c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 10 | neeq1d 2529 |
. . . . . . . . . . . 12
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![j](_j.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c 0c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | 12 | imbi2d 307 |
. . . . . . . . . . 11
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c
![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c 0c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | 13 | ralbidv 2634 |
. . . . . . . . . 10
![(](lp.gif) 0c ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
0c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 11, 14 | imbi12d 311 |
. . . . . . . . 9
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![j](_j.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) 0c ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
0c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | | addceq12 4385 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![(](lp.gif) ![j](_j.gif)
![(](lp.gif) ![m](_m.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | anidms 626 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![m](_m.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 17 | neeq1d 2529 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![j](_j.gif)
![(](lp.gif) ![m](_m.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 17 | neeq1d 2529 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 19 | imbi2d 307 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 20 | ralbidv 2634 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | | addceq12 4385 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif)
![p](_p.gif) ![(](lp.gif) ![n](_n.gif)
![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | anidms 626 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 23 | addceq1d 4389 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) |
25 | 24 | neeq1d 2529 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 24 | neeq2d 2530 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif)
![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 25, 26 | imbi12d 311 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c ![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 27 | cbvralv 2835 |
. . . . . . . . . . 11
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 21, 28 | syl6bb 252 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 18, 29 | imbi12d 311 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![j](_j.gif)
![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | | addceq12 4385 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 31 | anidms 626 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![j](_j.gif)
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | | addcass 4415 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
34 | | addc32 4416 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif)
1c
![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c![)](rp.gif) |
35 | 34 | addceq1i 4386 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c![)](rp.gif) |
36 | 33, 35 | eqtr3i 2375 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c![)](rp.gif) |
37 | 32, 36 | syl6eq 2401 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![j](_j.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c
1c![)](rp.gif) ![)](rp.gif) |
38 | 37 | neeq1d 2529 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![j](_j.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 37 | neeq1d 2529 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![j](_j.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 39 | imbi2d 307 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c
![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 40 | ralbidv 2634 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 38, 41 | imbi12d 311 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![j](_j.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
43 | | addceq12 4385 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif)
![k](_k.gif) ![(](lp.gif) ![j](_j.gif)
![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 43 | anidms 626 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 44 | neeq1d 2529 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![j](_j.gif)
![(](lp.gif) ![k](_k.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 44 | neeq1d 2529 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 46 | imbi2d 307 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 47 | ralbidv 2634 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 45, 48 | imbi12d 311 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![j](_j.gif)
![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![j](_j.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | | 0cnsuc 4401 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c 0c |
51 | 50 | necomi 2598 |
. . . . . . . . . . . 12
0c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) |
52 | 51 | a1i 10 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c 0c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
53 | 52 | rgenw 2681 |
. . . . . . . . . 10
![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
0c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
54 | 53 | a1i 10 |
. . . . . . . . 9
0c ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
0c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
55 | | addcass 4415 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c 1c![)](rp.gif) ![)](rp.gif) |
56 | 55 | neeq1i 2526 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c![)](rp.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
57 | | addcnnul 4453 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![m](_m.gif)
1c 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 57 | simpld 445 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c![)](rp.gif)
![(](lp.gif) ![m](_m.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
59 | 56, 58 | sylbi 187 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![(](lp.gif) ![m](_m.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
60 | 59 | adantl 452 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![m](_m.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
61 | | simprl 732 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) Nn ![)](rp.gif) |
62 | | nnc0suc 4412 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) Nn ![(](lp.gif)
0c ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
63 | 61, 62 | sylib 188 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) 0c ![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
64 | | 0cnsuc 4401 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 0c |
65 | | addceq12 4385 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif)
0c 0c ![(](lp.gif)
![n](_n.gif)
0c
0c![)](rp.gif) ![)](rp.gif) |
66 | 65 | anidms 626 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) 0c ![(](lp.gif) ![n](_n.gif)
0c
0c![)](rp.gif) ![)](rp.gif) |
67 | 66, 9 | syl6eq 2401 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) 0c ![(](lp.gif) ![n](_n.gif)
0c![)](rp.gif) |
68 | 67 | neeq2d 2530 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 0c![)](rp.gif) ![)](rp.gif) |
69 | 64, 68 | mpbiri 224 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
70 | 69 | a1i 10 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
71 | | simpr 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) 1c Nn Nn ![)](rp.gif) |
72 | 71 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) Nn ![)](rp.gif) |
73 | | addceq12 4385 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif)
![q](_q.gif) ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
74 | 73 | anidms 626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
75 | 74 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![p](_p.gif) 1c ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) |
76 | 75 | neeq1d 2529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
77 | 75 | neeq2d 2530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
78 | 76, 77 | imbi12d 311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c ![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
79 | 78 | rspcv 2951 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c ![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c ![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
80 | 72, 79 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c ![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
81 | | addc4 4417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c 1c![)](rp.gif) ![)](rp.gif) |
82 | 81 | addceq1i 4386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c 1c![)](rp.gif)
1c![)](rp.gif) |
83 | | addc32 4416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c 1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c 1c
1c![)](rp.gif) ![)](rp.gif) |
84 | 82, 83 | eqtri 2373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c 1c
1c![)](rp.gif) ![)](rp.gif) |
85 | 84 | neeq1i 2526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c 1c
1c![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
86 | | addcnnul 4453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c
1c 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c 1c 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
87 | 86 | simpld 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c
1c 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
88 | 85, 87 | sylbi 187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
89 | 88 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) 1c Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) |
90 | 89 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
91 | | addc32 4416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c
![(](lp.gif) ![(](lp.gif) 1c ![q](_q.gif) ![)](rp.gif) |
92 | 91 | addceq1i 4386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![q](_q.gif) 1c![)](rp.gif) |
93 | | addcass 4415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![q](_q.gif) 1c ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
94 | 92, 93 | eqtri 2373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
95 | 94 | eqeq2i 2363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c
1c
![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
96 | | simplll 734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c
1c![)](rp.gif) Nn ![)](rp.gif) |
97 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![m](_m.gif) Nn ![)](rp.gif) |
98 | 97 | anidms 626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) Nn ![(](lp.gif) ![m](_m.gif)
Nn ![)](rp.gif) |
99 | 96, 98 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c
1c![)](rp.gif) ![(](lp.gif) ![m](_m.gif) Nn ![)](rp.gif) |
100 | | simplrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c
1c![)](rp.gif) Nn ![)](rp.gif) |
101 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![q](_q.gif) Nn ![)](rp.gif) |
102 | 101 | anidms 626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) Nn ![(](lp.gif) ![q](_q.gif)
Nn ![)](rp.gif) |
103 | | peano2 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif) ![q](_q.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c
Nn ![)](rp.gif) |
104 | 100, 102,
103 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c Nn ![)](rp.gif) |
105 | | simpr 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c
1c![)](rp.gif) ![)](rp.gif) |
106 | | simpllr 735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![)](rp.gif) |
107 | | addcnnul 4453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
108 | 107 | simpld 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
109 | 106, 108 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
110 | | prepeano4 4451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![m](_m.gif)
![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) |
111 | 99, 104, 105, 109, 110 | syl22anc 1183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c
1c![)](rp.gif) ![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c![)](rp.gif) ![)](rp.gif) |
112 | 111 | ex 423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
113 | 95, 112 | syl5bir 209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
114 | 113 | necon3d 2554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
115 | 90, 114 | embantd 50 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
116 | 80, 115 | syld 40 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
Nn ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
117 | 116 | expr 598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
118 | 117 | com23 72 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c ![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
119 | 118 | ex 423 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
120 | 119 | com23 72 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c ![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif)
1c
![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
121 | 120 | imp31 421 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif)
1c
![(/)](varnothing.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
122 | 121 | com12 27 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif)
1c
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
123 | | addceq12 4385 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
124 | 123 | anidms 626 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![n](_n.gif)
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
125 | 124 | addceq1d 4389 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c![)](rp.gif) ![)](rp.gif) |
126 | 125 | neeq1d 2529 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
127 | 126 | anbi2d 684 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
128 | 124 | neeq2d 2530 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
129 | 127, 128 | imbi12d 311 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif)
1c
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
130 | 122, 129 | syl5ibrcom 213 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
131 | 130 | rexlimiv 2732 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
132 | 131 | com12 27 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
133 | 132 | adantrl 696 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
134 | 70, 133 | jaod 369 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) 0c ![E.](exists.gif) Nn ![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
135 | 63, 134 | mpd 14 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
136 | | simplll 734 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) Nn ![)](rp.gif) |
137 | 136 | adantr 451 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c![)](rp.gif)
Nn ![)](rp.gif) |
138 | | peano2 4403 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![m](_m.gif) Nn ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
Nn ![)](rp.gif) |
139 | 137, 98, 138 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c Nn ![)](rp.gif) |
140 | | simplrl 736 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c![)](rp.gif)
Nn ![)](rp.gif) |
141 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![n](_n.gif) Nn ![)](rp.gif) |
142 | 141 | anidms 626 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) Nn ![(](lp.gif) ![n](_n.gif)
Nn ![)](rp.gif) |
143 | 140, 142 | syl 15 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c![)](rp.gif)
![(](lp.gif) ![n](_n.gif) Nn ![)](rp.gif) |
144 | | simpr 447 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
145 | | simpllr 735 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![)](rp.gif) |
146 | 145 | adantr 451 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![)](rp.gif) |
147 | | prepeano4 4451 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
Nn ![(](lp.gif) ![n](_n.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
148 | 139, 143,
144, 146, 147 | syl22anc 1183 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) 1c ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
149 | 148 | ex 423 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
150 | 149 | necon3d 2554 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c ![(](lp.gif) ![n](_n.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
151 | 135, 150 | mpd 14 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
152 | 151 | expr 598 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
153 | 152 | ralrimiva 2697 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
154 | 153 | ex 423 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c ![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
155 | 60, 154 | embantd 50 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
156 | 155 | ex 423 |
. . . . . . . . . 10
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
157 | 156 | com23 72 |
. . . . . . . . 9
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
1c
1c
![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) 1c
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
158 | 6, 15, 30, 42, 49, 54, 157 | finds 4411 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
159 | | df-ne 2518 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) |
160 | 159 | imbi2i 303 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif)
![k](_k.gif)
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
161 | | con2b 324 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif)
![k](_k.gif)
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
162 | 160, 161 | bitri 240 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
163 | | imnan 411 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
164 | 162, 163 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![k](_k.gif)
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
165 | 164 | ralbii 2638 |
. . . . . . . . 9
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
166 | | ralnex 2624 |
. . . . . . . . 9
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
167 | 165, 166 | bitri 240 |
. . . . . . . 8
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
168 | 158, 167 | syl6ib 217 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
169 | | eqeq1 2359 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif)
![k](_k.gif)
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
170 | 169 | anbi1d 685 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
171 | 170 | rexbidv 2635 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
172 | 171 | notbid 285 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
173 | 172 | imbi2d 307 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
174 | 168, 173 | syl5ibrcom 213 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
175 | 174 | imp3a 420 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![k](_k.gif)
![(/)](varnothing.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
176 | 175 | rexlimiv 2732 |
. . . 4
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![k](_k.gif) ![(/)](varnothing.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
177 | | imnan 411 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![k](_k.gif) ![(/)](varnothing.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![k](_k.gif) ![(/)](varnothing.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
178 | 176, 177 | mpbi 199 |
. . 3
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif) ![(](lp.gif) ![k](_k.gif) ![(/)](varnothing.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
179 | 178 | abf 3584 |
. 2
![{](lbrace.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![k](_k.gif)
![(](lp.gif) ![k](_k.gif) ![(/)](varnothing.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![(/)](varnothing.gif) |
180 | 5, 179 | eqtri 2373 |
1
Evenfin Oddfin ![(/)](varnothing.gif) |