Prove coprimality of aks

[metakunt]

Hey @tirix I have proven all steps in your proof sketch except the following one:

|- ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) /\ ( R / ( N gcd R ) ) || A ) -> -. ( R / p ) || A )

I have thought about using pm2.65da to get a contradiction but it seemed so hard since the theorems in main weren't cutting it for some reason.
I feel as if I have to combine those two hypotheses

|- ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) /\ ( R / ( N gcd R ) ) || A ) -> p || A )
|- ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) /\ ( R / ( N gcd R ) ) || A ) -> -. R || A )

to get the result.

Idea was the following: Assume (R/p) divides A, but then together with p divides A we also get that (R/p)*p=R divides A, contradiction.

This is my current sketch

!315::             |- (  (  (  (  (  ( ph /\ 1 < ( N gcd R ) )
                                  /\ p e. Prime )
                               /\ ( p || R /\ -. p || N ) )
                            /\ ( R / ( N gcd R ) ) || A )
                         /\ ( R / p ) || A )
                      ->   ( ( R / ( p ^ ( p pCnt R ) ) )
                             gcd
                             ( p ^ ( p pCnt R ) ) )
                         = 1 )
!316::             |- (  (  (  (  (  ( ph /\ 1 < ( N gcd R ) )
                                  /\ p e. Prime )
                               /\ ( p || R /\ -. p || N ) )
                            /\ ( R / ( N gcd R ) ) || A )
                         /\ ( R / p ) || A )
                      -> ( R / ( p ^ ( p pCnt R ) ) )
                         ||
                         A )
!317::             |- (  (  (  (  (  ( ph /\ 1 < ( N gcd R ) )
                                  /\ p e. Prime )
                               /\ ( p || R /\ -. p || N ) )
                            /\ ( R / ( N gcd R ) ) || A )
                         /\ ( R / p ) || A )
                      -> ( p ^ ( p pCnt R ) ) || A )
318:308,313,314,315,316,317:coprmdvds2d |- (  (  (  (  (  ( ph /\ 1 < ( N gcd R ) )
                                  /\ p e. Prime )
                               /\ ( p || R /\ -. p || N ) )
                            /\ ( R / ( N gcd R ) ) || A )
                         /\ ( R / p ) || A )
                      -> ( ( R / ( p ^ ( p pCnt R ) ) )
                           x.
                           ( p ^ ( p pCnt R ) ) )
                         ||
                         A )
319:307,318:eqbrtrd |- (  (  (  (  (  ( ph /\ 1 < ( N gcd R ) )
                                  /\ p e. Prime )
                               /\ ( p || R /\ -. p || N ) )
                            /\ ( R / ( N gcd R ) ) || A )
                         /\ ( R / p ) || A )
                      -> R || A )
320:211:ad5antr    |- (  (  (  (  (  ( ph /\ 1 < ( N gcd R ) )
                                  /\ p e. Prime )
                               /\ ( p || R /\ -. p || N ) )
                            /\ ( R / ( N gcd R ) ) || A )
                         /\ ( R / p ) || A )
                      -> -. R || A )
321:319,320:pm2.65da |- (  (  (  (  ( ph /\ 1 < ( N gcd R ) )
                               /\ p e. Prime )
                            /\ ( p || R /\ -. p || N ) )
                         /\ ( R / ( N gcd R ) ) || A )
                      -> -. ( R / p ) || A )

[metakunt]

This is what chatgpt told me:

Thank you for the clarification! Let's break this down step by step, with the goal of proving that \( \frac{R}{p} \) does not divide \( A \), given the following facts:

1. \( p \) is a prime number that divides \( R \) (i.e., \( p \mid R \)),
2. \( p \mid A \) (i.e., \( p \) divides \( A \)),
3. \( R \nmid A \) (i.e., \( R \) does not divide \( A \)).

We want to prove that \( \frac{R}{p} \nmid A \) — that is, \( \frac{R}{p} \) does not divide \( A \).

### Step-by-step Proof Outline:

#### Step 1: Express \( R \) in terms of \( p \)
Since \( p \mid R \), we know that \( R = p \cdot k \) for some integer \( k \).

#### Step 2: Use the assumption that \( p \mid A \)
We are given that \( p \mid A \), so \( A = p \cdot m \) for some integer \( m \).

#### Step 3: Analyze the divisibility of \( R \) and \( A \)
We know \( R = p \cdot k \) and \( A = p \cdot m \). Now, if \( R \) divides \( A \), we would expect that:

