Metamath Proof Explorer

Theorem knoppndvlem18

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 14-Aug-2021)

Ref Expression
Hypotheses knoppndvlem18.c 
|- ( ph -> C e. ( -u 1 (,) 1 ) )
knoppndvlem18.n 
|- ( ph -> N e. NN )
knoppndvlem18.d 
|- ( ph -> D e. RR+ )
knoppndvlem18.e 
|- ( ph -> E e. RR+ )
knoppndvlem18.g 
|- ( ph -> G e. RR+ )
knoppndvlem18.1 
|- ( ph -> 1 < ( N x. ( abs ` C ) ) )
Assertion knoppndvlem18 
|- ( ph -> E. j e. NN0 ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. G ) ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem18.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
2 knoppndvlem18.n 
 |-  ( ph -> N e. NN )
3 knoppndvlem18.d 
 |-  ( ph -> D e. RR+ )
4 knoppndvlem18.e 
 |-  ( ph -> E e. RR+ )
5 knoppndvlem18.g 
 |-  ( ph -> G e. RR+ )
6 knoppndvlem18.1 
 |-  ( ph -> 1 < ( N x. ( abs ` C ) ) )
7 2re 
 |-  2 e. RR
8 7 a1i 
 |-  ( ph -> 2 e. RR )
9 2 nnred 
 |-  ( ph -> N e. RR )
10 8 9 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
11 10 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( 2 x. N ) e. RR )
12 11 recnd 
 |-  ( ( ph /\ j e. NN ) -> ( 2 x. N ) e. CC )
13 2pos 
 |-  0 < 2
14 13 a1i 
 |-  ( ph -> 0 < 2 )
15 2 nngt0d 
 |-  ( ph -> 0 < N )
16 8 9 14 15 mulgt0d 
 |-  ( ph -> 0 < ( 2 x. N ) )
17 16 gt0ne0d 
 |-  ( ph -> ( 2 x. N ) =/= 0 )
18 17 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( 2 x. N ) =/= 0 )
19 nnz 
 |-  ( j e. NN -> j e. ZZ )
20 19 adantl 
 |-  ( ( ph /\ j e. NN ) -> j e. ZZ )
21 12 18 20 expnegd 
 |-  ( ( ph /\ j e. NN ) -> ( ( 2 x. N ) ^ -u j ) = ( 1 / ( ( 2 x. N ) ^ j ) ) )
22 21 adantrr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( ( 2 x. N ) ^ -u j ) = ( 1 / ( ( 2 x. N ) ^ j ) ) )
23 2rp 
 |-  2 e. RR+
24 23 a1i 
 |-  ( ph -> 2 e. RR+ )
25 24 3 jca 
 |-  ( ph -> ( 2 e. RR+ /\ D e. RR+ ) )
26 rpmulcl 
 |-  ( ( 2 e. RR+ /\ D e. RR+ ) -> ( 2 x. D ) e. RR+ )
27 25 26 syl 
 |-  ( ph -> ( 2 x. D ) e. RR+ )
28 27 adantr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( 2 x. D ) e. RR+ )
29 10 16 elrpd 
 |-  ( ph -> ( 2 x. N ) e. RR+ )
30 29 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( 2 x. N ) e. RR+ )
31 30 20 rpexpcld 
 |-  ( ( ph /\ j e. NN ) -> ( ( 2 x. N ) ^ j ) e. RR+ )
32 31 adantrr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( ( 2 x. N ) ^ j ) e. RR+ )
33 28 rprecred 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( 1 / ( 2 x. D ) ) e. RR )
34 1 knoppndvlem3 
 |-  ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
35 34 simpld 
 |-  ( ph -> C e. RR )
36 35 recnd 
 |-  ( ph -> C e. CC )
37 36 abscld 
 |-  ( ph -> ( abs ` C ) e. RR )
38 10 37 remulcld 
 |-  ( ph -> ( ( 2 x. N ) x. ( abs ` C ) ) e. RR )
