If the decimal expansion of $a/b$ contains "$7143$" then $b>1250$

I recently stumbled upon this really interesting problem:

Suppose we have a fraction $\frac{a}{b}$ where $a,b \in \mathbb{N}$ and we know that the decimal fraction of $\frac{a}{b}$ has the numerical sequence $7143$ somewhere in the decimal place. Show that $b > 1250 $.

This question is part of der Bundeswettbewerb Mathematik 2015, zweite Rund. The competition ended September 1st, 2015.

Any kind of help will be appreciated!

The trick is to realize $7\times0.7143=5.0001$.

First let's multiply by $10^n$ to shift the decimal to the right - hence for some integers $k$ and $n$ and real number $c\in[0,1)$ we can write

$$\frac{10^na}{b}=k+0.7143+0.0001c$$

Now multiply by our magic number!

$$7\times\frac{10^na}{b}=7k+5.0001+0.0007c$$

Hence

$$7(10^na-kb)-5b=(0.0001+0.0007c)b$$

The left hand side is an integer, so there exists $m\in\mathbb{Z}$ such that

$$m=(0.0001+0.0007c)b$$

Since $0\le c<1$, we have

$$0.0001 b\le m<0.0008b$$

Additionally, since $b\in\mathbb{N}$, we have $$0<0.0001b\le m$$ so because $m$ is an integer, $$1\le m<0.0008b$$ giving $1250<b$ as desired.

First multiply a by a power of 10 such that 7143 comes right after the decimal point, and then subtract a multiple of b such that the decimal fraction starts with $0.7143$. The claim we need to prove is then that the interval $[0.7143,0.7144)$ does not contain any rational with a denominator $\le 1250$.

The continued fractions for $0.7143$ and $0.7144$ are $[0;1,2,1,1,1428]$ and $[0;1,2,1,1,178]$, so the continued fraction expansion for every number in this interval will have the form $[0;1,2,1,1,n,\ldots]$ where $178\le n\le 1428$ and there may or may not be more terms after the $n$.

If we work out $[0;1,2,1,1,n]$ as an ordinary fraction we get $\frac{5n+3}{7n+4}$, which (being a continued fraction approximant) is always in lowest terms.

When $n>178$ the denominator of this is at least $7\cdot 179+4=1257$. Since the denominators of continued fraction approximants always increase, we get $b \ge 1257$.

On the other hand we might have $n=178$ if there is a term after $n$ in the continued fraction expansion. But the simplest fraction we can then make corresponds to $n=178.5$, which would make the next approximant $\frac{5\cdot 178.5+3}{7\cdot 178.5+4}=\frac{1791}{2507}$, also with a large denominator.

By multiplying $a$ with a power of $10$ if necessary, we may assume that $1743$ occurs immediately after the decimal point, and by subtacting a multiple of $b$ from $a$ we may assume that in fact $\frac ab=0.1743\ldots$. Then $$ \frac57=0.7142857\ldots <\frac ab <0.7145 = \frac{893}{1250}$$ Hence the numeraotrs of the difference fractions $\frac ab-\frac 57=\frac{7a-5b}{7b}$ and $\frac{893}{1250}-\frac ab=\frac{893b-1250a}{1250b}$ are positive integers, i.e., $$ \begin{align}7a-\hphantom{88}5b&\ge 1\\-1250a+893b&\ge1\end{align}$$ Then $1250$ times the first plus $7$ times the second inequality eliminates $a$ and gives us $$ (-5\cdot 1250+7\cdot 893) b\ge 1250+7,$$ i.e., $$ b\ge 1257.$$