Description: Obsolete proof of prstcleval as of 12-Nov-2024. Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | prstcnid.c | No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |- | |
prstcnid.k | |
||
prstcle.l | |
||
Assertion | prstclevalOLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prstcnid.c | Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |- | |
2 | prstcnid.k | |
|
3 | prstcle.l | |
|
4 | pleid | |
|
5 | 10re | |
|
6 | 1nn0 | |
|
7 | 0nn0 | |
|
8 | 5nn | |
|
9 | 8 | nngt0i | |
10 | 6 7 8 9 | declt | |
11 | 5 10 | ltneii | |
12 | plendx | |
|
13 | ccondx | |
|
14 | 12 13 | neeq12i | |
15 | 11 14 | mpbir | |
16 | 4nn | |
|
17 | 16 | nngt0i | |
18 | 6 7 16 17 | declt | |
19 | 5 18 | ltneii | |
20 | homndx | |
|
21 | 12 20 | neeq12i | |
22 | 19 21 | mpbir | |
23 | 1 2 4 15 22 | prstcnid | |
24 | 3 23 | eqtrd | |