Metamath Proof Explorer

Theorem aks6d1c7lem1

Description: The last set of inequalities of Claim 7 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf . (Contributed by metakunt, 12-May-2025)

Ref Expression
Hypotheses aks6d1c7lem1.1 
|- ( ph -> P e. Prime )
aks6d1c7lem1.2 
|- ( ph -> R e. NN )
aks6d1c7lem1.3 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks6d1c7lem1.4 
|- ( ph -> P || N )
aks6d1c7lem1.5 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c7lem1.6 
|- E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
aks6d1c7lem1.7 
|- L = ( ZRHom ` ( Z/nZ ` R ) )
aks6d1c7lem1.8 
|- D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) )
aks6d1c7lem1.9 
|- A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
aks6d1c7lem1.10 
|- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
Assertion aks6d1c7lem1 
|- ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) < ( ( D + A ) _C ( D - 1 ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c7lem1.1 
 |-  ( ph -> P e. Prime )
2 aks6d1c7lem1.2 
 |-  ( ph -> R e. NN )
3 aks6d1c7lem1.3 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
4 aks6d1c7lem1.4 
 |-  ( ph -> P || N )
5 aks6d1c7lem1.5 
 |-  ( ph -> ( N gcd R ) = 1 )
6 aks6d1c7lem1.6 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
7 aks6d1c7lem1.7 
 |-  L = ( ZRHom ` ( Z/nZ ` R ) )
8 aks6d1c7lem1.8 
 |-  D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) )
9 aks6d1c7lem1.9 
 |-  A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
10 aks6d1c7lem1.10 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
11 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
12 3 11 syl 
 |-  ( ph -> N e. ZZ )
13 0red 
 |-  ( ph -> 0 e. RR )
14 3re 
 |-  3 e. RR
15 14 a1i 
 |-  ( ph -> 3 e. RR )
16 12 zred 
 |-  ( ph -> N e. RR )
17 3pos 
 |-  0 < 3
18 17 a1i 
 |-  ( ph -> 0 < 3 )
19 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
20 3 19 syl 
 |-  ( ph -> 3 <_ N )
21 13 15 16 18 20 ltletrd 
 |-  ( ph -> 0 < N )
22 12 21 jca 
 |-  ( ph -> ( N e. ZZ /\ 0 < N ) )
23 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
24 22 23 sylibr 
 |-  ( ph -> N e. NN )
25 24 nnred 
 |-  ( ph -> N e. RR )
26 8 a1i 
 |-  ( ph -> D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
27 eqid 
 |-  ( Z/nZ ` R ) = ( Z/nZ ` R )
28 24 1 4 2 5 6 7 27 hashscontpowcl 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )
29 26 28 eqeltrd 
 |-  ( ph -> D e. NN0 )
30 29 nn0red 
 |-  ( ph -> D e. RR )
31 29 nn0ge0d 
 |-  ( ph -> 0 <_ D )
32 30 31 resqrtcld 
 |-  ( ph -> ( sqrt ` D ) e. RR )
33 32 flcld 
 |-  ( ph -> ( |_ ` ( sqrt ` D ) ) e. ZZ )
34 30 31 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` D ) )
35 0zd 
 |-  ( ph -> 0 e. ZZ )
36 flge 
 |-  ( ( ( sqrt ` D ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( sqrt ` D ) <-> 0 <_ ( |_ ` ( sqrt ` D ) ) ) )
37 32 35 36 syl2anc 
 |-  ( ph -> ( 0 <_ ( sqrt ` D ) <-> 0 <_ ( |_ ` ( sqrt ` D ) ) ) )
38 34 37 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( sqrt ` D ) ) )
39 33 38 jca 
 |-  ( ph -> ( ( |_ ` ( sqrt ` D ) ) e. ZZ /\ 0 <_ ( |_ ` ( sqrt ` D ) ) ) )
40 elnn0z 
 |-  ( ( |_ ` ( sqrt ` D ) ) e. NN0 <-> ( ( |_ ` ( sqrt ` D ) ) e. ZZ /\ 0 <_ ( |_ ` ( sqrt ` D ) ) ) )
41 39 40 sylibr 
 |-  ( ph -> ( |_ ` ( sqrt ` D ) ) e. NN0 )
42 25 41 reexpcld 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) e. RR )
43 2re 
 |-  2 e. RR
44 43 a1i 
 |-  ( ph -> 2 e. RR )
45 2pos 
 |-  0 < 2
46 45 a1i 
 |-  ( ph -> 0 < 2 )
47 24 nngt0d 
 |-  ( ph -> 0 < N )
48 1ne2 
 |-  1 =/= 2
