Proof of Theorem bposlem6
Step | Hyp | Ref
| Expression |
1 | | 4nn 11064 |
. . . . 5
⊢ 4 ∈
ℕ |
2 | | 5nn 11065 |
. . . . . . 7
⊢ 5 ∈
ℕ |
3 | | bpos.1 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘5)) |
4 | | eluznn 11634 |
. . . . . . 7
⊢ ((5
∈ ℕ ∧ 𝑁
∈ (ℤ≥‘5)) → 𝑁 ∈ ℕ) |
5 | 2, 3, 4 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
6 | 5 | nnnn0d 11228 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
7 | | nnexpcl 12735 |
. . . . 5
⊢ ((4
∈ ℕ ∧ 𝑁
∈ ℕ0) → (4↑𝑁) ∈ ℕ) |
8 | 1, 6, 7 | sylancr 694 |
. . . 4
⊢ (𝜑 → (4↑𝑁) ∈ ℕ) |
9 | 8 | nnred 10912 |
. . 3
⊢ (𝜑 → (4↑𝑁) ∈ ℝ) |
10 | 9, 5 | nndivred 10946 |
. 2
⊢ (𝜑 → ((4↑𝑁) / 𝑁) ∈ ℝ) |
11 | | fzctr 12320 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0...(2
· 𝑁))) |
12 | 6, 11 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (0...(2 · 𝑁))) |
13 | | bccl2 12972 |
. . . 4
⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ) |
14 | 12, 13 | syl 17 |
. . 3
⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ) |
15 | 14 | nnred 10912 |
. 2
⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℝ) |
16 | | 2nn 11062 |
. . . . . . 7
⊢ 2 ∈
ℕ |
17 | | nnmulcl 10920 |
. . . . . . 7
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) |
18 | 16, 5, 17 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → (2 · 𝑁) ∈
ℕ) |
19 | 18 | nnrpd 11746 |
. . . . 5
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ+) |
20 | 18 | nnred 10912 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
21 | 19 | rpge0d 11752 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (2 · 𝑁)) |
22 | 20, 21 | resqrtcld 14004 |
. . . . . . 7
⊢ (𝜑 → (√‘(2 ·
𝑁)) ∈
ℝ) |
23 | | 3nn 11063 |
. . . . . . 7
⊢ 3 ∈
ℕ |
24 | | nndivre 10933 |
. . . . . . 7
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ)
→ ((√‘(2 · 𝑁)) / 3) ∈ ℝ) |
25 | 22, 23, 24 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → ((√‘(2
· 𝑁)) / 3) ∈
ℝ) |
26 | | 2re 10967 |
. . . . . 6
⊢ 2 ∈
ℝ |
27 | | readdcl 9898 |
. . . . . 6
⊢
((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈
ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈
ℝ) |
28 | 25, 26, 27 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) + 2)
∈ ℝ) |
29 | 19, 28 | rpcxpcld 24276 |
. . . 4
⊢ (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
∈ ℝ+) |
30 | 29 | rpred 11748 |
. . 3
⊢ (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
∈ ℝ) |
31 | | 2rp 11713 |
. . . . 5
⊢ 2 ∈
ℝ+ |
32 | | nnmulcl 10920 |
. . . . . . . . 9
⊢ ((4
∈ ℕ ∧ 𝑁
∈ ℕ) → (4 · 𝑁) ∈ ℕ) |
33 | 1, 5, 32 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → (4 · 𝑁) ∈
ℕ) |
34 | 33 | nnred 10912 |
. . . . . . 7
⊢ (𝜑 → (4 · 𝑁) ∈
ℝ) |
35 | | nndivre 10933 |
. . . . . . 7
⊢ (((4
· 𝑁) ∈ ℝ
∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ) |
36 | 34, 23, 35 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → ((4 · 𝑁) / 3) ∈
ℝ) |
37 | | 5re 10976 |
. . . . . 6
⊢ 5 ∈
ℝ |
38 | | resubcl 10224 |
. . . . . 6
⊢ ((((4
· 𝑁) / 3) ∈
ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈
ℝ) |
39 | 36, 37, 38 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈
ℝ) |
40 | | rpcxpcl 24222 |
. . . . 5
⊢ ((2
∈ ℝ+ ∧ (((4 · 𝑁) / 3) − 5) ∈ ℝ) →
(2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈
ℝ+) |
41 | 31, 39, 40 | sylancr 694 |
. . . 4
⊢ (𝜑 →
(2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈
ℝ+) |
42 | 41 | rpred 11748 |
. . 3
⊢ (𝜑 →
(2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈
ℝ) |
43 | 30, 42 | remulcld 9949 |
. 2
⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5))) ∈
ℝ) |
44 | | df-5 10959 |
. . . . 5
⊢ 5 = (4 +
1) |
45 | | 4z 11288 |
. . . . . 6
⊢ 4 ∈
ℤ |
46 | | uzid 11578 |
. . . . . 6
⊢ (4 ∈
ℤ → 4 ∈ (ℤ≥‘4)) |
47 | | peano2uz 11617 |
. . . . . 6
⊢ (4 ∈
(ℤ≥‘4) → (4 + 1) ∈
(ℤ≥‘4)) |
48 | 45, 46, 47 | mp2b 10 |
. . . . 5
⊢ (4 + 1)
∈ (ℤ≥‘4) |
49 | 44, 48 | eqeltri 2684 |
. . . 4
⊢ 5 ∈
(ℤ≥‘4) |
50 | | eqid 2610 |
. . . . 5
⊢
(ℤ≥‘4) =
(ℤ≥‘4) |
51 | 50 | uztrn2 11581 |
. . . 4
⊢ ((5
∈ (ℤ≥‘4) ∧ 𝑁 ∈ (ℤ≥‘5))
→ 𝑁 ∈
(ℤ≥‘4)) |
52 | 49, 3, 51 | sylancr 694 |
. . 3
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘4)) |
53 | | bclbnd 24805 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)) |
54 | 52, 53 | syl 17 |
. 2
⊢ (𝜑 → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)) |
55 | | bpos.3 |
. . . . . . . 8
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) |
56 | | id 22 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℙ → 𝑛 ∈
ℙ) |
57 | | pccl 15392 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℙ ∧ ((2
· 𝑁)C𝑁) ∈ ℕ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
58 | 56, 14, 57 | syl2anr 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
59 | 58 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
60 | 55, 59 | pcmptcl 15433 |
. . . . . . 7
⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( ·
, 𝐹):ℕ⟶ℕ)) |
61 | 60 | simprd 478 |
. . . . . 6
⊢ (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ) |
62 | | bpos.2 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) |
63 | | bpos.4 |
. . . . . . . . 9
⊢ 𝐾 = (⌊‘((2 ·
𝑁) / 3)) |
64 | | bpos.5 |
. . . . . . . . 9
⊢ 𝑀 =
(⌊‘(√‘(2 · 𝑁))) |
65 | 3, 62, 55, 63, 64 | bposlem4 24812 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (3...𝐾)) |
66 | | elfzuz 12209 |
. . . . . . . 8
⊢ (𝑀 ∈ (3...𝐾) → 𝑀 ∈
(ℤ≥‘3)) |
67 | 65, 66 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘3)) |
68 | | eluznn 11634 |
. . . . . . 7
⊢ ((3
∈ ℕ ∧ 𝑀
∈ (ℤ≥‘3)) → 𝑀 ∈ ℕ) |
69 | 23, 67, 68 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
70 | 61, 69 | ffvelrnd 6268 |
. . . . 5
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℕ) |
71 | 70 | nnred 10912 |
. . . 4
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℝ) |
72 | | 2z 11286 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
73 | | nndivre 10933 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑁) ∈ ℝ
∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℝ) |
74 | 20, 23, 73 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁) / 3) ∈
ℝ) |
75 | 74 | flcld 12461 |
. . . . . . . . . 10
⊢ (𝜑 → (⌊‘((2
· 𝑁) / 3)) ∈
ℤ) |
76 | 63, 75 | syl5eqel 2692 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℤ) |
77 | | zmulcl 11303 |
. . . . . . . . 9
⊢ ((2
∈ ℤ ∧ 𝐾
∈ ℤ) → (2 · 𝐾) ∈ ℤ) |
78 | 72, 76, 77 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝐾) ∈
ℤ) |
79 | 2 | nnzi 11278 |
. . . . . . . 8
⊢ 5 ∈
ℤ |
80 | | zsubcl 11296 |
. . . . . . . 8
⊢ (((2
· 𝐾) ∈ ℤ
∧ 5 ∈ ℤ) → ((2 · 𝐾) − 5) ∈
ℤ) |
81 | 78, 79, 80 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → ((2 · 𝐾) − 5) ∈
ℤ) |
82 | 81 | zred 11358 |
. . . . . 6
⊢ (𝜑 → ((2 · 𝐾) − 5) ∈
ℝ) |
83 | | rpcxpcl 24222 |
. . . . . 6
⊢ ((2
∈ ℝ+ ∧ ((2 · 𝐾) − 5) ∈ ℝ) →
(2↑𝑐((2 · 𝐾) − 5)) ∈
ℝ+) |
84 | 31, 82, 83 | sylancr 694 |
. . . . 5
⊢ (𝜑 →
(2↑𝑐((2 · 𝐾) − 5)) ∈
ℝ+) |
85 | 84 | rpred 11748 |
. . . 4
⊢ (𝜑 →
(2↑𝑐((2 · 𝐾) − 5)) ∈
ℝ) |
86 | 71, 85 | remulcld 9949 |
. . 3
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) − 5)))
∈ ℝ) |
87 | 3, 62, 55, 63 | bposlem3 24811 |
. . . 4
⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁)) |
88 | | elfzuz3 12210 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (3...𝐾) → 𝐾 ∈ (ℤ≥‘𝑀)) |
89 | 65, 88 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) |
90 | 55, 59, 69, 89 | pcmptdvds 15436 |
. . . . . . . 8
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾)) |
91 | 70 | nnzd 11357 |
. . . . . . . . 9
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℤ) |
92 | 70 | nnne0d 10942 |
. . . . . . . . 9
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≠ 0) |
93 | | uztrn 11580 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑀 ∈ (ℤ≥‘3))
→ 𝐾 ∈
(ℤ≥‘3)) |
94 | 89, 67, 93 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘3)) |
95 | | eluznn 11634 |
. . . . . . . . . . . 12
⊢ ((3
∈ ℕ ∧ 𝐾
∈ (ℤ≥‘3)) → 𝐾 ∈ ℕ) |
96 | 23, 94, 95 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ ℕ) |
97 | 61, 96 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℕ) |
98 | 97 | nnzd 11357 |
. . . . . . . . 9
⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℤ) |
99 | | dvdsval2 14824 |
. . . . . . . . 9
⊢ (((seq1(
· , 𝐹)‘𝑀) ∈ ℤ ∧ (seq1(
· , 𝐹)‘𝑀) ≠ 0 ∧ (seq1( · ,
𝐹)‘𝐾) ∈ ℤ) → ((seq1( · ,
𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾) ↔ ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ)) |
100 | 91, 92, 98, 99 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾) ↔ ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ)) |
101 | 90, 100 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ) |
102 | 101 | zred 11358 |
. . . . . 6
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℝ) |
103 | 69 | nnred 10912 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℝ) |
104 | 76 | zred 11358 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℝ) |
105 | | eluzle 11576 |
. . . . . . . . . 10
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝐾) |
106 | 89, 105 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ≤ 𝐾) |
107 | | efchtdvds 24685 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑀 ≤ 𝐾) → (exp‘(θ‘𝑀)) ∥
(exp‘(θ‘𝐾))) |
108 | 103, 104,
106, 107 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 →
(exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾))) |
109 | | efchtcl 24637 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℝ →
(exp‘(θ‘𝑀)) ∈ ℕ) |
110 | 103, 109 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(exp‘(θ‘𝑀)) ∈ ℕ) |
111 | 110 | nnzd 11357 |
. . . . . . . . 9
⊢ (𝜑 →
(exp‘(θ‘𝑀)) ∈ ℤ) |
112 | 110 | nnne0d 10942 |
. . . . . . . . 9
⊢ (𝜑 →
(exp‘(θ‘𝑀)) ≠ 0) |
113 | | efchtcl 24637 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℝ →
(exp‘(θ‘𝐾)) ∈ ℕ) |
114 | 104, 113 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(exp‘(θ‘𝐾)) ∈ ℕ) |
115 | 114 | nnzd 11357 |
. . . . . . . . 9
⊢ (𝜑 →
(exp‘(θ‘𝐾)) ∈ ℤ) |
116 | | dvdsval2 14824 |
. . . . . . . . 9
⊢
(((exp‘(θ‘𝑀)) ∈ ℤ ∧
(exp‘(θ‘𝑀)) ≠ 0 ∧
(exp‘(θ‘𝐾)) ∈ ℤ) →
((exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)) ↔
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈
ℤ)) |
117 | 111, 112,
115, 116 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 →
((exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)) ↔
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈
ℤ)) |
118 | 108, 117 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈
ℤ) |
119 | 118 | zred 11358 |
. . . . . 6
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈
ℝ) |
120 | | prmz 15227 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
121 | | fllt 12469 |
. . . . . . . . . . . . . . . . . 18
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ 𝑝 ∈ ℤ) → ((√‘(2
· 𝑁)) < 𝑝 ↔
(⌊‘(√‘(2 · 𝑁))) < 𝑝)) |
122 | 22, 120, 121 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2
· 𝑁)) < 𝑝 ↔
(⌊‘(√‘(2 · 𝑁))) < 𝑝)) |
123 | 64 | breq1i 4590 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 < 𝑝 ↔ (⌊‘(√‘(2
· 𝑁))) < 𝑝) |
124 | 122, 123 | syl6bbr 277 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2
· 𝑁)) < 𝑝 ↔ 𝑀 < 𝑝)) |
125 | 120 | zred 11358 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℝ) |
126 | | ltnle 9996 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ ℝ) → (𝑀 < 𝑝 ↔ ¬ 𝑝 ≤ 𝑀)) |
127 | 103, 125,
126 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀 < 𝑝 ↔ ¬ 𝑝 ≤ 𝑀)) |
128 | 124, 127 | bitrd 267 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2
· 𝑁)) < 𝑝 ↔ ¬ 𝑝 ≤ 𝑀)) |
129 | | bposlem1 24809 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) |
130 | 5, 129 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) |
131 | 125 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ) |
132 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℙ) |
133 | | pccl 15392 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ ℙ ∧ ((2
· 𝑁)C𝑁) ∈ ℕ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
134 | 132, 14, 133 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
135 | 131, 134 | reexpcld 12887 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ) |
136 | 20 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (2 · 𝑁) ∈
ℝ) |
137 | 131 | resqcld 12897 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝↑2) ∈ ℝ) |
138 | | lelttr 10007 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ (𝑝↑2) ∈ ℝ) →
(((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ∧ (2 · 𝑁) < (𝑝↑2)) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2))) |
139 | 135, 136,
137, 138 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ∧ (2 · 𝑁) < (𝑝↑2)) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2))) |
140 | 130, 139 | mpand 707 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((2 · 𝑁) < (𝑝↑2) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2))) |
141 | | resqrtth 13844 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((2
· 𝑁) ∈ ℝ
∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁))↑2) = (2 · 𝑁)) |
142 | 20, 21, 141 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((√‘(2
· 𝑁))↑2) = (2
· 𝑁)) |
143 | 142 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((√‘(2
· 𝑁))↑2) <
(𝑝↑2) ↔ (2
· 𝑁) < (𝑝↑2))) |
144 | 143 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((√‘(2
· 𝑁))↑2) <
(𝑝↑2) ↔ (2
· 𝑁) < (𝑝↑2))) |
145 | 134 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ) |
146 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 2 ∈
ℤ) |
147 | | prmgt1 15247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈ ℙ → 1 <
𝑝) |
148 | 147 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 1 < 𝑝) |
149 | 131, 145,
146, 148 | ltexp2d 12900 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2 ↔ (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2))) |
150 | 140, 144,
149 | 3imtr4d 282 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((√‘(2
· 𝑁))↑2) <
(𝑝↑2) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2)) |
151 | | df-2 10956 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 = (1 +
1) |
152 | 151 | breq2i 4591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)) |
153 | 150, 152 | syl6ib 240 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((√‘(2
· 𝑁))↑2) <
(𝑝↑2) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1))) |
154 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (√‘(2
· 𝑁)) ∈
ℝ) |
155 | 20, 21 | sqrtge0d 14007 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 ≤ (√‘(2
· 𝑁))) |
156 | 155 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 0 ≤
(√‘(2 · 𝑁))) |
157 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
158 | 157 | nnrpd 11746 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℝ+) |
159 | 158 | rpge0d 11752 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 0 ≤
𝑝) |
160 | 159 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 0 ≤ 𝑝) |
161 | 154, 131,
156, 160 | lt2sqd 12905 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2
· 𝑁)) < 𝑝 ↔ ((√‘(2
· 𝑁))↑2) <
(𝑝↑2))) |
162 | | 1z 11284 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℤ |
163 | | zleltp1 11305 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ ∧ 1 ∈ ℤ)
→ ((𝑝 pCnt ((2
· 𝑁)C𝑁)) ≤ 1 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1))) |
164 | 145, 162,
163 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1))) |
165 | 153, 161,
164 | 3imtr4d 282 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2
· 𝑁)) < 𝑝 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1)) |
166 | 128, 165 | sylbird 249 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (¬ 𝑝 ≤ 𝑀 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1)) |
167 | 166 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ ¬ 𝑝 ≤ 𝑀) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1) |
168 | 167 | adantrl 748 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1) |
169 | | iftrue 4042 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁))) |
170 | 169 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁))) |
171 | | iftrue 4042 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0) = 1) |
172 | 171 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0) = 1) |
173 | 168, 170,
172 | 3brtr4d 4615 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0)) |
174 | | 0le0 10987 |
. . . . . . . . . . . . 13
⊢ 0 ≤
0 |
175 | | iffalse 4045 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = 0) |
176 | | iffalse 4045 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0) = 0) |
177 | 175, 176 | breq12d 4596 |
. . . . . . . . . . . . 13
⊢ (¬
(𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → (if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0) ↔ 0 ≤ 0)) |
178 | 174, 177 | mpbiri 247 |
. . . . . . . . . . . 12
⊢ (¬
(𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0)) |
179 | 178 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ ¬ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0)) |
180 | 173, 179 | pm2.61dan 828 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0)) |
181 | 59 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
182 | 69 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑀 ∈ ℕ) |
183 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) |
184 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑝 → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = (𝑝 pCnt ((2 · 𝑁)C𝑁))) |
185 | 89 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝐾 ∈ (ℤ≥‘𝑀)) |
186 | 55, 181, 182, 183, 184, 185 | pcmpt2 15435 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) = if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0)) |
187 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) |
188 | 187 | prmorcht 24704 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℕ →
(exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾)) |
189 | 96, 188 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾)) |
190 | 187 | prmorcht 24704 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ →
(exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)) |
191 | 69, 190 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)) |
192 | 189, 191 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))) |
193 | 192 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))) |
194 | 193 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀)))) = (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)))) |
195 | | nncn 10905 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
196 | 195 | exp1d 12865 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛) |
197 | 196 | ifeq1d 4054 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → if(𝑛 ∈ ℙ, (𝑛↑1), 1) = if(𝑛 ∈ ℙ, 𝑛, 1)) |
198 | 197 | mpteq2ia 4668 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) |
199 | 198 | eqcomi 2619 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) |
200 | | 1nn0 11185 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℕ0 |
201 | 200 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℙ) → 1 ∈
ℕ0) |
202 | 201 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑛 ∈ ℙ 1 ∈
ℕ0) |
203 | 202 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ 1 ∈
ℕ0) |
204 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑝 → 1 = 1) |
205 | 199, 203,
182, 183, 204, 185 | pcmpt2 15435 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))) = if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0)) |
206 | 194, 205 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀)))) = if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0)) |
207 | 180, 186,
206 | 3brtr4d 4615 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))))) |
208 | 207 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))))) |
209 | | pc2dvds 15421 |
. . . . . . . . 9
⊢ ((((seq1(
· , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ ∧
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ) →
(((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀)))))) |
210 | 101, 118,
209 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀)))))) |
211 | 208, 210 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀)))) |
212 | 114 | nnred 10912 |
. . . . . . . . . 10
⊢ (𝜑 →
(exp‘(θ‘𝐾)) ∈ ℝ) |
213 | 110 | nnred 10912 |
. . . . . . . . . 10
⊢ (𝜑 →
(exp‘(θ‘𝑀)) ∈ ℝ) |
214 | 114 | nngt0d 10941 |
. . . . . . . . . 10
⊢ (𝜑 → 0 <
(exp‘(θ‘𝐾))) |
215 | 110 | nngt0d 10941 |
. . . . . . . . . 10
⊢ (𝜑 → 0 <
(exp‘(θ‘𝑀))) |
216 | 212, 213,
214, 215 | divgt0d 10838 |
. . . . . . . . 9
⊢ (𝜑 → 0 <
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))) |
217 | | elnnz 11264 |
. . . . . . . . 9
⊢
(((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ ↔
(((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ ∧ 0 <
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))) |
218 | 118, 216,
217 | sylanbrc 695 |
. . . . . . . 8
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈
ℕ) |
219 | | dvdsle 14870 |
. . . . . . . 8
⊢ ((((seq1(
· , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ ∧
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ) →
(((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))) → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))))) |
220 | 101, 218,
219 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))) → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))))) |
221 | 211, 220 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀)))) |
222 | | nndivre 10933 |
. . . . . . . 8
⊢
(((exp‘(θ‘𝐾)) ∈ ℝ ∧ 4 ∈ ℕ)
→ ((exp‘(θ‘𝐾)) / 4) ∈ ℝ) |
223 | 212, 1, 222 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / 4) ∈ ℝ) |
224 | | 4re 10974 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
225 | 224 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 4 ∈
ℝ) |
226 | | 6re 10978 |
. . . . . . . . . 10
⊢ 6 ∈
ℝ |
227 | 226 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 6 ∈
ℝ) |
228 | | 4lt6 11082 |
. . . . . . . . . 10
⊢ 4 <
6 |
229 | 228 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 4 < 6) |
230 | | cht3 24699 |
. . . . . . . . . . . 12
⊢
(θ‘3) = (log‘6) |
231 | 230 | fveq2i 6106 |
. . . . . . . . . . 11
⊢
(exp‘(θ‘3)) =
(exp‘(log‘6)) |
232 | | 6pos 10996 |
. . . . . . . . . . . . 13
⊢ 0 <
6 |
233 | 226, 232 | elrpii 11711 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℝ+ |
234 | | reeflog 24131 |
. . . . . . . . . . . 12
⊢ (6 ∈
ℝ+ → (exp‘(log‘6)) = 6) |
235 | 233, 234 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(exp‘(log‘6)) = 6 |
236 | 231, 235 | eqtri 2632 |
. . . . . . . . . 10
⊢
(exp‘(θ‘3)) = 6 |
237 | | 3re 10971 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℝ |
238 | 237 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 3 ∈
ℝ) |
239 | | eluzle 11576 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈
(ℤ≥‘3) → 3 ≤ 𝑀) |
240 | 67, 239 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 3 ≤ 𝑀) |
241 | | chtwordi 24682 |
. . . . . . . . . . . 12
⊢ ((3
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 3 ≤ 𝑀) → (θ‘3) ≤
(θ‘𝑀)) |
242 | 238, 103,
240, 241 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (θ‘3) ≤
(θ‘𝑀)) |
243 | | chtcl 24635 |
. . . . . . . . . . . . 13
⊢ (3 ∈
ℝ → (θ‘3) ∈ ℝ) |
244 | 237, 243 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(θ‘3) ∈ ℝ |
245 | | chtcl 24635 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℝ →
(θ‘𝑀) ∈
ℝ) |
246 | 103, 245 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (θ‘𝑀) ∈
ℝ) |
247 | | efle 14687 |
. . . . . . . . . . . 12
⊢
(((θ‘3) ∈ ℝ ∧ (θ‘𝑀) ∈ ℝ) →
((θ‘3) ≤ (θ‘𝑀) ↔ (exp‘(θ‘3)) ≤
(exp‘(θ‘𝑀)))) |
248 | 244, 246,
247 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → ((θ‘3) ≤
(θ‘𝑀) ↔
(exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀)))) |
249 | 242, 248 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 →
(exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀))) |
250 | 236, 249 | syl5eqbrr 4619 |
. . . . . . . . 9
⊢ (𝜑 → 6 ≤
(exp‘(θ‘𝑀))) |
251 | 225, 227,
213, 229, 250 | ltletrd 10076 |
. . . . . . . 8
⊢ (𝜑 → 4 <
(exp‘(θ‘𝑀))) |
252 | | 4pos 10993 |
. . . . . . . . . 10
⊢ 0 <
4 |
253 | 252 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 4) |
254 | | ltdiv2 10788 |
. . . . . . . . 9
⊢ (((4
∈ ℝ ∧ 0 < 4) ∧ ((exp‘(θ‘𝑀)) ∈ ℝ ∧ 0 <
(exp‘(θ‘𝑀))) ∧ ((exp‘(θ‘𝐾)) ∈ ℝ ∧ 0 <
(exp‘(θ‘𝐾)))) → (4 <
(exp‘(θ‘𝑀)) ↔ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4))) |
255 | 225, 253,
213, 215, 212, 214, 254 | syl222anc 1334 |
. . . . . . . 8
⊢ (𝜑 → (4 <
(exp‘(θ‘𝑀)) ↔ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4))) |
256 | 251, 255 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) <
((exp‘(θ‘𝐾)) / 4)) |
257 | 26 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℝ) |
258 | | 2lt3 11072 |
. . . . . . . . . . . . . 14
⊢ 2 <
3 |
259 | 258 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 < 3) |
260 | 238, 103,
104, 240, 106 | letrd 10073 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 3 ≤ 𝐾) |
261 | 257, 238,
104, 259, 260 | ltletrd 10076 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 < 𝐾) |
262 | | chtub 24737 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℝ ∧ 2 <
𝐾) →
(θ‘𝐾) <
((log‘2) · ((2 · 𝐾) − 3))) |
263 | 104, 261,
262 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (θ‘𝐾) < ((log‘2) ·
((2 · 𝐾) −
3))) |
264 | | chtcl 24635 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℝ →
(θ‘𝐾) ∈
ℝ) |
265 | 104, 264 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (θ‘𝐾) ∈
ℝ) |
266 | | relogcl 24126 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
ℝ+ → (log‘2) ∈ ℝ) |
267 | 31, 266 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(log‘2) ∈ ℝ |
268 | 23 | nnzi 11278 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℤ |
269 | | zsubcl 11296 |
. . . . . . . . . . . . . . 15
⊢ (((2
· 𝐾) ∈ ℤ
∧ 3 ∈ ℤ) → ((2 · 𝐾) − 3) ∈
ℤ) |
270 | 78, 268, 269 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · 𝐾) − 3) ∈
ℤ) |
271 | 270 | zred 11358 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝐾) − 3) ∈
ℝ) |
272 | | remulcl 9900 |
. . . . . . . . . . . . 13
⊢
(((log‘2) ∈ ℝ ∧ ((2 · 𝐾) − 3) ∈ ℝ) →
((log‘2) · ((2 · 𝐾) − 3)) ∈
ℝ) |
273 | 267, 271,
272 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((log‘2) ·
((2 · 𝐾) − 3))
∈ ℝ) |
274 | | eflt 14686 |
. . . . . . . . . . . 12
⊢
(((θ‘𝐾)
∈ ℝ ∧ ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ) →
((θ‘𝐾) <
((log‘2) · ((2 · 𝐾) − 3)) ↔
(exp‘(θ‘𝐾)) < (exp‘((log‘2) ·
((2 · 𝐾) −
3))))) |
275 | 265, 273,
274 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → ((θ‘𝐾) < ((log‘2) ·
((2 · 𝐾) − 3))
↔ (exp‘(θ‘𝐾)) < (exp‘((log‘2) ·
((2 · 𝐾) −
3))))) |
276 | 263, 275 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 →
(exp‘(θ‘𝐾)) < (exp‘((log‘2) ·
((2 · 𝐾) −
3)))) |
277 | | reexplog 24145 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ+ ∧ ((2 · 𝐾) − 3) ∈ ℤ) →
(2↑((2 · 𝐾)
− 3)) = (exp‘(((2 · 𝐾) − 3) ·
(log‘2)))) |
278 | 31, 270, 277 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → (2↑((2 · 𝐾) − 3)) = (exp‘(((2
· 𝐾) − 3)
· (log‘2)))) |
279 | 270 | zcnd 11359 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝐾) − 3) ∈
ℂ) |
280 | 267 | recni 9931 |
. . . . . . . . . . . . 13
⊢
(log‘2) ∈ ℂ |
281 | | mulcom 9901 |
. . . . . . . . . . . . 13
⊢ ((((2
· 𝐾) − 3)
∈ ℂ ∧ (log‘2) ∈ ℂ) → (((2 · 𝐾) − 3) ·
(log‘2)) = ((log‘2) · ((2 · 𝐾) − 3))) |
282 | 279, 280,
281 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2 · 𝐾) − 3) ·
(log‘2)) = ((log‘2) · ((2 · 𝐾) − 3))) |
283 | 282 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 → (exp‘(((2 ·
𝐾) − 3) ·
(log‘2))) = (exp‘((log‘2) · ((2 · 𝐾) − 3)))) |
284 | 278, 283 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑((2 · 𝐾) − 3)) =
(exp‘((log‘2) · ((2 · 𝐾) − 3)))) |
285 | 276, 284 | breqtrrd 4611 |
. . . . . . . . 9
⊢ (𝜑 →
(exp‘(θ‘𝐾)) < (2↑((2 · 𝐾) − 3))) |
286 | | 3p2e5 11037 |
. . . . . . . . . . . . . . . 16
⊢ (3 + 2) =
5 |
287 | 286 | oveq1i 6559 |
. . . . . . . . . . . . . . 15
⊢ ((3 + 2)
− 2) = (5 − 2) |
288 | | 3cn 10972 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℂ |
289 | | 2cn 10968 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ |
290 | 288, 289 | pncan3oi 10176 |
. . . . . . . . . . . . . . 15
⊢ ((3 + 2)
− 2) = 3 |
291 | 287, 290 | eqtr3i 2634 |
. . . . . . . . . . . . . 14
⊢ (5
− 2) = 3 |
292 | 291 | oveq2i 6560 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝐾) − (5
− 2)) = ((2 · 𝐾) − 3) |
293 | 78 | zcnd 11359 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 · 𝐾) ∈
ℂ) |
294 | | 5cn 10977 |
. . . . . . . . . . . . . . 15
⊢ 5 ∈
ℂ |
295 | | subsub 10190 |
. . . . . . . . . . . . . . 15
⊢ (((2
· 𝐾) ∈ ℂ
∧ 5 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 · 𝐾) − (5 − 2)) = (((2
· 𝐾) − 5) +
2)) |
296 | 294, 289,
295 | mp3an23 1408 |
. . . . . . . . . . . . . 14
⊢ ((2
· 𝐾) ∈ ℂ
→ ((2 · 𝐾)
− (5 − 2)) = (((2 · 𝐾) − 5) + 2)) |
297 | 293, 296 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝐾) − (5 − 2)) = (((2
· 𝐾) − 5) +
2)) |
298 | 292, 297 | syl5eqr 2658 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝐾) − 3) = (((2 ·
𝐾) − 5) +
2)) |
299 | 298 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 →
(2↑𝑐((2 · 𝐾) − 3)) =
(2↑𝑐(((2 · 𝐾) − 5) + 2))) |
300 | | 2ne0 10990 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
301 | | cxpexpz 24213 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ ((2 · 𝐾) − 3) ∈ ℤ) →
(2↑𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3))) |
302 | 289, 300,
301 | mp3an12 1406 |
. . . . . . . . . . . 12
⊢ (((2
· 𝐾) − 3)
∈ ℤ → (2↑𝑐((2 · 𝐾) − 3)) = (2↑((2
· 𝐾) −
3))) |
303 | 270, 302 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 →
(2↑𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3))) |
304 | 81 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝐾) − 5) ∈
ℂ) |
305 | | 2cnne0 11119 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
306 | | cxpadd 24225 |
. . . . . . . . . . . . 13
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ ((2 · 𝐾) − 5) ∈ ℂ ∧ 2 ∈
ℂ) → (2↑𝑐(((2 · 𝐾) − 5) + 2)) =
((2↑𝑐((2 · 𝐾) − 5)) ·
(2↑𝑐2))) |
307 | 305, 289,
306 | mp3an13 1407 |
. . . . . . . . . . . 12
⊢ (((2
· 𝐾) − 5)
∈ ℂ → (2↑𝑐(((2 · 𝐾) − 5) + 2)) =
((2↑𝑐((2 · 𝐾) − 5)) ·
(2↑𝑐2))) |
308 | 304, 307 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 →
(2↑𝑐(((2 · 𝐾) − 5) + 2)) =
((2↑𝑐((2 · 𝐾) − 5)) ·
(2↑𝑐2))) |
309 | 299, 303,
308 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑((2 · 𝐾) − 3)) =
((2↑𝑐((2 · 𝐾) − 5)) ·
(2↑𝑐2))) |
310 | | 2nn0 11186 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
311 | | cxpexp 24214 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 2 ∈ ℕ0) →
(2↑𝑐2) = (2↑2)) |
312 | 289, 310,
311 | mp2an 704 |
. . . . . . . . . . . 12
⊢
(2↑𝑐2) = (2↑2) |
313 | | sq2 12822 |
. . . . . . . . . . . 12
⊢
(2↑2) = 4 |
314 | 312, 313 | eqtri 2632 |
. . . . . . . . . . 11
⊢
(2↑𝑐2) = 4 |
315 | 314 | oveq2i 6560 |
. . . . . . . . . 10
⊢
((2↑𝑐((2 · 𝐾) − 5)) ·
(2↑𝑐2)) = ((2↑𝑐((2 ·
𝐾) − 5)) ·
4) |
316 | 309, 315 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝜑 → (2↑((2 · 𝐾) − 3)) =
((2↑𝑐((2 · 𝐾) − 5)) · 4)) |
317 | 285, 316 | breqtrd 4609 |
. . . . . . . 8
⊢ (𝜑 →
(exp‘(θ‘𝐾)) < ((2↑𝑐((2
· 𝐾) − 5))
· 4)) |
318 | 224, 252 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (4 ∈
ℝ ∧ 0 < 4) |
319 | 318 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (4 ∈ ℝ ∧ 0
< 4)) |
320 | | ltdivmul2 10779 |
. . . . . . . . 9
⊢
(((exp‘(θ‘𝐾)) ∈ ℝ ∧
(2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ ∧ (4 ∈
ℝ ∧ 0 < 4)) → (((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2
· 𝐾) − 5))
↔ (exp‘(θ‘𝐾)) < ((2↑𝑐((2
· 𝐾) − 5))
· 4))) |
321 | 212, 85, 319, 320 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 →
(((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2
· 𝐾) − 5))
↔ (exp‘(θ‘𝐾)) < ((2↑𝑐((2
· 𝐾) − 5))
· 4))) |
322 | 317, 321 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2
· 𝐾) −
5))) |
323 | 119, 223,
85, 256, 322 | lttrd 10077 |
. . . . . 6
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) <
(2↑𝑐((2 · 𝐾) − 5))) |
324 | 102, 119,
85, 221, 323 | lelttrd 10074 |
. . . . 5
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2
· 𝐾) −
5))) |
325 | 97 | nnred 10912 |
. . . . . 6
⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℝ) |
326 | | nnre 10904 |
. . . . . . . 8
⊢ ((seq1(
· , 𝐹)‘𝑀) ∈ ℕ → (seq1(
· , 𝐹)‘𝑀) ∈
ℝ) |
327 | | nngt0 10926 |
. . . . . . . 8
⊢ ((seq1(
· , 𝐹)‘𝑀) ∈ ℕ → 0 <
(seq1( · , 𝐹)‘𝑀)) |
328 | 326, 327 | jca 553 |
. . . . . . 7
⊢ ((seq1(
· , 𝐹)‘𝑀) ∈ ℕ → ((seq1(
· , 𝐹)‘𝑀) ∈ ℝ ∧ 0 <
(seq1( · , 𝐹)‘𝑀))) |
329 | 70, 328 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1(
· , 𝐹)‘𝑀))) |
330 | | ltdivmul 10777 |
. . . . . 6
⊢ (((seq1(
· , 𝐹)‘𝐾) ∈ ℝ ∧
(2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ ∧ ((seq1(
· , 𝐹)‘𝑀) ∈ ℝ ∧ 0 <
(seq1( · , 𝐹)‘𝑀))) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2
· 𝐾) − 5))
↔ (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) −
5))))) |
331 | 325, 85, 329, 330 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2
· 𝐾) − 5))
↔ (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) −
5))))) |
332 | 324, 331 | mpbid 221 |
. . . 4
⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) −
5)))) |
333 | 87, 332 | eqbrtrrd 4607 |
. . 3
⊢ (𝜑 → ((2 · 𝑁)C𝑁) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) −
5)))) |
334 | 30, 85 | remulcld 9949 |
. . . 4
⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐((2 · 𝐾) − 5))) ∈
ℝ) |
335 | 3, 62, 55, 63, 64 | bposlem5 24813 |
. . . . 5
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) +
2))) |
336 | 71, 30, 84 | lemul1d 11791 |
. . . . 5
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
↔ ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) − 5))) ≤
(((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐((2 · 𝐾) − 5))))) |
337 | 335, 336 | mpbid 221 |
. . . 4
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) − 5)))
≤ (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐((2 · 𝐾) − 5)))) |
338 | 78 | zred 11358 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐾) ∈
ℝ) |
339 | 37 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 5 ∈
ℝ) |
340 | | flle 12462 |
. . . . . . . . . . 11
⊢ (((2
· 𝑁) / 3) ∈
ℝ → (⌊‘((2 · 𝑁) / 3)) ≤ ((2 · 𝑁) / 3)) |
341 | 74, 340 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (⌊‘((2
· 𝑁) / 3)) ≤ ((2
· 𝑁) /
3)) |
342 | 63, 341 | syl5eqbr 4618 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ≤ ((2 · 𝑁) / 3)) |
343 | | 2pos 10989 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
344 | 26, 343 | pm3.2i 470 |
. . . . . . . . . . 11
⊢ (2 ∈
ℝ ∧ 0 < 2) |
345 | 344 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (2 ∈ ℝ ∧ 0
< 2)) |
346 | | lemul2 10755 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℝ ∧ ((2
· 𝑁) / 3) ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐾 ≤ ((2 · 𝑁) / 3) ↔ (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3)))) |
347 | 104, 74, 345, 346 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ≤ ((2 · 𝑁) / 3) ↔ (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3)))) |
348 | 342, 347 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝐾) ≤ (2 · ((2 ·
𝑁) / 3))) |
349 | 18 | nncnd 10913 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
350 | | 3ne0 10992 |
. . . . . . . . . . . 12
⊢ 3 ≠
0 |
351 | 288, 350 | pm3.2i 470 |
. . . . . . . . . . 11
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
352 | | divass 10582 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ
∧ 3 ≠ 0)) → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3))) |
353 | 289, 351,
352 | mp3an13 1407 |
. . . . . . . . . 10
⊢ ((2
· 𝑁) ∈ ℂ
→ ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3))) |
354 | 349, 353 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · (2 ·
𝑁)) / 3) = (2 · ((2
· 𝑁) /
3))) |
355 | | 2t2e4 11054 |
. . . . . . . . . . . 12
⊢ (2
· 2) = 4 |
356 | 355 | oveq1i 6559 |
. . . . . . . . . . 11
⊢ ((2
· 2) · 𝑁) =
(4 · 𝑁) |
357 | 5 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
358 | | mulass 9903 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((2 · 2)
· 𝑁) = (2 ·
(2 · 𝑁))) |
359 | 289, 289,
358 | mp3an12 1406 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → ((2
· 2) · 𝑁) =
(2 · (2 · 𝑁))) |
360 | 357, 359 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 2) ·
𝑁) = (2 · (2
· 𝑁))) |
361 | 356, 360 | syl5reqr 2659 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · (2 ·
𝑁)) = (4 · 𝑁)) |
362 | 361 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · (2 ·
𝑁)) / 3) = ((4 ·
𝑁) / 3)) |
363 | 354, 362 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝜑 → (2 · ((2 ·
𝑁) / 3)) = ((4 ·
𝑁) / 3)) |
364 | 348, 363 | breqtrd 4609 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐾) ≤ ((4 · 𝑁) / 3)) |
365 | 338, 36, 339, 364 | lesub1dd 10522 |
. . . . . 6
⊢ (𝜑 → ((2 · 𝐾) − 5) ≤ (((4 ·
𝑁) / 3) −
5)) |
366 | | 1lt2 11071 |
. . . . . . . 8
⊢ 1 <
2 |
367 | 366 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 < 2) |
368 | 257, 367,
82, 39 | cxpled 24266 |
. . . . . 6
⊢ (𝜑 → (((2 · 𝐾) − 5) ≤ (((4 ·
𝑁) / 3) − 5) ↔
(2↑𝑐((2 · 𝐾) − 5)) ≤
(2↑𝑐(((4 · 𝑁) / 3) − 5)))) |
369 | 365, 368 | mpbid 221 |
. . . . 5
⊢ (𝜑 →
(2↑𝑐((2 · 𝐾) − 5)) ≤
(2↑𝑐(((4 · 𝑁) / 3) − 5))) |
370 | 85, 42, 29 | lemul2d 11792 |
. . . . 5
⊢ (𝜑 →
((2↑𝑐((2 · 𝐾) − 5)) ≤
(2↑𝑐(((4 · 𝑁) / 3) − 5)) ↔ (((2 ·
𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5))))) |
371 | 369, 370 | mpbid 221 |
. . . 4
⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5)))) |
372 | 86, 334, 43, 337, 371 | letrd 10073 |
. . 3
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) − 5)))
≤ (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5)))) |
373 | 15, 86, 43, 333, 372 | ltletrd 10076 |
. 2
⊢ (𝜑 → ((2 · 𝑁)C𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5)))) |
374 | 10, 15, 43, 54, 373 | lttrd 10077 |
1
⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5)))) |