R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
⊢ IsUnit (gcd x y)
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
⊢ IsCoprime x y
rw [← gcd_isUnit_iff]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
h : ¬IsUnit (gcd x y)
⊢ False
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
⊢ IsUnit (gcd x y)
by_contra h
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
h : ¬IsUnit (gcd x y)
⊢ gcd x y ≠ 0
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
h : ¬IsUnit (gcd x y)
⊢ False
refine' H _ h _ (gcd_dvd_left _ _) (gcd_dvd_right _ _)
no goals
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
h : ¬IsUnit (gcd x y)
⊢ gcd x y ≠ 0
rwa [Ne, gcd_eq_zero_iff]