HomeTheorem List (p. 340 of 402)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 340 of 402) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-26513) |
Hilbert Space Explorer
(26514-28036) |
Users' Mathboxes
(28037-40133) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdlemefs32fvaN 33901* |
Part of proof of Lemma E in [Crawley] p. 113.
Value of  at an atom
not under  .
TODO: FIX COMMENT. TODO: consolidate uses of
lhpmat 33507 here and elsewhere, and presence/absence of
       term. Also, why can proof
be shortened with
cdleme27cl 33845? What is difference from cdlemefs27cl 33892? (Contributed
by NM, 29-Mar-2013.) (New usage is discouraged.)
|
       
 ![./\](_.wedge.gif "./\"){kind=small}
     
 
  
   ![/\](wedge.gif "/\"){kind=small}
 
  
  
 
  ![]_](_urbrack.gif "]_"){kind=small}
| ||
| Theorem | cdlemefs32fva1 33902* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
| ||
| Theorem | cdlemefs31fv1 33903* |
Value of when .
TODO This may be useful for shortening others that now use riotasv 32443
3d . TODO: FIX COMMENT.
***END OF VALUE AT ATOM STUFF TO REPLACE
ONES BELOW***
"cdleme3xsn1aw" decreased using "cdlemefs32sn1aw"
"cdleme32sn1aw" decreased from 3302 to 36 using "cdlemefs32sn1aw".
"cdleme32sn2aw" decreased from 1687 to 26 using "cdlemefr32sn2aw".
"cdleme32snaw" decreased from 376 to 375 using "cdlemefs32sn1aw".
"cdleme32snaw" decreased from 375 to 368 using "cdlemefr32sn2aw".
"cdleme35sn3a" decreased from 547 to 523 using "cdleme43frv1sn".
(Contributed by NM, 27-Mar-2013.)
|
 
| ||
| Theorem | cdlemefr44 33904* | Value of f(r) when r is an atom not under pq, using more compact hypotheses. TODO: eliminate and use cdlemefr45 instead? TODO: FIX COMMENT. (Contributed by NM, 31-Mar-2013.) |
|
| ||
| Theorem | cdlemefs44 33905* | Value of fs(r) when r is an atom under pq and s is any atom not under pq, using more compact hypotheses. TODO: eliminate and use cdlemefs45 33908 instead TODO: FIX COMMENT. (Contributed by NM, 31-Mar-2013.) |
|
| ||
| Theorem | cdlemefr45 33906* | Value of f(r) when r is an atom not under pq, using very compact hypotheses. TODO: FIX COMMENT. (Contributed by NM, 1-Apr-2013.) |
|
| ||
| Theorem | cdlemefr45e 33907* | Explicit expansion of cdlemefr45 33906. TODO: use to shorten cdlemefr45 33906 uses? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) |
|
| ||
| Theorem | cdlemefs45 33908* | Value of fs(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO: FIX COMMENT. (Contributed by NM, 1-Apr-2013.) |
|
| ||
| Theorem | cdlemefs45ee 33909* |
Explicit expansion of cdlemefs45 33908. TODO: use to shorten cdlemefs45 33908
uses? Should
be
assigned to a hypothesis letter? TODO: FIX COMMENT. (Contributed by
NM, 10-Apr-2013.)
|
|
| ||
| Theorem | cdlemefs45eN 33910* | Explicit expansion of cdlemefs45 33908. TODO: use to shorten cdlemefs45 33908 uses? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme32sn1awN 33911* |
Show that is an atom
not under when
. (Contributed by NM,
6-Mar-2013.)
(New usage is discouraged.)
|
|
| ||
| Theorem | cdleme41sn3a 33912* |
Show that is under
when
. (Contributed by NM,
19-Mar-2013.)
|
|
| ||
| Theorem | cdleme32sn2awN 33913* |
Show that is an atom
not under when
. (Contributed by NM, 6-Mar-2013.)
(New usage is discouraged.)
|
|
| ||
| Theorem | cdleme32snaw 33914* |
Show that is an atom
not under .
(Contributed
by NM, 6-Mar-2013.)
|
|
| ||
| Theorem | cdleme32snb 33915* |
Show closure of .
(Contributed by NM, 1-Mar-2013.)
|
|
| ||
| Theorem | cdleme32fva 33916* |
Part of proof of Lemma D in [Crawley] p. 113.
Value of at an atom
not under .
(Contributed by NM, 2-Mar-2013.)
|
|
| ||
| Theorem | cdleme32fva1 33917* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Mar-2013.) |
|
| ||
| Theorem | cdleme32fvaw 33918* |
Show that is
an atom not under
when is an
atom not under . (Contributed by NM, 18-Apr-2013.)
|
|
| ||
| Theorem | cdleme32fvcl 33919* |
Part of proof of Lemma D in [Crawley] p. 113.
Closure of the function
. (Contributed
by NM, 10-Feb-2013.)
|
| ||
| Theorem | cdleme32a 33920* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
|
| ||
| Theorem | cdleme32b 33921* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
|
| ||
| Theorem | cdleme32c 33922* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
|
| ||
| Theorem | cdleme32d 33923* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
|
| ||
| Theorem | cdleme32e 33924* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
|
| ||
| Theorem | cdleme32f 33925* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
|
| ||
| Theorem | cdleme32le 33926* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
|
| ||
| Theorem | cdleme35a 33927 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35fnpq 33928 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
|
| ||
| Theorem | cdleme35b 33929 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35c 33930 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35d 33931 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35e 33932 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35f 33933 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35g 33934 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35h 33935 |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(x) is
one-to-one outside of line. TODO: FIX COMMENT.
(Contributed by NM, 11-Mar-2013.)
|
| ||
| Theorem | cdleme35h2 33936 |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(x) is
one-to-one outside of line. TODO: FIX COMMENT.
(Contributed by NM, 18-Mar-2013.)
|
|
| ||
| Theorem | cdleme35sn2aw 33937* |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(x) is
one-to-one outside of line case; compare cdleme32sn2awN 33913.
TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013.)
|
|
| ||
| Theorem | cdleme35sn3a 33938* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
|
| ||
| Theorem | cdleme36a 33939 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 11-Mar-2013.) |
|
| ||
| Theorem | cdleme36m 33940 |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(x) is
one-to-one on
line. TODO: FIX COMMENT.
(Contributed by NM,
11-Mar-2013.)
|
| ||
| Theorem | cdleme37m 33941 |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(x) is
one-to-one on
line. TODO: FIX COMMENT.
(Contributed by NM,
13-Mar-2013.)
|
| ||
| Theorem | cdleme38m 33942 |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(x) is
one-to-one on
line. TODO: FIX COMMENT.
(Contributed by NM,
13-Mar-2013.)
|
|
| ||
| Theorem | cdleme38n 33943 |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(x) is
one-to-one on
line. TODO: FIX COMMENT.
TODO shorter if
proved directly from cdleme36m 33940 and cdleme37m 33941? (Contributed by NM,
14-Mar-2013.)
|
|
| ||
| Theorem | cdleme39a 33944 |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(x) is
one-to-one on line. TODO: FIX COMMENT.
, ,
, serve as f(t), f(u),
ft(), ft(). Put
hypotheses of cdleme38n 33943 in convention of cdleme32sn1awN 33911. TODO
see if this hypothesis conversion would be better if done earlier.
(Contributed by NM, 15-Mar-2013.)
|
|
| ||
| Theorem | cdleme39n 33945 |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(x) is
one-to-one on
line. TODO: FIX COMMENT.
, ,
, serve as f(t), f(u),
ft(), ft(). Put
hypotheses of cdleme38n 33943 in convention of cdleme32sn1awN 33911. TODO see
if this hypothesis conversion would be better if done earlier.
(Contributed by NM, 15-Mar-2013.)
|
|
| ||
| Theorem | cdleme40m 33946* |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(x) is
one-to-one on line. TODO: FIX COMMENT
Use proof idea
from cdleme32sn1awN 33911. (Contributed by NM, 18-Mar-2013.)
|
 
