Home | Metamath
Proof Explorer Theorem List (p. 316 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fprodeq02 31501* | If one of the factors is zero the product is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
โข (๐ = ๐พ โ ๐ต = ๐ถ) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐พ โ ๐ด) & โข (๐ โ ๐ถ = 0) โ โข (๐ โ โ๐ โ ๐ด ๐ต = 0) | ||
Theorem | pr01ssre 31502 | The range of the indicator function is a subset of โ. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
โข {0, 1} โ โ | ||
Theorem | fprodex01 31503* | A product of factors equal to zero or one is zero exactly when one of the factors is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
โข (๐ = ๐ โ ๐ต = ๐ถ) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ {0, 1}) โ โข (๐ โ โ๐ โ ๐ด ๐ต = if(โ๐ โ ๐ด ๐ถ = 1, 1, 0)) | ||
Theorem | prodpr 31504* | A product over a pair is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
โข (๐ = ๐ด โ ๐ท = ๐ธ) & โข (๐ = ๐ต โ ๐ท = ๐น) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐ธ โ โ) & โข (๐ โ ๐น โ โ) & โข (๐ โ ๐ด โ ๐ต) โ โข (๐ โ โ๐ โ {๐ด, ๐ต}๐ท = (๐ธ ยท ๐น)) | ||
Theorem | prodtp 31505* | A product over a triple is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
โข (๐ = ๐ด โ ๐ท = ๐ธ) & โข (๐ = ๐ต โ ๐ท = ๐น) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐ธ โ โ) & โข (๐ โ ๐น โ โ) & โข (๐ โ ๐ด โ ๐ต) & โข (๐ = ๐ถ โ ๐ท = ๐บ) & โข (๐ โ ๐ถ โ ๐) & โข (๐ โ ๐บ โ โ) & โข (๐ โ ๐ด โ ๐ถ) & โข (๐ โ ๐ต โ ๐ถ) โ โข (๐ โ โ๐ โ {๐ด, ๐ต, ๐ถ}๐ท = ((๐ธ ยท ๐น) ยท ๐บ)) | ||
Theorem | fsumub 31506* | An upper bound for a term of a positive finite sum. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
โข (๐ = ๐พ โ ๐ต = ๐ท) & โข (๐ โ ๐ด โ Fin) & โข (๐ โ ฮฃ๐ โ ๐ด ๐ต = ๐ถ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ+) & โข (๐ โ ๐พ โ ๐ด) โ โข (๐ โ ๐ท โค ๐ถ) | ||
Theorem | fsumiunle 31507* | Upper bound for a sum of nonnegative terms over an indexed union. The inequality may be strict if the indexed union is non-disjoint, since in the right hand side, a summand may be counted several times. (Contributed by Thierry Arnoux, 1-Jan-2021.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ Fin) & โข (((๐ โง ๐ฅ โ ๐ด) โง ๐ โ ๐ต) โ ๐ถ โ โ) & โข (((๐ โง ๐ฅ โ ๐ด) โง ๐ โ ๐ต) โ 0 โค ๐ถ) โ โข (๐ โ ฮฃ๐ โ โช ๐ฅ โ ๐ด ๐ต๐ถ โค ฮฃ๐ฅ โ ๐ด ฮฃ๐ โ ๐ต ๐ถ) | ||
Theorem | dfdec100 31508 | Split the hundreds from a decimal value. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ โ โข ;;๐ด๐ต๐ถ = ((;;100 ยท ๐ด) + ;๐ต๐ถ) | ||
Define a decimal expansion constructor. The decimal expansions built with this constructor are not meant to be used alone outside of this chapter. Rather, they are meant to be used exclusively as part of a decimal number with a decimal fraction, for example (3._1_4_1_59). That decimal point operator is defined in the next section. The bulk of these constructions have originally been proposed by David A. Wheeler on 12-May-2015, and discussed with Mario Carneiro in this thread: https://groups.google.com/g/metamath/c/2AW7T3d2YiQ. | ||
Syntax | cdp2 31509 | Constant used for decimal fraction constructor. See df-dp2 31510. |
class _๐ด๐ต | ||
Definition | df-dp2 31510 | Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12552. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.) |
โข _๐ด๐ต = (๐ด + (๐ต / ;10)) | ||
Theorem | dp2eq1 31511 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
โข (๐ด = ๐ต โ _๐ด๐ถ = _๐ต๐ถ) | ||
Theorem | dp2eq2 31512 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
โข (๐ด = ๐ต โ _๐ถ๐ด = _๐ถ๐ต) | ||
Theorem | dp2eq1i 31513 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
โข ๐ด = ๐ต โ โข _๐ด๐ถ = _๐ต๐ถ | ||
Theorem | dp2eq2i 31514 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
โข ๐ด = ๐ต โ โข _๐ถ๐ด = _๐ถ๐ต | ||
Theorem | dp2eq12i 31515 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
โข ๐ด = ๐ต & โข ๐ถ = ๐ท โ โข _๐ด๐ถ = _๐ต๐ท | ||
Theorem | dp20u 31516 | Add a zero in the tenths (lower) place. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 โ โข _๐ด0 = ๐ด | ||
Theorem | dp20h 31517 | Add a zero in the unit places. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ+ โ โข _0๐ด = (๐ด / ;10) | ||
Theorem | dp2cl 31518 | Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ _๐ด๐ต โ โ) | ||
Theorem | dp2clq 31519 | Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ โ โข _๐ด๐ต โ โ | ||
Theorem | rpdp2cl 31520 | Closure for a decimal fraction in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ โ โข _๐ด๐ต โ โ+ | ||
Theorem | rpdp2cl2 31521 | Closure for a decimal fraction with no decimal expansion in the positive real numbers. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
โข ๐ด โ โ โ โข _๐ด0 โ โ+ | ||
Theorem | dp2lt10 31522 | Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ & โข ๐ด < ;10 & โข ๐ต < ;10 โ โข _๐ด๐ต < ;10 | ||
Theorem | dp2lt 31523 | Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ & โข ๐ถ โ โ+ & โข ๐ต < ๐ถ โ โข _๐ด๐ต < _๐ด๐ถ | ||
Theorem | dp2ltsuc 31524 | Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ & โข ๐ต < ;10 & โข (๐ด + 1) = ๐ถ โ โข _๐ด๐ต < ๐ถ | ||
Theorem | dp2ltc 31525 | Comparing two decimal expansions (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ & โข ๐ถ โ โ0 & โข ๐ท โ โ+ & โข ๐ต < ;10 & โข ๐ด < ๐ถ โ โข _๐ด๐ต < _๐ถ๐ท | ||
Define the decimal point operator and the decimal fraction constructor. This can model traditional decimal point notation, and serve as a convenient way to write some fractional numbers. See df-dp 31527 and df-dp2 31510 for more information; dpval2 31531 and dpfrac1 31530 provide a more convenient way to obtain a value. This is intentionally similar to df-dec 12552. | ||
Syntax | cdp 31526 | Decimal point operator. See df-dp 31527. |
class . | ||
Definition | df-dp 31527* |
Define the . (decimal point) operator. For example,
(1.5) = (3 / 2), and
-(;32._7_18) =
-(;;;;32718 / ;;;1000)
Unary minus, if applied, should normally be applied in front of the
parentheses.
Metamath intentionally does not have a built-in construct for numbers, so it can show that numbers are something you can build based on set theory. However, that means that Metamath has no built-in way to parse and handle decimal numbers as traditionally written, e.g., "2.54". Here we create a system for modeling traditional decimal point notation; it is not syntactically identical, but it is sufficiently similar so it is a reasonable model of decimal point notation. It should also serve as a convenient way to write some fractional numbers. The RHS is โ, not โ; this should simplify some proofs. The LHS is โ0, since that is what is used in practice. The definition intentionally does not allow negative numbers on the LHS; if it did, nonzero fractions would produce the wrong results. (It would be possible to define the decimal point to do this, but using it would be more complicated, and the expression -(๐ด.๐ต) is just as convenient.) (Contributed by David A. Wheeler, 15-May-2015.) |
โข . = (๐ฅ โ โ0, ๐ฆ โ โ โฆ _๐ฅ๐ฆ) | ||
Theorem | dpval 31528 | Define the value of the decimal point operator. See df-dp 31527. (Contributed by David A. Wheeler, 15-May-2015.) |
โข ((๐ด โ โ0 โง ๐ต โ โ) โ (๐ด.๐ต) = _๐ด๐ต) | ||
Theorem | dpcl 31529 | Prove that the closure of the decimal point is โ as we have defined it. See df-dp 31527. (Contributed by David A. Wheeler, 15-May-2015.) |
โข ((๐ด โ โ0 โง ๐ต โ โ) โ (๐ด.๐ต) โ โ) | ||
Theorem | dpfrac1 31530 | Prove a simple equivalence involving the decimal point. See df-dp 31527 and dpcl 31529. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.) |
โข ((๐ด โ โ0 โง ๐ต โ โ) โ (๐ด.๐ต) = (;๐ด๐ต / ;10)) | ||
Theorem | dpval2 31531 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ โ โข (๐ด.๐ต) = (๐ด + (๐ต / ;10)) | ||
Theorem | dpval3 31532 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ โ โข (๐ด.๐ต) = _๐ด๐ต | ||
Theorem | dpmul10 31533 | Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ โ โข ((๐ด.๐ต) ยท ;10) = ;๐ด๐ต | ||
Theorem | decdiv10 31534 | Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ โ โข (;๐ด๐ต / ;10) = (๐ด.๐ต) | ||
Theorem | dpmul100 31535 | Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ โ โข ((๐ด._๐ต๐ถ) ยท ;;100) = ;;๐ด๐ต๐ถ | ||
Theorem | dp3mul10 31536 | Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ โ โข ((๐ด._๐ต๐ถ) ยท ;10) = (;๐ด๐ต.๐ถ) | ||
Theorem | dpmul1000 31537 | Multiply by 1000 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ โ โข ((๐ด._๐ต_๐ถ๐ท) ยท ;;;1000) = ;;;๐ด๐ต๐ถ๐ท | ||
Theorem | dpval3rp 31538 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ โ โข (๐ด.๐ต) = _๐ด๐ต | ||
Theorem | dp0u 31539 | Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 โ โข (๐ด.0) = ๐ด | ||
Theorem | dp0h 31540 | Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ+ โ โข (0.๐ด) = (๐ด / ;10) | ||
Theorem | rpdpcl 31541 | Closure of the decimal point in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ โ โข (๐ด.๐ต) โ โ+ | ||
Theorem | dplt 31542 | Comparing two decimal expansions (equal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ & โข ๐ถ โ โ+ & โข ๐ต < ๐ถ โ โข (๐ด.๐ต) < (๐ด.๐ถ) | ||
Theorem | dplti 31543 | Comparing a decimal expansions with the next higher integer. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ & โข ๐ถ โ โ0 & โข ๐ต < ;10 & โข (๐ด + 1) = ๐ถ โ โข (๐ด.๐ต) < ๐ถ | ||
Theorem | dpgti 31544 | Comparing a decimal expansions with the next lower integer. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ โ โข ๐ด < (๐ด.๐ต) | ||
Theorem | dpltc 31545 | Comparing two decimal integers (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ & โข ๐ถ โ โ0 & โข ๐ท โ โ+ & โข ๐ด < ๐ถ & โข ๐ต < ;10 โ โข (๐ด.๐ต) < (๐ถ.๐ท) | ||
Theorem | dpexpp1 31546 | Add one zero to the mantisse, and a one to the exponent in a scientific notation. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ & โข (๐ + 1) = ๐ & โข ๐ โ โค & โข ๐ โ โค โ โข ((๐ด.๐ต) ยท (;10โ๐)) = ((0._๐ด๐ต) ยท (;10โ๐)) | ||
Theorem | 0dp2dp 31547 | Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ โ โข ((0._๐ด๐ต) ยท ;10) = (๐ด.๐ต) | ||
Theorem | dpadd2 31548 | Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ+ & โข ๐ถ โ โ0 & โข ๐ท โ โ+ & โข ๐ธ โ โ0 & โข ๐น โ โ+ & โข ๐บ โ โ0 & โข ๐ป โ โ0 & โข (๐บ + ๐ป) = ๐ผ & โข ((๐ด.๐ต) + (๐ถ.๐ท)) = (๐ธ.๐น) โ โข ((๐บ._๐ด๐ต) + (๐ป._๐ถ๐ท)) = (๐ผ._๐ธ๐น) | ||
Theorem | dpadd 31549 | Addition with one decimal. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ธ โ โ0 & โข ๐น โ โ0 & โข (;๐ด๐ต + ;๐ถ๐ท) = ;๐ธ๐น โ โข ((๐ด.๐ต) + (๐ถ.๐ท)) = (๐ธ.๐น) | ||
Theorem | dpadd3 31550 | Addition with two decimals. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ธ โ โ0 & โข ๐บ โ โ0 & โข ๐น โ โ0 & โข ๐ป โ โ0 & โข ๐ผ โ โ0 & โข (;;๐ด๐ต๐ถ + ;;๐ท๐ธ๐น) = ;;๐บ๐ป๐ผ โ โข ((๐ด._๐ต๐ถ) + (๐ท._๐ธ๐น)) = (๐บ._๐ป๐ผ) | ||
Theorem | dpmul 31551 | Multiplication with one decimal point. (Contributed by Thierry Arnoux, 26-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ธ โ โ0 & โข ๐บ โ โ0 & โข ๐ฝ โ โ0 & โข ๐พ โ โ0 & โข (๐ด ยท ๐ถ) = ๐น & โข (๐ด ยท ๐ท) = ๐ & โข (๐ต ยท ๐ถ) = ๐ฟ & โข (๐ต ยท ๐ท) = ;๐ธ๐พ & โข ((๐ฟ + ๐) + ๐ธ) = ;๐บ๐ฝ & โข (๐น + ๐บ) = ๐ผ โ โข ((๐ด.๐ต) ยท (๐ถ.๐ท)) = (๐ผ._๐ฝ๐พ) | ||
Theorem | dpmul4 31552 | An upper bound to multiplication of decimal numbers with 4 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ธ โ โ0 & โข ๐บ โ โ0 & โข ๐ฝ โ โ0 & โข ๐พ โ โ0 & โข ๐น โ โ0 & โข ๐ป โ โ0 & โข ๐ผ โ โ0 & โข ๐ฟ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ < ;10 & โข ๐ < ;10 & โข ๐ < ;10 & โข (;;๐ฟ๐๐ + ๐) = ;;;๐ ๐๐๐ & โข ((๐ด.๐ต) ยท (๐ธ.๐น)) = (๐ผ._๐ฝ๐พ) & โข ((๐ถ.๐ท) ยท (๐บ.๐ป)) = (๐._๐๐) & โข (;;;๐ผ๐ฝ๐พ1 + ;;๐ ๐๐) = ;;;๐๐๐๐ & โข (((๐ด.๐ต) + (๐ถ.๐ท)) ยท ((๐ธ.๐น) + (๐บ.๐ป))) = (((๐ผ._๐ฝ๐พ) + (๐ฟ._๐๐)) + (๐._๐๐)) โ โข ((๐ด._๐ต_๐ถ๐ท) ยท (๐ธ._๐น_๐บ๐ป)) < (๐._๐_๐๐) | ||
Theorem | threehalves 31553 | Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
โข (3 / 2) = (1.5) | ||
Theorem | 1mhdrd 31554 | Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
โข ((0._99) + (0._01)) = 1 | ||
Syntax | cxdiv 31555 | Extend class notation to include division of extended reals. |
class /๐ | ||
Definition | df-xdiv 31556* | Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
โข /๐ = (๐ฅ โ โ*, ๐ฆ โ (โ โ {0}) โฆ (โฉ๐ง โ โ* (๐ฆ ยทe ๐ง) = ๐ฅ)) | ||
Theorem | xdivval 31557* | Value of division: the (unique) element ๐ฅ such that (๐ต ยท ๐ฅ) = ๐ด. This is meaningful only when ๐ต is nonzero. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
โข ((๐ด โ โ* โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด /๐ ๐ต) = (โฉ๐ฅ โ โ* (๐ต ยทe ๐ฅ) = ๐ด)) | ||
Theorem | xrecex 31558* | Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ โ๐ฅ โ โ (๐ด ยทe ๐ฅ) = 1) | ||
Theorem | xmulcand 31559 | Cancellation law for extended multiplication. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ถ โ 0) โ โข (๐ โ ((๐ถ ยทe ๐ด) = (๐ถ ยทe ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | xreceu 31560* | Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
โข ((๐ด โ โ* โง ๐ต โ โ โง ๐ต โ 0) โ โ!๐ฅ โ โ* (๐ต ยทe ๐ฅ) = ๐ด) | ||
Theorem | xdivcld 31561 | Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ (๐ด /๐ ๐ต) โ โ*) | ||
Theorem | xdivcl 31562 | Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
โข ((๐ด โ โ* โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด /๐ ๐ต) โ โ*) | ||
Theorem | xdivmul 31563 | Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ด /๐ ๐ถ) = ๐ต โ (๐ถ ยทe ๐ต) = ๐ด)) | ||
Theorem | rexdiv 31564 | The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด /๐ ๐ต) = (๐ด / ๐ต)) | ||
Theorem | xdivrec 31565 | Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
โข ((๐ด โ โ* โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด /๐ ๐ต) = (๐ด ยทe (1 /๐ ๐ต))) | ||
Theorem | xdivid 31566 | A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ (๐ด /๐ ๐ด) = 1) | ||
Theorem | xdiv0 31567 | Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ (0 /๐ ๐ด) = 0) | ||
Theorem | xdiv0rp 31568 | Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
โข (๐ด โ โ+ โ (0 /๐ ๐ด) = 0) | ||
Theorem | eliccioo 31569 | Membership in a closed interval of extended reals versus the same open interval. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ด โค ๐ต) โ (๐ถ โ (๐ด[,]๐ต) โ (๐ถ = ๐ด โจ ๐ถ โ (๐ด(,)๐ต) โจ ๐ถ = ๐ต))) | ||
Theorem | elxrge02 31570 | Elementhood in the set of nonnegative extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
โข (๐ด โ (0[,]+โ) โ (๐ด = 0 โจ ๐ด โ โ+ โจ ๐ด = +โ)) | ||
Theorem | xdivpnfrp 31571 | Plus infinity divided by a positive real number is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
โข (๐ด โ โ+ โ (+โ /๐ ๐ด) = +โ) | ||
Theorem | rpxdivcld 31572 | Closure law for extended division of positive reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด /๐ ๐ต) โ โ+) | ||
Theorem | xrpxdivcld 31573 | Closure law for extended division of positive extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
โข (๐ โ ๐ด โ (0[,]+โ)) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด /๐ ๐ต) โ (0[,]+โ)) | ||
Theorem | wrdfd 31574 | A word is a zero-based sequence with a recoverable upper limit, deduction version. (Contributed by Thierry Arnoux, 22-Dec-2021.) |
โข (๐ โ ๐ = (โฏโ๐)) & โข (๐ โ ๐ โ Word ๐) โ โข (๐ โ ๐:(0..^๐)โถ๐) | ||
Theorem | wrdres 31575 | Condition for the restriction of a word to be a word itself. (Contributed by Thierry Arnoux, 5-Oct-2018.) |
โข ((๐ โ Word ๐ โง ๐ โ (0...(โฏโ๐))) โ (๐ โพ (0..^๐)) โ Word ๐) | ||
Theorem | wrdsplex 31576* | Existence of a split of a word at a given index. (Contributed by Thierry Arnoux, 11-Oct-2018.) (Proof shortened by AV, 3-Nov-2022.) |
โข ((๐ โ Word ๐ โง ๐ โ (0...(โฏโ๐))) โ โ๐ฃ โ Word ๐๐ = ((๐ โพ (0..^๐)) ++ ๐ฃ)) | ||
Theorem | pfx1s2 31577 | The prefix of length 1 of a length 2 word. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ (โจโ๐ด๐ตโโฉ prefix 1) = โจโ๐ดโโฉ) | ||
Theorem | pfxrn2 31578 | The range of a prefix of a word is a subset of the range of that word. Stronger version of pfxrn 14505. (Contributed by Thierry Arnoux, 12-Dec-2023.) |
โข ((๐ โ Word ๐ โง ๐ฟ โ (0...(โฏโ๐))) โ ran (๐ prefix ๐ฟ) โ ran ๐) | ||
Theorem | pfxrn3 31579 | Express the range of a prefix of a word. Stronger version of pfxrn2 31578. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
โข ((๐ โ Word ๐ โง ๐ฟ โ (0...(โฏโ๐))) โ ran (๐ prefix ๐ฟ) = (๐ โ (0..^๐ฟ))) | ||
Theorem | pfxf1 31580 | Condition for a prefix to be injective. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
โข (๐ โ ๐ โ Word ๐) & โข (๐ โ ๐:dom ๐โ1-1โ๐) & โข (๐ โ ๐ฟ โ (0...(โฏโ๐))) โ โข (๐ โ (๐ prefix ๐ฟ):dom (๐ prefix ๐ฟ)โ1-1โ๐) | ||
Theorem | s1f1 31581 | Conditions for a length 1 string to be a one-to-one function. (Contributed by Thierry Arnoux, 11-Dec-2023.) |
โข (๐ โ ๐ผ โ ๐ท) โ โข (๐ โ โจโ๐ผโโฉ:dom โจโ๐ผโโฉโ1-1โ๐ท) | ||
Theorem | s2rn 31582 | Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
โข (๐ โ ๐ผ โ ๐ท) & โข (๐ โ ๐ฝ โ ๐ท) โ โข (๐ โ ran โจโ๐ผ๐ฝโโฉ = {๐ผ, ๐ฝ}) | ||
Theorem | s2f1 31583 | Conditions for a length 2 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
โข (๐ โ ๐ผ โ ๐ท) & โข (๐ โ ๐ฝ โ ๐ท) & โข (๐ โ ๐ผ โ ๐ฝ) โ โข (๐ โ โจโ๐ผ๐ฝโโฉ:dom โจโ๐ผ๐ฝโโฉโ1-1โ๐ท) | ||
Theorem | s3rn 31584 | Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
โข (๐ โ ๐ผ โ ๐ท) & โข (๐ โ ๐ฝ โ ๐ท) & โข (๐ โ ๐พ โ ๐ท) โ โข (๐ โ ran โจโ๐ผ๐ฝ๐พโโฉ = {๐ผ, ๐ฝ, ๐พ}) | ||
Theorem | s3f1 31585 | Conditions for a length 3 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
โข (๐ โ ๐ผ โ ๐ท) & โข (๐ โ ๐ฝ โ ๐ท) & โข (๐ โ ๐พ โ ๐ท) & โข (๐ โ ๐ผ โ ๐ฝ) & โข (๐ โ ๐ฝ โ ๐พ) & โข (๐ โ ๐พ โ ๐ผ) โ โข (๐ โ โจโ๐ผ๐ฝ๐พโโฉ:dom โจโ๐ผ๐ฝ๐พโโฉโ1-1โ๐ท) | ||
Theorem | s3clhash 31586 | Closure of the words of length 3 in a preimage using the hash function. (Contributed by Thierry Arnoux, 27-Sep-2023.) |
โข โจโ๐ผ๐ฝ๐พโโฉ โ (โกโฏ โ {3}) | ||
Theorem | ccatf1 31587 | Conditions for a concatenation to be injective. (Contributed by Thierry Arnoux, 11-Dec-2023.) |
โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ด โ Word ๐) & โข (๐ โ ๐ต โ Word ๐) & โข (๐ โ ๐ด:dom ๐ดโ1-1โ๐) & โข (๐ โ ๐ต:dom ๐ตโ1-1โ๐) & โข (๐ โ (ran ๐ด โฉ ran ๐ต) = โ ) โ โข (๐ โ (๐ด ++ ๐ต):dom (๐ด ++ ๐ต)โ1-1โ๐) | ||
Theorem | pfxlsw2ccat 31588 | Reconstruct a word from its prefix and its last two symbols. (Contributed by Thierry Arnoux, 26-Sep-2023.) |
โข ๐ = (โฏโ๐) โ โข ((๐ โ Word ๐ โง 2 โค ๐) โ ๐ = ((๐ prefix (๐ โ 2)) ++ โจโ(๐โ(๐ โ 2))(๐โ(๐ โ 1))โโฉ)) | ||
Theorem | wrdt2ind 31589* | Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023.) |
โข (๐ฅ = โ โ (๐ โ ๐)) & โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) & โข (๐ฅ = (๐ฆ ++ โจโ๐๐โโฉ) โ (๐ โ ๐)) & โข (๐ฅ = ๐ด โ (๐ โ ๐)) & โข ๐ & โข ((๐ฆ โ Word ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐)) โ โข ((๐ด โ Word ๐ต โง 2 โฅ (โฏโ๐ด)) โ ๐) | ||
Theorem | swrdrn2 31590 | The range of a subword is a subset of the range of that word. Stronger version of swrdrn 14472. (Contributed by Thierry Arnoux, 12-Dec-2023.) |
โข ((๐ โ Word ๐ โง ๐ โ (0...๐) โง ๐ โ (0...(โฏโ๐))) โ ran (๐ substr โจ๐, ๐โฉ) โ ran ๐) | ||
Theorem | swrdrn3 31591 | Express the range of a subword. Stronger version of swrdrn2 31590. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
โข ((๐ โ Word ๐ โง ๐ โ (0...๐) โง ๐ โ (0...(โฏโ๐))) โ ran (๐ substr โจ๐, ๐โฉ) = (๐ โ (๐..^๐))) | ||
Theorem | swrdf1 31592 | Condition for a subword to be injective. (Contributed by Thierry Arnoux, 12-Dec-2023.) |
โข (๐ โ ๐ โ Word ๐ท) & โข (๐ โ ๐ โ (0...๐)) & โข (๐ โ ๐ โ (0...(โฏโ๐))) & โข (๐ โ ๐:dom ๐โ1-1โ๐ท) โ โข (๐ โ (๐ substr โจ๐, ๐โฉ):dom (๐ substr โจ๐, ๐โฉ)โ1-1โ๐ท) | ||
Theorem | swrdrndisj 31593 | Condition for the range of two subwords of an injective word to be disjoint. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
โข (๐ โ ๐ โ Word ๐ท) & โข (๐ โ ๐ โ (0...๐)) & โข (๐ โ ๐ โ (0...(โฏโ๐))) & โข (๐ โ ๐:dom ๐โ1-1โ๐ท) & โข (๐ โ ๐ โ (๐...๐)) & โข (๐ โ ๐ โ (๐...(โฏโ๐))) โ โข (๐ โ (ran (๐ substr โจ๐, ๐โฉ) โฉ ran (๐ substr โจ๐, ๐โฉ)) = โ ) | ||
Theorem | splfv3 31594 | Symbols to the right of a splice are unaffected. (Contributed by Thierry Arnoux, 14-Dec-2023.) |
โข (๐ โ ๐ โ Word ๐ด) & โข (๐ โ ๐น โ (0...๐)) & โข (๐ โ ๐ โ (0...(โฏโ๐))) & โข (๐ โ ๐ โ Word ๐ด) & โข (๐ โ ๐ โ (0..^((โฏโ๐) โ ๐))) & โข (๐ โ ๐พ = (๐น + (โฏโ๐ ))) โ โข (๐ โ ((๐ splice โจ๐น, ๐, ๐ โฉ)โ(๐ + ๐พ)) = (๐โ(๐ + ๐))) | ||
Theorem | 1cshid 31595 | Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
โข ((๐ โ Word ๐ โง ๐ โ โค โง (โฏโ๐) = 1) โ (๐ cyclShift ๐) = ๐) | ||
Theorem | cshw1s2 31596 | Cyclically shifting a length 2 word swaps its symbols. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ (โจโ๐ด๐ตโโฉ cyclShift 1) = โจโ๐ต๐ดโโฉ) | ||
Theorem | cshwrnid 31597 | Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
โข ((๐ โ Word ๐ โง ๐ โ โค) โ ran (๐ cyclShift ๐) = ran ๐) | ||
Theorem | cshf1o 31598 | Condition for the cyclic shift to be a bijection. (Contributed by Thierry Arnoux, 4-Oct-2023.) |
โข ((๐ โ Word ๐ท โง ๐:dom ๐โ1-1โ๐ท โง ๐ โ โค) โ (๐ cyclShift ๐):dom ๐โ1-1-ontoโran ๐) | ||
Theorem | ressplusf 31599 | The group operation function +๐ of a structure's restriction is the operation function's restriction to the new base. (Contributed by Thierry Arnoux, 26-Mar-2017.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ป = (๐บ โพs ๐ด) & โข โจฃ = (+gโ๐บ) & โข โจฃ Fn (๐ต ร ๐ต) & โข ๐ด โ ๐ต โ โข (+๐โ๐ป) = ( โจฃ โพ (๐ด ร ๐ด)) | ||
Theorem | ressnm 31600 | The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.) |
โข ๐ป = (๐บ โพs ๐ด) & โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข ๐ = (normโ๐บ) โ โข ((๐บ โ Mnd โง 0 โ ๐ด โง ๐ด โ ๐ต) โ (๐ โพ ๐ด) = (normโ๐ป)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |