Metamath Proof Explorer

Theorem aks4d1p4

Description: There exists a small enough number such that it does not divide A . (Contributed by metakunt, 28-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 aks4d1p4.1 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
2 aks4d1p4.2 
 |-  A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
3 aks4d1p4.3 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
4 aks4d1p4.4 
 |-  R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < )
5 4 a1i 
 |-  ( ph -> R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) )
6 ltso 
 |-  < Or RR
7 6 a1i 
 |-  ( ph -> < Or RR )
8 fzfid 
 |-  ( ph -> ( 1 ... B ) e. Fin )
9 ssrab2 
 |-  { r e. ( 1 ... B ) | -. r || A } C_ ( 1 ... B )
10 9 a1i 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } C_ ( 1 ... B ) )
11 8 10 ssfid 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } e. Fin )
12 1 2 3 aks4d1p3 
 |-  ( ph -> E. r e. ( 1 ... B ) -. r || A )
13 rabn0 
 |-  ( { r e. ( 1 ... B ) | -. r || A } =/= (/) <-> E. r e. ( 1 ... B ) -. r || A )
14 12 13 sylibr 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } =/= (/) )
15 elfznn 
 |-  ( o e. ( 1 ... B ) -> o e. NN )
16 15 adantl 
 |-  ( ( ph /\ o e. ( 1 ... B ) ) -> o e. NN )
17 16 nnred 
 |-  ( ( ph /\ o e. ( 1 ... B ) ) -> o e. RR )
18 17 ex 
 |-  ( ph -> ( o e. ( 1 ... B ) -> o e. RR ) )
19 18 ssrdv 
 |-  ( ph -> ( 1 ... B ) C_ RR )
20 10 19 sstrd 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
21 11 14 20 3jca 
 |-  ( ph -> ( { r e. ( 1 ... B ) | -. r || A } e. Fin /\ { r e. ( 1 ... B ) | -. r || A } =/= (/) /\ { r e. ( 1 ... B ) | -. r || A } C_ RR ) )
22 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 } )
23 7 21 22 syl2anc 
 |-  ( ph -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) e. { r e. ( 1 ... B ) | -. r || A } )
24 5 23 eqeltrd 
 |-  ( ph -> R e. { r e. ( 1 ... B ) | -. r || A } )
25 breq1 
 |-  ( r = R -> ( r || A <-> R || A ) )
26 25 notbid 
 |-  ( r = R -> ( -. r || A <-> -. R || A ) )
27 26 elrab 
 |-  ( R e. { r e. ( 1 ... B ) | -. r || A } <-> ( R e. ( 1 ... B ) /\ -. R || A ) )
28 24 27 sylib 
 |-  ( ph -> ( R e. ( 1 ... B ) /\ -. R || A ) )