Step | Hyp | Ref
| Expression |
1 | | breq2 4657 |
. . . . 5
⊢ (𝑗 = 0 → (𝑁 ≤ 𝑗 ↔ 𝑁 ≤ 0)) |
2 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑗 = 0 → (!‘𝑗) =
(!‘0)) |
3 | 2 | oveq1d 6665 |
. . . . . 6
⊢ (𝑗 = 0 → ((!‘𝑗) / 𝑁) = ((!‘0) / 𝑁)) |
4 | 3 | eleq1d 2686 |
. . . . 5
⊢ (𝑗 = 0 → (((!‘𝑗) / 𝑁) ∈ ℕ ↔ ((!‘0) / 𝑁) ∈
ℕ)) |
5 | 1, 4 | imbi12d 334 |
. . . 4
⊢ (𝑗 = 0 → ((𝑁 ≤ 𝑗 → ((!‘𝑗) / 𝑁) ∈ ℕ) ↔ (𝑁 ≤ 0 → ((!‘0) / 𝑁) ∈
ℕ))) |
6 | 5 | imbi2d 330 |
. . 3
⊢ (𝑗 = 0 → ((𝑁 ∈ ℕ → (𝑁 ≤ 𝑗 → ((!‘𝑗) / 𝑁) ∈ ℕ)) ↔ (𝑁 ∈ ℕ → (𝑁 ≤ 0 → ((!‘0) / 𝑁) ∈
ℕ)))) |
7 | | breq2 4657 |
. . . . 5
⊢ (𝑗 = 𝑘 → (𝑁 ≤ 𝑗 ↔ 𝑁 ≤ 𝑘)) |
8 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘)) |
9 | 8 | oveq1d 6665 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ((!‘𝑗) / 𝑁) = ((!‘𝑘) / 𝑁)) |
10 | 9 | eleq1d 2686 |
. . . . 5
⊢ (𝑗 = 𝑘 → (((!‘𝑗) / 𝑁) ∈ ℕ ↔ ((!‘𝑘) / 𝑁) ∈ ℕ)) |
11 | 7, 10 | imbi12d 334 |
. . . 4
⊢ (𝑗 = 𝑘 → ((𝑁 ≤ 𝑗 → ((!‘𝑗) / 𝑁) ∈ ℕ) ↔ (𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ))) |
12 | 11 | imbi2d 330 |
. . 3
⊢ (𝑗 = 𝑘 → ((𝑁 ∈ ℕ → (𝑁 ≤ 𝑗 → ((!‘𝑗) / 𝑁) ∈ ℕ)) ↔ (𝑁 ∈ ℕ → (𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ)))) |
13 | | breq2 4657 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (𝑁 ≤ 𝑗 ↔ 𝑁 ≤ (𝑘 + 1))) |
14 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (!‘𝑗) = (!‘(𝑘 + 1))) |
15 | 14 | oveq1d 6665 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((!‘𝑗) / 𝑁) = ((!‘(𝑘 + 1)) / 𝑁)) |
16 | 15 | eleq1d 2686 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (((!‘𝑗) / 𝑁) ∈ ℕ ↔ ((!‘(𝑘 + 1)) / 𝑁) ∈ ℕ)) |
17 | 13, 16 | imbi12d 334 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → ((𝑁 ≤ 𝑗 → ((!‘𝑗) / 𝑁) ∈ ℕ) ↔ (𝑁 ≤ (𝑘 + 1) → ((!‘(𝑘 + 1)) / 𝑁) ∈ ℕ))) |
18 | 17 | imbi2d 330 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((𝑁 ∈ ℕ → (𝑁 ≤ 𝑗 → ((!‘𝑗) / 𝑁) ∈ ℕ)) ↔ (𝑁 ∈ ℕ → (𝑁 ≤ (𝑘 + 1) → ((!‘(𝑘 + 1)) / 𝑁) ∈ ℕ)))) |
19 | | breq2 4657 |
. . . . 5
⊢ (𝑗 = 𝑀 → (𝑁 ≤ 𝑗 ↔ 𝑁 ≤ 𝑀)) |
20 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑗 = 𝑀 → (!‘𝑗) = (!‘𝑀)) |
21 | 20 | oveq1d 6665 |
. . . . . 6
⊢ (𝑗 = 𝑀 → ((!‘𝑗) / 𝑁) = ((!‘𝑀) / 𝑁)) |
22 | 21 | eleq1d 2686 |
. . . . 5
⊢ (𝑗 = 𝑀 → (((!‘𝑗) / 𝑁) ∈ ℕ ↔ ((!‘𝑀) / 𝑁) ∈ ℕ)) |
23 | 19, 22 | imbi12d 334 |
. . . 4
⊢ (𝑗 = 𝑀 → ((𝑁 ≤ 𝑗 → ((!‘𝑗) / 𝑁) ∈ ℕ) ↔ (𝑁 ≤ 𝑀 → ((!‘𝑀) / 𝑁) ∈ ℕ))) |
24 | 23 | imbi2d 330 |
. . 3
⊢ (𝑗 = 𝑀 → ((𝑁 ∈ ℕ → (𝑁 ≤ 𝑗 → ((!‘𝑗) / 𝑁) ∈ ℕ)) ↔ (𝑁 ∈ ℕ → (𝑁 ≤ 𝑀 → ((!‘𝑀) / 𝑁) ∈ ℕ)))) |
25 | | nngt0 11049 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
26 | | 0re 10040 |
. . . . . 6
⊢ 0 ∈
ℝ |
27 | | nnre 11027 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
28 | | ltnle 10117 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ 𝑁
∈ ℝ) → (0 < 𝑁 ↔ ¬ 𝑁 ≤ 0)) |
29 | 26, 27, 28 | sylancr 695 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (0 <
𝑁 ↔ ¬ 𝑁 ≤ 0)) |
30 | 25, 29 | mpbid 222 |
. . . 4
⊢ (𝑁 ∈ ℕ → ¬
𝑁 ≤ 0) |
31 | 30 | pm2.21d 118 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑁 ≤ 0 → ((!‘0) /
𝑁) ∈
ℕ)) |
32 | | peano2nn0 11333 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
33 | 32 | nn0red 11352 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℝ) |
34 | | leloe 10124 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
(𝑁 ≤ (𝑘 + 1) ↔ (𝑁 < (𝑘 + 1) ∨ 𝑁 = (𝑘 + 1)))) |
35 | 27, 33, 34 | syl2an 494 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑁 ≤ (𝑘 + 1) ↔ (𝑁 < (𝑘 + 1) ∨ 𝑁 = (𝑘 + 1)))) |
36 | | nnnn0 11299 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
37 | | nn0leltp1 11436 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 ≤ 𝑘 ↔ 𝑁 < (𝑘 + 1))) |
38 | 36, 37 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑁 ≤ 𝑘 ↔ 𝑁 < (𝑘 + 1))) |
39 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ) |
40 | | nnmulcl 11043 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((!‘𝑘) /
𝑁) ∈ ℕ ∧
(𝑘 + 1) ∈ ℕ)
→ (((!‘𝑘) /
𝑁) · (𝑘 + 1)) ∈
ℕ) |
41 | 39, 40 | sylan2 491 |
. . . . . . . . . . . . . . . . . 18
⊢
((((!‘𝑘) /
𝑁) ∈ ℕ ∧
𝑘 ∈
ℕ0) → (((!‘𝑘) / 𝑁) · (𝑘 + 1)) ∈ ℕ) |
42 | 41 | expcom 451 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ0
→ (((!‘𝑘) /
𝑁) ∈ ℕ →
(((!‘𝑘) / 𝑁) · (𝑘 + 1)) ∈ ℕ)) |
43 | 42 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (((!‘𝑘) /
𝑁) ∈ ℕ →
(((!‘𝑘) / 𝑁) · (𝑘 + 1)) ∈ ℕ)) |
44 | | faccl 13070 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
45 | 44 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℂ) |
46 | 45 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (!‘𝑘) ∈
ℂ) |
47 | 32 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℂ) |
48 | 47 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℂ) |
49 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
50 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
51 | 49, 50 | jca 554 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑁 ∈ ℂ
∧ 𝑁 ≠
0)) |
53 | | div23 10704 |
. . . . . . . . . . . . . . . . . 18
⊢
(((!‘𝑘) ∈
ℂ ∧ (𝑘 + 1)
∈ ℂ ∧ (𝑁
∈ ℂ ∧ 𝑁 ≠
0)) → (((!‘𝑘)
· (𝑘 + 1)) / 𝑁) = (((!‘𝑘) / 𝑁) · (𝑘 + 1))) |
54 | 46, 48, 52, 53 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (((!‘𝑘)
· (𝑘 + 1)) / 𝑁) = (((!‘𝑘) / 𝑁) · (𝑘 + 1))) |
55 | 54 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((((!‘𝑘)
· (𝑘 + 1)) / 𝑁) ∈ ℕ ↔
(((!‘𝑘) / 𝑁) · (𝑘 + 1)) ∈ ℕ)) |
56 | 43, 55 | sylibrd 249 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (((!‘𝑘) /
𝑁) ∈ ℕ →
(((!‘𝑘) ·
(𝑘 + 1)) / 𝑁) ∈
ℕ)) |
57 | 56 | imim2d 57 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ) → (𝑁 ≤ 𝑘 → (((!‘𝑘) · (𝑘 + 1)) / 𝑁) ∈ ℕ))) |
58 | 57 | com23 86 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑁 ≤ 𝑘 → ((𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ) → (((!‘𝑘) · (𝑘 + 1)) / 𝑁) ∈ ℕ))) |
59 | 38, 58 | sylbird 250 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑁 < (𝑘 + 1) → ((𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ) → (((!‘𝑘) · (𝑘 + 1)) / 𝑁) ∈ ℕ))) |
60 | 49 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ 𝑁 ∈
ℂ) |
61 | 50 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ 𝑁 ≠
0) |
62 | 46, 60, 61 | divcan4d 10807 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (((!‘𝑘)
· 𝑁) / 𝑁) = (!‘𝑘)) |
63 | 44 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (!‘𝑘) ∈
ℕ) |
64 | 62, 63 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (((!‘𝑘)
· 𝑁) / 𝑁) ∈
ℕ) |
65 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = (𝑘 + 1) → ((!‘𝑘) · 𝑁) = ((!‘𝑘) · (𝑘 + 1))) |
66 | 65 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = (𝑘 + 1) → (((!‘𝑘) · 𝑁) / 𝑁) = (((!‘𝑘) · (𝑘 + 1)) / 𝑁)) |
67 | 66 | eleq1d 2686 |
. . . . . . . . . . . . . 14
⊢ (𝑁 = (𝑘 + 1) → ((((!‘𝑘) · 𝑁) / 𝑁) ∈ ℕ ↔ (((!‘𝑘) · (𝑘 + 1)) / 𝑁) ∈ ℕ)) |
68 | 64, 67 | syl5ibcom 235 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑁 = (𝑘 + 1) → (((!‘𝑘) · (𝑘 + 1)) / 𝑁) ∈ ℕ)) |
69 | 68 | a1dd 50 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑁 = (𝑘 + 1) → ((𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ) → (((!‘𝑘) · (𝑘 + 1)) / 𝑁) ∈ ℕ))) |
70 | 59, 69 | jaod 395 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 < (𝑘 + 1) ∨ 𝑁 = (𝑘 + 1)) → ((𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ) → (((!‘𝑘) · (𝑘 + 1)) / 𝑁) ∈ ℕ))) |
71 | 35, 70 | sylbid 230 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑁 ≤ (𝑘 + 1) → ((𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ) → (((!‘𝑘) · (𝑘 + 1)) / 𝑁) ∈ ℕ))) |
72 | 71 | ex 450 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑘 ∈ ℕ0
→ (𝑁 ≤ (𝑘 + 1) → ((𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ) → (((!‘𝑘) · (𝑘 + 1)) / 𝑁) ∈ ℕ)))) |
73 | 72 | com34 91 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑘 ∈ ℕ0
→ ((𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ) → (𝑁 ≤ (𝑘 + 1) → (((!‘𝑘) · (𝑘 + 1)) / 𝑁) ∈ ℕ)))) |
74 | 73 | com12 32 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (𝑁 ∈ ℕ
→ ((𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ) → (𝑁 ≤ (𝑘 + 1) → (((!‘𝑘) · (𝑘 + 1)) / 𝑁) ∈ ℕ)))) |
75 | 74 | imp4d 618 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ ((𝑁 ∈ ℕ
∧ ((𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ) ∧ 𝑁 ≤ (𝑘 + 1))) → (((!‘𝑘) · (𝑘 + 1)) / 𝑁) ∈ ℕ)) |
76 | | facp1 13065 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1)) =
((!‘𝑘) ·
(𝑘 + 1))) |
77 | 76 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ ((!‘(𝑘 + 1)) /
𝑁) = (((!‘𝑘) · (𝑘 + 1)) / 𝑁)) |
78 | 77 | eleq1d 2686 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (((!‘(𝑘 + 1))
/ 𝑁) ∈ ℕ ↔
(((!‘𝑘) ·
(𝑘 + 1)) / 𝑁) ∈
ℕ)) |
79 | 75, 78 | sylibrd 249 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ ((𝑁 ∈ ℕ
∧ ((𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ) ∧ 𝑁 ≤ (𝑘 + 1))) → ((!‘(𝑘 + 1)) / 𝑁) ∈ ℕ)) |
80 | 79 | exp4d 637 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝑁 ∈ ℕ
→ ((𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ) → (𝑁 ≤ (𝑘 + 1) → ((!‘(𝑘 + 1)) / 𝑁) ∈ ℕ)))) |
81 | 80 | a2d 29 |
. . 3
⊢ (𝑘 ∈ ℕ0
→ ((𝑁 ∈ ℕ
→ (𝑁 ≤ 𝑘 → ((!‘𝑘) / 𝑁) ∈ ℕ)) → (𝑁 ∈ ℕ → (𝑁 ≤ (𝑘 + 1) → ((!‘(𝑘 + 1)) / 𝑁) ∈ ℕ)))) |
82 | 6, 12, 18, 24, 31, 81 | nn0ind 11472 |
. 2
⊢ (𝑀 ∈ ℕ0
→ (𝑁 ∈ ℕ
→ (𝑁 ≤ 𝑀 → ((!‘𝑀) / 𝑁) ∈ ℕ))) |
83 | 82 | 3imp 1256 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑁 ≤ 𝑀) → ((!‘𝑀) / 𝑁) ∈ ℕ) |