α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ ¬p ∣ y → p ^ (i + 1) ∣ x
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ p ^ (i + 1) ∣ x ∨ p ∣ y
rw [or_iff_not_imp_right]
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
hy : ¬p ∣ y
⊢ p ^ (i + 1) ∣ x
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ ¬p ∣ y → p ^ (i + 1) ∣ x
intro hy
case zero
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i : ℕ
hxy✝ : p ^ (i + 1) ∣ x✝ * y
hy : ¬p ∣ y
x : α
hxy : p ^ (Nat.zero + 1) ∣ x * y
⊢ p ^ (Nat.zero + 1) ∣ x

case succ
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i✝ : ℕ
hxy✝ : p ^ (i✝ + 1) ∣ x✝ * y
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x : α
hxy : p ^ (Nat.succ i + 1) ∣ x * y
⊢ p ^ (Nat.succ i + 1) ∣ x
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
hy : ¬p ∣ y
⊢ p ^ (i + 1) ∣ x
induction' i with i ih generalizing x
case succ
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i✝ : ℕ
hxy✝ : p ^ (i✝ + 1) ∣ x✝ * y
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x : α
hxy : p * p ^ (i + 1) ∣ x * y
⊢ p * p ^ (i + 1) ∣ x
case succ
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i✝ : ℕ
hxy✝ : p ^ (i✝ + 1) ∣ x✝ * y
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x : α
hxy : p ^ (Nat.succ i + 1) ∣ x * y
⊢ p ^ (Nat.succ i + 1) ∣ x
rw [pow_succ] at hxy⊢
case succ.intro
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i✝ : ℕ
hxy✝ : p ^ (i✝ + 1) ∣ x * y
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x' : α
hxy : p * p ^ (i + 1) ∣ p * x' * y
⊢ p * p ^ (i + 1) ∣ p * x'
case succ
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i✝ : ℕ
hxy✝ : p ^ (i✝ + 1) ∣ x✝ * y
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x : α
hxy : p * p ^ (i + 1) ∣ x * y
⊢ p * p ^ (i + 1) ∣ x
obtain ⟨x', rfl⟩ := (h.dvd_or_dvd (dvd_of_mul_right_dvd hxy)).resolve_right hy
case succ.intro
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i✝ : ℕ
hxy✝ : p ^ (i✝ + 1) ∣ x * y
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x' : α
hxy : p * p ^ (i + 1) ∣ p * (x' * y)
⊢ p * p ^ (i + 1) ∣ p * x'
case succ.intro
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i✝ : ℕ
hxy✝ : p ^ (i✝ + 1) ∣ x * y
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x' : α
hxy : p * p ^ (i + 1) ∣ p * x' * y
⊢ p * p ^ (i + 1) ∣ p * x'
rw [mul_assoc] at hxy
no goals
case succ.intro
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i✝ : ℕ
hxy✝ : p ^ (i✝ + 1) ∣ x * y
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x' : α
hxy : p * p ^ (i + 1) ∣ p * (x' * y)
⊢ p * p ^ (i + 1) ∣ p * x'
exact mul_dvd_mul_left p (ih ((mul_dvd_mul_iff_left h.ne_zero).mp hxy))
case zero
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i : ℕ
hxy✝ : p ^ (i + 1) ∣ x✝ * y
hy : ¬p ∣ y
x : α
hxy : p ^ (Nat.zero + 1) ∣ x * y
⊢ p ^ (Nat.zero + 1) ∣ x
case zero
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i : ℕ
hxy✝ : p ^ (i + 1) ∣ x✝ * y
hy : ¬p ∣ y
x : α
hxy : p ^ (Nat.zero + 1) ∣ x * y
⊢ p ^ (Nat.zero + 1) ∣ x
simp only [zero_add, pow_one] at *
case zero
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i : ℕ
hxy✝ : p ^ (i + 1) ∣ x✝ * y
hy : ¬p ∣ y
x : α
hxy : p ^ (Nat.zero + 1) ∣ x * y
⊢ p ∣ x
case zero
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i : ℕ
hxy✝ : p ^ (i + 1) ∣ x✝ * y
hy : ¬p ∣ y
x : α
hxy : p ^ (Nat.zero + 1) ∣ x * y
⊢ p ^ (Nat.zero + 1) ∣ x
rw [pow_one]
case zero
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i : ℕ
hxy✝ : p ^ (i + 1) ∣ x✝ * y
hy : ¬p ∣ y
x : α
hxy : p ∣ x * y
⊢ p ∣ x
case zero
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i : ℕ
hxy✝ : p ^ (i + 1) ∣ x✝ * y
hy : ¬p ∣ y
x : α
hxy : p ^ (Nat.zero + 1) ∣ x * y
⊢ p ∣ x
rw [pow_one] at hxy
no goals
case zero
α✝ : Type ?u.61415
β : Type ?u.61418
γ : Type ?u.61421
δ : Type ?u.61424
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i : ℕ
hxy✝ : p ^ (i + 1) ∣ x✝ * y
hy : ¬p ∣ y
x : α
hxy : p ∣ x * y
⊢ p ∣ x
exact (h.dvd_or_dvd hxy).resolve_right hy