Theorem 4.1 of aks - Githubissues

Hey @tirix I have formalised the following theorem, which I will be opening a pr once the current pr is merged.

    aks4d1p3.1 $e |- ( ph -> N e. ( ZZ>= ` 3 ) ) $.
    aks4d1p3.2 $e |- A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e.
     ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) $.
    aks4d1p3.3 $e |- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) $.
    aks4d1p3 $p |- ( ph -> E. r e. ( 1 ... B ) -. r || A ) $.

Now I am struggling to dissect the proof in https://www3.nd.edu/~andyp/notes/AKS.pdf We conclude that some element of {1, . . . , B} does not divide A, so r ≤ B, as claimed. We now prove that gcd (n, r) = 1. If p is a prime divisor of r and pk is the maximal power of p dividing r, then since pk ≤ r ≤ B we must have k ≤ blog(B)/ log(p)c ≤ blog(B)c. If every prime divisor of r also divided n, then this would imply that r divided nblog Bc, contradicting our choice of r. From this, we see that r/ gcd(n, r) must also not divide A. Since r is the smallest integer not dividing A, we deduce that gcd(n, r) = 1, as claimed.

Let me try to find the necessary theorems to prove:

Let $$r \in \mathbb{N}$$, p prime and let $$k = sup( {k \in \mathbb{N} | p^k \text{divides~} r}) $$. By assumption
```
p^k \leq r
```
By previous proof
```
r \leq B 
```
By transitivity
```
p^k \leq B 
```
By logarithm monitonicity
```
k \leq log_p(B)
```
Since in our case we use the binary logarithm $$lb$$ we have
```
k \leq lb(B)/lb(p)
```
where $$lb(p) \geq 1 $$, since 2 is the smallest prime. Therefore
```
k \leq lb(B)
```
Introducing the floor is done by https://us.metamath.org/mpeuni/flge.html
```
k \leq \lfloor lb(B) \rfloor
```
Now it gets interesting: The statement to formalise is If every prime divisor of r also divided n, then this would imply that r divided $$n^{\lfloor lb(B) \rfloor}$$, I assume this is because $${\lfloor lb(B) \rfloor}$$ is a natural number and we have the monotonicity of exponentiation.https://us.metamath.org/mpeuni/leexp2ad.html

The last two statements are up in the air contradicting our choice of r. From this, we see that r/ gcd(n, r) must also not divide A. Since r is the smallest integer not dividing A, we deduce that gcd(n, r) = 1, as claimed

I don't know what api do we have in the database to formalise this. If we could find a general statement that I could work on that would be great, as I don't know how to proceed. I assume we need to have use the maximality of k in some way. That would mean to use sup and its sup* theorems. Not sure how enjoyable this will be.

tirix / metamath-blueprints

Theorem 4.1 of aks #12