Metamath Proof Explorer

Theorem aks4d1p3

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

Ref Expression
Hypotheses aks4d1p3.1 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks4d1p3.2 
|- A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
aks4d1p3.3 
|- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
Assertion aks4d1p3 
|- ( ph -> E. r e. ( 1 ... B ) -. r || A )

Proof

Step Hyp Ref Expression
1 aks4d1p3.1 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
2 aks4d1p3.2 
 |-  A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
3 aks4d1p3.3 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
4 1 2 3 aks4d1p1 
 |-  ( ph -> A < ( 2 ^ B ) )
5 4 adantr 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> A < ( 2 ^ B ) )
6 2re 
 |-  2 e. RR
7 6 a1i 
 |-  ( ph -> 2 e. RR )
8 3 a1i 
 |-  ( ph -> B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
9 2pos 
 |-  0 < 2
10 9 a1i 
 |-  ( ph -> 0 < 2 )
11 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
12 1 11 syl 
 |-  ( ph -> N e. ZZ )
13 12 zred 
 |-  ( ph -> N e. RR )
14 0red 
 |-  ( ph -> 0 e. RR )
15 3re 
 |-  3 e. RR
16 15 a1i 
 |-  ( ph -> 3 e. RR )
17 3pos 
 |-  0 < 3
18 17 a1i 
 |-  ( ph -> 0 < 3 )
19 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
20 1 19 syl 
 |-  ( ph -> 3 <_ N )
21 14 16 13 18 20 ltletrd 
 |-  ( ph -> 0 < N )
22 1red 
 |-  ( ph -> 1 e. RR )
23 1lt2 
 |-  1 < 2
24 23 a1i 
 |-  ( ph -> 1 < 2 )
25 22 24 ltned 
 |-  ( ph -> 1 =/= 2 )
26 25 necomd 
 |-  ( ph -> 2 =/= 1 )
27 7 10 13 21 26 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
28 5nn0 
 |-  5 e. NN0
29 28 a1i 
 |-  ( ph -> 5 e. NN0 )
30 27 29 reexpcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) e. RR )
31 ceilcl 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
32 30 31 syl 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
33 8 32 eqeltrd 
 |-  ( ph -> B e. ZZ )
34 32 zred 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. RR )
35 8 34 eqeltrd 
 |-  ( ph -> B e. RR )
36 7re 
 |-  7 e. RR
37 36 a1i 
 |-  ( ph -> 7 e. RR )
38 7pos 
 |-  0 < 7
39 38 a1i 
 |-  ( ph -> 0 < 7 )
40 13 20 3lexlogpow5ineq3 
 |-  ( ph -> 7 < ( ( 2 logb N ) ^ 5 ) )
41 14 37 30 39 40 lttrd 
 |-  ( ph -> 0 < ( ( 2 logb N ) ^ 5 ) )
42 ceilge 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
43 30 42 syl 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
44 14 30 34 41 43 ltletrd 
 |-  ( ph -> 0 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
45 44 8 breqtrrd 
 |-  ( ph -> 0 < B )
46 14 35 45 ltled 
 |-  ( ph -> 0 <_ B )
47 33 46 jca 
 |-  ( ph -> ( B e. ZZ /\ 0 <_ B ) )
48 elnn0z 
 |-  ( B e. NN0 <-> ( B e. ZZ /\ 0 <_ B ) )
49 47 48 sylibr 
 |-  ( ph -> B e. NN0 )
50 7 49 reexpcld 
 |-  ( ph -> ( 2 ^ B ) e. RR )
51 50 adantr 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( 2 ^ B ) e. RR )
52 elfznn 
 |-  ( q e. ( 1 ... B ) -> q e. NN )
53 52 adantl 
 |-  ( ( ph /\ q e. ( 1 ... B ) ) -> q e. NN )
54 53 nnzd 
 |-  ( ( ph /\ q e. ( 1 ... B ) ) -> q e. ZZ )
55 54 ex 
 |-  ( ph -> ( q e. ( 1 ... B ) -> q e. ZZ ) )
56 55 ssrdv 
 |-  ( ph -> ( 1 ... B ) C_ ZZ )
57 fzfid 
 |-  ( ph -> ( 1 ... B ) e. Fin )
58 lcmfcl 
 |-  ( ( ( 1 ... B ) C_ ZZ /\ ( 1 ... B ) e. Fin ) -> ( _lcm ` ( 1 ... B ) ) e. NN0 )
59 56 57 58 syl2anc 
 |-  ( ph -> ( _lcm ` ( 1 ... B ) ) e. NN0 )