49 48 necomi 
 |-  2 =/= 1
50 49 a1i 
 |-  ( ph -> 2 =/= 1 )
51 44 46 25 47 50 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
52 26 30 eqeltrrd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR )
53 31 26 breqtrd 
 |-  ( ph -> 0 <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
54 52 53 resqrtcld 
 |-  ( ph -> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. RR )
55 51 54 remulcld 
 |-  ( ph -> ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. RR )
56 55 flcld 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. ZZ )
57 1red 
 |-  ( ph -> 1 e. RR )
58 0le1 
 |-  0 <_ 1
59 58 a1i 
 |-  ( ph -> 0 <_ 1 )
60 44 recnd 
 |-  ( ph -> 2 e. CC )
61 13 46 gtned 
 |-  ( ph -> 2 =/= 0 )
62 logbid1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 2 ) = 1 )
63 60 61 50 62 syl3anc 
 |-  ( ph -> ( 2 logb 2 ) = 1 )
64 63 eqcomd 
 |-  ( ph -> 1 = ( 2 logb 2 ) )
65 2z 
 |-  2 e. ZZ
66 65 a1i 
 |-  ( ph -> 2 e. ZZ )
67 44 leidd 
 |-  ( ph -> 2 <_ 2 )
68 1nn0 
 |-  1 e. NN0
69 43 68 nn0addge1i 
 |-  2 <_ ( 2 + 1 )
70 2p1e3 
 |-  ( 2 + 1 ) = 3
71 69 70 breqtri 
 |-  2 <_ 3
72 71 a1i 
 |-  ( ph -> 2 <_ 3 )
73 44 15 16 72 20 letrd 
 |-  ( ph -> 2 <_ N )
74 66 67 44 46 16 21 73 logblebd 
 |-  ( ph -> ( 2 logb 2 ) <_ ( 2 logb N ) )
75 64 74 eqbrtrd 
 |-  ( ph -> 1 <_ ( 2 logb N ) )
76 13 57 51 59 75 letrd 
 |-  ( ph -> 0 <_ ( 2 logb N ) )
77 52 53 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
78 51 54 76 77 mulge0d 
 |-  ( ph -> 0 <_ ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
79 flge 
 |-  ( ( ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) <-> 0 <_ ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
80 55 35 79 syl2anc 
 |-  ( ph -> ( 0 <_ ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) <-> 0 <_ ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
81 78 80 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
82 56 81 jca 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
83 elnn0z 
 |-  ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. NN0 <-> ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
84 82 83 sylibr 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. NN0 )
85 68 a1i 
 |-  ( ph -> 1 e. NN0 )
86 84 85 nn0addcld 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) e. NN0 )
87 2 phicld 
 |-  ( ph -> ( phi ` R ) e. NN )
88 87 nnred 
 |-  ( ph -> ( phi ` R ) e. RR )
89 87 nnnn0d 
 |-  ( ph -> ( phi ` R ) e. NN0 )
90 89 nn0ge0d 
 |-  ( ph -> 0 <_ ( phi ` R ) )
91 88 90 resqrtcld 
 |-  ( ph -> ( sqrt ` ( phi ` R ) ) e. RR )
92 91 51 remulcld 
 |-  ( ph -> ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) e. RR )
93 92 flcld 
 |-  ( ph -> ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. ZZ )
