Metamath Proof Explorer - mmtheorems46

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 4501-4600 - Page 46 of 58

Type	Label	Description
Statement
Theorem	6p3e9 4501	6 + 3 = 9.
⊢ (6 + 3) = 9
Theorem	7p2e9 4502	7 + 2 = 9.
⊢ (7 + 2) = 9
Theorem	2t2e4 4503	2 times 2 equals 4.
⊢ (2 · 2) = 4
Theorem	3t2e6 4504	3 times 2 equals 6.
⊢ (3 · 2) = 6
Theorem	3t3e9 4505	3 times 3 equals 9.
⊢ (3 · 3) = 9
Theorem	4t2e8 4506	4 times 2 equals 8.
⊢ (4 · 2) = 8
Theorem	4d2e2 4507	One half of four is two.
⊢ (4 / 2) = 2
Theorem	halfpost 4508	A positive number is greater than its half.
⊢ (A ∈ ℝ → (0 < A ↔ (A / 2) < A))
Theorem	nominpos 4509	There exists no smallest positive real number.
⊢ ¬ ∃x ∈ ℝ (0 < x ∧ ¬ ∃y ∈ ℝ (0 < y ∧ y < x))
Theorem	sup2 4510	A non-empty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent).
⊢ ((A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃x ∈ ℝ ∀y ∈ A (y < x ∨ y = x)) → ∃x ∈ ℝ (∀y ∈ A ¬ x < y ∧ ∀y ∈ ℝ (y < x → ∃z ∈ A y < z)))
Theorem	sup3 4511	A version of the completeness axiom for reals.
⊢ ((A ⊆ ℝ ∧ ¬ A = ∅ ∧ ∃x ∈ ℝ ∀y ∈ A y ≤ x) → ∃x ∈ ℝ (∀y ∈ A ¬ x < y ∧ ∀y ∈ ℝ (y < x → ∃z ∈ A y < z)))
Theorem	suprcl 4512	Closure of supremum of a non-empty bounded set of reals.
⊢ ((A ⊆ ℝ ∧ ¬ A = ∅ ∧ ∃x ∈ ℝ ∀y ∈ A y ≤ x) → sup(A, ℝ, < ) ∈ ℝ)
Theorem	suprub 4513	A member of a non-empty bounded set of reals is less than or equal to the set's upper bound.
⊢ (((A ⊆ ℝ ∧ ¬ A = ∅ ∧ ∃x ∈ ℝ ∀y ∈ A y ≤ x) ∧ B ∈ A) → B ≤ sup(A, ℝ, < ))
Theorem	suprlub 4514	The supremum of a non-empty bounded set of reals is the least upper bound.
⊢ (((A ⊆ ℝ ∧ ¬ A = ∅ ∧ ∃x ∈ ℝ ∀y ∈ A y ≤ x) ∧ (B ∈ ℝ ∧ B < sup(A, ℝ, < ))) → ∃z ∈ A B < z)
Theorem	sup3i 4515	A version of the completeness axiom for reals.
⊢ (A ⊆ ℝ ∧ ¬ A = ∅ ∧ ∃x ∈ ℝ ∀y ∈ A y ≤ x)    ⇒   ⊢ ∃x ∈ ℝ (∀y ∈ A ¬ x < y ∧ ∀y ∈ ℝ (y < x → ∃z ∈ A y < z))
Theorem	suprcli 4516	Closure of supremum of a non-empty bounded set of reals.
⊢ (A ⊆ ℝ ∧ ¬ A = ∅ ∧ ∃x ∈ ℝ ∀y ∈ A y ≤ x)    ⇒   ⊢ sup(A, ℝ, < ) ∈ ℝ
Theorem	suprubi 4517	A member of a non-empty bounded set of reals is less than or equal to the set's upper bound.
⊢ (A ⊆ ℝ ∧ ¬ A = ∅ ∧ ∃x ∈ ℝ ∀y ∈ A y ≤ x)    ⇒   ⊢ (B ∈ A → B ≤ sup(A, ℝ, < ))
Theorem	suprlubi 4518	The supremum of a non-empty bounded set of reals is the least upper bound.
⊢ (A ⊆ ℝ ∧ ¬ A = ∅ ∧ ∃x ∈ ℝ ∀y ∈ A y ≤ x)    ⇒   ⊢ ((B ∈ ℝ ∧ B < sup(A, ℝ, < )) → ∃z ∈ A B < z)
Theorem	suprnubi 4519	An upper bound is not less than the supremum of a non-empty bounded set of reals.
⊢ (A ⊆ ℝ ∧ ¬ A = ∅ ∧ ∃x ∈ ℝ ∀y ∈ A y ≤ x)    ⇒   ⊢ ((B ∈ ℝ ∧ ∀z ∈ A ¬ B < z) → ¬ B < sup(A, ℝ, < ))
Theorem	nnunb 4520	The set of natural numbers is unbounded above. Theorem I.28 of [Apostol] p. 26.
⊢ ¬ ∃x ∈ ℝ ∀y ∈ ℕ (y < x ∨ y = x)
Theorem	arch 4521	Archimedean property of real numbers. For any real number, there is an integer greater than it. Theorem I.29 of [Apostol] p. 26.
⊢ (A ∈ ℝ → ∃x ∈ ℕ A < x)
Theorem	nnreclt 4522	There exists a natural number whose reciprocal is less than a given positive real. Exercise 3 of [Apostol] p. 28.
⊢ ((A ∈ ℝ ∧ 0 < A) → ∃x ∈ ℕ (1 / x) < A)
Theorem	avril1 4523	Poisson d'Avril's Theorem. This theorem is noted for its Selbstdokumentieren property, which means, literally, "self-documenting." (Contributed by Loof Lirpa 1-Apr-04.)
⊢ ¬ (A℘R(i ‘1) ∧ F∅(0 · 1))
Theorem	ine0 4524	The imaginary unit i is not zero.
⊢ ¬ i = 0
Theorem	isqm1 4525	i -squared is minus 1.
⊢ (i · i) = -1
Theorem	irec 4526	The reciprocal of i.
⊢ (1 / i) = -i
Theorem	inelr 4527	The imaginary unit i is not a real number.
⊢ ¬ i ∈ ℝ
Theorem	crulem 4528	The real representation of complex numbers is unique. Lemma for Proposition 10-1.3 of [Gleason] p. 130.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    &   ⊢ D ∈ ℝ    ⇒   ⊢ ((A + (B · i)) = (C + (D · i)) → B = D)
Theorem	cru 4529	The real representation of complex numbers is unique. Proposition 10-1.3 of [Gleason] p. 130.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    &   ⊢ D ∈ ℝ    ⇒   ⊢ ((A + (B · i)) = (C + (D · i)) → (A = C ∧ B = D))
Theorem	crmult 4530	Multiplication rule for complex number representation. Remark of [Apostol] p. 361.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    &   ⊢ D ∈ ℝ    ⇒   ⊢ ((A + (B · i)) · (C + (D · i))) = (((A · C) − (B · D)) + (((A · D) + (B · C)) · i))
Theorem	crut 4531	The real representation of complex numbers is unique. Proposition 10-1.3 of [Gleason] p. 130.
⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (C ∈ ℝ ∧ D ∈ ℝ)) → ((A + (B · i)) = (C + (D · i)) → (A = C ∧ B = D)))
Theorem	creur 4532	The real part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130.
⊢ (A ∈ ℂ → ∃!x ∈ ℝ ∃y ∈ ℝ A = (x + (y · i)))
Theorem	creui 4533	The imaginary part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130.
⊢ (A ∈ ℂ → ∃!y ∈ ℝ ∃x ∈ ℝ A = (x + (y · i)))
Theorem	rimul 4534	A real number times the imaginary unit is real only if the number is 0.
⊢ ((A ∈ ℝ ∧ (A · i) ∈ ℝ) → A = 0)
Definition	df-n0 4535	Define the set of nonnegative integers.
⊢ ℕ0 = (ℕ ∪ {0})
Theorem	elnn0 4536	Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-02.)
⊢ (A ∈ ℕ0 ↔ (A ∈ ℕ ∨ A = 0))
Theorem	nnssnn0 4537	Positive naturals are a subset of nonnegative integers. (Contributed by Raph Levien, 10-Dec-02.)
⊢ ℕ ⊆ ℕ0
Theorem	nn0ssre 4538	Nonnegative integers are a subset of the reals. (Contributed by Raph Levien, 10-Dec-02.)
⊢ ℕ0 ⊆ ℝ
Theorem	nn0sscn 4539	Nonnegative integers are a subset of the complex numbers.)
⊢ ℕ0 ⊆ ℂ
Theorem	nn0ex 4540	The set of nonnegative integers exists.
⊢ ℕ0 ∈ V
Theorem	nnnn0t 4541	A natural number is a nonnegative integer.
⊢ (A ∈ ℕ → A ∈ ℕ0)
Theorem	nn0ret 4542	A nonnegative integer is a real number.
⊢ (A ∈ ℕ0 → A ∈ ℝ)
Theorem	nn0cnt 4543	A nonnegative integer is a complex number.
⊢ (A ∈ ℕ0 → A ∈ ℂ)
Theorem	nn0re 4544	A nonnegative integer is a real number.
⊢ A ∈ ℕ0    ⇒   ⊢ A ∈ ℝ
Theorem	nn0cn 4545	A nonnegative integer is a complex number.
⊢ A ∈ ℕ0    ⇒   ⊢ A ∈ ℂ
Theorem	0nn0 4546	0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-02.)
⊢ 0 ∈ ℕ0
Theorem	1nn0 4547	1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-02.)
⊢ 1 ∈ ℕ0
Theorem	2nn0 4548	2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-02.)
⊢ 2 ∈ ℕ0
Theorem	lt0nnn0 4549	No number less than zero is a nonnegative integer.
⊢ ((A ∈ ℝ ∧ A < 0) → ¬ A ∈ ℕ0)
Theorem	nn0ge0t 4550	A nonnegative integer is greater than or equal to zero.
⊢ (A ∈ ℕ0 → 0 ≤ A)
Theorem	nn0addclt 4551	Closure of addition of nonnegative integers. (Contributed by Raph Levien, 10-Dec-02.)
⊢ ((A ∈ ℕ0 ∧ B ∈ ℕ0) → (A + B) ∈ ℕ0)
Theorem	nn0addcl 4552	Closure of addition of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-02.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    ⇒   ⊢ (A + B) ∈ ℕ0
Theorem	nn0mulcl 4553	Closure of multiplication of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-02.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    ⇒   ⊢ (A · B) ∈ ℕ0
Theorem	nn0mulclt 4554	Closure of multiplication of nonnegative integers.
⊢ ((A ∈ ℕ0 ∧ B ∈ ℕ0) → (A · B) ∈ ℕ0)
Theorem	peano2nn0 4555	Second Peano postulate for nonnegative integers.
⊢ (A ∈ ℕ0 → (A + 1) ∈ ℕ0)
Theorem	nn0ltp1let 4556	Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-02.)
⊢ ((A ∈ ℕ0 ∧ B ∈ ℕ0) → (A < B ↔ (A + 1) ≤ B))
Theorem	nn0leltp1t 4557	Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-04.)
⊢ ((A ∈ ℕ0 ∧ B ∈ ℕ0) → (A ≤ B ↔ A < (B + 1)))
Theorem	nn0ltlem1 4558	Nonnegative integer ordering relation.
⊢ ((A ∈ ℕ0 ∧ B ∈ ℕ0) → (A < B ↔ A ≤ (B − 1)))
Theorem	nn0ge0i 4559	Nonnegative integers are nonnegative. (Contributed by Raph Levien, 10-Dec-02.)
⊢ A ∈ ℕ0    ⇒   ⊢ 0 ≤ A
Theorem	nn0addge1 4560	A nonnegative integer is less than or equal to itself plus another. (Contributed by Raph Levien, 10-Dec-02.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    ⇒   ⊢ A ≤ (A + B)
Theorem	nn0addge2 4561	A nonnegative integer is less than or equal to itself plus another. (Contributed by Raph Levien, 10-Dec-02.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    ⇒   ⊢ B ≤ (A + B)
Theorem	nn0le2x 4562	A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-02.)
⊢ A ∈ ℕ0    ⇒   ⊢ A ≤ (2 · A)
Theorem	nn0lele2x 4563	'Less than or equal to' implies 'less than or equal to twice' for nonnegative integers. (Contributed by Raph Levien, 10-Dec-02.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    ⇒   ⊢ (B ≤ A → B ≤ (2 · A))
Definition	df-z 4564	Define the set of integers. Definition of integers in [Apostol] p. 22.
⊢ ℤ = {x ∈ ℝ∣(x = 0 ∨ x ∈ ℕ ∨ -x ∈ ℕ)}
Theorem	elz 4565	Membership in the set of integers.
⊢ (A ∈ ℤ ↔ (A ∈ ℝ ∧ (A = 0 ∨ A ∈ ℕ ∨ -A ∈ ℕ)))
Theorem	nnnegz 4566	The negative of a natural number is an integer.
⊢ (A ∈ ℕ → -A ∈ ℤ)
Theorem	zret 4567	An integer is a real.
⊢ (A ∈ ℤ → A ∈ ℝ)
Theorem	zcnt 4568	An integer is a complex number.
⊢ (A ∈ ℤ → A ∈ ℂ)
Theorem	zssre 4569	The integers are a subset of the reals.
⊢ ℤ ⊆ ℝ
Theorem	zsscn 4570	The integers are a subset of the complex numbers.
⊢ ℤ ⊆ ℂ
Theorem	zex 4571	The set of integers exists.
⊢ ℤ ∈ V
Theorem	elnnz 4572	Natural number property expressed in terms of integers.
⊢ (A ∈ ℕ ↔ (A ∈ ℤ ∧ 0 < A))
Theorem	0z 4573	Zero is an integer.
⊢ 0 ∈ ℤ
Theorem	elnn0z 4574	Nonnegative integer property expressed in terms of integers.
⊢ (A ∈ ℕ0 ↔ (A ∈ ℤ ∧ 0 ≤ A))
Theorem	elznn0nn 4575	Integer property expressed in terms nonnegative integers and natural numbers.
⊢ (A ∈ ℤ ↔ (A ∈ ℕ0 ∨ (A ∈ ℝ ∧ -A ∈ ℕ)))
Theorem	elznn0 4576	Integer property expressed in terms of nonnegative integers.
⊢ (A ∈ ℤ ↔ (A ∈ ℝ ∧ (A ∈ ℕ0 ∨ -A ∈ ℕ0)))
Theorem	nnssz 4577	Natural numbers are a subset of integers.
⊢ ℕ ⊆ ℤ
Theorem	nn0ssz 4578	Nonnegative integers are a subset of the integers.
⊢ ℕ0 ⊆ ℤ
Theorem	nnzt 4579	A natural number is an integer.
⊢ (A ∈ ℕ → A ∈ ℤ)
Theorem	nn0zt 4580	A nonnegative integer is an integer.
⊢ (A ∈ ℕ0 → A ∈ ℤ)
Theorem	elnnz1 4581	Natural number property expressed in terms of integers.
⊢ (A ∈ ℕ ↔ (A ∈ ℤ ∧ 1 ≤ A))
Theorem	nnz 4582	Natural numbers expressed as a subset of integers.
⊢ ℕ = {x ∈ ℤ∣1 ≤ x}
Theorem	nn0z 4583	Nonnegative integers expressed as a subset of integers.
⊢ ℕ0 = {x ∈ ℤ∣0 ≤ x}
Theorem	1z 4584	One is an integer.
⊢ 1 ∈ ℤ
Theorem	2z 4585	Two is an integer.
⊢ 2 ∈ ℤ
Theorem	halfnz 4586	One-half is not an integer.
⊢ ¬ (1 / 2) ∈ ℤ
Theorem	nn0subt 4587	Subtraction of nonnegative integers.
⊢ ((A ∈ ℕ0 ∧ B ∈ ℕ0) → (A ≤ B ↔ (B − A) ∈ ℕ0))
Theorem	znegclt 4588	Closure law for negative integers.
⊢ (A ∈ ℤ → -A ∈ ℤ)
Theorem	nn0negz 4589	The negative of a nonnegative integer is an integer.
⊢ (A ∈ ℕ0 → -A ∈ ℤ)
Theorem	zaddclt 4590	Closure of addition of integers.
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A + B) ∈ ℤ)
Theorem	zsubclt 4591	Closure of subtraction of integers.
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A − B) ∈ ℤ)
Theorem	zrevaddclt 4592	Reverse closure law for addition of integers.
⊢ (B ∈ ℤ → ((A ∈ ℂ ∧ (A + B) ∈ ℤ) ↔ A ∈ ℤ))
Theorem	elnn0nn 4593	The nonnegative integer property expressed in terms of natural numbers.
⊢ (A ∈ ℕ0 ↔ (A ∈ ℂ ∧ (A + 1) ∈ ℕ))
Theorem	elnnnn0 4594	The natural number property expressed in terms of nonnegative integers.
⊢ (A ∈ ℕ ↔ (A ∈ ℂ ∧ (A − 1) ∈ ℕ0))
Theorem	znnsubt 4595	The positive difference of unequal integers is a natural number. (Generalization of nnsubt 4451.)
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A < B ↔ (B − A) ∈ ℕ))
Theorem	zmulclt 4596	Closure of multiplication of integers.
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A · B) ∈ ℤ)
Theorem	zltp1let 4597	Integer ordering relation.
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A < B ↔ (A + 1) ≤ B))
Theorem	zleltp1t 4598	Integer ordering relation.
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A ≤ B ↔ A < (B + 1)))
Theorem	zlem1ltt 4599	Integer ordering relation.
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A ≤ B ↔ (A − 1) < B))
Theorem	sqznn 4600	The square of a non-zero integer is a natural number.
⊢ ((A ∈ ℤ ∧ A ≠ 0) → (A · A) ∈ ℕ)