HomeTheorem List (p. 127 of 502)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 127 of 502) | < 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-31005) |
Hilbert Space Explorer
(31006-32528) |
Users' Mathboxes
(32529-50158) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nn0indd 12601* | Principle of Mathematical Induction (inference schema) on nonnegative integers, a deduction version. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ (𝑥 = 0 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ0) → 𝜂) | ||
| Theorem | fzind 12602* | Induction on the integers from 𝑀 to 𝑁 inclusive . The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 31-Mar-2011.) |
| ⊢ (𝑥 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐾 → (𝜑 ↔ 𝜏)) & ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝜓) & ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁)) → (𝜒 → 𝜃)) ⇒ ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → 𝜏) | ||
| Theorem | fnn0ind 12603* | Induction on the integers from 0 to 𝑁 inclusive. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 31-Mar-2011.) |
| ⊢ (𝑥 = 0 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐾 → (𝜑 ↔ 𝜏)) & ⊢ (𝑁 ∈ ℕ0 → 𝜓) & ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ∧ 𝑦 < 𝑁) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁) → 𝜏) | ||
| Theorem | nn0ind-raph 12604* | Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Raph Levien remarks: "This seems a bit painful. I wonder if an explicit substitution version would be easier." (Contributed by Raph Levien, 10-Apr-2004.) |
| ⊢ (𝑥 = 0 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ℕ0 → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ ℕ0 → 𝜏) | ||
| Theorem | zindd 12605* | Principle of Mathematical Induction on all integers, deduction version. The first five hypotheses give the substitutions; the last three are the basis, the induction, and the extension to negative numbers. (Contributed by Paul Chapman, 17-Apr-2009.) (Proof shortened by Mario Carneiro, 4-Jan-2017.) |
| ⊢ (𝑥 = 0 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜏)) & ⊢ (𝑥 = -𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜂)) & ⊢ (𝜁 → 𝜓) & ⊢ (𝜁 → (𝑦 ∈ ℕ0 → (𝜒 → 𝜏))) & ⊢ (𝜁 → (𝑦 ∈ ℕ → (𝜒 → 𝜃))) ⇒ ⊢ (𝜁 → (𝐴 ∈ ℤ → 𝜂)) | ||
| Theorem | fzindd 12606* | Induction on the integers from M to N inclusive, a deduction version. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝑥 = 𝑀 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁) ∧ 𝜃) → 𝜏) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ ℤ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)) → 𝜂) | ||
| Theorem | btwnz 12607* | Any real number can be sandwiched between two integers. Exercise 2 of [Apostol] p. 28. (Contributed by NM, 10-Nov-2004.) |
| ⊢ (𝐴 ∈ ℝ → (∃𝑥 ∈ ℤ 𝑥 < 𝐴 ∧ ∃𝑦 ∈ ℤ 𝐴 < 𝑦)) | ||
| Theorem | zred 12608 | An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
| Theorem | zcnd 12609 | An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) | ||
| Theorem | znegcld 12610 | Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℤ) | ||
| Theorem | peano2zd 12611 | Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴 + 1) ∈ ℤ) | ||
| Theorem | zaddcld 12612 | Closure of addition of integers. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℤ) | ||
| Theorem | zsubcld 12613 | Closure of subtraction of integers. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℤ) | ||
| Theorem | zmulcld 12614 | Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℤ) | ||
| Theorem | znnn0nn 12615 | The negative of a negative integer, is a natural number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((𝑁 ∈ ℤ ∧ ¬ 𝑁 ∈ ℕ0) → -𝑁 ∈ ℕ) | ||
| Theorem | zadd2cl 12616 | Increasing an integer by 2 results in an integer. (Contributed by Alexander van der Vekens, 16-Sep-2018.) |
| ⊢ (𝑁 ∈ ℤ → (𝑁 + 2) ∈ ℤ) | ||
| Theorem | zriotaneg 12617* | The negative of the unique integer such that 𝜑. (Contributed by AV, 1-Dec-2018.) |
| ⊢ (𝑥 = -𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ ℤ 𝜑 → (℩𝑥 ∈ ℤ 𝜑) = -(℩𝑦 ∈ ℤ 𝜓)) | ||
| Theorem | suprfinzcl 12618 | The supremum of a nonempty finite set of integers is a member of the set. (Contributed by AV, 1-Oct-2019.) |
| ⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → sup(𝐴, ℝ, < ) ∈ 𝐴) | ||
| Syntax | cdc 12619 | Constant used for decimal constructor. |
| class ;𝐴𝐵 | ||
| Definition | df-dec 12620 | Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. For example, (;;;1000 + ;;;2000) = ;;;3000 1kp2ke3k 30533. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 1-Aug-2021.) |
| ⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵) | ||
| Theorem | 9p1e10 12621 | 9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 1-Aug-2021.) |
| ⊢ (9 + 1) = ;10 | ||
| Theorem | dfdec10 12622 | Version of the definition of the "decimal constructor" using ;10 instead of the symbol 10. Of course, this statement cannot be used as definition, because it uses the "decimal constructor". (Contributed by AV, 1-Aug-2021.) |
| ⊢ ;𝐴𝐵 = ((;10 · 𝐴) + 𝐵) | ||
| Theorem | decex 12623 | A decimal number is a set. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ ;𝐴𝐵 ∈ V | ||
| Theorem | deceq1 12624 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (𝐴 = 𝐵 → ;𝐴𝐶 = ;𝐵𝐶) | ||
| Theorem | deceq2 12625 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (𝐴 = 𝐵 → ;𝐶𝐴 = ;𝐶𝐵) | ||
| Theorem | deceq1i 12626 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ;𝐴𝐶 = ;𝐵𝐶 | ||
| Theorem | deceq2i 12627 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ;𝐶𝐴 = ;𝐶𝐵 | ||
| Theorem | deceq12i 12628 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ;𝐴𝐶 = ;𝐵𝐷 | ||
| Theorem | numnncl 12629 | Closure for a numeral (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ ((𝑇 · 𝐴) + 𝐵) ∈ ℕ | ||
| Theorem | num0u 12630 | Add a zero in the units place. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (𝑇 · 𝐴) = ((𝑇 · 𝐴) + 0) | ||
| Theorem | num0h 12631 | Add a zero in the higher places. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ 𝐴 = ((𝑇 · 0) + 𝐴) | ||
| Theorem | numcl 12632 | Closure for a decimal integer (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ ((𝑇 · 𝐴) + 𝐵) ∈ ℕ0 | ||
| Theorem | numsuc 12633 | The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ (𝐵 + 1) = 𝐶 & ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵) ⇒ ⊢ (𝑁 + 1) = ((𝑇 · 𝐴) + 𝐶) | ||
| Theorem | deccl 12634 | Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ ;𝐴𝐵 ∈ ℕ0 | ||
| Theorem | 10nn 12635 | 10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.) |
| ⊢ ;10 ∈ ℕ | ||
| Theorem | 10pos 12636 | The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 0 < ;10 | ||
| Theorem | 10nn0 12637 | 10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ ;10 ∈ ℕ0 | ||
| Theorem | 10re 12638 | The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 8-Oct-2022.) |
| ⊢ ;10 ∈ ℝ | ||
| Theorem | decnncl 12639 | Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ ;𝐴𝐵 ∈ ℕ | ||
| Theorem | dec0u 12640 | Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (;10 · 𝐴) = ;𝐴0 | ||
| Theorem | dec0h 12641 | Add a zero in the higher places. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ 𝐴 = ;0𝐴 | ||
| Theorem | numnncl2 12642 | Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015.) |
| ⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈ ℕ ⇒ ⊢ ((𝑇 · 𝐴) + 0) ∈ ℕ | ||
| Theorem | decnncl2 12643 | Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ ⇒ ⊢ ;𝐴0 ∈ ℕ | ||
| Theorem | numlt 12644 | Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ ((𝑇 · 𝐴) + 𝐵) < ((𝑇 · 𝐴) + 𝐶) | ||
| Theorem | numltc 12645 | Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐶 < 𝑇 & ⊢ 𝐴 < 𝐵 ⇒ ⊢ ((𝑇 · 𝐴) + 𝐶) < ((𝑇 · 𝐵) + 𝐷) | ||
| Theorem | le9lt10 12646 | A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less than 10. (Contributed by AV, 8-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐴 ≤ 9 ⇒ ⊢ 𝐴 < ;10 | ||
| Theorem | declt 12647 | Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ ;𝐴𝐵 < ;𝐴𝐶 | ||
| Theorem | decltc 12648 | Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐶 < ;10 & ⊢ 𝐴 < 𝐵 ⇒ ⊢ ;𝐴𝐶 < ;𝐵𝐷 | ||
| Theorem | declth 12649 | Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐶 ≤ 9 & ⊢ 𝐴 < 𝐵 ⇒ ⊢ ;𝐴𝐶 < ;𝐵𝐷 | ||
| Theorem | decsuc 12650 | The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ (𝐵 + 1) = 𝐶 & ⊢ 𝑁 = ;𝐴𝐵 ⇒ ⊢ (𝑁 + 1) = ;𝐴𝐶 | ||
| Theorem | 3declth 12651 | Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 8-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐴 < 𝐵 & ⊢ 𝐶 ≤ 9 & ⊢ 𝐸 ≤ 9 ⇒ ⊢ ;;𝐴𝐶𝐸 < ;;𝐵𝐷𝐹 | ||
| Theorem | 3decltc 12652 | Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 15-Jun-2021.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐴 < 𝐵 & ⊢ 𝐶 < ;10 & ⊢ 𝐸 < ;10 ⇒ ⊢ ;;𝐴𝐶𝐸 < ;;𝐵𝐷𝐹 | ||
| Theorem | decle 12653 | Comparing two decimal integers (equal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐵 ≤ 𝐶 ⇒ ⊢ ;𝐴𝐵 ≤ ;𝐴𝐶 | ||
| Theorem | decleh 12654 | Comparing two decimal integers (unequal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐶 ≤ 9 & ⊢ 𝐴 < 𝐵 ⇒ ⊢ ;𝐴𝐶 ≤ ;𝐵𝐷 | ||
| Theorem | declei 12655 | Comparing a digit to a decimal integer. (Contributed by AV, 17-Aug-2021.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 ≤ 9 ⇒ ⊢ 𝐶 ≤ ;𝐴𝐵 | ||
| Theorem | numlti 12656 | Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 < 𝑇 ⇒ ⊢ 𝐶 < ((𝑇 · 𝐴) + 𝐵) | ||
| Theorem | declti 12657 | Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 < ;10 ⇒ ⊢ 𝐶 < ;𝐴𝐵 | ||
| Theorem | decltdi 12658 | Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 ≤ 9 ⇒ ⊢ 𝐶 < ;𝐴𝐵 | ||
| Theorem | numsucc 12659 | The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑌 ∈ ℕ0 & ⊢ 𝑇 = (𝑌 + 1) & ⊢ 𝐴 ∈ ℕ0 & ⊢ (𝐴 + 1) = 𝐵 & ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝑌) ⇒ ⊢ (𝑁 + 1) = ((𝑇 · 𝐵) + 0) | ||
| Theorem | decsucc 12660 | The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ (𝐴 + 1) = 𝐵 & ⊢ 𝑁 = ;𝐴9 ⇒ ⊢ (𝑁 + 1) = ;𝐵0 | ||
| Theorem | 1e0p1 12661 | The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 1 = (0 + 1) | ||
| Theorem | dec10p 12662 | Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (;10 + 𝐴) = ;1𝐴 | ||
| Theorem | numma 12663 | Perform a multiply-add of two decimal integers 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷) & ⊢ 𝑃 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + 𝐶) = 𝐸 & ⊢ ((𝐵 · 𝑃) + 𝐷) = 𝐹 ⇒ ⊢ ((𝑀 · 𝑃) + 𝑁) = ((𝑇 · 𝐸) + 𝐹) | ||
| Theorem | nummac 12664 | Perform a multiply-add of two decimal integers 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷) & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + (𝐶 + 𝐺)) = 𝐸 & ⊢ ((𝐵 · 𝑃) + 𝐷) = ((𝑇 · 𝐺) + 𝐹) ⇒ ⊢ ((𝑀 · 𝑃) + 𝑁) = ((𝑇 · 𝐸) + 𝐹) | ||
| Theorem | numma2c 12665 | Perform a multiply-add of two decimal integers 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷) & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ ((𝑃 · 𝐴) + (𝐶 + 𝐺)) = 𝐸 & ⊢ ((𝑃 · 𝐵) + 𝐷) = ((𝑇 · 𝐺) + 𝐹) ⇒ ⊢ ((𝑃 · 𝑀) + 𝑁) = ((𝑇 · 𝐸) + 𝐹) | ||
| Theorem | numadd 12666 | Add two decimal integers 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷) & ⊢ (𝐴 + 𝐶) = 𝐸 & ⊢ (𝐵 + 𝐷) = 𝐹 ⇒ ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹) | ||
| Theorem | numaddc 12667 | Add two decimal integers 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷) & ⊢ 𝐹 ∈ ℕ0 & ⊢ ((𝐴 + 𝐶) + 1) = 𝐸 & ⊢ (𝐵 + 𝐷) = ((𝑇 · 1) + 𝐹) ⇒ ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹) | ||
| Theorem | nummul1c 12668 | The product of a decimal integer with a number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶 & ⊢ (𝐵 · 𝑃) = ((𝑇 · 𝐸) + 𝐷) ⇒ ⊢ (𝑁 · 𝑃) = ((𝑇 · 𝐶) + 𝐷) | ||
| Theorem | nummul2c 12669 | The product of a decimal integer with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ ((𝑃 · 𝐴) + 𝐸) = 𝐶 & ⊢ (𝑃 · 𝐵) = ((𝑇 · 𝐸) + 𝐷) ⇒ ⊢ (𝑃 · 𝑁) = ((𝑇 · 𝐶) + 𝐷) | ||
| Theorem | decma 12670 | Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ 𝑃 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + 𝐶) = 𝐸 & ⊢ ((𝐵 · 𝑃) + 𝐷) = 𝐹 ⇒ ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decmac 12671 | Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + (𝐶 + 𝐺)) = 𝐸 & ⊢ ((𝐵 · 𝑃) + 𝐷) = ;𝐺𝐹 ⇒ ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decma2c 12672 | Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplier 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ ((𝑃 · 𝐴) + (𝐶 + 𝐺)) = 𝐸 & ⊢ ((𝑃 · 𝐵) + 𝐷) = ;𝐺𝐹 ⇒ ⊢ ((𝑃 · 𝑀) + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decadd 12673 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ (𝐴 + 𝐶) = 𝐸 & ⊢ (𝐵 + 𝐷) = 𝐹 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decaddc 12674 | Add two numerals 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ ((𝐴 + 𝐶) + 1) = 𝐸 & ⊢ 𝐹 ∈ ℕ0 & ⊢ (𝐵 + 𝐷) = ;1𝐹 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decaddc2 12675 | Add two numerals 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ ((𝐴 + 𝐶) + 1) = 𝐸 & ⊢ (𝐵 + 𝐷) = ;10 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐸0 | ||
| Theorem | decrmanc 12676 | Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (no carry). (Contributed by AV, 16-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑃 ∈ ℕ0 & ⊢ (𝐴 · 𝑃) = 𝐸 & ⊢ ((𝐵 · 𝑃) + 𝑁) = 𝐹 ⇒ ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decrmac 12677 | Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by AV, 16-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + 𝐺) = 𝐸 & ⊢ ((𝐵 · 𝑃) + 𝑁) = ;𝐺𝐹 ⇒ ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decaddm10 12678 | The sum of two multiples of 10 is a multiple of 10. (Contributed by AV, 30-Jul-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ (;𝐴0 + ;𝐵0) = ;(𝐴 + 𝐵)0 | ||
| Theorem | decaddi 12679 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐴𝐶 | ||
| Theorem | decaddci 12680 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐴 + 1) = 𝐷 & ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐵 + 𝑁) = ;1𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐷𝐶 | ||
| Theorem | decaddci2 12681 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐴 + 1) = 𝐷 & ⊢ (𝐵 + 𝑁) = ;10 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐷0 | ||
| Theorem | decsubi 12682 | Difference between a numeral 𝑀 and a nonnegative integer 𝑁 (no underflow). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐴 + 1) = 𝐷 & ⊢ (𝐵 − 𝑁) = 𝐶 ⇒ ⊢ (𝑀 − 𝑁) = ;𝐴𝐶 | ||
| Theorem | decmul1 12683 | The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) Remove hypothesis 𝐷 ∈ ℕ0. (Revised by Steven Nguyen, 7-Dec-2022.) |
| ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵 & ⊢ (𝐴 · 𝑃) = 𝐶 & ⊢ (𝐵 · 𝑃) = 𝐷 ⇒ ⊢ (𝑁 · 𝑃) = ;𝐶𝐷 | ||
| Theorem | decmul1c 12684 | The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶 & ⊢ (𝐵 · 𝑃) = ;𝐸𝐷 ⇒ ⊢ (𝑁 · 𝑃) = ;𝐶𝐷 | ||
| Theorem | decmul2c 12685 | The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ ((𝑃 · 𝐴) + 𝐸) = 𝐶 & ⊢ (𝑃 · 𝐵) = ;𝐸𝐷 ⇒ ⊢ (𝑃 · 𝑁) = ;𝐶𝐷 | ||
| Theorem | decmulnc 12686 | The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
| ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ (𝑁 · ;𝐴𝐵) = ;(𝑁 · 𝐴)(𝑁 · 𝐵) | ||
| Theorem | 11multnc 12687 | The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
| ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝑁 · ;11) = ;𝑁𝑁 | ||
| Theorem | decmul10add 12688 | A multiplication of a number and a numeral expressed as addition with first summand as multiple of 10. (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ 𝐸 = (𝑀 · 𝐴) & ⊢ 𝐹 = (𝑀 · 𝐵) ⇒ ⊢ (𝑀 · ;𝐴𝐵) = (;𝐸0 + 𝐹) | ||
| Theorem | 6p5lem 12689 | Lemma for 6p5e11 12692 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐵 = (𝐷 + 1) & ⊢ 𝐶 = (𝐸 + 1) & ⊢ (𝐴 + 𝐷) = ;1𝐸 ⇒ ⊢ (𝐴 + 𝐵) = ;1𝐶 | ||
| Theorem | 5p5e10 12690 | 5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (5 + 5) = ;10 | ||
| Theorem | 6p4e10 12691 | 6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 + 4) = ;10 | ||
| Theorem | 6p5e11 12692 | 6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 + 5) = ;11 | ||
| Theorem | 6p6e12 12693 | 6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 + 6) = ;12 | ||
| Theorem | 7p3e10 12694 | 7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (7 + 3) = ;10 | ||
| Theorem | 7p4e11 12695 | 7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (7 + 4) = ;11 | ||
| Theorem | 7p5e12 12696 | 7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 5) = ;12 | ||
| Theorem | 7p6e13 12697 | 7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 6) = ;13 | ||
| Theorem | 7p7e14 12698 | 7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 7) = ;14 | ||
| Theorem | 8p2e10 12699 | 8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 + 2) = ;10 | ||
| Theorem | 8p3e11 12700 | 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 + 3) = ;11 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |