Theory "product"

Parents iterate

Signature

Constant	Type
nproduct	:(α -> bool) -> (α -> num) -> num
product	:(α -> bool) -> (α -> real) -> real

Definitions

product

⊢ product = iterate $*

nproduct

⊢ nproduct = iterate $*

Theorems

th

⊢ (∀f g s. (∀x. x ∈ s ⇒ (f x = g x)) ⇒ (nproduct s (λi. f i) = nproduct s g)) ∧
  (∀f g a b.
       (∀i. a ≤ i ∧ i ≤ b ⇒ (f i = g i)) ⇒
       (nproduct (a .. b) (λi. f i) = nproduct (a .. b) g)) ∧
  ∀f g p.
      (∀x. p x ⇒ (f x = g x)) ⇒
      (nproduct {y | p y} (λi. f i) = nproduct {y | p y} g)

REAL_OF_NUM_NPRODUCT

⊢ ∀f s. FINITE s ⇒ (&nproduct s f = product s (λx. &f x))

REAL_ADD_AC

⊢ (m + n = n + m) ∧ (m + n + p = m + (n + p)) ∧ (m + (n + p) = n + (m + p))

PRODUCT_UNION

⊢ ∀f s t.
      FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
      (product (s ∪ t) f = product s f * product t f)

PRODUCT_SUPPORT

⊢ ∀f s. product (support $* f s) f = product s f

PRODUCT_SUPERSET

⊢ ∀f u v.
      u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ (f x = 1)) ⇒ (product v f = product u f)

PRODUCT_SING_NUMSEG

⊢ ∀f n. product (n .. n) f = f n

PRODUCT_SING

⊢ ∀f x. product {x} f = f x

PRODUCT_POS_LT_NUMSEG

⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 < f x) ⇒ 0 < product (m .. n) f

PRODUCT_POS_LT

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < product s f

PRODUCT_POS_LE_NUMSEG

⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 ≤ f x) ⇒ 0 ≤ product (m .. n) f

PRODUCT_POS_LE

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ product s f

PRODUCT_PAIR

⊢ ∀f m n.
      product (2 * m .. 2 * n + 1) f =
      product (m .. n) (λi. f (2 * i) * f (2 * i + 1))

PRODUCT_ONE

⊢ ∀s. product s (λn. 1) = 1

PRODUCT_OFFSET

⊢ ∀f m p. product (m + p .. n + p) f = product (m .. n) (λi. f (i + p))

PRODUCT_NEG_NUMSEG_1

⊢ ∀f n. product (1 .. n) (λi. -f i) = -1 pow n * product (1 .. n) f

PRODUCT_NEG_NUMSEG

⊢ ∀f m n.
      product (m .. n) (λi. -f i) = -1 pow (n + 1 − m) * product (m .. n) f

PRODUCT_NEG

⊢ ∀f s. FINITE s ⇒ (product s (λi. -f i) = -1 pow CARD s * product s f)

PRODUCT_MUL_NUMSEG

⊢ ∀f g m n.
      product (m .. n) (λx. f x * g x) =
      product (m .. n) f * product (m .. n) g

PRODUCT_MUL_GEN

⊢ ∀f g s.
      FINITE {x | x ∈ s ∧ f x ≠ 1} ∧ FINITE {x | x ∈ s ∧ g x ≠ 1} ⇒
      (product s (λx. f x * g x) = product s f * product s g)

PRODUCT_MUL

⊢ ∀f g s. FINITE s ⇒ (product s (λx. f x * g x) = product s f * product s g)

PRODUCT_LE_NUMSEG

⊢ ∀f m n.
      (∀i. m ≤ i ∧ i ≤ n ⇒ 0 ≤ f i ∧ f i ≤ g i) ⇒
      product (m .. n) f ≤ product (m .. n) g

PRODUCT_LE_1

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ 1) ⇒ product s f ≤ 1

PRODUCT_LE

⊢ ∀f s.
      FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ⇒ product s f ≤ product s g

PRODUCT_INV

⊢ ∀f s. FINITE s ⇒ (product s (λx. (f x)⁻¹) = (product s f)⁻¹)

PRODUCT_IMAGE

⊢ ∀f g s.
      (∀x y. x ∈ s ∧ y ∈ s ∧ (f x = f y) ⇒ (x = y)) ⇒
      (product (IMAGE f s) g = product s (g ∘ f))

PRODUCT_EQ_NUMSEG

⊢ ∀f g m n.
      (∀i. m ≤ i ∧ i ≤ n ⇒ (f i = g i)) ⇒
      (product (m .. n) f = product (m .. n) g)

PRODUCT_EQ_1_NUMSEG

⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ (f i = 1)) ⇒ (product (m .. n) f = 1)

PRODUCT_EQ_1

