Proof of Theorem lcmineqlem18
Step | Hyp | Ref
| Expression |
1 | | 0zd 11981 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈
ℤ) |
2 | | 2z 12002 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ |
3 | 2 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ∈
ℤ) |
4 | | lcmineqlem18.1 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℕ) |
5 | 4 | nnzd 12074 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℤ) |
6 | 3, 5 | zmulcld 12081 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 · 𝑁) ∈
ℤ) |
7 | 6 | peano2zd 12078 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · 𝑁) + 1) ∈
ℤ) |
8 | 5 | peano2zd 12078 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
9 | 1, 7, 8 | 3jca 1125 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 ∈ ℤ ∧
((2 · 𝑁) + 1) ∈
ℤ ∧ (𝑁 + 1)
∈ ℤ)) |
10 | 4 | nnred 11640 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℝ) |
11 | | 1red 10631 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℝ) |
12 | 4 | nnnn0d 11943 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
13 | 12 | nn0ge0d 11946 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ 𝑁) |
14 | | 0le1 11152 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
1 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ 1) |
16 | 10, 11, 13, 15 | addge0d 11205 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ (𝑁 + 1)) |
17 | 10, 11 | readdcld 10659 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 + 1) ∈ ℝ) |
18 | 17, 10 | addge01d 11217 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0 ≤ 𝑁 ↔ (𝑁 + 1) ≤ ((𝑁 + 1) + 𝑁))) |
19 | 13, 18 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 + 1) ≤ ((𝑁 + 1) + 𝑁)) |
20 | 10 | recnd 10658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℂ) |
21 | | 1cnd 10625 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℂ) |
22 | 20, 21, 20 | add32d 10856 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑁 + 1) + 𝑁) = ((𝑁 + 𝑁) + 1)) |
23 | 20 | 2timesd 11868 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁)) |
24 | 23 | oveq1d 7150 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 · 𝑁) + 1) = ((𝑁 + 𝑁) + 1)) |
25 | 24 | eqcomd 2804 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑁 + 𝑁) + 1) = ((2 · 𝑁) + 1)) |
26 | 22, 25 | eqtrd 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 + 1) + 𝑁) = ((2 · 𝑁) + 1)) |
27 | 19, 26 | breqtrd 5056 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 + 1) ≤ ((2 · 𝑁) + 1)) |
28 | 16, 27 | jca 515 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 ≤ (𝑁 + 1) ∧ (𝑁 + 1) ≤ ((2 · 𝑁) + 1))) |
29 | 9, 28 | jca 515 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((0 ∈ ℤ ∧
((2 · 𝑁) + 1) ∈
ℤ ∧ (𝑁 + 1)
∈ ℤ) ∧ (0 ≤ (𝑁 + 1) ∧ (𝑁 + 1) ≤ ((2 · 𝑁) + 1)))) |
30 | | elfz2 12892 |
. . . . . . . . . . . 12
⊢ ((𝑁 + 1) ∈ (0...((2 ·
𝑁) + 1)) ↔ ((0 ∈
ℤ ∧ ((2 · 𝑁) + 1) ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) ∧ (0
≤ (𝑁 + 1) ∧ (𝑁 + 1) ≤ ((2 · 𝑁) + 1)))) |
31 | 29, 30 | sylibr 237 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈ (0...((2 · 𝑁) + 1))) |
32 | | bcval2 13661 |
. . . . . . . . . . 11
⊢ ((𝑁 + 1) ∈ (0...((2 ·
𝑁) + 1)) → (((2
· 𝑁) + 1)C(𝑁 + 1)) = ((!‘((2 ·
𝑁) + 1)) / ((!‘(((2
· 𝑁) + 1) −
(𝑁 + 1))) ·
(!‘(𝑁 +
1))))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁) + 1)C(𝑁 + 1)) = ((!‘((2 · 𝑁) + 1)) / ((!‘(((2
· 𝑁) + 1) −
(𝑁 + 1))) ·
(!‘(𝑁 +
1))))) |
34 | 6 | zcnd 12076 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
35 | 34, 21, 20, 21 | addsub4d 11033 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · 𝑁) + 1) − (𝑁 + 1)) = (((2 · 𝑁) − 𝑁) + (1 − 1))) |
36 | 23 | oveq1d 7150 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 · 𝑁) − 𝑁) = ((𝑁 + 𝑁) − 𝑁)) |
37 | 20, 20 | pncand 10987 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑁 + 𝑁) − 𝑁) = 𝑁) |
38 | 36, 37 | eqtrd 2833 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 · 𝑁) − 𝑁) = 𝑁) |
39 | | 1m1e0 11697 |
. . . . . . . . . . . . . . . . 17
⊢ (1
− 1) = 0 |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 − 1) =
0) |
41 | 38, 40 | oveq12d 7153 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2 · 𝑁) − 𝑁) + (1 − 1)) = (𝑁 + 0)) |
42 | 20 | addid1d 10829 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 + 0) = 𝑁) |
43 | 41, 42 | eqtrd 2833 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · 𝑁) − 𝑁) + (1 − 1)) = 𝑁) |
44 | 35, 43 | eqtrd 2833 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2 · 𝑁) + 1) − (𝑁 + 1)) = 𝑁) |
45 | 44 | fveq2d 6649 |
. . . . . . . . . . . 12
⊢ (𝜑 → (!‘(((2 ·
𝑁) + 1) − (𝑁 + 1))) = (!‘𝑁)) |
46 | 45 | oveq1d 7150 |
. . . . . . . . . . 11
⊢ (𝜑 → ((!‘(((2 ·
𝑁) + 1) − (𝑁 + 1))) · (!‘(𝑁 + 1))) = ((!‘𝑁) · (!‘(𝑁 + 1)))) |
47 | 46 | oveq2d 7151 |
. . . . . . . . . 10
⊢ (𝜑 → ((!‘((2 ·
𝑁) + 1)) / ((!‘(((2
· 𝑁) + 1) −
(𝑁 + 1))) ·
(!‘(𝑁 + 1)))) =
((!‘((2 · 𝑁) +
1)) / ((!‘𝑁) ·
(!‘(𝑁 +
1))))) |
48 | 33, 47 | eqtrd 2833 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝑁) + 1)C(𝑁 + 1)) = ((!‘((2 · 𝑁) + 1)) / ((!‘𝑁) · (!‘(𝑁 + 1))))) |
49 | | faccl 13639 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
50 | 12, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (!‘𝑁) ∈ ℕ) |
51 | 50 | nncnd 11641 |
. . . . . . . . . . . 12
⊢ (𝜑 → (!‘𝑁) ∈ ℂ) |
52 | | 1nn0 11901 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℕ0) |
54 | 12, 53 | nn0addcld 11947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
55 | | faccl 13639 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 + 1) ∈ ℕ0
→ (!‘(𝑁 + 1))
∈ ℕ) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (!‘(𝑁 + 1)) ∈
ℕ) |
57 | 56 | nncnd 11641 |
. . . . . . . . . . . 12
⊢ (𝜑 → (!‘(𝑁 + 1)) ∈
ℂ) |
58 | 51, 57 | mulcomd 10651 |
. . . . . . . . . . 11
⊢ (𝜑 → ((!‘𝑁) · (!‘(𝑁 + 1))) = ((!‘(𝑁 + 1)) · (!‘𝑁))) |
59 | | facp1 13634 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ (!‘(𝑁 + 1)) =
((!‘𝑁) ·
(𝑁 + 1))) |
60 | 12, 59 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1))) |
61 | 20, 21 | addcld 10649 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 + 1) ∈ ℂ) |
62 | 51, 61 | mulcomd 10651 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((!‘𝑁) · (𝑁 + 1)) = ((𝑁 + 1) · (!‘𝑁))) |
63 | 60, 62 | eqtrd 2833 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (!‘(𝑁 + 1)) = ((𝑁 + 1) · (!‘𝑁))) |
64 | 63 | oveq1d 7150 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((!‘(𝑁 + 1)) · (!‘𝑁)) = (((𝑁 + 1) · (!‘𝑁)) · (!‘𝑁))) |
65 | 61, 51, 51 | mulassd 10653 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑁 + 1) · (!‘𝑁)) · (!‘𝑁)) = ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁)))) |
66 | 64, 65 | eqtrd 2833 |
. . . . . . . . . . 11
⊢ (𝜑 → ((!‘(𝑁 + 1)) · (!‘𝑁)) = ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁)))) |
67 | 58, 66 | eqtrd 2833 |
. . . . . . . . . 10
⊢ (𝜑 → ((!‘𝑁) · (!‘(𝑁 + 1))) = ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁)))) |
68 | 67 | oveq2d 7151 |
. . . . . . . . 9
⊢ (𝜑 → ((!‘((2 ·
𝑁) + 1)) / ((!‘𝑁) · (!‘(𝑁 + 1)))) = ((!‘((2
· 𝑁) + 1)) / ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁))))) |
69 | 48, 68 | eqtrd 2833 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁) + 1)C(𝑁 + 1)) = ((!‘((2 · 𝑁) + 1)) / ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁))))) |
70 | | 2nn0 11902 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
71 | 70 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℕ0) |
72 | 71, 12 | nn0mulcld 11948 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝑁) ∈
ℕ0) |
73 | | facp1 13634 |
. . . . . . . . . . 11
⊢ ((2
· 𝑁) ∈
ℕ0 → (!‘((2 · 𝑁) + 1)) = ((!‘(2 · 𝑁)) · ((2 · 𝑁) + 1))) |
74 | 72, 73 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (!‘((2 ·
𝑁) + 1)) = ((!‘(2
· 𝑁)) · ((2
· 𝑁) +
1))) |
75 | | faccl 13639 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑁) ∈
ℕ0 → (!‘(2 · 𝑁)) ∈ ℕ) |
76 | 72, 75 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (!‘(2 · 𝑁)) ∈
ℕ) |
77 | 76 | nncnd 11641 |
. . . . . . . . . . 11
⊢ (𝜑 → (!‘(2 · 𝑁)) ∈
ℂ) |
78 | 34, 21 | addcld 10649 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁) + 1) ∈
ℂ) |
79 | 77, 78 | mulcomd 10651 |
. . . . . . . . . 10
⊢ (𝜑 → ((!‘(2 ·
𝑁)) · ((2 ·
𝑁) + 1)) = (((2 ·
𝑁) + 1) ·
(!‘(2 · 𝑁)))) |
80 | 74, 79 | eqtrd 2833 |
. . . . . . . . 9
⊢ (𝜑 → (!‘((2 ·
𝑁) + 1)) = (((2 ·
𝑁) + 1) ·
(!‘(2 · 𝑁)))) |
81 | 80 | oveq1d 7150 |
. . . . . . . 8
⊢ (𝜑 → ((!‘((2 ·
𝑁) + 1)) / ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁)))) = ((((2 · 𝑁) + 1) · (!‘(2
· 𝑁))) / ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁))))) |
82 | 69, 81 | eqtrd 2833 |
. . . . . . 7
⊢ (𝜑 → (((2 · 𝑁) + 1)C(𝑁 + 1)) = ((((2 · 𝑁) + 1) · (!‘(2 · 𝑁))) / ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁))))) |
83 | 82 | oveq2d 7151 |
. . . . . 6
⊢ (𝜑 → ((𝑁 + 1) · (((2 · 𝑁) + 1)C(𝑁 + 1))) = ((𝑁 + 1) · ((((2 · 𝑁) + 1) · (!‘(2
· 𝑁))) / ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁)))))) |
84 | 78, 77 | mulcld 10650 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁) + 1) · (!‘(2
· 𝑁))) ∈
ℂ) |
85 | 51, 51 | mulcld 10650 |
. . . . . . . . 9
⊢ (𝜑 → ((!‘𝑁) · (!‘𝑁)) ∈
ℂ) |
86 | 61, 85 | mulcld 10650 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁))) ∈ ℂ) |
87 | 4 | peano2nnd 11642 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + 1) ∈ ℕ) |
88 | 87 | nnne0d 11675 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 + 1) ≠ 0) |
89 | 50 | nnne0d 11675 |
. . . . . . . . . 10
⊢ (𝜑 → (!‘𝑁) ≠ 0) |
90 | 51, 51, 89, 89 | mulne0d 11281 |
. . . . . . . . 9
⊢ (𝜑 → ((!‘𝑁) · (!‘𝑁)) ≠ 0) |
91 | 61, 85, 88, 90 | mulne0d 11281 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁))) ≠ 0) |
92 | 61, 84, 86, 91 | divassd 11440 |
. . . . . . 7
⊢ (𝜑 → (((𝑁 + 1) · (((2 · 𝑁) + 1) · (!‘(2
· 𝑁)))) / ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁)))) = ((𝑁 + 1) · ((((2 · 𝑁) + 1) · (!‘(2
· 𝑁))) / ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁)))))) |
93 | 92 | eqcomd 2804 |
. . . . . 6
⊢ (𝜑 → ((𝑁 + 1) · ((((2 · 𝑁) + 1) · (!‘(2
· 𝑁))) / ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁))))) = (((𝑁 + 1) · (((2 · 𝑁) + 1) · (!‘(2
· 𝑁)))) / ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁))))) |
94 | 83, 93 | eqtrd 2833 |
. . . . 5
⊢ (𝜑 → ((𝑁 + 1) · (((2 · 𝑁) + 1)C(𝑁 + 1))) = (((𝑁 + 1) · (((2 · 𝑁) + 1) · (!‘(2
· 𝑁)))) / ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁))))) |
95 | 61, 61, 84, 85, 88, 90 | divmuldivd 11446 |
. . . . . 6
⊢ (𝜑 → (((𝑁 + 1) / (𝑁 + 1)) · ((((2 · 𝑁) + 1) · (!‘(2
· 𝑁))) /
((!‘𝑁) ·
(!‘𝑁)))) = (((𝑁 + 1) · (((2 ·
𝑁) + 1) ·
(!‘(2 · 𝑁))))
/ ((𝑁 + 1) ·
((!‘𝑁) ·
(!‘𝑁))))) |
96 | 95 | eqcomd 2804 |
. . . . 5
⊢ (𝜑 → (((𝑁 + 1) · (((2 · 𝑁) + 1) · (!‘(2
· 𝑁)))) / ((𝑁 + 1) · ((!‘𝑁) · (!‘𝑁)))) = (((𝑁 + 1) / (𝑁 + 1)) · ((((2 · 𝑁) + 1) · (!‘(2
· 𝑁))) /
((!‘𝑁) ·
(!‘𝑁))))) |
97 | 94, 96 | eqtrd 2833 |
. . . 4
⊢ (𝜑 → ((𝑁 + 1) · (((2 · 𝑁) + 1)C(𝑁 + 1))) = (((𝑁 + 1) / (𝑁 + 1)) · ((((2 · 𝑁) + 1) · (!‘(2
· 𝑁))) /
((!‘𝑁) ·
(!‘𝑁))))) |
98 | 61, 88 | dividd 11403 |
. . . . . 6
⊢ (𝜑 → ((𝑁 + 1) / (𝑁 + 1)) = 1) |
99 | 98 | oveq1d 7150 |
. . . . 5
⊢ (𝜑 → (((𝑁 + 1) / (𝑁 + 1)) · ((((2 · 𝑁) + 1) · (!‘(2
· 𝑁))) /
((!‘𝑁) ·
(!‘𝑁)))) = (1
· ((((2 · 𝑁)
+ 1) · (!‘(2 · 𝑁))) / ((!‘𝑁) · (!‘𝑁))))) |
100 | 84, 85, 90 | divcld 11405 |
. . . . . 6
⊢ (𝜑 → ((((2 · 𝑁) + 1) · (!‘(2
· 𝑁))) /
((!‘𝑁) ·
(!‘𝑁))) ∈
ℂ) |
101 | 100 | mulid2d 10648 |
. . . . 5
⊢ (𝜑 → (1 · ((((2 ·
𝑁) + 1) ·
(!‘(2 · 𝑁))) /
((!‘𝑁) ·
(!‘𝑁)))) = ((((2
· 𝑁) + 1) ·
(!‘(2 · 𝑁))) /
((!‘𝑁) ·
(!‘𝑁)))) |
102 | 99, 101 | eqtrd 2833 |
. . . 4
⊢ (𝜑 → (((𝑁 + 1) / (𝑁 + 1)) · ((((2 · 𝑁) + 1) · (!‘(2
· 𝑁))) /
((!‘𝑁) ·
(!‘𝑁)))) = ((((2
· 𝑁) + 1) ·
(!‘(2 · 𝑁))) /
((!‘𝑁) ·
(!‘𝑁)))) |
103 | 97, 102 | eqtrd 2833 |
. . 3
⊢ (𝜑 → ((𝑁 + 1) · (((2 · 𝑁) + 1)C(𝑁 + 1))) = ((((2 · 𝑁) + 1) · (!‘(2 · 𝑁))) / ((!‘𝑁) · (!‘𝑁)))) |
104 | 78, 77, 85, 90 | divassd 11440 |
. . 3
⊢ (𝜑 → ((((2 · 𝑁) + 1) · (!‘(2
· 𝑁))) /
((!‘𝑁) ·
(!‘𝑁))) = (((2
· 𝑁) + 1) ·
((!‘(2 · 𝑁)) /
((!‘𝑁) ·
(!‘𝑁))))) |
105 | 103, 104 | eqtrd 2833 |
. 2
⊢ (𝜑 → ((𝑁 + 1) · (((2 · 𝑁) + 1)C(𝑁 + 1))) = (((2 · 𝑁) + 1) · ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))))) |
106 | 1, 6, 5 | 3jca 1125 |
. . . . . . . 8
⊢ (𝜑 → (0 ∈ ℤ ∧ (2
· 𝑁) ∈ ℤ
∧ 𝑁 ∈
ℤ)) |
107 | 10, 10 | addge01d 11217 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 ≤ 𝑁 ↔ 𝑁 ≤ (𝑁 + 𝑁))) |
108 | 23 | breq2d 5042 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ≤ (2 · 𝑁) ↔ 𝑁 ≤ (𝑁 + 𝑁))) |
109 | 107, 108 | bitr4d 285 |
. . . . . . . . . 10
⊢ (𝜑 → (0 ≤ 𝑁 ↔ 𝑁 ≤ (2 · 𝑁))) |
110 | 13, 109 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ≤ (2 · 𝑁)) |
111 | 13, 110 | jca 515 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ 𝑁 ∧ 𝑁 ≤ (2 · 𝑁))) |
112 | 106, 111 | jca 515 |
. . . . . . 7
⊢ (𝜑 → ((0 ∈ ℤ ∧
(2 · 𝑁) ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (0 ≤ 𝑁
∧ 𝑁 ≤ (2 ·
𝑁)))) |
113 | | elfz2 12892 |
. . . . . . 7
⊢ (𝑁 ∈ (0...(2 · 𝑁)) ↔ ((0 ∈ ℤ
∧ (2 · 𝑁) ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (0 ≤ 𝑁
∧ 𝑁 ≤ (2 ·
𝑁)))) |
114 | 112, 113 | sylibr 237 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (0...(2 · 𝑁))) |
115 | | bcval2 13661 |
. . . . . 6
⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘((2 · 𝑁) − 𝑁)) · (!‘𝑁)))) |
116 | 114, 115 | syl 17 |
. . . . 5
⊢ (𝜑 → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘((2 · 𝑁) − 𝑁)) · (!‘𝑁)))) |
117 | 38 | fveq2d 6649 |
. . . . . . 7
⊢ (𝜑 → (!‘((2 ·
𝑁) − 𝑁)) = (!‘𝑁)) |
118 | 117 | oveq1d 7150 |
. . . . . 6
⊢ (𝜑 → ((!‘((2 ·
𝑁) − 𝑁)) · (!‘𝑁)) = ((!‘𝑁) · (!‘𝑁))) |
119 | 118 | oveq2d 7151 |
. . . . 5
⊢ (𝜑 → ((!‘(2 ·
𝑁)) / ((!‘((2
· 𝑁) − 𝑁)) · (!‘𝑁))) = ((!‘(2 ·
𝑁)) / ((!‘𝑁) · (!‘𝑁)))) |
120 | 116, 119 | eqtrd 2833 |
. . . 4
⊢ (𝜑 → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁)))) |
121 | 120 | oveq2d 7151 |
. . 3
⊢ (𝜑 → (((2 · 𝑁) + 1) · ((2 ·
𝑁)C𝑁)) = (((2 · 𝑁) + 1) · ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))))) |
122 | 121 | eqcomd 2804 |
. 2
⊢ (𝜑 → (((2 · 𝑁) + 1) · ((!‘(2
· 𝑁)) /
((!‘𝑁) ·
(!‘𝑁)))) = (((2
· 𝑁) + 1) ·
((2 · 𝑁)C𝑁))) |
123 | 105, 122 | eqtrd 2833 |
1
⊢ (𝜑 → ((𝑁 + 1) · (((2 · 𝑁) + 1)C(𝑁 + 1))) = (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁))) |