/-
Copyright (c) 2022 Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bhavik Mehta

! This file was ported from Lean 3 source module algebra.is_prime_pow
! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Associated
import Mathlib.NumberTheory.Divisors

/-!
# Prime powers

This file deals with prime powers: numbers which are positive integer powers of a single prime.
-/


variable {R: Type ?u.14
R : Type _: Type (?u.83807+1)
Type _} [CommMonoidWithZero: Type ?u.58671 → Type ?u.58671
CommMonoidWithZero R: Type ?u.14
R] (n: R
n p: R
p : R: Type ?u.2
R) (k: ℕ
k : ℕ: Type
ℕ)

/-- `n` is a prime power if there is a prime `p` and a positive natural `k` such that `n` can be
written as `p^k`. -/
def IsPrimePow: {R : Type u_1} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow : Prop: Type
Prop :=
  ∃ (p: R
p : R: Type ?u.14
R)(k: ℕ
k : ℕ: Type
ℕ), Prime: {α : Type ?u.35} → [inst : CommMonoidWithZero α] → α → Prop
Prime p: R
p ∧ 0: ?m.47
0 < k: ℕ
k ∧ p: R
p ^ k: ℕ
k = n: R
n
#align is_prime_pow IsPrimePow: {R : Type u_1} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow

theorem isPrimePow_def: IsPrimePow n ↔ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
isPrimePow_def : IsPrimePow: {R : Type ?u.18636} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: R
n ↔ ∃ (p: R
p : R: Type ?u.18624
R)(k: ℕ
k : ℕ: Type
ℕ), Prime: {α : Type ?u.18654} → [inst : CommMonoidWithZero α] → α → Prop
Prime p: R
p ∧ 0: ?m.18659
0 < k: ℕ
k ∧ p: R
p ^ k: ℕ
k = n: R
n :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align is_prime_pow_def isPrimePow_def: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] (n : R), IsPrimePow n ↔ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
isPrimePow_def

/-- An equivalent definition for prime powers: `n` is a prime power iff there is a prime `p` and a
natural `k` such that `n` can be written as `p^(k+1)`. -/
theorem isPrimePow_iff_pow_succ: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] (n : R), IsPrimePow n ↔ ∃ p k, Prime p ∧ p ^ (k + 1) = n
isPrimePow_iff_pow_succ : IsPrimePow: {R : Type ?u.37245} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: R
n ↔ ∃ (p: R
p : R: Type ?u.37233
R)(k: ℕ
k : ℕ: Type
ℕ), Prime: {α : Type ?u.37263} → [inst : CommMonoidWithZero α] → α → Prop
Prime p: R
p ∧ p: R
p ^ (k: ℕ
k + 1: ?m.37274
1) = n: R
n :=
  (isPrimePow_def: ∀ {R : Type ?u.56002} [inst : CommMonoidWithZero R] (n : R), IsPrimePow n ↔ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
isPrimePow_def _: ?m.56003
_).trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans
    ⟨fun ⟨p: R
p, k: ℕ
k, hp: Prime p
hp, hk: 0 < k
hk, hn: p ^ k = n
hn⟩ => ⟨_: ?m.56133
_, _: ?m.56142
_, hp: Prime p
hp, by
Goals accomplished! 🐙 R: Type u_1

inst✝: CommMonoidWithZero R

n, p✝: R

k✝: ℕ

x✝: ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n

p: R

k: ℕ

hp: Prime p

hk: 0 < k

hn: p ^ k = n

p ^ (?m.56323 x✝ p k hp hk hn + 1) = nrwa [R: Type u_1

inst✝: CommMonoidWithZero R

n, p✝: R

k✝: ℕ

x✝: ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n

p: R

k: ℕ

hp: Prime p

hk: 0 < k

hn: p ^ k = n

p ^ (?m.56323 x✝ p k hp hk hn + 1) = nNat.sub_add_cancel: ∀ {n m : ℕ}, m ≤ n → n - m + m = n
Nat.sub_add_cancel hk: 0 < k
hkR: Type u_1

inst✝: CommMonoidWithZero R

n, p✝: R

k✝: ℕ

x✝: ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n

p: R

k: ℕ

hp: Prime p

hk: 0 < k

hn: p ^ k = n

p ^ k = n]R: Type u_1

inst✝: CommMonoidWithZero R

n, p✝: R

k✝: ℕ

x✝: ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n

p: R

k: ℕ

hp: Prime p

hk: 0 < k

hn: p ^ k = n

p ^ k = n⟩, fun ⟨p: R
p, k: ℕ
k, hp: Prime p
hp, hn: p ^ (k + 1) = n
hn⟩ =>
      ⟨_: ?m.56409
_, _: ?m.56418
_, hp: Prime p
hp, Nat.succ_pos': ∀ {n : ℕ}, 0 < Nat.succ n
Nat.succ_pos', hn: p ^ (k + 1) = n
hn⟩⟩
#align is_prime_pow_iff_pow_succ isPrimePow_iff_pow_succ: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] (n : R), IsPrimePow n ↔ ∃ p k, Prime p ∧ p ^ (k + 1) = n
isPrimePow_iff_pow_succ

theorem not_isPrimePow_zero: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : NoZeroDivisors R], ¬IsPrimePow 0
not_isPrimePow_zero [NoZeroDivisors: (M₀ : Type ?u.56650) → [inst : Mul M₀] → [inst : Zero M₀] → Prop
NoZeroDivisors R: Type ?u.56638
R] : ¬IsPrimePow: {R : Type ?u.57010} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow (0: ?m.57015
0 : R: Type ?u.56638
R) := by
Goals accomplished! 🐙
  R: Type u_1

inst✝¹: CommMonoidWithZero R

n, p: R

k: ℕ

inst✝: NoZeroDivisors R

¬IsPrimePow 0simp only [isPrimePow_def: ∀ {R : Type ?u.57070} [inst : CommMonoidWithZero R] (n : R), IsPrimePow n ↔ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
isPrimePow_def, not_exists: ∀ {α : Sort ?u.57086} {p : α → Prop}, (¬∃ x, p x) ↔ ∀ (x : α), ¬p x
not_exists, not_and': ∀ {a b : Prop}, ¬(a ∧ b) ↔ b → ¬a
not_and', and_imp: ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → c
and_imp]R: Type u_1

inst✝¹: CommMonoidWithZero R

n, p: R

k: ℕ

inst✝: NoZeroDivisors R

∀ (x : R) (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x
  R: Type u_1

inst✝¹: CommMonoidWithZero R

n, p: R

k: ℕ

inst✝: NoZeroDivisors R

¬IsPrimePow 0intro x: R
x n: ℕ
n _hn: 0 < n
_hn hx: x ^ n = 0
hxR: Type u_1

inst✝¹: CommMonoidWithZero R

n✝, p: R

k: ℕ

inst✝: NoZeroDivisors R

x: R

n: ℕ

_hn: 0 < n

hx: x ^ n = 0

¬Prime x
  R: Type u_1

inst✝¹: CommMonoidWithZero R

n, p: R

k: ℕ

inst✝: NoZeroDivisors R

¬IsPrimePow 0rw [R: Type u_1

inst✝¹: CommMonoidWithZero R

n✝, p: R

k: ℕ

inst✝: NoZeroDivisors R

x: R

n: ℕ

_hn: 0 < n

hx: x ^ n = 0

¬Prime xpow_eq_zero: ∀ {M : Type ?u.57401} [inst : MonoidWithZero M] [inst_1 : NoZeroDivisors M] {x : M} {n : ℕ}, x ^ n = 0 → x = 0
pow_eq_zero hx: x ^ n = 0
hxR: Type u_1

inst✝¹: CommMonoidWithZero R

n✝, p: R

k: ℕ

inst✝: NoZeroDivisors R

x: R

n: ℕ

_hn: 0 < n

hx: x ^ n = 0

¬Prime 0]R: Type u_1

inst✝¹: CommMonoidWithZero R

n✝, p: R

k: ℕ

inst✝: NoZeroDivisors R

x: R

n: ℕ

_hn: 0 < n

hx: x ^ n = 0

¬Prime 0
  R: Type u_1

inst✝¹: CommMonoidWithZero R

n, p: R

k: ℕ

inst✝: NoZeroDivisors R

¬IsPrimePow 0simp
Goals accomplished! 🐙
#align not_is_prime_pow_zero not_isPrimePow_zero: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : NoZeroDivisors R], ¬IsPrimePow 0
not_isPrimePow_zero

theorem IsPrimePow.not_unit: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : R}, IsPrimePow n → ¬IsUnit n
IsPrimePow.not_unit {n: R
n : R: Type ?u.57729
R} (h: IsPrimePow n
h : IsPrimePow: {R : Type ?u.57743} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: R
n) : ¬IsUnit: {M : Type ?u.57769} → [inst : Monoid M] → M → Prop
IsUnit n: R
n :=
  let ⟨_p: R
_p, _k: ℕ
_k, hp: Prime _p
hp, hk: 0 < _k
hk, hn: _p ^ _k = n
hn⟩ := h: IsPrimePow n
h
  hn: _p ^ _k = n
hn ▸ (isUnit_pow_iff: ∀ {M : Type ?u.58085} [inst : Monoid M] {a : M} {n : ℕ}, n ≠ 0 → (IsUnit (a ^ n) ↔ IsUnit a)
isUnit_pow_iff hk: 0 < _k
hk.ne': ∀ {α : Type ?u.58090} [inst : Preorder α] {x y : α}, x < y → y ≠ x
ne').not: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr hp: Prime _p
hp.not_unit: ∀ {α : Type ?u.58242} [inst : CommMonoidWithZero α] {p : α}, Prime p → ¬IsUnit p
not_unit
#align is_prime_pow.not_unit IsPrimePow.not_unit: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : R}, IsPrimePow n → ¬IsUnit n
IsPrimePow.not_unit

theorem IsUnit.not_isPrimePow: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : R}, IsUnit n → ¬IsPrimePow n
IsUnit.not_isPrimePow {n: R
n : R: Type ?u.58668
R} (h: IsUnit n
h : IsUnit: {M : Type ?u.58682} → [inst : Monoid M] → M → Prop
IsUnit n: R
n) : ¬IsPrimePow: {R : Type ?u.58939} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: R
n := fun h': ?m.58953
h' => h': ?m.58953
h'.not_unit: ∀ {R : Type ?u.58955} [inst : CommMonoidWithZero R] {n : R}, IsPrimePow n → ¬IsUnit n
not_unit h: IsUnit n
h
#align is_unit.not_is_prime_pow IsUnit.not_isPrimePow: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : R}, IsUnit n → ¬IsPrimePow n
IsUnit.not_isPrimePow