\[
A = R \cdot q \text{ for some integer } q.
\]

Substitute \( R = p \cdot k \) and \( A = p \cdot m \):

\[
p \cdot m = (p \cdot k) \cdot q.
\]

Dividing both sides by \( p \) (which is nonzero since \( p \) is a prime), we get:

\[
m = k \cdot q.
\]

This would imply that \( m \) is divisible by \( k \), i.e., \( k \mid m \). 

#### Step 4: Use the fact that \( R \nmid A \)
However, we are told that \( R \nmid A \). This means that \( k \nmid m \), or equivalently, \( m \) is **not** divisible by \( k \).

Thus, \( R \nmid A \) implies that it is **not** possible for \( m \) to be divisible by \( k \).

#### Step 5: Analyze \( \frac{R}{p} \)
Now, let's consider the quantity \( \frac{R}{p} = k \). We want to show that \( k \nmid m \), or equivalently that \( \frac{R}{p} \nmid A \).

Since \( R = p \cdot k \) and \( A = p \cdot m \), if \( \frac{R}{p} = k \) divides \( A \), it would imply that:

\[
m = k \cdot q
\]

for some integer \( q \). But from Step 4, we know that \( k \nmid m \), so this is impossible.

Therefore, \( k \nmid m \), which means \( \frac{R}{p} \nmid A \).

### Conclusion:
Thus, we have shown that if \( p \mid R \), \( p \mid A \), and \( R \nmid A \), then \( \frac{R}{p} \nmid A \).

[metakunt]

Or counterquestion: Is the following theorem correct?

  ${
    aks4d1p8d2.1 $e |- ( ph -> P e. Prime ) $.
    aks4d1p8d2.2 $e |- ( ph -> R e. ZZ ) $.
    aks4d1p8d2.3 $e |- ( ph -> A e. ZZ ) $.
    aks4d1p8d2.4 $e |- ( ph -> P || A ) $.
    aks4d1p8d2.5 $e |- ( ph -> -. R || A ) $.
    aks4d1p8d2 $p |- ( ph -> -. ( R / P ) || A ) $= ? $.
  $}

If the lemma above is correct that would successfully close the proof. I have no idea how to prove it though as I have spent few hours on it.

This seems wrong though, for example p=2 A=4 R=8, we have 2 divides 4 and 8 does not divide 4 but 8/2 divides 4. So this is wrong.

I need a different statement to formalise.

[langgerard]

If P is a prime divisor of the integer A, and if R is any integer not dividing A, there is no reason that P would be a divisor of R, so that R/P cannot be an integer.

[metakunt]

I think we know a bit more, for context I am trying to formalise Lemma 4.1:
https://www3.nd.edu/~andyp/notes/AKS.pdf
I want to formalise this statement in particular

If every prime divisor of r also divided n, then this would imply that r divided

$$n^{\lfloor \log_2(B)\rfloor}$$

contradicting our choice of r. From this, we see that r/ gcd(n, r) must also not divide A.

I have already proven

$$R \vert n^{\lfloor \log_2(B)\rfloor}$$

in https://us.metamath.org/mpeuni/aks4d1p7d1.html

I guess I could finish the proof quite easily by showing that if A does not divide B, then

$$\frac{A}{gcd(A,B)} \text{ does not divide } B$$

I'm not sure if we have that theorem in main. But that theorem would indeed close the goal, if it is correct.

Maybe I just need to shift the divisor of coprmdvds2d to get the desired result?

[langgerard]

If I understand you correctly, you want to prove that if the integer A is not a divisor of the integer b, then the integer A/gcd(A,B) is not a divisor of B. Let us suppose that A is a divisor of the product B.gcd(A,B), then because A is not a divisor of B, A must be a divisor of gcd(A,B). But we know that gcd(A,B) is always a divisor of A. And because A and gcd(A,B) are boh positive integers, we must then have A = gcd(A,B). And because gcd(A,B) is always a divisor of B, we should have that A is a divisor of B, contradicting our hypothesis. So that A/gcd(A,B) cannot be a divisor of B.

…