⊢ ∀f s. (∀x. x ∈ s ⇒ (f x = 1)) ⇒ (product s f = 1)

PRODUCT_EQ_0_NUMSEG

⊢ ∀f m n. (product (m .. n) f = 0) ⇔ ∃x. m ≤ x ∧ x ≤ n ∧ (f x = 0)

PRODUCT_EQ_0

⊢ ∀f s. FINITE s ⇒ ((product s f = 0) ⇔ ∃x. x ∈ s ∧ (f x = 0))

PRODUCT_EQ

⊢ ∀f g s. (∀x. x ∈ s ⇒ (f x = g x)) ⇒ (product s f = product s g)

PRODUCT_DIV_NUMSEG

⊢ ∀f g m n.
      product (m .. n) (λx. f x / g x) =
      product (m .. n) f / product (m .. n) g

PRODUCT_DIV

⊢ ∀f g s. FINITE s ⇒ (product s (λx. f x / g x) = product s f / product s g)

PRODUCT_DELTA

⊢ ∀s a. product s (λx. if x = a then b else 1) = if a ∈ s then b else 1

PRODUCT_DELETE

⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ (f a * product (s DELETE a) f = product s f)

PRODUCT_CONST_NUMSEG_1

⊢ ∀c n. product (1 .. n) (λx. c) = c pow n

PRODUCT_CONST_NUMSEG

⊢ ∀c m n. product (m .. n) (λx. c) = c pow (n + 1 − m)

PRODUCT_CONST

⊢ ∀c s. FINITE s ⇒ (product s (λx. c) = c pow CARD s)

PRODUCT_CONG

⊢ (∀f g s. (∀x. x ∈ s ⇒ (f x = g x)) ⇒ (product s (λi. f i) = product s g)) ∧
  (∀f g a b.
       (∀i. a ≤ i ∧ i ≤ b ⇒ (f i = g i)) ⇒
       (product (a .. b) (λi. f i) = product (a .. b) g)) ∧
  ∀f g p.
      (∀x. p x ⇒ (f x = g x)) ⇒
      (product {y | p y} (λi. f i) = product {y | p y} g)

PRODUCT_CLOSED

⊢ ∀P f s.
      P 1 ∧ (∀x y. P x ∧ P y ⇒ P (x * y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
      P (product s f)

PRODUCT_CLAUSES_RIGHT

⊢ ∀f m n. 0 < n ∧ m ≤ n ⇒ (product (m .. n) f = product (m .. n − 1) f * f n)

PRODUCT_CLAUSES_NUMSEG

⊢ (∀m. product (m .. 0) f = if m = 0 then f 0 else 1) ∧
  ∀m n.
      product (m .. SUC n) f =
      if m ≤ SUC n then product (m .. n) f * f (SUC n) else product (m .. n) f

PRODUCT_CLAUSES_LEFT

⊢ ∀f m n. m ≤ n ⇒ (product (m .. n) f = f m * product (m + 1 .. n) f)

PRODUCT_CLAUSES

⊢ (∀f. product ∅ f = 1) ∧
  ∀x f s.
      FINITE s ⇒
      (product (x INSERT s) f =
       if x ∈ s then product s f else f x * product s f)

PRODUCT_ADD_SPLIT

⊢ ∀f m n p.
      m ≤ n + 1 ⇒
      (product (m .. n + p) f =
       product (m .. n) f * product (n + 1 .. n + p) f)

PRODUCT_ABS

⊢ ∀f s. FINITE s ⇒ (product s (λx. abs (f x)) = abs (product s f))

NPRODUCT_UNION

⊢ ∀f s t.
      FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
      (nproduct (s ∪ t) f = nproduct s f * nproduct t f)

NPRODUCT_SUPPORT

⊢ ∀f s. nproduct (support $* f s) f = nproduct s f

NPRODUCT_SUPERSET

⊢ ∀f u v.
      u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ (f x = 1)) ⇒ (nproduct v f = nproduct u f)

NPRODUCT_SING_NUMSEG

⊢ ∀f n. nproduct (n .. n) f = f n

NPRODUCT_SING

⊢ ∀f x. nproduct {x} f = f x

NPRODUCT_POS_LT_NUMSEG

⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 < f x) ⇒ 0 < nproduct (m .. n) f

NPRODUCT_POS_LT

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < nproduct s f

NPRODUCT_PAIR

⊢ ∀f m n.
      nproduct (2 * m .. 2 * n + 1) f =
      nproduct (m .. n) (λi. f (2 * i) * f (2 * i + 1))

NPRODUCT_ONE

⊢ ∀s. nproduct s (λn. 1) = 1

NPRODUCT_OFFSET

⊢ ∀f m p. nproduct (m + p .. n + p) f = nproduct (m .. n) (λi. f (i + p))

NPRODUCT_MUL_NUMSEG

