Metamath Proof Explorer

Theorem basellem1

Description: Lemma for basel . Closure of the sequence of roots. (Contributed by Mario Carneiro, 30-Jul-2014) Replace OLD theorem. (Revised ba Wolf Lammen, 18-Sep-2020.)

Ref Expression
Hypothesis basel.n 
|- N = ( ( 2 x. M ) + 1 )
Assertion basellem1 
|- ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( ( K x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) )

Proof

Step Hyp Ref Expression
1 basel.n 
 |-  N = ( ( 2 x. M ) + 1 )
2 elfznn 
 |-  ( K e. ( 1 ... M ) -> K e. NN )
3 2 nnrpd 
 |-  ( K e. ( 1 ... M ) -> K e. RR+ )
4 pirp 
 |-  _pi e. RR+
5 rpmulcl 
 |-  ( ( K e. RR+ /\ _pi e. RR+ ) -> ( K x. _pi ) e. RR+ )
6 3 4 5 sylancl 
 |-  ( K e. ( 1 ... M ) -> ( K x. _pi ) e. RR+ )
7 2nn 
 |-  2 e. NN
8 nnmulcl 
 |-  ( ( 2 e. NN /\ M e. NN ) -> ( 2 x. M ) e. NN )
9 7 8 mpan 
 |-  ( M e. NN -> ( 2 x. M ) e. NN )
10 9 peano2nnd 
 |-  ( M e. NN -> ( ( 2 x. M ) + 1 ) e. NN )
11 1 10 eqeltrid 
 |-  ( M e. NN -> N e. NN )
12 11 nnrpd 
 |-  ( M e. NN -> N e. RR+ )
13 rpdivcl 
 |-  ( ( ( K x. _pi ) e. RR+ /\ N e. RR+ ) -> ( ( K x. _pi ) / N ) e. RR+ )
14 6 12 13 syl2anr 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( ( K x. _pi ) / N ) e. RR+ )
15 14 rpred 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( ( K x. _pi ) / N ) e. RR )
16 14 rpgt0d 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> 0 < ( ( K x. _pi ) / N ) )
17 2 adantl 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> K e. NN )
18 nnmulcl 
 |-  ( ( K e. NN /\ 2 e. NN ) -> ( K x. 2 ) e. NN )
19 17 7 18 sylancl 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( K x. 2 ) e. NN )
20 19 nnred 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( K x. 2 ) e. RR )
21 9 adantr 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( 2 x. M ) e. NN )
22 21 nnred 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( 2 x. M ) e. RR )
23 11 adantr 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> N e. NN )
24 23 nnred 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> N e. RR )
25 1 24 eqeltrrid 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( ( 2 x. M ) + 1 ) e. RR )
26 17 nncnd 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> K e. CC )
27 2cn 
 |-  2 e. CC
28 mulcom 
 |-  ( ( K e. CC /\ 2 e. CC ) -> ( K x. 2 ) = ( 2 x. K ) )
29 26 27 28 sylancl 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( K x. 2 ) = ( 2 x. K ) )
30 elfzle2 
 |-  ( K e. ( 1 ... M ) -> K <_ M )
31 30 adantl 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> K <_ M )
32 17 nnred 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> K e. RR )
33 nnre 
 |-  ( M e. NN -> M e. RR )
34 33 adantr 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> M e. RR )
35 2re 
 |-  2 e. RR
36 2pos 
 |-  0 < 2
37 35 36 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
38 37 a1i 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( 2 e. RR /\ 0 < 2 ) )
39 lemul2 
 |-  ( ( K e. RR /\ M e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( K <_ M <-> ( 2 x. K ) <_ ( 2 x. M ) ) )
40 32 34 38 39 syl3anc 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( K <_ M <-> ( 2 x. K ) <_ ( 2 x. M ) ) )
41 31 40 mpbid 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( 2 x. K ) <_ ( 2 x. M ) )
42 29 41 eqbrtrd 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( K x. 2 ) <_ ( 2 x. M ) )
43 22 ltp1d 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( 2 x. M ) < ( ( 2 x. M ) + 1 ) )
44 20 22 25 42 43 lelttrd 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( K x. 2 ) < ( ( 2 x. M ) + 1 ) )
45 44 1 breqtrrdi 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( K x. 2 ) < N )
46 19 nngt0d 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> 0 < ( K x. 2 ) )
47 23 nngt0d 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> 0 < N )
48 pire 
 |-  _pi e. RR
49 remulcl 
 |-  ( ( K e. RR /\ _pi e. RR ) -> ( K x. _pi ) e. RR )
50 32 48 49 sylancl 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( K x. _pi ) e. RR )
51 6 adantl 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( K x. _pi ) e. RR+ )
52 51 rpgt0d 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> 0 < ( K x. _pi ) )
53 ltdiv2 
 |-  ( ( ( ( K x. 2 ) e. RR /\ 0 < ( K x. 2 ) ) /\ ( N e. RR /\ 0 < N ) /\ ( ( K x. _pi ) e. RR /\ 0 < ( K x. _pi ) ) ) -> ( ( K x. 2 ) < N <-> ( ( K x. _pi ) / N ) < ( ( K x. _pi ) / ( K x. 2 ) ) ) )
54 20 46 24 47 50 52 53 syl222anc 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( ( K x. 2 ) < N <-> ( ( K x. _pi ) / N ) < ( ( K x. _pi ) / ( K x. 2 ) ) ) )
55 45 54 mpbid 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( ( K x. _pi ) / N ) < ( ( K x. _pi ) / ( K x. 2 ) ) )
56 picn 
 |-  _pi e. CC
57 56 a1i 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> _pi e. CC )
58 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
59 58 a1i 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( 2 e. CC /\ 2 =/= 0 ) )
60 17 nnne0d 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> K =/= 0 )
61 divcan5 
 |-  ( ( _pi e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( K e. CC /\ K =/= 0 ) ) -> ( ( K x. _pi ) / ( K x. 2 ) ) = ( _pi / 2 ) )
62 57 59 26 60 61 syl112anc 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( ( K x. _pi ) / ( K x. 2 ) ) = ( _pi / 2 ) )
63 55 62 breqtrd 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( ( K x. _pi ) / N ) < ( _pi / 2 ) )
64 0xr 
 |-  0 e. RR*
65 rehalfcl 
 |-  ( _pi e. RR -> ( _pi / 2 ) e. RR )
66 rexr 
 |-  ( ( _pi / 2 ) e. RR -> ( _pi / 2 ) e. RR* )
67 48 65 66 mp2b 
 |-  ( _pi / 2 ) e. RR*
68 elioo2 
 |-  ( ( 0 e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( ( ( K x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) <-> ( ( ( K x. _pi ) / N ) e. RR /\ 0 < ( ( K x. _pi ) / N ) /\ ( ( K x. _pi ) / N ) < ( _pi / 2 ) ) ) )
69 64 67 68 mp2an 
 |-  ( ( ( K x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) <-> ( ( ( K x. _pi ) / N ) e. RR /\ 0 < ( ( K x. _pi ) / N ) /\ ( ( K x. _pi ) / N ) < ( _pi / 2 ) ) )
70 15 16 63 69 syl3anbrc 
 |-  ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( ( K x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) )