if a^7=b^7 then a=b

Stream: new members

[Lars Ericson]

This one will be a bit challenging to transcribe into Lean:

import tactic
import algebra.ordered_ring
universe u

theorem ex_1_3_5 (α: Type u) [linear_ordered_comm_ring α]
   (a b : α) (h: a^7 = b^7) : a = b :=
begin
  sorry,
end

Note:

a=b iff (a-b)^7 equal 0.

We want to prove that

(a-b)^7 =
= a^7 - 7*a^6*b + 21*a^5*b^2 - 35*a^4*b^3 + 35*a^3*b^4 - 21*a^2*b^5 + 7*a*b^6 - b^7
=0

By assumption a^7-b^7 = 0 so we want to prove that

 7*a^6*b + 21*a^5*b^2 - 35*a^4*b^3 + 35*a^3*b^4 - 21*a^2*b^5 + 7*a*b^6 =0

This factors to

-7*a*b*(a-b)*(a^2-a*b+b^2)^2 = 0

This has solutions when a=b=0 and when a=b. The remaining case is to look at

(a^2-a*b+b^2) = (a-b)^2 + a*b = 0

This has solution when a=b=0. Otherwise we have to have

(a-b)^2 = - a*b

But (a-b)^2 is positive or 0. When it is positive, the only solutions are when a<0, b>0 or a>0,b<0.

By calculus, the expression f = (a-b)^2 + a*b = 0 will only have a 0 when df/da = 0.

But df/da = 2*(a-b) + b which is 0 only when a = b/2. But then sign(a) = sign(b) which contradicts conditions a<0, b>0 or a>0,b<`.

So there are no additional solutions and the only solution is when a=b.

In terms of translation difficulty, I know how to do the expression reductions. I'm not sure how to do the calculus step. That seems bigger than a breadbox. I haven't tried to do anything with calculus yet. I guess the relevant stuff will be in analysis.calculus.fderiv.

`

[Kevin Buzzard]

Why not just prove that if a<b then a^7<b^7? More generally why not prove that if a<b then a^{2n+1}<b^{2n+1}? This doesn't look too hard. I definitely wouldn't go through what you're sketching above, it looks like a nightmare. Probably you just do some case split on the signs of a and b and then it's all over.

[Mario Carneiro]

theorem ex_1_3_5 {α} [linear_ordered_ring α] (a b : α) (h: a^7 = b^7) : a = b :=
(@strict_mono_pow_bit1 α _ 3).injective h

boom

[Mario Carneiro]

a similar proof also works for your earlier question about a^3<b^3

[Kevin Buzzard]

and indeed the proof of strict_mono_pow_bit1 is just a case split on the signs of a and b.

[Mario Carneiro]

The proof by expansion might conceivably be more general because you don't need a linear order, although I think you still need negation

[Kevin Buzzard]

it's not true without some order assumption, e.g. it's not true in the complexes

[Mario Carneiro]

well strict_mono itself doesn't typecheck on the complexes

[Mario Carneiro]

if you just want injectivity then it's false anyway on the complexes

[Kevin Buzzard]

sure -- we're saying the same thing. I just didn't understand your comment about a proof by expansion. There are finite fields where it's false too, you need something.

[Mario Carneiro]

but it might be true for an ordered_ring for example (not sure if there is a counterexample on ordered_semiring where it can still be stated)

[Kevin Buzzard]

oh I see. Yeah maybe.

[Mario Carneiro]

I'm talking about the version with an order, so finite fields are out

[Mario Carneiro]

but you just have a partial order

[Mario Carneiro]

so the case split proof doesn't work

[Kevin Buzzard]

I misinterpreted "you don't need a linear order" as "you don't need an order" :-)

[Lars Ericson]

Thank you @Kevin Buzzard and @Mario Carneiro for thinking about this. Regarding "Why not just prove that if a<b then a^7<b^7?", that's not the direction Birkhoff and Mac Lane asked for:

Screenshot-from-2021-02-01-23-43-33.png

I will study Mario's one-line proof. My long-winded sketch was inspired by the Internets.

[Mario Carneiro]

@Lars Ericson The question doesn't ask it, but if you can prove a < b -> A^7 < b^7 then a^7 = b^7 -> a = b follows, because if a != b then a < b so a^7 < b^7 and if b < a so b^7 < a^7, so in either case a^7 != b^7 and that's the contrapositive of the claim. This is one of the possible proof strategies to prove a function is injective