39 38 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( ( 2 x. N ) x. ( abs ` C ) ) e. RR )
40 nnnn0 
 |-  ( j e. NN -> j e. NN0 )
41 40 adantl 
 |-  ( ( ph /\ j e. NN ) -> j e. NN0 )
42 39 41 reexpcld 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) e. RR )
43 42 adantrr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) e. RR )
44 32 rpred 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( ( 2 x. N ) ^ j ) e. RR )
45 4 rpred 
 |-  ( ph -> E e. RR )
46 5 rpred 
 |-  ( ph -> G e. RR )
47 5 rpne0d 
 |-  ( ph -> G =/= 0 )
48 45 46 47 redivcld 
 |-  ( ph -> ( E / G ) e. RR )
49 27 rprecred 
 |-  ( ph -> ( 1 / ( 2 x. D ) ) e. RR )
50 48 49 ifcld 
 |-  ( ph -> if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) e. RR )
51 50 adantr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) e. RR )
52 49 48 jca 
 |-  ( ph -> ( ( 1 / ( 2 x. D ) ) e. RR /\ ( E / G ) e. RR ) )
53 max1 
 |-  ( ( ( 1 / ( 2 x. D ) ) e. RR /\ ( E / G ) e. RR ) -> ( 1 / ( 2 x. D ) ) <_ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) )
54 52 53 syl 
 |-  ( ph -> ( 1 / ( 2 x. D ) ) <_ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) )
55 54 adantr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( 1 / ( 2 x. D ) ) <_ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) )
56 simprr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) )
57 33 51 43 55 56 lelttrd 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( 1 / ( 2 x. D ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) )
58 37 recnd 
 |-  ( ph -> ( abs ` C ) e. CC )
59 58 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( abs ` C ) e. CC )
60 12 59 41 mulexpd 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) = ( ( ( 2 x. N ) ^ j ) x. ( ( abs ` C ) ^ j ) ) )
61 37 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( abs ` C ) e. RR )
62 61 41 reexpcld 
 |-  ( ( ph /\ j e. NN ) -> ( ( abs ` C ) ^ j ) e. RR )
63 1red 
 |-  ( ( ph /\ j e. NN ) -> 1 e. RR )
64 31 rpred 
 |-  ( ( ph /\ j e. NN ) -> ( ( 2 x. N ) ^ j ) e. RR )
65 31 rpge0d 
 |-  ( ( ph /\ j e. NN ) -> 0 <_ ( ( 2 x. N ) ^ j ) )
66 36 absge0d 
 |-  ( ph -> 0 <_ ( abs ` C ) )
67 1red 
 |-  ( ph -> 1 e. RR )
68 34 simprd 
 |-  ( ph -> ( abs ` C ) < 1 )
69 37 67 68 ltled 
 |-  ( ph -> ( abs ` C ) <_ 1 )
70 37 66 69 3jca 
 |-  ( ph -> ( ( abs ` C ) e. RR /\ 0 <_ ( abs ` C ) /\ ( abs ` C ) <_ 1 ) )
71 70 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( ( abs ` C ) e. RR /\ 0 <_ ( abs ` C ) /\ ( abs ` C ) <_ 1 ) )
72 71 41 jca 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( abs ` C ) e. RR /\ 0 <_ ( abs ` C ) /\ ( abs ` C ) <_ 1 ) /\ j e. NN0 ) )
73 exple1 
 |-  ( ( ( ( abs ` C ) e. RR /\ 0 <_ ( abs ` C ) /\ ( abs ` C ) <_ 1 ) /\ j e. NN0 ) -> ( ( abs ` C ) ^ j ) <_ 1 )
74 72 73 syl 
 |-  ( ( ph /\ j e. NN ) -> ( ( abs ` C ) ^ j ) <_ 1 )
75 62 63 64 65 74 lemul2ad 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( 2 x. N ) ^ j ) x. ( ( abs ` C ) ^ j ) ) <_ ( ( ( 2 x. N ) ^ j ) x. 1 ) )
76 64 recnd 
 |-  ( ( ph /\ j e. NN ) -> ( ( 2 x. N ) ^ j ) e. CC )
77 76 mulid1d 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( 2 x. N ) ^ j ) x. 1 ) = ( ( 2 x. N ) ^ j ) )
78 75 77 breqtrd 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( 2 x. N ) ^ j ) x. ( ( abs ` C ) ^ j ) ) <_ ( ( 2 x. N ) ^ j ) )
79 60 78 eqbrtrd 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) <_ ( ( 2 x. N ) ^ j ) )
80 79 adantrr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) <_ ( ( 2 x. N ) ^ j ) )
81 33 43 44 57 80 ltletrd 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( 1 / ( 2 x. D ) ) < ( ( 2 x. N ) ^ j ) )
82 28 32 81 ltrec1d 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( 1 / ( ( 2 x. N ) ^ j ) ) < ( 2 x. D ) )
83 22 82 eqbrtrd 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( ( 2 x. N ) ^ -u j ) < ( 2 x. D ) )
84 nnnegz 
 |-  ( j e. NN -> -u j e. ZZ )
85 84 adantl 
 |-  ( ( ph /\ j e. NN ) -> -u j e. ZZ )
86 11 18 85 reexpclzd 
 |-  ( ( ph /\ j e. NN ) -> ( ( 2 x. N ) ^ -u j ) e. RR )
87 3 rpred 
 |-  ( ph -> D e. RR )
88 87 adantr 
 |-  ( ( ph /\ j e. NN ) -> D e. RR )
89 23 a1i 
 |-  ( ( ph /\ j e. NN ) -> 2 e. RR+ )
90 86 88 89 ltdivmuld 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D <-> ( ( 2 x. N ) ^ -u j ) < ( 2 x. D ) ) )
91 90 adantrr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D <-> ( ( 2 x. N ) ^ -u j ) < ( 2 x. D ) ) )
92 83 91 mpbird 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D )
93 48 adantr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( E / G ) e. RR )
94 max2 
 |-  ( ( ( 1 / ( 2 x. D ) ) e. RR /\ ( E / G ) e. RR ) -> ( E / G ) <_ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) )
95 52 94 syl 
 |-  ( ph -> ( E / G ) <_ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) )
96 95 adantr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( E / G ) <_ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) )
97 51 43 56 ltled 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) <_ ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) )
98 93 51 43 96 97 letrd 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( E / G ) <_ ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) )
99 45 adantr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> E e. RR )
100 5 adantr 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> G e. RR+ )
101 99 43 100 ledivmul2d 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( ( E / G ) <_ ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) <-> E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. G ) ) )
102 98 101 mpbid 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. G ) )
103 92 102 jca 
 |-  ( ( ph /\ ( j e. NN /\ if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) ) ) -> ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. G ) ) )
104 1t1e1 
 |-  ( 1 x. 1 ) = 1
105 104 eqcomi 
 |-  1 = ( 1 x. 1 )
106 105 a1i 
 |-  ( ph -> 1 = ( 1 x. 1 ) )
107 9 37 remulcld 
 |-  ( ph -> ( N x. ( abs ` C ) ) e. RR )
108 0le1 
 |-  0 <_ 1
109 108 a1i 
 |-  ( ph -> 0 <_ 1 )
110 1lt2 
 |-  1 < 2
111 110 a1i 
 |-  ( ph -> 1 < 2 )
112 67 8 67 107 109 111 109 6 ltmul12ad 
 |-  ( ph -> ( 1 x. 1 ) < ( 2 x. ( N x. ( abs ` C ) ) ) )
113 106 112 eqbrtrd 
 |-  ( ph -> 1 < ( 2 x. ( N x. ( abs ` C ) ) ) )
114 8 recnd 
 |-  ( ph -> 2 e. CC )
115 9 recnd 
 |-  ( ph -> N e. CC )
116 114 115 58 mulassd 
 |-  ( ph -> ( ( 2 x. N ) x. ( abs ` C ) ) = ( 2 x. ( N x. ( abs ` C ) ) ) )
117 116 eqcomd 
 |-  ( ph -> ( 2 x. ( N x. ( abs ` C ) ) ) = ( ( 2 x. N ) x. ( abs ` C ) ) )
118 113 117 breqtrd 
 |-  ( ph -> 1 < ( ( 2 x. N ) x. ( abs ` C ) ) )
119 50 38 118 3jca 
 |-  ( ph -> ( if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) e. RR /\ ( ( 2 x. N ) x. ( abs ` C ) ) e. RR /\ 1 < ( ( 2 x. N ) x. ( abs ` C ) ) ) )
120 expnbnd 
 |-  ( ( if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) e. RR /\ ( ( 2 x. N ) x. ( abs ` C ) ) e. RR /\ 1 < ( ( 2 x. N ) x. ( abs ` C ) ) ) -> E. j e. NN if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) )
121 119 120 syl 
 |-  ( ph -> E. j e. NN if ( ( 1 / ( 2 x. D ) ) <_ ( E / G ) , ( E / G ) , ( 1 / ( 2 x. D ) ) ) < ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) )
122 103 121 reximddv 
 |-  ( ph -> E. j e. NN ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. G ) ) )
123 nnssnn0 
 |-  NN C_ NN0
124 ssrexv 
 |-  ( NN C_ NN0 -> ( E. j e. NN ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. G ) ) -> E. j e. NN0 ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. G ) ) ) )
125 123 124 ax-mp 
 |-  ( E. j e. NN ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. G ) ) -> E. j e. NN0 ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. G ) ) )
126 122 125 syl 
 |-  ( ph -> E. j e. NN0 ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. G ) ) )