[Usa2003Q1] finish proof

MathPuzzles/Usa2003Q1.lean

@@ -29,6 +29,34 @@ theorem Nat.digits_add'
   · simpa [forall_and, or_imp, hxb] using fun _ => Nat.digits_lt_base hb
   · simpa
 
+lemma nat_mod_inv (a : ℕ) : ∃ b, (a + b) % 5 = 0 := by
+  use (5 - (a % 5))
+  have h : a % 5 < 5 := Nat.mod_lt _ (by norm_num)
+  have h' : a % 5 ≤ 5 := Nat.le_of_lt h
+  rw[Nat.add_mod]
+  have h2 : a % 5 = a % 5 % 5 := (Nat.mod_mod a 5).symm
+  rw[h2, ← Nat.add_mod, Nat.mod_mod]
+  rw[Nat.add_sub_of_le h']
+  rfl
+
+lemma lemma2 (a c : ℕ) (h : ¬ a ≡ 0 [MOD 5]) : ∃ k, k < 5 ∧ a * k ≡ c [MOD 5] := by
+  -- use chinese remainder to find something that's
+  -- 0 mod a and c MOD 5.
+  have hc : Nat.coprime 5 a := by
+    have h5 : Nat.Prime 5 := by norm_num
+    refine' (Nat.Prime.coprime_iff_not_dvd h5).mpr _
+    rw[Nat.modEq_zero_iff_dvd] at h
+    exact h
+  let ⟨N, HN2, HN1⟩ := Nat.chineseRemainder hc c 0
+  have ⟨x, hx⟩ : a ∣ N := Iff.mp Nat.modEq_zero_iff_dvd HN1
+  use x % 5
+  constructor
+  · exact Nat.mod_lt _ (by norm_num)
+  · have h2 : N % 5 = c % 5 := HN2
+    suffices h : (a * (x % 5)) % 5 = c % 5 by exact h
+    rw[← h2, hx]
+    rw[Nat.mul_mod, Nat.mod_mod, ← Nat.mul_mod]
+
 theorem usa2003Q1 (n : ℕ) :
     ∃ m, ((Nat.digits 10 m).length = n ∧
           5^n ∣ m ∧
@@ -73,8 +101,40 @@ theorem usa2003Q1 (n : ℕ) :
             exact decide_eq_true hk0
 
     -- This is equivalent to proving that there exists an odd digit k such that
-    -- k·2ⁿ + a is divisible by 5,
-    -- which is true when k ≡ -3ⁿ⬝a MOD 5.
+    -- k·2ⁿ + a is divisible by 5...
+    suffices h : ∃ k, Odd k ∧ k < 10 ∧ 5 ∣ (2^n * k + a) by
+      obtain ⟨k, hk1, hk2, kk, hkk⟩ := h
+      refine' ⟨k, hk1, hk2, _⟩
+      use kk
+      rw[Nat.pow_succ, Nat.mul_assoc, ←hkk, Nat.mul_pow 5 2 n]
+      ring
+
+    -- ...which is true when k ≡ -3ⁿ⬝a MOD 5.
     -- Since there is an odd digit in each of the residue classes MOD 5,
     -- k exists and the induction is complete.
-    sorry
+
+    suffices h : ∃ j, j < 5 ∧ 5 ∣ (2^n * (2 * j + 1) + a) by
+      obtain ⟨j, hj1, hj2⟩ := h
+      refine' ⟨2 * j + 1, odd_two_mul_add_one j, _, hj2⟩
+      · linarith
+    clear ha hpm1 hpm3
+
+    obtain ⟨b, hb⟩ := nat_mod_inv (2^n + a)
+    have h11 : ¬ 2^(n + 1) ≡ 0 [MOD 5] := by
+      have h14 : Nat.coprime 5 2 := by norm_num
+      have h15 : Nat.coprime (5^1) (2^(n+1)) := Nat.coprime.pow _ _ h14
+      rw[Nat.pow_one] at h15
+      have h5 : Nat.Prime 5 := by norm_num
+      have h16 := (Nat.Prime.coprime_iff_not_dvd h5).mp h15
+      intro h17
+      have h18 : 5 ∣ 2 ^ (n + 1) := Iff.mp Nat.modEq_zero_iff_dvd h17
+      exact (h16 h18).elim
+    obtain ⟨aa, haa1, haa2⟩ := lemma2 (2^(n + 1)) b h11
+    use aa
+    constructor
+    · exact haa1
+    · have h12 : (2^n + a + 2 ^ (n + 1) * aa) % 5 = (2^n + a + b) % 5 := Nat.ModEq.add rfl haa2
+      rw[hb] at h12
+      have h13 : (2 ^ n + a + 2 ^ (n + 1) * aa) = 2 ^ n * (2 * aa + 1) + a := by ring
+      rw[h13] at h12
+      exact Iff.mp Nat.modEq_zero_iff_dvd h12