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

Theorem bposlem1 24990
Description: An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.)
Assertion
Ref Expression
bposlem1 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(𝑃 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))

Proof of Theorem bposlem1
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 fzfid 12755 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (1...(2 · 𝑁)) ∈ Fin)
2 2nn 11170 . . . . . . . . . . 11 2 ∈ ℕ
3 nnmulcl 11028 . . . . . . . . . . 11 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
42, 3mpan 705 . . . . . . . . . 10 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℕ)
54ad2antrr 761 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · 𝑁) ∈ ℕ)
6 prmnn 15369 . . . . . . . . . . 11 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
76ad2antlr 762 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑃 ∈ ℕ)
8 elfznn 12355 . . . . . . . . . . . 12 (𝑘 ∈ (1...(2 · 𝑁)) → 𝑘 ∈ ℕ)
98adantl 482 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑘 ∈ ℕ)
109nnnn0d 11336 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑘 ∈ ℕ0)
117, 10nnexpcld 13013 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑃𝑘) ∈ ℕ)
12 nnrp 11827 . . . . . . . . . 10 ((2 · 𝑁) ∈ ℕ → (2 · 𝑁) ∈ ℝ+)
13 nnrp 11827 . . . . . . . . . 10 ((𝑃𝑘) ∈ ℕ → (𝑃𝑘) ∈ ℝ+)
14 rpdivcl 11841 . . . . . . . . . 10 (((2 · 𝑁) ∈ ℝ+ ∧ (𝑃𝑘) ∈ ℝ+) → ((2 · 𝑁) / (𝑃𝑘)) ∈ ℝ+)
1512, 13, 14syl2an 494 . . . . . . . . 9 (((2 · 𝑁) ∈ ℕ ∧ (𝑃𝑘) ∈ ℕ) → ((2 · 𝑁) / (𝑃𝑘)) ∈ ℝ+)
165, 11, 15syl2anc 692 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) / (𝑃𝑘)) ∈ ℝ+)
1716rpred 11857 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) / (𝑃𝑘)) ∈ ℝ)
1817flcld 12582 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (⌊‘((2 · 𝑁) / (𝑃𝑘))) ∈ ℤ)
19 2z 11394 . . . . . . 7 2 ∈ ℤ
20 simpll 789 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑁 ∈ ℕ)
21 nnrp 11827 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ+)
22 rpdivcl 11841 . . . . . . . . . . 11 ((𝑁 ∈ ℝ+ ∧ (𝑃𝑘) ∈ ℝ+) → (𝑁 / (𝑃𝑘)) ∈ ℝ+)
2321, 13, 22syl2an 494 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑃𝑘) ∈ ℕ) → (𝑁 / (𝑃𝑘)) ∈ ℝ+)
2420, 11, 23syl2anc 692 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑁 / (𝑃𝑘)) ∈ ℝ+)
2524rpred 11857 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑁 / (𝑃𝑘)) ∈ ℝ)
2625flcld 12582 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (⌊‘(𝑁 / (𝑃𝑘))) ∈ ℤ)
27 zmulcl 11411 . . . . . . 7 ((2 ∈ ℤ ∧ (⌊‘(𝑁 / (𝑃𝑘))) ∈ ℤ) → (2 · (⌊‘(𝑁 / (𝑃𝑘)))) ∈ ℤ)
2819, 26, 27sylancr 694 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · (⌊‘(𝑁 / (𝑃𝑘)))) ∈ ℤ)
2918, 28zsubcld 11472 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ∈ ℤ)
3029zred 11467 . . . 4 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ∈ ℝ)
31 1re 10024 . . . . . 6 1 ∈ ℝ
32 0re 10025 . . . . . 6 0 ∈ ℝ
3331, 32keepel 4146 . . . . 5 if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0) ∈ ℝ
3433a1i 11 . . . 4 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0) ∈ ℝ)
3528zred 11467 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · (⌊‘(𝑁 / (𝑃𝑘)))) ∈ ℝ)
3617, 35resubcld 10443 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃𝑘)) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ∈ ℝ)
37 2re 11075 . . . . . . . . . 10 2 ∈ ℝ
3837a1i 11 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 2 ∈ ℝ)
3918zred 11467 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (⌊‘((2 · 𝑁) / (𝑃𝑘))) ∈ ℝ)
40 flle 12583 . . . . . . . . . . 11 (((2 · 𝑁) / (𝑃𝑘)) ∈ ℝ → (⌊‘((2 · 𝑁) / (𝑃𝑘))) ≤ ((2 · 𝑁) / (𝑃𝑘)))
4117, 40syl 17 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (⌊‘((2 · 𝑁) / (𝑃𝑘))) ≤ ((2 · 𝑁) / (𝑃𝑘)))
4239, 17, 35, 41lesub1dd 10628 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ (((2 · 𝑁) / (𝑃𝑘)) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))))
43 resubcl 10330 . . . . . . . . . . . . 13 (((𝑁 / (𝑃𝑘)) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑁 / (𝑃𝑘)) − 1) ∈ ℝ)
4425, 31, 43sylancl 693 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑁 / (𝑃𝑘)) − 1) ∈ ℝ)
45 remulcl 10006 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ ((𝑁 / (𝑃𝑘)) − 1) ∈ ℝ) → (2 · ((𝑁 / (𝑃𝑘)) − 1)) ∈ ℝ)
4637, 44, 45sylancr 694 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · ((𝑁 / (𝑃𝑘)) − 1)) ∈ ℝ)
47 flltp1 12584 . . . . . . . . . . . . . 14 ((𝑁 / (𝑃𝑘)) ∈ ℝ → (𝑁 / (𝑃𝑘)) < ((⌊‘(𝑁 / (𝑃𝑘))) + 1))
4825, 47syl 17 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑁 / (𝑃𝑘)) < ((⌊‘(𝑁 / (𝑃𝑘))) + 1))
49 1red 10040 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 1 ∈ ℝ)
5026zred 11467 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (⌊‘(𝑁 / (𝑃𝑘))) ∈ ℝ)
5125, 49, 50ltsubaddd 10608 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((𝑁 / (𝑃𝑘)) − 1) < (⌊‘(𝑁 / (𝑃𝑘))) ↔ (𝑁 / (𝑃𝑘)) < ((⌊‘(𝑁 / (𝑃𝑘))) + 1)))
5248, 51mpbird 247 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑁 / (𝑃𝑘)) − 1) < (⌊‘(𝑁 / (𝑃𝑘))))
53 2pos 11097 . . . . . . . . . . . . . . 15 0 < 2
5437, 53pm3.2i 471 . . . . . . . . . . . . . 14 (2 ∈ ℝ ∧ 0 < 2)
55 ltmul2 10859 . . . . . . . . . . . . . 14 ((((𝑁 / (𝑃𝑘)) − 1) ∈ ℝ ∧ (⌊‘(𝑁 / (𝑃𝑘))) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑁 / (𝑃𝑘)) − 1) < (⌊‘(𝑁 / (𝑃𝑘))) ↔ (2 · ((𝑁 / (𝑃𝑘)) − 1)) < (2 · (⌊‘(𝑁 / (𝑃𝑘))))))
5654, 55mp3an3 1411 . . . . . . . . . . . . 13 ((((𝑁 / (𝑃𝑘)) − 1) ∈ ℝ ∧ (⌊‘(𝑁 / (𝑃𝑘))) ∈ ℝ) → (((𝑁 / (𝑃𝑘)) − 1) < (⌊‘(𝑁 / (𝑃𝑘))) ↔ (2 · ((𝑁 / (𝑃𝑘)) − 1)) < (2 · (⌊‘(𝑁 / (𝑃𝑘))))))
5744, 50, 56syl2anc 692 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((𝑁 / (𝑃𝑘)) − 1) < (⌊‘(𝑁 / (𝑃𝑘))) ↔ (2 · ((𝑁 / (𝑃𝑘)) − 1)) < (2 · (⌊‘(𝑁 / (𝑃𝑘))))))
5852, 57mpbid 222 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · ((𝑁 / (𝑃𝑘)) − 1)) < (2 · (⌊‘(𝑁 / (𝑃𝑘)))))
5946, 35, 17, 58ltsub2dd 10625 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃𝑘)) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) < (((2 · 𝑁) / (𝑃𝑘)) − (2 · ((𝑁 / (𝑃𝑘)) − 1))))
60 2cnd 11078 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 2 ∈ ℂ)
61 nncn 11013 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
6261ad2antrr 761 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑁 ∈ ℂ)
6311nncnd 11021 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑃𝑘) ∈ ℂ)
6411nnne0d 11050 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑃𝑘) ≠ 0)
6560, 62, 63, 64divassd 10821 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) / (𝑃𝑘)) = (2 · (𝑁 / (𝑃𝑘))))
6625recnd 10053 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑁 / (𝑃𝑘)) ∈ ℂ)
67 1cnd 10041 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 1 ∈ ℂ)
6860, 66, 67subdid 10471 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · ((𝑁 / (𝑃𝑘)) − 1)) = ((2 · (𝑁 / (𝑃𝑘))) − (2 · 1)))
69 2t1e2 11161 . . . . . . . . . . . . . 14 (2 · 1) = 2
7069oveq2i 6646 . . . . . . . . . . . . 13 ((2 · (𝑁 / (𝑃𝑘))) − (2 · 1)) = ((2 · (𝑁 / (𝑃𝑘))) − 2)
7168, 70syl6eq 2670 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · ((𝑁 / (𝑃𝑘)) − 1)) = ((2 · (𝑁 / (𝑃𝑘))) − 2))
7265, 71oveq12d 6653 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃𝑘)) − (2 · ((𝑁 / (𝑃𝑘)) − 1))) = ((2 · (𝑁 / (𝑃𝑘))) − ((2 · (𝑁 / (𝑃𝑘))) − 2)))
73 remulcl 10006 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ (𝑁 / (𝑃𝑘)) ∈ ℝ) → (2 · (𝑁 / (𝑃𝑘))) ∈ ℝ)
7437, 25, 73sylancr 694 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · (𝑁 / (𝑃𝑘))) ∈ ℝ)
7574recnd 10053 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · (𝑁 / (𝑃𝑘))) ∈ ℂ)
76 2cn 11076 . . . . . . . . . . . 12 2 ∈ ℂ
77 nncan 10295 . . . . . . . . . . . 12 (((2 · (𝑁 / (𝑃𝑘))) ∈ ℂ ∧ 2 ∈ ℂ) → ((2 · (𝑁 / (𝑃𝑘))) − ((2 · (𝑁 / (𝑃𝑘))) − 2)) = 2)
7875, 76, 77sylancl 693 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · (𝑁 / (𝑃𝑘))) − ((2 · (𝑁 / (𝑃𝑘))) − 2)) = 2)
7972, 78eqtrd 2654 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃𝑘)) − (2 · ((𝑁 / (𝑃𝑘)) − 1))) = 2)
8059, 79breqtrd 4670 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃𝑘)) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) < 2)
8130, 36, 38, 42, 80lelttrd 10180 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) < 2)
82 df-2 11064 . . . . . . . 8 2 = (1 + 1)
8381, 82syl6breq 4685 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) < (1 + 1))
84 1z 11392 . . . . . . . 8 1 ∈ ℤ
85 zleltp1 11413 . . . . . . . 8 ((((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ∈ ℤ ∧ 1 ∈ ℤ) → (((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ 1 ↔ ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) < (1 + 1)))
8629, 84, 85sylancl 693 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ 1 ↔ ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) < (1 + 1)))
8783, 86mpbird 247 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ 1)
88 iftrue 4083 . . . . . . 7 (𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0) = 1)
8988breq2d 4656 . . . . . 6 (𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → (((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0) ↔ ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ 1))
9087, 89syl5ibrcom 237 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0)))
919nnge1d 11048 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 1 ≤ 𝑘)
9291biantrurd 529 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑘 ≤ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ↔ (1 ≤ 𝑘𝑘 ≤ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))))
936adantl 482 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈ ℕ)
9493nnred 11020 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈ ℝ)
95 prmuz2 15389 . . . . . . . . . . . . . . 15 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
9695adantl 482 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈ (ℤ‘2))
97 eluz2b1 11744 . . . . . . . . . . . . . . 15 (𝑃 ∈ (ℤ‘2) ↔ (𝑃 ∈ ℤ ∧ 1 < 𝑃))
9897simprbi 480 . . . . . . . . . . . . . 14 (𝑃 ∈ (ℤ‘2) → 1 < 𝑃)
9996, 98syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 1 < 𝑃)
10094, 99jca 554 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
101100adantr 481 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
102 elfzelz 12327 . . . . . . . . . . . 12 (𝑘 ∈ (1...(2 · 𝑁)) → 𝑘 ∈ ℤ)
103102adantl 482 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑘 ∈ ℤ)
1044adantr 481 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2 · 𝑁) ∈ ℕ)
105104nnrpd 11855 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2 · 𝑁) ∈ ℝ+)
106105adantr 481 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · 𝑁) ∈ ℝ+)
107 efexple 24987 . . . . . . . . . . 11 (((𝑃 ∈ ℝ ∧ 1 < 𝑃) ∧ 𝑘 ∈ ℤ ∧ (2 · 𝑁) ∈ ℝ+) → ((𝑃𝑘) ≤ (2 · 𝑁) ↔ 𝑘 ≤ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))))
108101, 103, 106, 107syl3anc 1324 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑃𝑘) ≤ (2 · 𝑁) ↔ 𝑘 ≤ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))))
1099nnzd 11466 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑘 ∈ ℤ)
11084a1i 11 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 1 ∈ ℤ)
111104nnred 11020 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2 · 𝑁) ∈ ℝ)
112 1red 10040 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 1 ∈ ℝ)
11337a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 2 ∈ ℝ)
114 1lt2 11179 . . . . . . . . . . . . . . . . . 18 1 < 2
115114a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 1 < 2)
116 nnre 11012 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
117116adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑁 ∈ ℝ)
118 0le2 11096 . . . . . . . . . . . . . . . . . . . . 21 0 ≤ 2
11937, 118pm3.2i 471 . . . . . . . . . . . . . . . . . . . 20 (2 ∈ ℝ ∧ 0 ≤ 2)
120119a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2 ∈ ℝ ∧ 0 ≤ 2))
121 nnge1 11031 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 1 ≤ 𝑁)
122121adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 1 ≤ 𝑁)
123 lemul2a 10863 . . . . . . . . . . . . . . . . . . 19 (((1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 ≤ 2)) ∧ 1 ≤ 𝑁) → (2 · 1) ≤ (2 · 𝑁))
124112, 117, 120, 122, 123syl31anc 1327 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2 · 1) ≤ (2 · 𝑁))
12569, 124syl5eqbrr 4680 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 2 ≤ (2 · 𝑁))
126112, 113, 111, 115, 125ltletrd 10182 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 1 < (2 · 𝑁))
127111, 126rplogcld 24356 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (log‘(2 · 𝑁)) ∈ ℝ+)
12894, 99rplogcld 24356 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (log‘𝑃) ∈ ℝ+)
129127, 128rpdivcld 11874 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((log‘(2 · 𝑁)) / (log‘𝑃)) ∈ ℝ+)
130129rpred 11857 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((log‘(2 · 𝑁)) / (log‘𝑃)) ∈ ℝ)
131130flcld 12582 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℤ)
132131adantr 481 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℤ)
133 elfz 12317 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ 1 ∈ ℤ ∧ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℤ) → (𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ↔ (1 ≤ 𝑘𝑘 ≤ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))))
134109, 110, 132, 133syl3anc 1324 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ↔ (1 ≤ 𝑘𝑘 ≤ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))))
13592, 108, 1343bitr4rd 301 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ↔ (𝑃𝑘) ≤ (2 · 𝑁)))
136135notbid 308 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (¬ 𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ↔ ¬ (𝑃𝑘) ≤ (2 · 𝑁)))
137111adantr 481 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · 𝑁) ∈ ℝ)
13811nnred 11020 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑃𝑘) ∈ ℝ)
139137, 138ltnled 10169 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) < (𝑃𝑘) ↔ ¬ (𝑃𝑘) ≤ (2 · 𝑁)))
140136, 139bitr4d 271 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (¬ 𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ↔ (2 · 𝑁) < (𝑃𝑘)))
14116rpge0d 11861 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 0 ≤ ((2 · 𝑁) / (𝑃𝑘)))
142141adantrr 752 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → 0 ≤ ((2 · 𝑁) / (𝑃𝑘)))
14311nngt0d 11049 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 0 < (𝑃𝑘))
144 ltdivmul 10883 . . . . . . . . . . . . . . . . 17 (((2 · 𝑁) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝑃𝑘) ∈ ℝ ∧ 0 < (𝑃𝑘))) → (((2 · 𝑁) / (𝑃𝑘)) < 1 ↔ (2 · 𝑁) < ((𝑃𝑘) · 1)))
145137, 49, 138, 143, 144syl112anc 1328 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃𝑘)) < 1 ↔ (2 · 𝑁) < ((𝑃𝑘) · 1)))
14663mulid1d 10042 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑃𝑘) · 1) = (𝑃𝑘))
147146breq2d 4656 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) < ((𝑃𝑘) · 1) ↔ (2 · 𝑁) < (𝑃𝑘)))
148145, 147bitrd 268 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃𝑘)) < 1 ↔ (2 · 𝑁) < (𝑃𝑘)))
149148biimprd 238 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) < (𝑃𝑘) → ((2 · 𝑁) / (𝑃𝑘)) < 1))
150149impr 648 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → ((2 · 𝑁) / (𝑃𝑘)) < 1)
151 0p1e1 11117 . . . . . . . . . . . . 13 (0 + 1) = 1
152150, 151syl6breqr 4686 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → ((2 · 𝑁) / (𝑃𝑘)) < (0 + 1))
15317adantrr 752 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → ((2 · 𝑁) / (𝑃𝑘)) ∈ ℝ)
154 0z 11373 . . . . . . . . . . . . 13 0 ∈ ℤ
155 flbi 12600 . . . . . . . . . . . . 13 ((((2 · 𝑁) / (𝑃𝑘)) ∈ ℝ ∧ 0 ∈ ℤ) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) = 0 ↔ (0 ≤ ((2 · 𝑁) / (𝑃𝑘)) ∧ ((2 · 𝑁) / (𝑃𝑘)) < (0 + 1))))
156153, 154, 155sylancl 693 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) = 0 ↔ (0 ≤ ((2 · 𝑁) / (𝑃𝑘)) ∧ ((2 · 𝑁) / (𝑃𝑘)) < (0 + 1))))
157142, 152, 156mpbir2and 956 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → (⌊‘((2 · 𝑁) / (𝑃𝑘))) = 0)
15824rpge0d 11861 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 0 ≤ (𝑁 / (𝑃𝑘)))
159158adantrr 752 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → 0 ≤ (𝑁 / (𝑃𝑘)))
160116, 21ltaddrp2d 11891 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 𝑁))
161612timesd 11260 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → (2 · 𝑁) = (𝑁 + 𝑁))
162160, 161breqtrrd 4672 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → 𝑁 < (2 · 𝑁))
163162ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑁 < (2 · 𝑁))
164116ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑁 ∈ ℝ)
165 lttr 10099 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ (𝑃𝑘) ∈ ℝ) → ((𝑁 < (2 · 𝑁) ∧ (2 · 𝑁) < (𝑃𝑘)) → 𝑁 < (𝑃𝑘)))
166164, 137, 138, 165syl3anc 1324 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑁 < (2 · 𝑁) ∧ (2 · 𝑁) < (𝑃𝑘)) → 𝑁 < (𝑃𝑘)))
167163, 166mpand 710 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) < (𝑃𝑘) → 𝑁 < (𝑃𝑘)))
168 ltdivmul 10883 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝑃𝑘) ∈ ℝ ∧ 0 < (𝑃𝑘))) → ((𝑁 / (𝑃𝑘)) < 1 ↔ 𝑁 < ((𝑃𝑘) · 1)))
169164, 49, 138, 143, 168syl112anc 1328 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑁 / (𝑃𝑘)) < 1 ↔ 𝑁 < ((𝑃𝑘) · 1)))
170146breq2d 4656 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑁 < ((𝑃𝑘) · 1) ↔ 𝑁 < (𝑃𝑘)))
171169, 170bitrd 268 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑁 / (𝑃𝑘)) < 1 ↔ 𝑁 < (𝑃𝑘)))
172167, 171sylibrd 249 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) < (𝑃𝑘) → (𝑁 / (𝑃𝑘)) < 1))
173172impr 648 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → (𝑁 / (𝑃𝑘)) < 1)
174173, 151syl6breqr 4686 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → (𝑁 / (𝑃𝑘)) < (0 + 1))
17525adantrr 752 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → (𝑁 / (𝑃𝑘)) ∈ ℝ)
176 flbi 12600 . . . . . . . . . . . . . . 15 (((𝑁 / (𝑃𝑘)) ∈ ℝ ∧ 0 ∈ ℤ) → ((⌊‘(𝑁 / (𝑃𝑘))) = 0 ↔ (0 ≤ (𝑁 / (𝑃𝑘)) ∧ (𝑁 / (𝑃𝑘)) < (0 + 1))))
177175, 154, 176sylancl 693 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → ((⌊‘(𝑁 / (𝑃𝑘))) = 0 ↔ (0 ≤ (𝑁 / (𝑃𝑘)) ∧ (𝑁 / (𝑃𝑘)) < (0 + 1))))
178159, 174, 177mpbir2and 956 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → (⌊‘(𝑁 / (𝑃𝑘))) = 0)
179178oveq2d 6651 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → (2 · (⌊‘(𝑁 / (𝑃𝑘)))) = (2 · 0))
180 2t0e0 11168 . . . . . . . . . . . 12 (2 · 0) = 0
181179, 180syl6eq 2670 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → (2 · (⌊‘(𝑁 / (𝑃𝑘)))) = 0)
182157, 181oveq12d 6653 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) = (0 − 0))
183 0m0e0 11115 . . . . . . . . . 10 (0 − 0) = 0
184182, 183syl6eq 2670 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) = 0)
185 0le0 11095 . . . . . . . . 9 0 ≤ 0
186184, 185syl6eqbr 4683 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃𝑘))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ 0)
187186expr 642 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) < (𝑃𝑘) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ 0))
188140, 187sylbid 230 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (¬ 𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ 0))
189 iffalse 4086 . . . . . . . 8 𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0) = 0)
190189eqcomd 2626 . . . . . . 7 𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → 0 = if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0))
191190breq2d 4656 . . . . . 6 𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → (((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ 0 ↔ ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0)))
192188, 191mpbidi 231 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (¬ 𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0)))
19390, 192pm2.61d 170 . . . 4 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0))
1941, 30, 34, 193fsumle 14512 . . 3 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))) ≤ Σ𝑘 ∈ (1...(2 · 𝑁))if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0))
195 pcbcctr 24982 . . 3 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃𝑘))) − (2 · (⌊‘(𝑁 / (𝑃𝑘))))))
196131zred 11467 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℝ)
197 flle 12583 . . . . . . . . 9 (((log‘(2 · 𝑁)) / (log‘𝑃)) ∈ ℝ → (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ≤ ((log‘(2 · 𝑁)) / (log‘𝑃)))
198130, 197syl 17 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ≤ ((log‘(2 · 𝑁)) / (log‘𝑃)))
199104nnnn0d 11336 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2 · 𝑁) ∈ ℕ0)
20093, 199nnexpcld 13013 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(2 · 𝑁)) ∈ ℕ)
201200nnred 11020 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(2 · 𝑁)) ∈ ℝ)
202 bernneq3 12975 . . . . . . . . . . . . 13 ((𝑃 ∈ (ℤ‘2) ∧ (2 · 𝑁) ∈ ℕ0) → (2 · 𝑁) < (𝑃↑(2 · 𝑁)))
20396, 199, 202syl2anc 692 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2 · 𝑁) < (𝑃↑(2 · 𝑁)))
204111, 201, 203ltled 10170 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2 · 𝑁) ≤ (𝑃↑(2 · 𝑁)))
205105reeflogd 24351 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (exp‘(log‘(2 · 𝑁))) = (2 · 𝑁))
20693nnrpd 11855 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈ ℝ+)
207104nnzd 11466 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2 · 𝑁) ∈ ℤ)
208 reexplog 24322 . . . . . . . . . . . . 13 ((𝑃 ∈ ℝ+ ∧ (2 · 𝑁) ∈ ℤ) → (𝑃↑(2 · 𝑁)) = (exp‘((2 · 𝑁) · (log‘𝑃))))
209206, 207, 208syl2anc 692 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(2 · 𝑁)) = (exp‘((2 · 𝑁) · (log‘𝑃))))
210209eqcomd 2626 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (exp‘((2 · 𝑁) · (log‘𝑃))) = (𝑃↑(2 · 𝑁)))
211204, 205, 2103brtr4d 4676 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (exp‘(log‘(2 · 𝑁))) ≤ (exp‘((2 · 𝑁) · (log‘𝑃))))
212105relogcld 24350 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (log‘(2 · 𝑁)) ∈ ℝ)
213128rpred 11857 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (log‘𝑃) ∈ ℝ)
214111, 213remulcld 10055 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((2 · 𝑁) · (log‘𝑃)) ∈ ℝ)
215 efle 14829 . . . . . . . . . . 11 (((log‘(2 · 𝑁)) ∈ ℝ ∧ ((2 · 𝑁) · (log‘𝑃)) ∈ ℝ) → ((log‘(2 · 𝑁)) ≤ ((2 · 𝑁) · (log‘𝑃)) ↔ (exp‘(log‘(2 · 𝑁))) ≤ (exp‘((2 · 𝑁) · (log‘𝑃)))))
216212, 214, 215syl2anc 692 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((log‘(2 · 𝑁)) ≤ ((2 · 𝑁) · (log‘𝑃)) ↔ (exp‘(log‘(2 · 𝑁))) ≤ (exp‘((2 · 𝑁) · (log‘𝑃)))))
217211, 216mpbird 247 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (log‘(2 · 𝑁)) ≤ ((2 · 𝑁) · (log‘𝑃)))
218212, 111, 128ledivmul2d 11911 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (((log‘(2 · 𝑁)) / (log‘𝑃)) ≤ (2 · 𝑁) ↔ (log‘(2 · 𝑁)) ≤ ((2 · 𝑁) · (log‘𝑃))))
219217, 218mpbird 247 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((log‘(2 · 𝑁)) / (log‘𝑃)) ≤ (2 · 𝑁))
220196, 130, 111, 198, 219letrd 10179 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ≤ (2 · 𝑁))
221 eluz 11686 . . . . . . . 8 (((⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ) → ((2 · 𝑁) ∈ (ℤ‘(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ↔ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ≤ (2 · 𝑁)))
222131, 207, 221syl2anc 692 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((2 · 𝑁) ∈ (ℤ‘(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ↔ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ≤ (2 · 𝑁)))
223220, 222mpbird 247 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2 · 𝑁) ∈ (ℤ‘(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))))
224 fzss2 12366 . . . . . 6 ((2 · 𝑁) ∈ (ℤ‘(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ⊆ (1...(2 · 𝑁)))
225223, 224syl 17 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ⊆ (1...(2 · 𝑁)))
226 sumhash 15581 . . . . 5 (((1...(2 · 𝑁)) ∈ Fin ∧ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ⊆ (1...(2 · 𝑁))) → Σ𝑘 ∈ (1...(2 · 𝑁))if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0) = (#‘(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))))
2271, 225, 226syl2anc 692 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → Σ𝑘 ∈ (1...(2 · 𝑁))if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0) = (#‘(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))))
228129rprege0d 11864 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (((log‘(2 · 𝑁)) / (log‘𝑃)) ∈ ℝ ∧ 0 ≤ ((log‘(2 · 𝑁)) / (log‘𝑃))))
229 flge0nn0 12604 . . . . 5 ((((log‘(2 · 𝑁)) / (log‘𝑃)) ∈ ℝ ∧ 0 ≤ ((log‘(2 · 𝑁)) / (log‘𝑃))) → (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℕ0)
230 hashfz1 13117 . . . . 5 ((⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℕ0 → (#‘(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))) = (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))
231228, 229, 2303syl 18 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (#‘(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))) = (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))
232227, 231eqtr2d 2655 . . 3 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) = Σ𝑘 ∈ (1...(2 · 𝑁))if(𝑘 ∈ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0))
233194, 195, 2323brtr4d 4676 . 2 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) ≤ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))
234 simpr 477 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈ ℙ)
235 nnnn0 11284 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
236 fzctr 12435 . . . . . . 7 (𝑁 ∈ ℕ0𝑁 ∈ (0...(2 · 𝑁)))
237 bccl2 13093 . . . . . . 7 (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
238235, 236, 2373syl 18 . . . . . 6 (𝑁 ∈ ℕ → ((2 · 𝑁)C𝑁) ∈ ℕ)
239238adantr 481 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((2 · 𝑁)C𝑁) ∈ ℕ)
240234, 239pccld 15536 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
241240nn0zd 11465 . . 3 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ)
242 efexple 24987 . . 3 (((𝑃 ∈ ℝ ∧ 1 < 𝑃) ∧ (𝑃 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ ∧ (2 · 𝑁) ∈ ℝ+) → ((𝑃↑(𝑃 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ↔ (𝑃 pCnt ((2 · 𝑁)C𝑁)) ≤ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))))
24394, 99, 241, 105, 242syl211anc 1330 . 2 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((𝑃↑(𝑃 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ↔ (𝑃 pCnt ((2 · 𝑁)C𝑁)) ≤ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))))
244233, 243mpbird 247 1 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(𝑃 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  wss 3567  ifcif 4077   class class class wbr 4644  cfv 5876  (class class class)co 6635  Fincfn 7940  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926   < clt 10059  cle 10060  cmin 10251   / cdiv 10669  cn 11005  2c2 11055  0cn0 11277  cz 11362  cuz 11672  +crp 11817  ...cfz 12311  cfl 12574  cexp 12843  Ccbc 13072  #chash 13100  Σcsu 14397  expce 14773  cprime 15366   pCnt cpc 15522  logclog 24282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999  ax-addf 10000  ax-mulf 10001
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-iin 4514  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-om 7051  df-1st 7153  df-2nd 7154  df-supp 7281  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-map 7844  df-pm 7845  df-ixp 7894  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fsupp 8261  df-fi 8302  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-cda 8975  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071  df-n0 11278  df-z 11363  df-dec 11479  df-uz 11673  df-q 11774  df-rp 11818  df-xneg 11931  df-xadd 11932  df-xmul 11933  df-ioo 12164  df-ioc 12165  df-ico 12166  df-icc 12167  df-fz 12312  df-fzo 12450  df-fl 12576  df-mod 12652  df-seq 12785  df-exp 12844  df-fac 13044  df-bc 13073  df-hash 13101  df-shft 13788  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-limsup 14183  df-clim 14200  df-rlim 14201  df-sum 14398  df-ef 14779  df-sin 14781  df-cos 14782  df-pi 14784  df-dvds 14965  df-gcd 15198  df-prm 15367  df-pc 15523  df-struct 15840  df-ndx 15841  df-slot 15842  df-base 15844  df-sets 15845  df-ress 15846  df-plusg 15935  df-mulr 15936  df-starv 15937  df-sca 15938  df-vsca 15939  df-ip 15940  df-tset 15941  df-ple 15942  df-ds 15945  df-unif 15946  df-hom 15947  df-cco 15948  df-rest 16064  df-topn 16065  df-0g 16083  df-gsum 16084  df-topgen 16085  df-pt 16086  df-prds 16089  df-xrs 16143  df-qtop 16148  df-imas 16149  df-xps 16151  df-mre 16227  df-mrc 16228  df-acs 16230  df-mgm 17223  df-sgrp 17265  df-mnd 17276  df-submnd 17317  df-mulg 17522  df-cntz 17731  df-cmn 18176  df-psmet 19719  df-xmet 19720  df-met 19721  df-bl 19722  df-mopn 19723  df-fbas 19724  df-fg 19725  df-cnfld 19728  df-top 20680  df-topon 20697  df-topsp 20718  df-bases 20731  df-cld 20804  df-ntr 20805  df-cls 20806  df-nei 20883  df-lp 20921  df-perf 20922  df-cn 21012  df-cnp 21013  df-haus 21100  df-tx 21346  df-hmeo 21539  df-fil 21631  df-fm 21723  df-flim 21724  df-flf 21725  df-xms 22106  df-ms 22107  df-tms 22108  df-cncf 22662  df-limc 23611  df-dv 23612  df-log 24284
This theorem is referenced by:  bposlem5  24994  bposlem6  24995  chebbnd1lem1  25139
  Copyright terms: Public domain W3C validator