| ||
| Theorem | cdleme40n 33947* |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(x) is
one-to-one on line. TODO: FIX COMMENT.
TODO get rid
of '.<' class? (Contributed by NM, 18-Mar-2013.)
|
| ||
| Theorem | cdleme40v 33948* |
Part of proof of Lemma E in [Crawley] p. 113.
Change bound variables
in (but we
use for
convenience
since we have its hypotheses available) . (Contributed by NM,
18-Mar-2013.)
|
|
| ||
| Theorem | cdleme40w 33949* |
Part of proof of Lemma E in [Crawley] p. 113.
Apply cdleme40v 33948 bound
variable change to .
TODO: FIX COMMENT. (Contributed
by NM, 19-Mar-2013.)
|
|
| ||
| Theorem | cdleme42a 33950 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 3-Mar-2013.) |
|
| ||
| Theorem | cdleme42c 33951 |
Part of proof of Lemma E in [Crawley] p. 113.
Match .
(Contributed by NM, 6-Mar-2013.)
|
|
| ||
| Theorem | cdleme42d 33952 |
Part of proof of Lemma E in [Crawley] p. 113.
Match
. (Contributed by NM, 6-Mar-2013.)
|
|
| ||
| Theorem | cdleme41sn3aw 33953* |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(r) is
different on and off the line. TODO: FIX COMMENT.
(Contributed by NM, 18-Mar-2013.)
|
|
| ||
| Theorem | cdleme41sn4aw 33954* |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(r) is for on
and off line. TODO: FIX COMMENT. (Contributed
by NM,
19-Mar-2013.)
|
|
| ||
| Theorem | cdleme41snaw 33955* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for combined cases; compare cdleme32snaw 33914. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013.) |
|
| ||
| Theorem | cdleme41fva11 33956* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is one-to-one for r in W (r an atom not under w). TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
|
| ||
| Theorem | cdleme42b 33957* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 6-Mar-2013.) |
|
| ||
| Theorem | cdleme42e 33958* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
|
| ||