[GOAL]
⊢ φ 1 = 1
[PROOFSTEP]
simp [totient]
[GOAL]
n : ℕ
⊢ φ n = Nat.card ↑{m | m < n ∧ coprime n m}
[PROOFSTEP]
let e : {m | m < n ∧ n.coprime m} ≃ Finset.filter n.coprime (Finset.range n) :=
  { toFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using m.property⟩
    invFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using m.property⟩
    left_inv := fun m => by simp only [Subtype.coe_mk, Subtype.coe_eta]
    right_inv := fun m => by simp only [Subtype.coe_mk, Subtype.coe_eta] }
[GOAL]
n : ℕ
m : ↑{m | m < n ∧ coprime n m}
⊢ ↑m ∈ filter (coprime n) (range n)
[PROOFSTEP]
simpa only [Finset.mem_filter, Finset.mem_range] using m.property
[GOAL]
n : ℕ
m : { x // x ∈ filter (coprime n) (range n) }
⊢ ↑m ∈ {m | m < n ∧ coprime n m}
[PROOFSTEP]
simpa only [Finset.mem_filter, Finset.mem_range] using m.property
[GOAL]
n : ℕ
m : ↑{m | m < n ∧ coprime n m}
⊢ (fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) })
      ((fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) }) m) =
    m
[PROOFSTEP]
simp only [Subtype.coe_mk, Subtype.coe_eta]
[GOAL]
n : ℕ
m : { x // x ∈ filter (coprime n) (range n) }
⊢ (fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) })
      ((fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) }) m) =
    m
[PROOFSTEP]
simp only [Subtype.coe_mk, Subtype.coe_eta]
[GOAL]
n : ℕ
e : ↑{m | m < n ∧ coprime n m} ≃ { x // x ∈ filter (coprime n) (range n) } :=
  { toFun := fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) },
    invFun := fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) },
    left_inv :=
      (_ :
        ∀ (m : ↑{m | m < n ∧ coprime n m}),
          { val := ↑m,
              property :=
                (_ :
                  ↑((fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) }) m) < n ∧
                    coprime n ↑((fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) }) m)) } =
            m),
    right_inv :=
      (_ :
        ∀ (m : { x // x ∈ filter (coprime n) (range n) }),
          { val := ↑m,
              property :=
                (_ :
                  ↑((fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) }) m) ∈
                    filter (coprime n) (range n)) } =
            m) }
⊢ φ n = Nat.card ↑{m | m < n ∧ coprime n m}
[PROOFSTEP]
rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, Fintype.card_coe]
[GOAL]
n : ℕ
hn : 1 < n
⊢ 0 ∈ range n ∧ ¬coprime n 0
[PROOFSTEP]
simp [hn.ne', pos_of_gt hn]
[GOAL]
⊢ 0 < 0 → 0 < φ 0
[PROOFSTEP]
decide
[GOAL]
⊢ 0 < 1 → 0 < φ 1
[PROOFSTEP]
simp [totient]
[GOAL]
n : ℕ
x✝ : 0 < n + 2
⊢ 1 < n + 2
[PROOFSTEP]
simp
[GOAL]
a n : ℕ
⊢ card (filter (coprime a) (Ico n (n + a))) = φ a
[PROOFSTEP]
rw [totient, filter_Ico_card_eq_of_periodic, count_eq_card_filter_range]
[GOAL]
case pp
a n : ℕ
⊢ Function.Periodic (coprime a) a
[PROOFSTEP]
exact periodic_coprime a
[GOAL]
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + n))) ≤ φ a * (n / a + 1)
[PROOFSTEP]
conv_lhs => rw [← Nat.mod_add_div n a]
[GOAL]
a k n : ℕ
a_pos : 0 < a
| card (filter (coprime a) (Ico k (k + n)))
[PROOFSTEP]
rw [← Nat.mod_add_div n a]
[GOAL]
a k n : ℕ
a_pos : 0 < a
| card (filter (coprime a) (Ico k (k + n)))
[PROOFSTEP]
rw [← Nat.mod_add_div n a]
[GOAL]
a k n : ℕ
a_pos : 0 < a
| card (filter (coprime a) (Ico k (k + n)))
[PROOFSTEP]
rw [← Nat.mod_add_div n a]
[GOAL]
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * (n / a))))) ≤ φ a * (n / a + 1)
[PROOFSTEP]
induction' n / a with i ih
[GOAL]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * zero)))) ≤ φ a * (zero + 1)
[PROOFSTEP]
rw [← filter_coprime_Ico_eq_totient a k]
[GOAL]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * zero)))) ≤ card (filter (coprime a) (Ico k (k + a))) * (zero + 1)
[PROOFSTEP]
simp only [add_zero, mul_one, mul_zero, le_of_lt (mod_lt n a_pos), Nat.zero_eq, zero_add]
  --Porting note: below line was `mono`
[GOAL]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + n % a))) ≤ card (filter (coprime a) (Ico k (k + a)))
[PROOFSTEP]
refine Finset.card_mono ?_
[GOAL]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ filter (coprime a) (Ico k (k + n % a)) ≤ filter (coprime a) (Ico k (k + a))
[PROOFSTEP]
refine' monotone_filter_left a.coprime _
[GOAL]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ Ico k (k + n % a) ≤ Ico k (k + a)
[PROOFSTEP]
simp only [Finset.le_eq_subset]
[GOAL]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ Ico k (k + n % a) ⊆ Ico k (k + a)
[PROOFSTEP]
exact Ico_subset_Ico rfl.le (add_le_add_left (le_of_lt (mod_lt n a_pos)) k)
[GOAL]
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + (n % a + a * i)))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * succ i)))) ≤ φ a * (succ i + 1)
[PROOFSTEP]
simp only [mul_succ]
[GOAL]
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + (n % a + a * i)))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + (n % a + (a * i + a))))) ≤ φ a * i + φ a + φ a
[PROOFSTEP]
simp_rw [← add_assoc] at ih ⊢
[GOAL]
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + n % a + a * i + a))) ≤ φ a * i + φ a + φ a
[PROOFSTEP]
calc
  (filter a.coprime (Ico k (k + n % a + a * i + a))).card =
      (filter a.coprime (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a))).card :=
    by
    congr
    rw [Ico_union_Ico_eq_Ico]
    rw [add_assoc]
    exact le_self_add
    exact le_self_add
  _ ≤ (filter a.coprime (Ico k (k + n % a + a * i))).card + a.totient :=
    by
    rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
    apply card_union_le
  _ ≤ a.totient * i + a.totient + a.totient := add_le_add_right ih (totient a)
[GOAL]
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + n % a + a * i + a))) =
    card (filter (coprime a) (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a)))
[PROOFSTEP]
congr
[GOAL]
case e_s.e_s
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ Ico k (k + n % a + a * i + a) = Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a)
[PROOFSTEP]
rw [Ico_union_Ico_eq_Ico]
[GOAL]
case e_s.e_s.hab
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k ≤ k + n % a + a * i
case e_s.e_s.hbc
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k + n % a + a * i ≤ k + n % a + a * i + a
[PROOFSTEP]
rw [add_assoc]
[GOAL]
case e_s.e_s.hab
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k ≤ k + (n % a + a * i)
case e_s.e_s.hbc
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k + n % a + a * i ≤ k + n % a + a * i + a
[PROOFSTEP]
exact le_self_add
[GOAL]
case e_s.e_s.hbc
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k + n % a + a * i ≤ k + n % a + a * i + a
[PROOFSTEP]
exact le_self_add
[GOAL]
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a))) ≤
    card (filter (coprime a) (Ico k (k + n % a + a * i))) + φ a
[PROOFSTEP]
rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
[GOAL]
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card
      (filter (coprime a) (Ico k (k + n % a + a * i)) ∪
        filter (coprime a) (Ico (k + n % a + a * i) (k + n % a + a * i + a))) ≤
    card (filter (coprime a) (Ico k (k + n % a + a * i))) +
      card (filter (coprime a) (Ico (k + n % a + a * i) (k + n % a + a * i + a)))
[PROOFSTEP]
apply card_union_le
[GOAL]
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype (ZMod n)ˣ
⊢ Fintype.card { x // coprime (ZMod.val x) n } = φ n
[PROOFSTEP]
obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero NeZero.out
[GOAL]
case intro
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ Fintype.card { x // coprime (ZMod.val x) (m + 1) } = φ (m + 1)
[PROOFSTEP]
simp only [totient, Finset.card_eq_sum_ones, Fintype.card_subtype, Finset.sum_filter, ← Fin.sum_univ_eq_sum_range,
  @Nat.coprime_comm (m + 1)]
[GOAL]
case intro
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ (∑ a : ZMod (m + 1), if coprime (ZMod.val a) (m + 1) then 1 else 0) =
    ∑ i : Fin (m + 1), if coprime (↑i) (m + 1) then 1 else 0
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
hn : 2 < n
⊢ Even (φ n)
[PROOFSTEP]
haveI : Fact (1 < n) := ⟨one_lt_two.trans hn⟩
[GOAL]
n : ℕ
hn : 2 < n
this : Fact (1 < n)
⊢ Even (φ n)
[PROOFSTEP]
haveI : NeZero n := NeZero.of_gt hn
[GOAL]
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ Even (φ n)
[PROOFSTEP]
suffices 2 = orderOf (-1 : (ZMod n)ˣ)
  by
  rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
  exact orderOf_dvd_card_univ
[GOAL]
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ Even (φ n)
[PROOFSTEP]
rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
[GOAL]
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ orderOf (-1) ∣ Fintype.card (ZMod n)ˣ
[PROOFSTEP]
exact orderOf_dvd_card_univ
[GOAL]
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ 2 = orderOf (-1)
[PROOFSTEP]
rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']
[GOAL]
m n : ℕ
h : coprime m n
hmn0 : m * n = 0
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
cases' Nat.mul_eq_zero.1 hmn0 with h h
[GOAL]
case inl
m n : ℕ
h✝ : coprime m n
hmn0 : m * n = 0
h : m = 0
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
simp only [totient_zero, mul_zero, zero_mul, h]
[GOAL]
case inr
m n : ℕ
h✝ : coprime m n
hmn0 : m * n = 0
h : n = 0
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
simp only [totient_zero, mul_zero, zero_mul, h]
[GOAL]
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
haveI : NeZero (m * n) := ⟨hmn0⟩
[GOAL]
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this : NeZero (m * n)
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩
[GOAL]
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this✝ : NeZero (m * n)
this : NeZero m
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩
[GOAL]
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
simp only [← ZMod.card_units_eq_totient]
[GOAL]
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
[PROOFSTEP]
rw [Fintype.card_congr (Units.mapEquiv (ZMod.chineseRemainder h).toMulEquiv).toEquiv,
  Fintype.card_congr (@MulEquiv.prodUnits (ZMod m) (ZMod n) _ _).toEquiv, Fintype.card_prod]
[GOAL]
n d : ℕ
hnd : d ∣ n
⊢ φ (n / d) = Finset.card (filter (fun k => gcd n k = d) (range n))
[PROOFSTEP]
rcases d.eq_zero_or_pos with (rfl | hd0)
[GOAL]
case inl
n : ℕ
hnd : 0 ∣ n
⊢ φ (n / 0) = Finset.card (filter (fun k => gcd n k = 0) (range n))
[PROOFSTEP]
simp [eq_zero_of_zero_dvd hnd]
[GOAL]
case inr
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
⊢ φ (n / d) = Finset.card (filter (fun k => gcd n k = d) (range n))
[PROOFSTEP]
rcases hnd with ⟨x, rfl⟩
[GOAL]
case inr.intro
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ (d * x / d) = Finset.card (filter (fun k => gcd (d * x) k = d) (range (d * x)))
[PROOFSTEP]
rw [Nat.mul_div_cancel_left x hd0]
[GOAL]
case inr.intro
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ x = Finset.card (filter (fun k => gcd (d * x) k = d) (range (d * x)))
[PROOFSTEP]
apply Finset.card_congr fun k _ => d * k
[GOAL]
case inr.intro.h₁
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a : ℕ), a ∈ filter (coprime x) (range x) → d * a ∈ filter (fun k => gcd (d * x) k = d) (range (d * x))
[PROOFSTEP]
simp only [mem_filter, mem_range, and_imp, coprime]
[GOAL]
case inr.intro.h₁
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a : ℕ), a < x → gcd x a = 1 → d * a < d * x ∧ gcd (d * x) (d * a) = d
[PROOFSTEP]
refine' fun a ha1 ha2 => ⟨(mul_lt_mul_left hd0).2 ha1, _⟩
[GOAL]
case inr.intro.h₁
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : gcd x a = 1
⊢ gcd (d * x) (d * a) = d
[PROOFSTEP]
rw [gcd_mul_left, ha2, mul_one]
[GOAL]
case inr.intro.h₂
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a b : ℕ), a ∈ filter (coprime x) (range x) → b ∈ filter (coprime x) (range x) → d * a = d * b → a = b
[PROOFSTEP]
simp [hd0.ne']
[GOAL]
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (b : ℕ), b ∈ filter (fun k => gcd (d * x) k = d) (range (d * x)) → ∃ a ha, d * a = b
[PROOFSTEP]
simp only [mem_filter, mem_range, exists_prop, and_imp]
[GOAL]
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (b : ℕ), b < d * x → gcd (d * x) b = d → ∃ a, (a < x ∧ coprime x a) ∧ d * a = b
[PROOFSTEP]
refine' fun b hb1 hb2 => _
[GOAL]
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
⊢ ∃ a, (a < x ∧ coprime x a) ∧ d * a = b
[PROOFSTEP]
have : d ∣ b := by
  rw [← hb2]
  apply gcd_dvd_right
[GOAL]
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
⊢ d ∣ b
[PROOFSTEP]
rw [← hb2]
[GOAL]
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
⊢ gcd (d * x) b ∣ b
[PROOFSTEP]
apply gcd_dvd_right
[GOAL]
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
this : d ∣ b
⊢ ∃ a, (a < x ∧ coprime x a) ∧ d * a = b
[PROOFSTEP]
rcases this with ⟨q, rfl⟩
[GOAL]
case inr.intro.h₃.intro
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : gcd (d * x) (d * q) = d
⊢ ∃ a, (a < x ∧ coprime x a) ∧ d * a = d * q
[PROOFSTEP]
refine' ⟨q, ⟨⟨(mul_lt_mul_left hd0).1 hb1, _⟩, rfl⟩⟩
[GOAL]
case inr.intro.h₃.intro
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : gcd (d * x) (d * q) = d
⊢ coprime x q
[PROOFSTEP]
rwa [gcd_mul_left, mul_right_eq_self_iff hd0] at hb2 
[GOAL]
n : ℕ
⊢ Finset.sum (divisors n) φ = n
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
⊢ Finset.sum (divisors 0) φ = 0
[PROOFSTEP]
simp
[GOAL]
case inr
n : ℕ
hn : n > 0
⊢ Finset.sum (divisors n) φ = n
[PROOFSTEP]
rw [← sum_div_divisors n φ]
[GOAL]
case inr
n : ℕ
hn : n > 0
⊢ ∑ d in divisors n, φ (n / d) = n
[PROOFSTEP]
have : n = ∑ d : ℕ in n.divisors, (filter (fun k : ℕ => n.gcd k = d) (range n)).card :=
  by
  nth_rw 1 [← card_range n]
  refine' card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨_, hn.ne'⟩
  apply gcd_dvd_left
[GOAL]
n : ℕ
hn : n > 0
⊢ n = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
[PROOFSTEP]
nth_rw 1 [← card_range n]
[GOAL]
n : ℕ
hn : n > 0
⊢ Finset.card (range n) = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
[PROOFSTEP]
refine' card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨_, hn.ne'⟩
[GOAL]
n : ℕ
hn : n > 0
x : ℕ
x✝ : x ∈ range n
⊢ gcd n x ∣ n
[PROOFSTEP]
apply gcd_dvd_left
[GOAL]
case inr
n : ℕ
hn : n > 0
this : n = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
⊢ ∑ d in divisors n, φ (n / d) = n
[PROOFSTEP]
nth_rw 3 [this]
[GOAL]
case inr
n : ℕ
hn : n > 0
this : n = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
⊢ ∑ d in divisors n, φ (n / d) = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
[PROOFSTEP]
exact sum_congr rfl fun x hx => totient_div_of_dvd (dvd_of_mem_divisors hx)
[GOAL]
n : ℕ
⊢ ∑ m in filter (fun x => x ∣ n) (range (succ n)), φ m = n
[PROOFSTEP]
convert sum_totient _ using 1
[GOAL]
case h.e'_2
n : ℕ
⊢ ∑ m in filter (fun x => x ∣ n) (range (succ n)), φ m = Finset.sum (divisors n) φ
[PROOFSTEP]
simp only [Nat.divisors, sum_filter, range_eq_Ico]
[GOAL]
case h.e'_2
n : ℕ
⊢ (∑ a in Ico 0 (succ n), if a ∣ n then φ a else 0) = ∑ a in Ico 1 (n + 1), if a ∣ n then φ a else 0
[PROOFSTEP]
rw [sum_eq_sum_Ico_succ_bot]
[GOAL]
case h.e'_2
n : ℕ
⊢ ((if 0 ∣ n then φ 0 else 0) + ∑ k in Ico (0 + 1) (succ n), if k ∣ n then φ k else 0) =
    ∑ a in Ico 1 (n + 1), if a ∣ n then φ a else 0
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.hab
n : ℕ
⊢ 0 < succ n
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ filter (coprime (p ^ (n + 1))) (range (p ^ (n + 1))) = range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))
[PROOFSTEP]
rw [sdiff_eq_filter]
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ filter (coprime (p ^ (n + 1))) (range (p ^ (n + 1))) =
    filter (fun x => ¬x ∈ image (fun x => x * p) (range (p ^ n))) (range (p ^ (n + 1)))
