Metamath Proof Explorer

Theorem aks4d1p7

Description: Technical step in AKS lemma 4.1. (Contributed by metakunt, 31-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 aks4d1p7.1 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
2 aks4d1p7.2 
 |-  A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
3 aks4d1p7.3 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
4 aks4d1p7.4 
 |-  R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < )
5 1 adantr 
 |-  ( ( ph /\ A. p e. Prime ( p || R -> p || N ) ) -> N e. ( ZZ>= ` 3 ) )
6 breq1 
 |-  ( p = q -> ( p || R <-> q || R ) )
7 breq1 
 |-  ( p = q -> ( p || N <-> q || N ) )
8 6 7 imbi12d 
 |-  ( p = q -> ( ( p || R -> p || N ) <-> ( q || R -> q || N ) ) )
9 8 cbvralvw 
 |-  ( A. p e. Prime ( p || R -> p || N ) <-> A. q e. Prime ( q || R -> q || N ) )
10 9 bilani 
 |-  ( ( ph /\ A. p e. Prime ( p || R -> p || N ) ) -> A. q e. Prime ( q || R -> q || N ) )
11 5 2 3 4 10 aks4d1p7d1 
 |-  ( ( ph /\ A. p e. Prime ( p || R -> p || N ) ) -> R || ( N ^ ( |_ ` ( 2 logb B ) ) ) )
12 4 a1i 
 |-  ( ph -> R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) )
13 ltso 
 |-  < Or RR
14 13 a1i 
 |-  ( ph -> < Or RR )
15 fzfid 
 |-  ( ph -> ( 1 ... B ) e. Fin )
16 ssrab2 
 |-  { r e. ( 1 ... B ) | -. r || A } C_ ( 1 ... B )
17 16 a1i 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } C_ ( 1 ... B ) )
18 15 17 ssfid 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } e. Fin )
19 1 2 3 aks4d1p3 
 |-  ( ph -> E. r e. ( 1 ... B ) -. r || A )
20 rabn0 
 |-  ( { r e. ( 1 ... B ) | -. r || A } =/= (/) <-> E. r e. ( 1 ... B ) -. r || A )
21 19 20 sylibr 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } =/= (/) )
22 elfznn 
 |-  ( o e. ( 1 ... B ) -> o e. NN )
23 22 adantl 
 |-  ( ( ph /\ o e. ( 1 ... B ) ) -> o e. NN )
24 23 nnred 
 |-  ( ( ph /\ o e. ( 1 ... B ) ) -> o e. RR )
25 24 ex 
 |-  ( ph -> ( o e. ( 1 ... B ) -> o e. RR ) )
26 25 ssrdv 
 |-  ( ph -> ( 1 ... B ) C_ RR )
27 17 26 sstrd 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
28 18 21 27 3jca 
 |-  ( ph -> ( { r e. ( 1 ... B ) | -. r || A } e. Fin /\ { r e. ( 1 ... B ) | -. r || A } =/= (/) /\ { r e. ( 1 ... B ) | -. r || A } C_ RR ) )
29 fiinfcl 
 |-  ( ( < Or RR /\ ( { r e. ( 1 ... B ) | -. r || A } e. Fin /\ { r e. ( 1 ... B ) | -. r || A } =/= (/) /\ { r e. ( 1 ... B ) | -. r || A } C_ RR ) ) -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) e. { r e. ( 1 ... B ) | -. r || A } )
30 14 28 29 syl2anc 
 |-  ( ph -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) e. { r e. ( 1 ... B ) | -. r || A } )
31 12 30 eqeltrd 
 |-  ( ph -> R e. { r e. ( 1 ... B ) | -. r || A } )
32 breq1 
 |-  ( r = R -> ( r || A <-> R || A ) )
33 32 notbid 
 |-  ( r = R -> ( -. r || A <-> -. R || A ) )
34 33 elrab 
 |-  ( R e. { r e. ( 1 ... B ) | -. r || A } <-> ( R e. ( 1 ... B ) /\ -. R || A ) )
35 31 34 sylib 
 |-  ( ph -> ( R e. ( 1 ... B ) /\ -. R || A ) )
36 35 simprd 
 |-  ( ph -> -. R || A )
37 1 2 3 4 aks4d1p4 
 |-  ( ph -> ( R e. ( 1 ... B ) /\ -. R || A ) )
38 37 simpld 
 |-  ( ph -> R e. ( 1 ... B ) )
39 38 elfzelzd 
 |-  ( ph -> R e. ZZ )
40 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
41 1 40 syl 
 |-  ( ph -> N e. ZZ )
42 2re 
 |-  2 e. RR
