Thm* a,b: , e:({a..b }  ). b a  ( i:{a..b }. e(i)) = 0 | [sum_via_intseg_null] |
Thm* a,b: , e:({a..b }  ). b a  ( i:{a..b }. e(i)) = 1 | [mul_via_intseg_null] |
Thm* ( i:{a..b }. e(i) = 0)  ( i:{a..b }. e(i)) = 0 | [zero_ann_iter_via_intseg] |
Thm* ( i:{a..b }. e(i)) = 0  ( i:{a..b }. e(i) = 0) | [iter_prod_zero_iff_factor_zero] |
Thm* e:({a..b }  ). ( i:{a..b }. e(i)) = 1  ( i:{a..b }. e(i) = 1) | [iter_nat_prod_one_iff_factors_one] |
Thm* a,b: , P:({a..b } Prop). ( i:{a..b }. P(i))  (Or i:{a..b }. P(i)) | [exist_intseg_vs_iter_or] |
Thm* a,b: , P:({a..b } Prop). ( i:{a..b }. P(i))  (And i:{a..b }. P(i)) | [all_intseg_vs_iter_and] |
Thm* a,b: , e:({a..b }  ).
Thm* a<b  ( i:{a..b }. e(i)) = ( i:{a..b-1 }. e(i))+e(b-1) | [sum_via_intseg_split_last] |
Thm* a,b,c: . (a b) c = a c b c | [exp_reduce1] |
Thm* a,b: , f,g:({a..b }  ).
Thm* ( i:{a..b }. f(i)) ( i:{a..b }. g(i)) = ( i:{a..b }. f(i) g(i)) | [mul_via_intseg_factors] |
Thm* a,b: , e:({a..b }  ).
Thm* a<b  ( i:{a..b }. e(i)) = ( i:{a..b-1 }. e(i)) e(b-1) | [mul_via_intseg_split_last] |
Thm* i: , x,y: . i x i y = i (x+y) | [sum_exponent] |
Thm* a,c,b: , e:({a..b }  ).
Thm* a c
Thm* 
Thm* c b  ( i:{a..b }. e(i)) = ( i:{a..c }. e(i)) ( i:{c..b }. e(i)) | [mul_via_intseg_split_mid] |
Thm* a,c,b: , e:({a..b }  ).
Thm* a c
Thm* 
Thm* c b  ( i:{a..b }. e(i)) = ( i:{a..c }. e(i))+( i:{c..b }. e(i)) | [sum_via_intseg_split_mid] |
Thm* a,b: , e:({a..b }  ), i:{a..b }. e(i) | ( i:{a..b }. e(i)) | [components_divide_iter_mul] |
Thm* a,c,b: , e:({a..b }  ).
Thm* a c
Thm* 
Thm* c<b
Thm* 
Thm* ( i:{a..b }. e(i)) = ( i:{a..c }. e(i)) e(c) ( i:{c+1..b }. e(i)) | [mul_via_intseg_split_pluck] |
Thm* a,c,b: , e:({a..b }  ).
Thm* a c
Thm* 
Thm* c<b
Thm* 
Thm* ( i:{a..b }. e(i)) = ( i:{a..c }. e(i))+e(c)+( i:{c+1..b }. e(i)) | [sum_via_intseg_split_pluck] |
Thm* f:(A A A), u:A.
Thm* is_ident(A; f; u)
Thm* 
Thm* is_assoc_sep(A; f)
Thm* 
Thm* ( a,c,b: , e:({a..b } A).
Thm* (a c
Thm* (
Thm* (c<b
Thm* (
Thm* ((Iter(f;u) i:{a..b }. e(i))
Thm* (=
Thm* (f((Iter(f;u) i:{a..c }. e(i)),f(e(c),Iter(f;u) i:{c+1..b }. e(i)))) | [iter_via_intseg_split_pluck] |
Thm* f:(A A A), u:A.
Thm* is_ident(A; f; u)
Thm* 
Thm* is_assoc_sep(A; f)
Thm* 
Thm* ( a,b: , c:{a...b}, d:{c..b }, e:({a..b } A).
Thm* (( i:{a..b }. i<c d i  e(i) = u)
Thm* (
Thm* ((Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) i:{c..d }. e(i))) | [iter_via_intseg_amputate_units] |
Thm* f:(A A A), u:A.
Thm* is_ident(A; f; u)
Thm* 
Thm* is_assoc_sep(A; f)
Thm* 
Thm* ( a,c,b: , e:({a..b } A).
Thm* (a c
Thm* (
Thm* (c b
Thm* (
Thm* ((Iter(f;u) i:{a..b }. e(i))
Thm* (=
Thm* (f((Iter(f;u) i:{a..c }. e(i)),Iter(f;u) i:{c..b }. e(i))) | [iter_via_intseg_split_mid] |
Thm* a,b: , f,g:({a..b }  ).
Thm* ( i:{a..b }. f(i))+( i:{a..b }. g(i)) = ( i:{a..b }. f(i)+g(i)) | [add_via_intseg_addends] |
Thm* f:(A A A), u:A.
Thm* is_commutative_sep(A; f)
Thm* 
Thm* is_ident(A; f; u)
Thm* 
Thm* is_assoc_sep(A; f)
Thm* 
Thm* ( a,b: , e,g:({a..b } A).
Thm* (f((Iter(f;u) i:{a..b }. e(i)),Iter(f;u) i:{a..b }. g(i))
Thm* (=
Thm* ((Iter(f;u) i:{a..b }. f(e(i),g(i)))
Thm* ( A) | [iter_via_intseg_comp_binop] |
Thm* f:(A A A), u:A, a,b,c,d: .
Thm* b-a = d-c
Thm* 
Thm* ( e:({a..b } A), g:({c..d } A).
Thm* (( i:{a..b }, j:{c..d }. j-i = c-a  e(i) = g(j) A)
Thm* (
Thm* ((Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) j:{c..d }. g(j))) | [iter_via_intseg_shift] |
Thm* f:(A A A), u:A, a,b: , e:({a..b } A), k: .
Thm* (Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) j:{a+k..b+k }. e(j-k)) | [iter_via_intseg_shift_rw] |
Thm* x: . 1 x = 1 | [one_exponentiation] |
Thm* a,b: , e:({a..b }  ). ( i:{a..b }. e(i) = 1)  ( i:{a..b }. e(i)) = 1 | [mul_via_intseg_one] |
Thm* f:(A A A), u:A.
Thm* is_ident(A; f; u)
Thm* 
Thm* ( a,b: , e:({a..b } A).
Thm* (( i:{a..b }. e(i) = u)  (Iter(f;u) i:{a..b }. e(i)) = u) | [iter_via_intseg_all_units] |
Thm* f:(A A A), u:A, a,b: , e:({a..b } A).
Thm* a<b
Thm* 
Thm* (Iter(f;u) i:{a..b }. e(i)) = f((Iter(f;u) i:{a..b-1 }. e(i)),e(b-1)) | [iter_via_intseg_split_last] |
Thm* a,b: , e:({a..b }  ).
Thm* a<b  ( c: . b = c+1  ( i:{a..b }. e(i)) = ( i:{a..c }. e(i))+e(c)) | [sum_via_intseg_notnull] |
Thm* a,b: , e:({a..b }  ).
Thm* a<b  ( c: . b = c+1  ( i:{a..b }. e(i)) = ( i:{a..c }. e(i)) e(c)) | [mul_via_intseg_notnull] |
Thm* f:(A A A), u:A, a,b: , e:({a..b } A).
Thm* a<b
Thm* 
Thm* ( c: .
Thm* (b = c+1
Thm* (
Thm* ((Iter(f;u) i:{a..b }. e(i)) = f((Iter(f;u) i:{a..c }. e(i)),e(c))) | [iter_via_intseg_notnull] |
Thm* a,b: , e:({a..b }  ). a+1 = b  ( i:{a..b }. e(i)) = e(a) | [mul_via_intseg_singleton] |
Thm* a,b: , e:({a..b }  ). a+1 = b  ( i:{a..b }. e(i)) = e(a) | [sum_via_intseg_singleton] |
Thm* f:(A A A), u:A.
Thm* is_ident(A; f; u)
Thm* 
Thm* ( a,b: , e:({a..b } A). a+1 = b  (Iter(f;u) i:{a..b }. e(i)) = e(a)) | [iter_via_intseg_singleton] |
Thm* f:(A A A), u:A, a,b: , e:({a..b } A).
Thm* b a  (Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) i:{a..a }. e(i)) | [iter_via_intseg_nullnorm] |
Thm* f:(A A A), u:A, a,b: , e:({a..b } A).
Thm* b a  (Iter(f;u) i:{a..b }. e(i)) = u | [iter_via_intseg_null] |
Thm* x: . x 1 = x | [exponent_one] |
Thm* x: . x 0 = 1 | [exponent_zero] |
Def k!m == i:{k-m..k }. i+1 | [factorial_tail_via_iter] |