60 59 nn0red 
 |-  ( ph -> ( _lcm ` ( 1 ... B ) ) e. RR )
61 60 adantr 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( _lcm ` ( 1 ... B ) ) e. RR )
62 2 a1i 
 |-  ( ph -> A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) )
63 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
64 12 21 63 sylanbrc 
 |-  ( ph -> N e. NN )
65 7 10 35 45 26 relogbcld 
 |-  ( ph -> ( 2 logb B ) e. RR )
66 65 flcld 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. ZZ )
67 7 10 7 10 26 relogbcld 
 |-  ( ph -> ( 2 logb 2 ) e. RR )
68 0le1 
 |-  0 <_ 1
69 68 a1i 
 |-  ( ph -> 0 <_ 1 )
70 7 recnd 
 |-  ( ph -> 2 e. CC )
71 14 10 gtned 
 |-  ( ph -> 2 =/= 0 )
72 logbid1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 2 ) = 1 )
73 70 71 26 72 syl3anc 
 |-  ( ph -> ( 2 logb 2 ) = 1 )
74 73 eqcomd 
 |-  ( ph -> 1 = ( 2 logb 2 ) )
75 69 74 breqtrd 
 |-  ( ph -> 0 <_ ( 2 logb 2 ) )
76 2z 
 |-  2 e. ZZ
77 76 a1i 
 |-  ( ph -> 2 e. ZZ )
78 7 leidd 
 |-  ( ph -> 2 <_ 2 )
79 2lt7 
 |-  2 < 7
80 79 a1i 
 |-  ( ph -> 2 < 7 )
81 7 37 80 ltled 
 |-  ( ph -> 2 <_ 7 )
82 37 30 34 40 43 ltletrd 
 |-  ( ph -> 7 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
83 82 8 breqtrrd 
 |-  ( ph -> 7 < B )
84 37 35 83 ltled 
 |-  ( ph -> 7 <_ B )
85 7 37 35 81 84 letrd 
 |-  ( ph -> 2 <_ B )
86 77 78 7 10 35 45 85 logblebd 
 |-  ( ph -> ( 2 logb 2 ) <_ ( 2 logb B ) )
87 14 67 65 75 86 letrd 
 |-  ( ph -> 0 <_ ( 2 logb B ) )
88 0zd 
 |-  ( ph -> 0 e. ZZ )
89 flge 
 |-  ( ( ( 2 logb B ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( 2 logb B ) <-> 0 <_ ( |_ ` ( 2 logb B ) ) ) )
90 65 88 89 syl2anc 
 |-  ( ph -> ( 0 <_ ( 2 logb B ) <-> 0 <_ ( |_ ` ( 2 logb B ) ) ) )
91 87 90 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( 2 logb B ) ) )
92 66 91 jca 
 |-  ( ph -> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) )
93 elnn0z 
 |-  ( ( |_ ` ( 2 logb B ) ) e. NN0 <-> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) )
94 92 93 sylibr 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. NN0 )
95 64 94 nnexpcld 
 |-  ( ph -> ( N ^ ( |_ ` ( 2 logb B ) ) ) e. NN )
96 fzfid 
 |-  ( ph -> ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) e. Fin )
97 12 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> N e. ZZ )
98 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> k e. NN )
99 98 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN )
100 99 nnnn0d 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN0 )
101 zexpcl 
 |-  ( ( N e. ZZ /\ k e. NN0 ) -> ( N ^ k ) e. ZZ )
102 97 100 101 syl2anc 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ k ) e. ZZ )
103 1zzd 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 e. ZZ )
104 102 103 zsubcld 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( N ^ k ) - 1 ) e. ZZ )
105 1cnd 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 e. CC )
106 105 addridd 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( 1 + 0 ) = 1 )
107 22 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 e. RR )
108 1nn0 
 |-  1 e. NN0
109 108 a1i 
 |-  ( ph -> 1 e. NN0 )
110 13 109 reexpcld 
 |-  ( ph -> ( N ^ 1 ) e. RR )
111 110 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ 1 ) e. RR )
112 102 zred 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ k ) e. RR )
113 1lt3 
 |-  1 < 3
114 113 a1i 
 |-  ( ph -> 1 < 3 )
115 22 16 13 114 20 ltletrd 
 |-  ( ph -> 1 < N )
116 13 recnd 
 |-  ( ph -> N e. CC )
117 116 exp1d 
 |-  ( ph -> ( N ^ 1 ) = N )
118 117 eqcomd 
 |-  ( ph -> N = ( N ^ 1 ) )
119 115 118 breqtrd 
 |-  ( ph -> 1 < ( N ^ 1 ) )
