Metamath Proof Explorer

Theorem aks4d1p9

Description: Show that the order is bound by the squared binary logarithm. (Contributed by metakunt, 14-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 aks4d1p9.1 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
2 aks4d1p9.2 
 |-  A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
3 aks4d1p9.3 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
4 aks4d1p9.4 
 |-  R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < )
5 2re 
 |-  2 e. RR
6 5 a1i 
 |-  ( ph -> 2 e. RR )
7 2pos 
 |-  0 < 2
8 7 a1i 
 |-  ( ph -> 0 < 2 )
9 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
10 1 9 syl 
 |-  ( ph -> N e. ZZ )
11 10 zred 
 |-  ( ph -> N e. RR )
12 0red 
 |-  ( ph -> 0 e. RR )
13 3re 
 |-  3 e. RR
14 13 a1i 
 |-  ( ph -> 3 e. RR )
15 3pos 
 |-  0 < 3
16 15 a1i 
 |-  ( ph -> 0 < 3 )
17 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
18 1 17 syl 
 |-  ( ph -> 3 <_ N )
19 12 14 11 16 18 ltletrd 
 |-  ( ph -> 0 < N )
20 1red 
 |-  ( ph -> 1 e. RR )
21 1lt2 
 |-  1 < 2
22 21 a1i 
 |-  ( ph -> 1 < 2 )
23 20 22 ltned 
 |-  ( ph -> 1 =/= 2 )
24 23 necomd 
 |-  ( ph -> 2 =/= 1 )
25 6 8 11 19 24 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
26 25 resqcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) e. RR )
27 1 2 3 4 aks4d1p4 
 |-  ( ph -> ( R e. ( 1 ... B ) /\ -. R || A ) )
28 27 simpld 
 |-  ( ph -> R e. ( 1 ... B ) )
29 elfznn 
 |-  ( R e. ( 1 ... B ) -> R e. NN )
30 28 29 syl 
 |-  ( ph -> R e. NN )
31 1 2 3 4 aks4d1p8 
 |-  ( ph -> ( N gcd R ) = 1 )
32 30 10 31 3jca 
 |-  ( ph -> ( R e. NN /\ N e. ZZ /\ ( N gcd R ) = 1 ) )
33 odzcl 
 |-  ( ( R e. NN /\ N e. ZZ /\ ( N gcd R ) = 1 ) -> ( ( odZ ` R ) ` N ) e. NN )
34 32 33 syl 
 |-  ( ph -> ( ( odZ ` R ) ` N ) e. NN )
35 34 nnzd 
 |-  ( ph -> ( ( odZ ` R ) ` N ) e. ZZ )
36 flge 
 |-  ( ( ( ( 2 logb N ) ^ 2 ) e. RR /\ ( ( odZ ` R ) ` N ) e. ZZ ) -> ( ( ( odZ ` R ) ` N ) <_ ( ( 2 logb N ) ^ 2 ) <-> ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) )
37 26 35 36 syl2anc 
 |-  ( ph -> ( ( ( odZ ` R ) ` N ) <_ ( ( 2 logb N ) ^ 2 ) <-> ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) )
38 37 biimpd 
 |-  ( ph -> ( ( ( odZ ` R ) ` N ) <_ ( ( 2 logb N ) ^ 2 ) -> ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) )
39 38 imp 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( ( 2 logb N ) ^ 2 ) ) -> ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) )
40 30 nnzd 
 |-  ( ph -> R e. ZZ )
41 40 adantr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> R e. ZZ )
42 10 adantr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> N e. ZZ )
43 34 nnnn0d 
 |-  ( ph -> ( ( odZ ` R ) ` N ) e. NN0 )
44 43 adantr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( ( odZ ` R ) ` N ) e. NN0 )
45 42 44 zexpcld 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( N ^ ( ( odZ ` R ) ` N ) ) e. ZZ )
46 1zzd 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> 1 e. ZZ )
47 45 46 zsubcld 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( ( N ^ ( ( odZ ` R ) ` N ) ) - 1 ) e. ZZ )
48 1 3 aks4d1lem1 
 |-  ( ph -> ( B e. NN /\ 9 < B ) )
49 48 simpld 
 |-  ( ph -> B e. NN )
50 49 nnred 
 |-  ( ph -> B e. RR )
51 49 nngt0d 
 |-  ( ph -> 0 < B )
52 6 8 50 51 24 relogbcld 
 |-  ( ph -> ( 2 logb B ) e. RR )
53 52 flcld 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. ZZ )
54 2cnd 
 |-  ( ph -> 2 e. CC )
55 12 8 gtned 
 |-  ( ph -> 2 =/= 0 )
56 54 55 24 3jca 
 |-  ( ph -> ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) )
57 logb1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 1 ) = 0 )
58 56 57 syl 
 |-  ( ph -> ( 2 logb 1 ) = 0 )
59 2z 
 |-  2 e. ZZ
60 59 a1i 
 |-  ( ph -> 2 e. ZZ )
61 6 leidd 
 |-  ( ph -> 2 <_ 2 )
62 0lt1 
 |-  0 < 1
63 62 a1i 
 |-  ( ph -> 0 < 1 )
64 49 nnge1d 
 |-  ( ph -> 1 <_ B )
65 60 61 20 63 50 51 64 logblebd 
 |-  ( ph -> ( 2 logb 1 ) <_ ( 2 logb B ) )
66 58 65 eqbrtrrd 
 |-  ( ph -> 0 <_ ( 2 logb B ) )
67 0zd 
 |-  ( ph -> 0 e. ZZ )
68 flge 
 |-  ( ( ( 2 logb B ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( 2 logb B ) <-> 0 <_ ( |_ ` ( 2 logb B ) ) ) )
69 52 67 68 syl2anc 
 |-  ( ph -> ( 0 <_ ( 2 logb B ) <-> 0 <_ ( |_ ` ( 2 logb B ) ) ) )
70 66 69 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( 2 logb B ) ) )
71 53 70 jca 
 |-  ( ph -> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) )
72 elnn0z 
 |-  ( ( |_ ` ( 2 logb B ) ) e. NN0 <-> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) )
73 71 72 sylibr 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. NN0 )
74 10 73 zexpcld 
 |-  ( ph -> ( N ^ ( |_ ` ( 2 logb B ) ) ) e. ZZ )
75 fzfid 
 |-  ( ph -> ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) e. Fin )
76 10 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> N e. ZZ )
77 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> k e. NN )
78 77 nnnn0d 
 |-  ( k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> k e. NN0 )
79 78 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN0 )
80 76 79 zexpcld 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ k ) e. ZZ )
81 1zzd 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 e. ZZ )
82 80 81 zsubcld 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( N ^ k ) - 1 ) e. ZZ )
83 75 82 fprodzcl 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) e. ZZ )
84 74 83 zmulcld 
 |-  ( ph -> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) e. ZZ )
85 2 a1i 
 |-  ( ph -> A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) )
86 85 eleq1d 
 |-  ( ph -> ( A e. ZZ <-> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) e. ZZ ) )
87 84 86 mpbird 
 |-  ( ph -> A e. ZZ )
88 87 adantr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> A e. ZZ )
89 iddvds 
 |-  ( ( ( odZ ` R ) ` N ) e. ZZ -> ( ( odZ ` R ) ` N ) || ( ( odZ ` R ) ` N ) )
90 35 89 syl 
 |-  ( ph -> ( ( odZ ` R ) ` N ) || ( ( odZ ` R ) ` N ) )
91 odzdvds 
 |-  ( ( ( R e. NN /\ N e. ZZ /\ ( N gcd R ) = 1 ) /\ ( ( odZ ` R ) ` N ) e. NN0 ) -> ( R || ( ( N ^ ( ( odZ ` R ) ` N ) ) - 1 ) <-> ( ( odZ ` R ) ` N ) || ( ( odZ ` R ) ` N ) ) )
92 32 43 91 syl2anc 
 |-  ( ph -> ( R || ( ( N ^ ( ( odZ ` R ) ` N ) ) - 1 ) <-> ( ( odZ ` R ) ` N ) || ( ( odZ ` R ) ` N ) ) )
93 90 92 mpbird 
 |-  ( ph -> R || ( ( N ^ ( ( odZ ` R ) ` N ) ) - 1 ) )
94 93 adantr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> R || ( ( N ^ ( ( odZ ` R ) ` N ) ) - 1 ) )
95 73 adantr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( |_ ` ( 2 logb B ) ) e. NN0 )
96 42 95 zexpcld 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( N ^ ( |_ ` ( 2 logb B ) ) ) e. ZZ )
97 fzfid 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) e. Fin )
98 42 adantr 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> N e. ZZ )
99 77 adantl 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN )
100 99 nnnn0d 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN0 )
101 98 100 zexpcld 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ k ) e. ZZ )
102 1zzd 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 e. ZZ )
103 101 102 zsubcld 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( N ^ k ) - 1 ) e. ZZ )
104 97 103 fprodzcl 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) e. ZZ )
105 fveq2 
 |-  ( z = ( ( odZ ` R ) ` N ) -> ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` z ) = ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` ( ( odZ ` R ) ` N ) ) )
106 105 breq1d 
 |-  ( z = ( ( odZ ` R ) ` N ) -> ( ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` z ) || prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` k ) <-> ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` ( ( odZ ` R ) ` N ) ) || prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` k ) ) )
107 ssidd 
 |-  ( ph -> ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) C_ ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) )
108 10 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> N e. ZZ )
109 elfznn 
 |-  ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> x e. NN )