theorem not_isPrimePow_one: ¬IsPrimePow 1
not_isPrimePow_one : ¬IsPrimePow: {R : Type ?u.58996} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow (1: ?m.59001
1 : R: Type ?u.58984
R) :=
  isUnit_one: ∀ {M : Type ?u.59413} [inst : Monoid M], IsUnit 1
isUnit_one.not_isPrimePow: ∀ {R : Type ?u.59437} [inst : CommMonoidWithZero R] {n : R}, IsUnit n → ¬IsPrimePow n
not_isPrimePow
#align not_is_prime_pow_one not_isPrimePow_one: ∀ {R : Type u_1} [inst : CommMonoidWithZero R], ¬IsPrimePow 1
not_isPrimePow_one

theorem Prime.isPrimePow: ∀ {p : R}, Prime p → IsPrimePow p
Prime.isPrimePow {p: R
p : R: Type ?u.59707
R} (hp: Prime p
hp : Prime: {α : Type ?u.59721} → [inst : CommMonoidWithZero α] → α → Prop
Prime p: R
p) : IsPrimePow: {R : Type ?u.59747} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow p: R
p :=
  ⟨p: R
p, 1: ?m.59794
1, hp: Prime p
hp, zero_lt_one: ∀ {α : Type ?u.59818} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
  [inst_4 : NeZero 1], 0 < 1
zero_lt_one, by
Goals accomplished! 🐙 R: Type u_1

inst✝: CommMonoidWithZero R

n, p✝: R

k: ℕ

p: R

hp: Prime p

p ^ 1 = psimp
Goals accomplished! 🐙⟩
#align prime.is_prime_pow Prime.isPrimePow: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {p : R}, Prime p → IsPrimePow p
Prime.isPrimePow

theorem IsPrimePow.pow: ∀ {n : R}, IsPrimePow n → ∀ {k : ℕ}, k ≠ 0 → IsPrimePow (n ^ k)
IsPrimePow.pow {n: R
n : R: Type ?u.60643
R} (hn: IsPrimePow n
hn : IsPrimePow: {R : Type ?u.60657} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: R
n) {k: ℕ
k : ℕ: Type
ℕ} (hk: k ≠ 0
hk : k: ℕ
k ≠ 0: ?m.60688
0) : IsPrimePow: {R : Type ?u.60700} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow (n: R
n ^ k: ℕ
k) :=
  let ⟨p: R
p, k': ℕ
k', hp: Prime p
hp, hk': 0 < k'
hk', hn: p ^ k' = n
hn⟩ := hn: IsPrimePow n
hn
  ⟨p: R
p, k: ℕ
k * k': ℕ
k', hp: Prime p
hp, mul_pos: ∀ {α : Type ?u.79410} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulStrictMono α],
  0 < a → 0 < b → 0 < a * b
mul_pos hk: k ≠ 0
hk.bot_lt: ∀ {α : Type ?u.79689} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a ≠ ⊥ → ⊥ < a
bot_lt hk': 0 < k'
hk', by
Goals accomplished! 🐙 R: Type u_1

inst✝: CommMonoidWithZero R

n✝, p✝: R

k✝: ℕ

n: R

hn✝: IsPrimePow n

k: ℕ

hk: k ≠ 0

p: R

k': ℕ

hp: Prime p

hk': 0 < k'

hn: p ^ k' = n

