Step | Hyp | Ref
| Expression |
1 | | ioossicc 12259 |
. . 3
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
3 | | ioombl 23333 |
. . 3
⊢ (𝐴(,)𝐵) ∈ dom vol |
4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
5 | | ere 14819 |
. . . . . 6
⊢ e ∈
ℝ |
6 | 5 | recni 10052 |
. . . . 5
⊢ e ∈
ℂ |
7 | 6 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → e ∈ ℂ) |
8 | | etransclem18.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
9 | | etransclem18.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
10 | 8, 9 | iccssred 39727 |
. . . . . . 7
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
11 | 10 | sselda 3603 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
12 | 11 | recnd 10068 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℂ) |
13 | 12 | negcld 10379 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → -𝑥 ∈ ℂ) |
14 | 7, 13 | cxpcld 24454 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (e↑𝑐-𝑥) ∈
ℂ) |
15 | | etransclem18.s |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
16 | | etransclem18.x |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
17 | 15, 16 | dvdmsscn 40151 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
18 | | etransclem18.p |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℕ) |
19 | | etransclem18.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) |
20 | 17, 18, 19 | etransclem8 40459 |
. . . . 5
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) |
21 | 20 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℂ) |
22 | 21, 11 | ffvelrnd 6360 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
23 | 14, 22 | mulcld 10060 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) →
((e↑𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ) |
24 | | eqidd 2623 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ ℂ ↦
(e↑𝑐𝑦)) = (𝑦 ∈ ℂ ↦
(e↑𝑐𝑦))) |
25 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑦 = -𝑥 → (e↑𝑐𝑦) =
(e↑𝑐-𝑥)) |
26 | 25 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑦 = -𝑥) → (e↑𝑐𝑦) =
(e↑𝑐-𝑥)) |
27 | 10, 17 | sstrd 3613 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
28 | 27 | sselda 3603 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℂ) |
29 | 28 | negcld 10379 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → -𝑥 ∈ ℂ) |
30 | 6 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → e ∈
ℂ) |
31 | | negcl 10281 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → -𝑥 ∈
ℂ) |
32 | 30, 31 | cxpcld 24454 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ →
(e↑𝑐-𝑥) ∈ ℂ) |
33 | 28, 32 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (e↑𝑐-𝑥) ∈
ℂ) |
34 | 24, 26, 29, 33 | fvmptd 6288 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑦 ∈ ℂ ↦
(e↑𝑐𝑦))‘-𝑥) = (e↑𝑐-𝑥)) |
35 | 34 | eqcomd 2628 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (e↑𝑐-𝑥) = ((𝑦 ∈ ℂ ↦
(e↑𝑐𝑦))‘-𝑥)) |
36 | 35 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (e↑𝑐-𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑦 ∈ ℂ ↦
(e↑𝑐𝑦))‘-𝑥))) |
37 | | epr 14936 |
. . . . . . . . 9
⊢ e ∈
ℝ+ |
38 | | mnfxr 10096 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ (e ∈
ℝ+ → -∞ ∈
ℝ*) |
40 | | 0red 10041 |
. . . . . . . . . 10
⊢ (e ∈
ℝ+ → 0 ∈ ℝ) |
41 | | rpxr 11840 |
. . . . . . . . . 10
⊢ (e ∈
ℝ+ → e ∈ ℝ*) |
42 | | rpgt0 11844 |
. . . . . . . . . 10
⊢ (e ∈
ℝ+ → 0 < e) |
43 | 39, 40, 41, 42 | gtnelioc 39712 |
. . . . . . . . 9
⊢ (e ∈
ℝ+ → ¬ e ∈ (-∞(,]0)) |
44 | 37, 43 | ax-mp 5 |
. . . . . . . 8
⊢ ¬ e
∈ (-∞(,]0) |
45 | | eldif 3584 |
. . . . . . . 8
⊢ (e ∈
(ℂ ∖ (-∞(,]0)) ↔ (e ∈ ℂ ∧ ¬ e ∈
(-∞(,]0))) |
46 | 6, 44, 45 | mpbir2an 955 |
. . . . . . 7
⊢ e ∈
(ℂ ∖ (-∞(,]0)) |
47 | | cxpcncf2 40113 |
. . . . . . 7
⊢ (e ∈
(ℂ ∖ (-∞(,]0)) → (𝑦 ∈ ℂ ↦
(e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ)) |
48 | 46, 47 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ℂ ↦
(e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ)) |
49 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ -𝑥) = (𝑥 ∈ (𝐴[,]𝐵) ↦ -𝑥) |
50 | 49 | negcncf 22721 |
. . . . . . 7
⊢ ((𝐴[,]𝐵) ⊆ ℂ → (𝑥 ∈ (𝐴[,]𝐵) ↦ -𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
51 | 27, 50 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ -𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
52 | 48, 51 | cncfmpt1f 22716 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑦 ∈ ℂ ↦
(e↑𝑐𝑦))‘-𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
53 | 36, 52 | eqeltrd 2701 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (e↑𝑐-𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
54 | | ax-resscn 9993 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
55 | 54 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ℝ ⊆
ℂ) |
56 | 18 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑃 ∈ ℕ) |
57 | | etransclem18.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
58 | 57 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑀 ∈
ℕ0) |
59 | | etransclem6 40457 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃))) |
60 | 19, 59 | eqtri 2644 |
. . . . . . 7
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃))) |
61 | 55, 56, 58, 60, 11 | etransclem13 40464 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) = ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) |
62 | 61 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) |
63 | | fzfid 12772 |
. . . . . 6
⊢ (𝜑 → (0...𝑀) ∈ Fin) |
64 | 12 | 3adant3 1081 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑘 ∈ (0...𝑀)) → 𝑥 ∈ ℂ) |
65 | | elfzelz 12342 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ) |
66 | 65 | zcnd 11483 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ) |
67 | 66 | 3ad2ant3 1084 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ) |
68 | 64, 67 | subcld 10392 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 − 𝑘) ∈ ℂ) |
69 | | nnm1nn0 11334 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
70 | 18, 69 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
71 | 18 | nnnn0d 11351 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
72 | 70, 71 | ifcld 4131 |
. . . . . . . 8
⊢ (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
73 | 72 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
74 | 68, 73 | expcld 13008 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ) |
75 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ (0...𝑀)) |
76 | | ssid 3624 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
77 | 76 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℂ ⊆
ℂ) |
78 | 27, 77 | idcncfg 40085 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
79 | 78 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
80 | 27 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝐴[,]𝐵) ⊆ ℂ) |
81 | 66 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ) |
82 | 76 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆
ℂ) |
83 | 80, 81, 82 | constcncfg 40084 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑘) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
84 | 79, 83 | subcncf 40082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 − 𝑘)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
85 | | expcncf 22725 |
. . . . . . . . 9
⊢ (if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ)) |
86 | 72, 85 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ)) |
87 | 86 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ)) |
88 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑦 = (𝑥 − 𝑘) → (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) |
89 | 75, 84, 87, 82, 88 | cncfcompt2 40112 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
90 | 27, 63, 74, 89 | fprodcncf 40114 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
91 | 62, 90 | eqeltrd 2701 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
92 | 53, 91 | mulcncf 23215 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦
((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
93 | | cniccibl 23607 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦
((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦
((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈
𝐿1) |
94 | 8, 9, 92, 93 | syl3anc 1326 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦
((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈
𝐿1) |
95 | 2, 4, 23, 94 | iblss 23571 |
1
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦
((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈
𝐿1) |