 Home Intuitionistic Logic ExplorerTheorem List (p. 84 of 95) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 8301-8400   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremuz2mulcl 8301 Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012.)
((𝑀 (ℤ‘2) 𝑁 (ℤ‘2)) → (𝑀 · 𝑁) (ℤ‘2))

Theoremindstr2 8302* Strong Mathematical Induction for positive integers (inference schema). The first two hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 21-Nov-2012.)
(x = 1 → (φχ))    &   (x = y → (φψ))    &   χ    &   (x (ℤ‘2) → (y ℕ (y < xψ) → φ))       (x ℕ → φ)

Theoremeluzdc 8303 Membership of an integer in an upper set of integers is decidable. (Contributed by Jim Kingdon, 18-Apr-2020.)
((𝑀 𝑁 ℤ) → DECID 𝑁 (ℤ𝑀))

Theoremublbneg 8304* The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011.)
(x y A yxx y {z ℝ ∣ -z A}xy)

Theoremeqreznegel 8305* Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.)
(A ⊆ ℤ → {z ℝ ∣ -z A} = {z ℤ ∣ -z A})

Theoremnegm 8306* The image under negation of an inhabited set of reals is inhabited. (Contributed by Jim Kingdon, 10-Apr-2020.)
((A ⊆ ℝ x x A) → y y {z ℝ ∣ -z A})

Theoremlbzbi 8307* If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.)
(A ⊆ ℝ → (x y A xyx y A xy))

Theoremnn01to3 8308 A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed by Alexander van der Vekens, 13-Sep-2018.)
((𝑁 0 1 ≤ 𝑁 𝑁 ≤ 3) → (𝑁 = 1 𝑁 = 2 𝑁 = 3))

Theoremnn0ge2m1nnALT 8309 Alternate proof of nn0ge2m1nn 7998: If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. This version is proved using eluz2 8235, a theorem for upper sets of integers, which are defined later than the positive and nonnegative integers. This proof is, however, much shorter than the proof of nn0ge2m1nn 7998. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
((𝑁 0 2 ≤ 𝑁) → (𝑁 − 1) ℕ)

3.4.11  Rational numbers (as a subset of complex numbers)

Syntaxcq 8310 Extend class notation to include the class of rationals.
class

Definitiondf-q 8311 Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 8313 for the relation "is rational." (Contributed by NM, 8-Jan-2002.)
ℚ = ( / “ (ℤ × ℕ))

Theoremdivfnzn 8312 Division restricted to ℤ × ℕ is a function. Given excluded middle, it would be easy to prove this for ℂ × (ℂ ∖ {0}). The key difference is that an element of is apart from zero, whereas being an element of ℂ ∖ {0} implies being not equal to zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
( / ↾ (ℤ × ℕ)) Fn (ℤ × ℕ)

Theoremelq 8313* Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.)
(A ℚ ↔ x y A = (x / y))

Theoremqmulz 8314* If A is rational, then some integer multiple of it is an integer. (Contributed by NM, 7-Nov-2008.) (Revised by Mario Carneiro, 22-Jul-2014.)
(A ℚ → x ℕ (A · x) ℤ)

Theoremznq 8315 The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.)
((A B ℕ) → (A / B) ℚ)

Theoremqre 8316 A rational number is a real number. (Contributed by NM, 14-Nov-2002.)
(A ℚ → A ℝ)

Theoremzq 8317 An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
(A ℤ → A ℚ)

Theoremzssq 8318 The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.)
ℤ ⊆ ℚ

Theoremnn0ssq 8319 The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
0 ⊆ ℚ

Theoremnnssq 8320 The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.)
ℕ ⊆ ℚ

Theoremqssre 8321 The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.)
ℚ ⊆ ℝ

Theoremqsscn 8322 The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
ℚ ⊆ ℂ

Theoremqex 8323 The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
V

Theoremnnq 8324 A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
(A ℕ → A ℚ)

Theoremqcn 8325 A rational number is a complex number. (Contributed by NM, 2-Aug-2004.)
(A ℚ → A ℂ)

