natseg

　よって今度は

find_theorems "setprod ?f ?A * setprod ?f ?B"

とすれば使えそうな定理

Big_Operators.setprod_Un_disjoint:
finite ?A ⟹
finite ?B ⟹
?A ∩ ?B = {} ⟹ setprod ?g (?A ∪ ?B) = setprod ?g ?A * setprod ?g ?B

が見付かりますので，これを用いる為に定義域を直和に分割する補題

  have natseg [simp]:
  "{Suc m..m + 2 * 2 ^ N} = union {Suc m..m + 2 ^ N} {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N}"
    by auto

をhave "GM a m (2 ^ Suc N... に先立って作っておきます．またこのように [simp]，つまり，simpやautoが自動参照する属性を与えておくと

proof (simp add: real_root_mult_exp real_root_mult)

のOutputが

goal (1 subgoal):
1. setprod a ({Suc m..m + 2 ^ N} ∪ {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N}) =
setprod a {Suc m..m + 2 ^ N} *
setprod a {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N}

となるので，上の定理が直ちに使えて

by (simp add: real_root_mult_exp real_root_mult setprod_Un_disjoint)

で証明完了です．