[PROOFSTEP]
apply filter_congr
[GOAL]
case H
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (p ^ (n + 1)) → (coprime (p ^ (n + 1)) x ↔ ¬x ∈ image (fun x => x * p) (range (p ^ n)))
[PROOFSTEP]
simp only [mem_range, mem_filter, coprime_pow_left_iff n.succ_pos, mem_image, not_exists, hp.coprime_iff_not_dvd]
[GOAL]
case H
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (x : ℕ), x < p ^ (n + 1) → (¬p ∣ x ↔ ∀ (x_1 : ℕ), ¬(x_1 < p ^ n ∧ x_1 * p = x))
[PROOFSTEP]
intro a ha
[GOAL]
case H
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
[PROOFSTEP]
constructor
[GOAL]
case H.mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a → ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
[PROOFSTEP]
intro hap b h
[GOAL]
case H.mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
⊢ False
[PROOFSTEP]
rcases h with ⟨_, rfl⟩
[GOAL]
case H.mp.intro
p : ℕ
hp : Prime p
n b : ℕ
left✝ : b < p ^ n
ha : b * p < p ^ (n + 1)
hap : ¬p ∣ b * p
⊢ False
[PROOFSTEP]
exact hap (dvd_mul_left _ _)
[GOAL]
case H.mpr
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ (∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)) → ¬p ∣ a
[PROOFSTEP]
rintro h ⟨b, rfl⟩
[GOAL]
case H.mpr.intro
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p ^ (n + 1)
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False
[PROOFSTEP]
rw [pow_succ'] at ha 
[GOAL]
case H.mpr.intro
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p * p ^ n
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False
[PROOFSTEP]
exact h b ⟨lt_of_mul_lt_mul_left ha (zero_le _), mul_comm _ _⟩
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ Finset.card (range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))) = p ^ n * (p - 1)
[PROOFSTEP]
have h1 : Function.Injective (· * p) := mul_left_injective₀ hp.ne_zero
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
⊢ Finset.card (range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))) = p ^ n * (p - 1)
[PROOFSTEP]
have h2 : (range (p ^ n)).image (· * p) ⊆ range (p ^ (n + 1)) := fun a =>
  by
  simp only [mem_image, mem_range, exists_imp]
  rintro b ⟨h, rfl⟩
  rw [pow_succ]
  exact (mul_lt_mul_right hp.pos).2 h
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
a : ℕ
⊢ a ∈ image (fun x => x * p) (range (p ^ n)) → a ∈ range (p ^ (n + 1))
[PROOFSTEP]
simp only [mem_image, mem_range, exists_imp]
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
a : ℕ
⊢ ∀ (x : ℕ), x < p ^ n ∧ x * p = a → a < p ^ (n + 1)
[PROOFSTEP]
rintro b ⟨h, rfl⟩
[GOAL]
case intro
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case intro
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ n * p
[PROOFSTEP]
exact (mul_lt_mul_right hp.pos).2 h
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
h2 : image (fun x => x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ Finset.card (range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))) = p ^ n * (p - 1)
[PROOFSTEP]
rw [card_sdiff h2, card_image_of_injOn (h1.injOn _), card_range, card_range, ← one_mul (p ^ n), pow_succ', ← tsub_mul,
  one_mul, mul_comm]
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
hn : 0 < n
⊢ φ (p ^ n) = p ^ (n - 1) * (p - 1)
[PROOFSTEP]
rcases exists_eq_succ_of_ne_zero (pos_iff_ne_zero.1 hn) with ⟨m, rfl⟩
[GOAL]
case intro
p : ℕ
hp : Prime p
m : ℕ
hn : 0 < succ m
⊢ φ (p ^ succ m) = p ^ (succ m - 1) * (p - 1)
[PROOFSTEP]
exact totient_prime_pow_succ hp _
[GOAL]
p : ℕ
hp : Prime p
⊢ φ p = p - 1
[PROOFSTEP]
rw [← pow_one p, totient_prime_pow hp]
[GOAL]
p : ℕ
hp : Prime p
⊢ p ^ (1 - 1) * (p - 1) = p ^ 1 - 1
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Prime p
⊢ 0 < 1
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : 0 < p
⊢ φ p = p - 1 ↔ Prime p
[PROOFSTEP]
refine' ⟨fun h => _, totient_prime⟩
[GOAL]
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ Prime p
[PROOFSTEP]
replace hp : 1 < p
[GOAL]
case hp
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 < p
[PROOFSTEP]
apply lt_of_le_of_ne
[GOAL]
case hp.a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≤ p
[PROOFSTEP]
rwa [succ_le_iff]
[GOAL]
case hp.a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≠ p
[PROOFSTEP]
rintro rfl
[GOAL]
case hp.a
hp : 0 < 1
h : φ 1 = 1 - 1
⊢ False
[PROOFSTEP]
rw [totient_one, tsub_self] at h 
[GOAL]
case hp.a
hp : 0 < 1
h✝ : 1 = 1 - 1
h : 1 = 0
⊢ False
[PROOFSTEP]
exact one_ne_zero h
[GOAL]
p : ℕ
h : φ p = p - 1
hp : 1 < p
⊢ Prime p
[PROOFSTEP]
rw [totient_eq_card_coprime, range_eq_Ico, ← Ico_insert_succ_left hp.le, Finset.filter_insert,
  if_neg (not_coprime_of_dvd_of_dvd hp (dvd_refl p) (dvd_zero p)), ← Nat.card_Ico 1 p] at h 