Le 12 nov. 2024 à 18:25, metakunt ***@***.***> a écrit : I think we know a bit more, for context I am trying to formalise Lemma 4.1: https://www3.nd.edu/~andyp/notes/AKS.pdf I want to formalise this statement in particular If every prime divisor of r also divided n, then this would imply that r divided $$n^{\lfloor \log_2(B)\rfloor}$$ contradicting our choice of r. From this, we see that r/ gcd(n, r) must also not divide A. I have already proven $$R \vert n^{\lfloor \log_2(B)\rfloor}$$ in https://us.metamath.org/mpeuni/aks4d1p7d1.html I guess I could finish the proof quite easily by showing that if A does not divide B, then $$\frac{A}{gcd(A,B)} \text{ does not divide } B$$ I'm not sure if we have that theorem in main. But that theorem would indeed close the goal, if it is correct. Maybe I just need to shift the divisor of coprmdvds2d to get the desired result? — Reply to this email directly, view it on GitHub <#4382 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ANSR5QSAB6MS5FZHNGCZ2CL2AI2W3AVCNFSM6AAAAABRQO4OUKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINZRGE2DIMZZHE>. You are receiving this because you commented.

[metakunt]

Not quite: Here is the statement I need to show to close the goal:

350: |- (  (  (  (  ( ph /\ 1 < ( N gcd R ) )
                               /\ p e. Prime )
                            /\ ( p || R /\ -. p || N ) )
                         /\ ( R / ( N gcd R ) ) || A )
                      -> -. ( R / p ) || A )

I need to show that (R/p) does not divide A.
Here is the context of the proof.

The definition of R is the smallest number that does not divide A, I have shown that it exists and that it is smaller than B.
I have also shown that there exist a prime p that divides R but not N, not sure how that helps me.

A proof of contradiction would work by decomposing R into a product qs, where q and s are coprime and both strictly smaller than R, then we have that q divides A and s divides A, and together with the coprimality of q and s we also have that qs divides A, but qs=r which by hypothesis does not divide A, which is a contradiction and this closes the goal.

https://www3.nd.edu/~andyp/notes/AKS.pdf just nonchalantly mentions that R/gcd(R,n) must not divide A, but this is what I am trying to prove.
In #4347 I have tried to explain what I need to show and where I am stuck and @tirix has drafted very thankfully a proof outline for me.
I could formalise all steps besides the step above, which states that (R/p) does not divide A. This is absurd, which means the hypotheses and the context are wrong, in our case it is 1 < ( N gcd R ). So I need to use the assumption that N and R are not coprime to derive to a contradiction.

Here is the context once more

|- ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) /\ ( R / ( N gcd R ) ) || A ) -> p || A )
|- ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) /\ ( R / ( N gcd R ) ) || A ) -> -. R || A )
|- ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) /\ ( R / ( N gcd R ) ) || A ) -> -. ( R / p ) || A )

And in prosa: Assume there exists an integer R that does not divide A, further more assume that there exists a prime that does divide A, then (R/p) also does not divide A.

It seems tempting to directly argue that we can use https://us.metamath.org/mpeuni/coprmdvds2d.html to arrive to a contradiction, but this fails for the following simple reason that we don't know that (R/p) and p are coprime.
Basically we need to show aswell that p has multiplicity 1. We need to use multiple facts that are complicatedly interwoven. The proof context is utterly polluted and in my opinion highly nontrivial.

It is unclear which facts from this proof context matter, here are some examples:
The fact that even a number less than B exists that does not divide A is remarkably difficult to show, it encompasses more than 50 theorems in my mathbox and ends in a proof of contradiction
https://us.metamath.org/mpeuni/aks4d1p1.html and
https://us.metamath.org/mpeuni/aks4d1p2.html which lead to the existence of a non-divisor
https://us.metamath.org/mpeuni/aks4d1p3.html

Now with that information equipped we can define R to be the smallest integer that does not divide A and we can also show that it exists, which is
https://us.metamath.org/mpeuni/aks4d1p4.html

https://us.metamath.org/mpeuni/aks4d1p5.html tries to prove the coprimality of R and N with the additional absurd assumption that 1 < gcd(N,R), we now need to discharge this assumption.
https://us.metamath.org/mpeuni/aks4d1p6.html shows that the multiplicity of the prime factors of R is bounded, as such if all prime factors of R also divide N, then we have that R divides A, which is a contradiction. This however means that there exists a prime factor of R, here called p, that does not divide N.
This is shown in https://us.metamath.org/mpeuni/aks4d1p7d1.html and https://us.metamath.org/mpeuni/aks4d1p7.html

Now we somehow need to arrive to a contradiction and here is where I am struggling hard. This statement

From this, we see that r/ gcd(n, r) must also not divide A.

