theorem
proved
tactic proof
balanced_pair_phase_support_gives_repr
show as:
view Lean formalization →
formal statement (Lean)
111theorem balanced_pair_phase_support_gives_repr {n c : ℕ}
112 (h : BalancedPairPhaseSupport n c) :
113 HasRationalErdosStrausRepr (n : ℚ) := by
proof body
Tactic-mode proof.
114 rcases h with ⟨x, N, d, e, hnpos, hcpos, hxpos, hNpos, hdpos, hepos,
115 hN, hcdefNat, hde, _hcd, _hce⟩
116 have hn : (n : ℚ) ≠ 0 := by exact_mod_cast hnpos.ne'
117 have hx : (x : ℚ) ≠ 0 := by exact_mod_cast hxpos.ne'
118 have hc : (c : ℚ) ≠ 0 := by exact_mod_cast hcpos.ne'
119 have hy : (((N : ℚ) + (d : ℚ)) / (c : ℚ)) ≠ 0 := by
120 have hnum : ((N : ℚ) + (d : ℚ)) ≠ 0 := by
121 have hpos : (0 : ℚ) < (N : ℚ) + (d : ℚ) := by
122 exact add_pos (by exact_mod_cast hNpos) (by exact_mod_cast hdpos)
123 exact ne_of_gt hpos
124 exact div_ne_zero hnum hc
125 have hz : (((N : ℚ) + (e : ℚ)) / (c : ℚ)) ≠ 0 := by
126 have hnum : ((N : ℚ) + (e : ℚ)) ≠ 0 := by
127 have hpos : (0 : ℚ) < (N : ℚ) + (e : ℚ) := by
128 exact add_pos (by exact_mod_cast hNpos) (by exact_mod_cast hepos)
129 exact ne_of_gt hpos
130 exact div_ne_zero hnum hc
131 have hNQ : (N : ℚ) = (n : ℚ) * (x : ℚ) := by
132 exact_mod_cast hN
133 have hcdefQ : (c : ℚ) = 4 * (x : ℚ) - (n : ℚ) := by
134 have hcadd : c + n = 4 * x := by omega
135 have hcaddQ : (c : ℚ) + (n : ℚ) = 4 * (x : ℚ) := by
136 exact_mod_cast hcadd
137 linarith
138 have hdeQ : (d : ℚ) * (e : ℚ) = (N : ℚ) ^ 2 := by
139 exact_mod_cast hde
140 refine repr_of_balanced_factor_pair
141 (n := (n : ℚ)) (x := (x : ℚ)) (c := (c : ℚ)) (N := (N : ℚ))
142 (d := (d : ℚ)) (e := (e : ℚ))
143 (y := ((N : ℚ) + (d : ℚ)) / (c : ℚ))
144 (z := ((N : ℚ) + (e : ℚ)) / (c : ℚ))
145 hn hx hc hy hz hNQ hcdefQ hdeQ ?_ ?_
146 · field_simp [hc]
147 · field_simp [hc]
148
149/-! ## 4. Trap characterization -/
150
151/-- Every prime divisor of `m` lies in residue class `1 mod 3`. -/