[GOAL]
p : ℕ
h : Finset.card (filter (coprime p) (Ico (succ 0) p)) = Finset.card (Ico 1 p)
hp : 1 < p
⊢ Prime p
[PROOFSTEP]
refine' p.prime_of_coprime hp fun n hn hnz => Finset.filter_card_eq h n <| Finset.mem_Ico.mpr ⟨_, hn⟩
[GOAL]
p : ℕ
h : Finset.card (filter (coprime p) (Ico (succ 0) p)) = Finset.card (Ico 1 p)
hp : 1 < p
n : ℕ
hn : n < p
hnz : n ≠ 0
⊢ succ 0 ≤ n
[PROOFSTEP]
rwa [succ_le_iff, pos_iff_ne_zero]
[GOAL]
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1
[PROOFSTEP]
haveI : NeZero p := ⟨(pos_of_gt hp).ne'⟩
[GOAL]
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
this : NeZero p
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1
[PROOFSTEP]
rw [ZMod.card_units_eq_totient p]
[GOAL]
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
this : NeZero p
⊢ φ p ≤ p - 1
[PROOFSTEP]
exact Nat.le_pred_of_lt (Nat.totient_lt p hp)
[GOAL]
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
[PROOFSTEP]
cases' eq_zero_or_neZero p with hp hp
[GOAL]
case inl
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : p = 0
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
[PROOFSTEP]
subst hp
[GOAL]
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Prime 0 ↔ Fintype.card (ZMod 0)ˣ = 0 - 1
[PROOFSTEP]
simp only [ZMod, not_prime_zero, false_iff_iff, zero_tsub]
  -- the subst created a non-defeq but subsingleton instance diamond; resolve it
