Step | Hyp | Ref
| Expression |
1 | | simpl2 1201 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐵 ∈ (ℤ≥‘𝐴)) |
2 | | simpl1 1199 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝑁 ∈
ℕ0) |
3 | | eluzel2 11997 |
. . . . . 6
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → 𝐴 ∈ ℤ) |
4 | 3 | 3ad2ant2 1125 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → 𝐴 ∈ ℤ) |
5 | 4 | anim1i 608 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴)) |
6 | | elnn0z 11741 |
. . . 4
⊢ (𝐴 ∈ ℕ0
↔ (𝐴 ∈ ℤ
∧ 0 ≤ 𝐴)) |
7 | 5, 6 | sylibr 226 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐴 ∈
ℕ0) |
8 | | simpl3 1203 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → 𝐵 ≤ (𝑁 / 2)) |
9 | | breq1 4889 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 ≤ (𝑁 / 2) ↔ 𝐴 ≤ (𝑁 / 2))) |
10 | | oveq2 6930 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑁C𝑥) = (𝑁C𝐴)) |
11 | 10 | breq2d 4898 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝐴))) |
12 | 9, 11 | imbi12d 336 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))) |
13 | 12 | imbi2d 332 |
. . . . 5
⊢ (𝑥 = 𝐴 → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))))) |
14 | | breq1 4889 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 ≤ (𝑁 / 2) ↔ 𝑘 ≤ (𝑁 / 2))) |
15 | | oveq2 6930 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (𝑁C𝑥) = (𝑁C𝑘)) |
16 | 15 | breq2d 4898 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝑘))) |
17 | 14, 16 | imbi12d 336 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)))) |
18 | 17 | imbi2d 332 |
. . . . 5
⊢ (𝑥 = 𝑘 → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))))) |
19 | | breq1 4889 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (𝑥 ≤ (𝑁 / 2) ↔ (𝑘 + 1) ≤ (𝑁 / 2))) |
20 | | oveq2 6930 |
. . . . . . . 8
⊢ (𝑥 = (𝑘 + 1) → (𝑁C𝑥) = (𝑁C(𝑘 + 1))) |
21 | 20 | breq2d 4898 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))) |
22 | 19, 21 | imbi12d 336 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))) |
23 | 22 | imbi2d 332 |
. . . . 5
⊢ (𝑥 = (𝑘 + 1) → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))) |
24 | | breq1 4889 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥 ≤ (𝑁 / 2) ↔ 𝐵 ≤ (𝑁 / 2))) |
25 | | oveq2 6930 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝑁C𝑥) = (𝑁C𝐵)) |
26 | 25 | breq2d 4898 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → ((𝑁C𝐴) ≤ (𝑁C𝑥) ↔ (𝑁C𝐴) ≤ (𝑁C𝐵))) |
27 | 24, 26 | imbi12d 336 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥)) ↔ (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵)))) |
28 | 27 | imbi2d 332 |
. . . . 5
⊢ (𝑥 = 𝐵 → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑥 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑥))) ↔ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵))))) |
29 | | bccl 13427 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (𝑁C𝐴) ∈
ℕ0) |
30 | 29 | nn0red 11703 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (𝑁C𝐴) ∈ ℝ) |
31 | 30 | leidd 10941 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (𝑁C𝐴) ≤ (𝑁C𝐴)) |
32 | 31 | a1d 25 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴))) |
33 | 32 | expcom 404 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝑁 ∈ ℕ0
→ (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))) |
34 | 33 | adantrd 487 |
. . . . 5
⊢ (𝐴 ∈ ℤ → ((𝑁 ∈ ℕ0
∧ 𝐴 ∈
ℕ0) → (𝐴 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐴)))) |
35 | | eluzelz 12002 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘𝐴) → 𝑘 ∈ ℤ) |
36 | 35 | 3ad2ant1 1124 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ 𝑘 ∈
ℤ) |
37 | 36 | zred 11834 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ 𝑘 ∈
ℝ) |
38 | 37 | lep1d 11309 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ 𝑘 ≤ (𝑘 + 1)) |
39 | | peano2re 10549 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
40 | 37, 39 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℝ) |
41 | | nn0re 11652 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
42 | 41 | 3ad2ant2 1125 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ 𝑁 ∈
ℝ) |
43 | 42 | rehalfcld 11629 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁 / 2) ∈
ℝ) |
44 | | letr 10470 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧
(𝑁 / 2) ∈ ℝ)
→ ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑁 / 2))) |
45 | 37, 40, 43, 44 | syl3anc 1439 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑁 / 2))) |
46 | 38, 45 | mpand 685 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 + 1) ≤ (𝑁 / 2) → 𝑘 ≤ (𝑁 / 2))) |
47 | 46 | imim1d 82 |
. . . . . . . 8
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)))) |
48 | | eluznn0 12064 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝐴)) → 𝑘 ∈ ℕ0) |
49 | | nn0re 11652 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
50 | 49 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℝ) |
51 | | nn0p1nn 11683 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ) |
52 | 51 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℕ) |
53 | 52 | nnnn0d 11702 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈
ℕ0) |
54 | 53 | nn0red 11703 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℝ) |
55 | 50, 54 | readdcld 10406 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + (𝑘 + 1)) ∈ ℝ) |
56 | 54, 54 | readdcld 10406 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) + (𝑘 + 1)) ∈ ℝ) |
57 | 41 | 3ad2ant2 1125 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℝ) |
58 | 50 | lep1d 11309 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ (𝑘 + 1)) |
59 | 50, 54, 54, 58 | leadd1dd 10989 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + (𝑘 + 1)) ≤ ((𝑘 + 1) + (𝑘 + 1))) |
60 | 52 | nncnd 11392 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℂ) |
61 | 60 | 2timesd 11625 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 · (𝑘 + 1)) = ((𝑘 + 1) + (𝑘 + 1))) |
62 | | simp3 1129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ (𝑁 / 2)) |
63 | | 2re 11449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ |
64 | | 2pos 11485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
2 |
65 | 63, 64 | pm3.2i 464 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℝ ∧ 0 < 2) |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 ∈ ℝ ∧ 0 <
2)) |
67 | | lemuldiv2 11258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑘 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((2 · (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 / 2))) |
68 | 54, 57, 66, 67 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((2 · (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 / 2))) |
69 | 62, 68 | mpbird 249 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (2 · (𝑘 + 1)) ≤ 𝑁) |
70 | 61, 69 | eqbrtrrd 4910 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) + (𝑘 + 1)) ≤ 𝑁) |
71 | 55, 56, 57, 59, 70 | letrd 10533 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + (𝑘 + 1)) ≤ 𝑁) |
72 | 50, 54, 57 | leaddsub2d 10977 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + (𝑘 + 1)) ≤ 𝑁 ↔ (𝑘 + 1) ≤ (𝑁 − 𝑘))) |
73 | 71, 72 | mpbid 224 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ (𝑁 − 𝑘)) |
74 | | nnre 11382 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 + 1) ∈ ℕ →
(𝑘 + 1) ∈
ℝ) |
75 | | nngt0 11407 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 + 1) ∈ ℕ → 0
< (𝑘 +
1)) |
76 | 74, 75 | jca 507 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 + 1) ∈ ℕ →
((𝑘 + 1) ∈ ℝ
∧ 0 < (𝑘 +
1))) |
77 | 52, 76 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1))) |
78 | | nn0z 11752 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
79 | 78 | 3ad2ant2 1125 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℤ) |
80 | | nn0z 11752 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
81 | 80 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℤ) |
82 | 79, 81 | zsubcld 11839 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − 𝑘) ∈ ℤ) |
83 | 57 | rehalfcld 11629 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 / 2) ∈ ℝ) |
84 | 57, 63 | jctir 516 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 ∈ ℝ ∧ 2 ∈
ℝ)) |
85 | | nn0ge0 11669 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
86 | 85 | 3ad2ant2 1125 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ 𝑁) |
87 | | 1le2 11591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ≤
2 |
88 | 86, 87 | jctir 516 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (0 ≤ 𝑁 ∧ 1 ≤ 2)) |
89 | | lemulge12 11240 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℝ ∧ 2 ∈
ℝ) ∧ (0 ≤ 𝑁
∧ 1 ≤ 2)) → 𝑁
≤ (2 · 𝑁)) |
90 | 84, 88, 89 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ≤ (2 · 𝑁)) |
91 | | ledivmul 11253 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((𝑁 / 2) ≤ 𝑁 ↔ 𝑁 ≤ (2 · 𝑁))) |
92 | 57, 57, 66, 91 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁 / 2) ≤ 𝑁 ↔ 𝑁 ≤ (2 · 𝑁))) |
93 | 90, 92 | mpbird 249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 / 2) ≤ 𝑁) |
94 | 54, 83, 57, 62, 93 | letrd 10533 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≤ 𝑁) |
95 | | 1red 10377 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ∈
ℝ) |
96 | 50, 95, 57 | leaddsub2d 10977 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁 − 𝑘))) |
97 | 94, 96 | mpbid 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ≤ (𝑁 − 𝑘)) |
98 | | elnnz1 11755 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 𝑘) ∈ ℕ ↔ ((𝑁 − 𝑘) ∈ ℤ ∧ 1 ≤ (𝑁 − 𝑘))) |
99 | 82, 97, 98 | sylanbrc 578 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − 𝑘) ∈ ℕ) |
100 | | nnre 11382 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 𝑘) ∈ ℕ → (𝑁 − 𝑘) ∈ ℝ) |
101 | | nngt0 11407 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 𝑘) ∈ ℕ → 0 < (𝑁 − 𝑘)) |
102 | 100, 101 | jca 507 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 − 𝑘) ∈ ℕ → ((𝑁 − 𝑘) ∈ ℝ ∧ 0 < (𝑁 − 𝑘))) |
103 | 99, 102 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁 − 𝑘) ∈ ℝ ∧ 0 < (𝑁 − 𝑘))) |
104 | | faccl 13388 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
105 | 104 | 3ad2ant2 1125 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑁) ∈ ℕ) |
106 | | nnm1nn0 11685 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 − 𝑘) ∈ ℕ → ((𝑁 − 𝑘) − 1) ∈
ℕ0) |
107 | | faccl 13388 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 − 𝑘) − 1) ∈ ℕ0
→ (!‘((𝑁 −
𝑘) − 1)) ∈
ℕ) |
108 | 99, 106, 107 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘((𝑁 − 𝑘) − 1)) ∈
ℕ) |
109 | | faccl 13388 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
110 | 109 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑘) ∈ ℕ) |
111 | 108, 110 | nnmulcld 11428 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈
ℕ) |
112 | | nnrp 12150 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((!‘𝑁) ∈
ℕ → (!‘𝑁)
∈ ℝ+) |
113 | | nnrp 12150 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((!‘((𝑁
− 𝑘) − 1))
· (!‘𝑘))
∈ ℕ → ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈
ℝ+) |
114 | | rpdivcl 12164 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((!‘𝑁) ∈
ℝ+ ∧ ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈ ℝ+)
→ ((!‘𝑁) /
((!‘((𝑁 − 𝑘) − 1)) ·
(!‘𝑘))) ∈
ℝ+) |
115 | 112, 113,
114 | syl2an 589 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((!‘𝑁) ∈
ℕ ∧ ((!‘((𝑁
− 𝑘) − 1))
· (!‘𝑘))
∈ ℕ) → ((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈
ℝ+) |
116 | 105, 111,
115 | syl2anc 579 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈
ℝ+) |
117 | 116 | rpregt0d 12187 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈ ℝ ∧ 0 <
((!‘𝑁) /
((!‘((𝑁 − 𝑘) − 1)) ·
(!‘𝑘))))) |
118 | | lediv2 11267 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑘 + 1) ∈ ℝ ∧ 0
< (𝑘 + 1)) ∧ ((𝑁 − 𝑘) ∈ ℝ ∧ 0 < (𝑁 − 𝑘)) ∧ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) ∈ ℝ ∧ 0 <
((!‘𝑁) /
((!‘((𝑁 − 𝑘) − 1)) ·
(!‘𝑘))))) →
((𝑘 + 1) ≤ (𝑁 − 𝑘) ↔ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)))) |
119 | 77, 103, 117, 118 | syl3anc 1439 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ≤ (𝑁 − 𝑘) ↔ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)))) |
120 | 73, 119 | mpbid 224 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)) ≤ (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1))) |
121 | | facnn2 13387 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 − 𝑘) ∈ ℕ → (!‘(𝑁 − 𝑘)) = ((!‘((𝑁 − 𝑘) − 1)) · (𝑁 − 𝑘))) |
122 | 99, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑁 − 𝑘)) = ((!‘((𝑁 − 𝑘) − 1)) · (𝑁 − 𝑘))) |
123 | 122 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − 𝑘)) · (!‘𝑘)) = (((!‘((𝑁 − 𝑘) − 1)) · (𝑁 − 𝑘)) · (!‘𝑘))) |
124 | 108 | nncnd 11392 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘((𝑁 − 𝑘) − 1)) ∈
ℂ) |
125 | 110 | nncnd 11392 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑘) ∈ ℂ) |
126 | 82 | zcnd 11835 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − 𝑘) ∈ ℂ) |
127 | 124, 125,
126 | mul32d 10586 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑁 − 𝑘)) = (((!‘((𝑁 − 𝑘) − 1)) · (𝑁 − 𝑘)) · (!‘𝑘))) |
128 | 123, 127 | eqtr4d 2817 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − 𝑘)) · (!‘𝑘)) = (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑁 − 𝑘))) |
129 | 128 | oveq2d 6938 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘(𝑁 − 𝑘)) · (!‘𝑘))) = ((!‘𝑁) / (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑁 − 𝑘)))) |
130 | | nn0ge0 11669 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ 0 ≤ 𝑘) |
131 | 130 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ 𝑘) |
132 | 50, 54, 57, 58, 94 | letrd 10533 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ≤ 𝑁) |
133 | | 0zd 11740 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ∈
ℤ) |
134 | | elfz 12649 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑘 ∈
(0...𝑁) ↔ (0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁))) |
135 | 81, 133, 79, 134 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 ∈ (0...𝑁) ↔ (0 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
136 | 131, 132,
135 | mpbir2and 703 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ (0...𝑁)) |
137 | | bcval2 13410 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) = ((!‘𝑁) / ((!‘(𝑁 − 𝑘)) · (!‘𝑘)))) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) = ((!‘𝑁) / ((!‘(𝑁 − 𝑘)) · (!‘𝑘)))) |
139 | 105 | nncnd 11392 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘𝑁) ∈ ℂ) |
140 | 111 | nncnd 11392 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ∈
ℂ) |
141 | 111 | nnne0d 11425 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) ≠ 0) |
142 | 99 | nnne0d 11425 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − 𝑘) ≠ 0) |
143 | 139, 140,
126, 141, 142 | divdiv1d 11182 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘)) = ((!‘𝑁) / (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑁 − 𝑘)))) |
144 | 129, 138,
143 | 3eqtr4d 2824 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) = (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑁 − 𝑘))) |
145 | | nn0cn 11653 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
146 | 145 | 3ad2ant2 1125 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑁 ∈ ℂ) |
147 | | nn0cn 11653 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
148 | 147 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 𝑘 ∈ ℂ) |
149 | | 1cnd 10371 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 1 ∈
ℂ) |
150 | 146, 148,
149 | subsub4d 10765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑁 − 𝑘) − 1) = (𝑁 − (𝑘 + 1))) |
151 | 150 | eqcomd 2784 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁 − (𝑘 + 1)) = ((𝑁 − 𝑘) − 1)) |
152 | 151 | fveq2d 6450 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑁 − (𝑘 + 1))) = (!‘((𝑁 − 𝑘) − 1))) |
153 | | facp1 13383 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1)) =
((!‘𝑘) ·
(𝑘 + 1))) |
154 | 153 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1))) |
155 | 152, 154 | oveq12d 6940 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))) = ((!‘((𝑁 − 𝑘) − 1)) · ((!‘𝑘) · (𝑘 + 1)))) |
156 | 124, 125,
60 | mulassd 10400 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)) = ((!‘((𝑁 − 𝑘) − 1)) · ((!‘𝑘) · (𝑘 + 1)))) |
157 | 155, 156 | eqtr4d 2817 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))) = (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1))) |
158 | 157 | oveq2d 6938 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1)))) = ((!‘𝑁) / (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)))) |
159 | 53 | nn0ge0d 11705 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → 0 ≤ (𝑘 + 1)) |
160 | 52 | nnzd 11833 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ ℤ) |
161 | | elfz 12649 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑘 + 1) ∈ ℤ ∧ 0
∈ ℤ ∧ 𝑁
∈ ℤ) → ((𝑘
+ 1) ∈ (0...𝑁) ↔
(0 ≤ (𝑘 + 1) ∧
(𝑘 + 1) ≤ 𝑁))) |
162 | 160, 133,
79, 161 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → ((𝑘 + 1) ∈ (0...𝑁) ↔ (0 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁))) |
163 | 159, 94, 162 | mpbir2and 703 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ∈ (0...𝑁)) |
164 | | bcval2 13410 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 + 1) ∈ (0...𝑁) → (𝑁C(𝑘 + 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))))) |
165 | 163, 164 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C(𝑘 + 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑘 + 1))) · (!‘(𝑘 + 1))))) |
166 | 52 | nnne0d 11425 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑘 + 1) ≠ 0) |
167 | 139, 140,
60, 141, 166 | divdiv1d 11182 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1)) = ((!‘𝑁) / (((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘)) · (𝑘 + 1)))) |
168 | 158, 165,
167 | 3eqtr4d 2824 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C(𝑘 + 1)) = (((!‘𝑁) / ((!‘((𝑁 − 𝑘) − 1)) · (!‘𝑘))) / (𝑘 + 1))) |
169 | 120, 144,
168 | 3brtr4d 4918 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 + 1) ≤ (𝑁 / 2)) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) |
170 | 169 | 3exp 1109 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (𝑁 ∈
ℕ0 → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))))) |
171 | 48, 170 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝐴)) → (𝑁 ∈ ℕ0 → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))))) |
172 | 171 | 3impia 1106 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))) |
173 | 172 | 3coml 1118 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)))) |
174 | | simp2 1128 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
175 | | nn0z 11752 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℤ) |
176 | 175 | 3ad2ant3 1126 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ 𝐴 ∈
ℤ) |
177 | 174, 176,
29 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁C𝐴) ∈
ℕ0) |
178 | 177 | nn0red 11703 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁C𝐴) ∈ ℝ) |
179 | | bccl 13427 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) |
180 | 174, 36, 179 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁C𝑘) ∈
ℕ0) |
181 | 180 | nn0red 11703 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁C𝑘) ∈
ℝ) |
182 | 36 | peano2zd 11837 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℤ) |
183 | | bccl 13427 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑘 + 1) ∈
ℤ) → (𝑁C(𝑘 + 1)) ∈
ℕ0) |
184 | 174, 182,
183 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁C(𝑘 + 1)) ∈
ℕ0) |
185 | 184 | nn0red 11703 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑁C(𝑘 + 1)) ∈
ℝ) |
186 | | letr 10470 |
. . . . . . . . . . . 12
⊢ (((𝑁C𝐴) ∈ ℝ ∧ (𝑁C𝑘) ∈ ℝ ∧ (𝑁C(𝑘 + 1)) ∈ ℝ) → (((𝑁C𝐴) ≤ (𝑁C𝑘) ∧ (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))) |
187 | 178, 181,
185, 186 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (((𝑁C𝐴) ≤ (𝑁C𝑘) ∧ (𝑁C𝑘) ≤ (𝑁C(𝑘 + 1))) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))) |
188 | 187 | expcomd 408 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑁C𝑘) ≤ (𝑁C(𝑘 + 1)) → ((𝑁C𝐴) ≤ (𝑁C𝑘) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))) |
189 | 173, 188 | syld 47 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 + 1) ≤ (𝑁 / 2) → ((𝑁C𝐴) ≤ (𝑁C𝑘) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))) |
190 | 189 | a2d 29 |
. . . . . . . 8
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (((𝑘 + 1) ≤
(𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))) |
191 | 47, 190 | syld 47 |
. . . . . . 7
⊢ ((𝑘 ∈
(ℤ≥‘𝐴) ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1))))) |
192 | 191 | 3expib 1113 |
. . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘𝐴) → ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘)) → ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))) |
193 | 192 | a2d 29 |
. . . . 5
⊢ (𝑘 ∈
(ℤ≥‘𝐴) → (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝑘 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝑘))) → ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑘 + 1) ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C(𝑘 + 1)))))) |
194 | 13, 18, 23, 28, 34, 193 | uzind4 12052 |
. . . 4
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (𝐵 ≤ (𝑁 / 2) → (𝑁C𝐴) ≤ (𝑁C𝐵)))) |
195 | 194 | 3imp 1098 |
. . 3
⊢ ((𝐵 ∈
(ℤ≥‘𝐴) ∧ (𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵)) |
196 | 1, 2, 7, 8, 195 | syl121anc 1443 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 0 ≤ 𝐴) → (𝑁C𝐴) ≤ (𝑁C𝐵)) |
197 | | simpl1 1199 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝑁 ∈
ℕ0) |
198 | 4 | adantr 474 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐴 ∈ ℤ) |
199 | | orc 856 |
. . . . 5
⊢ (𝐴 < 0 → (𝐴 < 0 ∨ 𝑁 < 𝐴)) |
200 | 199 | adantl 475 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝐴 < 0 ∨ 𝑁 < 𝐴)) |
201 | | bcval4 13412 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ (𝐴 < 0 ∨ 𝑁 < 𝐴)) → (𝑁C𝐴) = 0) |
202 | 197, 198,
200, 201 | syl3anc 1439 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐴) = 0) |
203 | | simpl2 1201 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐵 ∈ (ℤ≥‘𝐴)) |
204 | | eluzelz 12002 |
. . . . . 6
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → 𝐵 ∈ ℤ) |
205 | 203, 204 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 𝐵 ∈ ℤ) |
206 | | bccl 13427 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵 ∈ ℤ)
→ (𝑁C𝐵) ∈
ℕ0) |
207 | 197, 205,
206 | syl2anc 579 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐵) ∈
ℕ0) |
208 | 207 | nn0ge0d 11705 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → 0 ≤ (𝑁C𝐵)) |
209 | 202, 208 | eqbrtrd 4908 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) ∧ 𝐴 < 0) → (𝑁C𝐴) ≤ (𝑁C𝐵)) |
210 | | 0re 10378 |
. . 3
⊢ 0 ∈
ℝ |
211 | 4 | zred 11834 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → 𝐴 ∈ ℝ) |
212 | | lelttric 10483 |
. . 3
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 ≤ 𝐴 ∨ 𝐴 < 0)) |
213 | 210, 211,
212 | sylancr 581 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (0 ≤ 𝐴 ∨ 𝐴 < 0)) |
214 | 196, 209,
213 | mpjaodan 944 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵 ∈
(ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵)) |