Metamath Proof Explorer

Theorem aks4d1p5

Description: Show that N and R are coprime for AKS existence theorem. Precondition will be eliminated in further theorem. (Contributed by metakunt, 30-Oct-2024)

Ref Expression
Hypotheses aks4d1p5.1 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks4d1p5.2 
|- A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
aks4d1p5.3 
|- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
aks4d1p5.4 
|- R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < )
aks4d1p5.5 
|- ( ( ( ph /\ 1 < ( N gcd R ) ) /\ ( R / ( N gcd R ) ) || A ) -> -. ( R / ( N gcd R ) ) || A )
Assertion aks4d1p5 
|- ( ph -> ( N gcd R ) = 1 )

Proof

Step Hyp Ref Expression
1 aks4d1p5.1 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
2 aks4d1p5.2 
 |-  A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
3 aks4d1p5.3 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
4 aks4d1p5.4 
 |-  R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < )
5 aks4d1p5.5 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ ( R / ( N gcd R ) ) || A ) -> -. ( R / ( N gcd R ) ) || A )
6 simpr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ R <_ ( R / ( N gcd R ) ) ) -> R <_ ( R / ( N gcd R ) ) )
7 1 2 3 4 aks4d1p4 
 |-  ( ph -> ( R e. ( 1 ... B ) /\ -. R || A ) )
8 7 simpld 
 |-  ( ph -> R e. ( 1 ... B ) )
9 elfznn 
 |-  ( R e. ( 1 ... B ) -> R e. NN )
10 8 9 syl 
 |-  ( ph -> R e. NN )
11 10 nnred 
 |-  ( ph -> R e. RR )
12 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
13 1 12 syl 
 |-  ( ph -> N e. ZZ )
14 0red 
 |-  ( ph -> 0 e. RR )
15 3re 
 |-  3 e. RR
16 15 a1i 
 |-  ( ph -> 3 e. RR )
17 13 zred 
 |-  ( ph -> N e. RR )
18 3pos 
 |-  0 < 3
19 18 a1i 
 |-  ( ph -> 0 < 3 )
20 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
21 1 20 syl 
 |-  ( ph -> 3 <_ N )
22 14 16 17 19 21 ltletrd 
 |-  ( ph -> 0 < N )
23 13 22 jca 
 |-  ( ph -> ( N e. ZZ /\ 0 < N ) )
24 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
25 23 24 sylibr 
 |-  ( ph -> N e. NN )
26 gcdnncl 
 |-  ( ( N e. NN /\ R e. NN ) -> ( N gcd R ) e. NN )
27 25 10 26 syl2anc 
 |-  ( ph -> ( N gcd R ) e. NN )
28 27 nnred 
 |-  ( ph -> ( N gcd R ) e. RR )
29 27 nnne0d 
 |-  ( ph -> ( N gcd R ) =/= 0 )
30 11 28 29 redivcld 
 |-  ( ph -> ( R / ( N gcd R ) ) e. RR )
31 30 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / ( N gcd R ) ) e. RR )
32 11 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R e. RR )
33 31 32 ltnled 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( ( R / ( N gcd R ) ) < R <-> -. R <_ ( R / ( N gcd R ) ) ) )
34 33 biimprd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( -. R <_ ( R / ( N gcd R ) ) -> ( R / ( N gcd R ) ) < R ) )
35 34 imp 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ -. R <_ ( R / ( N gcd R ) ) ) -> ( R / ( N gcd R ) ) < R )
36 4 a1i 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) )
37 ssrab2 
 |-  { r e. ( 1 ... B ) | -. r || A } C_ ( 1 ... B )
38 37 a1i 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } C_ ( 1 ... B ) )
39 elfznn 
 |-  ( o e. ( 1 ... B ) -> o e. NN )
40 39 adantl 
 |-  ( ( ph /\ o e. ( 1 ... B ) ) -> o e. NN )
41 40 nnred 
 |-  ( ( ph /\ o e. ( 1 ... B ) ) -> o e. RR )
42 41 ex 
 |-  ( ph -> ( o e. ( 1 ... B ) -> o e. RR ) )
43 42 ssrdv 
 |-  ( ph -> ( 1 ... B ) C_ RR )
44 38 43 sstrd 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
45 44 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
46 fzfid 
 |-  ( ph -> ( 1 ... B ) e. Fin )
47 46 38 ssfid 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } e. Fin )
48 47 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> { r e. ( 1 ... B ) | -. r || A } e. Fin )
49 1 2 3 aks4d1p3 
 |-  ( ph -> E. r e. ( 1 ... B ) -. r || A )
50 rabn0 
 |-  ( { r e. ( 1 ... B ) | -. r || A } =/= (/) <-> E. r e. ( 1 ... B ) -. r || A )
51 49 50 sylibr 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } =/= (/) )
52 51 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> { r e. ( 1 ... B ) | -. r || A } =/= (/) )
53 fiminre 
 |-  ( ( { r e. ( 1 ... B ) | -. r || A } C_ RR /\ { r e. ( 1 ... B ) | -. r || A } e. Fin /\ { r e. ( 1 ... B ) | -. r || A } =/= (/) ) -> E. x e. { r e. ( 1 ... B ) | -. r || A } A. y e. { r e. ( 1 ... B ) | -. r || A } x <_ y )