120 119 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 < ( N ^ 1 ) )
121 13 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> N e. RR )
122 64 nnge1d 
 |-  ( ph -> 1 <_ N )
123 122 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 <_ N )
124 elfzuz 
 |-  ( k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> k e. ( ZZ>= ` 1 ) )
125 124 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. ( ZZ>= ` 1 ) )
126 121 123 125 leexp2ad 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ 1 ) <_ ( N ^ k ) )
127 107 111 112 120 126 ltletrd 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 < ( N ^ k ) )
128 106 127 eqbrtrd 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( 1 + 0 ) < ( N ^ k ) )
129 14 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 0 e. RR )
130 107 129 112 ltaddsub2d 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( 1 + 0 ) < ( N ^ k ) <-> 0 < ( ( N ^ k ) - 1 ) ) )
131 128 130 mpbid 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 0 < ( ( N ^ k ) - 1 ) )
132 104 131 jca 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( ( N ^ k ) - 1 ) e. ZZ /\ 0 < ( ( N ^ k ) - 1 ) ) )
133 elnnz 
 |-  ( ( ( N ^ k ) - 1 ) e. NN <-> ( ( ( N ^ k ) - 1 ) e. ZZ /\ 0 < ( ( N ^ k ) - 1 ) ) )
134 132 133 sylibr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( N ^ k ) - 1 ) e. NN )
135 96 134 fprodnncl 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) e. NN )
136 95 135 nnmulcld 
 |-  ( ph -> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) e. NN )
137 62 136 eqeltrd 
 |-  ( ph -> A e. NN )
138 137 nnred 
 |-  ( ph -> A e. RR )
139 138 adantr 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> A e. RR )
140 1 2 3 aks4d1p2 
 |-  ( ph -> ( 2 ^ B ) <_ ( _lcm ` ( 1 ... B ) ) )
141 140 adantr 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( 2 ^ B ) <_ ( _lcm ` ( 1 ... B ) ) )
142 137 nnzd 
 |-  ( ph -> A e. ZZ )
143 142 adantr 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> A e. ZZ )
144 56 adantr 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( 1 ... B ) C_ ZZ )
145 fzfid 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( 1 ... B ) e. Fin )
146 lcmfdvdsb 
 |-  ( ( A e. ZZ /\ ( 1 ... B ) C_ ZZ /\ ( 1 ... B ) e. Fin ) -> ( A. r e. ( 1 ... B ) r || A <-> ( _lcm ` ( 1 ... B ) ) || A ) )
147 143 144 145 146 syl3anc 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( A. r e. ( 1 ... B ) r || A <-> ( _lcm ` ( 1 ... B ) ) || A ) )
148 147 biimpd 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( A. r e. ( 1 ... B ) r || A -> ( _lcm ` ( 1 ... B ) ) || A ) )
149 148 syldbl2 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( _lcm ` ( 1 ... B ) ) || A )
150 59 nn0zd 
 |-  ( ph -> ( _lcm ` ( 1 ... B ) ) e. ZZ )
151 150 adantr 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( _lcm ` ( 1 ... B ) ) e. ZZ )
152 137 adantr 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> A e. NN )
153 dvdsle 
 |-  ( ( ( _lcm ` ( 1 ... B ) ) e. ZZ /\ A e. NN ) -> ( ( _lcm ` ( 1 ... B ) ) || A -> ( _lcm ` ( 1 ... B ) ) <_ A ) )
154 151 152 153 syl2anc 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( ( _lcm ` ( 1 ... B ) ) || A -> ( _lcm ` ( 1 ... B ) ) <_ A ) )
155 149 154 mpd 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( _lcm ` ( 1 ... B ) ) <_ A )
156 51 61 139 141 155 letrd 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( 2 ^ B ) <_ A )
157 51 139 lenltd 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> ( ( 2 ^ B ) <_ A <-> -. A < ( 2 ^ B ) ) )
158 156 157 mpbid 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> -. A < ( 2 ^ B ) )
159 5 158 pm2.21dd 
 |-  ( ( ph /\ A. r e. ( 1 ... B ) r || A ) -> -. A. r e. ( 1 ... B ) r || A )
160 simpr 
 |-  ( ( ph /\ -. A. r e. ( 1 ... B ) r || A ) -> -. A. r e. ( 1 ... B ) r || A )
161 159 160 pm2.61dan 
 |-  ( ph -> -. A. r e. ( 1 ... B ) r || A )
162 rexnal 
 |-  ( E. r e. ( 1 ... B ) -. r || A <-> -. A. r e. ( 1 ... B ) r || A )
163 161 162 sylibr 
 |-  ( ph -> E. r e. ( 1 ... B ) -. r || A )