94 88 90 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( phi ` R ) ) )
95 91 51 94 76 mulge0d 
 |-  ( ph -> 0 <_ ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
96 flge 
 |-  ( ( ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) <-> 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) )
97 92 35 96 syl2anc 
 |-  ( ph -> ( 0 <_ ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) <-> 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) )
98 95 97 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) )
99 93 98 jca 
 |-  ( ph -> ( ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) )
100 elnn0z 
 |-  ( ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. NN0 <-> ( ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) )
101 99 100 sylibr 
 |-  ( ph -> ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. NN0 )
102 86 101 nn0addcld 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) e. NN0 )
103 56 peano2zd 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) e. ZZ )
104 1zzd 
 |-  ( ph -> 1 e. ZZ )
105 104 znegcld 
 |-  ( ph -> -u 1 e. ZZ )
106 103 105 zaddcld 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + -u 1 ) e. ZZ )
107 bccl 
 |-  ( ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) e. NN0 /\ ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + -u 1 ) e. ZZ ) -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + -u 1 ) ) e. NN0 )
108 102 106 107 syl2anc 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + -u 1 ) ) e. NN0 )
109 108 nn0red 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + -u 1 ) ) e. RR )
110 28 101 nn0addcld 
 |-  ( ph -> ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) e. NN0 )
111 28 nn0zd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. ZZ )
112 111 105 zaddcld 
 |-  ( ph -> ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + -u 1 ) e. ZZ )
113 bccl 
 |-  ( ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) e. NN0 /\ ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + -u 1 ) e. ZZ ) -> ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + -u 1 ) ) e. NN0 )
114 110 112 113 syl2anc 
 |-  ( ph -> ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + -u 1 ) ) e. NN0 )
115 114 nn0red 
 |-  ( ph -> ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + -u 1 ) ) e. RR )
116 54 51 remulcld 
 |-  ( ph -> ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) e. RR )
117 116 flcld 
 |-  ( ph -> ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) e. ZZ )
118 54 51 77 76 mulge0d 
 |-  ( ph -> 0 <_ ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) )
119 flge 
 |-  ( ( ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) <-> 0 <_ ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) )
120 116 35 119 syl2anc 
 |-  ( ph -> ( 0 <_ ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) <-> 0 <_ ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) )
121 118 120 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) )
122 117 121 jca 
 |-  ( ph -> ( ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) )
123 elnn0z 
 |-  ( ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) e. NN0 <-> ( ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) )
124 122 123 sylibr 
 |-  ( ph -> ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) e. NN0 )
125 86 124 nn0addcld 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) e. NN0 )
126 bccl 
 |-  ( ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) e. NN0 /\ ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. ZZ ) -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) e. NN0 )
127 125 56 126 syl2anc 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) e. NN0 )
128 127 nn0red 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) e. RR )
129 bccl 
 |-  ( ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) e. NN0 /\ ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. ZZ ) -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) e. NN0 )
130 102 56 129 syl2anc 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) e. NN0 )
131 130 nn0red 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) e. RR )
132 44 86 reexpcld 
 |-  ( ph -> ( 2 ^ ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) e. RR )
133 2nn0 
 |-  2 e. NN0
134 133 a1i 
 |-  ( ph -> 2 e. NN0 )
135 134 84 nn0mulcld 
 |-  ( ph -> ( 2 x. ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) e. NN0 )
136 135 85 nn0addcld 
 |-  ( ph -> ( ( 2 x. ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) e. NN0 )
137 bccl 
 |-  ( ( ( ( 2 x. ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) e. NN0 /\ ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. ZZ ) -> ( ( ( 2 x. ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) e. NN0 )
138 136 56 137 syl2anc 
 |-  ( ph -> ( ( ( 2 x. ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) e. NN0 )
139 138 nn0red 
 |-  ( ph -> ( ( ( 2 x. ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) e. RR )
140 13 44 46 ltled 
 |-  ( ph -> 0 <_ 2 )
141 44 140 55 recxpcld 
 |-  ( ph -> ( 2 ^c ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. RR )
142 reflcl 
 |-  ( ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. RR -> ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. RR )
143 55 142 syl 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. RR )
144 143 57 readdcld 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) e. RR )
145 44 140 144 recxpcld 
 |-  ( ph -> ( 2 ^c ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) e. RR )
146 1le2 
 |-  1 <_ 2
147 146 a1i 
 |-  ( ph -> 1 <_ 2 )
148 57 44 16 147 73 letrd 
 |-  ( ph -> 1 <_ N )
149 reflcl 
 |-  ( ( sqrt ` D ) e. RR -> ( |_ ` ( sqrt ` D ) ) e. RR )
150 32 149 syl 
 |-  ( ph -> ( |_ ` ( sqrt ` D ) ) e. RR )
151 26 fveq2d 
 |-  ( ph -> ( sqrt ` D ) = ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
152 151 fveq2d 
 |-  ( ph -> ( |_ ` ( sqrt ` D ) ) = ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
153 flle 
 |-  ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. RR -> ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
154 54 153 syl 
 |-  ( ph -> ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
155 152 154 eqbrtrd 
 |-  ( ph -> ( |_ ` ( sqrt ` D ) ) <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
156 16 148 150 54 155 cxplead 
 |-  ( ph -> ( N ^c ( |_ ` ( sqrt ` D ) ) ) <_ ( N ^c ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
157 16 recnd 
 |-  ( ph -> N e. CC )
158 13 21 gtned 
 |-  ( ph -> N =/= 0 )
159 157 158 33 cxpexpzd 
 |-  ( ph -> ( N ^c ( |_ ` ( sqrt ` D ) ) ) = ( N ^ ( |_ ` ( sqrt ` D ) ) ) )
160 61 50 nelprd 
 |-  ( ph -> -. 2 e. { 0 , 1 } )
161 60 160 eldifd 
 |-  ( ph -> 2 e. ( CC \ { 0 , 1 } ) )
162 158 neneqd 
 |-  ( ph -> -. N = 0 )
163 elsng 
 |-  ( N e. NN -> ( N e. { 0 } <-> N = 0 ) )
164 24 163 syl 
 |-  ( ph -> ( N e. { 0 } <-> N = 0 ) )
165 162 164 mtbird 
 |-  ( ph -> -. N e. { 0 } )
166 157 165 eldifd 
 |-  ( ph -> N e. ( CC \ { 0 } ) )
167 cxplogb 
 |-  ( ( 2 e. ( CC \ { 0 , 1 } ) /\ N e. ( CC \ { 0 } ) ) -> ( 2 ^c ( 2 logb N ) ) = N )
168 161 166 167 syl2anc 
 |-  ( ph -> ( 2 ^c ( 2 logb N ) ) = N )
169 168 eqcomd 
 |-  ( ph -> N = ( 2 ^c ( 2 logb N ) ) )
170 169 oveq1d 
 |-  ( ph -> ( N ^c ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) = ( ( 2 ^c ( 2 logb N ) ) ^c ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
171 156 159 170 3brtr3d 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) <_ ( ( 2 ^c ( 2 logb N ) ) ^c ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
172 44 46 elrpd 
 |-  ( ph -> 2 e. RR+ )
173 54 recnd 
 |-  ( ph -> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. CC )
174 cxpmul 
 |-  ( ( 2 e. RR+ /\ ( 2 logb N ) e. RR /\ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. CC ) -> ( 2 ^c ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) = ( ( 2 ^c ( 2 logb N ) ) ^c ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
175 172 51 173 174 syl3anc 
 |-  ( ph -> ( 2 ^c ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) = ( ( 2 ^c ( 2 logb N ) ) ^c ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
176 171 175 breqtrrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) <_ ( 2 ^c ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
177 fllep1 
 |-  ( ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. RR -> ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) <_ ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) )
178 55 177 syl 
 |-  ( ph -> ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) <_ ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) )
179 57 44 147 50 leneltd 
 |-  ( ph -> 1 < 2 )
180 86 nn0red 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) e. RR )
181 44 179 55 180 cxpled 
 |-  ( ph -> ( ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) <_ ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) <-> ( 2 ^c ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) <_ ( 2 ^c ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) ) )
182 178 181 mpbid 
 |-  ( ph -> ( 2 ^c ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) <_ ( 2 ^c ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) )
183 42 141 145 176 182 letrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) <_ ( 2 ^c ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) )
184 cxpexpz 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) e. ZZ ) -> ( 2 ^c ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) = ( 2 ^ ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) )
185 60 61 103 184 syl3anc 
 |-  ( ph -> ( 2 ^c ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) = ( 2 ^ ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) )
186 183 185 breqtrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) <_ ( 2 ^ ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) )
187 51 51 jca 
 |-  ( ph -> ( ( 2 logb N ) e. RR /\ ( 2 logb N ) e. RR ) )
188 remulcl 
 |-  ( ( ( 2 logb N ) e. RR /\ ( 2 logb N ) e. RR ) -> ( ( 2 logb N ) x. ( 2 logb N ) ) e. RR )
189 187 188 syl 
 |-  ( ph -> ( ( 2 logb N ) x. ( 2 logb N ) ) e. RR )
190 reflcl 
 |-  ( ( ( 2 logb N ) x. ( 2 logb N ) ) e. RR -> ( |_ ` ( ( 2 logb N ) x. ( 2 logb N ) ) ) e. RR )
191 189 190 syl 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) x. ( 2 logb N ) ) ) e. RR )
192 84 nn0red 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. RR )
193 44 46 15 18 50 relogbcld 
 |-  ( ph -> ( 2 logb 3 ) e. RR )
194 193 resqcld 
 |-  ( ph -> ( ( 2 logb 3 ) ^ 2 ) e. RR )
195 51 recnd 
 |-  ( ph -> ( 2 logb N ) e. CC )
196 195 sqvald 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) = ( ( 2 logb N ) x. ( 2 logb N ) ) )
197 196 189 eqeltrd 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) e. RR )
198 3lexlogpow2ineq2 
 |-  ( 2 < ( ( 2 logb 3 ) ^ 2 ) /\ ( ( 2 logb 3 ) ^ 2 ) < 3 )
199 198 simpli 
 |-  2 < ( ( 2 logb 3 ) ^ 2 )
200 199 a1i 
 |-  ( ph -> 2 < ( ( 2 logb 3 ) ^ 2 ) )
201 44 194 200 ltled 
 |-  ( ph -> 2 <_ ( ( 2 logb 3 ) ^ 2 ) )
202 15 44 61 redivcld 
 |-  ( ph -> ( 3 / 2 ) e. RR )
203 2rp 
 |-  2 e. RR+
204 203 a1i 
 |-  ( ph -> 2 e. RR+ )
205 13 15 18 ltled 
 |-  ( ph -> 0 <_ 3 )
206 15 204 205 divge0d 
 |-  ( ph -> 0 <_ ( 3 / 2 ) )
207 3lexlogpow2ineq1 
 |-  ( ( 3 / 2 ) < ( 2 logb 3 ) /\ ( 2 logb 3 ) < ( 5 / 3 ) )
208 207 simpli 
 |-  ( 3 / 2 ) < ( 2 logb 3 )
209 208 a1i 
 |-  ( ph -> ( 3 / 2 ) < ( 2 logb 3 ) )
210 202 193 209 ltled 
 |-  ( ph -> ( 3 / 2 ) <_ ( 2 logb 3 ) )
211 13 202 193 206 210 letrd 
 |-  ( ph -> 0 <_ ( 2 logb 3 ) )
212 66 67 15 18 16 21 20 logblebd 
 |-  ( ph -> ( 2 logb 3 ) <_ ( 2 logb N ) )
213 193 51 134 211 212 leexp1ad 
 |-  ( ph -> ( ( 2 logb 3 ) ^ 2 ) <_ ( ( 2 logb N ) ^ 2 ) )
214 44 194 197 201 213 letrd 
 |-  ( ph -> 2 <_ ( ( 2 logb N ) ^ 2 ) )
215 214 196 breqtrd 
 |-  ( ph -> 2 <_ ( ( 2 logb N ) x. ( 2 logb N ) ) )
216 flge 
 |-  ( ( ( ( 2 logb N ) x. ( 2 logb N ) ) e. RR /\ 2 e. ZZ ) -> ( 2 <_ ( ( 2 logb N ) x. ( 2 logb N ) ) <-> 2 <_ ( |_ ` ( ( 2 logb N ) x. ( 2 logb N ) ) ) ) )
217 189 66 216 syl2anc 
 |-  ( ph -> ( 2 <_ ( ( 2 logb N ) x. ( 2 logb N ) ) <-> 2 <_ ( |_ ` ( ( 2 logb N ) x. ( 2 logb N ) ) ) ) )
218 215 217 mpbid 
 |-  ( ph -> 2 <_ ( |_ ` ( ( 2 logb N ) x. ( 2 logb N ) ) ) )
219 51 51 remulcld 
 |-  ( ph -> ( ( 2 logb N ) x. ( 2 logb N ) ) e. RR )
220 24 1 4 2 5 6 7 27 10 aks6d1c3 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
221 173 sqvald 
 |-  ( ph -> ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ^ 2 ) = ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
222 28 nn0cnd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. CC )
223 222 msqsqrtd 
 |-  ( ph -> ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
224 221 223 eqtr2d 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) = ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ^ 2 ) )
225 220 224 breqtrd 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ^ 2 ) )
226 51 54 76 77 lt2sqd 
 |-  ( ph -> ( ( 2 logb N ) < ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) <-> ( ( 2 logb N ) ^ 2 ) < ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ^ 2 ) ) )
227 225 226 mpbird 
 |-  ( ph -> ( 2 logb N ) < ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
228 51 54 227 ltled 
 |-  ( ph -> ( 2 logb N ) <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
229 51 54 51 76 228 lemul2ad 
 |-  ( ph -> ( ( 2 logb N ) x. ( 2 logb N ) ) <_ ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
230 flwordi 
 |-  ( ( ( ( 2 logb N ) x. ( 2 logb N ) ) e. RR /\ ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. RR /\ ( ( 2 logb N ) x. ( 2 logb N ) ) <_ ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) -> ( |_ ` ( ( 2 logb N ) x. ( 2 logb N ) ) ) <_ ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
231 219 55 229 230 syl3anc 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) x. ( 2 logb N ) ) ) <_ ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
232 44 191 192 218 231 letrd 
 |-  ( ph -> 2 <_ ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
233 56 232 2ap1caineq 
 |-  ( ph -> ( 2 ^ ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) < ( ( ( 2 x. ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
234 42 132 139 186 233 lelttrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) < ( ( ( 2 x. ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
235 84 nn0cnd 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) e. CC )
236 235 2timesd 
 |-  ( ph -> ( 2 x. ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) = ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
237 236 oveq1d 
 |-  ( ph -> ( ( 2 x. ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) = ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) )
238 237 oveq1d 
 |-  ( ph -> ( ( ( 2 x. ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) = ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
239 234 238 breqtrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) < ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
240 1cnd 
 |-  ( ph -> 1 e. CC )
241 235 235 240 addassd 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) = ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) )
242 86 nn0cnd 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) e. CC )
243 235 242 addcomd 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) ) = ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
244 241 243 eqtrd 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) = ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
245 244 oveq1d 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) + 1 ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) = ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
246 239 245 breqtrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) < ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
247 195 173 mulcomd 
 |-  ( ph -> ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) = ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) )
248 247 fveq2d 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) = ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) )
249 248 oveq2d 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) = ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) )
250 249 oveq1d 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) = ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
251 246 250 breqtrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) < ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
252 124 nn0red 
 |-  ( ph -> ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) e. RR )
253 101 nn0red 
 |-  ( ph -> ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. RR )
254 8 29 eqeltrrid 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )
255 254 nn0red 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR )
256 254 nn0ge0d 
 |-  ( ph -> 0 <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
257 255 256 resqrtcld 
 |-  ( ph -> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. RR )
258 257 51 remulcld 
 |-  ( ph -> ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) e. RR )
259 24 1 4 2 5 6 7 aks6d1c4 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( phi ` R ) )
260 52 53 88 90 sqrtled 
 |-  ( ph -> ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( phi ` R ) <-> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) <_ ( sqrt ` ( phi ` R ) ) ) )
261 259 260 mpbid 
 |-  ( ph -> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) <_ ( sqrt ` ( phi ` R ) ) )
262 257 91 51 76 261 lemul1ad 
 |-  ( ph -> ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) <_ ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
263 flwordi 
 |-  ( ( ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) e. RR /\ ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) e. RR /\ ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) <_ ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) -> ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) )
264 258 92 262 263 syl3anc 
 |-  ( ph -> ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) )
265 252 253 144 264 leadd2dd 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) <_ ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) )
266 125 102 56 265 bcled 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( 2 logb N ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) <_ ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
267 42 128 131 251 266 ltletrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) < ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
268 235 240 pncand 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) - 1 ) = ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
269 268 eqcomd 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) = ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) - 1 ) )
270 242 240 negsubd 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + -u 1 ) = ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) - 1 ) )
271 270 eqcomd 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) - 1 ) = ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + -u 1 ) )
272 269 271 eqtrd 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) = ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + -u 1 ) )
273 272 oveq2d 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) ) = ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + -u 1 ) ) )
274 267 273 breqtrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) < ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + -u 1 ) ) )
275 2 nnnn0d 
 |-  ( ph -> R e. NN0 )
276 27 zncrng 
 |-  ( R e. NN0 -> ( Z/nZ ` R ) e. CRing )
277 275 276 syl 
 |-  ( ph -> ( Z/nZ ` R ) e. CRing )
278 crngring 
 |-  ( ( Z/nZ ` R ) e. CRing -> ( Z/nZ ` R ) e. Ring )
279 7 zrhrhm 
 |-  ( ( Z/nZ ` R ) e. Ring -> L e. ( ZZring RingHom ( Z/nZ ` R ) ) )
280 zringbas 
 |-  ZZ = ( Base ` ZZring )
281 eqid 
 |-  ( Base ` ( Z/nZ ` R ) ) = ( Base ` ( Z/nZ ` R ) )
282 280 281 rhmf 
 |-  ( L e. ( ZZring RingHom ( Z/nZ ` R ) ) -> L : ZZ --> ( Base ` ( Z/nZ ` R ) ) )
283 277 278 279 282 4syl 
 |-  ( ph -> L : ZZ --> ( Base ` ( Z/nZ ` R ) ) )
284 283 ffnd 
 |-  ( ph -> L Fn ZZ )
285 24 1 4 6 aks6d1c2p1 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> NN )
286 nnssz 
 |-  NN C_ ZZ
287 286 a1i 
 |-  ( ph -> NN C_ ZZ )
288 285 287 fssd 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> ZZ )
289 frn 
 |-  ( E : ( NN0 X. NN0 ) --> ZZ -> ran E C_ ZZ )
290 288 289 syl 
 |-  ( ph -> ran E C_ ZZ )
291 285 ffnd 
 |-  ( ph -> E Fn ( NN0 X. NN0 ) )
292 fnima 
 |-  ( E Fn ( NN0 X. NN0 ) -> ( E " ( NN0 X. NN0 ) ) = ran E )
293 291 292 syl 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) = ran E )
294 293 sseq1d 
 |-  ( ph -> ( ( E " ( NN0 X. NN0 ) ) C_ ZZ <-> ran E C_ ZZ ) )
295 290 294 mpbird 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) C_ ZZ )
296 vex 
 |-  k e. _V
297 vex 
 |-  l e. _V
298 296 297 op1std 
 |-  ( v = <. k , l >. -> ( 1st ` v ) = k )
299 298 oveq2d 
 |-  ( v = <. k , l >. -> ( P ^ ( 1st ` v ) ) = ( P ^ k ) )
300 296 297 op2ndd 
 |-  ( v = <. k , l >. -> ( 2nd ` v ) = l )
301 300 oveq2d 
 |-  ( v = <. k , l >. -> ( ( N / P ) ^ ( 2nd ` v ) ) = ( ( N / P ) ^ l ) )
302 299 301 oveq12d 
 |-  ( v = <. k , l >. -> ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) = ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
303 302 mpompt 
 |-  ( v e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ) = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
304 303 eqcomi 
 |-  ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) = ( v e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) )
305 6 304 eqtri 
 |-  E = ( v e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) )
306 305 a1i 
 |-  ( ph -> E = ( v e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ) )
307 c0ex 
 |-  0 e. _V
308 307 307 op1std 
 |-  ( v = <. 0 , 0 >. -> ( 1st ` v ) = 0 )
309 308 adantl 
 |-  ( ( ph /\ v = <. 0 , 0 >. ) -> ( 1st ` v ) = 0 )
310 309 oveq2d 
 |-  ( ( ph /\ v = <. 0 , 0 >. ) -> ( P ^ ( 1st ` v ) ) = ( P ^ 0 ) )
311 307 307 op2ndd 
 |-  ( v = <. 0 , 0 >. -> ( 2nd ` v ) = 0 )
312 311 adantl 
 |-  ( ( ph /\ v = <. 0 , 0 >. ) -> ( 2nd ` v ) = 0 )
313 312 oveq2d 
 |-  ( ( ph /\ v = <. 0 , 0 >. ) -> ( ( N / P ) ^ ( 2nd ` v ) ) = ( ( N / P ) ^ 0 ) )
314 310 313 oveq12d 
 |-  ( ( ph /\ v = <. 0 , 0 >. ) -> ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) = ( ( P ^ 0 ) x. ( ( N / P ) ^ 0 ) ) )
315 prmnn 
 |-  ( P e. Prime -> P e. NN )
316 1 315 syl 
 |-  ( ph -> P e. NN )
317 316 nncnd 
 |-  ( ph -> P e. CC )
318 317 exp0d 
 |-  ( ph -> ( P ^ 0 ) = 1 )
319 316 nnne0d 
 |-  ( ph -> P =/= 0 )
320 157 317 319 divcld 
 |-  ( ph -> ( N / P ) e. CC )
321 320 exp0d 
 |-  ( ph -> ( ( N / P ) ^ 0 ) = 1 )
322 318 321 oveq12d 
 |-  ( ph -> ( ( P ^ 0 ) x. ( ( N / P ) ^ 0 ) ) = ( 1 x. 1 ) )
323 240 mulridd 
 |-  ( ph -> ( 1 x. 1 ) = 1 )
324 322 323 eqtrd 
 |-  ( ph -> ( ( P ^ 0 ) x. ( ( N / P ) ^ 0 ) ) = 1 )
325 324 adantr 
 |-  ( ( ph /\ v = <. 0 , 0 >. ) -> ( ( P ^ 0 ) x. ( ( N / P ) ^ 0 ) ) = 1 )
326 314 325 eqtrd 
 |-  ( ( ph /\ v = <. 0 , 0 >. ) -> ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) = 1 )
327 0nn0 
 |-  0 e. NN0
328 327 a1i 
 |-  ( ph -> 0 e. NN0 )
329 328 328 opelxpd 
 |-  ( ph -> <. 0 , 0 >. e. ( NN0 X. NN0 ) )
330 1nn 
 |-  1 e. NN
331 330 a1i 
 |-  ( ph -> 1 e. NN )
332 306 326 329 331 fvmptd 
 |-  ( ph -> ( E ` <. 0 , 0 >. ) = 1 )
333 ssidd 
 |-  ( ph -> ( NN0 X. NN0 ) C_ ( NN0 X. NN0 ) )
334 fnfvima 
 |-  ( ( E Fn ( NN0 X. NN0 ) /\ ( NN0 X. NN0 ) C_ ( NN0 X. NN0 ) /\ <. 0 , 0 >. e. ( NN0 X. NN0 ) ) -> ( E ` <. 0 , 0 >. ) e. ( E " ( NN0 X. NN0 ) ) )
335 291 333 329 334 syl3anc 
 |-  ( ph -> ( E ` <. 0 , 0 >. ) e. ( E " ( NN0 X. NN0 ) ) )
336 332 335 eqeltrrd 
 |-  ( ph -> 1 e. ( E " ( NN0 X. NN0 ) ) )
337 fnfvima 
 |-  ( ( L Fn ZZ /\ ( E " ( NN0 X. NN0 ) ) C_ ZZ /\ 1 e. ( E " ( NN0 X. NN0 ) ) ) -> ( L ` 1 ) e. ( L " ( E " ( NN0 X. NN0 ) ) ) )
338 284 295 336 337 syl3anc 
 |-  ( ph -> ( L ` 1 ) e. ( L " ( E " ( NN0 X. NN0 ) ) ) )
339 7 a1i 
 |-  ( ph -> L = ( ZRHom ` ( Z/nZ ` R ) ) )
340 fvexd 
 |-  ( ph -> ( ZRHom ` ( Z/nZ ` R ) ) e. _V )
341 339 340 eqeltrd 
 |-  ( ph -> L e. _V )
342 341 imaexd 
 |-  ( ph -> ( L " ( E " ( NN0 X. NN0 ) ) ) e. _V )
343 338 342 hashelne0d 
 |-  ( ph -> -. ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) = 0 )
344 343 neqned 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) =/= 0 )
345 28 344 jca 
 |-  ( ph -> ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 /\ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) =/= 0 ) )
346 elnnne0 
 |-  ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN <-> ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 /\ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) =/= 0 ) )
347 345 346 sylibr 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN )
348 347 nnrpd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR+ )
349 348 rpsqrtcld 
 |-  ( ph -> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. RR+ )
350 51 54 349 227 ltmul1dd 
 |-  ( ph -> ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) < ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
351 52 53 52 53 sqrtmuld 
 |-  ( ph -> ( sqrt ` ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) x. ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) = ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
352 351 eqcomd 
 |-  ( ph -> ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) = ( sqrt ` ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) x. ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
353 350 352 breqtrd 
 |-  ( ph -> ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) < ( sqrt ` ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) x. ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
354 351 223 eqtrd 
 |-  ( ph -> ( sqrt ` ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) x. ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
355 353 354 breqtrd 
 |-  ( ph -> ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) < ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
356 fllt 
 |-  ( ( ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. RR /\ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. ZZ ) -> ( ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) < ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <-> ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) < ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
357 55 111 356 syl2anc 
 |-  ( ph -> ( ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) < ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <-> ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) < ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
358 355 357 mpbid 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) < ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
359 56 111 zltp1led 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) < ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <-> ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
360 358 359 mpbid 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
361 57 renegcld 
 |-  ( ph -> -u 1 e. RR )
362 df-neg 
 |-  -u 1 = ( 0 - 1 )
363 362 a1i 
 |-  ( ph -> -u 1 = ( 0 - 1 ) )
364 13 lem1d 
 |-  ( ph -> ( 0 - 1 ) <_ 0 )
365 363 364 eqbrtrd 
 |-  ( ph -> -u 1 <_ 0 )
366 361 13 253 365 98 letrd 
 |-  ( ph -> -u 1 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) )
367 86 28 101 105 360 366 bcle2d 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( ( |_ ` ( ( 2 logb N ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) + 1 ) + -u 1 ) ) <_ ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + -u 1 ) ) )
368 42 109 115 274 367 ltletrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) < ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + -u 1 ) ) )
369 222 240 negsubd 
 |-  ( ph -> ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + -u 1 ) = ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) - 1 ) )
370 369 oveq2d 
 |-  ( ph -> ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + -u 1 ) ) = ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) - 1 ) ) )
371 368 370 breqtrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) < ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) - 1 ) ) )
372 9 eqcomi 
 |-  ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) = A
373 372 a1i 
 |-  ( ph -> ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) = A )
374 373 oveq2d 
 |-  ( ph -> ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) = ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + A ) )
375 374 oveq1d 
 |-  ( ph -> ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) _C ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) - 1 ) ) = ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + A ) _C ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) - 1 ) ) )
376 371 375 breqtrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) < ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + A ) _C ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) - 1 ) ) )
377 26 eqcomd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) = D )
378 377 oveq1d 
 |-  ( ph -> ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + A ) = ( D + A ) )
379 377 oveq1d 
 |-  ( ph -> ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) - 1 ) = ( D - 1 ) )
380 378 379 oveq12d 
 |-  ( ph -> ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) + A ) _C ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) - 1 ) ) = ( ( D + A ) _C ( D - 1 ) ) )
381 376 380 breqtrd 
 |-  ( ph -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) < ( ( D + A ) _C ( D - 1 ) ) )