Proof of Theorem bcmax
| Step | Hyp | Ref
| Expression |
| 1 | | 2nn0 12543 |
. . . 4
⊢ 2 ∈
ℕ0 |
| 2 | | simpll 767 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝑁 ∈
(ℤ≥‘𝐾)) → 𝑁 ∈
ℕ0) |
| 3 | | nn0mulcl 12562 |
. . . 4
⊢ ((2
∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (2
· 𝑁) ∈
ℕ0) |
| 4 | 1, 2, 3 | sylancr 587 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝑁 ∈
(ℤ≥‘𝐾)) → (2 · 𝑁) ∈
ℕ0) |
| 5 | | simpr 484 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝑁 ∈
(ℤ≥‘𝐾)) → 𝑁 ∈ (ℤ≥‘𝐾)) |
| 6 | | nn0re 12535 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
| 7 | 6 | leidd 11829 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ≤ 𝑁) |
| 8 | | nn0cn 12536 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
| 9 | | 2cn 12341 |
. . . . . . 7
⊢ 2 ∈
ℂ |
| 10 | | 2ne0 12370 |
. . . . . . 7
⊢ 2 ≠
0 |
| 11 | | divcan3 11948 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → ((2 · 𝑁) / 2) = 𝑁) |
| 12 | 9, 10, 11 | mp3an23 1455 |
. . . . . 6
⊢ (𝑁 ∈ ℂ → ((2
· 𝑁) / 2) = 𝑁) |
| 13 | 8, 12 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((2 · 𝑁) / 2)
= 𝑁) |
| 14 | 7, 13 | breqtrrd 5171 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ≤ ((2 ·
𝑁) / 2)) |
| 15 | 2, 14 | syl 17 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝑁 ∈
(ℤ≥‘𝐾)) → 𝑁 ≤ ((2 · 𝑁) / 2)) |
| 16 | | bcmono 27321 |
. . 3
⊢ (((2
· 𝑁) ∈
ℕ0 ∧ 𝑁
∈ (ℤ≥‘𝐾) ∧ 𝑁 ≤ ((2 · 𝑁) / 2)) → ((2 · 𝑁)C𝐾) ≤ ((2 · 𝑁)C𝑁)) |
| 17 | 4, 5, 15, 16 | syl3anc 1373 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝑁 ∈
(ℤ≥‘𝐾)) → ((2 · 𝑁)C𝐾) ≤ ((2 · 𝑁)C𝑁)) |
| 18 | | simpll 767 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈
ℕ0) |
| 19 | 1, 18, 3 | sylancr 587 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → (2 · 𝑁) ∈
ℕ0) |
| 20 | | simplr 769 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → 𝐾 ∈ ℤ) |
| 21 | | bccmpl 14348 |
. . . 4
⊢ (((2
· 𝑁) ∈
ℕ0 ∧ 𝐾
∈ ℤ) → ((2 · 𝑁)C𝐾) = ((2 · 𝑁)C((2 · 𝑁) − 𝐾))) |
| 22 | 19, 20, 21 | syl2anc 584 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → ((2 · 𝑁)C𝐾) = ((2 · 𝑁)C((2 · 𝑁) − 𝐾))) |
| 23 | 18 | nn0red 12588 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈ ℝ) |
| 24 | 23 | recnd 11289 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈ ℂ) |
| 25 | 24 | 2timesd 12509 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → (2 · 𝑁) = (𝑁 + 𝑁)) |
| 26 | 20 | zred 12722 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → 𝐾 ∈ ℝ) |
| 27 | | eluzle 12891 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘𝑁) → 𝑁 ≤ 𝐾) |
| 28 | 27 | adantl 481 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → 𝑁 ≤ 𝐾) |
| 29 | 23, 26, 23, 28 | leadd2dd 11878 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → (𝑁 + 𝑁) ≤ (𝑁 + 𝐾)) |
| 30 | 25, 29 | eqbrtrd 5165 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → (2 · 𝑁) ≤ (𝑁 + 𝐾)) |
| 31 | 19 | nn0red 12588 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → (2 · 𝑁) ∈ ℝ) |
| 32 | 31, 26, 23 | lesubaddd 11860 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → (((2 · 𝑁) − 𝐾) ≤ 𝑁 ↔ (2 · 𝑁) ≤ (𝑁 + 𝐾))) |
| 33 | 30, 32 | mpbird 257 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → ((2 · 𝑁) − 𝐾) ≤ 𝑁) |
| 34 | 19 | nn0zd 12639 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → (2 · 𝑁) ∈ ℤ) |
| 35 | 34, 20 | zsubcld 12727 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → ((2 · 𝑁) − 𝐾) ∈ ℤ) |
| 36 | 18 | nn0zd 12639 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈ ℤ) |
| 37 | | eluz 12892 |
. . . . . 6
⊢ ((((2
· 𝑁) − 𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘((2 · 𝑁) − 𝐾)) ↔ ((2 · 𝑁) − 𝐾) ≤ 𝑁)) |
| 38 | 35, 36, 37 | syl2anc 584 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → (𝑁 ∈ (ℤ≥‘((2
· 𝑁) − 𝐾)) ↔ ((2 · 𝑁) − 𝐾) ≤ 𝑁)) |
| 39 | 33, 38 | mpbird 257 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈ (ℤ≥‘((2
· 𝑁) − 𝐾))) |
| 40 | 18, 14 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → 𝑁 ≤ ((2 · 𝑁) / 2)) |
| 41 | | bcmono 27321 |
. . . 4
⊢ (((2
· 𝑁) ∈
ℕ0 ∧ 𝑁
∈ (ℤ≥‘((2 · 𝑁) − 𝐾)) ∧ 𝑁 ≤ ((2 · 𝑁) / 2)) → ((2 · 𝑁)C((2 · 𝑁) − 𝐾)) ≤ ((2 · 𝑁)C𝑁)) |
| 42 | 19, 39, 40, 41 | syl3anc 1373 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → ((2 · 𝑁)C((2 · 𝑁) − 𝐾)) ≤ ((2 · 𝑁)C𝑁)) |
| 43 | 22, 42 | eqbrtrd 5165 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈
(ℤ≥‘𝑁)) → ((2 · 𝑁)C𝐾) ≤ ((2 · 𝑁)C𝑁)) |
| 44 | | simpr 484 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ 𝐾 ∈
ℤ) |
| 45 | | nn0z 12638 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 46 | 45 | adantr 480 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ 𝑁 ∈
ℤ) |
| 47 | | uztric 12902 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝐾) ∨ 𝐾 ∈ (ℤ≥‘𝑁))) |
| 48 | 44, 46, 47 | syl2anc 584 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ (𝑁 ∈
(ℤ≥‘𝐾) ∨ 𝐾 ∈ (ℤ≥‘𝑁))) |
| 49 | 17, 43, 48 | mpjaodan 961 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ ((2 · 𝑁)C𝐾) ≤ ((2 · 𝑁)C𝑁)) |