Metamath Proof Explorer

Theorem knoppndvlem19

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

Ref Expression
Hypotheses knoppndvlem19.a 
|- A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m )
knoppndvlem19.b 
|- B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) )
knoppndvlem19.j 
|- ( ph -> J e. NN0 )
knoppndvlem19.h 
|- ( ph -> H e. RR )
knoppndvlem19.n 
|- ( ph -> N e. NN )
Assertion knoppndvlem19 
|- ( ph -> E. m e. ZZ ( A <_ H /\ H <_ B ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem19.a 
 |-  A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m )
2 knoppndvlem19.b 
 |-  B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) )
3 knoppndvlem19.j 
 |-  ( ph -> J e. NN0 )
4 knoppndvlem19.h 
 |-  ( ph -> H e. RR )
5 knoppndvlem19.n 
 |-  ( ph -> N e. NN )
6 2re 
 |-  2 e. RR
7 6 a1i 
 |-  ( ph -> 2 e. RR )
8 5 nnred 
 |-  ( ph -> N e. RR )
9 7 8 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
10 2pos 
 |-  0 < 2
11 10 a1i 
 |-  ( ph -> 0 < 2 )
12 5 nngt0d 
 |-  ( ph -> 0 < N )
13 7 8 11 12 mulgt0d 
 |-  ( ph -> 0 < ( 2 x. N ) )
14 13 gt0ne0d 
 |-  ( ph -> ( 2 x. N ) =/= 0 )
15 3 nn0zd 
 |-  ( ph -> J e. ZZ )
16 15 znegcld 
 |-  ( ph -> -u J e. ZZ )
17 9 14 16 reexpclzd 
 |-  ( ph -> ( ( 2 x. N ) ^ -u J ) e. RR )
18 7 recnd 
 |-  ( ph -> 2 e. CC )
19 8 recnd 
 |-  ( ph -> N e. CC )
20 18 19 14 mulne0bad 
 |-  ( ph -> 2 =/= 0 )
21 17 7 20 redivcld 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. RR )
22 9 16 13 3jca 
 |-  ( ph -> ( ( 2 x. N ) e. RR /\ -u J e. ZZ /\ 0 < ( 2 x. N ) ) )
23 expgt0 
 |-  ( ( ( 2 x. N ) e. RR /\ -u J e. ZZ /\ 0 < ( 2 x. N ) ) -> 0 < ( ( 2 x. N ) ^ -u J ) )
24 22 23 syl 
 |-  ( ph -> 0 < ( ( 2 x. N ) ^ -u J ) )
25 17 7 24 11 divgt0d 
 |-  ( ph -> 0 < ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
26 25 gt0ne0d 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) =/= 0 )
27 4 21 26 redivcld 
 |-  ( ph -> ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) e. RR )
28 27 flcld 
 |-  ( ph -> ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) e. ZZ )
29 1 a1i 
 |-  ( m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) -> A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) )
30 id 
 |-  ( m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) -> m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) )
31 30 oveq2d 
 |-  ( m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) ) )
32 29 31 eqtrd 
 |-  ( m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) -> A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) ) )
33 32 breq1d 
 |-  ( m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) -> ( A <_ H <-> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) ) <_ H ) )
34 2 a1i 
 |-  ( m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) -> B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) )
35 30 oveq1d 
 |-  ( m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) -> ( m + 1 ) = ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) )
36 35 oveq2d 
 |-  ( m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) ) )
37 34 36 eqtrd 
 |-  ( m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) -> B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) ) )
38 37 breq2d 
 |-  ( m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) -> ( H <_ B <-> H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) ) ) )
39 33 38 anbi12d 
 |-  ( m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) -> ( ( A <_ H /\ H <_ B ) <-> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) ) ) ) )
40 39 adantl 
 |-  ( ( ph /\ m = ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) ) -> ( ( A <_ H /\ H <_ B ) <-> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) ) ) ) )
41 28 zred 
 |-  ( ph -> ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) e. RR )
42 0red 
 |-  ( ph -> 0 e. RR )
43 42 21 25 ltled 
 |-  ( ph -> 0 <_ ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
44 flle 
 |-  ( ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) e. RR -> ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) <_ ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) )
45 27 44 syl 
 |-  ( ph -> ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) <_ ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) )
46 41 27 21 43 45 lemul2ad 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) ) <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) )
47 4 recnd 
 |-  ( ph -> H e. CC )
48 21 recnd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. CC )
49 47 48 26 divcan2d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) = H )
50 46 49 breqtrd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) ) <_ H )
51 49 eqcomd 
 |-  ( ph -> H = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) )
52 peano2re 
 |-  ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) e. RR -> ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) e. RR )
53 41 52 syl 
 |-  ( ph -> ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) e. RR )
54 fllep1 
 |-  ( ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) e. RR -> ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) <_ ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) )
55 27 54 syl 
 |-  ( ph -> ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) <_ ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) )
56 27 53 21 43 55 lemul2ad 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) ) )
57 51 56 eqbrtrd 
 |-  ( ph -> H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) ) )
58 50 57 jca 
 |-  ( ph -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( |_ ` ( H / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) + 1 ) ) ) )
59 28 40 58 rspcedvd 
 |-  ( ph -> E. m e. ZZ ( A <_ H /\ H <_ B ) )