54 45 48 52 53 syl3anc 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> E. x e. { r e. ( 1 ... B ) | -. r || A } A. y e. { r e. ( 1 ... B ) | -. r || A } x <_ y )
55 breq1 
 |-  ( r = ( R / ( N gcd R ) ) -> ( r || A <-> ( R / ( N gcd R ) ) || A ) )
56 55 notbid 
 |-  ( r = ( R / ( N gcd R ) ) -> ( -. r || A <-> -. ( R / ( N gcd R ) ) || A ) )
57 1zzd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> 1 e. ZZ )
58 3 a1i 
 |-  ( ph -> B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
59 2re 
 |-  2 e. RR
60 59 a1i 
 |-  ( ph -> 2 e. RR )
61 2pos 
 |-  0 < 2
62 61 a1i 
 |-  ( ph -> 0 < 2 )
63 1red 
 |-  ( ph -> 1 e. RR )
64 1lt2 
 |-  1 < 2
65 64 a1i 
 |-  ( ph -> 1 < 2 )
66 63 65 ltned 
 |-  ( ph -> 1 =/= 2 )
67 66 necomd 
 |-  ( ph -> 2 =/= 1 )
68 60 62 17 22 67 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
69 5nn0 
 |-  5 e. NN0
70 69 a1i 
 |-  ( ph -> 5 e. NN0 )
71 68 70 reexpcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) e. RR )
72 ceilcl 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
73 71 72 syl 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
74 58 73 eqeltrd 
 |-  ( ph -> B e. ZZ )
75 74 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> B e. ZZ )
76 25 nnzd 
 |-  ( ph -> N e. ZZ )
77 divgcdnnr 
 |-  ( ( R e. NN /\ N e. ZZ ) -> ( R / ( N gcd R ) ) e. NN )
78 10 76 77 syl2anc 
 |-  ( ph -> ( R / ( N gcd R ) ) e. NN )
79 78 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / ( N gcd R ) ) e. NN )
80 79 nnzd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / ( N gcd R ) ) e. ZZ )
81 79 nnge1d 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> 1 <_ ( R / ( N gcd R ) ) )
82 75 zred 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> B e. RR )
83 10 nnrpd 
 |-  ( ph -> R e. RR+ )
84 83 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R e. RR+ )
85 27 nnrpd 
 |-  ( ph -> ( N gcd R ) e. RR+ )
86 85 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( N gcd R ) e. RR+ )
87 32 recnd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R e. CC )
88 84 rpne0d 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R =/= 0 )
89 87 88 dividd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / R ) = 1 )
90 simpr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> 1 < ( N gcd R ) )
91 89 90 eqbrtrd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / R ) < ( N gcd R ) )
92 32 84 86 91 ltdiv23d 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / ( N gcd R ) ) < R )
93 31 32 92 ltled 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / ( N gcd R ) ) <_ R )
94 elfzle2 
 |-  ( R e. ( 1 ... B ) -> R <_ B )
95 8 94 syl 
 |-  ( ph -> R <_ B )
96 95 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R <_ B )
97 31 32 82 93 96 letrd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / ( N gcd R ) ) <_ B )
98 57 75 80 81 97 elfzd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / ( N gcd R ) ) e. ( 1 ... B ) )
99 simpr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ -. ( R / ( N gcd R ) ) || A ) -> -. ( R / ( N gcd R ) ) || A )
100 exmidd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( ( R / ( N gcd R ) ) || A \/ -. ( R / ( N gcd R ) ) || A ) )
101 5 99 100 mpjaodan 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> -. ( R / ( N gcd R ) ) || A )
102 56 98 101 elrabd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / ( N gcd R ) ) e. { r e. ( 1 ... B ) | -. r || A } )
103 lbinfle 
 |-  ( ( { r e. ( 1 ... B ) | -. r || A } C_ RR /\ E. x e. { r e. ( 1 ... B ) | -. r || A } A. y e. { r e. ( 1 ... B ) | -. r || A } x <_ y /\ ( R / ( N gcd R ) ) e. { r e. ( 1 ... B ) | -. r || A } ) -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( R / ( N gcd R ) ) )
104 45 54 102 103 syl3anc 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( R / ( N gcd R ) ) )
105 36 104 eqbrtrd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R <_ ( R / ( N gcd R ) ) )
106 32 31 lenltd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R <_ ( R / ( N gcd R ) ) <-> -. ( R / ( N gcd R ) ) < R ) )
107 105 106 mpbid 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> -. ( R / ( N gcd R ) ) < R )
108 107 adantr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ -. R <_ ( R / ( N gcd R ) ) ) -> -. ( R / ( N gcd R ) ) < R )
109 35 108 pm2.21dd 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ -. R <_ ( R / ( N gcd R ) ) ) -> R <_ ( R / ( N gcd R ) ) )
110 6 109 pm2.61dan 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R <_ ( R / ( N gcd R ) ) )
111 83 rpred 
 |-  ( ph -> R e. RR )