[GOAL]
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ ¬Fintype.card ℤˣ = 0
[PROOFSTEP]
suffices Fintype.card ℤˣ ≠ 0 by convert this
[GOAL]
inst✝ : Fintype (ZMod 0)ˣ
this : Fintype.card ℤˣ ≠ 0
⊢ ¬Fintype.card ℤˣ = 0
[PROOFSTEP]
convert this
[GOAL]
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Fintype.card ℤˣ ≠ 0
[PROOFSTEP]
simp
[GOAL]
case inr
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : NeZero p
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
[PROOFSTEP]
rw [ZMod.card_units_eq_totient, Nat.totient_eq_iff_prime <| NeZero.pos p]
[GOAL]
⊢ φ 0 = 1 ↔ 0 = 1 ∨ 0 = 2
[PROOFSTEP]
simp
[GOAL]
⊢ φ 1 = 1 ↔ 1 = 1 ∨ 1 = 2
[PROOFSTEP]
simp
[GOAL]
⊢ φ 2 = 1 ↔ 2 = 1 ∨ 2 = 2
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2
[PROOFSTEP]
have : 3 ≤ n + 3 := le_add_self
[GOAL]
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2
[PROOFSTEP]
simp only [succ_succ_ne_one, false_or_iff]
[GOAL]
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 2
[PROOFSTEP]
exact ⟨fun h => not_even_one.elim <| h ▸ totient_even this, by rintro ⟨⟩⟩
[GOAL]
n : ℕ
this : 3 ≤ n + 3
⊢ n + 3 = 2 → φ (n + 3) = 1
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ φ n = Finsupp.prod (factorization n) fun p k => p ^ (k - 1) * (p - 1)
[PROOFSTEP]
rw [multiplicative_factorization φ (@totient_mul) totient_one hn]
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ (Finsupp.prod (factorization n) fun p k => φ (p ^ k)) =
    Finsupp.prod (factorization n) fun p k => p ^ (k - 1) * (p - 1)
[PROOFSTEP]
apply Finsupp.prod_congr _
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ ∀ (x : ℕ), x ∈ (factorization n).support → φ (x ^ ↑(factorization n) x) = x ^ (↑(factorization n) x - 1) * (x - 1)
[PROOFSTEP]
intro p hp
[GOAL]
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ (factorization n).support
⊢ φ (p ^ ↑(factorization n) p) = p ^ (↑(factorization n) p - 1) * (p - 1)
[PROOFSTEP]
have h := zero_lt_iff.mpr (Finsupp.mem_support_iff.mp hp)
[GOAL]
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ (factorization n).support
h : 0 < ↑(factorization n) p
⊢ φ (p ^ ↑(factorization n) p) = p ^ (↑(factorization n) p - 1) * (p - 1)
[PROOFSTEP]
rw [totient_prime_pow (prime_of_mem_factorization hp) h]
[GOAL]
n : ℕ
⊢ φ n * ∏ p in List.toFinset (factors n), p = n * ∏ p in List.toFinset (factors n), (p - 1)
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
n : ℕ
hn : n = 0
⊢ φ n * ∏ p in List.toFinset (factors n), p = n * ∏ p in List.toFinset (factors n), (p - 1)
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p in List.toFinset (factors n), p = n * ∏ p in List.toFinset (factors n), (p - 1)
[PROOFSTEP]
rw [totient_eq_prod_factorization hn]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun p k => p ^ (k - 1) * (p - 1)) * ∏ p in List.toFinset (factors n), p =
    n * ∏ p in List.toFinset (factors n), (p - 1)
[PROOFSTEP]
nth_rw 3 [← factorization_prod_pow_eq_self hn]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun p k => p ^ (k - 1) * (p - 1)) * ∏ p in List.toFinset (factors n), p =
    (Finsupp.prod (factorization n) fun x x_1 => x ^ x_1) * ∏ p in List.toFinset (factors n), (p - 1)
[PROOFSTEP]
simp only [← prod_factorization_eq_prod_factors, ← Finsupp.prod_mul]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun a b => a ^ (b - 1) * (a - 1) * a) =
    Finsupp.prod (factorization n) fun a b => a ^ b * (a - 1)
[PROOFSTEP]
refine' Finsupp.prod_congr (M := ℕ) (N := ℕ) fun p hp => _
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ (factorization n).support
⊢ p ^ (↑(factorization n) p - 1) * (p - 1) * p = p ^ ↑(factorization n) p * (p - 1)
[PROOFSTEP]
rw [Finsupp.mem_support_iff, ← zero_lt_iff] at hp 
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < ↑(factorization n) p
⊢ p ^ (↑(factorization n) p - 1) * (p - 1) * p = p ^ ↑(factorization n) p * (p - 1)
[PROOFSTEP]
rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]
[GOAL]
n : ℕ
⊢ φ n = (n / ∏ p in List.toFinset (factors n), p) * ∏ p in List.toFinset (factors n), (p - 1)
[PROOFSTEP]
rw [← mul_div_left n.totient, totient_mul_prod_factors, mul_comm, Nat.mul_div_assoc _ (prod_prime_factors_dvd n),
  mul_comm]
