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