110 109 adantl 
 |-  ( ( ph /\ x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> x e. NN )
111 110 nnnn0d 
 |-  ( ( ph /\ x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> x e. NN0 )
112 108 111 zexpcld 
 |-  ( ( ph /\ x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ x ) e. ZZ )
113 1zzd 
 |-  ( ( ph /\ x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 e. ZZ )
114 112 113 zsubcld 
 |-  ( ( ph /\ x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( N ^ x ) - 1 ) e. ZZ )
115 114 fmpttd 
 |-  ( ph -> ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) : ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) --> ZZ )
116 75 107 115 fprodfvdvdsd 
 |-  ( ph -> A. z e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` z ) || prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` k ) )
117 116 adantr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> A. z e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` z ) || prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` k ) )
118 25 adantr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( 2 logb N ) e. RR )
119 118 resqcld 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( ( 2 logb N ) ^ 2 ) e. RR )
120 119 flcld 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. ZZ )
121 35 adantr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( ( odZ ` R ) ` N ) e. ZZ )
122 34 nnge1d 
 |-  ( ph -> 1 <_ ( ( odZ ` R ) ` N ) )
123 122 adantr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> 1 <_ ( ( odZ ` R ) ` N ) )
124 simpr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) )
125 46 120 121 123 124 elfzd 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( ( odZ ` R ) ` N ) e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) )
126 106 117 125 rspcdva 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` ( ( odZ ` R ) ` N ) ) || prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` k ) )
127 eqidd 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) = ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) )
128 simpr 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ x = ( ( odZ ` R ) ` N ) ) -> x = ( ( odZ ` R ) ` N ) )
129 128 oveq2d 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ x = ( ( odZ ` R ) ` N ) ) -> ( N ^ x ) = ( N ^ ( ( odZ ` R ) ` N ) ) )
130 129 oveq1d 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ x = ( ( odZ ` R ) ` N ) ) -> ( ( N ^ x ) - 1 ) = ( ( N ^ ( ( odZ ` R ) ` N ) ) - 1 ) )
131 127 130 125 47 fvmptd 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` ( ( odZ ` R ) ` N ) ) = ( ( N ^ ( ( odZ ` R ) ` N ) ) - 1 ) )
132 eqidd 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) = ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) )
133 simpr 
 |-  ( ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) /\ x = k ) -> x = k )
134 133 oveq2d 
 |-  ( ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) /\ x = k ) -> ( N ^ x ) = ( N ^ k ) )
135 134 oveq1d 
 |-  ( ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) /\ x = k ) -> ( ( N ^ x ) - 1 ) = ( ( N ^ k ) - 1 ) )
136 simpr 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) )
137 132 135 136 103 fvmptd 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` k ) = ( ( N ^ k ) - 1 ) )
138 137 prodeq2dv 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` k ) = prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
139 131 138 breq12d 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` ( ( odZ ` R ) ` N ) ) || prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( x e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) |-> ( ( N ^ x ) - 1 ) ) ` k ) <-> ( ( N ^ ( ( odZ ` R ) ` N ) ) - 1 ) || prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) )
140 126 139 mpbid 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( ( N ^ ( ( odZ ` R ) ` N ) ) - 1 ) || prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
141 47 96 104 140 dvdsmultr2d 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( ( N ^ ( ( odZ ` R ) ` N ) ) - 1 ) || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) )
142 2 a1i 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) )
143 141 142 breqtrrd 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> ( ( N ^ ( ( odZ ` R ) ` N ) ) - 1 ) || A )
144 41 47 88 94 143 dvdstrd 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> R || A )
145 144 ex 
 |-  ( ph -> ( ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) -> R || A ) )
146 145 adantr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( ( 2 logb N ) ^ 2 ) ) -> ( ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) -> R || A ) )
147 146 imp 
 |-  ( ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( ( 2 logb N ) ^ 2 ) ) /\ ( ( odZ ` R ) ` N ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> R || A )
148 39 147 mpdan 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( ( 2 logb N ) ^ 2 ) ) -> R || A )
149 27 simprd 
 |-  ( ph -> -. R || A )
150 149 adantr 
 |-  ( ( ph /\ ( ( odZ ` R ) ` N ) <_ ( ( 2 logb N ) ^ 2 ) ) -> -. R || A )
151 148 150 pm2.65da 
 |-  ( ph -> -. ( ( odZ ` R ) ` N ) <_ ( ( 2 logb N ) ^ 2 ) )
152 34 nnred 
 |-  ( ph -> ( ( odZ ` R ) ` N ) e. RR )
153 26 152 ltnled 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) <-> -. ( ( odZ ` R ) ` N ) <_ ( ( 2 logb N ) ^ 2 ) ) )
154 151 153 mpbird 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )