The integer ababab (a,b>0) is always divisible by 7, without remainder

Question

The integer $ababab$ $(a>0,b>0)$ is always divisible by $7$, without rest.

I tried to prove this by:

Solve[Mod[(a*10^5 + b*10^4 + a*10^3 + b*10^2 + a*10^1 + b), 7] == 0, {a, b}, PositiveIntegers]

I expected a True as result. What do I wrong?

What does the result show?

$\{\{a\to \fbox{$7 c_1\text{ if }(c_2|c_1)\in \mathbb{Z}\land c_1\geq 1\land c_2\geq 0$},b\to \fbox{$7 c_2+1\text{ if }(c_2|c_1)\in \mathbb{Z}\land c_1\geq 1\land c_2\geq 0$}\},...\}$

Answer 1

One may regard this question as the test of the system ability of proving theorems, but there is another view to understand what lies beneath this theorem.

Then we figure out that the problem is quite trivial.

$$a\;10^5+a\; 10^3+a\; 10 +b\; 10^4+b \;10^2+b=101010 a+ 10101 b$$

The simplest proof:

    And @@ Divisible[{101010, 10101}, 7]

True

Stronger theorem: all common divisors divide the number $ababab$:

Intersection[Divisors[101010], Divisors[10101]]

{1, 3, 7, 13, 21, 37, 39, 91, 111, 259, 273, 481, 777, 1443, 3367, 10101}

among them $7$, regardless $a$ and $b$ are positive or nonnegative integers. Q.E.D.

Answer 2

Reduce[ForAll[{a, b}, 
a > 0 && b > 0 && a ∈ Integers && b ∈ Integers, 
Mod[(a*10^5 + b*10^4 + a*10^3 + b*10^2 + a*10^1 + b), 7] == 0], {a, 
 b}]

(*   True   *)

Answer 3

Simplify[Mod[FromDigits[{a, b, a, b, a, b}], 7]==0, {a, b} ∈ 
  PositiveIntegers]

True

BTW,{a, b} ∈ Integers also work.