Home | Metamath
Proof Explorer Theorem List (p. 294 of 309) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-30843) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemefs32fva1 29301* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 29-Mar-2013.) |
Theorem | cdlemefs31fv1 29302* |
Value of when .
TODO This may be useful for shortening others that now use riotasv 6238
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 29303* | 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 29304* | Value of f_{s}(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 29307 instead TODO FIX COMMENT (Contributed by NM, 31-Mar-2013.) |
Theorem | cdlemefr45 29305* | 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 29306* | Explicit expansion of cdlemefr45 29305. TODO: use to shorten cdlemefr45 29305 uses? TODO FIX COMMENT (Contributed by NM, 10-Apr-2013.) |
Theorem | cdlemefs45 29307* | Value of f_{s}(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 29308* | Explicit expansion of cdlemefs45 29307. TODO: use to shorten cdlemefs45 29307 uses? Should be assigned to a hypothesis letter? TODO FIX COMMENT (Contributed by NM, 10-Apr-2013.) |
Theorem | cdlemefs45eN 29309* | Explicit expansion of cdlemefs45 29307. TODO: use to shorten cdlemefs45 29307 uses? TODO FIX COMMENT (Contributed by NM, 10-Apr-2013.) (New usage is discouraged.) |
Theorem | cdleme32sn1awN 29310* | Show that is an atom not under when . (Contributed by NM, 6-Mar-2013.) (New usage is discouraged.) |
Theorem | cdleme41sn3a 29311* | Show that is under when . (Contributed by NM, 19-Mar-2013.) |
Theorem | cdleme32sn2awN 29312* | Show that is an atom not under when . (Contributed by NM, 6-Mar-2013.) (New usage is discouraged.) |
Theorem | cdleme32snaw 29313* | Show that is an atom not under . (Contributed by NM, 6-Mar-2013.) |
Theorem | cdleme32snb 29314* | Show closure of . (Contributed by NM, 1-Mar-2013.) |
Theorem | cdleme32fva 29315* | 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 29316* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Mar-2013.) |
Theorem | cdleme32fvaw 29317* | Show that is an atom not under when is an atom not under . (Contributed by NM, 18-Apr-2013.) |
Theorem | cdleme32fvcl 29318* | Part of proof of Lemma D in [Crawley] p. 113. Closure of the function . (Contributed by NM, 10-Feb-2013.) |
Theorem | cdleme32a 29319* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
Theorem | cdleme32b 29320* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
Theorem | cdleme32c 29321* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
Theorem | cdleme32d 29322* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
Theorem | cdleme32e 29323* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
Theorem | cdleme32f 29324* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
Theorem | cdleme32le 29325* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
Theorem | cdleme35a 29326 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35fnpq 29327 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.) |
Theorem | cdleme35b 29328 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35c 29329 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35d 29330 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35e 29331 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35f 29332 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35g 29333 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35h 29334 | 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 29335 | 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 29336* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of line case; compare cdleme32sn2awN 29312. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.) |
Theorem | cdleme35sn3a 29337* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.) |
Theorem | cdleme36a 29338 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.) |
Theorem | cdleme36m 29339 | 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 29340 | 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 29341 | 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 29342 | 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 29339 and cdleme37m 29340? (Contributed by NM, 14-Mar-2013.) |
Theorem | cdleme39a 29343 | 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), f_{t}(), f_{t}(). Put hypotheses of cdleme38n 29342 in convention of cdleme32sn1awN 29310. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.) |
Theorem | cdleme39n 29344 | 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), f_{t}(), f_{t}(). Put hypotheses of cdleme38n 29342 in convention of cdleme32sn1awN 29310. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.) |
Theorem | cdleme40m 29345* | 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 29310. (Contributed by NM, 18-Mar-2013.) |
Theorem | cdleme40n 29346* | 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 29347* | 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 29348* | Part of proof of Lemma E in [Crawley] p. 113. Apply cdleme40v 29347 bound variable change to . TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.) |
Theorem | cdleme42a 29349 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 3-Mar-2013.) |
Theorem | cdleme42c 29350 | Part of proof of Lemma E in [Crawley] p. 113. Match . (Contributed by NM, 6-Mar-2013.) |
Theorem | cdleme42d 29351 | Part of proof of Lemma E in [Crawley] p. 113. Match . (Contributed by NM, 6-Mar-2013.) |
Theorem | cdleme41sn3aw 29352* | 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 29353* | 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 29354* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for combined cases; compare cdleme32snaw 29313. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.) |
Theorem | cdleme41fva11 29355* | 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 29356* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 6-Mar-2013.) |
Theorem | cdleme42e 29357* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
Theorem | cdleme42f 29358* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |