Proof of Theorem fourierdlem40
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fourierdlem40.h | . . . . 5
⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) | 
| 2 | 1 | reseq1i 5993 | . . . 4
⊢ (𝐻 ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ (𝐴(,)𝐵)) | 
| 3 | 2 | a1i 11 | . . 3
⊢ (𝜑 → (𝐻 ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ (𝐴(,)𝐵))) | 
| 4 |  | pire 26500 | . . . . . . . . 9
⊢ π
∈ ℝ | 
| 5 | 4 | renegcli 11570 | . . . . . . . 8
⊢ -π
∈ ℝ | 
| 6 | 5 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -π ∈
ℝ) | 
| 7 | 4 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → π ∈
ℝ) | 
| 8 |  | elioore 13417 | . . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ) | 
| 9 | 8 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ) | 
| 10 | 5 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → -π ∈
ℝ) | 
| 11 | 4 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → π ∈
ℝ) | 
| 12 | 10, 11 | iccssred 13474 | . . . . . . . . . . 11
⊢ (𝜑 → (-π[,]π) ⊆
ℝ) | 
| 13 |  | fourierdlem40.a | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ (-π[,]π)) | 
| 14 | 12, 13 | sseldd 3984 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 15 | 14 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) | 
| 16 | 5, 4 | elicc2i 13453 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ (-π[,]π) ↔
(𝐴 ∈ ℝ ∧
-π ≤ 𝐴 ∧ 𝐴 ≤ π)) | 
| 17 | 16 | simp2bi 1147 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (-π[,]π) →
-π ≤ 𝐴) | 
| 18 | 13, 17 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → -π ≤ 𝐴) | 
| 19 | 18 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -π ≤ 𝐴) | 
| 20 | 15 | rexrd 11311 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈
ℝ*) | 
| 21 |  | fourierdlem40.b | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ (-π[,]π)) | 
| 22 | 12, 21 | sseldd 3984 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 23 | 22 | rexrd 11311 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 24 | 23 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈
ℝ*) | 
| 25 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵)) | 
| 26 |  | ioogtlb 45508 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) | 
| 27 | 20, 24, 25, 26 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) | 
| 28 | 6, 15, 9, 19, 27 | lelttrd 11419 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -π < 𝑠) | 
| 29 | 6, 9, 28 | ltled 11409 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -π ≤ 𝑠) | 
| 30 | 22 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ) | 
| 31 |  | iooltub 45523 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) | 
| 32 | 20, 24, 25, 31 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) | 
| 33 | 5, 4 | elicc2i 13453 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ (-π[,]π) ↔
(𝐵 ∈ ℝ ∧
-π ≤ 𝐵 ∧ 𝐵 ≤ π)) | 
| 34 | 33 | simp3bi 1148 | . . . . . . . . . . 11
⊢ (𝐵 ∈ (-π[,]π) →
𝐵 ≤
π) | 
| 35 | 21, 34 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ≤ π) | 
| 36 | 35 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ≤ π) | 
| 37 | 9, 30, 7, 32, 36 | ltletrd 11421 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < π) | 
| 38 | 9, 7, 37 | ltled 11409 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≤ π) | 
| 39 | 6, 7, 9, 29, 38 | eliccd 45517 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (-π[,]π)) | 
| 40 | 39 | ex 412 | . . . . 5
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ (-π[,]π))) | 
| 41 | 40 | ssrdv 3989 | . . . 4
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π)) | 
| 42 | 41 | resmptd 6058 | . . 3
⊢ (𝜑 → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))) | 
| 43 |  | eleq1 2829 | . . . . . . . . 9
⊢ (𝑠 = 0 → (𝑠 ∈ (𝐴(,)𝐵) ↔ 0 ∈ (𝐴(,)𝐵))) | 
| 44 | 43 | biimpac 478 | . . . . . . . 8
⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵)) | 
| 45 | 44 | adantll 714 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵)) | 
| 46 |  | fourierdlem40.nxelab | . . . . . . . 8
⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵)) | 
| 47 | 46 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴(,)𝐵)) | 
| 48 | 45, 47 | pm2.65da 817 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 = 0) | 
| 49 | 48 | iffalsed 4536 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) | 
| 50 |  | fourierdlem40.f | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) | 
| 51 | 50 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ) | 
| 52 |  | fourierdlem40.x | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 53 | 52 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ) | 
| 54 | 53, 9 | readdcld 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ) | 
| 55 | 51, 54 | ffvelcdmd 7105 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ) | 
| 56 |  | fourierdlem40.y | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 57 |  | fourierdlem40.w | . . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ ℝ) | 
| 58 | 56, 57 | ifcld 4572 | . . . . . . . . 9
⊢ (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ) | 
| 59 | 58 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ) | 
| 60 | 55, 59 | resubcld 11691 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℝ) | 
| 61 | 60 | recnd 11289 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ) | 
| 62 | 9 | recnd 11289 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℂ) | 
| 63 | 48 | neqned 2947 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0) | 
| 64 | 61, 62, 63 | divrecd 12046 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠))) | 
| 65 | 49, 64 | eqtrd 2777 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠))) | 
| 66 | 65 | mpteq2dva 5242 | . . 3
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠)))) | 
| 67 | 3, 42, 66 | 3eqtrd 2781 | . 2
⊢ (𝜑 → (𝐻 ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠)))) | 
| 68 | 55 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ) | 
| 69 | 59 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ) | 
| 70 | 68, 69 | negsubd 11626 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) | 
| 71 | 70 | eqcomd 2743 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊))) | 
| 72 | 71 | mpteq2dva 5242 | . . . 4
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊)))) | 
| 73 | 14, 52 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 + 𝑋) ∈ ℝ) | 
| 74 | 73 | rexrd 11311 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + 𝑋) ∈
ℝ*) | 
| 75 | 74 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) ∈
ℝ*) | 
| 76 | 22, 52 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 + 𝑋) ∈ ℝ) | 
| 77 | 76 | rexrd 11311 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐵 + 𝑋) ∈
ℝ*) | 
| 78 | 77 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐵 + 𝑋) ∈
ℝ*) | 
| 79 | 14 | recnd 11289 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 80 | 52 | recnd 11289 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 81 | 79, 80 | addcomd 11463 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 + 𝑋) = (𝑋 + 𝐴)) | 
| 82 | 81 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) = (𝑋 + 𝐴)) | 
| 83 | 15, 9, 53, 27 | ltadd2dd 11420 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠)) | 
| 84 | 82, 83 | eqbrtrd 5165 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) < (𝑋 + 𝑠)) | 
| 85 | 9, 30, 53, 32 | ltadd2dd 11420 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵)) | 
| 86 | 22 | recnd 11289 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 87 | 80, 86 | addcomd 11463 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 + 𝐵) = (𝐵 + 𝑋)) | 
| 88 | 87 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) = (𝐵 + 𝑋)) | 
| 89 | 85, 88 | breqtrd 5169 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝐵 + 𝑋)) | 
| 90 | 75, 78, 54, 84, 89 | eliood 45511 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋))) | 
| 91 |  | fvres 6925 | . . . . . . . . 9
⊢ ((𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) → ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠))) | 
| 92 | 90, 91 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠))) | 
| 93 | 92 | eqcomd 2743 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠))) | 
| 94 | 93 | mpteq2dva 5242 | . . . . . 6
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)))) | 
| 95 |  | ioosscn 13449 | . . . . . . . 8
⊢ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) ⊆ ℂ | 
| 96 | 95 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) ⊆ ℂ) | 
| 97 |  | fourierdlem40.fcn | . . . . . . 7
⊢ (𝜑 → (𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐵 + 𝑋))–cn→ℂ)) | 
| 98 |  | ioosscn 13449 | . . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ ℂ | 
| 99 | 98 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) | 
| 100 | 96, 97, 99, 80, 90 | fourierdlem23 46145 | . . . . . 6
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 101 | 94, 100 | eqeltrd 2841 | . . . . 5
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 102 |  | 0red 11264 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ) | 
| 103 | 14 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) | 
| 104 | 8 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ) | 
| 105 |  | simplr 769 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ≤ 𝐴) | 
| 106 | 27 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) | 
| 107 | 102, 103,
104, 105, 106 | lelttrd 11419 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 < 𝑠) | 
| 108 | 107 | iftrued 4533 | . . . . . . . . 9
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌) | 
| 109 | 108 | negeqd 11502 | . . . . . . . 8
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -if(0 < 𝑠, 𝑌, 𝑊) = -𝑌) | 
| 110 | 109 | mpteq2dva 5242 | . . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌)) | 
| 111 | 56 | renegcld 11690 | . . . . . . . . . 10
⊢ (𝜑 → -𝑌 ∈ ℝ) | 
| 112 | 111 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → -𝑌 ∈ ℂ) | 
| 113 |  | ssid 4006 | . . . . . . . . . 10
⊢ ℂ
⊆ ℂ | 
| 114 | 113 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 115 | 99, 112, 114 | constcncfg 45887 | . . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 116 | 115 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 117 | 110, 116 | eqeltrd 2841 | . . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 118 | 14 | rexrd 11311 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 119 | 118 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐴 ∈
ℝ*) | 
| 120 | 23 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐵 ∈
ℝ*) | 
| 121 |  | 0red 11264 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 ∈
ℝ) | 
| 122 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → ¬ 0 ≤ 𝐴) | 
| 123 | 14 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐴 ∈ ℝ) | 
| 124 |  | 0red 11264 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 0 ∈
ℝ) | 
| 125 | 123, 124 | ltnled 11408 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → (𝐴 < 0 ↔ ¬ 0 ≤ 𝐴)) | 
| 126 | 122, 125 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐴 < 0) | 
| 127 | 126 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐴 < 0) | 
| 128 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 0) → ¬ 𝐵 ≤ 0) | 
| 129 |  | 0red 11264 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 0 ∈
ℝ) | 
| 130 | 22 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 𝐵 ∈ ℝ) | 
| 131 | 129, 130 | ltnled 11408 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 0) → (0 < 𝐵 ↔ ¬ 𝐵 ≤ 0)) | 
| 132 | 128, 131 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 0 < 𝐵) | 
| 133 | 132 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 < 𝐵) | 
| 134 | 119, 120,
121, 127, 133 | eliood 45511 | . . . . . . . 8
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 ∈ (𝐴(,)𝐵)) | 
| 135 | 46 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → ¬ 0 ∈ (𝐴(,)𝐵)) | 
| 136 | 134, 135 | condan 818 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐵 ≤ 0) | 
| 137 | 8 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ) | 
| 138 |  | 0red 11264 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ) | 
| 139 | 22 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ) | 
| 140 | 32 | adantlr 715 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) | 
| 141 |  | simplr 769 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ≤ 0) | 
| 142 | 137, 139,
138, 140, 141 | ltletrd 11421 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 0) | 
| 143 | 137, 138,
142 | ltnsymd 11410 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 0 < 𝑠) | 
| 144 | 143 | iffalsed 4536 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊) | 
| 145 | 144 | negeqd 11502 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -if(0 < 𝑠, 𝑌, 𝑊) = -𝑊) | 
| 146 | 145 | mpteq2dva 5242 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊)) | 
| 147 | 57 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ ℂ) | 
| 148 | 147 | negcld 11607 | . . . . . . . . . 10
⊢ (𝜑 → -𝑊 ∈ ℂ) | 
| 149 | 99, 148, 114 | constcncfg 45887 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 150 | 149 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 151 | 146, 150 | eqeltrd 2841 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 152 | 136, 151 | syldan 591 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 153 | 117, 152 | pm2.61dan 813 | . . . . 5
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 154 | 101, 153 | addcncf 25478 | . . . 4
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 155 | 72, 154 | eqeltrd 2841 | . . 3
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 156 |  | eqid 2737 | . . . 4
⊢ (𝑠 ∈ (ℂ ∖ {0})
↦ (1 / 𝑠)) = (𝑠 ∈ (ℂ ∖ {0})
↦ (1 / 𝑠)) | 
| 157 |  | 1cnd 11256 | . . . . 5
⊢ (𝜑 → 1 ∈
ℂ) | 
| 158 | 156 | cdivcncf 24947 | . . . . 5
⊢ (1 ∈
ℂ → (𝑠 ∈
(ℂ ∖ {0}) ↦ (1 / 𝑠)) ∈ ((ℂ ∖ {0})–cn→ℂ)) | 
| 159 | 157, 158 | syl 17 | . . . 4
⊢ (𝜑 → (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑠)) ∈ ((ℂ
∖ {0})–cn→ℂ)) | 
| 160 |  | velsn 4642 | . . . . . . . 8
⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0) | 
| 161 | 48, 160 | sylnibr 329 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 ∈ {0}) | 
| 162 | 62, 161 | eldifd 3962 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (ℂ ∖
{0})) | 
| 163 | 162 | ralrimiva 3146 | . . . . 5
⊢ (𝜑 → ∀𝑠 ∈ (𝐴(,)𝐵)𝑠 ∈ (ℂ ∖
{0})) | 
| 164 |  | dfss3 3972 | . . . . 5
⊢ ((𝐴(,)𝐵) ⊆ (ℂ ∖ {0}) ↔
∀𝑠 ∈ (𝐴(,)𝐵)𝑠 ∈ (ℂ ∖
{0})) | 
| 165 | 163, 164 | sylibr 234 | . . . 4
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (ℂ ∖
{0})) | 
| 166 | 9, 63 | rereccld 12094 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (1 / 𝑠) ∈ ℝ) | 
| 167 | 166 | recnd 11289 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (1 / 𝑠) ∈ ℂ) | 
| 168 | 156, 159,
165, 114, 167 | cncfmptssg 45886 | . . 3
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 169 | 155, 168 | mulcncf 25480 | . 2
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 170 | 67, 169 | eqeltrd 2841 | 1
⊢ (𝜑 → (𝐻 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |