Metamath Proof Explorer

Theorem aks4d1p7d1

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

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

Proof

Step Hyp Ref Expression
1 aks4d1p7d1.1 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
2 aks4d1p7d1.2 
 |-  A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
3 aks4d1p7d1.3 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
4 aks4d1p7d1.4 
 |-  R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < )
5 aks4d1p7d1.5 
 |-  ( ph -> A. p e. Prime ( p || R -> p || N ) )
6 simp2 
 |-  ( ( ph /\ p e. Prime /\ p || R ) -> p e. Prime )
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 3ad2ant1 
 |-  ( ( ph /\ p e. Prime /\ p || R ) -> R e. NN )
12 6 11 pccld 
 |-  ( ( ph /\ p e. Prime /\ p || R ) -> ( p pCnt R ) e. NN0 )
13 12 3expa 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( p pCnt R ) e. NN0 )
14 13 nn0red 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( p pCnt R ) e. RR )
15 2re 
 |-  2 e. RR
16 15 a1i 
 |-  ( ph -> 2 e. RR )
17 2pos 
 |-  0 < 2
18 17 a1i 
 |-  ( ph -> 0 < 2 )
19 3 a1i 
 |-  ( ph -> B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
20 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
21 1 20 syl 
 |-  ( ph -> N e. ZZ )
22 21 zred 
 |-  ( ph -> N e. RR )
23 0red 
 |-  ( ph -> 0 e. RR )
24 3re 
 |-  3 e. RR
25 24 a1i 
 |-  ( ph -> 3 e. RR )
26 3pos 
 |-  0 < 3
27 26 a1i 
 |-  ( ph -> 0 < 3 )
28 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
29 1 28 syl 
 |-  ( ph -> 3 <_ N )
30 23 25 22 27 29 ltletrd 
 |-  ( ph -> 0 < N )
31 1red 
 |-  ( ph -> 1 e. RR )
32 1lt2 
 |-  1 < 2
33 32 a1i 
 |-  ( ph -> 1 < 2 )
34 31 33 ltned 
 |-  ( ph -> 1 =/= 2 )
35 34 necomd 
 |-  ( ph -> 2 =/= 1 )
36 16 18 22 30 35 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
37 5nn0 
 |-  5 e. NN0
38 37 a1i 
 |-  ( ph -> 5 e. NN0 )
39 36 38 reexpcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) e. RR )
40 ceilcl 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
41 39 40 syl 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
42 41 zred 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. RR )
43 19 42 eqeltrd 
 |-  ( ph -> B e. RR )
44 9re 
 |-  9 e. RR
45 44 a1i 
 |-  ( ph -> 9 e. RR )
46 9pos 
 |-  0 < 9
47 46 a1i 
 |-  ( ph -> 0 < 9 )
48 22 29 3lexlogpow5ineq4 
 |-  ( ph -> 9 < ( ( 2 logb N ) ^ 5 ) )
49 23 45 39 47 48 lttrd 
 |-  ( ph -> 0 < ( ( 2 logb N ) ^ 5 ) )
50 ceilge 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
51 39 50 syl 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
52 23 39 42 49 51 ltletrd 
 |-  ( ph -> 0 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
53 52 19 breqtrrd 
 |-  ( ph -> 0 < B )
54 16 18 43 53 35 relogbcld 
 |-  ( ph -> ( 2 logb B ) e. RR )
55 54 flcld 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. ZZ )
56 55 zred 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. RR )
57 56 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( |_ ` ( 2 logb B ) ) e. RR )
58 simplr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> p e. Prime )
59 21 30 jca 
 |-  ( ph -> ( N e. ZZ /\ 0 < N ) )
60 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
61 59 60 sylibr 
 |-  ( ph -> N e. NN )
62 61 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> N e. NN )
63 1cnd 
 |-  ( ph -> 1 e. CC )
64 63 addid2d 
 |-  ( ph -> ( 0 + 1 ) = 1 )
65 16 recnd 
 |-  ( ph -> 2 e. CC )
66 23 18 gtned 
 |-  ( ph -> 2 =/= 0 )
67 logbid1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 2 ) = 1 )
68 65 66 35 67 syl3anc 
 |-  ( ph -> ( 2 logb 2 ) = 1 )
69 68 eqcomd 
 |-  ( ph -> 1 = ( 2 logb 2 ) )
70 64 69 eqtrd 
 |-  ( ph -> ( 0 + 1 ) = ( 2 logb 2 ) )
71 2z 
 |-  2 e. ZZ
72 71 a1i 
 |-  ( ph -> 2 e. ZZ )
73 16 leidd 
 |-  ( ph -> 2 <_ 2 )
74 2lt9 
 |-  2 < 9
75 74 a1i 
 |-  ( ph -> 2 < 9 )
76 16 45 75 ltled 
 |-  ( ph -> 2 <_ 9 )
77 45 39 42 48 51 ltletrd 
 |-  ( ph -> 9 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
78 77 19 breqtrrd 
 |-  ( ph -> 9 < B )
79 45 43 78 ltled 
 |-  ( ph -> 9 <_ B )
80 16 45 43 76 79 letrd 
 |-  ( ph -> 2 <_ B )
81 72 73 16 18 43 53 80 logblebd 
 |-  ( ph -> ( 2 logb 2 ) <_ ( 2 logb B ) )
82 70 81 eqbrtrd 
 |-  ( ph -> ( 0 + 1 ) <_ ( 2 logb B ) )
83 0zd 
 |-  ( ph -> 0 e. ZZ )
84 83 peano2zd 
 |-  ( ph -> ( 0 + 1 ) e. ZZ )
85 flge 
 |-  ( ( ( 2 logb B ) e. RR /\ ( 0 + 1 ) e. ZZ ) -> ( ( 0 + 1 ) <_ ( 2 logb B ) <-> ( 0 + 1 ) <_ ( |_ ` ( 2 logb B ) ) ) )