43 42 a1i 
 |-  ( ph -> 2 e. RR )
44 2pos 
 |-  0 < 2
45 44 a1i 
 |-  ( ph -> 0 < 2 )
46 3 a1i 
 |-  ( ph -> B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
47 41 zred 
 |-  ( ph -> N e. RR )
48 0red 
 |-  ( ph -> 0 e. RR )
49 3re 
 |-  3 e. RR
50 49 a1i 
 |-  ( ph -> 3 e. RR )
51 3pos 
 |-  0 < 3
52 51 a1i 
 |-  ( ph -> 0 < 3 )
53 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
54 1 53 syl 
 |-  ( ph -> 3 <_ N )
55 48 50 47 52 54 ltletrd 
 |-  ( ph -> 0 < N )
56 1red 
 |-  ( ph -> 1 e. RR )
57 1lt2 
 |-  1 < 2
58 57 a1i 
 |-  ( ph -> 1 < 2 )
59 56 58 ltned 
 |-  ( ph -> 1 =/= 2 )
60 59 necomd 
 |-  ( ph -> 2 =/= 1 )
61 43 45 47 55 60 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
62 5nn0 
 |-  5 e. NN0
63 62 a1i 
 |-  ( ph -> 5 e. NN0 )
64 61 63 reexpcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) e. RR )
65 64 ceilcld 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
66 65 zred 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. RR )
67 46 66 eqeltrd 
 |-  ( ph -> B e. RR )
68 9re 
 |-  9 e. RR
69 68 a1i 
 |-  ( ph -> 9 e. RR )
70 9pos 
 |-  0 < 9
71 70 a1i 
 |-  ( ph -> 0 < 9 )
72 47 54 3lexlogpow5ineq4 
 |-  ( ph -> 9 < ( ( 2 logb N ) ^ 5 ) )
73 64 ceilged 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
74 69 64 66 72 73 ltletrd 
 |-  ( ph -> 9 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
75 74 46 breqtrrd 
 |-  ( ph -> 9 < B )
76 48 69 67 71 75 lttrd 
 |-  ( ph -> 0 < B )
77 43 45 67 76 60 relogbcld 
 |-  ( ph -> ( 2 logb B ) e. RR )
78 77 flcld 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. ZZ )
79 43 recnd 
 |-  ( ph -> 2 e. CC )
80 48 45 gtned 
 |-  ( ph -> 2 =/= 0 )
81 logb1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 1 ) = 0 )
82 79 80 60 81 syl3anc 
 |-  ( ph -> ( 2 logb 1 ) = 0 )
83 82 eqcomd 
 |-  ( ph -> 0 = ( 2 logb 1 ) )
84 2z 
 |-  2 e. ZZ
85 84 a1i 
 |-  ( ph -> 2 e. ZZ )
86 43 leidd 
 |-  ( ph -> 2 <_ 2 )
87 0lt1 
 |-  0 < 1
88 87 a1i 
 |-  ( ph -> 0 < 1 )
89 1lt9 
 |-  1 < 9
90 89 a1i 
 |-  ( ph -> 1 < 9 )
91 56 69 90 ltled 
 |-  ( ph -> 1 <_ 9 )
92 69 67 75 ltled 
 |-  ( ph -> 9 <_ B )
93 56 69 67 91 92 letrd 
 |-  ( ph -> 1 <_ B )
94 85 86 56 88 67 76 93 logblebd 
 |-  ( ph -> ( 2 logb 1 ) <_ ( 2 logb B ) )
95 83 94 eqbrtrd 
 |-  ( ph -> 0 <_ ( 2 logb B ) )
96 0zd 
 |-  ( ph -> 0 e. ZZ )
97 flge 
 |-  ( ( ( 2 logb B ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( 2 logb B ) <-> 0 <_ ( |_ ` ( 2 logb B ) ) ) )
98 77 96 97 syl2anc 
 |-  ( ph -> ( 0 <_ ( 2 logb B ) <-> 0 <_ ( |_ ` ( 2 logb B ) ) ) )
99 95 98 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( 2 logb B ) ) )
100 78 99 jca 
 |-  ( ph -> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) )
101 elnn0z 
 |-  ( ( |_ ` ( 2 logb B ) ) e. NN0 <-> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) )
102 100 101 sylibr 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. NN0 )
103 41 102 zexpcld 
 |-  ( ph -> ( N ^ ( |_ ` ( 2 logb B ) ) ) e. ZZ )
104 fzfid 
 |-  ( ph -> ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) e. Fin )