⊢ ∀f g m n.
      nproduct (m .. n) (λx. f x * g x) =
      nproduct (m .. n) f * nproduct (m .. n) g

NPRODUCT_MUL_GEN

⊢ ∀f g s.
      FINITE {x | x ∈ s ∧ f x ≠ 1} ∧ FINITE {x | x ∈ s ∧ g x ≠ 1} ⇒
      (nproduct s (λx. f x * g x) = nproduct s f * nproduct s g)

NPRODUCT_MUL

⊢ ∀f g s.
      FINITE s ⇒ (nproduct s (λx. f x * g x) = nproduct s f * nproduct s g)

NPRODUCT_LE_NUMSEG

⊢ ∀f m n.
      (∀i. m ≤ i ∧ i ≤ n ⇒ 0 ≤ f i ∧ f i ≤ g i) ⇒
      nproduct (m .. n) f ≤ nproduct (m .. n) g

NPRODUCT_LE

⊢ ∀f s.
      FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ⇒
      nproduct s f ≤ nproduct s g

NPRODUCT_IMAGE

⊢ ∀f g s.
      (∀x y. x ∈ s ∧ y ∈ s ∧ (f x = f y) ⇒ (x = y)) ⇒
      (nproduct (IMAGE f s) g = nproduct s (g ∘ f))

NPRODUCT_FACT

⊢ ∀n. nproduct (1 .. n) (λm. m) = FACT n

NPRODUCT_EQ_NUMSEG

⊢ ∀f g m n.
      (∀i. m ≤ i ∧ i ≤ n ⇒ (f i = g i)) ⇒
      (nproduct (m .. n) f = nproduct (m .. n) g)

NPRODUCT_EQ_1_NUMSEG

⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ (f i = 1)) ⇒ (nproduct (m .. n) f = 1)

NPRODUCT_EQ_1

⊢ ∀f s. (∀x. x ∈ s ⇒ (f x = 1)) ⇒ (nproduct s f = 1)

NPRODUCT_EQ_0_NUMSEG

⊢ ∀f m n. (nproduct (m .. n) f = 0) ⇔ ∃x. m ≤ x ∧ x ≤ n ∧ (f x = 0)

NPRODUCT_EQ_0

⊢ ∀f s. FINITE s ⇒ ((nproduct s f = 0) ⇔ ∃x. x ∈ s ∧ (f x = 0))

NPRODUCT_EQ

⊢ ∀f g s. (∀x. x ∈ s ⇒ (f x = g x)) ⇒ (nproduct s f = nproduct s g)

NPRODUCT_DELTA

⊢ ∀s a. nproduct s (λx. if x = a then b else 1) = if a ∈ s then b else 1

NPRODUCT_DELETE

⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ (f a * nproduct (s DELETE a) f = nproduct s f)

NPRODUCT_CONST_NUMSEG_1

⊢ ∀c n. nproduct (1 .. n) (λx. c) = c ** n

NPRODUCT_CONST_NUMSEG

⊢ ∀c m n. nproduct (m .. n) (λx. c) = c ** (n + 1 − m)

NPRODUCT_CONST

⊢ ∀c s. FINITE s ⇒ (nproduct s (λx. c) = c ** CARD s)

NPRODUCT_CLOSED

⊢ ∀P f s.
      P 1 ∧ (∀x y. P x ∧ P y ⇒ P (x * y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
      P (nproduct s f)

NPRODUCT_CLAUSES_RIGHT

⊢ ∀f m n.
      0 < n ∧ m ≤ n ⇒ (nproduct (m .. n) f = nproduct (m .. n − 1) f * f n)

NPRODUCT_CLAUSES_NUMSEG

⊢ (∀m. nproduct (m .. 0) f = if m = 0 then f 0 else 1) ∧
  ∀m n.
      nproduct (m .. SUC n) f =
      if m ≤ SUC n then nproduct (m .. n) f * f (SUC n)
      else nproduct (m .. n) f

NPRODUCT_CLAUSES_LEFT

⊢ ∀f m n. m ≤ n ⇒ (nproduct (m .. n) f = f m * nproduct (m + 1 .. n) f)

NPRODUCT_CLAUSES

⊢ (∀f. nproduct ∅ f = 1) ∧
  ∀x f s.
      FINITE s ⇒
      (nproduct (x INSERT s) f =
       if x ∈ s then nproduct s f else f x * nproduct s f)

NPRODUCT_ADD_SPLIT

⊢ ∀f m n p.
      m ≤ n + 1 ⇒
      (nproduct (m .. n + p) f =
       nproduct (m .. n) f * nproduct (n + 1 .. n + p) f)

MULT_AC

⊢ (m * n = n * m) ∧ (m * n * p = m * (n * p)) ∧ (m * (n * p) = n * (m * p))