86 54 84 85 syl2anc 
 |-  ( ph -> ( ( 0 + 1 ) <_ ( 2 logb B ) <-> ( 0 + 1 ) <_ ( |_ ` ( 2 logb B ) ) ) )
87 82 86 mpbid 
 |-  ( ph -> ( 0 + 1 ) <_ ( |_ ` ( 2 logb B ) ) )
88 83 55 zltp1led 
 |-  ( ph -> ( 0 < ( |_ ` ( 2 logb B ) ) <-> ( 0 + 1 ) <_ ( |_ ` ( 2 logb B ) ) ) )
89 87 88 mpbird 
 |-  ( ph -> 0 < ( |_ ` ( 2 logb B ) ) )
90 55 89 jca 
 |-  ( ph -> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 < ( |_ ` ( 2 logb B ) ) ) )
91 elnnz 
 |-  ( ( |_ ` ( 2 logb B ) ) e. NN <-> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 < ( |_ ` ( 2 logb B ) ) ) )
92 90 91 sylibr 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. NN )
93 92 nnnn0d 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. NN0 )
94 93 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( |_ ` ( 2 logb B ) ) e. NN0 )
95 62 94 nnexpcld 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( N ^ ( |_ ` ( 2 logb B ) ) ) e. NN )
96 58 95 pccld 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) e. NN0 )
97 96 nn0red 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) e. RR )
98 1 3ad2ant1 
 |-  ( ( ph /\ p e. Prime /\ p || R ) -> N e. ( ZZ>= ` 3 ) )
99 simp3 
 |-  ( ( ph /\ p e. Prime /\ p || R ) -> p || R )
100 eqid 
 |-  ( p pCnt R ) = ( p pCnt R )
101 98 2 3 4 6 99 100 aks4d1p6 
 |-  ( ( ph /\ p e. Prime /\ p || R ) -> ( p pCnt R ) <_ ( |_ ` ( 2 logb B ) ) )
102 101 3expa 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( p pCnt R ) <_ ( |_ ` ( 2 logb B ) ) )
103 58 62 pccld 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( p pCnt N ) e. NN0 )
104 103 nn0red 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( p pCnt N ) e. RR )
105 23 56 89 ltled 
 |-  ( ph -> 0 <_ ( |_ ` ( 2 logb B ) ) )
106 105 adantr 
 |-  ( ( ph /\ p e. Prime ) -> 0 <_ ( |_ ` ( 2 logb B ) ) )
107 106 adantr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> 0 <_ ( |_ ` ( 2 logb B ) ) )
108 rsp 
 |-  ( A. p e. Prime ( p || R -> p || N ) -> ( p e. Prime -> ( p || R -> p || N ) ) )
109 5 108 syl 
 |-  ( ph -> ( p e. Prime -> ( p || R -> p || N ) ) )
110 109 imp 
 |-  ( ( ph /\ p e. Prime ) -> ( p || R -> p || N ) )
111 110 imp 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> p || N )
112 61 adantr 
 |-  ( ( ph /\ p e. Prime ) -> N e. NN )
113 112 adantr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> N e. NN )
114 pcelnn 
 |-  ( ( p e. Prime /\ N e. NN ) -> ( ( p pCnt N ) e. NN <-> p || N ) )
115 58 113 114 syl2anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( ( p pCnt N ) e. NN <-> p || N ) )
116 111 115 mpbird 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( p pCnt N ) e. NN )
117 nnge1 
 |-  ( ( p pCnt N ) e. NN -> 1 <_ ( p pCnt N ) )
118 116 117 syl 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> 1 <_ ( p pCnt N ) )
119 57 104 107 118 lemulge11d 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( |_ ` ( 2 logb B ) ) <_ ( ( |_ ` ( 2 logb B ) ) x. ( p pCnt N ) ) )
120 zq 
 |-  ( N e. ZZ -> N e. QQ )
121 21 120 syl 
 |-  ( ph -> N e. QQ )
122 61 nnne0d 
 |-  ( ph -> N =/= 0 )
123 121 122 jca 
 |-  ( ph -> ( N e. QQ /\ N =/= 0 ) )
124 123 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( N e. QQ /\ N =/= 0 ) )
125 124 adantr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( N e. QQ /\ N =/= 0 ) )
126 55 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( |_ ` ( 2 logb B ) ) e. ZZ )
127 126 adantr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( |_ ` ( 2 logb B ) ) e. ZZ )
128 pcexp 
 |-  ( ( p e. Prime /\ ( N e. QQ /\ N =/= 0 ) /\ ( |_ ` ( 2 logb B ) ) e. ZZ ) -> ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) = ( ( |_ ` ( 2 logb B ) ) x. ( p pCnt N ) ) )
129 58 125 127 128 syl3anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) = ( ( |_ ` ( 2 logb B ) ) x. ( p pCnt N ) ) )
130 119 129 breqtrrd 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( |_ ` ( 2 logb B ) ) <_ ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) )
131 14 57 97 102 130 letrd 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || R ) -> ( p pCnt R ) <_ ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) )
132 simpr 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p || R ) -> -. p || R )
133 simplr 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p || R ) -> p e. Prime )
134 10 adantr 
 |-  ( ( ph /\ p e. Prime ) -> R e. NN )
135 134 adantr 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p || R ) -> R e. NN )
136 pceq0 
 |-  ( ( p e. Prime /\ R e. NN ) -> ( ( p pCnt R ) = 0 <-> -. p || R ) )
137 133 135 136 syl2anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p || R ) -> ( ( p pCnt R ) = 0 <-> -. p || R ) )
138 132 137 mpbird 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p || R ) -> ( p pCnt R ) = 0 )
139 112 adantr 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p || R ) -> N e. NN )
140 93 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( |_ ` ( 2 logb B ) ) e. NN0 )
141 140 adantr 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p || R ) -> ( |_ ` ( 2 logb B ) ) e. NN0 )
142 139 141 nnexpcld 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p || R ) -> ( N ^ ( |_ ` ( 2 logb B ) ) ) e. NN )
143 133 142 pccld 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p || R ) -> ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) e. NN0 )
144 143 nn0ge0d 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p || R ) -> 0 <_ ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) )
145 138 144 eqbrtrd 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p || R ) -> ( p pCnt R ) <_ ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) )
146 131 145 pm2.61dan 
 |-  ( ( ph /\ p e. Prime ) -> ( p pCnt R ) <_ ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) )
147 146 ralrimiva 
 |-  ( ph -> A. p e. Prime ( p pCnt R ) <_ ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) )
148 8 elfzelzd 
 |-  ( ph -> R e. ZZ )
149 21 93 zexpcld 
 |-  ( ph -> ( N ^ ( |_ ` ( 2 logb B ) ) ) e. ZZ )
150 pc2dvds 
 |-  ( ( R e. ZZ /\ ( N ^ ( |_ ` ( 2 logb B ) ) ) e. ZZ ) -> ( R || ( N ^ ( |_ ` ( 2 logb B ) ) ) <-> A. p e. Prime ( p pCnt R ) <_ ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) ) )
151 148 149 150 syl2anc 
 |-  ( ph -> ( R || ( N ^ ( |_ ` ( 2 logb B ) ) ) <-> A. p e. Prime ( p pCnt R ) <_ ( p pCnt ( N ^ ( |_ ` ( 2 logb B ) ) ) ) ) )
152 147 151 mpbird 
 |-  ( ph -> R || ( N ^ ( |_ ` ( 2 logb B ) ) ) )