Metamath Proof Explorer

Theorem lcmineqlem17

Description: Inequality of 2^{2n}. (Contributed by metakunt, 29-Apr-2024)

Ref Expression
Hypothesis lcmineqlem17.1 
|- ( ph -> N e. NN0 )
Assertion lcmineqlem17 
|- ( ph -> ( 2 ^ ( 2 x. N ) ) <_ ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem17.1 
 |-  ( ph -> N e. NN0 )
2 2nn0 
 |-  2 e. NN0
3 2 a1i 
 |-  ( ph -> 2 e. NN0 )
4 3 1 nn0mulcld 
 |-  ( ph -> ( 2 x. N ) e. NN0 )
5 binom11 
 |-  ( ( 2 x. N ) e. NN0 -> ( 2 ^ ( 2 x. N ) ) = sum_ k e. ( 0 ... ( 2 x. N ) ) ( ( 2 x. N ) _C k ) )
6 4 5 syl 
 |-  ( ph -> ( 2 ^ ( 2 x. N ) ) = sum_ k e. ( 0 ... ( 2 x. N ) ) ( ( 2 x. N ) _C k ) )
7 fzfid 
 |-  ( ph -> ( 0 ... ( 2 x. N ) ) e. Fin )
8 4 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( 2 x. N ) ) ) -> ( 2 x. N ) e. NN0 )
9 elfzelz 
 |-  ( k e. ( 0 ... ( 2 x. N ) ) -> k e. ZZ )
10 9 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( 2 x. N ) ) ) -> k e. ZZ )
11 8 10 jca 
 |-  ( ( ph /\ k e. ( 0 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) e. NN0 /\ k e. ZZ ) )
12 bccl 
 |-  ( ( ( 2 x. N ) e. NN0 /\ k e. ZZ ) -> ( ( 2 x. N ) _C k ) e. NN0 )
13 11 12 syl 
 |-  ( ( ph /\ k e. ( 0 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) _C k ) e. NN0 )
14 13 nn0red 
 |-  ( ( ph /\ k e. ( 0 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) _C k ) e. RR )
15 1 nn0zd 
 |-  ( ph -> N e. ZZ )
16 bccl 
 |-  ( ( ( 2 x. N ) e. NN0 /\ N e. ZZ ) -> ( ( 2 x. N ) _C N ) e. NN0 )
17 4 15 16 syl2anc 
 |-  ( ph -> ( ( 2 x. N ) _C N ) e. NN0 )
18 17 nn0red 
 |-  ( ph -> ( ( 2 x. N ) _C N ) e. RR )
19 18 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) _C N ) e. RR )
20 bcmax 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( ( 2 x. N ) _C k ) <_ ( ( 2 x. N ) _C N ) )
21 1 9 20 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) _C k ) <_ ( ( 2 x. N ) _C N ) )
22 7 14 19 21 fsumle 
 |-  ( ph -> sum_ k e. ( 0 ... ( 2 x. N ) ) ( ( 2 x. N ) _C k ) <_ sum_ k e. ( 0 ... ( 2 x. N ) ) ( ( 2 x. N ) _C N ) )
23 6 22 eqbrtrd 
 |-  ( ph -> ( 2 ^ ( 2 x. N ) ) <_ sum_ k e. ( 0 ... ( 2 x. N ) ) ( ( 2 x. N ) _C N ) )
24 17 nn0cnd 
 |-  ( ph -> ( ( 2 x. N ) _C N ) e. CC )
25 fsumconst 
 |-  ( ( ( 0 ... ( 2 x. N ) ) e. Fin /\ ( ( 2 x. N ) _C N ) e. CC ) -> sum_ k e. ( 0 ... ( 2 x. N ) ) ( ( 2 x. N ) _C N ) = ( ( # ` ( 0 ... ( 2 x. N ) ) ) x. ( ( 2 x. N ) _C N ) ) )
26 7 24 25 syl2anc 
 |-  ( ph -> sum_ k e. ( 0 ... ( 2 x. N ) ) ( ( 2 x. N ) _C N ) = ( ( # ` ( 0 ... ( 2 x. N ) ) ) x. ( ( 2 x. N ) _C N ) ) )
27 hashfz0 
 |-  ( ( 2 x. N ) e. NN0 -> ( # ` ( 0 ... ( 2 x. N ) ) ) = ( ( 2 x. N ) + 1 ) )
28 4 27 syl 
 |-  ( ph -> ( # ` ( 0 ... ( 2 x. N ) ) ) = ( ( 2 x. N ) + 1 ) )
29 28 oveq1d 
 |-  ( ph -> ( ( # ` ( 0 ... ( 2 x. N ) ) ) x. ( ( 2 x. N ) _C N ) ) = ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) )
30 26 29 eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... ( 2 x. N ) ) ( ( 2 x. N ) _C N ) = ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) )
31 23 30 breqtrd 
 |-  ( ph -> ( 2 ^ ( 2 x. N ) ) <_ ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) )