Metamath Proof Explorer

Theorem proththdlem

Description: Lemma for proththd . (Contributed by AV, 4-Jul-2020)

Ref Expression
Hypotheses proththd.n 
|- ( ph -> N e. NN )
proththd.k 
|- ( ph -> K e. NN )
proththd.p 
|- ( ph -> P = ( ( K x. ( 2 ^ N ) ) + 1 ) )
Assertion proththdlem 
|- ( ph -> ( P e. NN /\ 1 < P /\ ( ( P - 1 ) / 2 ) e. NN ) )

Proof

Step Hyp Ref Expression
1 proththd.n 
 |-  ( ph -> N e. NN )
2 proththd.k 
 |-  ( ph -> K e. NN )
3 proththd.p 
 |-  ( ph -> P = ( ( K x. ( 2 ^ N ) ) + 1 ) )
4 2nn 
 |-  2 e. NN
5 4 a1i 
 |-  ( ph -> 2 e. NN )
6 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
7 5 6 nnexpcld 
 |-  ( ph -> ( 2 ^ N ) e. NN )
8 2 7 nnmulcld 
 |-  ( ph -> ( K x. ( 2 ^ N ) ) e. NN )
9 8 peano2nnd 
 |-  ( ph -> ( ( K x. ( 2 ^ N ) ) + 1 ) e. NN )
10 1m1e0 
 |-  ( 1 - 1 ) = 0
11 8 nngt0d 
 |-  ( ph -> 0 < ( K x. ( 2 ^ N ) ) )
12 10 11 eqbrtrid 
 |-  ( ph -> ( 1 - 1 ) < ( K x. ( 2 ^ N ) ) )
13 1red 
 |-  ( ph -> 1 e. RR )
14 8 nnred 
 |-  ( ph -> ( K x. ( 2 ^ N ) ) e. RR )
15 13 13 14 ltsubaddd 
 |-  ( ph -> ( ( 1 - 1 ) < ( K x. ( 2 ^ N ) ) <-> 1 < ( ( K x. ( 2 ^ N ) ) + 1 ) ) )
16 12 15 mpbid 
 |-  ( ph -> 1 < ( ( K x. ( 2 ^ N ) ) + 1 ) )
17 8 nncnd 
 |-  ( ph -> ( K x. ( 2 ^ N ) ) e. CC )
18 pncan1 
 |-  ( ( K x. ( 2 ^ N ) ) e. CC -> ( ( ( K x. ( 2 ^ N ) ) + 1 ) - 1 ) = ( K x. ( 2 ^ N ) ) )
19 17 18 syl 
 |-  ( ph -> ( ( ( K x. ( 2 ^ N ) ) + 1 ) - 1 ) = ( K x. ( 2 ^ N ) ) )
20 19 oveq1d 
 |-  ( ph -> ( ( ( ( K x. ( 2 ^ N ) ) + 1 ) - 1 ) / 2 ) = ( ( K x. ( 2 ^ N ) ) / 2 ) )
21 2z 
 |-  2 e. ZZ
22 21 a1i 
 |-  ( ph -> 2 e. ZZ )
23 2 nnzd 
 |-  ( ph -> K e. ZZ )
24 7 nnzd 
 |-  ( ph -> ( 2 ^ N ) e. ZZ )
25 22 23 24 3jca 
 |-  ( ph -> ( 2 e. ZZ /\ K e. ZZ /\ ( 2 ^ N ) e. ZZ ) )
26 iddvdsexp 
 |-  ( ( 2 e. ZZ /\ N e. NN ) -> 2 || ( 2 ^ N ) )
27 22 1 26 syl2anc 
 |-  ( ph -> 2 || ( 2 ^ N ) )
28 dvdsmultr2 
 |-  ( ( 2 e. ZZ /\ K e. ZZ /\ ( 2 ^ N ) e. ZZ ) -> ( 2 || ( 2 ^ N ) -> 2 || ( K x. ( 2 ^ N ) ) ) )
29 25 27 28 sylc 
 |-  ( ph -> 2 || ( K x. ( 2 ^ N ) ) )
30 nndivdvds 
 |-  ( ( ( K x. ( 2 ^ N ) ) e. NN /\ 2 e. NN ) -> ( 2 || ( K x. ( 2 ^ N ) ) <-> ( ( K x. ( 2 ^ N ) ) / 2 ) e. NN ) )
31 8 5 30 syl2anc 
 |-  ( ph -> ( 2 || ( K x. ( 2 ^ N ) ) <-> ( ( K x. ( 2 ^ N ) ) / 2 ) e. NN ) )
32 29 31 mpbid 
 |-  ( ph -> ( ( K x. ( 2 ^ N ) ) / 2 ) e. NN )
33 20 32 eqeltrd 
 |-  ( ph -> ( ( ( ( K x. ( 2 ^ N ) ) + 1 ) - 1 ) / 2 ) e. NN )
34 9 16 33 3jca 
 |-  ( ph -> ( ( ( K x. ( 2 ^ N ) ) + 1 ) e. NN /\ 1 < ( ( K x. ( 2 ^ N ) ) + 1 ) /\ ( ( ( ( K x. ( 2 ^ N ) ) + 1 ) - 1 ) / 2 ) e. NN ) )
35 eleq1 
 |-  ( P = ( ( K x. ( 2 ^ N ) ) + 1 ) -> ( P e. NN <-> ( ( K x. ( 2 ^ N ) ) + 1 ) e. NN ) )
36 breq2 
 |-  ( P = ( ( K x. ( 2 ^ N ) ) + 1 ) -> ( 1 < P <-> 1 < ( ( K x. ( 2 ^ N ) ) + 1 ) ) )
37 oveq1 
 |-  ( P = ( ( K x. ( 2 ^ N ) ) + 1 ) -> ( P - 1 ) = ( ( ( K x. ( 2 ^ N ) ) + 1 ) - 1 ) )
38 37 oveq1d 
 |-  ( P = ( ( K x. ( 2 ^ N ) ) + 1 ) -> ( ( P - 1 ) / 2 ) = ( ( ( ( K x. ( 2 ^ N ) ) + 1 ) - 1 ) / 2 ) )
39 38 eleq1d 
 |-  ( P = ( ( K x. ( 2 ^ N ) ) + 1 ) -> ( ( ( P - 1 ) / 2 ) e. NN <-> ( ( ( ( K x. ( 2 ^ N ) ) + 1 ) - 1 ) / 2 ) e. NN ) )
40 35 36 39 3anbi123d 
 |-  ( P = ( ( K x. ( 2 ^ N ) ) + 1 ) -> ( ( P e. NN /\ 1 < P /\ ( ( P - 1 ) / 2 ) e. NN ) <-> ( ( ( K x. ( 2 ^ N ) ) + 1 ) e. NN /\ 1 < ( ( K x. ( 2 ^ N ) ) + 1 ) /\ ( ( ( ( K x. ( 2 ^ N ) ) + 1 ) - 1 ) / 2 ) e. NN ) ) )
41 34 40 syl5ibrcom 
 |-  ( ph -> ( P = ( ( K x. ( 2 ^ N ) ) + 1 ) -> ( P e. NN /\ 1 < P /\ ( ( P - 1 ) / 2 ) e. NN ) ) )
42 3 41 mpd 
 |-  ( ph -> ( P e. NN /\ 1 < P /\ ( ( P - 1 ) / 2 ) e. NN ) )