Step | Hyp | Ref
| Expression |
1 | | simpl2 1191 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐵 ∈ (ℤ≥‘𝐴)) |
2 | | simpl1 1190 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝑁 ∈
ℕ0) |
3 | | eluzel2 12597 |
. . . . . 6
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → 𝐴 ∈ ℤ) |
4 | 3 | 3ad2ant2 1133 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → 𝐴 ∈ ℤ) |
5 | 4 | anim1i 615 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴)) |
6 | | elnn0z 12342 |
. . . 4
⊢ (𝐴 ∈ ℕ0
↔ (𝐴 ∈ ℤ
∧ 0 ≤ 𝐴)) |
7 | 5, 6 | sylibr 233 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐴 ∈
ℕ0) |
8 | | simpl3 1192 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐵 ≤ (𝑁 / 2)) |
9 | | breq1 5076 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 ≤ (𝑁 / 2) ↔ 𝐴 ≤ (𝑁 / 2))) |
10 | | oveq2 7275 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑁C𝑥) = (𝑁C𝐴)) |
11 | 10 | breq2d 5085 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝐴))) |
12 | 9, 11 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))) |
13 | 12 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = 𝐴 → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))) |
14 | | breq1 5076 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 ≤ (𝑁 / 2) ↔ 𝑘 ≤ (𝑁 / 2))) |
15 | | oveq2 7275 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (𝑁C𝑥) = (𝑁C𝑘)) |
16 | 15 | breq2d 5085 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝑘))) |
17 | 14, 16 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)))) |
18 | 17 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = 𝑘 → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))))) |
19 | | breq1 5076 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (𝑥 ≤ (𝑁 / 2) ↔ (𝑘 + 1) ≤ (𝑁 / 2))) |
20 | | oveq2 7275 |
. . . . . . . 8
⊢ (𝑥 = (𝑘 + 1) → (𝑁C𝑥) = (𝑁C(𝑘 + 1))) |
21 | 20 | breq2d 5085 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))) |
22 | 19, 21 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))) |
23 | 22 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = (𝑘 + 1) → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))) |
24 | | breq1 5076 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥 ≤ (𝑁 / 2) ↔ 𝐵 ≤ (𝑁 / 2))) |
25 | | oveq2 7275 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝑁C𝑥) = (𝑁C𝐵)) |
26 | 25 | breq2d 5085 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝐵))) |
27 | 24, 26 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵)))) |
28 | 27 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = 𝐵 → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵))))) |
29 | | bccl 14046 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (𝑁C𝐴) ∈
ℕ0) |
30 | 29 | nn0red 12304 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (𝑁C𝐴) ∈ ℝ) |
31 | 30 | leidd 11551 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (𝑁C𝐴) ≤ (𝑁C𝐴)) |
32 | 31 | a1d 25 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))) |
33 | 32 | expcom 414 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝑁 ∈ ℕ0
→ (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))) |
34 | 33 | adantrd 492 |
. . . . 5
⊢ (𝐴 ∈ ℤ → ((𝑁 ∈ ℕ0
∧ 𝐴 ∈
ℕ0) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))) |
35 | | eluzelz 12602 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘𝐴) → 𝑘 ∈ ℤ) |
36 | 35 | 3ad2ant1 1132 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ 𝑘 ∈
ℤ) |
37 | 36 | zred 12436 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ 𝑘 ∈
ℝ) |
38 | 37 | lep1d 11916 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ 𝑘 ≤ (𝑘 + 1)) |
39 | | peano2re 11158 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
40 | 37, 39 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℝ) |
41 | | nn0re 12252 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
42 | 41 | 3ad2ant2 1133 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ 𝑁 ∈
ℝ) |
43 | 42 | rehalfcld 12230 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁 / 2) ∈
ℝ) |
44 | | letr 11079 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧
(𝑁 / 2) ∈ ℝ)
→ ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑁 / 2))) |
45 | 37, 40, 43, 44 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑁 / 2))) |
46 | 38, 45 | mpand 692 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 + 1) ≤ (𝑁 / 2) → 𝑘 ≤ (𝑁 / 2))) |
47 | 46 | imim1d 82 |
. . . . . . . 8
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)))) |
48 | | eluznn0 12667 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝐴)) → 𝑘 ∈ ℕ0) |
49 | 41 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℝ) |
50 | | nn0re 12252 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
51 | 50 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℝ) |
52 | | nn0p1nn 12282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ) |
53 | 52 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℕ) |
54 | 53 | nnnn0d 12303 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈
ℕ0) |
55 | 54 | nn0red 12304 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℝ) |
56 | 53 | nncnd 11999 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℂ) |
57 | 56 | 2timesd 12226 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 · (𝑘 + 1)) = ((𝑘 + 1) + (𝑘 + 1))) |
58 | | simp3 1137 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ (𝑁 / 2)) |
59 | | 2re 12057 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℝ |
60 | | 2pos 12086 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 <
2 |
61 | 59, 60 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℝ ∧ 0 < 2) |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 ∈ ℝ ∧ 0 <
2)) |
63 | | lemuldiv2 11866 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑘 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((2 · (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 / 2))) |
64 | 55, 49, 62, 63 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((2 · (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 / 2))) |
65 | 58, 64 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 · (𝑘 + 1)) ≤ 𝑁) |
66 | 57, 65 | eqbrtrrd 5097 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) + (𝑘 + 1)) ≤ 𝑁) |
67 | 51 | lep1d 11916 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑘 + 1)) |
68 | 49, 51, 55, 55, 66, 67 | lesub3d 11603 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ (𝑁 − 𝑘)) |
69 | | nnre 11990 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 + 1) ∈ ℕ →
(𝑘 + 1) ∈
ℝ) |
70 | | nngt0 12014 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 + 1) ∈ ℕ → 0
< (𝑘 +
1)) |
71 | 69, 70 | jca 512 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 + 1) ∈ ℕ →
((𝑘 + 1) ∈ ℝ
∧ 0 < (𝑘 +
1))) |
72 | 53, 71 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1))) |
73 | | nn0z 12353 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
74 | 73 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℤ) |
75 | | nn0z 12353 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
76 | 75 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℤ) |
77 | 74, 76 | zsubcld 12441 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − 𝑘) ∈ ℤ) |
78 | 49 | rehalfcld 12230 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 / 2) ∈ ℝ) |
79 | 49, 59 | jctir 521 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 ∈ ℝ ∧ 2 ∈
ℝ)) |
80 | | nn0ge0 12268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
81 | 80 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ 𝑁) |
82 | | 1le2 12192 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ≤
2 |
83 | 81, 82 | jctir 521 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (0 ≤ 𝑁 ∧ 1 ≤ 2)) |
84 | | lemulge12 11848 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℝ ∧ 2 ∈
ℝ) ∧ (0 ≤ 𝑁
∧ 1 ≤ 2)) → 𝑁
≤ (2 · 𝑁)) |
85 | 79, 83, 84 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ≤ (2 · 𝑁)) |
86 | | ledivmul 11861 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((𝑁 / 2) ≤ 𝑁 ↔ 𝑁 ≤ (2 · 𝑁))) |
87 | 49, 49, 62, 86 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁 / 2) ≤ 𝑁 ↔ 𝑁 ≤ (2 · 𝑁))) |
88 | 85, 87 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 / 2) ≤ 𝑁) |
89 | 55, 78, 49, 58, 88 | letrd 11142 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ 𝑁) |
90 | | 1red 10986 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ∈
ℝ) |
91 | 51, 90, 49 | leaddsub2d 11587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁 − 𝑘))) |
92 | 89, 91 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ≤ (𝑁 − 𝑘)) |
93 | | elnnz1 12356 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 𝑘) ∈ ℕ ↔ ((𝑁 − 𝑘) ∈ ℤ ∧ 1 ≤ (𝑁 − 𝑘))) |
94 | 77, 92, 93 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − 𝑘) ∈ ℕ) |
95 | | nnre 11990 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 𝑘) ∈ ℕ → (𝑁 − 𝑘) ∈ ℝ) |
96 | | nngt0 12014 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 𝑘) ∈ ℕ → 0 < (𝑁 − 𝑘)) |
97 | 95, 96 | jca 512 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 − 𝑘) ∈ ℕ → ((𝑁 − 𝑘) ∈ ℝ ∧ 0 < (𝑁 − 𝑘))) |
98 | 94, 97 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁 − 𝑘) ∈ ℝ ∧ 0 < (𝑁 − 𝑘))) |
99 | | faccl 14007 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
100 | 99 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑁) ∈ ℕ) |
101 | | nnm1nn0 12284 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 − 𝑘) ∈ ℕ → ((𝑁 − 𝑘) − 1) ∈
ℕ0) |
102 | | faccl 14007 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 − 𝑘) − 1) ∈ ℕ0
→ (!‘((𝑁 −
𝑘) − 1)) ∈
ℕ) |
103 | 94, 101, 102 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘((𝑁 − 𝑘) − 1)) ∈
ℕ) |
104 | | faccl 14007 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
105 | 104 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑘) ∈ ℕ) |
106 | 103, 105 | nnmulcld 12036 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈
ℕ) |
107 | | nnrp 12751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((!‘𝑁) ∈
ℕ → (!‘𝑁)
∈ ℝ+) |
108 | | nnrp 12751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((!‘((𝑁
− 𝑘) − 1))
· (!‘𝑘))
∈ ℕ → ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈
ℝ+) |
109 | | rpdivcl 12765 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((!‘𝑁) ∈
ℝ+ ∧ ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈ ℝ+)
→ ((!‘𝑁) /
((!‘((𝑁 − 𝑘) − 1)) ·
(!‘𝑘))) ∈
ℝ+) |
110 | 107, 108,
109 | syl2an 596 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((!‘𝑁) ∈
ℕ ∧ ((!‘((𝑁
− 𝑘) − 1))
· (!‘𝑘))
∈ ℕ) → ((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈
ℝ+) |
111 | 100, 106,
110 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈
ℝ+) |
112 | 111 | rpregt0d 12788 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈ ℝ ∧ 0 <
((!‘𝑁) /
((!‘((𝑁 − 𝑘) − 1)) ·
(!‘𝑘))))) |
113 | | lediv2 11875 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑘 + 1) ∈ ℝ ∧ 0
< (𝑘 + 1)) ∧ ((𝑁 − 𝑘) ∈ ℝ ∧ 0 < (𝑁 − 𝑘)) ∧ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈ ℝ ∧ 0 <
((!‘𝑁) /
((!‘((𝑁 − 𝑘) − 1)) ·
(!‘𝑘))))) →
((𝑘 + 1) ≤ (𝑁 − 𝑘) ↔ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)))) |
114 | 72, 98, 112, 113 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ≤ (𝑁 − 𝑘) ↔ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)))) |
115 | 68, 114 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1))) |
116 | | facnn2 14006 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 − 𝑘) ∈ ℕ → (!‘(𝑁 − 𝑘)) = ((!‘((𝑁 − 𝑘) − 1)) · (𝑁 − 𝑘))) |
117 | 94, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑁 − 𝑘)) = ((!‘((𝑁 − 𝑘) − 1)) · (𝑁 − 𝑘))) |
118 | 117 | oveq1d 7282 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − 𝑘)) · (!‘𝑘)) = (((!‘((𝑁 − 𝑘) − 1)) · (𝑁 − 𝑘)) · (!‘𝑘))) |
119 | 103 | nncnd 11999 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘((𝑁 − 𝑘) − 1)) ∈
ℂ) |
120 | 105 | nncnd 11999 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑘) ∈ ℂ) |
121 | 77 | zcnd 12437 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − 𝑘) ∈ ℂ) |
122 | 119, 120,
121 | mul32d 11195 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑁 − 𝑘)) = (((!‘((𝑁 − 𝑘) − 1)) · (𝑁 − 𝑘)) · (!‘𝑘))) |
123 | 118, 122 | eqtr4d 2781 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − 𝑘)) · (!‘𝑘)) = (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑁 − 𝑘))) |
124 | 123 | oveq2d 7283 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘(𝑁 − 𝑘)) · (!‘𝑘))) = ((!‘𝑁) / (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑁 − 𝑘)))) |
125 | | 0zd 12341 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ∈
ℤ) |
126 | | nn0ge0 12268 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ 0 ≤ 𝑘) |
127 | 126 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ 𝑘) |
128 | 51, 55, 49, 67, 89 | letrd 11142 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ 𝑁) |
129 | 125, 74, 76, 127, 128 | elfzd 13257 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ (0...𝑁)) |
130 | | bcval2 14029 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) = ((!‘𝑁) / ((!‘(𝑁 − 𝑘)) · (!‘𝑘)))) |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) = ((!‘𝑁) / ((!‘(𝑁 − 𝑘)) · (!‘𝑘)))) |
132 | 100 | nncnd 11999 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑁) ∈ ℂ) |
133 | 106 | nncnd 11999 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈
ℂ) |
134 | 106 | nnne0d 12033 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ≠ 0) |
135 | 94 | nnne0d 12033 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − 𝑘) ≠ 0) |
136 | 132, 133,
121, 134, 135 | divdiv1d 11792 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)) = ((!‘𝑁) / (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑁 − 𝑘)))) |
137 | 124, 131,
136 | 3eqtr4d 2788 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) = (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘))) |
138 | | nn0cn 12253 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
139 | 138 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℂ) |
140 | | nn0cn 12253 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
141 | 140 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℂ) |
142 | | 1cnd 10980 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ∈
ℂ) |
143 | 139, 141,
142 | subsub4d 11373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁 − 𝑘) − 1) = (𝑁 − (𝑘 + 1))) |
144 | 143 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − (𝑘 + 1)) = ((𝑁 − 𝑘) − 1)) |
145 | 144 | fveq2d 6770 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑁 − (𝑘 + 1))) = (!‘((𝑁 − 𝑘) − 1))) |
146 | | facp1 14002 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1)) =
((!‘𝑘) ·
(𝑘 + 1))) |
147 | 146 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1))) |
148 | 145, 147 | oveq12d 7285 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))) = ((!‘((𝑁 − 𝑘) − 1)) · ((!‘𝑘) · (𝑘 + 1)))) |
149 | 119, 120,
56 | mulassd 11008 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)) = ((!‘((𝑁 − 𝑘) − 1)) · ((!‘𝑘) · (𝑘 + 1)))) |
150 | 148, 149 | eqtr4d 2781 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))) = (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1))) |
151 | 150 | oveq2d 7283 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))) = ((!‘𝑁) / (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)))) |
152 | 53 | nnzd 12435 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℤ) |
153 | 54 | nn0ge0d 12306 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ (𝑘 + 1)) |
154 | 125, 74, 152, 153, 89 | elfzd 13257 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ (0...𝑁)) |
155 | | bcval2 14029 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 + 1) ∈ (0...𝑁) → (𝑁C(𝑘 + 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))))) |
156 | 154, 155 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C(𝑘 + 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))))) |
157 | 53 | nnne0d 12033 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≠ 0) |
158 | 132, 133,
56, 134, 157 | divdiv1d 11792 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)) = ((!‘𝑁) / (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)))) |
159 | 151, 156,
158 | 3eqtr4d 2788 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C(𝑘 + 1)) = (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1))) |
160 | 115, 137,
159 | 3brtr4d 5105 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) |
161 | 160 | 3exp 1118 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (𝑁 ∈
ℕ0 → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))))) |
162 | 48, 161 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝐴)) → (𝑁 ∈ ℕ0 → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))))) |
163 | 162 | 3impia 1116 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))) |
164 | 163 | 3coml 1126 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))) |
165 | | simp2 1136 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
166 | | nn0z 12353 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℤ) |
167 | 166 | 3ad2ant3 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ 𝐴 ∈
ℤ) |
168 | 165, 167,
29 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁C𝐴) ∈
ℕ0) |
169 | 168 | nn0red 12304 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁C𝐴) ∈ ℝ) |
170 | | bccl 14046 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) |
171 | 165, 36, 170 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁C𝑘) ∈
ℕ0) |
172 | 171 | nn0red 12304 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁C𝑘) ∈
ℝ) |
173 | 36 | peano2zd 12439 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℤ) |
174 | | bccl 14046 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑘 + 1) ∈
ℤ) → (𝑁C(𝑘 + 1)) ∈
ℕ0) |
175 | 165, 173,
174 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁C(𝑘 + 1)) ∈
ℕ0) |
176 | 175 | nn0red 12304 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁C(𝑘 + 1)) ∈
ℝ) |
177 | | letr 11079 |
. . . . . . . . . . . 12
⊢ (((𝑁C𝐴) ∈ ℝ ∧ (𝑁C𝑘) ∈ ℝ ∧ (𝑁C(𝑘 + 1)) ∈ ℝ) → (((𝑁C𝐴) ≤ (𝑁C𝑘) ∧ (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))) |
178 | 169, 172,
176, 177 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (((𝑁C𝐴) ≤ (𝑁C𝑘) ∧ (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))) |
179 | 178 | expcomd 417 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)) → ((𝑁C𝐴) ≤ (𝑁C𝑘) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))) |
180 | 164, 179 | syld 47 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 + 1) ≤ (𝑁 / 2) → ((𝑁C𝐴) ≤ (𝑁C𝑘) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))) |
181 | 180 | a2d 29 |
. . . . . . . 8
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (((𝑘 + 1) ≤
(𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))) |
182 | 47, 181 | syld 47 |
. . . . . . 7
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))) |
183 | 182 | 3expib 1121 |
. . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘𝐴) → ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))) |
184 | 183 | a2d 29 |
. . . . 5
⊢ (𝑘 ∈
(ℤ≥‘𝐴) → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))) → ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))) |
185 | 13, 18, 23, 28, 34, 184 | uzind4 12656 |
. . . 4
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵)))) |
186 | 185 | 3imp 1110 |
. . 3
⊢ ((𝐵 ∈
(ℤ≥‘𝐴) ∧ (𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵)) |
187 | 1, 2, 7, 8, 186 | syl121anc 1374 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → (𝑁C𝐴) ≤ (𝑁C𝐵)) |
188 | | simpl1 1190 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝑁 ∈
ℕ0) |
189 | 4 | adantr 481 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐴 ∈ ℤ) |
190 | | animorrl 978 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝐴 < 0 ∨ 𝑁 < 𝐴)) |
191 | | bcval4 14031 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ (𝐴 < 0 ∨ 𝑁 < 𝐴)) → (𝑁C𝐴) = 0) |
192 | 188, 189,
190, 191 | syl3anc 1370 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐴) = 0) |
193 | | simpl2 1191 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐵 ∈ (ℤ≥‘𝐴)) |
194 | | eluzelz 12602 |
. . . . . 6
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → 𝐵 ∈ ℤ) |
195 | 193, 194 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐵 ∈ ℤ) |
196 | | bccl 14046 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵 ∈ ℤ)
→ (𝑁C𝐵) ∈
ℕ0) |
197 | 188, 195,
196 | syl2anc 584 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐵) ∈
ℕ0) |
198 | 197 | nn0ge0d 12306 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 0 ≤ (𝑁C𝐵)) |
199 | 192, 198 | eqbrtrd 5095 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐴) ≤ (𝑁C𝐵)) |
200 | | 0re 10987 |
. . 3
⊢ 0 ∈
ℝ |
201 | 4 | zred 12436 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → 𝐴 ∈ ℝ) |
202 | | lelttric 11092 |
. . 3
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 ≤ 𝐴 ∨ 𝐴 < 0)) |
203 | 200, 201,
202 | sylancr 587 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (0 ≤ 𝐴 ∨ 𝐴 < 0)) |
204 | 187, 199,
203 | mpjaodan 956 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵)) |