Theorem: HTPI.phi_is_numElts (HTPILib/Chap8Part2.lean)

State before:
m : ℕ
⊢ numElts (Set_rp_below m) (phi m)
Tactic:
rewrite [numElts_def]
State after:
m : ℕ
⊢ I (phi m) ∼ Set_rp_below m

State before:
m : ℕ
⊢ I (phi m) ∼ Set_rp_below m
Tactic:
have h1 : ∀ n ∈ Set_rp_below m, n < m := by
  fix n : Nat
  assume h2 : n ∈ Set_rp_below m
  define at h2
  show n < m from h2.right
  done
State after:
m : ℕ
h1 : ∀ n ∈ Set_rp_below m, n < m
⊢ I (phi m) ∼ Set_rp_below m

State before:
m : ℕ
h1 : ∀ n ∈ Set_rp_below m, n < m
⊢ I (phi m) ∼ Set_rp_below m
Tactic:
have h2 : num_elts_below (Set_rp_below m) m (phi m) := neb_phi m
State after:
m : ℕ
h1 : ∀ n ∈ Set_rp_below m, n < m
h2 : num_elts_below (Set_rp_below m) m (phi m)
⊢ I (phi m) ∼ Set_rp_below m

State before:
m : ℕ
h1 : ∀ n ∈ Set_rp_below m, n < m
h2 : num_elts_below (Set_rp_below m) m (phi m)
⊢ I (phi m) ∼ Set_rp_below m
Tactic:
show I (phi m) ∼ Set_rp_below m from bdd_subset_nat h1 h2
State after:
no goals

State before:
m : ℕ
⊢ ∀ n ∈ Set_rp_below m, n < m
Tactic:
fix n : Nat
State after:
m n : ℕ
⊢ n ∈ Set_rp_below m → n < m

State before:
m n : ℕ
⊢ n ∈ Set_rp_below m → n < m
Tactic:
assume h2 : n ∈ Set_rp_below m
State after:
m n : ℕ
h2 : n ∈ Set_rp_below m
⊢ n < m

State before:
m n : ℕ
h2 : n ∈ Set_rp_below m
⊢ n < m
Tactic:
define at h2
State after:
m n : ℕ
h2 : rel_prime m n ∧ n < m
⊢ n < m

State before:
m n : ℕ
h2 : rel_prime m n ∧ n < m
⊢ n < m
Tactic:
show n < m from h2.right
State after:
no goals