[STATEMENT]
lemma Infinitesimal_HFinite_mult:
  fixes x y :: "'a::real_normed_algebra star"
  assumes "x \<in> Infinitesimal" "y \<in> HFinite"
  shows "x * y \<in> Infinitesimal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<in> Infinitesimal
[PROOF STEP]
proof (rule InfinitesimalI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm (x * y) < r
[PROOF STEP]
obtain t where "hnorm y < t" "t \<in> Reals"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>hnorm y < t; t \<in> \<real>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using HFiniteD \<open>y \<in> HFinite\<close>
[PROOF STATE]
proof (prove)
using this:
?x \<in> HFinite \<Longrightarrow> \<exists>t\<in>\<real>. hnorm ?x < t
y \<in> HFinite

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>hnorm y < t; t \<in> \<real>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
hnorm y < t
t \<in> \<real>

goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm (x * y) < r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hnorm y < t
t \<in> \<real>
[PROOF STEP]
have "t > 0"
[PROOF STATE]
proof (prove)
using this:
hnorm y < t
t \<in> \<real>

goal (1 subgoal):
 1. 0 < t
[PROOF STEP]
using hnorm_ge_zero le_less_trans
[PROOF STATE]
proof (prove)
using this:
hnorm y < t
t \<in> \<real>
0 \<le> hnorm ?x
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. 0 < t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < t

goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm (x * y) < r
[PROOF STEP]
show "hnorm (x * y) < r"
    if "r \<in> \<real>" and "0 < r" for r :: "real star"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hnorm (x * y) < r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hnorm (x * y) < r
[PROOF STEP]
have "hnorm x < r/t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hnorm x < r / t
[PROOF STEP]
by (meson InfinitesimalD Reals_divide \<open>hnorm y < t\<close> \<open>t \<in> \<real>\<close> assms(1) divide_pos_pos hnorm_ge_zero le_less_trans that)
[PROOF STATE]
proof (state)
this:
hnorm x < r / t

goal (1 subgoal):
 1. hnorm (x * y) < r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hnorm x < r / t
[PROOF STEP]
have "hnorm (x * y) < (r / t) * t"
[PROOF STATE]
proof (prove)
using this:
hnorm x < r / t

goal (1 subgoal):
 1. hnorm (x * y) < r / t * t
[PROOF STEP]
using \<open>hnorm y < t\<close> hnorm_mult_less
[PROOF STATE]
proof (prove)
using this:
hnorm x < r / t
hnorm y < t
\<lbrakk>hnorm ?x < ?r; hnorm ?y < ?s\<rbrakk> \<Longrightarrow> hnorm (?x * ?y) < ?r * ?s

goal (1 subgoal):
 1. hnorm (x * y) < r / t * t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
hnorm (x * y) < r / t * t

goal (1 subgoal):
 1. hnorm (x * y) < r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hnorm (x * y) < r / t * t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hnorm (x * y) < r / t * t

goal (1 subgoal):
 1. hnorm (x * y) < r
[PROOF STEP]
using \<open>0 < t\<close>
[PROOF STATE]
proof (prove)
using this:
hnorm (x * y) < r / t * t
0 < t

goal (1 subgoal):
 1. hnorm (x * y) < r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hnorm (x * y) < r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?r \<in> \<real>; 0 < ?r\<rbrakk> \<Longrightarrow> hnorm (x * y) < ?r

goal:
No subgoals!
[PROOF STEP]
qed