Proof of Theorem etransclem4
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0...𝑀)) |
2 | | etransclem4.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
3 | | cnex 9896 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
4 | 3 | ssex 4730 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ℂ → 𝐴 ∈ V) |
5 | | mptexg 6389 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝑥 ∈ 𝐴 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) ∈ V) |
6 | 2, 4, 5 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) ∈ V) |
7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ 𝐴 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) ∈ V) |
8 | | etransclem4.h |
. . . . . . . . 9
⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
9 | 8 | fvmpt2 6200 |
. . . . . . . 8
⊢ ((𝑗 ∈ (0...𝑀) ∧ (𝑥 ∈ 𝐴 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) ∈ V) → (𝐻‘𝑗) = (𝑥 ∈ 𝐴 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
10 | 1, 7, 9 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐻‘𝑗) = (𝑥 ∈ 𝐴 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
11 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)) ∈ V |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝐴) → ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)) ∈ V) |
13 | 10, 12 | fvmpt2d 6202 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝐴) → ((𝐻‘𝑗)‘𝑥) = ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) |
14 | 13 | an32s 842 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (0...𝑀)) → ((𝐻‘𝑗)‘𝑥) = ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) |
15 | 14 | prodeq2dv 14492 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∏𝑗 ∈ (0...𝑀)((𝐻‘𝑗)‘𝑥) = ∏𝑗 ∈ (0...𝑀)((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) |
16 | | etransclem4.M |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
17 | | nn0uz 11598 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
18 | 16, 17 | syl6eleq 2698 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
19 | 18 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈
(ℤ≥‘0)) |
20 | 2 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ) |
21 | 20 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (0...𝑀)) → 𝑥 ∈ ℂ) |
22 | | elfzelz 12213 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ) |
23 | 22 | zcnd 11359 |
. . . . . . . 8
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ) |
24 | 23 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ) |
25 | 21, 24 | subcld 10271 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 − 𝑗) ∈ ℂ) |
26 | | etransclem4.p |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) |
27 | | nnm1nn0 11211 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
29 | 26 | nnnn0d 11228 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
30 | 28, 29 | ifcld 4081 |
. . . . . . 7
⊢ (𝜑 → if(𝑗 = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
31 | 30 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (0...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
32 | 25, 31 | expcld 12870 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ) |
33 | | oveq2 6557 |
. . . . . 6
⊢ (𝑗 = 0 → (𝑥 − 𝑗) = (𝑥 − 0)) |
34 | | iftrue 4042 |
. . . . . 6
⊢ (𝑗 = 0 → if(𝑗 = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1)) |
35 | 33, 34 | oveq12d 6567 |
. . . . 5
⊢ (𝑗 = 0 → ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 − 0)↑(𝑃 − 1))) |
36 | 19, 32, 35 | fprod1p 14537 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∏𝑗 ∈ (0...𝑀)((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)) = (((𝑥 − 0)↑(𝑃 − 1)) · ∏𝑗 ∈ ((0 + 1)...𝑀)((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
37 | 20 | subid1d 10260 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 − 0) = 𝑥) |
38 | 37 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 − 0)↑(𝑃 − 1)) = (𝑥↑(𝑃 − 1))) |
39 | | 0p1e1 11009 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
40 | 39 | oveq1i 6559 |
. . . . . . . 8
⊢ ((0 +
1)...𝑀) = (1...𝑀) |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((0 + 1)...𝑀) = (1...𝑀)) |
42 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 0 ∈ ℝ) |
43 | | 1red 9934 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 1 ∈ ℝ) |
44 | | elfzelz 12213 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℤ) |
45 | 44 | zred 11358 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℝ) |
46 | | 0lt1 10429 |
. . . . . . . . . . . . . 14
⊢ 0 <
1 |
47 | 46 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 0 < 1) |
48 | | elfzle1 12215 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 1 ≤ 𝑗) |
49 | 42, 43, 45, 47, 48 | ltletrd 10076 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑀) → 0 < 𝑗) |
50 | 49 | gt0ne0d 10471 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ≠ 0) |
51 | 50 | neneqd 2787 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...𝑀) → ¬ 𝑗 = 0) |
52 | 51 | iffalsed 4047 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑀) → if(𝑗 = 0, (𝑃 − 1), 𝑃) = 𝑃) |
53 | 52 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...𝑀) → ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 − 𝑗)↑𝑃)) |
54 | 53 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 − 𝑗)↑𝑃)) |
55 | 41, 54 | prodeq12rdv 14496 |
. . . . . 6
⊢ (𝜑 → ∏𝑗 ∈ ((0 + 1)...𝑀)((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)) = ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)) |
56 | 55 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∏𝑗 ∈ ((0 + 1)...𝑀)((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)) = ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)) |
57 | 38, 56 | oveq12d 6567 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 − 0)↑(𝑃 − 1)) · ∏𝑗 ∈ ((0 + 1)...𝑀)((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) = ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) |
58 | 15, 36, 57 | 3eqtrrd 2649 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)) = ∏𝑗 ∈ (0...𝑀)((𝐻‘𝑗)‘𝑥)) |
59 | 58 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑥 ∈ 𝐴 ↦ ∏𝑗 ∈ (0...𝑀)((𝐻‘𝑗)‘𝑥))) |
60 | | etransclem4.f |
. 2
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) |
61 | | etransclem4.e |
. 2
⊢ 𝐸 = (𝑥 ∈ 𝐴 ↦ ∏𝑗 ∈ (0...𝑀)((𝐻‘𝑗)‘𝑥)) |
62 | 59, 60, 61 | 3eqtr4g 2669 |
1
⊢ (𝜑 → 𝐹 = 𝐸) |