MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bposlem5 Structured version   Visualization version   GIF version

Theorem bposlem5 27332
Description: Lemma for bpos 27337. Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)
Hypotheses
Ref Expression
bpos.1 (𝜑𝑁 ∈ (ℤ‘5))
bpos.2 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
bpos.3 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
bpos.4 𝐾 = (⌊‘((2 · 𝑁) / 3))
bpos.5 𝑀 = (⌊‘(√‘(2 · 𝑁)))
Assertion
Ref Expression
bposlem5 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
Distinct variable groups:   𝐹,𝑝   𝑛,𝑝,𝐾   𝑀,𝑝   𝑛,𝑁,𝑝   𝜑,𝑛,𝑝
Allowed substitution hints:   𝐹(𝑛)   𝑀(𝑛)

Proof of Theorem bposlem5
Dummy variables 𝑘 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bpos.3 . . . . . 6 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
2 id 22 . . . . . . . 8 (𝑛 ∈ ℙ → 𝑛 ∈ ℙ)
3 5nn 12352 . . . . . . . . . . 11 5 ∈ ℕ
4 bpos.1 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘5))
5 eluznn 12960 . . . . . . . . . . 11 ((5 ∈ ℕ ∧ 𝑁 ∈ (ℤ‘5)) → 𝑁 ∈ ℕ)
63, 4, 5sylancr 587 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
76nnnn0d 12587 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
8 fzctr 13680 . . . . . . . . 9 (𝑁 ∈ ℕ0𝑁 ∈ (0...(2 · 𝑁)))
9 bccl2 14362 . . . . . . . . 9 (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
107, 8, 93syl 18 . . . . . . . 8 (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ)
11 pccl 16887 . . . . . . . 8 ((𝑛 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
122, 10, 11syl2anr 597 . . . . . . 7 ((𝜑𝑛 ∈ ℙ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
1312ralrimiva 3146 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
141, 13pcmptcl 16929 . . . . 5 (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
1514simprd 495 . . . 4 (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ)
16 3nn 12345 . . . . 5 3 ∈ ℕ
17 bpos.5 . . . . . 6 𝑀 = (⌊‘(√‘(2 · 𝑁)))
18 2z 12649 . . . . . . . . . . 11 2 ∈ ℤ
196nnzd 12640 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
20 zmulcl 12666 . . . . . . . . . . 11 ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 · 𝑁) ∈ ℤ)
2118, 19, 20sylancr 587 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℤ)
2221zred 12722 . . . . . . . . 9 (𝜑 → (2 · 𝑁) ∈ ℝ)
23 2nn 12339 . . . . . . . . . . . 12 2 ∈ ℕ
24 nnmulcl 12290 . . . . . . . . . . . 12 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
2523, 6, 24sylancr 587 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) ∈ ℕ)
2625nnrpd 13075 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℝ+)
2726rpge0d 13081 . . . . . . . . 9 (𝜑 → 0 ≤ (2 · 𝑁))
2822, 27resqrtcld 15456 . . . . . . . 8 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
2928flcld 13838 . . . . . . 7 (𝜑 → (⌊‘(√‘(2 · 𝑁))) ∈ ℤ)
30 sqrt9 15312 . . . . . . . . 9 (√‘9) = 3
31 9re 12365 . . . . . . . . . . . 12 9 ∈ ℝ
3231a1i 11 . . . . . . . . . . 11 (𝜑 → 9 ∈ ℝ)
33 10re 12752 . . . . . . . . . . . 12 10 ∈ ℝ
3433a1i 11 . . . . . . . . . . 11 (𝜑10 ∈ ℝ)
35 lep1 12108 . . . . . . . . . . . . . 14 (9 ∈ ℝ → 9 ≤ (9 + 1))
3631, 35ax-mp 5 . . . . . . . . . . . . 13 9 ≤ (9 + 1)
37 9p1e10 12735 . . . . . . . . . . . . 13 (9 + 1) = 10
3836, 37breqtri 5168 . . . . . . . . . . . 12 9 ≤ 10
3938a1i 11 . . . . . . . . . . 11 (𝜑 → 9 ≤ 10)
40 5cn 12354 . . . . . . . . . . . . 13 5 ∈ ℂ
41 2cn 12341 . . . . . . . . . . . . 13 2 ∈ ℂ
42 5t2e10 12833 . . . . . . . . . . . . 13 (5 · 2) = 10
4340, 41, 42mulcomli 11270 . . . . . . . . . . . 12 (2 · 5) = 10
44 eluzle 12891 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘5) → 5 ≤ 𝑁)
454, 44syl 17 . . . . . . . . . . . . 13 (𝜑 → 5 ≤ 𝑁)
466nnred 12281 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
47 5re 12353 . . . . . . . . . . . . . . 15 5 ∈ ℝ
48 2re 12340 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
49 2pos 12369 . . . . . . . . . . . . . . . 16 0 < 2
5048, 49pm3.2i 470 . . . . . . . . . . . . . . 15 (2 ∈ ℝ ∧ 0 < 2)
51 lemul2 12120 . . . . . . . . . . . . . . 15 ((5 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2 · 𝑁)))
5247, 50, 51mp3an13 1454 . . . . . . . . . . . . . 14 (𝑁 ∈ ℝ → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2 · 𝑁)))
5346, 52syl 17 . . . . . . . . . . . . 13 (𝜑 → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2 · 𝑁)))
5445, 53mpbid 232 . . . . . . . . . . . 12 (𝜑 → (2 · 5) ≤ (2 · 𝑁))
5543, 54eqbrtrrid 5179 . . . . . . . . . . 11 (𝜑10 ≤ (2 · 𝑁))
5632, 34, 22, 39, 55letrd 11418 . . . . . . . . . 10 (𝜑 → 9 ≤ (2 · 𝑁))
57 0re 11263 . . . . . . . . . . . . 13 0 ∈ ℝ
58 9pos 12379 . . . . . . . . . . . . 13 0 < 9
5957, 31, 58ltleii 11384 . . . . . . . . . . . 12 0 ≤ 9
6031, 59pm3.2i 470 . . . . . . . . . . 11 (9 ∈ ℝ ∧ 0 ≤ 9)
6122, 27jca 511 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)))
62 sqrtle 15299 . . . . . . . . . . 11 (((9 ∈ ℝ ∧ 0 ≤ 9) ∧ ((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁))) → (9 ≤ (2 · 𝑁) ↔ (√‘9) ≤ (√‘(2 · 𝑁))))
6360, 61, 62sylancr 587 . . . . . . . . . 10 (𝜑 → (9 ≤ (2 · 𝑁) ↔ (√‘9) ≤ (√‘(2 · 𝑁))))
6456, 63mpbid 232 . . . . . . . . 9 (𝜑 → (√‘9) ≤ (√‘(2 · 𝑁)))
6530, 64eqbrtrrid 5179 . . . . . . . 8 (𝜑 → 3 ≤ (√‘(2 · 𝑁)))
66 3z 12650 . . . . . . . . 9 3 ∈ ℤ
67 flge 13845 . . . . . . . . 9 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℤ) → (3 ≤ (√‘(2 · 𝑁)) ↔ 3 ≤ (⌊‘(√‘(2 · 𝑁)))))
6828, 66, 67sylancl 586 . . . . . . . 8 (𝜑 → (3 ≤ (√‘(2 · 𝑁)) ↔ 3 ≤ (⌊‘(√‘(2 · 𝑁)))))
6965, 68mpbid 232 . . . . . . 7 (𝜑 → 3 ≤ (⌊‘(√‘(2 · 𝑁))))
7066eluz1i 12886 . . . . . . 7 ((⌊‘(√‘(2 · 𝑁))) ∈ (ℤ‘3) ↔ ((⌊‘(√‘(2 · 𝑁))) ∈ ℤ ∧ 3 ≤ (⌊‘(√‘(2 · 𝑁)))))
7129, 69, 70sylanbrc 583 . . . . . 6 (𝜑 → (⌊‘(√‘(2 · 𝑁))) ∈ (ℤ‘3))
7217, 71eqeltrid 2845 . . . . 5 (𝜑𝑀 ∈ (ℤ‘3))
73 eluznn 12960 . . . . 5 ((3 ∈ ℕ ∧ 𝑀 ∈ (ℤ‘3)) → 𝑀 ∈ ℕ)
7416, 72, 73sylancr 587 . . . 4 (𝜑𝑀 ∈ ℕ)
7515, 74ffvelcdmd 7105 . . 3 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℕ)
7675nnred 12281 . 2 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
7774nnred 12281 . . . . 5 (𝜑𝑀 ∈ ℝ)
78 ppicl 27174 . . . . 5 (𝑀 ∈ ℝ → (π𝑀) ∈ ℕ0)
7977, 78syl 17 . . . 4 (𝜑 → (π𝑀) ∈ ℕ0)
8025, 79nnexpcld 14284 . . 3 (𝜑 → ((2 · 𝑁)↑(π𝑀)) ∈ ℕ)
8180nnred 12281 . 2 (𝜑 → ((2 · 𝑁)↑(π𝑀)) ∈ ℝ)
82 nndivre 12307 . . . . 5 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
8328, 16, 82sylancl 586 . . . 4 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
84 readdcl 11238 . . . 4 ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
8583, 48, 84sylancl 586 . . 3 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
8622, 27, 85recxpcld 26765 . 2 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ)
87 fveq2 6906 . . . . . 6 (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
88 fveq2 6906 . . . . . . . 8 (𝑥 = 1 → (π𝑥) = (π‘1))
89 ppi1 27207 . . . . . . . 8 (π‘1) = 0
9088, 89eqtrdi 2793 . . . . . . 7 (𝑥 = 1 → (π𝑥) = 0)
9190oveq2d 7447 . . . . . 6 (𝑥 = 1 → ((2 · 𝑁)↑(π𝑥)) = ((2 · 𝑁)↑0))
9287, 91breq12d 5156 . . . . 5 (𝑥 = 1 → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥)) ↔ (seq1( · , 𝐹)‘1) ≤ ((2 · 𝑁)↑0)))
9392imbi2d 340 . . . 4 (𝑥 = 1 → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘1) ≤ ((2 · 𝑁)↑0))))
94 fveq2 6906 . . . . . 6 (𝑥 = 𝑘 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑘))
95 fveq2 6906 . . . . . . 7 (𝑥 = 𝑘 → (π𝑥) = (π𝑘))
9695oveq2d 7447 . . . . . 6 (𝑥 = 𝑘 → ((2 · 𝑁)↑(π𝑥)) = ((2 · 𝑁)↑(π𝑘)))
9794, 96breq12d 5156 . . . . 5 (𝑥 = 𝑘 → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥)) ↔ (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘))))
9897imbi2d 340 . . . 4 (𝑥 = 𝑘 → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)))))
99 fveq2 6906 . . . . . 6 (𝑥 = (𝑘 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑘 + 1)))
100 fveq2 6906 . . . . . . 7 (𝑥 = (𝑘 + 1) → (π𝑥) = (π‘(𝑘 + 1)))
101100oveq2d 7447 . . . . . 6 (𝑥 = (𝑘 + 1) → ((2 · 𝑁)↑(π𝑥)) = ((2 · 𝑁)↑(π‘(𝑘 + 1))))
10299, 101breq12d 5156 . . . . 5 (𝑥 = (𝑘 + 1) → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥)) ↔ (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
103102imbi2d 340 . . . 4 (𝑥 = (𝑘 + 1) → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))))
104 fveq2 6906 . . . . . 6 (𝑥 = 𝑀 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑀))
105 fveq2 6906 . . . . . . 7 (𝑥 = 𝑀 → (π𝑥) = (π𝑀))
106105oveq2d 7447 . . . . . 6 (𝑥 = 𝑀 → ((2 · 𝑁)↑(π𝑥)) = ((2 · 𝑁)↑(π𝑀)))
107104, 106breq12d 5156 . . . . 5 (𝑥 = 𝑀 → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥)) ↔ (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π𝑀))))
108107imbi2d 340 . . . 4 (𝑥 = 𝑀 → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π𝑀)))))
109 1z 12647 . . . . . . . 8 1 ∈ ℤ
110 seq1 14055 . . . . . . . 8 (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
111109, 110ax-mp 5 . . . . . . 7 (seq1( · , 𝐹)‘1) = (𝐹‘1)
112 1nn 12277 . . . . . . . 8 1 ∈ ℕ
113 1nprm 16716 . . . . . . . . . . 11 ¬ 1 ∈ ℙ
114 eleq1 2829 . . . . . . . . . . 11 (𝑛 = 1 → (𝑛 ∈ ℙ ↔ 1 ∈ ℙ))
115113, 114mtbiri 327 . . . . . . . . . 10 (𝑛 = 1 → ¬ 𝑛 ∈ ℙ)
116115iffalsed 4536 . . . . . . . . 9 (𝑛 = 1 → if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1) = 1)
117 1ex 11257 . . . . . . . . 9 1 ∈ V
118116, 1, 117fvmpt 7016 . . . . . . . 8 (1 ∈ ℕ → (𝐹‘1) = 1)
119112, 118ax-mp 5 . . . . . . 7 (𝐹‘1) = 1
120111, 119eqtri 2765 . . . . . 6 (seq1( · , 𝐹)‘1) = 1
121 1le1 11891 . . . . . 6 1 ≤ 1
122120, 121eqbrtri 5164 . . . . 5 (seq1( · , 𝐹)‘1) ≤ 1
12321zcnd 12723 . . . . . 6 (𝜑 → (2 · 𝑁) ∈ ℂ)
124123exp0d 14180 . . . . 5 (𝜑 → ((2 · 𝑁)↑0) = 1)
125122, 124breqtrrid 5181 . . . 4 (𝜑 → (seq1( · , 𝐹)‘1) ≤ ((2 · 𝑁)↑0))
12615ffvelcdmda 7104 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘𝑘) ∈ ℕ)
127126nnred 12281 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘𝑘) ∈ ℝ)
128127adantr 480 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘𝑘) ∈ ℝ)
12925ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (2 · 𝑁) ∈ ℕ)
130 nnre 12273 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
131130ad2antlr 727 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → 𝑘 ∈ ℝ)
132 ppicl 27174 . . . . . . . . . . . . 13 (𝑘 ∈ ℝ → (π𝑘) ∈ ℕ0)
133131, 132syl 17 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (π𝑘) ∈ ℕ0)
134129, 133nnexpcld 14284 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π𝑘)) ∈ ℕ)
135134nnred 12281 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π𝑘)) ∈ ℝ)
136 nnre 12273 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℕ → (2 · 𝑁) ∈ ℝ)
137 nngt0 12297 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℕ → 0 < (2 · 𝑁))
138136, 137jca 511 . . . . . . . . . . . 12 ((2 · 𝑁) ∈ ℕ → ((2 · 𝑁) ∈ ℝ ∧ 0 < (2 · 𝑁)))
13925, 138syl 17 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ 0 < (2 · 𝑁)))
140139ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁) ∈ ℝ ∧ 0 < (2 · 𝑁)))
141 lemul1 12119 . . . . . . . . . 10 (((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ ((2 · 𝑁)↑(π𝑘)) ∈ ℝ ∧ ((2 · 𝑁) ∈ ℝ ∧ 0 < (2 · 𝑁))) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁))))
142128, 135, 140, 141syl3anc 1373 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁))))
143 nnz 12634 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
144143adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
145 ppiprm 27194 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ (𝑘 + 1) ∈ ℙ) → (π‘(𝑘 + 1)) = ((π𝑘) + 1))
146144, 145sylan 580 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (π‘(𝑘 + 1)) = ((π𝑘) + 1))
147146oveq2d 7447 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) = ((2 · 𝑁)↑((π𝑘) + 1)))
148123ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (2 · 𝑁) ∈ ℂ)
149148, 133expp1d 14187 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑((π𝑘) + 1)) = (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁)))
150147, 149eqtrd 2777 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) = (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁)))
151150breq2d 5155 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁))))
152142, 151bitr4d 282 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
153 simpr 484 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
154 nnuz 12921 . . . . . . . . . . . . 13 ℕ = (ℤ‘1)
155153, 154eleqtrdi 2851 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
156 seqp1 14057 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ‘1) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))
157155, 156syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))
158157adantr 480 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))
159 peano2nn 12278 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
160159adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
161 eleq1 2829 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘 + 1) → (𝑛 ∈ ℙ ↔ (𝑘 + 1) ∈ ℙ))
162 id 22 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1))
163 oveq1 7438 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑘 + 1) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = ((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁)))
164162, 163oveq12d 7449 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘 + 1) → (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))) = ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))))
165161, 164ifbieq1d 4550 . . . . . . . . . . . . . . 15 (𝑛 = (𝑘 + 1) → if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1))
166 ovex 7464 . . . . . . . . . . . . . . . 16 ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) ∈ V
167166, 117ifex 4576 . . . . . . . . . . . . . . 15 if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1) ∈ V
168165, 1, 167fvmpt 7016 . . . . . . . . . . . . . 14 ((𝑘 + 1) ∈ ℕ → (𝐹‘(𝑘 + 1)) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1))
169160, 168syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1))
170 iftrue 4531 . . . . . . . . . . . . 13 ((𝑘 + 1) ∈ ℙ → if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1) = ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))))
171169, 170sylan9eq 2797 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) = ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))))
1726adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑁 ∈ ℕ)
173 bposlem1 27328 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ (𝑘 + 1) ∈ ℙ) → ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
174172, 173sylan 580 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
175171, 174eqbrtrd 5165 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) ≤ (2 · 𝑁))
17614simpld 494 . . . . . . . . . . . . . . 15 (𝜑𝐹:ℕ⟶ℕ)
177 ffvelcdm 7101 . . . . . . . . . . . . . . 15 ((𝐹:ℕ⟶ℕ ∧ (𝑘 + 1) ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℕ)
178176, 159, 177syl2an 596 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℕ)
179178nnred 12281 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℝ)
180179adantr 480 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) ∈ ℝ)
18122ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (2 · 𝑁) ∈ ℝ)
182 nnre 12273 . . . . . . . . . . . . . . 15 ((seq1( · , 𝐹)‘𝑘) ∈ ℕ → (seq1( · , 𝐹)‘𝑘) ∈ ℝ)
183 nngt0 12297 . . . . . . . . . . . . . . 15 ((seq1( · , 𝐹)‘𝑘) ∈ ℕ → 0 < (seq1( · , 𝐹)‘𝑘))
184182, 183jca 511 . . . . . . . . . . . . . 14 ((seq1( · , 𝐹)‘𝑘) ∈ ℕ → ((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑘)))
185126, 184syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑘)))
186185adantr 480 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑘)))
187 lemul2 12120 . . . . . . . . . . . 12 (((𝐹‘(𝑘 + 1)) ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ ((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑘))) → ((𝐹‘(𝑘 + 1)) ≤ (2 · 𝑁) ↔ ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁))))
188180, 181, 186, 187syl3anc 1373 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((𝐹‘(𝑘 + 1)) ≤ (2 · 𝑁) ↔ ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁))))
189175, 188mpbid 232 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)))
190158, 189eqbrtrd 5165 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)))
191 ffvelcdm 7101 . . . . . . . . . . . . 13 ((seq1( · , 𝐹):ℕ⟶ℕ ∧ (𝑘 + 1) ∈ ℕ) → (seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℕ)
19215, 159, 191syl2an 596 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℕ)
193192nnred 12281 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℝ)
19425adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
195126, 194nnmulcld 12319 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∈ ℕ)
196195nnred 12281 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∈ ℝ)
197160nnred 12281 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
198 ppicl 27174 . . . . . . . . . . . . . 14 ((𝑘 + 1) ∈ ℝ → (π‘(𝑘 + 1)) ∈ ℕ0)
199197, 198syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (π‘(𝑘 + 1)) ∈ ℕ0)
200194, 199nnexpcld 14284 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) ∈ ℕ)
201200nnred 12281 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) ∈ ℝ)
202 letr 11355 . . . . . . . . . . 11 (((seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℝ ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∈ ℝ ∧ ((2 · 𝑁)↑(π‘(𝑘 + 1))) ∈ ℝ) → (((seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
203193, 196, 201, 202syl3anc 1373 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (((seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
204203adantr 480 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (((seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
205190, 204mpand 695 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
206152, 205sylbid 240 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
207157adantr 480 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))
208 iffalse 4534 . . . . . . . . . . . 12 (¬ (𝑘 + 1) ∈ ℙ → if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1) = 1)
209169, 208sylan9eq 2797 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) = 1)
210209oveq2d 7447 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) = ((seq1( · , 𝐹)‘𝑘) · 1))
211126adantr 480 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘𝑘) ∈ ℕ)
212211nncnd 12282 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘𝑘) ∈ ℂ)
213212mulridd 11278 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) · 1) = (seq1( · , 𝐹)‘𝑘))
214207, 210, 2133eqtrd 2781 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘(𝑘 + 1)) = (seq1( · , 𝐹)‘𝑘))
215 ppinprm 27195 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ ¬ (𝑘 + 1) ∈ ℙ) → (π‘(𝑘 + 1)) = (π𝑘))
216144, 215sylan 580 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (π‘(𝑘 + 1)) = (π𝑘))
217216oveq2d 7447 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) = ((2 · 𝑁)↑(π𝑘)))
218214, 217breq12d 5156 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))) ↔ (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘))))
219218biimprd 248 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
220206, 219pm2.61dan 813 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
221220expcom 413 . . . . 5 (𝑘 ∈ ℕ → (𝜑 → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))))
222221a2d 29 . . . 4 (𝑘 ∈ ℕ → ((𝜑 → (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘))) → (𝜑 → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))))
22393, 98, 103, 108, 125, 222nnind 12284 . . 3 (𝑀 ∈ ℕ → (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π𝑀))))
22474, 223mpcom 38 . 2 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π𝑀)))
225 cxpexp 26710 . . . 4 (((2 · 𝑁) ∈ ℂ ∧ (π𝑀) ∈ ℕ0) → ((2 · 𝑁)↑𝑐(π𝑀)) = ((2 · 𝑁)↑(π𝑀)))
226123, 79, 225syl2anc 584 . . 3 (𝜑 → ((2 · 𝑁)↑𝑐(π𝑀)) = ((2 · 𝑁)↑(π𝑀)))
22779nn0red 12588 . . . . 5 (𝜑 → (π𝑀) ∈ ℝ)
228 nndivre 12307 . . . . . . 7 ((𝑀 ∈ ℝ ∧ 3 ∈ ℕ) → (𝑀 / 3) ∈ ℝ)
22977, 16, 228sylancl 586 . . . . . 6 (𝜑 → (𝑀 / 3) ∈ ℝ)
230 readdcl 11238 . . . . . 6 (((𝑀 / 3) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑀 / 3) + 2) ∈ ℝ)
231229, 48, 230sylancl 586 . . . . 5 (𝜑 → ((𝑀 / 3) + 2) ∈ ℝ)
23274nnnn0d 12587 . . . . . . 7 (𝜑𝑀 ∈ ℕ0)
233232nn0ge0d 12590 . . . . . 6 (𝜑 → 0 ≤ 𝑀)
234 ppiub 27248 . . . . . 6 ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (π𝑀) ≤ ((𝑀 / 3) + 2))
23577, 233, 234syl2anc 584 . . . . 5 (𝜑 → (π𝑀) ≤ ((𝑀 / 3) + 2))
23648a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℝ)
237 flle 13839 . . . . . . . . 9 ((√‘(2 · 𝑁)) ∈ ℝ → (⌊‘(√‘(2 · 𝑁))) ≤ (√‘(2 · 𝑁)))
23828, 237syl 17 . . . . . . . 8 (𝜑 → (⌊‘(√‘(2 · 𝑁))) ≤ (√‘(2 · 𝑁)))
23917, 238eqbrtrid 5178 . . . . . . 7 (𝜑𝑀 ≤ (√‘(2 · 𝑁)))
240 3re 12346 . . . . . . . . . 10 3 ∈ ℝ
241 3pos 12371 . . . . . . . . . 10 0 < 3
242240, 241pm3.2i 470 . . . . . . . . 9 (3 ∈ ℝ ∧ 0 < 3)
243242a1i 11 . . . . . . . 8 (𝜑 → (3 ∈ ℝ ∧ 0 < 3))
244 lediv1 12133 . . . . . . . 8 ((𝑀 ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (𝑀 ≤ (√‘(2 · 𝑁)) ↔ (𝑀 / 3) ≤ ((√‘(2 · 𝑁)) / 3)))
24577, 28, 243, 244syl3anc 1373 . . . . . . 7 (𝜑 → (𝑀 ≤ (√‘(2 · 𝑁)) ↔ (𝑀 / 3) ≤ ((√‘(2 · 𝑁)) / 3)))
246239, 245mpbid 232 . . . . . 6 (𝜑 → (𝑀 / 3) ≤ ((√‘(2 · 𝑁)) / 3))
247229, 83, 236, 246leadd1dd 11877 . . . . 5 (𝜑 → ((𝑀 / 3) + 2) ≤ (((√‘(2 · 𝑁)) / 3) + 2))
248227, 231, 85, 235, 247letrd 11418 . . . 4 (𝜑 → (π𝑀) ≤ (((√‘(2 · 𝑁)) / 3) + 2))
249 2t1e2 12429 . . . . . . . 8 (2 · 1) = 2
2506nnge1d 12314 . . . . . . . . 9 (𝜑 → 1 ≤ 𝑁)
251 1re 11261 . . . . . . . . . . 11 1 ∈ ℝ
252 lemul2 12120 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
253251, 50, 252mp3an13 1454 . . . . . . . . . 10 (𝑁 ∈ ℝ → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
25446, 253syl 17 . . . . . . . . 9 (𝜑 → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
255250, 254mpbid 232 . . . . . . . 8 (𝜑 → (2 · 1) ≤ (2 · 𝑁))
256249, 255eqbrtrrid 5179 . . . . . . 7 (𝜑 → 2 ≤ (2 · 𝑁))
25718eluz1i 12886 . . . . . . 7 ((2 · 𝑁) ∈ (ℤ‘2) ↔ ((2 · 𝑁) ∈ ℤ ∧ 2 ≤ (2 · 𝑁)))
25821, 256, 257sylanbrc 583 . . . . . 6 (𝜑 → (2 · 𝑁) ∈ (ℤ‘2))
259 eluz2gt1 12962 . . . . . 6 ((2 · 𝑁) ∈ (ℤ‘2) → 1 < (2 · 𝑁))
260258, 259syl 17 . . . . 5 (𝜑 → 1 < (2 · 𝑁))
26122, 260, 227, 85cxpled 26762 . . . 4 (𝜑 → ((π𝑀) ≤ (((√‘(2 · 𝑁)) / 3) + 2) ↔ ((2 · 𝑁)↑𝑐(π𝑀)) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2))))
262248, 261mpbid 232 . . 3 (𝜑 → ((2 · 𝑁)↑𝑐(π𝑀)) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
263226, 262eqbrtrrd 5167 . 2 (𝜑 → ((2 · 𝑁)↑(π𝑀)) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
26476, 81, 86, 224, 263letrd 11418 1 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wrex 3070  ifcif 4525   class class class wbr 5143  cmpt 5225  wf 6557  cfv 6561  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295  cle 11296   / cdiv 11920  cn 12266  2c2 12321  3c3 12322  5c5 12324  9c9 12328  0cn0 12526  cz 12613  cdc 12733  cuz 12878  ...cfz 13547  cfl 13830  seqcseq 14042  cexp 14102  Ccbc 14341  csqrt 15272  cprime 16708   pCnt cpc 16874  𝑐ccxp 26597  πcppi 27137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-xnn0 12600  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ioc 13392  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-shft 15106  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-limsup 15507  df-clim 15524  df-rlim 15525  df-sum 15723  df-ef 16103  df-sin 16105  df-cos 16106  df-pi 16108  df-dvds 16291  df-gcd 16532  df-prm 16709  df-pc 16875  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-fbas 21361  df-fg 21362  df-cnfld 21365  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144  df-perf 23145  df-cn 23235  df-cnp 23236  df-haus 23323  df-tx 23570  df-hmeo 23763  df-fil 23854  df-fm 23946  df-flim 23947  df-flf 23948  df-xms 24330  df-ms 24331  df-tms 24332  df-cncf 24904  df-limc 25901  df-dv 25902  df-log 26598  df-cxp 26599  df-ppi 27143
This theorem is referenced by:  bposlem6  27333
  Copyright terms: Public domain W3C validator