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 by Wolf Lammen, 18-Sep-2020)

Ref Expression
Hypothesis basel.n ⊒ 𝑁 = ( ( 2 Β· 𝑀 ) + 1 )
Assertion basellem1 ( ( 𝑀 ∈ β„• ∧ 𝐾 ∈ ( 1 ... 𝑀 ) ) β†’ ( ( 𝐾 Β· Ο€ ) / 𝑁 ) ∈ ( 0 (,) ( Ο€ / 2 ) ) )

Proof

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