p ^ (k * k') = n ^ krw [R: Type u_1

inst✝: CommMonoidWithZero R

n✝, p✝: R

k✝: ℕ

n: R

hn✝: IsPrimePow n

k: ℕ

hk: k ≠ 0

p: R

k': ℕ

hp: Prime p

hk': 0 < k'

hn: p ^ k' = n

p ^ (k * k') = n ^ kpow_mul': ∀ {M : Type ?u.80041} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ n) ^ m
pow_mul',R: Type u_1

inst✝: CommMonoidWithZero R

n✝, p✝: R

k✝: ℕ

n: R

hn✝: IsPrimePow n

k: ℕ

hk: k ≠ 0

p: R

k': ℕ

hp: Prime p

hk': 0 < k'

hn: p ^ k' = n

(p ^ k') ^ k = n ^ k R: Type u_1

inst✝: CommMonoidWithZero R

n✝, p✝: R

k✝: ℕ

n: R

hn✝: IsPrimePow n

k: ℕ

hk: k ≠ 0

p: R

k': ℕ

hp: Prime p

hk': 0 < k'

hn: p ^ k' = n

p ^ (k * k') = n ^ khn: p ^ k' = n
hnR: Type u_1

inst✝: CommMonoidWithZero R

n✝, p✝: R

k✝: ℕ

n: R

hn✝: IsPrimePow n

k: ℕ

hk: k ≠ 0

p: R

k': ℕ

hp: Prime p

hk': 0 < k'

hn: p ^ k' = n

n ^ k = n ^ k]
Goals accomplished! 🐙⟩
#align is_prime_pow.pow IsPrimePow.pow: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : R}, IsPrimePow n → ∀ {k : ℕ}, k ≠ 0 → IsPrimePow (n ^ k)
IsPrimePow.pow

theorem IsPrimePow.ne_zero: ∀ [inst : NoZeroDivisors R] {n : R}, IsPrimePow n → n ≠ 0
IsPrimePow.ne_zero [NoZeroDivisors: (M₀ : Type ?u.80378) → [inst : Mul M₀] → [inst : Zero M₀] → Prop
NoZeroDivisors R: Type ?u.80366
R] {n: R
n : R: Type ?u.80366
R} (h: IsPrimePow n
h : IsPrimePow: {R : Type ?u.80740} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: R
n) : n: R
n ≠ 0: ?m.80767
0 := fun t: ?m.80809
t =>
  not_isPrimePow_zero: ∀ {R : Type ?u.80811} [inst : CommMonoidWithZero R] [inst_1 : NoZeroDivisors R], ¬IsPrimePow 0
not_isPrimePow_zero (t: ?m.80809
t ▸ h: IsPrimePow n
h)
#align is_prime_pow.ne_zero IsPrimePow.ne_zero: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : NoZeroDivisors R] {n : R}, IsPrimePow n → n ≠ 0
IsPrimePow.ne_zero

theorem IsPrimePow.ne_one: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : R}, IsPrimePow n → n ≠ 1
IsPrimePow.ne_one {n: R
n : R: Type ?u.81038
R} (h: IsPrimePow n
h : IsPrimePow: {R : Type ?u.81052} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: R
n) : n: R
n ≠ 1: ?m.81081
1 := fun t: ?m.81491
t =>
  not_isPrimePow_one: ∀ {R : Type ?u.81493} [inst : CommMonoidWithZero R], ¬IsPrimePow 1
not_isPrimePow_one (t: ?m.81491
t ▸ h: IsPrimePow n
h)
#align is_prime_pow.ne_one IsPrimePow.ne_one: ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : R}, IsPrimePow n → n ≠ 1
IsPrimePow.ne_one

section Nat

theorem isPrimePow_nat_iff: ∀ (n : ℕ), IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
isPrimePow_nat_iff (n: ℕ
n : ℕ: Type
ℕ) : IsPrimePow: {R : Type ?u.81652} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: ℕ
n ↔ ∃ p: ℕ
p k: ℕ
k : ℕ: Type
ℕ, Nat.Prime: ℕ → Prop
Nat.Prime p: ℕ
p ∧ 0: ?m.81677
0 < k: ℕ
k ∧ p: ℕ
p ^ k: ℕ
k = n: ℕ
n := by
Goals accomplished! 🐙
  R: Type ?u.81638

inst✝: CommMonoidWithZero R

n✝, p: R

k, n: ℕ

IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = nsimp only [isPrimePow_def: ∀ {R : Type ?u.81773} [inst : CommMonoidWithZero R] (n : R), IsPrimePow n ↔ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
isPrimePow_def, Nat.prime_iff: ∀ {p : ℕ}, Nat.Prime p ↔ Prime p
Nat.prime_iff]
Goals accomplished! 🐙
#align is_prime_pow_nat_iff isPrimePow_nat_iff: ∀ (n : ℕ), IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
isPrimePow_nat_iff

theorem Nat.Prime.isPrimePow: ∀ {p : ℕ}, Prime p → IsPrimePow p
Nat.Prime.isPrimePow {p: ℕ
p : ℕ: Type
ℕ} (hp: Prime p
hp : p: ℕ
p.Prime: ℕ → Prop
Prime) : IsPrimePow: {R : Type ?u.82161} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow p: ℕ
p :=
  _root_.Prime.isPrimePow: ∀ {R : Type ?u.82195} [inst : CommMonoidWithZero R] {p : R}, _root_.Prime p → IsPrimePow p
_root_.Prime.isPrimePow (prime_iff: ∀ {p : ℕ}, Prime p ↔ _root_.Prime p
prime_iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp hp: Prime p
hp)
#align nat.prime.is_prime_pow Nat.Prime.isPrimePow: ∀ {p : ℕ}, Nat.Prime p → IsPrimePow p
Nat.Prime.isPrimePow

theorem isPrimePow_nat_iff_bounded: ∀ (n : ℕ), IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
isPrimePow_nat_iff_bounded (n: ℕ
n : ℕ: Type
ℕ) :
    IsPrimePow: {R : Type ?u.82241} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: ℕ
n ↔ ∃ p: ℕ
p : ℕ: Type
ℕ, p: ℕ
p ≤ n: ℕ
n ∧ ∃ k: ℕ
k : ℕ: Type
ℕ, k: ℕ
k ≤ n: ℕ
n ∧ p: ℕ
p.Prime: ℕ → Prop
Prime ∧ 0: ?m.82276
0 < k: ℕ
k ∧ p: ℕ
p ^ k: ℕ
k = n: ℕ
n := by
Goals accomplished! 🐙
  R: Type ?u.82227

inst✝: CommMonoidWithZero R

n✝, p: R

k, n: ℕ

IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = nrw [R: Type ?u.82227

inst✝: CommMonoidWithZero R

n✝, p: R

k, n: ℕ

IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = nisPrimePow_nat_iff: ∀ (n : ℕ), IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
isPrimePow_nat_iffR: Type ?u.82227

inst✝: CommMonoidWithZero R

n✝, p: R

k, n: ℕ

(∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n]R: Type ?u.82227

inst✝: CommMonoidWithZero R

n✝, p: R

k, n: ℕ

(∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
  R: Type ?u.82227

inst✝: CommMonoidWithZero R

n✝, p: R

k, n: ℕ

IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = nrefine' Iff.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
Iff.symm ⟨fun ⟨p: ℕ
p, _, k: ℕ
k, _, hp: Nat.Prime p
hp, hk: 0 < k
hk, hn: p ^ k = n
hn⟩ => ⟨p: ℕ
p, k: ℕ
k, hp: Nat.Prime p
hp, hk: 0 < k
hk, hn: p ^ k = n
hn⟩, _: ?m.82400 → ?m.82399
_⟩R: Type ?u.82227

inst✝: CommMonoidWithZero R

n✝, p: R

k, n: ℕ

(∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
  R: Type ?u.82227

inst✝: CommMonoidWithZero R

n✝, p: R

k, n: ℕ

IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = nrintro ⟨p, k, hp, hk, rfl⟩: Nat.Prime p ∧ 0 < k ∧ p ^ k = n
⟨p: ℕ
p⟨p, k, hp, hk, rfl⟩: Nat.Prime p ∧ 0 < k ∧ p ^ k = n
, k: ℕ
k⟨p, k, hp, hk, rfl⟩: Nat.Prime p ∧ 0 < k ∧ p ^ k = n
, hp: Nat.Prime p
hp⟨p, k, hp, hk, rfl⟩: Nat.Prime p ∧ 0 < k ∧ p ^ k = n
, hk: 0 < k
hk⟨p, k, hp, hk, rfl⟩: Nat.Prime p ∧ 0 < k ∧ p ^ k = n
, rfl: p ^ k = n
rfl⟨p, k, hp, hk, rfl⟩: Nat.Prime p ∧ 0 < k ∧ p ^ k = n
⟩R: Type ?u.82227

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

hk: 0 < k

intro.intro.intro.intro∃ p_1, p_1 ≤ p ^ k ∧ ∃ k_1, k_1 ≤ p ^ k ∧ Nat.Prime p_1 ∧ 0 < k_1 ∧ p_1 ^ k_1 = p ^ k
  R: Type ?u.82227

inst✝: CommMonoidWithZero R

n✝, p: R

k, n: ℕ

IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = nrefine' ⟨p: ℕ
p, _: ?m.82864
_, k: ℕ
k, (Nat.lt_pow_self: ∀ {p : ℕ}, 1 < p → ∀ (n : ℕ), n < p ^ n
Nat.lt_pow_self hp: Nat.Prime p
hp.one_lt: ∀ {p : ℕ}, Nat.Prime p → 1 < p
one_lt _: ℕ
_).le: ∀ {α : Type ?u.82894} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le, hp: Nat.Prime p
hp, hk: 0 < k
hk, rfl: ∀ {α : Sort ?u.83014} {a : α}, a = a
rfl⟩R: Type ?u.82227

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

hk: 0 < k

intro.intro.intro.introp ≤ p ^ k
  R: Type ?u.82227

inst✝: CommMonoidWithZero R

n✝, p: R

k, n: ℕ

IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = nconv =>
Goals accomplished! 🐙 R: Type ?u.82227

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

hk: 0 < k

intro.intro.intro.introp ≤ p ^ k{R: Type ?u.82227

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

hk: 0 < k

p ≤ p ^ k R: Type ?u.82227

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

hk: 0 < k

p ≤ p ^ klhsR: Type ?u.82227

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

hk: 0 < k

p;R: Type ?u.82227

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

hk: 0 < k

p R: Type ?u.82227

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

hk: 0 < k

p ≤ p ^ krw [R: Type ?u.82227

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

hk: 0 < k

p←(pow_one: ∀ {M : Type ?u.83058} [inst : Monoid M] (a : M), a ^ 1 = a
pow_one p: ℕ
p)R: Type ?u.82227

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

hk: 0 < k

p ^ 1]R: Type ?u.82227

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

hk: 0 < k

p ^ 1 }
Goals accomplished! 🐙
  R: Type ?u.82227

inst✝: CommMonoidWithZero R

n✝, p: R

k, n: ℕ

IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = nexact (Nat.pow_le_iff_le_right: ∀ {x m n : ℕ}, 2 ≤ x → (x ^ m ≤ x ^ n ↔ m ≤ n)
Nat.pow_le_iff_le_right hp: Nat.Prime p
hp.two_le: ∀ {p : ℕ}, Nat.Prime p → 2 ≤ p
two_le).mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr hk: 0 < k
hk
Goals accomplished! 🐙
#align is_prime_pow_nat_iff_bounded isPrimePow_nat_iff_bounded: ∀ (n : ℕ), IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
isPrimePow_nat_iff_bounded

instance: {n : ℕ} → Decidable (IsPrimePow n)
instance {n: ℕ
n : ℕ: Type
ℕ} : Decidable: Prop → Type
Decidable (IsPrimePow: {R : Type ?u.83287} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: ℕ
n) :=
  decidable_of_iff': {a : Prop} → (b : Prop) → (a ↔ b) → [inst : Decidable b] → Decidable a
decidable_of_iff' _: Prop
_ (isPrimePow_nat_iff_bounded: ∀ (n : ℕ), IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
isPrimePow_nat_iff_bounded n: ℕ
n)

theorem IsPrimePow.dvd: ∀ {n m : ℕ}, IsPrimePow n → m ∣ n → m ≠ 1 → IsPrimePow m
IsPrimePow.dvd {n: ℕ
n m: ℕ
m : ℕ: Type
ℕ} (hn: IsPrimePow n
hn : IsPrimePow: {R : Type ?u.83823} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: ℕ
n) (hm: m ∣ n
hm : m: ℕ
m ∣ n: ℕ
n) (hm₁: m ≠ 1
hm₁ : m: ℕ
m ≠ 1: ?m.83868
1) : IsPrimePow: {R : Type ?u.83880} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow m: ℕ
m := by
Goals accomplished! 🐙
  R: Type ?u.83807

inst✝: CommMonoidWithZero R

n✝, p: R

k, n, m: ℕ

hn: IsPrimePow n

hm: m ∣ n

hm₁: m ≠ 1

IsPrimePow mrw [R: Type ?u.83807

inst✝: CommMonoidWithZero R

n✝, p: R

k, n, m: ℕ

hn: IsPrimePow n

hm: m ∣ n

hm₁: m ≠ 1

IsPrimePow misPrimePow_nat_iff: ∀ (n : ℕ), IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
isPrimePow_nat_iffR: Type ?u.83807

inst✝: CommMonoidWithZero R

n✝, p: R

k, n, m: ℕ

hn: ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

hm: m ∣ n

hm₁: m ≠ 1

∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m]R: Type ?u.83807

inst✝: CommMonoidWithZero R

n✝, p: R

k, n, m: ℕ

hn: ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

hm: m ∣ n

hm₁: m ≠ 1

∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m at hn: IsPrimePow n
hn⊢R: Type ?u.83807

inst✝: CommMonoidWithZero R

n✝, p: R

k, n, m: ℕ

hn: ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

hm: m ∣ n

hm₁: m ≠ 1

∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m
  R: Type ?u.83807

inst✝: CommMonoidWithZero R

n✝, p: R

k, n, m: ℕ

hn: IsPrimePow n

hm: m ∣ n

hm₁: m ≠ 1

IsPrimePow mrcases hn: ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
hn with ⟨p, k, hp, _hk, rfl⟩: Nat.Prime p ∧ 0 < k ∧ p ^ k = n
⟨p: ℕ
p⟨p, k, hp, _hk, rfl⟩: Nat.Prime p ∧ 0 < k ∧ p ^ k = n
, k: ℕ
k⟨p, k, hp, _hk, rfl⟩: Nat.Prime p ∧ 0 < k ∧ p ^ k = n
, hp: Nat.Prime p
hp⟨p, k, hp, _hk, rfl⟩: Nat.Prime p ∧ 0 < k ∧ p ^ k = n
, _hk: 0 < k
_hk⟨p, k, hp, _hk, rfl⟩: Nat.Prime p ∧ 0 < k ∧ p ^ k = n
, rfl: p ^ k = n
rfl⟨p, k, hp, _hk, rfl⟩: Nat.Prime p ∧ 0 < k ∧ p ^ k = n
⟩R: Type ?u.83807

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, m: ℕ

hm₁: m ≠ 1

p, k: ℕ

hp: Nat.Prime p

_hk: 0 < k

hm: m ∣ p ^ k

intro.intro.intro.intro∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m
  R: Type ?u.83807

inst✝: CommMonoidWithZero R

n✝, p: R

k, n, m: ℕ

hn: IsPrimePow n

hm: m ∣ n

hm₁: m ≠ 1

IsPrimePow mobtain ⟨i, hik, rfl⟩: i ≤ k ∧ m = p ^ i
⟨i: ℕ
i⟨i, hik, rfl⟩: i ≤ k ∧ m = p ^ i
, hik: i ≤ k
hik⟨i, hik, rfl⟩: i ≤ k ∧ m = p ^ i
, rfl: m = p ^ i
rfl⟨i, hik, rfl⟩: i ≤ k ∧ m = p ^ i
⟩ := (Nat.dvd_prime_pow: ∀ {p : ℕ}, Nat.Prime p → ∀ {m i : ℕ}, i ∣ p ^ m ↔ ∃ k, k ≤ m ∧ i = p ^ k
Nat.dvd_prime_pow hp: Nat.Prime p
hp).1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 hm: m ∣ p ^ k
hmR: Type ?u.83807

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

_hk: 0 < k

i: ℕ

hik: i ≤ k

hm₁: p ^ i ≠ 1

hm: p ^ i ∣ p ^ k

intro.intro.intro.intro.intro.intro∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ i
  R: Type ?u.83807

inst✝: CommMonoidWithZero R

n✝, p: R

k, n, m: ℕ

hn: IsPrimePow n

hm: m ∣ n

hm₁: m ≠ 1

IsPrimePow mrefine' ⟨p: ℕ
p, i: ℕ
i, hp: Nat.Prime p
hp, _: ?m.84159
_, rfl: ∀ {α : Sort ?u.84162} {a : α}, a = a
rfl⟩R: Type ?u.83807

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

_hk: 0 < k

i: ℕ

hik: i ≤ k

hm₁: p ^ i ≠ 1

hm: p ^ i ∣ p ^ k

intro.intro.intro.intro.intro.intro0 < i
  R: Type ?u.83807

inst✝: CommMonoidWithZero R

n✝, p: R

k, n, m: ℕ

hn: IsPrimePow n

hm: m ∣ n

hm₁: m ≠ 1

IsPrimePow mapply Nat.pos_of_ne_zero: ∀ {n : ℕ}, n ≠ 0 → 0 < n
Nat.pos_of_ne_zeroR: Type ?u.83807

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

_hk: 0 < k

i: ℕ

hik: i ≤ k

hm₁: p ^ i ≠ 1

hm: p ^ i ∣ p ^ k

intro.intro.intro.intro.intro.intro.ai ≠ 0
  R: Type ?u.83807

inst✝: CommMonoidWithZero R

n✝, p: R

k, n, m: ℕ

hn: IsPrimePow n

hm: m ∣ n

hm₁: m ≠ 1

IsPrimePow mrintro rfl: i = 0
rflR: Type ?u.83807

inst✝: CommMonoidWithZero R

n, p✝: R

k✝, p, k: ℕ

hp: Nat.Prime p

_hk: 0 < k

hik: 0 ≤ k

hm₁: p ^ 0 ≠ 1

hm: p ^ 0 ∣ p ^ k

intro.intro.intro.intro.intro.intro.aFalse
  R: Type ?u.83807

inst✝: CommMonoidWithZero R

n✝, p: R

k, n, m: ℕ

hn: IsPrimePow n

hm: m ∣ n

hm₁: m ≠ 1

IsPrimePow msimp only [pow_zero: ∀ {M : Type ?u.84207} [inst : Monoid M] (a : M), a ^ 0 = 1
pow_zero, ne_eq: ∀ {α : Sort ?u.84224} (a b : α), (a ≠ b) = ¬a = b
ne_eq] at hm₁: p ^ 0 ≠ 1
hm₁
Goals accomplished! 🐙
#align is_prime_pow.dvd IsPrimePow.dvd: ∀ {n m : ℕ}, IsPrimePow n → m ∣ n → m ≠ 1 → IsPrimePow m
IsPrimePow.dvd

theorem Nat.disjoint_divisors_filter_isPrimePow: ∀ {a b : ℕ}, coprime a b → Disjoint (Finset.filter IsPrimePow (divisors a)) (Finset.filter IsPrimePow (divisors b))
Nat.disjoint_divisors_filter_isPrimePow {a: ℕ
a b: ℕ
b : ℕ: Type
ℕ} (hab: coprime a b
hab : a: ℕ
a.coprime: ℕ → ℕ → Prop
coprime b: ℕ
b) :
    Disjoint: {α : Type ?u.84436} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint (a: ℕ
a.divisors: ℕ → Finset ℕ
divisors.filter: {α : Type ?u.84518} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter IsPrimePow: {R : Type ?u.84525} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow) (b: ℕ
b.divisors: ℕ → Finset ℕ
divisors.filter: {α : Type ?u.84591} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter IsPrimePow: {R : Type ?u.84598} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow) := by
Goals accomplished! 🐙
  R: Type ?u.84416

inst✝: CommMonoidWithZero R

n, p: R

k, a, b: ℕ

hab: coprime a b

Disjoint (Finset.filter IsPrimePow (divisors a)) (Finset.filter IsPrimePow (divisors b))simp only [Finset.disjoint_left: ∀ {α : Type ?u.84683} {s t : Finset α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
Finset.disjoint_left, Finset.mem_filter: ∀ {α : Type ?u.84704} {p : α → Prop} [inst : DecidablePred p] {s : Finset α} {a : α},
  a ∈ Finset.filter p s ↔ a ∈ s ∧ p a
Finset.mem_filter, and_imp: ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → c
and_imp, Nat.mem_divisors: ∀ {n m : ℕ}, n ∈ divisors m ↔ n ∣ m ∧ m ≠ 0
Nat.mem_divisors, not_and: ∀ {a b : Prop}, ¬(a ∧ b) ↔ a → ¬b
not_and]R: Type ?u.84416

inst✝: CommMonoidWithZero R

n, p: R

k, a, b: ℕ

hab: coprime a b

∀ ⦃a_1 : ℕ⦄, a_1 ∣ a → a ≠ 0 → IsPrimePow a_1 → a_1 ∣ b → b ≠ 0 → ¬IsPrimePow a_1
  R: Type ?u.84416

inst✝: CommMonoidWithZero R

n, p: R

k, a, b: ℕ

hab: coprime a b

Disjoint (Finset.filter IsPrimePow (divisors a)) (Finset.filter IsPrimePow (divisors b))rintro n: ℕ
n han: n ∣ a
han _ha: a ≠ 0
_ha hn: IsPrimePow n
hn hbn: n ∣ b
hbn _hb: b ≠ 0
_hb -: IsPrimePow n
-R: Type ?u.84416

inst✝: CommMonoidWithZero R

n✝, p: R

k, a, b: ℕ

hab: coprime a b

n: ℕ

han: n ∣ a

_ha: a ≠ 0

hn: IsPrimePow n

hbn: n ∣ b

_hb: b ≠ 0

False
  R: Type ?u.84416

inst✝: CommMonoidWithZero R

n, p: R

k, a, b: ℕ

hab: coprime a b

Disjoint (Finset.filter IsPrimePow (divisors a)) (Finset.filter IsPrimePow (divisors b))exact hn: IsPrimePow n
hn.ne_one: ∀ {R : Type ?u.85099} [inst : CommMonoidWithZero R] {n : R}, IsPrimePow n → n ≠ 1
ne_one (Nat.eq_one_of_dvd_coprimes: ∀ {a b k : ℕ}, coprime a b → k ∣ a → k ∣ b → k = 1
Nat.eq_one_of_dvd_coprimes hab: coprime a b
hab han: n ∣ a
han hbn: n ∣ b
hbn)
Goals accomplished! 🐙
#align nat.disjoint_divisors_filter_prime_pow Nat.disjoint_divisors_filter_isPrimePow: ∀ {a b : ℕ},
  Nat.coprime a b → Disjoint (Finset.filter IsPrimePow (Nat.divisors a)) (Finset.filter IsPrimePow (Nat.divisors b))
Nat.disjoint_divisors_filter_isPrimePow

theorem IsPrimePow.two_le: ∀ {n : ℕ}, IsPrimePow n → 2 ≤ n
IsPrimePow.two_le : ∀ {n: ℕ
n : ℕ: Type
ℕ}, IsPrimePow: {R : Type ?u.85203} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: ℕ
n → 2: ?m.85235
2 ≤ n: ℕ
n
  | 0: ℕ
0, h: IsPrimePow 0
h => (not_isPrimePow_zero: ∀ {R : Type ?u.85296} [inst : CommMonoidWithZero R] [inst_1 : NoZeroDivisors R], ¬IsPrimePow 0
not_isPrimePow_zero h: IsPrimePow 0
h).elim: ∀ {C : Sort ?u.85320}, False → C
elim
  | 1: ℕ
1, h: IsPrimePow 1
h => (not_isPrimePow_one: ∀ {R : Type ?u.85344} [inst : CommMonoidWithZero R], ¬IsPrimePow 1
not_isPrimePow_one h: IsPrimePow 1
h).elim: ∀ {C : Sort ?u.85350}, False → C
elim
  | _n: ℕ
_n + 2, _ => le_add_self: ∀ {α : Type ?u.85443} [inst : CanonicallyOrderedAddMonoid α] {a b : α}, a ≤ b + a
le_add_self
#align is_prime_pow.two_le IsPrimePow.two_le: ∀ {n : ℕ}, IsPrimePow n → 2 ≤ n
IsPrimePow.two_le

theorem IsPrimePow.pos: ∀ {n : ℕ}, IsPrimePow n → 0 < n
IsPrimePow.pos {n: ℕ
n : ℕ: Type
ℕ} (hn: IsPrimePow n
hn : IsPrimePow: {R : Type ?u.85646} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: ℕ
n) : 0: ?m.85679
0 < n: ℕ
n :=
  pos_of_gt: ∀ {M : Type ?u.85717} [inst : CanonicallyOrderedAddMonoid M] {n m : M}, n < m → 0 < m
pos_of_gt hn: IsPrimePow n
hn.two_le: ∀ {n : ℕ}, IsPrimePow n → 2 ≤ n
two_le
#align is_prime_pow.pos IsPrimePow.pos: ∀ {n : ℕ}, IsPrimePow n → 0 < n
IsPrimePow.pos

theorem IsPrimePow.one_lt: ∀ {n : ℕ}, IsPrimePow n → 1 < n
IsPrimePow.one_lt {n: ℕ
n : ℕ: Type
ℕ} (h: IsPrimePow n
h : IsPrimePow: {R : Type ?u.85785} → [inst : CommMonoidWithZero R] → R → Prop
IsPrimePow n: ℕ
n) : 1: ?m.85818
1 < n: ℕ
n :=
  h: IsPrimePow n
h.two_le: ∀ {n : ℕ}, IsPrimePow n → 2 ≤ n
two_le
#align is_prime_pow.one_lt IsPrimePow.one_lt: ∀ {n : ℕ}, IsPrimePow n → 1 < n
IsPrimePow.one_lt

end Nat