Proof of Theorem etransclem7
Step | Hyp | Ref
| Expression |
1 | | fzfid 13546 |
. 2
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
2 | | 0zd 12188 |
. . 3
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑃 < (𝐶‘𝑗)) → 0 ∈ ℤ) |
3 | | 0zd 12188 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → 0 ∈ ℤ) |
4 | | etransclem7.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) |
5 | 4 | nnzd 12281 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℤ) |
6 | 5 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → 𝑃 ∈ ℤ) |
7 | 5 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℤ) |
8 | | etransclem7.c |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) |
9 | 8 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐶:(0...𝑀)⟶(0...𝑁)) |
10 | | 0zd 12188 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → 0 ∈ ℤ) |
11 | | fzp1ss 13163 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
ℤ → ((0 + 1)...𝑀) ⊆ (0...𝑀)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → ((0 + 1)...𝑀) ⊆ (0...𝑀)) |
13 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (1...𝑀)) |
14 | | 1e0p1 12335 |
. . . . . . . . . . . . . . 15
⊢ 1 = (0 +
1) |
15 | 14 | oveq1i 7223 |
. . . . . . . . . . . . . 14
⊢
(1...𝑀) = ((0 +
1)...𝑀) |
16 | 13, 15 | eleqtrdi 2848 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ((0 + 1)...𝑀)) |
17 | 12, 16 | sseldd 3902 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (0...𝑀)) |
18 | 17 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀)) |
19 | 9, 18 | ffvelrnd 6905 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐶‘𝑗) ∈ (0...𝑁)) |
20 | 19 | elfzelzd 13113 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐶‘𝑗) ∈ ℤ) |
21 | 7, 20 | zsubcld 12287 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − (𝐶‘𝑗)) ∈ ℤ) |
22 | 21 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝑃 − (𝐶‘𝑗)) ∈ ℤ) |
23 | 20 | zred 12282 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐶‘𝑗) ∈ ℝ) |
24 | 23 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝐶‘𝑗) ∈ ℝ) |
25 | 6 | zred 12282 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → 𝑃 ∈ ℝ) |
26 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → ¬ 𝑃 < (𝐶‘𝑗)) |
27 | 24, 25, 26 | nltled 10982 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝐶‘𝑗) ≤ 𝑃) |
28 | 25, 24 | subge0d 11422 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (0 ≤ (𝑃 − (𝐶‘𝑗)) ↔ (𝐶‘𝑗) ≤ 𝑃)) |
29 | 27, 28 | mpbird 260 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → 0 ≤ (𝑃 − (𝐶‘𝑗))) |
30 | | elfzle1 13115 |
. . . . . . . . . 10
⊢ ((𝐶‘𝑗) ∈ (0...𝑁) → 0 ≤ (𝐶‘𝑗)) |
31 | 19, 30 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 0 ≤ (𝐶‘𝑗)) |
32 | 31 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → 0 ≤ (𝐶‘𝑗)) |
33 | 25, 24 | subge02d 11424 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (0 ≤ (𝐶‘𝑗) ↔ (𝑃 − (𝐶‘𝑗)) ≤ 𝑃)) |
34 | 32, 33 | mpbid 235 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝑃 − (𝐶‘𝑗)) ≤ 𝑃) |
35 | 3, 6, 22, 29, 34 | elfzd 13103 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝑃 − (𝐶‘𝑗)) ∈ (0...𝑃)) |
36 | | permnn 13892 |
. . . . . 6
⊢ ((𝑃 − (𝐶‘𝑗)) ∈ (0...𝑃) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) ∈ ℕ) |
37 | 35, 36 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) ∈ ℕ) |
38 | 37 | nnzd 12281 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) ∈ ℤ) |
39 | | etransclem7.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) |
40 | 39 | elfzelzd 13113 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ ℤ) |
41 | 40 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐽 ∈ ℤ) |
42 | | elfzelz 13112 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℤ) |
43 | 42 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℤ) |
44 | 41, 43 | zsubcld 12287 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐽 − 𝑗) ∈ ℤ) |
45 | 44 | adantr 484 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝐽 − 𝑗) ∈ ℤ) |
46 | | elnn0z 12189 |
. . . . . 6
⊢ ((𝑃 − (𝐶‘𝑗)) ∈ ℕ0 ↔ ((𝑃 − (𝐶‘𝑗)) ∈ ℤ ∧ 0 ≤ (𝑃 − (𝐶‘𝑗)))) |
47 | 22, 29, 46 | sylanbrc 586 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝑃 − (𝐶‘𝑗)) ∈
ℕ0) |
48 | | zexpcl 13650 |
. . . . 5
⊢ (((𝐽 − 𝑗) ∈ ℤ ∧ (𝑃 − (𝐶‘𝑗)) ∈ ℕ0) → ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))) ∈ ℤ) |
49 | 45, 47, 48 | syl2anc 587 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))) ∈ ℤ) |
50 | 38, 49 | zmulcld 12288 |
. . 3
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))) ∈ ℤ) |
51 | 2, 50 | ifclda 4474 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) |
52 | 1, 51 | fprodzcl 15516 |
1
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) |