| Step | Hyp | Ref
| Expression |
| 1 | | ioossicc 13473 |
. . 3
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
| 2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
| 3 | | ioombl 25600 |
. . 3
⊢ (𝐴(,)𝐵) ∈ dom vol |
| 4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
| 5 | | ere 16125 |
. . . . . 6
⊢ e ∈
ℝ |
| 6 | 5 | recni 11275 |
. . . . 5
⊢ e ∈
ℂ |
| 7 | 6 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → e ∈ ℂ) |
| 8 | | etransclem18.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 9 | | etransclem18.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 10 | 8, 9 | iccssred 13474 |
. . . . . . 7
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
| 11 | 10 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
| 12 | 11 | recnd 11289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℂ) |
| 13 | 12 | negcld 11607 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → -𝑥 ∈ ℂ) |
| 14 | 7, 13 | cxpcld 26750 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (e↑𝑐-𝑥) ∈
ℂ) |
| 15 | | etransclem18.s |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
| 16 | | etransclem18.x |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
| 17 | 15, 16 | dvdmsscn 45951 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
| 18 | | etransclem18.p |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 19 | | etransclem18.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) |
| 20 | 17, 18, 19 | etransclem8 46257 |
. . . . 5
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) |
| 21 | 20 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℂ) |
| 22 | 21, 11 | ffvelcdmd 7105 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
| 23 | 14, 22 | mulcld 11281 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) →
((e↑𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ) |
| 24 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ ℂ ↦
(e↑𝑐𝑦)) = (𝑦 ∈ ℂ ↦
(e↑𝑐𝑦))) |
| 25 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑦 = -𝑥 → (e↑𝑐𝑦) =
(e↑𝑐-𝑥)) |
| 26 | 25 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑦 = -𝑥) → (e↑𝑐𝑦) =
(e↑𝑐-𝑥)) |
| 27 | 10, 17 | sstrd 3994 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
| 28 | 27 | sselda 3983 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℂ) |
| 29 | 28 | negcld 11607 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → -𝑥 ∈ ℂ) |
| 30 | 6 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → e ∈
ℂ) |
| 31 | | negcl 11508 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → -𝑥 ∈
ℂ) |
| 32 | 30, 31 | cxpcld 26750 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ →
(e↑𝑐-𝑥) ∈ ℂ) |
| 33 | 28, 32 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (e↑𝑐-𝑥) ∈
ℂ) |
| 34 | 24, 26, 29, 33 | fvmptd 7023 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑦 ∈ ℂ ↦
(e↑𝑐𝑦))‘-𝑥) = (e↑𝑐-𝑥)) |
| 35 | 34 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (e↑𝑐-𝑥) = ((𝑦 ∈ ℂ ↦
(e↑𝑐𝑦))‘-𝑥)) |
| 36 | 35 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (e↑𝑐-𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑦 ∈ ℂ ↦
(e↑𝑐𝑦))‘-𝑥))) |
| 37 | | epr 16244 |
. . . . . . . . 9
⊢ e ∈
ℝ+ |
| 38 | | mnfxr 11318 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
| 39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ (e ∈
ℝ+ → -∞ ∈
ℝ*) |
| 40 | | 0red 11264 |
. . . . . . . . . 10
⊢ (e ∈
ℝ+ → 0 ∈ ℝ) |
| 41 | | rpxr 13044 |
. . . . . . . . . 10
⊢ (e ∈
ℝ+ → e ∈ ℝ*) |
| 42 | | rpgt0 13047 |
. . . . . . . . . 10
⊢ (e ∈
ℝ+ → 0 < e) |
| 43 | 39, 40, 41, 42 | gtnelioc 45504 |
. . . . . . . . 9
⊢ (e ∈
ℝ+ → ¬ e ∈ (-∞(,]0)) |
| 44 | 37, 43 | ax-mp 5 |
. . . . . . . 8
⊢ ¬ e
∈ (-∞(,]0) |
| 45 | | eldif 3961 |
. . . . . . . 8
⊢ (e ∈
(ℂ ∖ (-∞(,]0)) ↔ (e ∈ ℂ ∧ ¬ e ∈
(-∞(,]0))) |
| 46 | 6, 44, 45 | mpbir2an 711 |
. . . . . . 7
⊢ e ∈
(ℂ ∖ (-∞(,]0)) |
| 47 | | cxpcncf2 45914 |
. . . . . . 7
⊢ (e ∈
(ℂ ∖ (-∞(,]0)) → (𝑦 ∈ ℂ ↦
(e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ)) |
| 48 | 46, 47 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ℂ ↦
(e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ)) |
| 49 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ -𝑥) = (𝑥 ∈ (𝐴[,]𝐵) ↦ -𝑥) |
| 50 | 49 | negcncf 24948 |
. . . . . . 7
⊢ ((𝐴[,]𝐵) ⊆ ℂ → (𝑥 ∈ (𝐴[,]𝐵) ↦ -𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 51 | 27, 50 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ -𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 52 | 48, 51 | cncfmpt1f 24940 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑦 ∈ ℂ ↦
(e↑𝑐𝑦))‘-𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 53 | 36, 52 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (e↑𝑐-𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 54 | | ax-resscn 11212 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
| 55 | 54 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ℝ ⊆
ℂ) |
| 56 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑃 ∈ ℕ) |
| 57 | | etransclem18.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
| 58 | 57 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑀 ∈
ℕ0) |
| 59 | | etransclem6 46255 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃))) |
| 60 | 19, 59 | eqtri 2765 |
. . . . . . 7
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃))) |
| 61 | 55, 56, 58, 60, 11 | etransclem13 46262 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) = ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) |
| 62 | 61 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) |
| 63 | | fzfid 14014 |
. . . . . 6
⊢ (𝜑 → (0...𝑀) ∈ Fin) |
| 64 | 12 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑘 ∈ (0...𝑀)) → 𝑥 ∈ ℂ) |
| 65 | | elfzelz 13564 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ) |
| 66 | 65 | zcnd 12723 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ) |
| 67 | 66 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ) |
| 68 | 64, 67 | subcld 11620 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 − 𝑘) ∈ ℂ) |
| 69 | | nnm1nn0 12567 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
| 70 | 18, 69 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
| 71 | 18 | nnnn0d 12587 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
| 72 | 70, 71 | ifcld 4572 |
. . . . . . . 8
⊢ (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
| 73 | 72 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
| 74 | 68, 73 | expcld 14186 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ) |
| 75 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ (0...𝑀)) |
| 76 | | ssid 4006 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
| 77 | 76 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℂ ⊆
ℂ) |
| 78 | 27, 77 | idcncfg 45888 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 79 | 78 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 80 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝐴[,]𝐵) ⊆ ℂ) |
| 81 | 66 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ) |
| 82 | 76 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆
ℂ) |
| 83 | 80, 81, 82 | constcncfg 45887 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑘) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 84 | 79, 83 | subcncf 25479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 − 𝑘)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 85 | | expcncf 24953 |
. . . . . . . . 9
⊢ (if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ)) |
| 86 | 72, 85 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ)) |
| 87 | 86 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ)) |
| 88 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑦 = (𝑥 − 𝑘) → (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) |
| 89 | 75, 84, 87, 82, 88 | cncfcompt2 24934 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 90 | 27, 63, 74, 89 | fprodcncf 45915 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 91 | 62, 90 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 92 | 53, 91 | mulcncf 25480 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦
((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 93 | | cniccibl 25876 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦
((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦
((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈
𝐿1) |
| 94 | 8, 9, 92, 93 | syl3anc 1373 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦
((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈
𝐿1) |
| 95 | 2, 4, 23, 94 | iblss 25840 |
1
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦
((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈
𝐿1) |