case pos
a✝ b : Cardinal
n m : ℕ
a : Cardinal
h : ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n

case neg
a✝ b : Cardinal
n m : ℕ
a : Cardinal
h : ¬ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
a✝ b : Cardinal
n m : ℕ
a : Cardinal
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
by_cases h : ℵ₀ ≤ a
case neg
a✝ b : Cardinal
n m : ℕ
a : Cardinal
h : ¬ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ∃ n, a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
case neg
a✝ b : Cardinal
n m : ℕ
a : Cardinal
h : ¬ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
simp only [h, Nat.cast_inj, exists_eq_left', false_or_iff, isPrimePow_nat_iff]
case neg.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ IsPrimePow ↑a ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
case neg
a✝ b : Cardinal
n m : ℕ
a : Cardinal
h : ¬ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ∃ n, a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
lift a to ℕ using not_le.mp h
case neg.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ (∃ p k, Prime p ∧ 0 < k ∧ p ^ k = ↑a) ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
case neg.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ IsPrimePow ↑a ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
rw [isPrimePow_def]
case neg.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ (∃ p k, Prime p ∧ 0 < k ∧ p ^ k = ↑a) → ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
case neg.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ (∃ p k, Prime p ∧ 0 < k ∧ p ^ k = ↑a) ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
refine'
  ⟨_, fun ⟨n, han, p, k, hp, hk, h⟩ =>
        ⟨p, k, nat_is_prime_iff.2 hp, hk, by rw [han]; exact_mod_cast h⟩⟩
case neg.intro.intro.intro.intro.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
case neg.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ (∃ p k, Prime p ∧ 0 < k ∧ p ^ k = ↑a) → ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
rintro ⟨p, k, hp, hk, hpk⟩
case neg.intro.intro.intro.intro.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
key : p ^ 1 ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
case neg.intro.intro.intro.intro.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have key : p ^ 1 ≤ ↑a := by rw [←hpk]; apply power_le_power_left hp.ne_zero; exact_mod_cast hk
case neg.intro.intro.intro.intro.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
key : p ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
case neg.intro.intro.intro.intro.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
key : p ^ 1 ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
rw [power_one] at key
case neg.intro.intro.intro.intro.intro.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
k : ℕ
hk : 0 < k
p : ℕ
hp : Prime ↑p
hpk : ↑p ^ k = ↑a
key : ↑p ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
case neg.intro.intro.intro.intro.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
key : p ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
lift p to ℕ using key.trans_lt (nat_lt_aleph0 a)
no goals
case neg.intro.intro.intro.intro.intro.intro
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
k : ℕ
hk : 0 < k
p : ℕ
hp : Prime ↑p
hpk : ↑p ^ k = ↑a
key : ↑p ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
exact ⟨a, rfl, p, k, nat_is_prime_iff.mp hp, hk, by exact_mod_cast hpk⟩
no goals
case pos
a✝ b : Cardinal
n m : ℕ
a : Cardinal
h : ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
simp [h, (prime_of_aleph0_le h).isPrimePow]
a✝ b : Cardinal
n✝ m a : ℕ
h✝ : ¬ℵ₀ ≤ ↑a
x✝ : ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
n : ℕ
han : ↑a = ↑n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
h : p ^ k = n
⊢ ↑p ^ k = ↑n
a✝ b : Cardinal
n✝ m a : ℕ
h✝ : ¬ℵ₀ ≤ ↑a
x✝ : ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
n : ℕ
han : ↑a = ↑n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
h : p ^ k = n
⊢ ↑p ^ k = ↑a
rw [han]
no goals
a✝ b : Cardinal
n✝ m a : ℕ
h✝ : ¬ℵ₀ ≤ ↑a
x✝ : ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
n : ℕ
han : ↑a = ↑n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
h : p ^ k = n
⊢ ↑p ^ k = ↑n
exact_mod_cast h
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ p ^ 1 ≤ p ^ k
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ p ^ 1 ≤ ↑a
rw [←hpk]
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ 1 ≤ ↑k
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ p ^ 1 ≤ p ^ k
apply power_le_power_left hp.ne_zero
no goals
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ 1 ≤ ↑k
exact_mod_cast hk
no goals
a✝ b : Cardinal
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
k : ℕ
hk : 0 < k
p : ℕ
hp : Prime ↑p
hpk : ↑p ^ k = ↑a
key : ↑p ≤ ↑a
⊢ p ^ k = a
exact_mod_cast hpk