![]() |
Metamath
Proof Explorer Theorem List (p. 115 of 443) | < 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: | ![]() (1-28474) |
![]() (28475-29999) |
![]() (30000-44271) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | infm3 11401* | The completeness axiom for reals in terms of infimum: a nonempty, bounded-below set of reals has an infimum. (This theorem is the dual of sup3 11399.) (Contributed by NM, 14-Jun-2005.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) | ||
Theorem | suprcl 11402* | Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Oct-2004.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ ℝ) | ||
Theorem | suprub 11403* | A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Oct-2004.) |
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐵 ∈ 𝐴) → 𝐵 ≤ sup(𝐴, ℝ, < )) | ||
Theorem | suprubd 11404* | Natural deduction form of suprubd 11404. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < )) | ||
Theorem | suprcld 11405* | Natural deduction form of suprcl 11402. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ) | ||
Theorem | suprlub 11406* | The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (𝐵 < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 𝐵 < 𝑧)) | ||
Theorem | suprnub 11407* | An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (¬ 𝐵 < sup(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 ¬ 𝐵 < 𝑧)) | ||
Theorem | suprleub 11408* | The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.) |
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵)) | ||
Theorem | supaddc 11409* | The supremum function distributes over addition in a sense similar to that in supmul1 11411. (Contributed by Brendan Leahy, 25-Sep-2017.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 𝑧 = (𝑣 + 𝐵)} ⇒ ⊢ (𝜑 → (sup(𝐴, ℝ, < ) + 𝐵) = sup(𝐶, ℝ, < )) | ||
Theorem | supadd 11410* | The supremum function distributes over addition in a sense similar to that in supmul 11414. (Contributed by Brendan Leahy, 26-Sep-2017.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥) & ⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 + 𝑏)} ⇒ ⊢ (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < )) | ||
Theorem | supmul1 11411* | The supremum function distributes over multiplication, in the sense that 𝐴 · (sup𝐵) = sup(𝐴 · 𝐵), where 𝐴 · 𝐵 is shorthand for {𝐴 · 𝑏 ∣ 𝑏 ∈ 𝐵} and is defined as 𝐶 below. This is the simple version, with only one set argument; see supmul 11414 for the more general case with two set arguments. (Contributed by Mario Carneiro, 5-Jul-2013.) |
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐵 𝑧 = (𝐴 · 𝑣)} & ⊢ (𝜑 ↔ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ 𝐵 0 ≤ 𝑥) ∧ (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥))) ⇒ ⊢ (𝜑 → (𝐴 · sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < )) | ||
Theorem | supmullem1 11412* | Lemma for supmul 11414. (Contributed by Mario Carneiro, 5-Jul-2013.) |
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 · 𝑏)} & ⊢ (𝜑 ↔ ((∀𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐵 0 ≤ 𝑥) ∧ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥))) ⇒ ⊢ (𝜑 → ∀𝑤 ∈ 𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) · sup(𝐵, ℝ, < ))) | ||
Theorem | supmullem2 11413* | Lemma for supmul 11414. (Contributed by Mario Carneiro, 5-Jul-2013.) |
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 · 𝑏)} & ⊢ (𝜑 ↔ ((∀𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐵 0 ≤ 𝑥) ∧ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥))) ⇒ ⊢ (𝜑 → (𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥)) | ||
Theorem | supmul 11414* | The supremum function distributes over multiplication, in the sense that (sup𝐴) · (sup𝐵) = sup(𝐴 · 𝐵), where 𝐴 · 𝐵 is shorthand for {𝑎 · 𝑏 ∣ 𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵} and is defined as 𝐶 below. We made use of this in our definition of multiplication in the Dedekind cut construction of the reals (see df-mp 10204). (Contributed by Mario Carneiro, 5-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2014.) |
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 · 𝑏)} & ⊢ (𝜑 ↔ ((∀𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐵 0 ≤ 𝑥) ∧ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥))) ⇒ ⊢ (𝜑 → (sup(𝐴, ℝ, < ) · sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < )) | ||
Theorem | sup3ii 11415* | A version of the completeness axiom for reals. (Contributed by NM, 23-Aug-1999.) |
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) | ||
Theorem | suprclii 11416* | Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Sep-1999.) |
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ sup(𝐴, ℝ, < ) ∈ ℝ | ||
Theorem | suprubii 11417* | A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Sep-1999.) |
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 ≤ sup(𝐴, ℝ, < )) | ||
Theorem | suprlubii 11418* | The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Oct-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝐵 ∈ ℝ → (𝐵 < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 𝐵 < 𝑧)) | ||
Theorem | suprnubii 11419* | An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Oct-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝐵 ∈ ℝ → (¬ 𝐵 < sup(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 ¬ 𝐵 < 𝑧)) | ||
Theorem | suprleubii 11420* | The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.) |
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝐵 ∈ ℝ → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵)) | ||
Theorem | riotaneg 11421* | The negative of the unique real such that 𝜑. (Contributed by NM, 13-Jun-2005.) |
⊢ (𝑥 = -𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ ℝ 𝜑 → (℩𝑥 ∈ ℝ 𝜑) = -(℩𝑦 ∈ ℝ 𝜓)) | ||
Theorem | negiso 11422 | Negation is an order anti-isomorphism of the real numbers, which is its own inverse. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ -𝑥) ⇒ ⊢ (𝐹 Isom < , ◡ < (ℝ, ℝ) ∧ ◡𝐹 = 𝐹) | ||
Theorem | dfinfre 11423* | The infimum of a set of reals 𝐴. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
⊢ (𝐴 ⊆ ℝ → inf(𝐴, ℝ, < ) = ∪ {𝑥 ∈ ℝ ∣ (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))}) | ||
Theorem | infrecl 11424* | Closure of infimum of a nonempty bounded set of reals. (Contributed by NM, 8-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ∈ ℝ) | ||
Theorem | infrenegsup 11425* | The infimum of a set of reals 𝐴 is the negative of the supremum of the negatives of its elements. The antecedent ensures that 𝐴 is nonempty and has a lower bound. (Contributed by NM, 14-Jun-2005.) (Revised by AV, 4-Sep-2020.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) = -sup({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < )) | ||
Theorem | infregelb 11426* | Any lower bound of a nonempty set of real numbers is less than or equal to its infimum. (Contributed by Jeff Hankins, 1-Sep-2013.) (Revised by AV, 4-Sep-2020.) (Proof modification is discouraged.) |
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 𝐵 ≤ 𝑧)) | ||
Theorem | infrelb 11427* | If a nonempty set of real numbers has a lower bound, its infimum is less than or equal to any of its elements. (Contributed by Jeff Hankins, 15-Sep-2013.) (Revised by AV, 4-Sep-2020.) |
⊢ ((𝐵 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝐵) → inf(𝐵, ℝ, < ) ≤ 𝐴) | ||
Theorem | supfirege 11428 | The supremum of a finite set of real numbers is greater than or equal to all the real numbers of the set. (Contributed by AV, 1-Oct-2019.) |
⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 = sup(𝐵, ℝ, < )) ⇒ ⊢ (𝜑 → 𝐶 ≤ 𝑆) | ||
Theorem | inelr 11429 | The imaginary unit i is not a real number. (Contributed by NM, 6-May-1999.) |
⊢ ¬ i ∈ ℝ | ||
Theorem | rimul 11430 | A real number times the imaginary unit is real only if the number is 0. (Contributed by NM, 28-May-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ (i · 𝐴) ∈ ℝ) → 𝐴 = 0) | ||
Theorem | cru 11431 | The representation of complex numbers in terms of real and imaginary parts is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 + (i · 𝐵)) = (𝐶 + (i · 𝐷)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | crne0 11432 | The real representation of complex numbers is nonzero iff one of its terms is nonzero. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ (𝐴 + (i · 𝐵)) ≠ 0)) | ||
Theorem | creur 11433* | The real part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Theorem | creui 11434* | The imaginary part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℂ → ∃!𝑦 ∈ ℝ ∃𝑥 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Theorem | cju 11435* | The complex conjugate of a complex number is unique. (Contributed by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)) | ||
Theorem | ofsubeq0 11436 | Function analogue of subeq0 10713. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ) → ((𝐹 ∘𝑓 − 𝐺) = (𝐴 × {0}) ↔ 𝐹 = 𝐺)) | ||
Theorem | ofnegsub 11437 | Function analogue of negsub 10735. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ) → (𝐹 ∘𝑓 + ((𝐴 × {-1}) ∘𝑓 · 𝐺)) = (𝐹 ∘𝑓 − 𝐺)) | ||
Theorem | ofsubge0 11438 | Function analogue of subge0 10954. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ) → ((𝐴 × {0}) ∘𝑟 ≤ (𝐹 ∘𝑓 − 𝐺) ↔ 𝐺 ∘𝑟 ≤ 𝐹)) | ||
Syntax | cn 11439 | Extend class notation to include the class of positive integers. |
class ℕ | ||
Definition | df-nn 11440 |
Define the set of positive integers. Some authors, especially in analysis
books, call these the natural numbers, whereas other authors choose to
include 0 in their definition of natural numbers. Note that ℕ is a
subset of complex numbers (nnsscn 11444), in contrast to the more elementary
ordinal natural numbers ω, df-om 7397). See nnind 11459 for the
principle of mathematical induction. See df-n0 11708 for the set of
nonnegative integers ℕ0. See dfn2 11722
for ℕ defined in terms of
ℕ0.
This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 8898 in certain proofs. For a more conventional and intuitive definition ("the smallest set of reals containing 1 as well as the successor of every member") see dfnn3 11455 (or its slight variant dfnn2 11454). (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 3-May-2014.) |
⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) | ||
Theorem | nnexALT 11441 | Alternate proof of nnex 11446, more direct, that makes use of ax-rep 5049. (Contributed by Mario Carneiro, 3-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ℕ ∈ V | ||
Theorem | peano5nni 11442* | Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of [Apostol] p. 34. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ((1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ℕ ⊆ 𝐴) | ||
Theorem | nnssre 11443 | The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.) |
⊢ ℕ ⊆ ℝ | ||
Theorem | nnsscn 11444 | The positive integers are a subset of the complex numbers. Remark: this could also be proven from nnssre 11443 and ax-resscn 10392 at the cost of using more axioms. (Contributed by NM, 2-Aug-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
⊢ ℕ ⊆ ℂ | ||
Theorem | nnsscnOLD 11445 | Obsolete version of nnsscn 11444 as of 4-Oct-2022. The positive integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ℕ ⊆ ℂ | ||
Theorem | nnex 11446 | The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ℕ ∈ V | ||
Theorem | nnre 11447 | A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ) | ||
Theorem | nncn 11448 | A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ) | ||
Theorem | nnrei 11449 | A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ∈ ℝ | ||
Theorem | nncni 11450 | A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ∈ ℂ | ||
Theorem | nncniOLD 11451 | Obsolete version of nncni 11450 as of 4-Oct-2022. A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ∈ ℂ | ||
Theorem | 1nn 11452 | Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 1 ∈ ℕ | ||
Theorem | peano2nn 11453 | Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ) | ||
Theorem | dfnn2 11454* | Alternate definition of the set of positive integers. This was our original definition, before the current df-nn 11440 replaced it. This definition requires the axiom of infinity to ensure it has the properties we expect. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.) |
⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} | ||
Theorem | dfnn3 11455* | Alternate definition of the set of positive integers. Definition of positive integers in [Apostol] p. 22. (Contributed by NM, 3-Jul-2005.) |
⊢ ℕ = ∩ {𝑥 ∣ (𝑥 ⊆ ℝ ∧ 1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} | ||
Theorem | nnred 11456 | A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | nncnd 11457 | A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) | ||
Theorem | peano2nnd 11458 | Peano postulate: a successor of a positive integer is a positive integer. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 + 1) ∈ ℕ) | ||
Theorem | nnind 11459* | Principle of Mathematical Induction (inference schema). The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. See nnaddcl 11463 for an example of its use. See nn0ind 11890 for induction on nonnegative integers and uzind 11887, uzind4 12120 for induction on an arbitrary upper set of integers. See indstr 12130 for strong induction. See also nnindALT 11460. This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.) |
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ ℕ → 𝜏) | ||
Theorem | nnindALT 11460* |
Principle of Mathematical Induction (inference schema). The last four
hypotheses give us the substitution instances we need; the first two are
the induction step and the basis.
This ALT version of nnind 11459 has a different hypothesis order. It may be easier to use with the Metamath program Proof Assistant, because "MM-PA> ASSIGN LAST" will be applied to the substitution instances first. We may eventually use this one as the official version. You may use either version. After the proof is complete, the ALT version can be changed to the non-ALT version with "MM-PA> MINIMIZE_WITH nnind / MAYGROW". (Contributed by NM, 7-Dec-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) & ⊢ 𝜓 & ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) ⇒ ⊢ (𝐴 ∈ ℕ → 𝜏) | ||
Theorem | nn1m1nn 11461 | Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014.) |
⊢ (𝐴 ∈ ℕ → (𝐴 = 1 ∨ (𝐴 − 1) ∈ ℕ)) | ||
Theorem | nn1suc 11462* | If a statement holds for 1 and also holds for a successor, it holds for all positive integers. The first three hypotheses give us the substitution instances we need; the last two show that it holds for 1 and for a successor. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 16-May-2014.) |
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜃)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ℕ → 𝜒) ⇒ ⊢ (𝐴 ∈ ℕ → 𝜃) | ||
Theorem | nnaddcl 11463 | Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) ∈ ℕ) | ||
Theorem | nnmulcl 11464 | Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.) Remove dependency on ax-mulcom 10399 and ax-mulass 10401. (Revised by Steven Nguyen, 24-Sep-2022.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ) | ||
Theorem | nnmulcli 11465 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℕ | ||
Theorem | nnmtmip 11466 | "Minus times minus is plus, The reason for this we need not discuss." (W. H. Auden, as quoted in M. Guillen "Bridges to Infinity", p. 64, see also Metamath Book, section 1.1.1, p. 5) This statement, formalized to "The product of two negative integers is a positive integer", is proved by the following theorem, therefore it actually need not be discussed anymore. "The reason for this" is that (-𝐴 · -𝐵) = (𝐴 · 𝐵) for all complex numbers 𝐴 and 𝐵 because of mul2neg 10880, 𝐴 and 𝐵 are complex numbers because of nncn 11448, and (𝐴 · 𝐵) ∈ ℕ because of nnmulcl 11464. This also holds for positive reals, see rpmtmip 12230. Note that the opposites -𝐴 and -𝐵 of the positive integers 𝐴 and 𝐵 are negative integers. (Contributed by AV, 23-Dec-2022.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (-𝐴 · -𝐵) ∈ ℕ) | ||
Theorem | nn2ge 11467* | There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ (𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥)) | ||
Theorem | nnge1 11468 | A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.) |
⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴) | ||
Theorem | nngt1ne1 11469 | A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.) |
⊢ (𝐴 ∈ ℕ → (1 < 𝐴 ↔ 𝐴 ≠ 1)) | ||
Theorem | nnle1eq1 11470 | A positive integer is less than or equal to one iff it is equal to one. (Contributed by NM, 3-Apr-2005.) |
⊢ (𝐴 ∈ ℕ → (𝐴 ≤ 1 ↔ 𝐴 = 1)) | ||
Theorem | nngt0 11471 | A positive integer is positive. (Contributed by NM, 26-Sep-1999.) |
⊢ (𝐴 ∈ ℕ → 0 < 𝐴) | ||
Theorem | nnnlt1 11472 | A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 < 1) | ||
Theorem | nnnle0 11473 | A positive integer is not less than or equal to zero . (Contributed by AV, 13-May-2020.) |
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 ≤ 0) | ||
Theorem | nnne0 11474 | A positive integer is nonzero. See nnne0ALT 11478 for a shorter proof using ax-pre-mulgt0 10412. This proof avoids 0lt1 10963, and thus ax-pre-mulgt0 10412, by splitting ax-1ne0 10404 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 10412. (Revised by Steven Nguyen, 30-Jan-2023.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0) | ||
Theorem | nnneneg 11475 | No positive integer is equal to its negation. (Contributed by AV, 20-Jun-2023.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ -𝐴) | ||
Theorem | 0nnn 11476 | Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) Remove dependency on ax-pre-mulgt0 10412. (Revised by Steven Nguyen, 30-Jan-2023.) |
⊢ ¬ 0 ∈ ℕ | ||
Theorem | 0nnnALT 11477 | Alternate proof of 0nnn 11476, which requires ax-pre-mulgt0 10412 but is not based on nnne0 11474 (and which can therefore be used in nnne0ALT 11478). (Contributed by NM, 25-Aug-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ¬ 0 ∈ ℕ | ||
Theorem | nnne0ALT 11478 | Alternate version of nnne0 11474. A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0) | ||
Theorem | nngt0i 11479 | A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 0 < 𝐴 | ||
Theorem | nnne0i 11480 | A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ≠ 0 | ||
Theorem | nndivre 11481 | The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ) | ||
Theorem | nnrecre 11482 | The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.) |
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ) | ||
Theorem | nnrecgt0 11483 | The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.) |
⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴)) | ||
Theorem | nnsub 11484 | Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)) | ||
Theorem | nnsubi 11485 | Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ) | ||
Theorem | nndiv 11486* | Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ)) | ||
Theorem | nndivtr 11487 | Transitive property of divisibility: if 𝐴 divides 𝐵 and 𝐵 divides 𝐶, then 𝐴 divides 𝐶. Typically, 𝐶 would be an integer, although the theorem holds for complex 𝐶. (Contributed by NM, 3-May-2005.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℂ) ∧ ((𝐵 / 𝐴) ∈ ℕ ∧ (𝐶 / 𝐵) ∈ ℕ)) → (𝐶 / 𝐴) ∈ ℕ) | ||
Theorem | nnge1d 11488 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 1 ≤ 𝐴) | ||
Theorem | nngt0d 11489 | A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 0 < 𝐴) | ||
Theorem | nnne0d 11490 | A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | nnrecred 11491 | The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) | ||
Theorem | nnaddcld 11492 | Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ) | ||
Theorem | nnmulcld 11493 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) | ||
Theorem | nndivred 11494 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ) | ||
The decimal representation of numbers/integers is based on the decimal digits 0 through 9 (df-0 10342 through df-9 11510), which are explicitly defined in the following. Note that the numbers 0 and 1 are constants defined as primitives of the complex number axiom system (see df-0 10342 and df-1 10343). With the decimal constructor df-dec 11912, it is possible to easily express larger integers in base 10. See deccl 11926 and the theorems that follow it. See also 4001prm 16334 (4001 is prime) and the proof of bpos 25571. Note that the decimal constructor builds on the definitions in this section. Note: The number 10 will be represented by its digits using the decimal constructor only, i.e. by ;10. Therefore, only decimal digits are needed (as symbols) for the decimal representation of a number. Integers can also be exhibited as sums of powers of 10 (e.g. the number 103 can be expressed as ((;10↑2) + 3)) or as some other expression built from operations on the numbers 0 through 9. For example, the prime number 823541 can be expressed as (7↑7) − 2. Decimals can be expressed as ratios of integers, as in cos2bnd 15401. Most abstract math rarely requires numbers larger than 4. Even in Wiles' proof of Fermat's Last Theorem, the largest number used appears to be 12. | ||
Syntax | c2 11495 | Extend class notation to include the number 2. |
class 2 | ||
Syntax | c3 11496 | Extend class notation to include the number 3. |
class 3 | ||
Syntax | c4 11497 | Extend class notation to include the number 4. |
class 4 | ||
Syntax | c5 11498 | Extend class notation to include the number 5. |
class 5 | ||
Syntax | c6 11499 | Extend class notation to include the number 6. |
class 6 | ||
Syntax | c7 11500 | Extend class notation to include the number 7. |
class 7 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |