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 ⊢ 𝑁 = ( ( 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 ) ) )