| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fourierdlem46.h | . . . . . . . . 9
⊢ 𝐻 = ({-π, π, 𝐶} ∪ ((-π[,]π) ∖
dom 𝐹)) | 
| 2 |  | pire 26500 | . . . . . . . . . . . . 13
⊢ π
∈ ℝ | 
| 3 | 2 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → π ∈
ℝ) | 
| 4 | 3 | renegcld 11690 | . . . . . . . . . . 11
⊢ (𝜑 → -π ∈
ℝ) | 
| 5 |  | fourierdlem46.c | . . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 6 |  | tpssi 4838 | . . . . . . . . . . 11
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ ∧ 𝐶 ∈ ℝ) → {-π, π, 𝐶} ⊆
ℝ) | 
| 7 | 4, 3, 5, 6 | syl3anc 1373 | . . . . . . . . . 10
⊢ (𝜑 → {-π, π, 𝐶} ⊆
ℝ) | 
| 8 | 4, 3 | iccssred 13474 | . . . . . . . . . . 11
⊢ (𝜑 → (-π[,]π) ⊆
ℝ) | 
| 9 | 8 | ssdifssd 4147 | . . . . . . . . . 10
⊢ (𝜑 → ((-π[,]π) ∖
dom 𝐹) ⊆
ℝ) | 
| 10 | 7, 9 | unssd 4192 | . . . . . . . . 9
⊢ (𝜑 → ({-π, π, 𝐶} ∪ ((-π[,]π) ∖
dom 𝐹)) ⊆
ℝ) | 
| 11 | 1, 10 | eqsstrid 4022 | . . . . . . . 8
⊢ (𝜑 → 𝐻 ⊆ ℝ) | 
| 12 |  | fourierdlem46.qf | . . . . . . . . 9
⊢ (𝜑 → 𝑄:(0...𝑀)⟶𝐻) | 
| 13 |  | fourierdlem46.i | . . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ (0..^𝑀)) | 
| 14 |  | elfzofz 13715 | . . . . . . . . . 10
⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ∈ (0...𝑀)) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (0...𝑀)) | 
| 16 | 12, 15 | ffvelcdmd 7105 | . . . . . . . 8
⊢ (𝜑 → (𝑄‘𝐼) ∈ 𝐻) | 
| 17 | 11, 16 | sseldd 3984 | . . . . . . 7
⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ) | 
| 18 | 17 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝑄‘𝐼) ∈ ℝ) | 
| 19 |  | fzofzp1 13803 | . . . . . . . . . . 11
⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀)) | 
| 20 | 13, 19 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀)) | 
| 21 | 12, 20 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ 𝐻) | 
| 22 | 11, 21 | sseldd 3984 | . . . . . . . 8
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ) | 
| 23 | 22 | rexrd 11311 | . . . . . . 7
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈
ℝ*) | 
| 24 | 23 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) | 
| 25 |  | fourierdlem46.10 | . . . . . . 7
⊢ (𝜑 → (𝑄‘𝐼) < (𝑄‘(𝐼 + 1))) | 
| 26 | 25 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝑄‘𝐼) < (𝑄‘(𝐼 + 1))) | 
| 27 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝑄‘𝐼) ∈ dom 𝐹 ∧ 𝑥 = (𝑄‘𝐼)) → 𝑥 = (𝑄‘𝐼)) | 
| 28 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ (((𝑄‘𝐼) ∈ dom 𝐹 ∧ 𝑥 = (𝑄‘𝐼)) → (𝑄‘𝐼) ∈ dom 𝐹) | 
| 29 | 27, 28 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ (((𝑄‘𝐼) ∈ dom 𝐹 ∧ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ dom 𝐹) | 
| 30 | 29 | adantll 714 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) ∧ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ dom 𝐹) | 
| 31 | 30 | adantlr 715 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ dom 𝐹) | 
| 32 |  | ssun2 4179 | . . . . . . . . . . . . . . . . . . 19
⊢
((-π[,]π) ∖ dom 𝐹) ⊆ ({-π, π, 𝐶} ∪ ((-π[,]π) ∖ dom 𝐹)) | 
| 33 | 32, 1 | sseqtrri 4033 | . . . . . . . . . . . . . . . . . 18
⊢
((-π[,]π) ∖ dom 𝐹) ⊆ 𝐻 | 
| 34 |  | fourierdlem46.qiss | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆
(-π(,)π)) | 
| 35 |  | ioossicc 13473 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(-π(,)π) ⊆ (-π[,]π) | 
| 36 | 34, 35 | sstrdi 3996 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆
(-π[,]π)) | 
| 37 | 36 | sselda 3983 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ (-π[,]π)) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ (-π[,]π)) | 
| 39 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → ¬ 𝑥 ∈ dom 𝐹) | 
| 40 | 38, 39 | eldifd 3962 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ ((-π[,]π) ∖ dom 𝐹)) | 
| 41 | 33, 40 | sselid 3981 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ 𝐻) | 
| 42 |  | fourierdlem46.ranq | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ran 𝑄 = 𝐻) | 
| 43 | 42 | eqcomd 2743 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐻 = ran 𝑄) | 
| 44 | 43 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝐻 = ran 𝑄) | 
| 45 | 41, 44 | eleqtrd 2843 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ ran 𝑄) | 
| 46 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ran 𝑄) | 
| 47 |  | ffn 6736 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑄:(0...𝑀)⟶𝐻 → 𝑄 Fn (0...𝑀)) | 
| 48 | 12, 47 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑄 Fn (0...𝑀)) | 
| 49 | 48 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝑄) → 𝑄 Fn (0...𝑀)) | 
| 50 |  | fvelrnb 6969 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑄 Fn (0...𝑀) → (𝑥 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑥)) | 
| 51 | 49, 50 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝑄) → (𝑥 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑥)) | 
| 52 | 46, 51 | mpbid 232 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑥) | 
| 53 | 52 | adantlr 715 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑥) | 
| 54 |  | elfzelz 13564 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ) | 
| 55 | 54 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = 𝑥) → 𝑗 ∈ ℤ) | 
| 56 |  | simplll 775 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = 𝑥) → 𝜑) | 
| 57 |  | simplr 769 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = 𝑥) → 𝑗 ∈ (0...𝑀)) | 
| 58 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ (𝑄‘𝑗) = 𝑥) → (𝑄‘𝑗) = 𝑥) | 
| 59 |  | simplr 769 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ (𝑄‘𝑗) = 𝑥) → 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) | 
| 60 | 58, 59 | eqeltrd 2841 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ (𝑄‘𝑗) = 𝑥) → (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) | 
| 61 | 60 | adantlr 715 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = 𝑥) → (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) | 
| 62 |  | elfzoelz 13699 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ∈ ℤ) | 
| 63 | 13, 62 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐼 ∈ ℤ) | 
| 64 | 63 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝐼 ∈ ℤ) | 
| 65 | 17 | rexrd 11311 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑄‘𝐼) ∈
ℝ*) | 
| 66 | 65 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) ∈
ℝ*) | 
| 67 | 23 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) | 
| 68 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) | 
| 69 |  | ioogtlb 45508 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
(𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) < (𝑄‘𝑗)) | 
| 70 | 66, 67, 68, 69 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) < (𝑄‘𝑗)) | 
| 71 |  | fourierdlem46.qiso | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑄 Isom < , < ((0...𝑀), 𝐻)) | 
| 72 | 71 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑄 Isom < , < ((0...𝑀), 𝐻)) | 
| 73 | 15 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝐼 ∈ (0...𝑀)) | 
| 74 |  | simplr 769 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑗 ∈ (0...𝑀)) | 
| 75 |  | isorel 7346 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝐼 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑀))) → (𝐼 < 𝑗 ↔ (𝑄‘𝐼) < (𝑄‘𝑗))) | 
| 76 | 72, 73, 74, 75 | syl12anc 837 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝐼 < 𝑗 ↔ (𝑄‘𝐼) < (𝑄‘𝑗))) | 
| 77 | 70, 76 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝐼 < 𝑗) | 
| 78 |  | iooltub 45523 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
(𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝑗) < (𝑄‘(𝐼 + 1))) | 
| 79 | 66, 67, 68, 78 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝑗) < (𝑄‘(𝐼 + 1))) | 
| 80 | 20 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝐼 + 1) ∈ (0...𝑀)) | 
| 81 |  | isorel 7346 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑗 ∈ (0...𝑀) ∧ (𝐼 + 1) ∈ (0...𝑀))) → (𝑗 < (𝐼 + 1) ↔ (𝑄‘𝑗) < (𝑄‘(𝐼 + 1)))) | 
| 82 | 72, 74, 80, 81 | syl12anc 837 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑗 < (𝐼 + 1) ↔ (𝑄‘𝑗) < (𝑄‘(𝐼 + 1)))) | 
| 83 | 79, 82 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑗 < (𝐼 + 1)) | 
| 84 |  | btwnnz 12694 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐼 ∈ ℤ ∧ 𝐼 < 𝑗 ∧ 𝑗 < (𝐼 + 1)) → ¬ 𝑗 ∈ ℤ) | 
| 85 | 64, 77, 83, 84 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → ¬ 𝑗 ∈ ℤ) | 
| 86 | 56, 57, 61, 85 | syl21anc 838 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = 𝑥) → ¬ 𝑗 ∈ ℤ) | 
| 87 | 86 | adantllr 719 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = 𝑥) → ¬ 𝑗 ∈ ℤ) | 
| 88 | 55, 87 | pm2.65da 817 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) → ¬ (𝑄‘𝑗) = 𝑥) | 
| 89 | 88 | nrexdv 3149 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) → ¬ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑥) | 
| 90 | 53, 89 | pm2.65da 817 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → ¬ 𝑥 ∈ ran 𝑄) | 
| 91 | 90 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → ¬ 𝑥 ∈ ran 𝑄) | 
| 92 | 45, 91 | condan 818 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ dom 𝐹) | 
| 93 | 92 | ralrimiva 3146 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹) | 
| 94 |  | dfss3 3972 | . . . . . . . . . . . . . 14
⊢ (((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 ↔ ∀𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹) | 
| 95 | 93, 94 | sylibr 234 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹) | 
| 96 | 95 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹) | 
| 97 | 65 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → (𝑄‘𝐼) ∈
ℝ*) | 
| 98 | 23 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) | 
| 99 |  | icossre 13468 | . . . . . . . . . . . . . . . 16
⊢ (((𝑄‘𝐼) ∈ ℝ ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ*) →
((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ ℝ) | 
| 100 | 17, 23, 99 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ ℝ) | 
| 101 | 100 | sselda 3983 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ ℝ) | 
| 102 | 101 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ ℝ) | 
| 103 | 17 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → (𝑄‘𝐼) ∈ ℝ) | 
| 104 | 65 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) ∈
ℝ*) | 
| 105 | 23 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) | 
| 106 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) | 
| 107 |  | icogelb 13438 | . . . . . . . . . . . . . . . 16
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) ≤ 𝑥) | 
| 108 | 104, 105,
106, 107 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) ≤ 𝑥) | 
| 109 | 108 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → (𝑄‘𝐼) ≤ 𝑥) | 
| 110 |  | neqne 2948 | . . . . . . . . . . . . . . 15
⊢ (¬
𝑥 = (𝑄‘𝐼) → 𝑥 ≠ (𝑄‘𝐼)) | 
| 111 | 110 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → 𝑥 ≠ (𝑄‘𝐼)) | 
| 112 | 103, 102,
109, 111 | leneltd 11415 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → (𝑄‘𝐼) < 𝑥) | 
| 113 |  | icoltub 45521 | . . . . . . . . . . . . . . 15
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 < (𝑄‘(𝐼 + 1))) | 
| 114 | 104, 105,
106, 113 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 < (𝑄‘(𝐼 + 1))) | 
| 115 | 114 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → 𝑥 < (𝑄‘(𝐼 + 1))) | 
| 116 | 97, 98, 102, 112, 115 | eliood 45511 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) | 
| 117 | 96, 116 | sseldd 3984 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ dom 𝐹) | 
| 118 | 117 | adantllr 719 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ dom 𝐹) | 
| 119 | 31, 118 | pm2.61dan 813 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ dom 𝐹) | 
| 120 | 119 | ralrimiva 3146 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ∀𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹) | 
| 121 |  | dfss3 3972 | . . . . . . . 8
⊢ (((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 ↔ ∀𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹) | 
| 122 | 120, 121 | sylibr 234 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹) | 
| 123 |  | fourierdlem46.cn | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (dom 𝐹–cn→ℂ)) | 
| 124 | 123 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → 𝐹 ∈ (dom 𝐹–cn→ℂ)) | 
| 125 |  | rescncf 24923 | . . . . . . 7
⊢ (((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 → (𝐹 ∈ (dom 𝐹–cn→ℂ) → (𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∈ (((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))–cn→ℂ))) | 
| 126 | 122, 124,
125 | sylc 65 | . . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∈ (((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))–cn→ℂ)) | 
| 127 | 18, 24, 26, 126 | icocncflimc 45904 | . . . . 5
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄‘𝐼)) ∈ (((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼))) | 
| 128 | 17 | leidd 11829 | . . . . . . . . 9
⊢ (𝜑 → (𝑄‘𝐼) ≤ (𝑄‘𝐼)) | 
| 129 | 65, 23, 65, 128, 25 | elicod 13437 | . . . . . . . 8
⊢ (𝜑 → (𝑄‘𝐼) ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) | 
| 130 |  | fvres 6925 | . . . . . . . 8
⊢ ((𝑄‘𝐼) ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) → ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄‘𝐼)) = (𝐹‘(𝑄‘𝐼))) | 
| 131 | 129, 130 | syl 17 | . . . . . . 7
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄‘𝐼)) = (𝐹‘(𝑄‘𝐼))) | 
| 132 | 131 | eqcomd 2743 | . . . . . 6
⊢ (𝜑 → (𝐹‘(𝑄‘𝐼)) = ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄‘𝐼))) | 
| 133 | 132 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝐹‘(𝑄‘𝐼)) = ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄‘𝐼))) | 
| 134 |  | ioossico 13478 | . . . . . . . . 9
⊢ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) | 
| 135 | 134 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) | 
| 136 | 135 | resabs1d 6026 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) | 
| 137 | 136 | eqcomd 2743 | . . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) | 
| 138 | 137 | oveq1d 7446 | . . . . 5
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) = (((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼))) | 
| 139 | 127, 133,
138 | 3eltr4d 2856 | . . . 4
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝐹‘(𝑄‘𝐼)) ∈ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼))) | 
| 140 | 139 | ne0d 4342 | . . 3
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅) | 
| 141 |  | pnfxr 11315 | . . . . . . . . 9
⊢ +∞
∈ ℝ* | 
| 142 | 141 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → +∞ ∈
ℝ*) | 
| 143 | 22 | ltpnfd 13163 | . . . . . . . . . 10
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) < +∞) | 
| 144 | 23, 142, 143 | xrltled 13192 | . . . . . . . . 9
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ≤ +∞) | 
| 145 |  | iooss2 13423 | . . . . . . . . 9
⊢
((+∞ ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ≤ +∞) → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄‘𝐼)(,)+∞)) | 
| 146 | 141, 144,
145 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄‘𝐼)(,)+∞)) | 
| 147 | 146 | resabs1d 6026 | . . . . . . 7
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) | 
| 148 | 147 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) = ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼))) | 
| 149 | 148 | eqcomd 2743 | . . . . 5
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) = (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼))) | 
| 150 | 149 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) = (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼))) | 
| 151 |  | limcresi 25920 | . . . . 5
⊢ ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ⊆ (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) | 
| 152 | 17 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → (𝑄‘𝐼) ∈ ℝ) | 
| 153 |  | simpl 482 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → 𝜑) | 
| 154 | 2 | renegcli 11570 | . . . . . . . . . . . 12
⊢ -π
∈ ℝ | 
| 155 | 154 | rexri 11319 | . . . . . . . . . . 11
⊢ -π
∈ ℝ* | 
| 156 | 155 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → -π ∈
ℝ*) | 
| 157 | 2 | rexri 11319 | . . . . . . . . . . 11
⊢ π
∈ ℝ* | 
| 158 | 157 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → π ∈
ℝ*) | 
| 159 | 4, 3, 17, 22, 25, 34 | fourierdlem10 46132 | . . . . . . . . . . 11
⊢ (𝜑 → (-π ≤ (𝑄‘𝐼) ∧ (𝑄‘(𝐼 + 1)) ≤ π)) | 
| 160 | 159 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → -π ≤ (𝑄‘𝐼)) | 
| 161 | 159 | simprd 495 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ≤ π) | 
| 162 | 17, 22, 3, 25, 161 | ltletrd 11421 | . . . . . . . . . 10
⊢ (𝜑 → (𝑄‘𝐼) < π) | 
| 163 | 156, 158,
65, 160, 162 | elicod 13437 | . . . . . . . . 9
⊢ (𝜑 → (𝑄‘𝐼) ∈ (-π[,)π)) | 
| 164 | 163 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → (𝑄‘𝐼) ∈ (-π[,)π)) | 
| 165 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → ¬ (𝑄‘𝐼) ∈ dom 𝐹) | 
| 166 | 164, 165 | eldifd 3962 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → (𝑄‘𝐼) ∈ ((-π[,)π) ∖ dom 𝐹)) | 
| 167 | 153, 166 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → (𝜑 ∧ (𝑄‘𝐼) ∈ ((-π[,)π) ∖ dom 𝐹))) | 
| 168 |  | eleq1 2829 | . . . . . . . . 9
⊢ (𝑥 = (𝑄‘𝐼) → (𝑥 ∈ ((-π[,)π) ∖ dom 𝐹) ↔ (𝑄‘𝐼) ∈ ((-π[,)π) ∖ dom 𝐹))) | 
| 169 | 168 | anbi2d 630 | . . . . . . . 8
⊢ (𝑥 = (𝑄‘𝐼) → ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐹)) ↔ (𝜑 ∧ (𝑄‘𝐼) ∈ ((-π[,)π) ∖ dom 𝐹)))) | 
| 170 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑄‘𝐼) → (𝑥(,)+∞) = ((𝑄‘𝐼)(,)+∞)) | 
| 171 | 170 | reseq2d 5997 | . . . . . . . . . 10
⊢ (𝑥 = (𝑄‘𝐼) → (𝐹 ↾ (𝑥(,)+∞)) = (𝐹 ↾ ((𝑄‘𝐼)(,)+∞))) | 
| 172 |  | id 22 | . . . . . . . . . 10
⊢ (𝑥 = (𝑄‘𝐼) → 𝑥 = (𝑄‘𝐼)) | 
| 173 | 171, 172 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑥 = (𝑄‘𝐼) → ((𝐹 ↾ (𝑥(,)+∞)) limℂ 𝑥) = ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼))) | 
| 174 | 173 | neeq1d 3000 | . . . . . . . 8
⊢ (𝑥 = (𝑄‘𝐼) → (((𝐹 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅ ↔ ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ≠ ∅)) | 
| 175 | 169, 174 | imbi12d 344 | . . . . . . 7
⊢ (𝑥 = (𝑄‘𝐼) → (((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) ↔ ((𝜑 ∧ (𝑄‘𝐼) ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ≠ ∅))) | 
| 176 |  | fourierdlem46.rlim | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) | 
| 177 | 175, 176 | vtoclg 3554 | . . . . . 6
⊢ ((𝑄‘𝐼) ∈ ℝ → ((𝜑 ∧ (𝑄‘𝐼) ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ≠ ∅)) | 
| 178 | 152, 167,
177 | sylc 65 | . . . . 5
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ≠ ∅) | 
| 179 |  | ssn0 4404 | . . . . 5
⊢ ((((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ⊆ (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ∧ ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ≠ ∅) → (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅) | 
| 180 | 151, 178,
179 | sylancr 587 | . . . 4
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅) | 
| 181 | 150, 180 | eqnetrd 3008 | . . 3
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅) | 
| 182 | 140, 181 | pm2.61dan 813 | . 2
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅) | 
| 183 | 65 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘𝐼) ∈
ℝ*) | 
| 184 | 22 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈ ℝ) | 
| 185 | 25 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘𝐼) < (𝑄‘(𝐼 + 1))) | 
| 186 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝑄‘(𝐼 + 1)) ∈ dom 𝐹 ∧ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 = (𝑄‘(𝐼 + 1))) | 
| 187 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ (((𝑄‘(𝐼 + 1)) ∈ dom 𝐹 ∧ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) | 
| 188 | 186, 187 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ (((𝑄‘(𝐼 + 1)) ∈ dom 𝐹 ∧ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹) | 
| 189 | 188 | adantll 714 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) ∧ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹) | 
| 190 | 189 | adantlr 715 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹) | 
| 191 | 95 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹) | 
| 192 | 65 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘𝐼) ∈
ℝ*) | 
| 193 | 23 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) | 
| 194 | 65 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) ∈
ℝ*) | 
| 195 | 22 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄‘(𝐼 + 1)) ∈ ℝ) | 
| 196 |  | iocssre 13467 | . . . . . . . . . . . . . . . 16
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) → ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ ℝ) | 
| 197 | 194, 195,
196 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ ℝ) | 
| 198 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) | 
| 199 | 197, 198 | sseldd 3984 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ∈ ℝ) | 
| 200 | 199 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ ℝ) | 
| 201 | 23 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) | 
| 202 |  | iocgtlb 45515 | . . . . . . . . . . . . . . 15
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) < 𝑥) | 
| 203 | 194, 201,
198, 202 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) < 𝑥) | 
| 204 | 203 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘𝐼) < 𝑥) | 
| 205 | 22 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ) | 
| 206 |  | iocleub 45516 | . . . . . . . . . . . . . . . 16
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ≤ (𝑄‘(𝐼 + 1))) | 
| 207 | 194, 201,
198, 206 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ≤ (𝑄‘(𝐼 + 1))) | 
| 208 | 207 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ≤ (𝑄‘(𝐼 + 1))) | 
| 209 |  | neqne 2948 | . . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 = (𝑄‘(𝐼 + 1)) → 𝑥 ≠ (𝑄‘(𝐼 + 1))) | 
| 210 | 209 | necomd 2996 | . . . . . . . . . . . . . . 15
⊢ (¬
𝑥 = (𝑄‘(𝐼 + 1)) → (𝑄‘(𝐼 + 1)) ≠ 𝑥) | 
| 211 | 210 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ≠ 𝑥) | 
| 212 | 200, 205,
208, 211 | leneltd 11415 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 < (𝑄‘(𝐼 + 1))) | 
| 213 | 192, 193,
200, 204, 212 | eliood 45511 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) | 
| 214 | 191, 213 | sseldd 3984 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹) | 
| 215 | 214 | adantllr 719 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹) | 
| 216 | 190, 215 | pm2.61dan 813 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ∈ dom 𝐹) | 
| 217 | 216 | ralrimiva 3146 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ∀𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹) | 
| 218 |  | dfss3 3972 | . . . . . . . 8
⊢ (((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 ↔ ∀𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹) | 
| 219 | 217, 218 | sylibr 234 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ dom 𝐹) | 
| 220 | 123 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → 𝐹 ∈ (dom 𝐹–cn→ℂ)) | 
| 221 |  | rescncf 24923 | . . . . . . 7
⊢ (((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 → (𝐹 ∈ (dom 𝐹–cn→ℂ) → (𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∈ (((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))–cn→ℂ))) | 
| 222 | 219, 220,
221 | sylc 65 | . . . . . 6
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∈ (((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))–cn→ℂ)) | 
| 223 | 183, 184,
185, 222 | ioccncflimc 45900 | . . . . 5
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) ∈ (((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1)))) | 
| 224 | 22 | leidd 11829 | . . . . . . . . . 10
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ≤ (𝑄‘(𝐼 + 1))) | 
| 225 | 65, 23, 23, 25, 224 | eliocd 45520 | . . . . . . . . 9
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) | 
| 226 |  | fvres 6925 | . . . . . . . . 9
⊢ ((𝑄‘(𝐼 + 1)) ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) → ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) = (𝐹‘(𝑄‘(𝐼 + 1)))) | 
| 227 | 225, 226 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) = (𝐹‘(𝑄‘(𝐼 + 1)))) | 
| 228 | 227 | eqcomd 2743 | . . . . . . 7
⊢ (𝜑 → (𝐹‘(𝑄‘(𝐼 + 1))) = ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1)))) | 
| 229 |  | ioossioc 45505 | . . . . . . . . . . 11
⊢ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) | 
| 230 |  | resabs1 6024 | . . . . . . . . . . 11
⊢ (((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) → ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) | 
| 231 | 229, 230 | ax-mp 5 | . . . . . . . . . 10
⊢ ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) | 
| 232 | 231 | eqcomi 2746 | . . . . . . . . 9
⊢ (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) | 
| 233 | 232 | oveq1i 7441 | . . . . . . . 8
⊢ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) = (((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) | 
| 234 | 233 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) = (((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1)))) | 
| 235 | 228, 234 | eleq12d 2835 | . . . . . 6
⊢ (𝜑 → ((𝐹‘(𝑄‘(𝐼 + 1))) ∈ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ↔ ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) ∈ (((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))))) | 
| 236 | 235 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹‘(𝑄‘(𝐼 + 1))) ∈ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ↔ ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) ∈ (((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))))) | 
| 237 | 223, 236 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝐹‘(𝑄‘(𝐼 + 1))) ∈ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1)))) | 
| 238 | 237 | ne0d 4342 | . . 3
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) | 
| 239 |  | mnfxr 11318 | . . . . . . . . 9
⊢ -∞
∈ ℝ* | 
| 240 | 239 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → -∞ ∈
ℝ*) | 
| 241 | 17 | mnfltd 13166 | . . . . . . . . . 10
⊢ (𝜑 → -∞ < (𝑄‘𝐼)) | 
| 242 | 240, 65, 241 | xrltled 13192 | . . . . . . . . 9
⊢ (𝜑 → -∞ ≤ (𝑄‘𝐼)) | 
| 243 |  | iooss1 13422 | . . . . . . . . 9
⊢
((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑄‘𝐼)) → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (-∞(,)(𝑄‘(𝐼 + 1)))) | 
| 244 | 239, 242,
243 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (-∞(,)(𝑄‘(𝐼 + 1)))) | 
| 245 | 244 | resabs1d 6026 | . . . . . . 7
⊢ (𝜑 → ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) | 
| 246 | 245 | eqcomd 2743 | . . . . . 6
⊢ (𝜑 → (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) | 
| 247 | 246 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) | 
| 248 | 247 | oveq1d 7446 | . . . 4
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) = (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1)))) | 
| 249 |  | limcresi 25920 | . . . . 5
⊢ ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ⊆ (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) | 
| 250 | 22 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈ ℝ) | 
| 251 |  | simpl 482 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → 𝜑) | 
| 252 | 155 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → -π ∈
ℝ*) | 
| 253 | 157 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → π ∈
ℝ*) | 
| 254 | 23 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) | 
| 255 | 4, 17, 22, 160, 25 | lelttrd 11419 | . . . . . . . . . 10
⊢ (𝜑 → -π < (𝑄‘(𝐼 + 1))) | 
| 256 | 255 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → -π < (𝑄‘(𝐼 + 1))) | 
| 257 | 161 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ≤ π) | 
| 258 | 252, 253,
254, 256, 257 | eliocd 45520 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈
(-π(,]π)) | 
| 259 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) | 
| 260 | 258, 259 | eldifd 3962 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom
𝐹)) | 
| 261 | 251, 260 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom
𝐹))) | 
| 262 |  | eleq1 2829 | . . . . . . . . 9
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → (𝑥 ∈ ((-π(,]π) ∖ dom 𝐹) ↔ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom
𝐹))) | 
| 263 | 262 | anbi2d 630 | . . . . . . . 8
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐹)) ↔ (𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom
𝐹)))) | 
| 264 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → (-∞(,)𝑥) = (-∞(,)(𝑄‘(𝐼 + 1)))) | 
| 265 | 264 | reseq2d 5997 | . . . . . . . . . 10
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → (𝐹 ↾ (-∞(,)𝑥)) = (𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1))))) | 
| 266 |  | id 22 | . . . . . . . . . 10
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → 𝑥 = (𝑄‘(𝐼 + 1))) | 
| 267 | 265, 266 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → ((𝐹 ↾ (-∞(,)𝑥)) limℂ 𝑥) = ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1)))) | 
| 268 | 267 | neeq1d 3000 | . . . . . . . 8
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → (((𝐹 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅ ↔ ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅)) | 
| 269 | 263, 268 | imbi12d 344 | . . . . . . 7
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → (((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐹)) → ((𝐹 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) ↔ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom
𝐹)) → ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅))) | 
| 270 |  | fourierdlem46.llim | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐹)) → ((𝐹 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) | 
| 271 | 269, 270 | vtoclg 3554 | . . . . . 6
⊢ ((𝑄‘(𝐼 + 1)) ∈ ℝ → ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom
𝐹)) → ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅)) | 
| 272 | 250, 261,
271 | sylc 65 | . . . . 5
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) | 
| 273 |  | ssn0 4404 | . . . . 5
⊢ ((((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ⊆ (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ∧ ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) → (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) | 
| 274 | 249, 272,
273 | sylancr 587 | . . . 4
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) | 
| 275 | 248, 274 | eqnetrd 3008 | . . 3
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) | 
| 276 | 238, 275 | pm2.61dan 813 | . 2
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) | 
| 277 | 182, 276 | jca 511 | 1
⊢ (𝜑 → (((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅ ∧ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅)) |