((A B ℚ) → (A + B) ℚ)

Theoremqnegcl 8327 Closure law for the negative of a rational. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
(A ℚ → -A ℚ)

Theoremqmulcl 8328 Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.)
((A B ℚ) → (A · B) ℚ)

Theoremqsubcl 8329 Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
((A B ℚ) → (AB) ℚ)

Theoremqapne 8330 Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 20-Mar-2020.)
((A B ℚ) → (A # BAB))

Theoremqreccl 8331 Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
((A A ≠ 0) → (1 / A) ℚ)

Theoremqdivcl 8332 Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
((A B B ≠ 0) → (A / B) ℚ)

Theoremqrevaddcl 8333 Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004.)
(B ℚ → ((A (A + B) ℚ) ↔ A ℚ))

Theoremnnrecq 8334 The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.)
(A ℕ → (1 / A) ℚ)

Theoremirradd 8335 The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008.)
((A (ℝ ∖ ℚ) B ℚ) → (A + B) (ℝ ∖ ℚ))

Theoremirrmul 8336 The product of a real which is not rational with a nonzero rational is not rational. Note that by "not rational" we mean the negation of "is rational" (whereas "irrational" is often defined to mean apart from any rational number - given excluded middle these two definitions would be equivalent). (Contributed by NM, 7-Nov-2008.)
((A (ℝ ∖ ℚ) B B ≠ 0) → (A · B) (ℝ ∖ ℚ))

3.4.12  Complex numbers as pairs of reals

Theoremcnref1o 8337* There is a natural one-to-one mapping from (ℝ × ℝ) to , where we map x, y to (x + (i · y)). In our construction of the complex numbers, this is in fact our definition of (see df-c 6697), but in the axiomatic treatment we can only show that there is the expected mapping between these two sets. (Contributed by Mario Carneiro, 16-Jun-2013.) (Revised by Mario Carneiro, 17-Feb-2014.)
𝐹 = (x ℝ, y ℝ ↦ (x + (i · y)))       𝐹:(ℝ × ℝ)–1-1-onto→ℂ

3.5  Order sets

3.5.1  Positive reals (as a subset of complex numbers)

Syntaxcrp 8338 Extend class notation to include the class of positive reals.
class +

Definitiondf-rp 8339 Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
+ = {x ℝ ∣ 0 < x}

Theoremelrp 8340 Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
(A + ↔ (A 0 < A))

Theoremelrpii 8341 Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.)
A     &   0 < A       A +

Theorem1rp 8342 1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
1 +

Theorem2rp 8343 2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
2 +

Theoremrpre 8344 A positive real is a real. (Contributed by NM, 27-Oct-2007.)
(A +A ℝ)

Theoremrpxr 8345 A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)
(A +A *)

Theoremrpcn 8346 A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
(A +A ℂ)

Theoremnnrp 8347 A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)
(A ℕ → A +)

Theoremrpssre 8348 The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)
+ ⊆ ℝ

Theoremrpgt0 8349 A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)
(A + → 0 < A)

Theoremrpge0 8350 A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.)
(A + → 0 ≤ A)

Theoremrpregt0 8351 A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
(A + → (A 0 < A))

Theoremrprege0 8352 A positive real is a nonnegative real number. (Contributed by Mario Carneiro, 31-Jan-2014.)
(A + → (A 0 ≤ A))

Theoremrpne0 8353 A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
(A +A ≠ 0)

Theoremrpap0 8354 A positive real is apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
(A +A # 0)

Theoremrprene0 8355 A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.)
(A + → (A A ≠ 0))

Theoremrpreap0 8356 A positive real is a real number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
(A + → (A A # 0))

Theoremrpcnne0 8357 A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.)
(A + → (A A ≠ 0))

Theoremrpcnap0 8358 A positive real is a complex number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
(A + → (A A # 0))

Theoremralrp 8359 Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
(x + φx ℝ (0 < xφ))

Theoremrexrp 8360 Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014.)
(x + φx ℝ (0 < x φ))

Theoremrpaddcl 8361 Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
((A + B +) → (A + B) +)

Theoremrpmulcl 8362 Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
((A + B +) → (A · B) +)

Theoremrpdivcl 8363 Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007.)
((A + B +) → (A / B) +)

Theoremrpreccl 8364 Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.)
(A + → (1 / A) +)

