Metamath Proof Explorer - mmtheorems45

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 - 4401-4500 - Page 45 of 58

Type	Label	Description
Statement
Theorem	recgt0t 4401	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21.
⊢ (A ∈ ℝ → (0 < A → 0 < (1 / A)))
Theorem	divgt0t 4402	The ratio of two positive numbers is positive.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((0 < A ∧ 0 < B) → 0 < (A / B)))
Theorem	divge0t 4403	The ratio of nonnegative and positive numbers is nonnegative.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((0 ≤ A ∧ 0 < B) → 0 ≤ (A / B)))
Theorem	ltdivt 4404	Division of both sides of 'less than' by a positive number.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → (0 < C → (A < B ↔ (A / C) < (B / C))))
Theorem	ledivt 4405	Division of both sides of a less than or equal to relation by a positive number.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → (0 < C → (A ≤ B ↔ (A / C) ≤ (B / C))))
Theorem	ltmuldivt 4406	'Less than' relationship between division and multiplication.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → (0 < B → ((A · B) < C ↔ A < (C / B))))
Theorem	ltmuldiv2t 4407	'Less than' relationship between division and multiplication.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → (0 < A → ((A · B) < C ↔ B < (C / A))))
Theorem	ltdivmult 4408	'Less than' relationship between division and multiplication.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → (0 < B → ((A / B) < C ↔ A < (B · C))))
Theorem	ltreci 4409	The reciprocal of both sides of 'less than'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 0 < A    &   ⊢ 0 < B    ⇒   ⊢ (A < B ↔ (1 / B) < (1 / A))
Theorem	ltrec 4410	The reciprocal of both sides of 'less than'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 < A ∧ 0 < B) → (A < B ↔ (1 / B) < (1 / A)))
Theorem	lerec 4411	The reciprocal of both sides of 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 < A ∧ 0 < B) → (A ≤ B ↔ (1 / B) ≤ (1 / A)))
Theorem	ltdiv23i 4412	Swap denominator with other side of 'less than'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    &   ⊢ 0 < B    &   ⊢ 0 < C    ⇒   ⊢ ((A / B) < C ↔ (A / C) < B)
Theorem	ltdiv23 4413	Swap denominator with other side of 'less than'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((0 < B ∧ 0 < C) → ((A / B) < C ↔ (A / C) < B))
Theorem	lt2sq 4414	Two nonnegative numbers compare the same as their squares.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → (A < B ↔ (A · A) < (B · B)))
Theorem	le2sq 4415	Two nonnegative numbers compare the same as their squares.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → (A ≤ B ↔ (A · A) ≤ (B · B)))
Theorem	sq11 4416	The square of a nonnegative number is a one-to-one function.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → ((A · A) = (B · B) ↔ A = B))
Theorem	ltrect 4417	The reciprocal of both sides of 'less than'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((0 < A ∧ 0 < B) → (A < B ↔ (1 / B) < (1 / A))))
Theorem	lerect 4418	The reciprocal of both sides of 'less than or equal to'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((0 < A ∧ 0 < B) → (A ≤ B ↔ (1 / B) ≤ (1 / A))))
Theorem	ltdiv23t 4419	Swap denominator with other side of 'less than'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → ((0 < B ∧ 0 < C) → ((A / B) < C ↔ (A / C) < B)))
Theorem	le2sqt 4420	Two nonnegative numbers compare the same as their squares.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((0 ≤ A ∧ 0 ≤ B) → (A ≤ B ↔ (A · A) ≤ (B · B))))
Theorem	halfpos 4421	A positive number is greater than its half.
⊢ A ∈ ℝ    ⇒   ⊢ (0 < A ↔ (A / (1 + 1)) < A)
Theorem	posex 4422	There exists a positive number less than two others.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 0 < A    &   ⊢ 0 < B    ⇒   ⊢ ∃x ∈ ℝ (0 < x ∧ (x < A ∧ x < B))
Definition	df-n 4423	The natural numbers of analysis start at one (unlike the natural numbers of set theory, i.e. the members of set omega, which start at zero). This is the convention used by most analysis books, and it also convenient for proofs in that we never have to worry about division by zero. See nnind 4434 for the principle of mathematical induction. Definition of positive integers in [Apostol] p. 22.
⊢ ℕ = ∩{x∣(1 ∈ x ∧ ∀y(y ∈ x → (y + 1) ∈ x))}
Theorem	peano5nn 4424	Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of [Apostol] p. 34.
⊢ A ∈ V    ⇒   ⊢ ((1 ∈ A ∧ ∀x(x ∈ A → (x + 1) ∈ A)) → ℕ ⊆ A)
Theorem	nnssre 4425	The natural numbers are a subset of the reals.
⊢ ℕ ⊆ ℝ
Theorem	nnsscn 4426	The natural numbers are a subset of the complex numbers.
⊢ ℕ ⊆ ℂ
Theorem	nnret 4427	A natural number is a real number.
⊢ (A ∈ ℕ → A ∈ ℝ)
Theorem	nncnt 4428	A natural number is a complex number.
⊢ (A ∈ ℕ → A ∈ ℂ)
Theorem	nnre 4429	A natural number is a real number.
⊢ A ∈ ℕ    ⇒   ⊢ A ∈ ℝ
Theorem	nncn 4430	A natural number is a complex number.
⊢ A ∈ ℕ    ⇒   ⊢ A ∈ ℂ
Theorem	nnex 4431	The set of natural numbers exists.
⊢ ℕ ∈ V
Theorem	1nn 4432	Peano postulate: 1 is a natural number.
⊢ 1 ∈ ℕ
Theorem	peano2nn 4433	Peano postulate: a successor of a natural number is a natural number.
⊢ (A ∈ ℕ → (A + 1) ∈ ℕ)
Theorem	nnind 4434	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 hypothesis. See nnaddclt 4436 for an example of its use.
⊢ (x = 1 → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (y + 1) → (φ ↔ θ))    &   ⊢ (x = A → (φ ↔ τ))    &   ⊢ ψ    &   ⊢ (y ∈ ℕ → (χ → θ))    ⇒   ⊢ (A ∈ ℕ → τ)
Theorem	nn1suc 4435	If a statement holds for 1 and also holds for a successor, it holds for all natural numbers. The first three hypotheses give us the substitution instances we need; the last two show that it holds for 1 and for a successor.
⊢ (x = 1 → (φ ↔ ψ))    &   ⊢ (x = (y + 1) → (φ ↔ χ))    &   ⊢ (x = A → (φ ↔ θ))    &   ⊢ ψ    &   ⊢ (y ∈ ℕ → χ)    ⇒   ⊢ (A ∈ ℕ → θ)
Theorem	nnaddclt 4436	Closure of addition of natural numbers, proved by induction on the second addend.
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A + B) ∈ ℕ)
Theorem	nnmulclt 4437	Closure of multiplication of natural numbers.
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A · B) ∈ ℕ)
Theorem	nn2get 4438	There exists a natural number greater than or equal to any two others.
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → ∃x ∈ ℕ (A ≤ x ∧ B ≤ x))
Theorem	nnge1t 4439	A natural number is one or greater.
⊢ (A ∈ ℕ → 1 ≤ A)
Theorem	nngt1ne1t 4440	A natural number is greater than one iff it is not equal to one.
⊢ (A ∈ ℕ → (1 < A ↔ ¬ A = 1))
Theorem	nngt0t 4441	A natural number is positive.
⊢ (A ∈ ℕ → 0 < A)
Theorem	lt1nnn 4442	A number less than one is not a natural number.
⊢ ((A ∈ ℝ ∧ A < 1) → ¬ A ∈ ℕ)
Theorem	0nnn 4443	Zero is not a natural number.
⊢ ¬ 0 ∈ ℕ
Theorem	nnne0t 4444	A natural number is non-zero.
⊢ (A ∈ ℕ → A ≠ 0)
Theorem	nngt0 4445	A natural number is positive (inference version).
⊢ A ∈ ℕ    ⇒   ⊢ 0 < A
Theorem	nnne0 4446	A natural number is non-zero (inference version).
⊢ A ∈ ℕ    ⇒   ⊢ A ≠ 0
Theorem	nnrecgt0t 4447	The reciprocal of a natural number is positive.
⊢ (A ∈ ℕ → 0 < (1 / A))
Theorem	nnleltp1t 4448	Natural number ordering relation.
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A ≤ B ↔ A < (B + 1)))
Theorem	nnltp1let 4449	Natural number ordering relation.
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A < B ↔ (A + 1) ≤ B))
Theorem	nnsub 4450	Subtraction of natural numbers.
⊢ A ∈ ℕ    &   ⊢ B ∈ ℕ    ⇒   ⊢ (A < B ↔ (B − A) ∈ ℕ)
Theorem	nnsubt 4451	Subtraction of natural numbers.
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A < B ↔ (B − A) ∈ ℕ))
Theorem	nnaddm1clt 4452	Closure of addition of natural numbers minus one.
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → ((A + B) − 1) ∈ ℕ)
Theorem	nndiv 4453	Two ways to express "A divides B" for natural numbers.
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (∃x ∈ ℕ (A · x) = B ↔ (B / A) ∈ ℕ))
Syntax	c2 4454	Extend class notation to include the number 2.
class 2
Syntax	c3 4455	Extend class notation to include the number 3.
class 3
Syntax	c4 4456	Extend class notation to include the number 4.
class 4
Syntax	c5 4457	Extend class notation to include the number 5.
class 5
Syntax	c6 4458	Extend class notation to include the number 6.
class 6
Syntax	c7 4459	Extend class notation to include the number 7.
class 7
Syntax	c8 4460	Extend class notation to include the number 8.
class 8
Syntax	c9 4461	Extend class notation to include the number 9.
class 9
Definition	df-2 4462	Define the number 2. Note that the numbers 0 and 1 are primitive constants of the complex number axiom system (see df-0 4035 and df-1 4036). Note: The decimal representation of numbers will undergo a major revision at some point in the future, and the old rather clumsy development has been deleted. For now, every number that is needed should be exhibited as an explicit expression built from operations on the digits 0 through 9. For example, 350 can be expressed as ((7↑3) + 7).
⊢ 2 = (1 + 1)
Definition	df-3 4463	Define the number 3.
⊢ 3 = (2 + 1)
Definition	df-4 4464	Define the number 4.
⊢ 4 = (3 + 1)
Definition	df-5 4465	Define the number 5.
⊢ 5 = (4 + 1)
Definition	df-6 4466	Define the number 6.
⊢ 6 = (5 + 1)
Definition	df-7 4467	Define the number 7.
⊢ 7 = (6 + 1)
Definition	df-8 4468	Define the number 8.
⊢ 8 = (7 + 1)
Definition	df-9 4469	Define the number 9.
⊢ 9 = (8 + 1)
Theorem	2re 4470	The number 2 is real.
⊢ 2 ∈ ℝ
Theorem	2cn 4471	The number 2 is a complex number.
⊢ 2 ∈ ℂ
Theorem	3re 4472	The number 3 is real.
⊢ 3 ∈ ℝ
Theorem	4re 4473	The number 4 is real.
⊢ 4 ∈ ℝ
Theorem	5re 4474	The number 5 is real.
⊢ 5 ∈ ℝ
Theorem	6re 4475	The number 6 is real.
⊢ 6 ∈ ℝ
Theorem	7re 4476	The number 7 is real.
⊢ 7 ∈ ℝ
Theorem	8re 4477	The number 8 is real.
⊢ 8 ∈ ℝ
Theorem	9re 4478	The number 9 is real.
⊢ 9 ∈ ℝ
Theorem	2pos 4479	The number 2 is positive.
⊢ 0 < 2
Theorem	3pos 4480	The number 3 is positive.
⊢ 0 < 3
Theorem	4pos 4481	The number 4 is positive.
⊢ 0 < 4
Theorem	5pos 4482	The number 5 is positive.
⊢ 0 < 5
Theorem	6pos 4483	The number 6 is positive.
⊢ 0 < 6
Theorem	7pos 4484	The number 7 is positive.
⊢ 0 < 7
Theorem	8pos 4485	The number 8 is positive.
⊢ 0 < 8
Theorem	9pos 4486	The number 9 is positive.
⊢ 0 < 9
Theorem	2nn 4487	2 is a natural number.
⊢ 2 ∈ ℕ
Theorem	2p2e4 4488	Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page.
⊢ (2 + 2) = 4
Theorem	2times 4489	Two times a number.
⊢ A ∈ ℂ    ⇒   ⊢ (2 · A) = (A + A)
Theorem	2timest 4490	Two times a number.
⊢ (A ∈ ℂ → (2 · A) = (A + A))
Theorem	times2 4491	A number times 2.
⊢ A ∈ ℂ    ⇒   ⊢ (A · 2) = (A + A)
Theorem	3p2e5 4492	3 + 2 = 5.
⊢ (3 + 2) = 5
Theorem	3p3e6 4493	3 + 3 = 6.
⊢ (3 + 3) = 6
Theorem	4p2e6 4494	4 + 2 = 6.
⊢ (4 + 2) = 6
Theorem	4p3e7 4495	4 + 3 = 7.
⊢ (4 + 3) = 7
Theorem	4p4e8 4496	4 + 4 = 8.
⊢ (4 + 4) = 8
Theorem	5p2e7 4497	5 + 2 = 7.
⊢ (5 + 2) = 7
Theorem	5p3e8 4498	5 + 3 = 8.
⊢ (5 + 3) = 8
Theorem	5p4e9 4499	5 + 4 = 9.
⊢ (5 + 4) = 9
Theorem	6p2e8 4500	6 + 2 = 8.
⊢ (6 + 2) = 8