Step | Hyp | Ref
| Expression |
1 | | opkeq2 4060 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![n](_n.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) ![>>](rrangle.gif) ![)](rp.gif) |
2 | 1 | eleq1d 2419 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) |
3 | | eqeq2 2362 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | opkeq1 4059 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![M](_cm.gif) ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) ![>>](rrangle.gif) ![)](rp.gif) |
5 | 4 | eleq1d 2419 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![M](_cm.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) |
6 | 2, 3, 5 | 3orbi123d 1251 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![M](_cm.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin
![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | 6 | imbi2d 307 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![M](_cm.gif) fin ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | 7 | imbi2d 307 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | ltfintrilem1 4465 |
. . . . . 6
![{](lbrace.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif)
fin
![<<](llangle.gif) ![n](_n.gif)
![k](_k.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
10 | | neeq1 2524 |
. . . . . . . 8
![(](lp.gif) 0c ![(](lp.gif)
0c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
11 | | opkeq1 4059 |
. . . . . . . . . 10
![(](lp.gif) 0c ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) 0c ![n](_n.gif) ![>>](rrangle.gif) ![)](rp.gif) |
12 | 11 | eleq1d 2419 |
. . . . . . . . 9
![(](lp.gif) 0c ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) fin 0c ![n](_n.gif)
fin ![)](rp.gif) ![)](rp.gif) |
13 | | eqeq1 2359 |
. . . . . . . . 9
![(](lp.gif) 0c ![(](lp.gif) 0c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | opkeq2 4060 |
. . . . . . . . . 10
![(](lp.gif) 0c ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) ![<<](llangle.gif) ![n](_n.gif)
0c![>>](rrangle.gif) ![)](rp.gif) |
15 | 14 | eleq1d 2419 |
. . . . . . . . 9
![(](lp.gif) 0c ![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) fin ![<<](llangle.gif) ![n](_n.gif)
0c fin ![)](rp.gif) ![)](rp.gif) |
16 | 12, 13, 15 | 3orbi123d 1251 |
. . . . . . . 8
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif)
fin
![<<](llangle.gif) ![n](_n.gif)
![k](_k.gif) fin ![(](lp.gif) 0c ![n](_n.gif) fin 0c ![<<](llangle.gif) ![n](_n.gif) 0c fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 10, 16 | imbi12d 311 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif)
fin
![<<](llangle.gif) ![n](_n.gif)
![k](_k.gif) fin ![)](rp.gif) 0c ![(](lp.gif) 0c ![n](_n.gif)
fin 0c ![<<](llangle.gif) ![n](_n.gif) 0c fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 17 | imbi2d 307 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) fin ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) Nn 0c
![(](lp.gif) 0c ![n](_n.gif)
fin 0c ![<<](llangle.gif) ![n](_n.gif) 0c fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | neeq1 2524 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | opkeq1 4059 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) ![>>](rrangle.gif) ![)](rp.gif) |
21 | 20 | eleq1d 2419 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![)](rp.gif) ![)](rp.gif) |
22 | | eqeq1 2359 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
23 | | opkeq2 4060 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) ![>>](rrangle.gif) ![)](rp.gif) |
24 | 23 | eleq1d 2419 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![)](rp.gif) ![)](rp.gif) |
25 | 21, 22, 24 | 3orbi123d 1251 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin
![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 19, 25 | imbi12d 311 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) fin ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 26 | imbi2d 307 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif)
fin
![<<](llangle.gif) ![n](_n.gif)
![k](_k.gif) fin ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
28 | | neeq1 2524 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
29 | | opkeq1 4059 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![>>](rrangle.gif) ![)](rp.gif) |
30 | 29 | eleq1d 2419 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![)](rp.gif) ![)](rp.gif) |
31 | | eqeq1 2359 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif)
1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
32 | | opkeq2 4060 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) ![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif) 1c![)](rp.gif) ![>>](rrangle.gif) ![)](rp.gif) |
33 | 32 | eleq1d 2419 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif) 1c![)](rp.gif) fin ![)](rp.gif) ![)](rp.gif) |
34 | 30, 31, 33 | 3orbi123d 1251 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif)
fin
![<<](llangle.gif) ![n](_n.gif)
![k](_k.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 28, 34 | imbi12d 311 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif)
fin
![<<](llangle.gif) ![n](_n.gif)
![k](_k.gif) fin ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 35 | imbi2d 307 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) fin ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | | neeq1 2524 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
38 | | opkeq1 4059 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) ![<<](llangle.gif) ![M](_cm.gif) ![n](_n.gif) ![>>](rrangle.gif) ![)](rp.gif) |
39 | 38 | eleq1d 2419 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![M](_cm.gif) ![n](_n.gif) fin ![)](rp.gif) ![)](rp.gif) |
40 | | eqeq1 2359 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
41 | | opkeq2 4060 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) ![<<](llangle.gif) ![n](_n.gif) ![M](_cm.gif) ![>>](rrangle.gif) ![)](rp.gif) |
42 | 41 | eleq1d 2419 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) |
43 | 39, 40, 42 | 3orbi123d 1251 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![n](_n.gif) fin
![<<](llangle.gif) ![n](_n.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 37, 43 | imbi12d 311 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![k](_k.gif) fin ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 44 | imbi2d 307 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![k](_k.gif) ![n](_n.gif)
fin
![<<](llangle.gif) ![n](_n.gif)
![k](_k.gif) fin ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
46 | | 0cminle 4461 |
. . . . . . . . . 10
![(](lp.gif) Nn 0c ![n](_n.gif)
fin ![)](rp.gif) |
47 | 46 | adantr 451 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn 0c ![(/)](varnothing.gif) 0c ![n](_n.gif) fin ![)](rp.gif) |
48 | | 0cex 4392 |
. . . . . . . . . . 11
0c
![_V](rmcv.gif) |
49 | | lefinlteq 4463 |
. . . . . . . . . . 11
![(](lp.gif) 0c Nn 0c ![(/)](varnothing.gif) ![(](lp.gif) 0c ![n](_n.gif)
fin ![(](lp.gif) 0c ![n](_n.gif) fin 0c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 48, 49 | mp3an1 1264 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn 0c ![(/)](varnothing.gif) ![(](lp.gif) 0c ![n](_n.gif)
fin ![(](lp.gif) 0c ![n](_n.gif) fin 0c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | | orcom 376 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 0c ![n](_n.gif)
fin 0c ![n](_n.gif)
0c
0c ![n](_n.gif) fin ![)](rp.gif) ![)](rp.gif) |
52 | 50, 51 | syl6bb 252 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn 0c ![(/)](varnothing.gif) ![(](lp.gif) 0c ![n](_n.gif)
fin 0c 0c ![n](_n.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | 47, 52 | mpbid 201 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn 0c ![(/)](varnothing.gif) 0c 0c ![n](_n.gif) fin ![)](rp.gif) ![)](rp.gif) |
54 | | 3mix2 1125 |
. . . . . . . . 9
0c ![(](lp.gif) 0c ![n](_n.gif) fin 0c ![<<](llangle.gif) ![n](_n.gif) 0c fin ![)](rp.gif) ![)](rp.gif) |
55 | | 3mix1 1124 |
. . . . . . . . 9
![(](lp.gif) 0c ![n](_n.gif) fin ![(](lp.gif) 0c ![n](_n.gif) fin 0c ![<<](llangle.gif) ![n](_n.gif) 0c fin ![)](rp.gif) ![)](rp.gif) |
56 | 54, 55 | jaoi 368 |
. . . . . . . 8
![(](lp.gif) 0c 0c ![n](_n.gif) fin ![(](lp.gif) 0c ![n](_n.gif) fin 0c ![<<](llangle.gif) ![n](_n.gif) 0c fin ![)](rp.gif) ![)](rp.gif) |
57 | 53, 56 | syl 15 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nn 0c ![(/)](varnothing.gif) ![(](lp.gif) 0c ![n](_n.gif)
fin 0c ![<<](llangle.gif) ![n](_n.gif) 0c fin ![)](rp.gif) ![)](rp.gif) |
58 | 57 | ex 423 |
. . . . . 6
![(](lp.gif) Nn 0c
![(](lp.gif) 0c ![n](_n.gif)
fin 0c ![<<](llangle.gif) ![n](_n.gif) 0c fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
59 | | addcnnul 4453 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif)
1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
60 | 59 | simpld 445 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) |
61 | 60 | 3ad2ant3 978 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
62 | | addc32 4416 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c
![(](lp.gif) ![(](lp.gif) 1c ![p](_p.gif) ![)](rp.gif) |
63 | 62 | eqeq2i 2363 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c
![(](lp.gif) ![(](lp.gif)
1c
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
64 | 63 | rexbii 2639 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif)
1c
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
65 | 64 | biimpi 186 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
66 | 65 | adantl 452 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c![)](rp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
67 | 66 | a1i 10 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif)
![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c![)](rp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
68 | | opkltfing 4449 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
69 | 68 | 3adant3 975 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
70 | | simp1 955 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) Nn ![)](rp.gif) |
71 | | peano2 4403 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) |
72 | 70, 71 | syl 15 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) 1c Nn ![)](rp.gif) |
73 | | simp2 956 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) Nn ![)](rp.gif) |
74 | | opklefing 4448 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif)
1c
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
75 | 72, 73, 74 | syl2anc 642 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif)
1c
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
76 | 67, 69, 75 | 3imtr4d 259 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif)
fin ![)](rp.gif) ![)](rp.gif) |
77 | | lefinlteq 4463 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif)
fin ![(](lp.gif)
1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
78 | 71, 77 | syl3an1 1215 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif)
fin ![(](lp.gif)
1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
79 | 76, 78 | sylibd 205 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) fin ![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
80 | | 3mix1 1124 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) |
81 | | 3mix2 1125 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif)
fin ![(](lp.gif)
1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif) 1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) |
82 | 80, 81 | jaoi 368 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) 1c ![n](_n.gif) ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) |
83 | 79, 82 | syl6 29 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
84 | | ltfinp1 4462 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![<<](llangle.gif) ![m](_m.gif) ![(](lp.gif) 1c![)](rp.gif) fin ![)](rp.gif) |
85 | 60, 84 | sylan2 460 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![<<](llangle.gif) ![m](_m.gif) ![(](lp.gif) 1c![)](rp.gif) fin ![)](rp.gif) |
86 | 85 | 3adant2 974 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![<<](llangle.gif) ![m](_m.gif) ![(](lp.gif) 1c![)](rp.gif) fin ![)](rp.gif) |
87 | | opkeq1 4059 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![(](lp.gif) 1c![)](rp.gif) ![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif) 1c![)](rp.gif) ![>>](rrangle.gif) ![)](rp.gif) |
88 | 87 | eleq1d 2419 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![(](lp.gif) 1c![)](rp.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) |
89 | 86, 88 | syl5ibcom 211 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif)
![<<](llangle.gif) ![n](_n.gif)
![(](lp.gif) 1c![)](rp.gif) fin ![)](rp.gif) ![)](rp.gif) |
90 | | 3mix3 1126 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif) 1c![)](rp.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) |
91 | 89, 90 | syl6 29 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif)
fin ![(](lp.gif)
1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif) 1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
92 | | ltfintr 4459 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![<<](llangle.gif) ![m](_m.gif) ![(](lp.gif) 1c![)](rp.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) |
93 | 73, 70, 72, 92 | syl3anc 1182 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![<<](llangle.gif) ![m](_m.gif) ![(](lp.gif) 1c![)](rp.gif)
fin ![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif) 1c![)](rp.gif) fin ![)](rp.gif) ![)](rp.gif) |
94 | 86, 93 | mpan2d 655 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif) 1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) |
95 | 94, 90 | syl6 29 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
96 | 83, 91, 95 | 3jaod 1246 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
97 | 61, 96 | embantd 50 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
98 | 97 | 3expia 1153 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
99 | 98 | com23 72 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
100 | 99 | ex 423 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
101 | 100 | a2d 23 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![m](_m.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![m](_m.gif) fin ![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) 1c
![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) fin ![(](lp.gif) 1c
![<<](llangle.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif)
fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
102 | 9, 18, 27, 36, 45, 58, 101 | finds 4411 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
103 | 102 | com12 27 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![n](_n.gif) fin ![<<](llangle.gif) ![n](_n.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
104 | 8, 103 | vtoclga 2920 |
. . 3
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
105 | 104 | com12 27 |
. 2
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
106 | 105 | 3imp 1145 |
1
![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) |