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-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fz1nnct 31501 | NN and integer ranges starting from 1 are countable. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
β’ ((π΄ = β β¨ π΄ = (1..^π)) β π΄ βΌ Ο) | ||
Theorem | fz1nntr 31502 | NN and integer ranges starting from 1 are a transitive family of set. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
β’ (((π΄ = β β¨ π΄ = (1..^π)) β§ π β π΄) β (1..^π) β π΄) | ||
Theorem | hashunif 31503* | The cardinality of a disjoint finite union of finite sets. Cf. hashuni 15646. (Contributed by Thierry Arnoux, 17-Feb-2017.) |
β’ β²π₯π & β’ (π β π΄ β Fin) & β’ (π β π΄ β Fin) & β’ (π β Disj π₯ β π΄ π₯) β β’ (π β (β―ββͺ π΄) = Ξ£π₯ β π΄ (β―βπ₯)) | ||
Theorem | hashxpe 31504 | The size of the Cartesian product of two finite sets is the product of their sizes. This is a version of hashxp 14262 valid for infinite sets, which uses extended real numbers. (Contributed by Thierry Arnoux, 27-May-2023.) |
β’ ((π΄ β π β§ π΅ β π) β (β―β(π΄ Γ π΅)) = ((β―βπ΄) Β·e (β―βπ΅))) | ||
Theorem | hashgt1 31505 | Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
β’ (π΄ β π β (Β¬ π΄ β (β‘β― β {0, 1}) β 1 < (β―βπ΄))) | ||
Theorem | dvdszzq 31506 | Divisibility for an integer quotient. (Contributed by Thierry Arnoux, 17-Sep-2023.) |
β’ π = (π΄ / π΅) & β’ (π β π β β) & β’ (π β π β β€) & β’ (π β π΅ β β€) & β’ (π β π΅ β 0) & β’ (π β π β₯ π΄) & β’ (π β Β¬ π β₯ π΅) β β’ (π β π β₯ π) | ||
Theorem | prmdvdsbc 31507 | Condition for a prime number to divide a binomial coefficient. (Contributed by Thierry Arnoux, 17-Sep-2023.) |
β’ ((π β β β§ π β (1...(π β 1))) β π β₯ (πCπ)) | ||
Theorem | numdenneg 31508 | Numerator and denominator of the negative. (Contributed by Thierry Arnoux, 27-Oct-2017.) |
β’ (π β β β ((numerβ-π) = -(numerβπ) β§ (denomβ-π) = (denomβπ))) | ||
Theorem | divnumden2 31509 | Calculate the reduced form of a quotient using gcd. This version extends divnumden 16558 for the negative integers. (Contributed by Thierry Arnoux, 25-Oct-2017.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β ((numerβ(π΄ / π΅)) = -(π΄ / (π΄ gcd π΅)) β§ (denomβ(π΄ / π΅)) = -(π΅ / (π΄ gcd π΅)))) | ||
Theorem | nnindf 31510* | Principle of Mathematical Induction, using a bound-variable hypothesis instead of distinct variables. (Contributed by Thierry Arnoux, 6-May-2018.) |
β’ β²π¦π & β’ (π₯ = 1 β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ + 1) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ (π¦ β β β (π β π)) β β’ (π΄ β β β π) | ||
Theorem | nn0min 31511* | Extracting the minimum positive integer for which a property π does not hold. This uses substitutions similar to nn0ind 12529. (Contributed by Thierry Arnoux, 6-May-2018.) |
β’ (π = 0 β (π β π)) & β’ (π = π β (π β π)) & β’ (π = (π + 1) β (π β π)) & β’ (π β Β¬ π) & β’ (π β βπ β β π) β β’ (π β βπ β β0 (Β¬ π β§ π)) | ||
Theorem | subne0nn 31512 | A nonnegative difference is positive if the two numbers are not equal. (Contributed by Thierry Arnoux, 17-Dec-2023.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π β π) β β0) & β’ (π β π β π) β β’ (π β (π β π) β β) | ||
Theorem | ltesubnnd 31513 | Subtracting an integer number from another number decreases it. See ltsubrpd 12918. (Contributed by Thierry Arnoux, 18-Apr-2017.) |
β’ (π β π β β€) & β’ (π β π β β) β β’ (π β ((π + 1) β π) β€ π) | ||
Theorem | fprodeq02 31514* | If one of the factors is zero the product is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
β’ (π = πΎ β π΅ = πΆ) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΎ β π΄) & β’ (π β πΆ = 0) β β’ (π β βπ β π΄ π΅ = 0) | ||
Theorem | pr01ssre 31515 | The range of the indicator function is a subset of β. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
β’ {0, 1} β β | ||
Theorem | fprodex01 31516* | 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 31517* | A product over a pair is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
β’ (π = π΄ β π· = πΈ) & β’ (π = π΅ β π· = πΉ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΈ β β) & β’ (π β πΉ β β) & β’ (π β π΄ β π΅) β β’ (π β βπ β {π΄, π΅}π· = (πΈ Β· πΉ)) | ||
Theorem | prodtp 31518* | A product over a triple is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
β’ (π = π΄ β π· = πΈ) & β’ (π = π΅ β π· = πΉ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΈ β β) & β’ (π β πΉ β β) & β’ (π β π΄ β π΅) & β’ (π = πΆ β π· = πΊ) & β’ (π β πΆ β π) & β’ (π β πΊ β β) & β’ (π β π΄ β πΆ) & β’ (π β π΅ β πΆ) β β’ (π β βπ β {π΄, π΅, πΆ}π· = ((πΈ Β· πΉ) Β· πΊ)) | ||
Theorem | fsumub 31519* | An upper bound for a term of a positive finite sum. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
β’ (π = πΎ β π΅ = π·) & β’ (π β π΄ β Fin) & β’ (π β Ξ£π β π΄ π΅ = πΆ) & β’ ((π β§ π β π΄) β π΅ β β+) & β’ (π β πΎ β π΄) β β’ (π β π· β€ πΆ) | ||
Theorem | fsumiunle 31520* | 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 31521 | 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 31522 | Constant used for decimal fraction constructor. See df-dp2 31523. |
class _π΄π΅ | ||
Definition | df-dp2 31523 | 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 31524 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ (π΄ = π΅ β _π΄πΆ = _π΅πΆ) | ||
Theorem | dp2eq2 31525 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ (π΄ = π΅ β _πΆπ΄ = _πΆπ΅) | ||
Theorem | dp2eq1i 31526 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ π΄ = π΅ β β’ _π΄πΆ = _π΅πΆ | ||
Theorem | dp2eq2i 31527 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ π΄ = π΅ β β’ _πΆπ΄ = _πΆπ΅ | ||
Theorem | dp2eq12i 31528 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ π΄ = π΅ & β’ πΆ = π· β β’ _π΄πΆ = _π΅π· | ||
Theorem | dp20u 31529 | Add a zero in the tenths (lower) place. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 β β’ _π΄0 = π΄ | ||
Theorem | dp20h 31530 | Add a zero in the unit places. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β+ β β’ _0π΄ = (π΄ / ;10) | ||
Theorem | dp2cl 31531 | Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ ((π΄ β β β§ π΅ β β) β _π΄π΅ β β) | ||
Theorem | dp2clq 31532 | Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β β β’ _π΄π΅ β β | ||
Theorem | rpdp2cl 31533 | Closure for a decimal fraction in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β+ β β’ _π΄π΅ β β+ | ||
Theorem | rpdp2cl2 31534 | Closure for a decimal fraction with no decimal expansion in the positive real numbers. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
β’ π΄ β β β β’ _π΄0 β β+ | ||
Theorem | dp2lt10 31535 | Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β+ & β’ π΄ < ;10 & β’ π΅ < ;10 β β’ _π΄π΅ < ;10 | ||
Theorem | dp2lt 31536 | Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β+ & β’ πΆ β β+ & β’ π΅ < πΆ β β’ _π΄π΅ < _π΄πΆ | ||
Theorem | dp2ltsuc 31537 | Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β+ & β’ π΅ < ;10 & β’ (π΄ + 1) = πΆ β β’ _π΄π΅ < πΆ | ||
Theorem | dp2ltc 31538 | 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 31540 and df-dp2 31523 for more information; dpval2 31544 and dpfrac1 31543 provide a more convenient way to obtain a value. This is intentionally similar to df-dec 12552. | ||
Syntax | cdp 31539 | Decimal point operator. See df-dp 31540. |
class . | ||
Definition | df-dp 31540* |
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 31541 | Define the value of the decimal point operator. See df-dp 31540. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ ((π΄ β β0 β§ π΅ β β) β (π΄.π΅) = _π΄π΅) | ||
Theorem | dpcl 31542 | Prove that the closure of the decimal point is β as we have defined it. See df-dp 31540. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ ((π΄ β β0 β§ π΅ β β) β (π΄.π΅) β β) | ||
Theorem | dpfrac1 31543 | Prove a simple equivalence involving the decimal point. See df-dp 31540 and dpcl 31542. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.) |
β’ ((π΄ β β0 β§ π΅ β β) β (π΄.π΅) = (;π΄π΅ / ;10)) | ||
Theorem | dpval2 31544 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β β β’ (π΄.π΅) = (π΄ + (π΅ / ;10)) | ||
Theorem | dpval3 31545 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β β β’ (π΄.π΅) = _π΄π΅ | ||
Theorem | dpmul10 31546 | Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β β β’ ((π΄.π΅) Β· ;10) = ;π΄π΅ | ||
Theorem | decdiv10 31547 | Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β β β’ (;π΄π΅ / ;10) = (π΄.π΅) | ||
Theorem | dpmul100 31548 | Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β β β’ ((π΄._π΅πΆ) Β· ;;100) = ;;π΄π΅πΆ | ||
Theorem | dp3mul10 31549 | Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β β β’ ((π΄._π΅πΆ) Β· ;10) = (;π΄π΅.πΆ) | ||
Theorem | dpmul1000 31550 | Multiply by 1000 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β0 & β’ π· β β β β’ ((π΄._π΅_πΆπ·) Β· ;;;1000) = ;;;π΄π΅πΆπ· | ||
Theorem | dpval3rp 31551 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β+ β β’ (π΄.π΅) = _π΄π΅ | ||
Theorem | dp0u 31552 | Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 β β’ (π΄.0) = π΄ | ||
Theorem | dp0h 31553 | Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β+ β β’ (0.π΄) = (π΄ / ;10) | ||
Theorem | rpdpcl 31554 | Closure of the decimal point in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β+ β β’ (π΄.π΅) β β+ | ||
Theorem | dplt 31555 | Comparing two decimal expansions (equal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β+ & β’ πΆ β β+ & β’ π΅ < πΆ β β’ (π΄.π΅) < (π΄.πΆ) | ||
Theorem | dplti 31556 | Comparing a decimal expansions with the next higher integer. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β+ & β’ πΆ β β0 & β’ π΅ < ;10 & β’ (π΄ + 1) = πΆ β β’ (π΄.π΅) < πΆ | ||
Theorem | dpgti 31557 | Comparing a decimal expansions with the next lower integer. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β+ β β’ π΄ < (π΄.π΅) | ||
Theorem | dpltc 31558 | Comparing two decimal integers (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β+ & β’ πΆ β β0 & β’ π· β β+ & β’ π΄ < πΆ & β’ π΅ < ;10 β β’ (π΄.π΅) < (πΆ.π·) | ||
Theorem | dpexpp1 31559 | 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 31560 | Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β+ β β’ ((0._π΄π΅) Β· ;10) = (π΄.π΅) | ||
Theorem | dpadd2 31561 | Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β+ & β’ πΆ β β0 & β’ π· β β+ & β’ πΈ β β0 & β’ πΉ β β+ & β’ πΊ β β0 & β’ π» β β0 & β’ (πΊ + π») = πΌ & β’ ((π΄.π΅) + (πΆ.π·)) = (πΈ.πΉ) β β’ ((πΊ._π΄π΅) + (π»._πΆπ·)) = (πΌ._πΈπΉ) | ||
Theorem | dpadd 31562 | Addition with one decimal. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β0 & β’ π· β β0 & β’ πΈ β β0 & β’ πΉ β β0 & β’ (;π΄π΅ + ;πΆπ·) = ;πΈπΉ β β’ ((π΄.π΅) + (πΆ.π·)) = (πΈ.πΉ) | ||
Theorem | dpadd3 31563 | Addition with two decimals. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β0 & β’ π· β β0 & β’ πΈ β β0 & β’ πΊ β β0 & β’ πΉ β β0 & β’ π» β β0 & β’ πΌ β β0 & β’ (;;π΄π΅πΆ + ;;π·πΈπΉ) = ;;πΊπ»πΌ β β’ ((π΄._π΅πΆ) + (π·._πΈπΉ)) = (πΊ._π»πΌ) | ||
Theorem | dpmul 31564 | Multiplication with one decimal point. (Contributed by Thierry Arnoux, 26-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β0 & β’ π· β β0 & β’ πΈ β β0 & β’ πΊ β β0 & β’ π½ β β0 & β’ πΎ β β0 & β’ (π΄ Β· πΆ) = πΉ & β’ (π΄ Β· π·) = π & β’ (π΅ Β· πΆ) = πΏ & β’ (π΅ Β· π·) = ;πΈπΎ & β’ ((πΏ + π) + πΈ) = ;πΊπ½ & β’ (πΉ + πΊ) = πΌ β β’ ((π΄.π΅) Β· (πΆ.π·)) = (πΌ._π½πΎ) | ||
Theorem | dpmul4 31565 | 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 31566 | Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
β’ (3 / 2) = (1.5) | ||
Theorem | 1mhdrd 31567 | Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
β’ ((0._99) + (0._01)) = 1 | ||
Syntax | cxdiv 31568 | Extend class notation to include division of extended reals. |
class /π | ||
Definition | df-xdiv 31569* | Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
β’ /π = (π₯ β β*, π¦ β (β β {0}) β¦ (β©π§ β β* (π¦ Β·e π§) = π₯)) | ||
Theorem | xdivval 31570* | 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 31571* | Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
β’ ((π΄ β β β§ π΄ β 0) β βπ₯ β β (π΄ Β·e π₯) = 1) | ||
Theorem | xmulcand 31572 | Cancellation law for extended multiplication. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β) & β’ (π β πΆ β 0) β β’ (π β ((πΆ Β·e π΄) = (πΆ Β·e π΅) β π΄ = π΅)) | ||
Theorem | xreceu 31573* | Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
β’ ((π΄ β β* β§ π΅ β β β§ π΅ β 0) β β!π₯ β β* (π΅ Β·e π₯) = π΄) | ||
Theorem | xdivcld 31574 | Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β) & β’ (π β π΅ β 0) β β’ (π β (π΄ /π π΅) β β*) | ||
Theorem | xdivcl 31575 | Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
β’ ((π΄ β β* β§ π΅ β β β§ π΅ β 0) β (π΄ /π π΅) β β*) | ||
Theorem | xdivmul 31576 | Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016.) |
β’ ((π΄ β β* β§ π΅ β β* β§ (πΆ β β β§ πΆ β 0)) β ((π΄ /π πΆ) = π΅ β (πΆ Β·e π΅) = π΄)) | ||
Theorem | rexdiv 31577 | The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (π΄ /π π΅) = (π΄ / π΅)) | ||
Theorem | xdivrec 31578 | Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
β’ ((π΄ β β* β§ π΅ β β β§ π΅ β 0) β (π΄ /π π΅) = (π΄ Β·e (1 /π π΅))) | ||
Theorem | xdivid 31579 | A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
β’ ((π΄ β β β§ π΄ β 0) β (π΄ /π π΄) = 1) | ||
Theorem | xdiv0 31580 | Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
β’ ((π΄ β β β§ π΄ β 0) β (0 /π π΄) = 0) | ||
Theorem | xdiv0rp 31581 | Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
β’ (π΄ β β+ β (0 /π π΄) = 0) | ||
Theorem | eliccioo 31582 | Membership in a closed interval of extended reals versus the same open interval. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ β€ π΅) β (πΆ β (π΄[,]π΅) β (πΆ = π΄ β¨ πΆ β (π΄(,)π΅) β¨ πΆ = π΅))) | ||
Theorem | elxrge02 31583 | Elementhood in the set of nonnegative extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
β’ (π΄ β (0[,]+β) β (π΄ = 0 β¨ π΄ β β+ β¨ π΄ = +β)) | ||
Theorem | xdivpnfrp 31584 | Plus infinity divided by a positive real number is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
β’ (π΄ β β+ β (+β /π π΄) = +β) | ||
Theorem | rpxdivcld 31585 | Closure law for extended division of positive reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) β β’ (π β (π΄ /π π΅) β β+) | ||
Theorem | xrpxdivcld 31586 | Closure law for extended division of positive extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
β’ (π β π΄ β (0[,]+β)) & β’ (π β π΅ β β+) β β’ (π β (π΄ /π π΅) β (0[,]+β)) | ||
Theorem | wrdfd 31587 | 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 31588 | 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 31589* | 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 31590 | The prefix of length 1 of a length 2 word. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ ((π΄ β π β§ π΅ β π) β (β¨βπ΄π΅ββ© prefix 1) = β¨βπ΄ββ©) | ||
Theorem | pfxrn2 31591 | 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 31592 | Express the range of a prefix of a word. Stronger version of pfxrn2 31591. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β ran (π prefix πΏ) = (π β (0..^πΏ))) | ||
Theorem | pfxf1 31593 | 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 31594 | 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 31595 | Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ (π β πΌ β π·) & β’ (π β π½ β π·) β β’ (π β ran β¨βπΌπ½ββ© = {πΌ, π½}) | ||
Theorem | s2f1 31596 | 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 31597 | Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) β β’ (π β ran β¨βπΌπ½πΎββ© = {πΌ, π½, πΎ}) | ||
Theorem | s3f1 31598 | 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 31599 | Closure of the words of length 3 in a preimage using the hash function. (Contributed by Thierry Arnoux, 27-Sep-2023.) |
β’ β¨βπΌπ½πΎββ© β (β‘β― β {3}) | ||
Theorem | ccatf1 31600 | 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βπ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |