Proof of Theorem etransclem10
Step | Hyp | Ref
| Expression |
1 | | 0zd 12086 |
. 2
⊢ ((𝜑 ∧ (𝑃 − 1) < (𝐶‘0)) → 0 ∈
ℤ) |
2 | | 0zd 12086 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℤ) |
3 | | etransclem10.n |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℕ) |
4 | | nnm1nn0 12029 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
5 | 3, 4 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
6 | 5 | nn0zd 12178 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − 1) ∈ ℤ) |
7 | | etransclem10.c |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) |
8 | | etransclem10.m |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
9 | | nn0uz 12374 |
. . . . . . . . . . . . . 14
⊢
ℕ0 = (ℤ≥‘0) |
10 | 8, 9 | eleqtrdi 2844 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
11 | | eluzfz1 13017 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑀)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
13 | 7, 12 | ffvelrnd 6874 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶‘0) ∈ (0...𝑁)) |
14 | 13 | elfzelzd 13011 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶‘0) ∈ ℤ) |
15 | 6, 14 | zsubcld 12185 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 − 1) − (𝐶‘0)) ∈ ℤ) |
16 | 2, 6, 15 | 3jca 1129 |
. . . . . . . 8
⊢ (𝜑 → (0 ∈ ℤ ∧
(𝑃 − 1) ∈
ℤ ∧ ((𝑃 −
1) − (𝐶‘0))
∈ ℤ)) |
17 | 16 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (0 ∈ ℤ ∧
(𝑃 − 1) ∈
ℤ ∧ ((𝑃 −
1) − (𝐶‘0))
∈ ℤ)) |
18 | 14 | zred 12180 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶‘0) ∈ ℝ) |
19 | 18 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (𝐶‘0) ∈ ℝ) |
20 | 5 | nn0red 12049 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 − 1) ∈ ℝ) |
21 | 20 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (𝑃 − 1) ∈ ℝ) |
22 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ¬ (𝑃 − 1) < (𝐶‘0)) |
23 | 19, 21, 22 | nltled 10880 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (𝐶‘0) ≤ (𝑃 − 1)) |
24 | 21, 19 | subge0d 11320 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (0 ≤ ((𝑃 − 1) − (𝐶‘0)) ↔ (𝐶‘0) ≤ (𝑃 − 1))) |
25 | 23, 24 | mpbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → 0 ≤ ((𝑃 − 1) − (𝐶‘0))) |
26 | | elfzle1 13013 |
. . . . . . . . . 10
⊢ ((𝐶‘0) ∈ (0...𝑁) → 0 ≤ (𝐶‘0)) |
27 | 13, 26 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝐶‘0)) |
28 | 27 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → 0 ≤ (𝐶‘0)) |
29 | 21, 19 | subge02d 11322 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (0 ≤ (𝐶‘0) ↔ ((𝑃 − 1) − (𝐶‘0)) ≤ (𝑃 − 1))) |
30 | 28, 29 | mpbid 235 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ((𝑃 − 1) − (𝐶‘0)) ≤ (𝑃 − 1)) |
31 | 17, 25, 30 | jca32 519 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ((0 ∈ ℤ ∧
(𝑃 − 1) ∈
ℤ ∧ ((𝑃 −
1) − (𝐶‘0))
∈ ℤ) ∧ (0 ≤ ((𝑃 − 1) − (𝐶‘0)) ∧ ((𝑃 − 1) − (𝐶‘0)) ≤ (𝑃 − 1)))) |
32 | | elfz2 13000 |
. . . . . 6
⊢ (((𝑃 − 1) − (𝐶‘0)) ∈ (0...(𝑃 − 1)) ↔ ((0 ∈
ℤ ∧ (𝑃 − 1)
∈ ℤ ∧ ((𝑃
− 1) − (𝐶‘0)) ∈ ℤ) ∧ (0 ≤
((𝑃 − 1) −
(𝐶‘0)) ∧ ((𝑃 − 1) − (𝐶‘0)) ≤ (𝑃 − 1)))) |
33 | 31, 32 | sylibr 237 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ((𝑃 − 1) − (𝐶‘0)) ∈ (0...(𝑃 − 1))) |
34 | | permnn 13790 |
. . . . 5
⊢ (((𝑃 − 1) − (𝐶‘0)) ∈ (0...(𝑃 − 1)) →
((!‘(𝑃 − 1)) /
(!‘((𝑃 − 1)
− (𝐶‘0))))
∈ ℕ) |
35 | 33, 34 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) ∈
ℕ) |
36 | 35 | nnzd 12179 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) ∈
ℤ) |
37 | | etransclem10.j |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ ℤ) |
38 | 37 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → 𝐽 ∈ ℤ) |
39 | 15 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ((𝑃 − 1) − (𝐶‘0)) ∈ ℤ) |
40 | | elnn0z 12087 |
. . . . 5
⊢ (((𝑃 − 1) − (𝐶‘0)) ∈
ℕ0 ↔ (((𝑃 − 1) − (𝐶‘0)) ∈ ℤ ∧ 0 ≤
((𝑃 − 1) −
(𝐶‘0)))) |
41 | 39, 25, 40 | sylanbrc 586 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ((𝑃 − 1) − (𝐶‘0)) ∈
ℕ0) |
42 | | zexpcl 13548 |
. . . 4
⊢ ((𝐽 ∈ ℤ ∧ ((𝑃 − 1) − (𝐶‘0)) ∈
ℕ0) → (𝐽↑((𝑃 − 1) − (𝐶‘0))) ∈ ℤ) |
43 | 38, 41, 42 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (𝐽↑((𝑃 − 1) − (𝐶‘0))) ∈ ℤ) |
44 | 36, 43 | zmulcld 12186 |
. 2
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0)))) ∈
ℤ) |
45 | 1, 44 | ifclda 4459 |
1
⊢ (𝜑 → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) ∈
ℤ) |