Proof of Theorem etransclem3
Step | Hyp | Ref
| Expression |
1 | | 0zd 11996 |
. 2
⊢ ((𝜑 ∧ 𝑃 < (𝐶‘𝐽)) → 0 ∈ ℤ) |
2 | | 0zd 11996 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → 0 ∈ ℤ) |
3 | | etransclem3.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℕ) |
4 | 3 | nnzd 12089 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℤ) |
5 | 4 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → 𝑃 ∈ ℤ) |
6 | | etransclem3.c |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) |
7 | | etransclem3.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) |
8 | 6, 7 | ffvelrnd 6855 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶‘𝐽) ∈ (0...𝑁)) |
9 | 8 | elfzelzd 41588 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶‘𝐽) ∈ ℤ) |
10 | 4, 9 | zsubcld 12095 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − (𝐶‘𝐽)) ∈ ℤ) |
11 | 10 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (𝑃 − (𝐶‘𝐽)) ∈ ℤ) |
12 | 2, 5, 11 | 3jca 1124 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (0 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − (𝐶‘𝐽)) ∈ ℤ)) |
13 | 9 | zred 12090 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶‘𝐽) ∈ ℝ) |
14 | 13 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (𝐶‘𝐽) ∈ ℝ) |
15 | 5 | zred 12090 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → 𝑃 ∈ ℝ) |
16 | | simpr 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → ¬ 𝑃 < (𝐶‘𝐽)) |
17 | 14, 15, 16 | nltled 10793 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (𝐶‘𝐽) ≤ 𝑃) |
18 | 15, 14 | subge0d 11233 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (0 ≤ (𝑃 − (𝐶‘𝐽)) ↔ (𝐶‘𝐽) ≤ 𝑃)) |
19 | 17, 18 | mpbird 259 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → 0 ≤ (𝑃 − (𝐶‘𝐽))) |
20 | | elfzle1 12913 |
. . . . . . . . . 10
⊢ ((𝐶‘𝐽) ∈ (0...𝑁) → 0 ≤ (𝐶‘𝐽)) |
21 | 8, 20 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝐶‘𝐽)) |
22 | 3 | nnred 11656 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℝ) |
23 | 22, 13 | subge02d 11235 |
. . . . . . . . 9
⊢ (𝜑 → (0 ≤ (𝐶‘𝐽) ↔ (𝑃 − (𝐶‘𝐽)) ≤ 𝑃)) |
24 | 21, 23 | mpbid 234 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 − (𝐶‘𝐽)) ≤ 𝑃) |
25 | 24 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (𝑃 − (𝐶‘𝐽)) ≤ 𝑃) |
26 | 12, 19, 25 | jca32 518 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → ((0 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − (𝐶‘𝐽)) ∈ ℤ) ∧ (0 ≤ (𝑃 − (𝐶‘𝐽)) ∧ (𝑃 − (𝐶‘𝐽)) ≤ 𝑃))) |
27 | | elfz2 12902 |
. . . . . 6
⊢ ((𝑃 − (𝐶‘𝐽)) ∈ (0...𝑃) ↔ ((0 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − (𝐶‘𝐽)) ∈ ℤ) ∧ (0 ≤ (𝑃 − (𝐶‘𝐽)) ∧ (𝑃 − (𝐶‘𝐽)) ≤ 𝑃))) |
28 | 26, 27 | sylibr 236 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (𝑃 − (𝐶‘𝐽)) ∈ (0...𝑃)) |
29 | | permnn 13689 |
. . . . 5
⊢ ((𝑃 − (𝐶‘𝐽)) ∈ (0...𝑃) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) ∈ ℕ) |
30 | 28, 29 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) ∈ ℕ) |
31 | 30 | nnzd 12089 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) ∈ ℤ) |
32 | | etransclem3.4 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℤ) |
33 | 7 | elfzelzd 41588 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ ℤ) |
34 | 32, 33 | zsubcld 12095 |
. . . . 5
⊢ (𝜑 → (𝐾 − 𝐽) ∈ ℤ) |
35 | 34 | adantr 483 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (𝐾 − 𝐽) ∈ ℤ) |
36 | | elnn0z 11997 |
. . . . 5
⊢ ((𝑃 − (𝐶‘𝐽)) ∈ ℕ0 ↔ ((𝑃 − (𝐶‘𝐽)) ∈ ℤ ∧ 0 ≤ (𝑃 − (𝐶‘𝐽)))) |
37 | 11, 19, 36 | sylanbrc 585 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (𝑃 − (𝐶‘𝐽)) ∈
ℕ0) |
38 | | zexpcl 13447 |
. . . 4
⊢ (((𝐾 − 𝐽) ∈ ℤ ∧ (𝑃 − (𝐶‘𝐽)) ∈ ℕ0) →
((𝐾 − 𝐽)↑(𝑃 − (𝐶‘𝐽))) ∈ ℤ) |
39 | 35, 37, 38 | syl2anc 586 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → ((𝐾 − 𝐽)↑(𝑃 − (𝐶‘𝐽))) ∈ ℤ) |
40 | 31, 39 | zmulcld 12096 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · ((𝐾 − 𝐽)↑(𝑃 − (𝐶‘𝐽)))) ∈ ℤ) |
41 | 1, 40 | ifclda 4504 |
1
⊢ (𝜑 → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · ((𝐾 − 𝐽)↑(𝑃 − (𝐶‘𝐽))))) ∈ ℤ) |