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

Theorem bposlem5 25850
Description: Lemma for bpos 25855. 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 11701 . . . . . . . . . . 11 5 ∈ ℕ
4 bpos.1 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘5))
5 eluznn 12296 . . . . . . . . . . 11 ((5 ∈ ℕ ∧ 𝑁 ∈ (ℤ‘5)) → 𝑁 ∈ ℕ)
63, 4, 5sylancr 590 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
76nnnn0d 11933 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
8 fzctr 13002 . . . . . . . . 9 (𝑁 ∈ ℕ0𝑁 ∈ (0...(2 · 𝑁)))
9 bccl2 13667 . . . . . . . . 9 (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
107, 8, 93syl 18 . . . . . . . 8 (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ)
11 pccl 16163 . . . . . . . 8 ((𝑛 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
122, 10, 11syl2anr 599 . . . . . . 7 ((𝜑𝑛 ∈ ℙ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
1312ralrimiva 3170 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
141, 13pcmptcl 16204 . . . . 5 (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
1514simprd 499 . . . 4 (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ)
16 3nn 11694 . . . . 5 3 ∈ ℕ
17 bpos.5 . . . . . 6 𝑀 = (⌊‘(√‘(2 · 𝑁)))
18 2z 11992 . . . . . . . . . . 11 2 ∈ ℤ
196nnzd 12064 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
20 zmulcl 12009 . . . . . . . . . . 11 ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 · 𝑁) ∈ ℤ)
2118, 19, 20sylancr 590 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℤ)
2221zred 12065 . . . . . . . . 9 (𝜑 → (2 · 𝑁) ∈ ℝ)
23 2nn 11688 . . . . . . . . . . . 12 2 ∈ ℕ
24 nnmulcl 11639 . . . . . . . . . . . 12 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
2523, 6, 24sylancr 590 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) ∈ ℕ)
2625nnrpd 12407 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℝ+)
2726rpge0d 12413 . . . . . . . . 9 (𝜑 → 0 ≤ (2 · 𝑁))
2822, 27resqrtcld 14756 . . . . . . . 8 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
2928flcld 13151 . . . . . . 7 (𝜑 → (⌊‘(√‘(2 · 𝑁))) ∈ ℤ)
30 sqrt9 14612 . . . . . . . . 9 (√‘9) = 3
31 9re 11714 . . . . . . . . . . . 12 9 ∈ ℝ
3231a1i 11 . . . . . . . . . . 11 (𝜑 → 9 ∈ ℝ)
33 10re 12095 . . . . . . . . . . . 12 10 ∈ ℝ
3433a1i 11 . . . . . . . . . . 11 (𝜑10 ∈ ℝ)
35 lep1 11458 . . . . . . . . . . . . . 14 (9 ∈ ℝ → 9 ≤ (9 + 1))
3631, 35ax-mp 5 . . . . . . . . . . . . 13 9 ≤ (9 + 1)
37 9p1e10 12078 . . . . . . . . . . . . 13 (9 + 1) = 10
3836, 37breqtri 5064 . . . . . . . . . . . 12 9 ≤ 10
3938a1i 11 . . . . . . . . . . 11 (𝜑 → 9 ≤ 10)
40 5cn 11703 . . . . . . . . . . . . 13 5 ∈ ℂ
41 2cn 11690 . . . . . . . . . . . . 13 2 ∈ ℂ
42 5t2e10 12176 . . . . . . . . . . . . 13 (5 · 2) = 10
4340, 41, 42mulcomli 10627 . . . . . . . . . . . 12 (2 · 5) = 10
44 eluzle 12234 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘5) → 5 ≤ 𝑁)
454, 44syl 17 . . . . . . . . . . . . 13 (𝜑 → 5 ≤ 𝑁)
466nnred 11630 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
47 5re 11702 . . . . . . . . . . . . . . 15 5 ∈ ℝ
48 2re 11689 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
49 2pos 11718 . . . . . . . . . . . . . . . 16 0 < 2
5048, 49pm3.2i 474 . . . . . . . . . . . . . . 15 (2 ∈ ℝ ∧ 0 < 2)
51 lemul2 11470 . . . . . . . . . . . . . . 15 ((5 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2 · 𝑁)))
5247, 50, 51mp3an13 1449 . . . . . . . . . . . . . 14 (𝑁 ∈ ℝ → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2 · 𝑁)))
5346, 52syl 17 . . . . . . . . . . . . 13 (𝜑 → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2 · 𝑁)))
5445, 53mpbid 235 . . . . . . . . . . . 12 (𝜑 → (2 · 5) ≤ (2 · 𝑁))
5543, 54eqbrtrrid 5075 . . . . . . . . . . 11 (𝜑10 ≤ (2 · 𝑁))
5632, 34, 22, 39, 55letrd 10774 . . . . . . . . . 10 (𝜑 → 9 ≤ (2 · 𝑁))
57 0re 10620 . . . . . . . . . . . . 13 0 ∈ ℝ
58 9pos 11728 . . . . . . . . . . . . 13 0 < 9
5957, 31, 58ltleii 10740 . . . . . . . . . . . 12 0 ≤ 9
6031, 59pm3.2i 474 . . . . . . . . . . 11 (9 ∈ ℝ ∧ 0 ≤ 9)
6122, 27jca 515 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)))
62 sqrtle 14599 . . . . . . . . . . 11 (((9 ∈ ℝ ∧ 0 ≤ 9) ∧ ((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁))) → (9 ≤ (2 · 𝑁) ↔ (√‘9) ≤ (√‘(2 · 𝑁))))
6360, 61, 62sylancr 590 . . . . . . . . . 10 (𝜑 → (9 ≤ (2 · 𝑁) ↔ (√‘9) ≤ (√‘(2 · 𝑁))))
6456, 63mpbid 235 . . . . . . . . 9 (𝜑 → (√‘9) ≤ (√‘(2 · 𝑁)))
6530, 64eqbrtrrid 5075 . . . . . . . 8 (𝜑 → 3 ≤ (√‘(2 · 𝑁)))
66 3z 11993 . . . . . . . . 9 3 ∈ ℤ
67 flge 13158 . . . . . . . . 9 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℤ) → (3 ≤ (√‘(2 · 𝑁)) ↔ 3 ≤ (⌊‘(√‘(2 · 𝑁)))))
6828, 66, 67sylancl 589 . . . . . . . 8 (𝜑 → (3 ≤ (√‘(2 · 𝑁)) ↔ 3 ≤ (⌊‘(√‘(2 · 𝑁)))))
6965, 68mpbid 235 . . . . . . 7 (𝜑 → 3 ≤ (⌊‘(√‘(2 · 𝑁))))
7066eluz1i 12229 . . . . . . 7 ((⌊‘(√‘(2 · 𝑁))) ∈ (ℤ‘3) ↔ ((⌊‘(√‘(2 · 𝑁))) ∈ ℤ ∧ 3 ≤ (⌊‘(√‘(2 · 𝑁)))))
7129, 69, 70sylanbrc 586 . . . . . 6 (𝜑 → (⌊‘(√‘(2 · 𝑁))) ∈ (ℤ‘3))
7217, 71eqeltrid 2916 . . . . 5 (𝜑𝑀 ∈ (ℤ‘3))
73 eluznn 12296 . . . . 5 ((3 ∈ ℕ ∧ 𝑀 ∈ (ℤ‘3)) → 𝑀 ∈ ℕ)
7416, 72, 73sylancr 590 . . . 4 (𝜑𝑀 ∈ ℕ)
7515, 74ffvelrnd 6825 . . 3 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℕ)
7675nnred 11630 . 2 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
7774nnred 11630 . . . . 5 (𝜑𝑀 ∈ ℝ)
78 ppicl 25694 . . . . 5 (𝑀 ∈ ℝ → (π𝑀) ∈ ℕ0)
7977, 78syl 17 . . . 4 (𝜑 → (π𝑀) ∈ ℕ0)
8025, 79nnexpcld 13590 . . 3 (𝜑 → ((2 · 𝑁)↑(π𝑀)) ∈ ℕ)
8180nnred 11630 . 2 (𝜑 → ((2 · 𝑁)↑(π𝑀)) ∈ ℝ)
82 nndivre 11656 . . . . 5 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
8328, 16, 82sylancl 589 . . . 4 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
84 readdcl 10597 . . . 4 ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
8583, 48, 84sylancl 589 . . 3 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
8622, 27, 85recxpcld 25292 . 2 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ)
87 fveq2 6643 . . . . . 6 (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
88 fveq2 6643 . . . . . . . 8 (𝑥 = 1 → (π𝑥) = (π‘1))
89 ppi1 25727 . . . . . . . 8 (π‘1) = 0
9088, 89syl6eq 2872 . . . . . . 7 (𝑥 = 1 → (π𝑥) = 0)
9190oveq2d 7146 . . . . . 6 (𝑥 = 1 → ((2 · 𝑁)↑(π𝑥)) = ((2 · 𝑁)↑0))
9287, 91breq12d 5052 . . . . 5 (𝑥 = 1 → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥)) ↔ (seq1( · , 𝐹)‘1) ≤ ((2 · 𝑁)↑0)))
9392imbi2d 344 . . . 4 (𝑥 = 1 → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘1) ≤ ((2 · 𝑁)↑0))))
94 fveq2 6643 . . . . . 6 (𝑥 = 𝑘 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑘))
95 fveq2 6643 . . . . . . 7 (𝑥 = 𝑘 → (π𝑥) = (π𝑘))
9695oveq2d 7146 . . . . . 6 (𝑥 = 𝑘 → ((2 · 𝑁)↑(π𝑥)) = ((2 · 𝑁)↑(π𝑘)))
9794, 96breq12d 5052 . . . . 5 (𝑥 = 𝑘 → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥)) ↔ (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘))))
9897imbi2d 344 . . . 4 (𝑥 = 𝑘 → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)))))
99 fveq2 6643 . . . . . 6 (𝑥 = (𝑘 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑘 + 1)))
100 fveq2 6643 . . . . . . 7 (𝑥 = (𝑘 + 1) → (π𝑥) = (π‘(𝑘 + 1)))
101100oveq2d 7146 . . . . . 6 (𝑥 = (𝑘 + 1) → ((2 · 𝑁)↑(π𝑥)) = ((2 · 𝑁)↑(π‘(𝑘 + 1))))
10299, 101breq12d 5052 . . . . 5 (𝑥 = (𝑘 + 1) → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥)) ↔ (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
103102imbi2d 344 . . . 4 (𝑥 = (𝑘 + 1) → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))))
104 fveq2 6643 . . . . . 6 (𝑥 = 𝑀 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑀))
105 fveq2 6643 . . . . . . 7 (𝑥 = 𝑀 → (π𝑥) = (π𝑀))
106105oveq2d 7146 . . . . . 6 (𝑥 = 𝑀 → ((2 · 𝑁)↑(π𝑥)) = ((2 · 𝑁)↑(π𝑀)))
107104, 106breq12d 5052 . . . . 5 (𝑥 = 𝑀 → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥)) ↔ (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π𝑀))))
108107imbi2d 344 . . . 4 (𝑥 = 𝑀 → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π𝑀)))))
109 1z 11990 . . . . . . . 8 1 ∈ ℤ
110 seq1 13365 . . . . . . . 8 (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
111109, 110ax-mp 5 . . . . . . 7 (seq1( · , 𝐹)‘1) = (𝐹‘1)
112 1nn 11626 . . . . . . . 8 1 ∈ ℕ
113 1nprm 16000 . . . . . . . . . . 11 ¬ 1 ∈ ℙ
114 eleq1 2899 . . . . . . . . . . 11 (𝑛 = 1 → (𝑛 ∈ ℙ ↔ 1 ∈ ℙ))
115113, 114mtbiri 330 . . . . . . . . . 10 (𝑛 = 1 → ¬ 𝑛 ∈ ℙ)
116115iffalsed 4451 . . . . . . . . 9 (𝑛 = 1 → if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1) = 1)
117 1ex 10614 . . . . . . . . 9 1 ∈ V
118116, 1, 117fvmpt 6741 . . . . . . . 8 (1 ∈ ℕ → (𝐹‘1) = 1)
119112, 118ax-mp 5 . . . . . . 7 (𝐹‘1) = 1
120111, 119eqtri 2844 . . . . . 6 (seq1( · , 𝐹)‘1) = 1
121 1le1 11245 . . . . . 6 1 ≤ 1
122120, 121eqbrtri 5060 . . . . 5 (seq1( · , 𝐹)‘1) ≤ 1
12321zcnd 12066 . . . . . 6 (𝜑 → (2 · 𝑁) ∈ ℂ)
124123exp0d 13488 . . . . 5 (𝜑 → ((2 · 𝑁)↑0) = 1)
125122, 124breqtrrid 5077 . . . 4 (𝜑 → (seq1( · , 𝐹)‘1) ≤ ((2 · 𝑁)↑0))
12615ffvelrnda 6824 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘𝑘) ∈ ℕ)
127126nnred 11630 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘𝑘) ∈ ℝ)
128127adantr 484 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘𝑘) ∈ ℝ)
12925ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (2 · 𝑁) ∈ ℕ)
130 nnre 11622 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
131130ad2antlr 726 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → 𝑘 ∈ ℝ)
132 ppicl 25694 . . . . . . . . . . . . 13 (𝑘 ∈ ℝ → (π𝑘) ∈ ℕ0)
133131, 132syl 17 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (π𝑘) ∈ ℕ0)
134129, 133nnexpcld 13590 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π𝑘)) ∈ ℕ)
135134nnred 11630 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π𝑘)) ∈ ℝ)
136 nnre 11622 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℕ → (2 · 𝑁) ∈ ℝ)
137 nngt0 11646 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℕ → 0 < (2 · 𝑁))
138136, 137jca 515 . . . . . . . . . . . 12 ((2 · 𝑁) ∈ ℕ → ((2 · 𝑁) ∈ ℝ ∧ 0 < (2 · 𝑁)))
13925, 138syl 17 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ 0 < (2 · 𝑁)))
140139ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁) ∈ ℝ ∧ 0 < (2 · 𝑁)))
141 lemul1 11469 . . . . . . . . . 10 (((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ ((2 · 𝑁)↑(π𝑘)) ∈ ℝ ∧ ((2 · 𝑁) ∈ ℝ ∧ 0 < (2 · 𝑁))) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁))))
142128, 135, 140, 141syl3anc 1368 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁))))
143 nnz 11982 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
144143adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
145 ppiprm 25714 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ (𝑘 + 1) ∈ ℙ) → (π‘(𝑘 + 1)) = ((π𝑘) + 1))
146144, 145sylan 583 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (π‘(𝑘 + 1)) = ((π𝑘) + 1))
147146oveq2d 7146 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) = ((2 · 𝑁)↑((π𝑘) + 1)))
148123ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (2 · 𝑁) ∈ ℂ)
149148, 133expp1d 13495 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑((π𝑘) + 1)) = (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁)))
150147, 149eqtrd 2856 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) = (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁)))
151150breq2d 5051 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁))))
152142, 151bitr4d 285 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
153 simpr 488 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
154 nnuz 12259 . . . . . . . . . . . . 13 ℕ = (ℤ‘1)
155153, 154eleqtrdi 2922 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
156 seqp1 13367 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ‘1) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))
157155, 156syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))
158157adantr 484 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))
159 peano2nn 11627 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
160159adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
161 eleq1 2899 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘 + 1) → (𝑛 ∈ ℙ ↔ (𝑘 + 1) ∈ ℙ))
162 id 22 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1))
163 oveq1 7137 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑘 + 1) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = ((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁)))
164162, 163oveq12d 7148 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘 + 1) → (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))) = ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))))
165161, 164ifbieq1d 4463 . . . . . . . . . . . . . . 15 (𝑛 = (𝑘 + 1) → if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1))
166 ovex 7163 . . . . . . . . . . . . . . . 16 ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) ∈ V
167166, 117ifex 4488 . . . . . . . . . . . . . . 15 if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1) ∈ V
168165, 1, 167fvmpt 6741 . . . . . . . . . . . . . 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 4446 . . . . . . . . . . . . 13 ((𝑘 + 1) ∈ ℙ → if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1) = ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))))
171169, 170sylan9eq 2876 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) = ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))))
1726adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑁 ∈ ℕ)
173 bposlem1 25846 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ (𝑘 + 1) ∈ ℙ) → ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
174172, 173sylan 583 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
175171, 174eqbrtrd 5061 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) ≤ (2 · 𝑁))
17614simpld 498 . . . . . . . . . . . . . . 15 (𝜑𝐹:ℕ⟶ℕ)
177 ffvelrn 6822 . . . . . . . . . . . . . . 15 ((𝐹:ℕ⟶ℕ ∧ (𝑘 + 1) ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℕ)
178176, 159, 177syl2an 598 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℕ)
179178nnred 11630 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℝ)
180179adantr 484 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) ∈ ℝ)
18122ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (2 · 𝑁) ∈ ℝ)
182 nnre 11622 . . . . . . . . . . . . . . 15 ((seq1( · , 𝐹)‘𝑘) ∈ ℕ → (seq1( · , 𝐹)‘𝑘) ∈ ℝ)
183 nngt0 11646 . . . . . . . . . . . . . . 15 ((seq1( · , 𝐹)‘𝑘) ∈ ℕ → 0 < (seq1( · , 𝐹)‘𝑘))
184182, 183jca 515 . . . . . . . . . . . . . 14 ((seq1( · , 𝐹)‘𝑘) ∈ ℕ → ((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑘)))
185126, 184syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑘)))
186185adantr 484 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑘)))
187 lemul2 11470 . . . . . . . . . . . 12 (((𝐹‘(𝑘 + 1)) ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ ((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑘))) → ((𝐹‘(𝑘 + 1)) ≤ (2 · 𝑁) ↔ ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁))))
188180, 181, 186, 187syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((𝐹‘(𝑘 + 1)) ≤ (2 · 𝑁) ↔ ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁))))
189175, 188mpbid 235 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)))
190158, 189eqbrtrd 5061 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)))
191 ffvelrn 6822 . . . . . . . . . . . . 13 ((seq1( · , 𝐹):ℕ⟶ℕ ∧ (𝑘 + 1) ∈ ℕ) → (seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℕ)
19215, 159, 191syl2an 598 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℕ)
193192nnred 11630 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℝ)
19425adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
195126, 194nnmulcld 11668 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∈ ℕ)
196195nnred 11630 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∈ ℝ)
197160nnred 11630 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
198 ppicl 25694 . . . . . . . . . . . . . 14 ((𝑘 + 1) ∈ ℝ → (π‘(𝑘 + 1)) ∈ ℕ0)
199197, 198syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (π‘(𝑘 + 1)) ∈ ℕ0)
200194, 199nnexpcld 13590 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) ∈ ℕ)
201200nnred 11630 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) ∈ ℝ)
202 letr 10711 . . . . . . . . . . 11 (((seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℝ ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∈ ℝ ∧ ((2 · 𝑁)↑(π‘(𝑘 + 1))) ∈ ℝ) → (((seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
203193, 196, 201, 202syl3anc 1368 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (((seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
204203adantr 484 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (((seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
205190, 204mpand 694 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
206152, 205sylbid 243 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
207157adantr 484 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))
208 iffalse 4449 . . . . . . . . . . . 12 (¬ (𝑘 + 1) ∈ ℙ → if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1) = 1)
209169, 208sylan9eq 2876 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) = 1)
210209oveq2d 7146 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) = ((seq1( · , 𝐹)‘𝑘) · 1))
211126adantr 484 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘𝑘) ∈ ℕ)
212211nncnd 11631 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘𝑘) ∈ ℂ)
213212mulid1d 10635 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) · 1) = (seq1( · , 𝐹)‘𝑘))
214207, 210, 2133eqtrd 2860 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘(𝑘 + 1)) = (seq1( · , 𝐹)‘𝑘))
215 ppinprm 25715 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ ¬ (𝑘 + 1) ∈ ℙ) → (π‘(𝑘 + 1)) = (π𝑘))
216144, 215sylan 583 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (π‘(𝑘 + 1)) = (π𝑘))
217216oveq2d 7146 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) = ((2 · 𝑁)↑(π𝑘)))
218214, 217breq12d 5052 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))) ↔ (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘))))
219218biimprd 251 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
220206, 219pm2.61dan 812 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
221220expcom 417 . . . . 5 (𝑘 ∈ ℕ → (𝜑 → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))))
222221a2d 29 . . . 4 (𝑘 ∈ ℕ → ((𝜑 → (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘))) → (𝜑 → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))))
22393, 98, 103, 108, 125, 222nnind 11633 . . 3 (𝑀 ∈ ℕ → (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π𝑀))))
22474, 223mpcom 38 . 2 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π𝑀)))
225 cxpexp 25237 . . . 4 (((2 · 𝑁) ∈ ℂ ∧ (π𝑀) ∈ ℕ0) → ((2 · 𝑁)↑𝑐(π𝑀)) = ((2 · 𝑁)↑(π𝑀)))
226123, 79, 225syl2anc 587 . . 3 (𝜑 → ((2 · 𝑁)↑𝑐(π𝑀)) = ((2 · 𝑁)↑(π𝑀)))
22779nn0red 11934 . . . . 5 (𝜑 → (π𝑀) ∈ ℝ)
228 nndivre 11656 . . . . . . 7 ((𝑀 ∈ ℝ ∧ 3 ∈ ℕ) → (𝑀 / 3) ∈ ℝ)
22977, 16, 228sylancl 589 . . . . . 6 (𝜑 → (𝑀 / 3) ∈ ℝ)
230 readdcl 10597 . . . . . 6 (((𝑀 / 3) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑀 / 3) + 2) ∈ ℝ)
231229, 48, 230sylancl 589 . . . . 5 (𝜑 → ((𝑀 / 3) + 2) ∈ ℝ)
23274nnnn0d 11933 . . . . . . 7 (𝜑𝑀 ∈ ℕ0)
233232nn0ge0d 11936 . . . . . 6 (𝜑 → 0 ≤ 𝑀)
234 ppiub 25766 . . . . . 6 ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (π𝑀) ≤ ((𝑀 / 3) + 2))
23577, 233, 234syl2anc 587 . . . . 5 (𝜑 → (π𝑀) ≤ ((𝑀 / 3) + 2))
23648a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℝ)
237 flle 13152 . . . . . . . . 9 ((√‘(2 · 𝑁)) ∈ ℝ → (⌊‘(√‘(2 · 𝑁))) ≤ (√‘(2 · 𝑁)))
23828, 237syl 17 . . . . . . . 8 (𝜑 → (⌊‘(√‘(2 · 𝑁))) ≤ (√‘(2 · 𝑁)))
23917, 238eqbrtrid 5074 . . . . . . 7 (𝜑𝑀 ≤ (√‘(2 · 𝑁)))
240 3re 11695 . . . . . . . . . 10 3 ∈ ℝ
241 3pos 11720 . . . . . . . . . 10 0 < 3
242240, 241pm3.2i 474 . . . . . . . . 9 (3 ∈ ℝ ∧ 0 < 3)
243242a1i 11 . . . . . . . 8 (𝜑 → (3 ∈ ℝ ∧ 0 < 3))
244 lediv1 11482 . . . . . . . 8 ((𝑀 ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (𝑀 ≤ (√‘(2 · 𝑁)) ↔ (𝑀 / 3) ≤ ((√‘(2 · 𝑁)) / 3)))
24577, 28, 243, 244syl3anc 1368 . . . . . . 7 (𝜑 → (𝑀 ≤ (√‘(2 · 𝑁)) ↔ (𝑀 / 3) ≤ ((√‘(2 · 𝑁)) / 3)))
246239, 245mpbid 235 . . . . . 6 (𝜑 → (𝑀 / 3) ≤ ((√‘(2 · 𝑁)) / 3))
247229, 83, 236, 246leadd1dd 11231 . . . . 5 (𝜑 → ((𝑀 / 3) + 2) ≤ (((√‘(2 · 𝑁)) / 3) + 2))
248227, 231, 85, 235, 247letrd 10774 . . . 4 (𝜑 → (π𝑀) ≤ (((√‘(2 · 𝑁)) / 3) + 2))
249 2t1e2 11778 . . . . . . . 8 (2 · 1) = 2
2506nnge1d 11663 . . . . . . . . 9 (𝜑 → 1 ≤ 𝑁)
251 1re 10618 . . . . . . . . . . 11 1 ∈ ℝ
252 lemul2 11470 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
253251, 50, 252mp3an13 1449 . . . . . . . . . 10 (𝑁 ∈ ℝ → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
25446, 253syl 17 . . . . . . . . 9 (𝜑 → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
255250, 254mpbid 235 . . . . . . . 8 (𝜑 → (2 · 1) ≤ (2 · 𝑁))
256249, 255eqbrtrrid 5075 . . . . . . 7 (𝜑 → 2 ≤ (2 · 𝑁))
25718eluz1i 12229 . . . . . . 7 ((2 · 𝑁) ∈ (ℤ‘2) ↔ ((2 · 𝑁) ∈ ℤ ∧ 2 ≤ (2 · 𝑁)))
25821, 256, 257sylanbrc 586 . . . . . 6 (𝜑 → (2 · 𝑁) ∈ (ℤ‘2))
259 eluz2gt1 12298 . . . . . 6 ((2 · 𝑁) ∈ (ℤ‘2) → 1 < (2 · 𝑁))
260258, 259syl 17 . . . . 5 (𝜑 → 1 < (2 · 𝑁))
26122, 260, 227, 85cxpled 25289 . . . 4 (𝜑 → ((π𝑀) ≤ (((√‘(2 · 𝑁)) / 3) + 2) ↔ ((2 · 𝑁)↑𝑐(π𝑀)) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2))))
262248, 261mpbid 235 . . 3 (𝜑 → ((2 · 𝑁)↑𝑐(π𝑀)) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
263226, 262eqbrtrrd 5063 . 2 (𝜑 → ((2 · 𝑁)↑(π𝑀)) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
26476, 81, 86, 224, 263letrd 10774 1 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wrex 3127  ifcif 4440   class class class wbr 5039  cmpt 5119  wf 6324  cfv 6328  (class class class)co 7130  cc 10512  cr 10513  0cc0 10514  1c1 10515   + caddc 10517   · cmul 10519   < clt 10652  cle 10653   / cdiv 11274  cn 11615  2c2 11670  3c3 11671  5c5 11673  9c9 11677  0cn0 11875  cz 11959  cdc 12076  cuz 12221  ...cfz 12875  cfl 13143  seqcseq 13352  cexp 13413  Ccbc 13646  csqrt 14571  cprime 15992   pCnt cpc 16150  𝑐ccxp 25125  πcppi 25657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-inf2 9080  ax-cnex 10570  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590  ax-pre-mulgt0 10591  ax-pre-sup 10592  ax-addf 10593  ax-mulf 10594
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-int 4850  df-iun 4894  df-iin 4895  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-of 7384  df-om 7556  df-1st 7664  df-2nd 7665  df-supp 7806  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-1o 8077  df-2o 8078  df-oadd 8081  df-er 8264  df-map 8383  df-pm 8384  df-ixp 8437  df-en 8485  df-dom 8486  df-sdom 8487  df-fin 8488  df-fsupp 8810  df-fi 8851  df-sup 8882  df-inf 8883  df-oi 8950  df-dju 9306  df-card 9344  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-sub 10849  df-neg 10850  df-div 11275  df-nn 11616  df-2 11678  df-3 11679  df-4 11680  df-5 11681  df-6 11682  df-7 11683  df-8 11684  df-9 11685  df-n0 11876  df-xnn0 11946  df-z 11960  df-dec 12077  df-uz 12222  df-q 12327  df-rp 12368  df-xneg 12485  df-xadd 12486  df-xmul 12487  df-ioo 12720  df-ioc 12721  df-ico 12722  df-icc 12723  df-fz 12876  df-fzo 13017  df-fl 13145  df-mod 13221  df-seq 13353  df-exp 13414  df-fac 13618  df-bc 13647  df-hash 13675  df-shft 14405  df-cj 14437  df-re 14438  df-im 14439  df-sqrt 14573  df-abs 14574  df-limsup 14807  df-clim 14824  df-rlim 14825  df-sum 15022  df-ef 15400  df-sin 15402  df-cos 15403  df-pi 15405  df-dvds 15587  df-gcd 15821  df-prm 15993  df-pc 16151  df-struct 16463  df-ndx 16464  df-slot 16465  df-base 16467  df-sets 16468  df-ress 16469  df-plusg 16556  df-mulr 16557  df-starv 16558  df-sca 16559  df-vsca 16560  df-ip 16561  df-tset 16562  df-ple 16563  df-ds 16565  df-unif 16566  df-hom 16567  df-cco 16568  df-rest 16674  df-topn 16675  df-0g 16693  df-gsum 16694  df-topgen 16695  df-pt 16696  df-prds 16699  df-xrs 16753  df-qtop 16758  df-imas 16759  df-xps 16761  df-mre 16835  df-mrc 16836  df-acs 16838  df-mgm 17830  df-sgrp 17879  df-mnd 17890  df-submnd 17935  df-mulg 18203  df-cntz 18425  df-cmn 18886  df-psmet 20512  df-xmet 20513  df-met 20514  df-bl 20515  df-mopn 20516  df-fbas 20517  df-fg 20518  df-cnfld 20521  df-top 21477  df-topon 21494  df-topsp 21516  df-bases 21529  df-cld 21602  df-ntr 21603  df-cls 21604  df-nei 21681  df-lp 21719  df-perf 21720  df-cn 21810  df-cnp 21811  df-haus 21898  df-tx 22145  df-hmeo 22338  df-fil 22429  df-fm 22521  df-flim 22522  df-flf 22523  df-xms 22905  df-ms 22906  df-tms 22907  df-cncf 23461  df-limc 24447  df-dv 24448  df-log 25126  df-cxp 25127  df-ppi 25663
This theorem is referenced by:  bposlem6  25851
  Copyright terms: Public domain W3C validator