[GOAL]
n : ℕ
⊢ 0 < ∏ p in List.toFinset (factors n), p
[PROOFSTEP]
have := prod_pos (fun p => pos_of_mem_factorization (n := n))
[GOAL]
n : ℕ
this : 0 < ∏ i in (factorization n).support, i
⊢ 0 < ∏ p in List.toFinset (factors n), p
[PROOFSTEP]
simpa [prod_factorization_eq_prod_factors] using this
[GOAL]
n : ℕ
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
n : ℕ
hn : n = 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
[PROOFSTEP]
have hn' : (n : ℚ) ≠ 0 := by simp [hn]
[GOAL]
n : ℕ
hn : ¬n = 0
⊢ ↑n ≠ 0
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
[PROOFSTEP]
have hpQ : (∏ p in n.factors.toFinset, (p : ℚ)) ≠ 0 :=
  by
  rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, ← prod_factorization_eq_prod_factors]
  exact prod_pos fun p hp => pos_of_mem_factorization hp
[GOAL]
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ∏ p in List.toFinset (factors n), ↑p ≠ 0
[PROOFSTEP]
rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, ← prod_factorization_eq_prod_factors]
[GOAL]
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ 0 < Finsupp.prod (factorization n) fun p x => p
[PROOFSTEP]
exact prod_pos fun p hp => pos_of_mem_factorization hp
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
[PROOFSTEP]
simp only [totient_eq_div_factors_mul n, prod_prime_factors_dvd n, cast_mul, cast_prod, cast_div_charZero, mul_comm_div,
  mul_right_inj' hn', div_eq_iff hpQ, ← prod_mul_distrib]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
⊢ ∏ i in List.toFinset (factors n), ↑(i - 1) = ∏ x in List.toFinset (factors n), (1 - (↑x)⁻¹) * ↑x
[PROOFSTEP]
refine' prod_congr rfl fun p hp => _
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
p : ℕ
hp : p ∈ List.toFinset (factors n)
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
[PROOFSTEP]
have hp := pos_of_mem_factors (List.mem_toFinset.mp hp)
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
p : ℕ
hp✝ : p ∈ List.toFinset (factors n)
hp : 0 < p
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
[PROOFSTEP]
have hp' : (p : ℚ) ≠ 0 := cast_ne_zero.mpr hp.ne.symm
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
p : ℕ
hp✝ : p ∈ List.toFinset (factors n)
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
[PROOFSTEP]
rw [sub_mul, one_mul, mul_comm, mul_inv_cancel hp', cast_pred hp]
[GOAL]
a b : ℕ
⊢ φ (gcd a b) * φ (a * b) = φ a * φ b * gcd a b
[PROOFSTEP]
have shuffle :
  ∀ a1 a2 b1 b2 c1 c2 : ℕ, b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2) :=
  by
  intro a1 a2 b1 b2 c1 c2 h1 h2
  calc
    a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2) := by apply mul_mul_mul_comm
    _ = a1 * a2 / (b1 * b2) * (c1 * c2) := by
      congr 1
      exact div_mul_div_comm h1 h2
[GOAL]
a b : ℕ
⊢ ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
[PROOFSTEP]
intro a1 a2 b1 b2 c1 c2 h1 h2
[GOAL]
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
[PROOFSTEP]
calc
  a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2) := by apply mul_mul_mul_comm
  _ = a1 * a2 / (b1 * b2) * (c1 * c2) := by
    congr 1
    exact div_mul_div_comm h1 h2
[GOAL]
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2)
[PROOFSTEP]
apply mul_mul_mul_comm
[GOAL]
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * (a2 / b2) * (c1 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * (a2 / b2) = a1 * a2 / (b1 * b2)
[PROOFSTEP]
exact div_mul_div_comm h1 h2
[GOAL]
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ φ (gcd a b) * φ (a * b) = φ a * φ b * gcd a b
[PROOFSTEP]
simp only [totient_eq_div_factors_mul]
[GOAL]
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ((gcd a b / ∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (gcd a b)), (p - 1)) *
      ((a * b / ∏ p in List.toFinset (factors (a * b)), p) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    ((a / ∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors a), (p - 1)) *
        ((b / ∏ p in List.toFinset (factors b), p) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
[PROOFSTEP]
rw [shuffle, shuffle]
[GOAL]
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors a), p ∣ a
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors b), p ∣ b
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors (gcd a b)), p ∣ gcd a b
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors (a * b)), p ∣ a * b
[PROOFSTEP]
rotate_left
[GOAL]
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors a), p ∣ a
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors b), p ∣ b
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors (gcd a b)), p ∣ gcd a b
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors (a * b)), p ∣ a * b
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
[PROOFSTEP]
repeat' apply prod_prime_factors_dvd
[GOAL]
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors a), p ∣ a
[PROOFSTEP]
apply prod_prime_factors_dvd
[GOAL]
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors b), p ∣ b
[PROOFSTEP]
apply prod_prime_factors_dvd
[GOAL]
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors (gcd a b)), p ∣ gcd a b
[PROOFSTEP]
apply prod_prime_factors_dvd
[GOAL]
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors (a * b)), p ∣ a * b
[PROOFSTEP]
apply prod_prime_factors_dvd
[GOAL]
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
[PROOFSTEP]
apply prod_prime_factors_dvd
[GOAL]
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
[PROOFSTEP]
simp only [prod_factors_gcd_mul_prod_factors_mul]
[GOAL]
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
      ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
