Zulip Chat Archive

Stream: new members

Topic: Composite not prime


Dev-Indra (Apr 26 2020 at 16:26):

Here is a converse lemma I'm trying to prove (composite ==> not prime)

def dvd (m n: ): Prop :=  k, n = m * k
def prime (p : ) : Prop := p  2   n, dvd n p  n = 1  n = p
def composite (d : ): Prop:=  (a b: ), d = a*b  a  b  b < d

lemma greater_than_not_zero (n : )(n  2): n  0:=
begin
    exact lattice.ne_bot_of_gt H,
end

lemma dvd_n_less_than_n (u n : ) (ha: dvd u n) (hb: u  1) (hc: u  n) (hn : n  0) : u < n :=
begin
  refine lt_of_le_of_ne _ hc,
  rcases ha with k, rfl,
  simpa using nat.mul_le_mul_left _ (_:1≤_),
  refine nat.pos_iff_ne_zero.2 (mt _ hn),
  rintro rfl, refl,
end

lemma composite_not_prime (n: ) (ge: n 2): (¬ (prime n)  composite n) :=
begin
       intros h,
      rw composite at h,
      by_contradiction,
      rw prime at a,

      cases h with a1 ha1,
      cases ha1 with b hb,
end

My tactic state is :

1 goal
n : ,
ge : n  2,
a : n  2   (n_1 : ), dvd n_1  n  n_1 = 1  n_1 = n,
a1 b : ,
hb : n = a1 * b  a1  b  b < n
 false

How do I extract the from for all the variable n_1 and use b as my n_1?

Dev-Indra (Apr 26 2020 at 16:46):

actually, this was my lemma:

lemma composite_not_prime (n: ) (ge: n 2): ( composite n ==> ¬ (prime n) ) :=
begin
       intros h,
      rw composite at h,
      by_contradiction,
      rw prime at a,

      cases h with a1 ha1,
      cases ha1 with b hb,
end

Kevin Buzzard (Apr 26 2020 at 17:45):

[solved in different thread]


Last updated: Dec 20 2023 at 11:08 UTC