is a non-sequitur to me. I have looked at the main theorems regarding coprimality and dividing the gcd but nothing seems to work. It basically says take the prime decomposition of r/gcd(n,r) which includes all prime factors of r which are not part of n and show that this also does not divide A. But here it is unclear what the primitive mathematical justification for that is. Intuitively the only part where the multiplicities of n arise is the first factor of A.

Thereby I am hoping that gcd(n,r) divides the second factor of A. Essentially any coprime decomposition helps.

As you can see the proof context is quite polluted and I am helpless here.

I assume I need the following: By the proof context I have

1 < gcd(N,R)

By ( p || R /\ -. p || N ) I can assume that

gcd(N,R)<R

Therefore we have that the greatest common divisor of R and N is strictly between 1 and R, now all we need to do is to find one coprime factorisation of R into factors and likely use https://us.metamath.org/mpeuni/coprmdvds2d.html to show that R divides A, which is a contradiction.

But still I feel very close yet very far. While I have lots of ideas how to prove it every attempt as failed so far. It just feels that the theorem has a very sneaky non-triviality that I have just missed. And finding it is very hard because you don't know which of the several facts are actually relevant.

[metakunt]

I think this ansatz may work.

!372::             |- (  (  (  ( ph /\ 1 < ( N gcd R ) )
                            /\ p e. Prime )
                         /\ ( p || R /\ -. p || N ) )
                      ->   ( ( R / ( p ^ ( p pCnt R ) ) )
                             gcd
                             ( p ^ ( p pCnt R ) ) )
                         = 1 )
!373::             |- (  (  (  ( ph /\ 1 < ( N gcd R ) )
                            /\ p e. Prime )
                         /\ ( p || R /\ -. p || N ) )
                      -> ( R / ( p ^ ( p pCnt R ) ) )
                         ||
                         A )
!374::             |- (  (  (  ( ph /\ 1 < ( N gcd R ) )
                            /\ p e. Prime )
                         /\ ( p || R /\ -. p || N ) )
                      -> ( p ^ ( p pCnt R ) ) || A )
375:365,368,369,372,373,374:coprmdvds2d 
                   |- (  (  (  ( ph /\ 1 < ( N gcd R ) )
                            /\ p e. Prime )
                         /\ ( p || R /\ -. p || N ) )
                      -> ( ( R / ( p ^ ( p pCnt R ) ) )
                           x.
                           ( p ^ ( p pCnt R ) ) )
                         ||
                         A )

372 is true because for any prime factor q, either q=p which does not divide the lhs or q!=p which does not divide the rhs. As such both have no prime factors in common.
373 is true because R/p^k is smaller than R
374 is true because p^k is less than R, indeed if it were equal to R, then we have a contradiction which I can't see yet.

I am dizzy...

[icecream17]

350: |- (  (  (  (  ( ph /\ 1 < ( N gcd R ) )
                               /\ p e. Prime )
                            /\ ( p || R /\ -. p || N ) )
                         /\ ( R / ( N gcd R ) ) || A )
                      -> -. ( R / p ) || A )

looks impossible without restrictions on A, since A = ( R / ( N gcd R ) ) x. ( R / p ) (and R = 6, N = 2, p = 3) is possible

Edit: There are restrictions on A of course... nevermind

A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )

[tirix]

@metakunt Yes, there be some issue with my last proposal, sorry I misled you.
I'll try to review my proposal and check where my mistake is.

[metakunt]

@tirix No issues, it's a very convoluted proof indeed and neither author in the papers bothered to mention the critical step. I think I have figured out how to remedy it.

Basically the core idea of 1<gcd(N,R) is that there exists a prime q that divides both N and R, but p divides R but not N, which means R has at least two prime factors. From that we know that both p^k is smaller than R, because p^k*q is less or equal to R and R/p^k is also less than R, because we divide by something greater than 1.

They are obviously coprime, because p^k has only p as prime factor, but we have divided that one out in R/p^k. However sadly there is no theorem that explicitly states that in main ;(
I think now that sounds plausible and I have finally found the justification for 374.

[metakunt]

The proof was quite nice to formalise once I knew that there are two prime divisors of R. Can't believe that it took me that long to find it.

[tirix]

Very nice!

You really should not attribute to me the proof of aks4d1p8, that's fully yours.

[metakunt]

I've updated the contributor. I still kept you as proof sketch author since your work was very important and helpful to me.

This proof was a chore to formalise as both authors were failing to see the core idea why that proof works and I had to sadly figure it out myself. I think I've overall spent over 20 hours just trying to get the last line to work.