105 41 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> N e. ZZ )
106 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> k e. NN )
107 106 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN )
108 107 nnnn0d 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN0 )
109 105 108 zexpcld 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ k ) e. ZZ )
110 1zzd 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 e. ZZ )
111 109 110 zsubcld 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( N ^ k ) - 1 ) e. ZZ )
112 104 111 fprodzcl 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) e. ZZ )
113 dvdsmultr1 
 |-  ( ( R e. ZZ /\ ( N ^ ( |_ ` ( 2 logb B ) ) ) e. ZZ /\ prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) e. ZZ ) -> ( R || ( N ^ ( |_ ` ( 2 logb B ) ) ) -> R || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) ) )
114 39 103 112 113 syl3anc 
 |-  ( ph -> ( R || ( N ^ ( |_ ` ( 2 logb B ) ) ) -> R || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) ) )
115 114 imp 
 |-  ( ( ph /\ R || ( N ^ ( |_ ` ( 2 logb B ) ) ) ) -> R || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) )
116 2 a1i 
 |-  ( ph -> A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) )
117 116 breq2d 
 |-  ( ph -> ( R || A <-> R || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) ) )
118 117 adantr 
 |-  ( ( ph /\ R || ( N ^ ( |_ ` ( 2 logb B ) ) ) ) -> ( R || A <-> R || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) ) )
119 115 118 mpbird 
 |-  ( ( ph /\ R || ( N ^ ( |_ ` ( 2 logb B ) ) ) ) -> R || A )
120 119 ex 
 |-  ( ph -> ( R || ( N ^ ( |_ ` ( 2 logb B ) ) ) -> R || A ) )
121 120 con3d 
 |-  ( ph -> ( -. R || A -> -. R || ( N ^ ( |_ ` ( 2 logb B ) ) ) ) )
122 36 121 mpd 
 |-  ( ph -> -. R || ( N ^ ( |_ ` ( 2 logb B ) ) ) )
123 122 adantr 
 |-  ( ( ph /\ A. p e. Prime ( p || R -> p || N ) ) -> -. R || ( N ^ ( |_ ` ( 2 logb B ) ) ) )
124 11 123 pm2.65da 
 |-  ( ph -> -. A. p e. Prime ( p || R -> p || N ) )
125 ianor 
 |-  ( -. ( p || R /\ -. p || N ) <-> ( -. p || R \/ -. -. p || N ) )
126 notnotb 
 |-  ( p || N <-> -. -. p || N )
127 126 orbi2i 
 |-  ( ( -. p || R \/ p || N ) <-> ( -. p || R \/ -. -. p || N ) )
128 127 bicomi 
 |-  ( ( -. p || R \/ -. -. p || N ) <-> ( -. p || R \/ p || N ) )
129 125 128 bitri 
 |-  ( -. ( p || R /\ -. p || N ) <-> ( -. p || R \/ p || N ) )
130 df-or 
 |-  ( ( -. p || R \/ p || N ) <-> ( -. -. p || R -> p || N ) )
131 129 130 bitri 
 |-  ( -. ( p || R /\ -. p || N ) <-> ( -. -. p || R -> p || N ) )
132 notnotb 
 |-  ( p || R <-> -. -. p || R )
133 132 imbi1i 
 |-  ( ( p || R -> p || N ) <-> ( -. -. p || R -> p || N ) )
134 133 bicomi 
 |-  ( ( -. -. p || R -> p || N ) <-> ( p || R -> p || N ) )
135 131 134 bitri 
 |-  ( -. ( p || R /\ -. p || N ) <-> ( p || R -> p || N ) )
136 135 ralbii 
 |-  ( A. p e. Prime -. ( p || R /\ -. p || N ) <-> A. p e. Prime ( p || R -> p || N ) )
137 136 notbii 
 |-  ( -. A. p e. Prime -. ( p || R /\ -. p || N ) <-> -. A. p e. Prime ( p || R -> p || N ) )
138 124 137 sylibr 
 |-  ( ph -> -. A. p e. Prime -. ( p || R /\ -. p || N ) )
139 ralnex 
 |-  ( A. p e. Prime -. ( p || R /\ -. p || N ) <-> -. E. p e. Prime ( p || R /\ -. p || N ) )
140 139 con2bii 
 |-  ( E. p e. Prime ( p || R /\ -. p || N ) <-> -. A. p e. Prime -. ( p || R /\ -. p || N ) )
141 140 bicomi 
 |-  ( -. A. p e. Prime -. ( p || R /\ -. p || N ) <-> E. p e. Prime ( p || R /\ -. p || N ) )
142 138 141 sylib 
 |-  ( ph -> E. p e. Prime ( p || R /\ -. p || N ) )