[PROOFSTEP]
rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc]
[GOAL]
case H
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ (∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p ∣ a * b
[PROOFSTEP]
exact mul_dvd_mul (prod_prime_factors_dvd a) (prod_prime_factors_dvd b)
[GOAL]
a b : ℕ
⊢ φ a * φ b ≤ φ (a * b)
[PROOFSTEP]
let d := a.gcd b
[GOAL]
a b : ℕ
d : ℕ := gcd a b
⊢ φ a * φ b ≤ φ (a * b)
[PROOFSTEP]
rcases(zero_le a).eq_or_lt with (rfl | ha0)
[GOAL]
case inl
b : ℕ
d : ℕ := gcd 0 b
⊢ φ 0 * φ b ≤ φ (0 * b)
[PROOFSTEP]
simp
[GOAL]
case inr
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
⊢ φ a * φ b ≤ φ (a * b)
[PROOFSTEP]
have hd0 : 0 < d := Nat.gcd_pos_of_pos_left _ ha0
[GOAL]
case inr
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ a * φ b ≤ φ (a * b)
[PROOFSTEP]
apply le_of_mul_le_mul_right _ hd0
[GOAL]
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ a * φ b * d ≤ φ (a * b) * d
[PROOFSTEP]
rw [← totient_gcd_mul_totient_mul a b, mul_comm]
[GOAL]
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ (a * b) * φ (gcd a b) ≤ φ (a * b) * d
[PROOFSTEP]
apply mul_le_mul_left' (Nat.totient_le d)
[GOAL]
a b : ℕ
h : a ∣ b
⊢ φ a ∣ φ b
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha0)
[GOAL]
case inl
b : ℕ
h : 0 ∣ b
⊢ φ 0 ∣ φ b
[PROOFSTEP]
simp [zero_dvd_iff.1 h]
[GOAL]
case inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
⊢ φ a ∣ φ b
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb0)
[GOAL]
case inr.inl
a : ℕ
ha0 : a ≠ 0
h : a ∣ 0
⊢ φ a ∣ φ 0
[PROOFSTEP]
simp
[GOAL]
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ φ a ∣ φ b
[PROOFSTEP]
have hab' : a.factorization.support ⊆ b.factorization.support :=
  by
  intro p
  simp only [support_factorization, List.mem_toFinset]
  apply factors_subset_of_dvd h hb0
[GOAL]
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ (factorization a).support ⊆ (factorization b).support
[PROOFSTEP]
intro p
[GOAL]
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
p : ℕ
⊢ p ∈ (factorization a).support → p ∈ (factorization b).support
[PROOFSTEP]
simp only [support_factorization, List.mem_toFinset]
[GOAL]
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
p : ℕ
⊢ p ∈ factors a → p ∈ factors b
[PROOFSTEP]
apply factors_subset_of_dvd h hb0
[GOAL]
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : (factorization a).support ⊆ (factorization b).support
⊢ φ a ∣ φ b
[PROOFSTEP]
rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0]
[GOAL]
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : (factorization a).support ⊆ (factorization b).support
⊢ (Finsupp.prod (factorization a) fun p k => p ^ (k - 1) * (p - 1)) ∣
    Finsupp.prod (factorization b) fun p k => p ^ (k - 1) * (p - 1)
[PROOFSTEP]
refine' Finsupp.prod_dvd_prod_of_subset_of_dvd hab' fun p _ => mul_dvd_mul _ dvd_rfl
[GOAL]
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : (factorization a).support ⊆ (factorization b).support
p : ℕ
x✝ : p ∈ (factorization a).support
⊢ p ^ (↑(factorization a) p - 1) ∣ p ^ (↑(factorization b) p - 1)
[PROOFSTEP]
exact pow_dvd_pow p (tsub_le_tsub_right ((factorization_le_iff_dvd ha0 hb0).2 h p) 1)
[GOAL]
p n : ℕ
hp : Prime p
h : p ∣ n
⊢ φ (p * n) = p * φ n
[PROOFSTEP]
have h1 := totient_gcd_mul_totient_mul p n
[GOAL]
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ (gcd p n) * φ (p * n) = φ p * φ n * gcd p n
⊢ φ (p * n) = p * φ n
[PROOFSTEP]
rw [gcd_eq_left h, mul_assoc] at h1 
[GOAL]
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * (φ n * p)
⊢ φ (p * n) = p * φ n
[PROOFSTEP]
simpa [(totient_pos hp.pos).ne', mul_comm] using h1
[GOAL]
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ φ (p * n) = (p - 1) * φ n
[PROOFSTEP]
rw [totient_mul _, totient_prime hp]
[GOAL]
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ coprime p n
[PROOFSTEP]
simpa [h] using coprime_or_dvd_of_prime hp n