Theoremrphalfcl 8365 Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.)
(A + → (A / 2) +)

Theoremrpgecl 8366 A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)
((A + B AB) → B +)

Theoremrphalflt 8367 Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.)
(A + → (A / 2) < A)

Theoremrerpdivcl 8368 Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008.)
((A B +) → (A / B) ℝ)

Theoremge0p1rp 8369 A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015.)
((A 0 ≤ A) → (A + 1) +)

Theoremrpnegap 8370 Either a real apart from zero or its negation is a positive real, but not both. (Contributed by Jim Kingdon, 23-Mar-2020.)
((A A # 0) → (A + ⊻ -A +))

Theorem0nrp 8371 Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
¬ 0 +

Theoremltsubrp 8372 Subtracting a positive real from another number decreases it. (Contributed by FL, 27-Dec-2007.)
((A B +) → (AB) < A)

Theoremltaddrp 8373 Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.)
((A B +) → A < (A + B))

Theoremdifrp 8374 Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014.)
((A B ℝ) → (A < B ↔ (BA) +))

Theoremelrpd 8375 Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φ → 0 < A)       (φA +)

Theoremnnrpd 8376 A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℕ)       (φA +)

Theoremrpred 8377 A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φA ℝ)

Theoremrpxrd 8378 A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φA *)

Theoremrpcnd 8379 A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φA ℂ)

Theoremrpgt0d 8380 A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φ → 0 < A)

Theoremrpge0d 8381 A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φ → 0 ≤ A)

Theoremrpne0d 8382 A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φA ≠ 0)

Theoremrpregt0d 8383 A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φ → (A 0 < A))

Theoremrprege0d 8384 A positive real is real and greater or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φ → (A 0 ≤ A))

Theoremrprene0d 8385 A positive real is a nonzero real number. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φ → (A A ≠ 0))

Theoremrpcnne0d 8386 A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φ → (A A ≠ 0))

Theoremrpreccld 8387 Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φ → (1 / A) +)

Theoremrprecred 8388 Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φ → (1 / A) ℝ)

Theoremrphalfcld 8389 Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φ → (A / 2) +)

Theoremreclt1d 8390 The reciprocal of a positive number less than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φ → (A < 1 ↔ 1 < (1 / A)))

Theoremrecgt1d 8391 The reciprocal of a positive number greater than 1 is less than 1. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)       (φ → (1 < A ↔ (1 / A) < 1))

Theoremrpaddcld 8392 Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)    &   (φB +)       (φ → (A + B) +)

Theoremrpmulcld 8393 Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)    &   (φB +)       (φ → (A · B) +)

Theoremrpdivcld 8394 Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)    &   (φB +)       (φ → (A / B) +)

Theoremltrecd 8395 The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)    &   (φB +)       (φ → (A < B ↔ (1 / B) < (1 / A)))

Theoremlerecd 8396 The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)    &   (φB +)       (φ → (AB ↔ (1 / B) ≤ (1 / A)))

Theoremltrec1d 8397 Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)    &   (φB +)    &   (φ → (1 / A) < B)       (φ → (1 / B) < A)

Theoremlerec2d 8398 Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)    &   (φB +)    &   (φA ≤ (1 / B))       (φB ≤ (1 / A))

Theoremlediv2ad 8399 Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)    &   (φB +)    &   (φ𝐶 ℝ)    &   (φ → 0 ≤ 𝐶)    &   (φAB)       (φ → (𝐶 / B) ≤ (𝐶 / A))

Theoremltdiv2d 8400 Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)    &   (φB +)    &   (φ𝐶 +)       (φ → (A < B ↔ (𝐶 / B) < (𝐶 / A)))

Page List
Jump to page: Contents  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-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9427
 Copyright terms: Public domain < Previous  Next >