112 111 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R e. RR )
113 92 107 pm2.21dd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( N gcd R ) e. NN )
114 113 nnrpd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( N gcd R ) e. RR+ )
115 112 recnd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R e. CC )
116 115 88 dividd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / R ) = 1 )
117 116 90 eqbrtrd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / R ) < ( N gcd R ) )
118 112 84 114 117 ltdiv23d 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( R / ( N gcd R ) ) < R )
119 78 nnred 
 |-  ( ph -> ( R / ( N gcd R ) ) e. RR )
120 119 111 ltnled 
 |-  ( ph -> ( ( R / ( N gcd R ) ) < R <-> -. R <_ ( R / ( N gcd R ) ) ) )
121 120 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( ( R / ( N gcd R ) ) < R <-> -. R <_ ( R / ( N gcd R ) ) ) )
122 118 121 mpbid 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> -. R <_ ( R / ( N gcd R ) ) )
123 110 122 pm2.21dd 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> ( N gcd R ) = 1 )
124 simpr 
 |-  ( ( ( ph /\ -. 1 < ( N gcd R ) ) /\ ( N gcd R ) = 1 ) -> ( N gcd R ) = 1 )
125 27 adantr 
 |-  ( ( ph /\ -. 1 < ( N gcd R ) ) -> ( N gcd R ) e. NN )
126 125 nnred 
 |-  ( ( ph /\ -. 1 < ( N gcd R ) ) -> ( N gcd R ) e. RR )
127 126 adantr 
 |-  ( ( ( ph /\ -. 1 < ( N gcd R ) ) /\ ( N gcd R ) e. ( ZZ>= ` 2 ) ) -> ( N gcd R ) e. RR )
128 59 a1i 
 |-  ( ( ( ph /\ -. 1 < ( N gcd R ) ) /\ ( N gcd R ) e. ( ZZ>= ` 2 ) ) -> 2 e. RR )
129 1red 
 |-  ( ( ( ph /\ -. 1 < ( N gcd R ) ) /\ ( N gcd R ) e. ( ZZ>= ` 2 ) ) -> 1 e. RR )
130 28 63 lenltd 
 |-  ( ph -> ( ( N gcd R ) <_ 1 <-> -. 1 < ( N gcd R ) ) )
131 130 biimprd 
 |-  ( ph -> ( -. 1 < ( N gcd R ) -> ( N gcd R ) <_ 1 ) )
132 131 imp 
 |-  ( ( ph /\ -. 1 < ( N gcd R ) ) -> ( N gcd R ) <_ 1 )
133 132 adantr 
 |-  ( ( ( ph /\ -. 1 < ( N gcd R ) ) /\ ( N gcd R ) e. ( ZZ>= ` 2 ) ) -> ( N gcd R ) <_ 1 )
134 64 a1i 
 |-  ( ( ( ph /\ -. 1 < ( N gcd R ) ) /\ ( N gcd R ) e. ( ZZ>= ` 2 ) ) -> 1 < 2 )
135 127 129 128 133 134 lelttrd 
 |-  ( ( ( ph /\ -. 1 < ( N gcd R ) ) /\ ( N gcd R ) e. ( ZZ>= ` 2 ) ) -> ( N gcd R ) < 2 )
136 eluzle 
 |-  ( ( N gcd R ) e. ( ZZ>= ` 2 ) -> 2 <_ ( N gcd R ) )
137 136 adantl 
 |-  ( ( ( ph /\ -. 1 < ( N gcd R ) ) /\ ( N gcd R ) e. ( ZZ>= ` 2 ) ) -> 2 <_ ( N gcd R ) )
138 127 128 127 135 137 ltletrd 
 |-  ( ( ( ph /\ -. 1 < ( N gcd R ) ) /\ ( N gcd R ) e. ( ZZ>= ` 2 ) ) -> ( N gcd R ) < ( N gcd R ) )
139 127 ltnrd 
 |-  ( ( ( ph /\ -. 1 < ( N gcd R ) ) /\ ( N gcd R ) e. ( ZZ>= ` 2 ) ) -> -. ( N gcd R ) < ( N gcd R ) )
140 138 139 pm2.21dd 
 |-  ( ( ( ph /\ -. 1 < ( N gcd R ) ) /\ ( N gcd R ) e. ( ZZ>= ` 2 ) ) -> ( N gcd R ) = 1 )
141 elnn1uz2 
 |-  ( ( N gcd R ) e. NN <-> ( ( N gcd R ) = 1 \/ ( N gcd R ) e. ( ZZ>= ` 2 ) ) )
142 125 141 sylib 
 |-  ( ( ph /\ -. 1 < ( N gcd R ) ) -> ( ( N gcd R ) = 1 \/ ( N gcd R ) e. ( ZZ>= ` 2 ) ) )
143 124 140 142 mpjaodan 
 |-  ( ( ph /\ -. 1 < ( N gcd R ) ) -> ( N gcd R ) = 1 )
144 123 143 pm2.61dan 
 |-  ( ph -> ( N gcd R ) = 1 )