MAT3253 Complex Variables

            
              1.2. Linear equation in complex numbers🔗
            section Linear_equation
/-- Show that i/5 is the only solution to 5z=i -/
example (z : ℂ) : 5*z = I ↔ z = (1/5)*I := byz:ℂ⊢ 5 * z = I ↔ z = 1 / 5 * I
  constructormpz:ℂ⊢ 5 * z = I → z = 1 / 5 * Imprz:ℂ⊢ z = 1 / 5 * I → 5 * z = I
  ·mpz:ℂ⊢ 5 * z = I → z = 1 / 5 * I -- the forward direction
    intro hmpz:ℂh:5 * z = I⊢ z = 1 / 5 * I
    rw [mul_comm 5 z] at hmpz:ℂh:z * 5 = I⊢ z = 1 / 5 * I
    -- isolate z
    have h1 : z = I/5 := byz:ℂ⊢ 5 * z = I ↔ z = 1 / 5 * I
      apply (eq_div_iff_mul_eq ?_).mpr hz:ℂh:z * 5 = I⊢ 5 ≠ 0
      norm_numAll goals completed! 🐙
    -- simplify right-hand side
    rw [h1]mpz:ℂh:z * 5 = Ih1:z = I / 5⊢ I / 5 = 1 / 5 * I
    ringAll goals completed! 🐙
  ·mprz:ℂ⊢ z = 1 / 5 * I → 5 * z = I -- the backward direction
    intro hmprz:ℂh:z = 1 / 5 * I⊢ 5 * z = I
    rw [h]mprz:ℂh:z = 1 / 5 * I⊢ 5 * (1 / 5 * I) = I
    ringAll goals completed! 🐙
/-- solve iz = 2 -/
example (z : ℂ) : I*z = 2 →  z = -2*I := byz:ℂ⊢ I * z = 2 → z = -2 * I
  intro hz:ℂh:I * z = 2⊢ z = -2 * I
  rw [mul_comm I z] at hz:ℂh:z * I = 2⊢ z = -2 * I

  have hnz : I ≠ 0 := byz:ℂ⊢ I * z = 2 → z = -2 * I
    apply_fun imz:ℂh:z * I = 2⊢ I.im ≠ im 0; norm_numAll goals completed! 🐙

  -- isolate z
  have h1 : z = 2/I := byz:ℂ⊢ I * z = 2 → z = -2 * I
    apply (eq_div_iff_mul_eq hnz).mpr hAll goals completed! 🐙

  -- simplify right-hand side
  rw [h1]z:ℂh:z * I = 2hnz:I ≠ 0h1:z = 2 / I⊢ 2 / I = -2 * I
  field_simp [hnz]z:ℂh:z * I = 2hnz:I ≠ 0h1:z = 2 / I⊢ 1 = -I ^ 2
  rw [I_sq]z:ℂh:z * I = 2hnz:I ≠ 0h1:z = 2 / I⊢ 1 = - -1
  ringAll goals completed! 🐙
/-- solve 2*z + 2*I*z - 3 = 5*I -/
example (z : ℂ) :
  (2*z + 2*I*z - 3 = 5*I) → z = 2 + (1/2)*I := byz:ℂ⊢ 2 * z + 2 * I * z - 3 = 5 * I → z = 2 + 1 / 2 * I
  intro hz:ℂh:2 * z + 2 * I * z - 3 = 5 * I⊢ z = 2 + 1 / 2 * I

  -- bring -3 to the right-hand side
  have h1 : 2*z + 2 *I*z = 3 + 5 * I := byz:ℂ⊢ 2 * z + 2 * I * z - 3 = 5 * I → z = 2 + 1 / 2 * I
    apply Eq.symm (add_eq_of_eq_sub' (Eq.symm h))All goals completed! 🐙

  -- factor out z
  have h2 : z * (2 + 2 * I)  = 3 + 5 * I := byz:ℂ⊢ 2 * z + 2 * I * z - 3 = 5 * I → z = 2 + 1 / 2 * I
    simpa [left_distrib, mul_comm] using h1All goals completed! 🐙

  -- verify that 2+2*I is nonzero
  have hnz1 : 2+2*I ≠ 0 := byz:ℂ⊢ 2 * z + 2 * I * z - 3 = 5 * I → z = 2 + 1 / 2 * I
    apply_fun rez:ℂh:2 * z + 2 * I * z - 3 = 5 * Ih1:2 * z + 2 * I * z = 3 + 5 * Ih2:z * (2 + 2 * I) = 3 + 5 * I⊢ (2 + 2 * I).re ≠ re 0; norm_numAll goals completed! 🐙

  -- isolate z
  have h_iso : z = (3 + 5 * I) / (2 + 2 * I) := byz:ℂ⊢ 2 * z + 2 * I * z - 3 = 5 * I → z = 2 + 1 / 2 * I
    exact (eq_div_iff_mul_eq hnz1).mpr h2All goals completed! 🐙

  -- verify that 1+I is nonzero
  have hnz2 : 1+I ≠ 0 := byz:ℂ⊢ 2 * z + 2 * I * z - 3 = 5 * I → z = 2 + 1 / 2 * I
    apply_fun imz:ℂh:2 * z + 2 * I * z - 3 = 5 * Ih1:2 * z + 2 * I * z = 3 + 5 * Ih2:z * (2 + 2 * I) = 3 + 5 * Ihnz1:2 + 2 * I ≠ 0h_iso:z = (3 + 5 * I) / (2 + 2 * I)⊢ (1 + I).im ≠ im 0 ; norm_numAll goals completed! 🐙

  -- Simplify the right-hand side to 2 + (1/2)*I
  rw [h_iso]z:ℂh:2 * z + 2 * I * z - 3 = 5 * Ih1:2 * z + 2 * I * z = 3 + 5 * Ih2:z * (2 + 2 * I) = 3 + 5 * Ihnz1:2 + 2 * I ≠ 0h_iso:z = (3 + 5 * I) / (2 + 2 * I)hnz2:1 + I ≠ 0⊢ (3 + 5 * I) / (2 + 2 * I) = 2 + 1 / 2 * I
  field_simp [hnz2]z:ℂh:2 * z + 2 * I * z - 3 = 5 * Ih1:2 * z + 2 * I * z = 3 + 5 * Ih2:z * (2 + 2 * I) = 3 + 5 * Ihnz1:2 + 2 * I ≠ 0h_iso:z = (3 + 5 * I) / (2 + 2 * I)hnz2:1 + I ≠ 0⊢ 3 + 5 * I = (1 + I) * (2 ^ 2 + I)
  -- we now prove 3 + 5 * I = (1 + I) * (2 ^ 2 + I) by ring
  ring_nfz:ℂh:2 * z + 2 * I * z - 3 = 5 * Ih1:2 * z + 2 * I * z = 3 + 5 * Ih2:z * (2 + 2 * I) = 3 + 5 * Ihnz1:2 + 2 * I ≠ 0h_iso:z = (3 + 5 * I) / (2 + 2 * I)hnz2:1 + I ≠ 0⊢ 3 + I * 5 = 4 + I * 5 + I ^ 2
  rewrite [I_sq]z:ℂh:2 * z + 2 * I * z - 3 = 5 * Ih1:2 * z + 2 * I * z = 3 + 5 * Ih2:z * (2 + 2 * I) = 3 + 5 * Ihnz1:2 + 2 * I ≠ 0h_iso:z = (3 + 5 * I) / (2 + 2 * I)hnz2:1 + I ≠ 0⊢ 3 + I * 5 = 4 + I * 5 + -1
  ringAll goals completed! 🐙
end Linear_equation