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

Theorem bposlem5 25058
 Description: Lemma for bpos 25063. 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 11226 . . . . . . . . . . 11 5 ∈ ℕ
4 bpos.1 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘5))
5 eluznn 11796 . . . . . . . . . . 11 ((5 ∈ ℕ ∧ 𝑁 ∈ (ℤ‘5)) → 𝑁 ∈ ℕ)
63, 4, 5sylancr 696 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
76nnnn0d 11389 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
8 fzctr 12490 . . . . . . . . 9 (𝑁 ∈ ℕ0𝑁 ∈ (0...(2 · 𝑁)))
9 bccl2 13150 . . . . . . . . 9 (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
107, 8, 93syl 18 . . . . . . . 8 (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ)
11 pccl 15601 . . . . . . . 8 ((𝑛 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
122, 10, 11syl2anr 494 . . . . . . 7 ((𝜑𝑛 ∈ ℙ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
1312ralrimiva 2995 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
141, 13pcmptcl 15642 . . . . 5 (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
1514simprd 478 . . . 4 (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ)
16 3nn 11224 . . . . 5 3 ∈ ℕ
17 bpos.5 . . . . . 6 𝑀 = (⌊‘(√‘(2 · 𝑁)))
18 2z 11447 . . . . . . . . . . 11 2 ∈ ℤ
196nnzd 11519 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
20 zmulcl 11464 . . . . . . . . . . 11 ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 · 𝑁) ∈ ℤ)
2118, 19, 20sylancr 696 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℤ)
2221zred 11520 . . . . . . . . 9 (𝜑 → (2 · 𝑁) ∈ ℝ)
23 2nn 11223 . . . . . . . . . . . 12 2 ∈ ℕ
24 nnmulcl 11081 . . . . . . . . . . . 12 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
2523, 6, 24sylancr 696 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) ∈ ℕ)
2625nnrpd 11908 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℝ+)
2726rpge0d 11914 . . . . . . . . 9 (𝜑 → 0 ≤ (2 · 𝑁))
2822, 27resqrtcld 14200 . . . . . . . 8 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
2928flcld 12639 . . . . . . 7 (𝜑 → (⌊‘(√‘(2 · 𝑁))) ∈ ℤ)
30 sqrt9 14058 . . . . . . . . 9 (√‘9) = 3
31 9re 11145 . . . . . . . . . . . 12 9 ∈ ℝ
3231a1i 11 . . . . . . . . . . 11 (𝜑 → 9 ∈ ℝ)
33 10re 11555 . . . . . . . . . . . 12 10 ∈ ℝ
3433a1i 11 . . . . . . . . . . 11 (𝜑10 ∈ ℝ)
35 lep1 10900 . . . . . . . . . . . . . 14 (9 ∈ ℝ → 9 ≤ (9 + 1))
3631, 35ax-mp 5 . . . . . . . . . . . . 13 9 ≤ (9 + 1)
37 9p1e10 11534 . . . . . . . . . . . . 13 (9 + 1) = 10
3836, 37breqtri 4710 . . . . . . . . . . . 12 9 ≤ 10
3938a1i 11 . . . . . . . . . . 11 (𝜑 → 9 ≤ 10)
40 5cn 11138 . . . . . . . . . . . . 13 5 ∈ ℂ
41 2cn 11129 . . . . . . . . . . . . 13 2 ∈ ℂ
42 5t2e10 11672 . . . . . . . . . . . . 13 (5 · 2) = 10
4340, 41, 42mulcomli 10085 . . . . . . . . . . . 12 (2 · 5) = 10
44 eluzle 11738 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘5) → 5 ≤ 𝑁)
454, 44syl 17 . . . . . . . . . . . . 13 (𝜑 → 5 ≤ 𝑁)
466nnred 11073 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
47 5re 11137 . . . . . . . . . . . . . . 15 5 ∈ ℝ
48 2re 11128 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
49 2pos 11150 . . . . . . . . . . . . . . . 16 0 < 2
5048, 49pm3.2i 470 . . . . . . . . . . . . . . 15 (2 ∈ ℝ ∧ 0 < 2)
51 lemul2 10914 . . . . . . . . . . . . . . 15 ((5 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2 · 𝑁)))
5247, 50, 51mp3an13 1455 . . . . . . . . . . . . . 14 (𝑁 ∈ ℝ → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2 · 𝑁)))
5346, 52syl 17 . . . . . . . . . . . . 13 (𝜑 → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2 · 𝑁)))
5445, 53mpbid 222 . . . . . . . . . . . 12 (𝜑 → (2 · 5) ≤ (2 · 𝑁))
5543, 54syl5eqbrr 4721 . . . . . . . . . . 11 (𝜑10 ≤ (2 · 𝑁))
5632, 34, 22, 39, 55letrd 10232 . . . . . . . . . 10 (𝜑 → 9 ≤ (2 · 𝑁))
57 0re 10078 . . . . . . . . . . . . 13 0 ∈ ℝ
58 9pos 11160 . . . . . . . . . . . . 13 0 < 9
5957, 31, 58ltleii 10198 . . . . . . . . . . . 12 0 ≤ 9
6031, 59pm3.2i 470 . . . . . . . . . . 11 (9 ∈ ℝ ∧ 0 ≤ 9)
6122, 27jca 553 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)))
62 sqrtle 14045 . . . . . . . . . . 11 (((9 ∈ ℝ ∧ 0 ≤ 9) ∧ ((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁))) → (9 ≤ (2 · 𝑁) ↔ (√‘9) ≤ (√‘(2 · 𝑁))))
6360, 61, 62sylancr 696 . . . . . . . . . 10 (𝜑 → (9 ≤ (2 · 𝑁) ↔ (√‘9) ≤ (√‘(2 · 𝑁))))
6456, 63mpbid 222 . . . . . . . . 9 (𝜑 → (√‘9) ≤ (√‘(2 · 𝑁)))
6530, 64syl5eqbrr 4721 . . . . . . . 8 (𝜑 → 3 ≤ (√‘(2 · 𝑁)))
66 3z 11448 . . . . . . . . 9 3 ∈ ℤ
67 flge 12646 . . . . . . . . 9 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℤ) → (3 ≤ (√‘(2 · 𝑁)) ↔ 3 ≤ (⌊‘(√‘(2 · 𝑁)))))
6828, 66, 67sylancl 695 . . . . . . . 8 (𝜑 → (3 ≤ (√‘(2 · 𝑁)) ↔ 3 ≤ (⌊‘(√‘(2 · 𝑁)))))
6965, 68mpbid 222 . . . . . . 7 (𝜑 → 3 ≤ (⌊‘(√‘(2 · 𝑁))))
7066eluz1i 11733 . . . . . . 7 ((⌊‘(√‘(2 · 𝑁))) ∈ (ℤ‘3) ↔ ((⌊‘(√‘(2 · 𝑁))) ∈ ℤ ∧ 3 ≤ (⌊‘(√‘(2 · 𝑁)))))
7129, 69, 70sylanbrc 699 . . . . . 6 (𝜑 → (⌊‘(√‘(2 · 𝑁))) ∈ (ℤ‘3))
7217, 71syl5eqel 2734 . . . . 5 (𝜑𝑀 ∈ (ℤ‘3))
73 eluznn 11796 . . . . 5 ((3 ∈ ℕ ∧ 𝑀 ∈ (ℤ‘3)) → 𝑀 ∈ ℕ)
7416, 72, 73sylancr 696 . . . 4 (𝜑𝑀 ∈ ℕ)
7515, 74ffvelrnd 6400 . . 3 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℕ)
7675nnred 11073 . 2 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
7774nnred 11073 . . . . 5 (𝜑𝑀 ∈ ℝ)
78 ppicl 24902 . . . . 5 (𝑀 ∈ ℝ → (π𝑀) ∈ ℕ0)
7977, 78syl 17 . . . 4 (𝜑 → (π𝑀) ∈ ℕ0)
8025, 79nnexpcld 13070 . . 3 (𝜑 → ((2 · 𝑁)↑(π𝑀)) ∈ ℕ)
8180nnred 11073 . 2 (𝜑 → ((2 · 𝑁)↑(π𝑀)) ∈ ℝ)
82 nndivre 11094 . . . . 5 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
8328, 16, 82sylancl 695 . . . 4 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
84 readdcl 10057 . . . 4 ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
8583, 48, 84sylancl 695 . . 3 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
8622, 27, 85recxpcld 24514 . 2 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ)
87 fveq2 6229 . . . . . 6 (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
88 fveq2 6229 . . . . . . . 8 (𝑥 = 1 → (π𝑥) = (π‘1))
89 ppi1 24935 . . . . . . . 8 (π‘1) = 0
9088, 89syl6eq 2701 . . . . . . 7 (𝑥 = 1 → (π𝑥) = 0)
9190oveq2d 6706 . . . . . 6 (𝑥 = 1 → ((2 · 𝑁)↑(π𝑥)) = ((2 · 𝑁)↑0))
9287, 91breq12d 4698 . . . . 5 (𝑥 = 1 → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥)) ↔ (seq1( · , 𝐹)‘1) ≤ ((2 · 𝑁)↑0)))
9392imbi2d 329 . . . 4 (𝑥 = 1 → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘1) ≤ ((2 · 𝑁)↑0))))
94 fveq2 6229 . . . . . 6 (𝑥 = 𝑘 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑘))
95 fveq2 6229 . . . . . . 7 (𝑥 = 𝑘 → (π𝑥) = (π𝑘))
9695oveq2d 6706 . . . . . 6 (𝑥 = 𝑘 → ((2 · 𝑁)↑(π𝑥)) = ((2 · 𝑁)↑(π𝑘)))
9794, 96breq12d 4698 . . . . 5 (𝑥 = 𝑘 → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥)) ↔ (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘))))
9897imbi2d 329 . . . 4 (𝑥 = 𝑘 → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)))))
99 fveq2 6229 . . . . . 6 (𝑥 = (𝑘 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑘 + 1)))
100 fveq2 6229 . . . . . . 7 (𝑥 = (𝑘 + 1) → (π𝑥) = (π‘(𝑘 + 1)))
101100oveq2d 6706 . . . . . 6 (𝑥 = (𝑘 + 1) → ((2 · 𝑁)↑(π𝑥)) = ((2 · 𝑁)↑(π‘(𝑘 + 1))))
10299, 101breq12d 4698 . . . . 5 (𝑥 = (𝑘 + 1) → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥)) ↔ (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
103102imbi2d 329 . . . 4 (𝑥 = (𝑘 + 1) → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))))
104 fveq2 6229 . . . . . 6 (𝑥 = 𝑀 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑀))
105 fveq2 6229 . . . . . . 7 (𝑥 = 𝑀 → (π𝑥) = (π𝑀))
106105oveq2d 6706 . . . . . 6 (𝑥 = 𝑀 → ((2 · 𝑁)↑(π𝑥)) = ((2 · 𝑁)↑(π𝑀)))
107104, 106breq12d 4698 . . . . 5 (𝑥 = 𝑀 → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥)) ↔ (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π𝑀))))
108107imbi2d 329 . . . 4 (𝑥 = 𝑀 → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π𝑀)))))
109 1z 11445 . . . . . . . 8 1 ∈ ℤ
110 seq1 12854 . . . . . . . 8 (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
111109, 110ax-mp 5 . . . . . . 7 (seq1( · , 𝐹)‘1) = (𝐹‘1)
112 1nn 11069 . . . . . . . 8 1 ∈ ℕ
113 1nprm 15439 . . . . . . . . . . 11 ¬ 1 ∈ ℙ
114 eleq1 2718 . . . . . . . . . . 11 (𝑛 = 1 → (𝑛 ∈ ℙ ↔ 1 ∈ ℙ))
115113, 114mtbiri 316 . . . . . . . . . 10 (𝑛 = 1 → ¬ 𝑛 ∈ ℙ)
116115iffalsed 4130 . . . . . . . . 9 (𝑛 = 1 → if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1) = 1)
117 1ex 10073 . . . . . . . . 9 1 ∈ V
118116, 1, 117fvmpt 6321 . . . . . . . 8 (1 ∈ ℕ → (𝐹‘1) = 1)
119112, 118ax-mp 5 . . . . . . 7 (𝐹‘1) = 1
120111, 119eqtri 2673 . . . . . 6 (seq1( · , 𝐹)‘1) = 1
121 1le1 10693 . . . . . 6 1 ≤ 1
122120, 121eqbrtri 4706 . . . . 5 (seq1( · , 𝐹)‘1) ≤ 1
12321zcnd 11521 . . . . . 6 (𝜑 → (2 · 𝑁) ∈ ℂ)
124123exp0d 13042 . . . . 5 (𝜑 → ((2 · 𝑁)↑0) = 1)
125122, 124syl5breqr 4723 . . . 4 (𝜑 → (seq1( · , 𝐹)‘1) ≤ ((2 · 𝑁)↑0))
12615ffvelrnda 6399 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘𝑘) ∈ ℕ)
127126nnred 11073 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘𝑘) ∈ ℝ)
128127adantr 480 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘𝑘) ∈ ℝ)
12925ad2antrr 762 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (2 · 𝑁) ∈ ℕ)
130 nnre 11065 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
131130ad2antlr 763 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → 𝑘 ∈ ℝ)
132 ppicl 24902 . . . . . . . . . . . . 13 (𝑘 ∈ ℝ → (π𝑘) ∈ ℕ0)
133131, 132syl 17 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (π𝑘) ∈ ℕ0)
134129, 133nnexpcld 13070 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π𝑘)) ∈ ℕ)
135134nnred 11073 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π𝑘)) ∈ ℝ)
136 nnre 11065 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℕ → (2 · 𝑁) ∈ ℝ)
137 nngt0 11087 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℕ → 0 < (2 · 𝑁))
138136, 137jca 553 . . . . . . . . . . . 12 ((2 · 𝑁) ∈ ℕ → ((2 · 𝑁) ∈ ℝ ∧ 0 < (2 · 𝑁)))
13925, 138syl 17 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ 0 < (2 · 𝑁)))
140139ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁) ∈ ℝ ∧ 0 < (2 · 𝑁)))
141 lemul1 10913 . . . . . . . . . 10 (((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ ((2 · 𝑁)↑(π𝑘)) ∈ ℝ ∧ ((2 · 𝑁) ∈ ℝ ∧ 0 < (2 · 𝑁))) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁))))
142128, 135, 140, 141syl3anc 1366 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁))))
143 nnz 11437 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
144143adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
145 ppiprm 24922 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ (𝑘 + 1) ∈ ℙ) → (π‘(𝑘 + 1)) = ((π𝑘) + 1))
146144, 145sylan 487 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (π‘(𝑘 + 1)) = ((π𝑘) + 1))
147146oveq2d 6706 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) = ((2 · 𝑁)↑((π𝑘) + 1)))
148123ad2antrr 762 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (2 · 𝑁) ∈ ℂ)
149148, 133expp1d 13049 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑((π𝑘) + 1)) = (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁)))
150147, 149eqtrd 2685 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) = (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁)))
151150breq2d 4697 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ (((2 · 𝑁)↑(π𝑘)) · (2 · 𝑁))))
152142, 151bitr4d 271 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
153 simpr 476 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
154 nnuz 11761 . . . . . . . . . . . . 13 ℕ = (ℤ‘1)
155153, 154syl6eleq 2740 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
156 seqp1 12856 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ‘1) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))
157155, 156syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))
158157adantr 480 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))
159 peano2nn 11070 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
160159adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
161 eleq1 2718 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘 + 1) → (𝑛 ∈ ℙ ↔ (𝑘 + 1) ∈ ℙ))
162 id 22 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1))
163 oveq1 6697 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑘 + 1) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = ((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁)))
164162, 163oveq12d 6708 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘 + 1) → (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))) = ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))))
165161, 164ifbieq1d 4142 . . . . . . . . . . . . . . 15 (𝑛 = (𝑘 + 1) → if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1))
166 ovex 6718 . . . . . . . . . . . . . . . 16 ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) ∈ V
167166, 117ifex 4189 . . . . . . . . . . . . . . 15 if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1) ∈ V
168165, 1, 167fvmpt 6321 . . . . . . . . . . . . . 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 4125 . . . . . . . . . . . . 13 ((𝑘 + 1) ∈ ℙ → if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1) = ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))))
171169, 170sylan9eq 2705 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) = ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))))
1726adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑁 ∈ ℕ)
173 bposlem1 25054 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ (𝑘 + 1) ∈ ℙ) → ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
174172, 173sylan 487 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
175171, 174eqbrtrd 4707 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) ≤ (2 · 𝑁))
17614simpld 474 . . . . . . . . . . . . . . 15 (𝜑𝐹:ℕ⟶ℕ)
177 ffvelrn 6397 . . . . . . . . . . . . . . 15 ((𝐹:ℕ⟶ℕ ∧ (𝑘 + 1) ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℕ)
178176, 159, 177syl2an 493 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℕ)
179178nnred 11073 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℝ)
180179adantr 480 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) ∈ ℝ)
18122ad2antrr 762 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (2 · 𝑁) ∈ ℝ)
182 nnre 11065 . . . . . . . . . . . . . . 15 ((seq1( · , 𝐹)‘𝑘) ∈ ℕ → (seq1( · , 𝐹)‘𝑘) ∈ ℝ)
183 nngt0 11087 . . . . . . . . . . . . . . 15 ((seq1( · , 𝐹)‘𝑘) ∈ ℕ → 0 < (seq1( · , 𝐹)‘𝑘))
184182, 183jca 553 . . . . . . . . . . . . . 14 ((seq1( · , 𝐹)‘𝑘) ∈ ℕ → ((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑘)))
185126, 184syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑘)))
186185adantr 480 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑘)))
187 lemul2 10914 . . . . . . . . . . . 12 (((𝐹‘(𝑘 + 1)) ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ ((seq1( · , 𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑘))) → ((𝐹‘(𝑘 + 1)) ≤ (2 · 𝑁) ↔ ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁))))
188180, 181, 186, 187syl3anc 1366 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((𝐹‘(𝑘 + 1)) ≤ (2 · 𝑁) ↔ ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁))))
189175, 188mpbid 222 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)))
190158, 189eqbrtrd 4707 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)))
191 ffvelrn 6397 . . . . . . . . . . . . 13 ((seq1( · , 𝐹):ℕ⟶ℕ ∧ (𝑘 + 1) ∈ ℕ) → (seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℕ)
19215, 159, 191syl2an 493 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℕ)
193192nnred 11073 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℝ)
19425adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
195126, 194nnmulcld 11106 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∈ ℕ)
196195nnred 11073 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∈ ℝ)
197160nnred 11073 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
198 ppicl 24902 . . . . . . . . . . . . . 14 ((𝑘 + 1) ∈ ℝ → (π‘(𝑘 + 1)) ∈ ℕ0)
199197, 198syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (π‘(𝑘 + 1)) ∈ ℕ0)
200194, 199nnexpcld 13070 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) ∈ ℕ)
201200nnred 11073 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) ∈ ℝ)
202 letr 10169 . . . . . . . . . . 11 (((seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℝ ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∈ ℝ ∧ ((2 · 𝑁)↑(π‘(𝑘 + 1))) ∈ ℝ) → (((seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
203193, 196, 201, 202syl3anc 1366 . . . . . . . . . 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 711 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
206152, 205sylbid 230 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
207157adantr 480 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))
208 iffalse 4128 . . . . . . . . . . . 12 (¬ (𝑘 + 1) ∈ ℙ → if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1) = 1)
209169, 208sylan9eq 2705 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) = 1)
210209oveq2d 6706 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) = ((seq1( · , 𝐹)‘𝑘) · 1))
211126adantr 480 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘𝑘) ∈ ℕ)
212211nncnd 11074 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘𝑘) ∈ ℂ)
213212mulid1d 10095 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) · 1) = (seq1( · , 𝐹)‘𝑘))
214207, 210, 2133eqtrd 2689 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (seq1( · , 𝐹)‘(𝑘 + 1)) = (seq1( · , 𝐹)‘𝑘))
215 ppinprm 24923 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ ¬ (𝑘 + 1) ∈ ℙ) → (π‘(𝑘 + 1)) = (π𝑘))
216144, 215sylan 487 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (π‘(𝑘 + 1)) = (π𝑘))
217216oveq2d 6706 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) = ((2 · 𝑁)↑(π𝑘)))
218214, 217breq12d 4698 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))) ↔ (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘))))
219218biimprd 238 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
220206, 219pm2.61dan 849 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))
221220expcom 450 . . . . 5 (𝑘 ∈ ℕ → (𝜑 → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))))
222221a2d 29 . . . 4 (𝑘 ∈ ℕ → ((𝜑 → (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π𝑘))) → (𝜑 → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))))
22393, 98, 103, 108, 125, 222nnind 11076 . . 3 (𝑀 ∈ ℕ → (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π𝑀))))
22474, 223mpcom 38 . 2 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π𝑀)))
225 cxpexp 24459 . . . 4 (((2 · 𝑁) ∈ ℂ ∧ (π𝑀) ∈ ℕ0) → ((2 · 𝑁)↑𝑐(π𝑀)) = ((2 · 𝑁)↑(π𝑀)))
226123, 79, 225syl2anc 694 . . 3 (𝜑 → ((2 · 𝑁)↑𝑐(π𝑀)) = ((2 · 𝑁)↑(π𝑀)))
22779nn0red 11390 . . . . 5 (𝜑 → (π𝑀) ∈ ℝ)
228 nndivre 11094 . . . . . . 7 ((𝑀 ∈ ℝ ∧ 3 ∈ ℕ) → (𝑀 / 3) ∈ ℝ)
22977, 16, 228sylancl 695 . . . . . 6 (𝜑 → (𝑀 / 3) ∈ ℝ)
230 readdcl 10057 . . . . . 6 (((𝑀 / 3) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑀 / 3) + 2) ∈ ℝ)
231229, 48, 230sylancl 695 . . . . 5 (𝜑 → ((𝑀 / 3) + 2) ∈ ℝ)
23274nnnn0d 11389 . . . . . . 7 (𝜑𝑀 ∈ ℕ0)
233232nn0ge0d 11392 . . . . . 6 (𝜑 → 0 ≤ 𝑀)
234 ppiub 24974 . . . . . 6 ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (π𝑀) ≤ ((𝑀 / 3) + 2))
23577, 233, 234syl2anc 694 . . . . 5 (𝜑 → (π𝑀) ≤ ((𝑀 / 3) + 2))
23648a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℝ)
237 flle 12640 . . . . . . . . 9 ((√‘(2 · 𝑁)) ∈ ℝ → (⌊‘(√‘(2 · 𝑁))) ≤ (√‘(2 · 𝑁)))
23828, 237syl 17 . . . . . . . 8 (𝜑 → (⌊‘(√‘(2 · 𝑁))) ≤ (√‘(2 · 𝑁)))
23917, 238syl5eqbr 4720 . . . . . . 7 (𝜑𝑀 ≤ (√‘(2 · 𝑁)))
240 3re 11132 . . . . . . . . . 10 3 ∈ ℝ
241 3pos 11152 . . . . . . . . . 10 0 < 3
242240, 241pm3.2i 470 . . . . . . . . 9 (3 ∈ ℝ ∧ 0 < 3)
243242a1i 11 . . . . . . . 8 (𝜑 → (3 ∈ ℝ ∧ 0 < 3))
244 lediv1 10926 . . . . . . . 8 ((𝑀 ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (𝑀 ≤ (√‘(2 · 𝑁)) ↔ (𝑀 / 3) ≤ ((√‘(2 · 𝑁)) / 3)))
24577, 28, 243, 244syl3anc 1366 . . . . . . 7 (𝜑 → (𝑀 ≤ (√‘(2 · 𝑁)) ↔ (𝑀 / 3) ≤ ((√‘(2 · 𝑁)) / 3)))
246239, 245mpbid 222 . . . . . 6 (𝜑 → (𝑀 / 3) ≤ ((√‘(2 · 𝑁)) / 3))
247229, 83, 236, 246leadd1dd 10679 . . . . 5 (𝜑 → ((𝑀 / 3) + 2) ≤ (((√‘(2 · 𝑁)) / 3) + 2))
248227, 231, 85, 235, 247letrd 10232 . . . 4 (𝜑 → (π𝑀) ≤ (((√‘(2 · 𝑁)) / 3) + 2))
249 2t1e2 11214 . . . . . . . 8 (2 · 1) = 2
2506nnge1d 11101 . . . . . . . . 9 (𝜑 → 1 ≤ 𝑁)
251 1re 10077 . . . . . . . . . . 11 1 ∈ ℝ
252 lemul2 10914 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
253251, 50, 252mp3an13 1455 . . . . . . . . . 10 (𝑁 ∈ ℝ → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
25446, 253syl 17 . . . . . . . . 9 (𝜑 → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
255250, 254mpbid 222 . . . . . . . 8 (𝜑 → (2 · 1) ≤ (2 · 𝑁))
256249, 255syl5eqbrr 4721 . . . . . . 7 (𝜑 → 2 ≤ (2 · 𝑁))
25718eluz1i 11733 . . . . . . 7 ((2 · 𝑁) ∈ (ℤ‘2) ↔ ((2 · 𝑁) ∈ ℤ ∧ 2 ≤ (2 · 𝑁)))
25821, 256, 257sylanbrc 699 . . . . . 6 (𝜑 → (2 · 𝑁) ∈ (ℤ‘2))
259 eluz2gt1 11798 . . . . . 6 ((2 · 𝑁) ∈ (ℤ‘2) → 1 < (2 · 𝑁))
260258, 259syl 17 . . . . 5 (𝜑 → 1 < (2 · 𝑁))
26122, 260, 227, 85cxpled 24511 . . . 4 (𝜑 → ((π𝑀) ≤ (((√‘(2 · 𝑁)) / 3) + 2) ↔ ((2 · 𝑁)↑𝑐(π𝑀)) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2))))
262248, 261mpbid 222 . . 3 (𝜑 → ((2 · 𝑁)↑𝑐(π𝑀)) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
263226, 262eqbrtrrd 4709 . 2 (𝜑 → ((2 · 𝑁)↑(π𝑀)) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
26476, 81, 86, 224, 263letrd 10232 1 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ∃wrex 2942  ifcif 4119   class class class wbr 4685   ↦ cmpt 4762  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112   ≤ cle 10113   / cdiv 10722  ℕcn 11058  2c2 11108  3c3 11109  5c5 11111  9c9 11115  ℕ0cn0 11330  ℤcz 11415  ;cdc 11531  ℤ≥cuz 11725  ...cfz 12364  ⌊cfl 12631  seqcseq 12841  ↑cexp 12900  Ccbc 13129  √csqrt 14017  ℙcprime 15432   pCnt cpc 15588  ↑𝑐ccxp 24347  πcppi 24865 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-xnn0 11402  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-pi 14847  df-dvds 15028  df-gcd 15264  df-prm 15433  df-pc 15589  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676  df-log 24348  df-cxp 24349  df-ppi 24871 This theorem is referenced by:  bposlem6  25059
 Copyright terms: Public domain W3C validator