Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem46 Structured version   Visualization version   GIF version

Theorem fourierdlem46 40872
 Description: The function 𝐹 has a limit at the bounds of every interval induced by the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem46.cn (𝜑𝐹 ∈ (dom 𝐹cn→ℂ))
fourierdlem46.rlim ((𝜑𝑥 ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ (𝑥(,)+∞)) lim 𝑥) ≠ ∅)
fourierdlem46.llim ((𝜑𝑥 ∈ ((-π(,]π) ∖ dom 𝐹)) → ((𝐹 ↾ (-∞(,)𝑥)) lim 𝑥) ≠ ∅)
fourierdlem46.qiso (𝜑𝑄 Isom < , < ((0...𝑀), 𝐻))
fourierdlem46.qf (𝜑𝑄:(0...𝑀)⟶𝐻)
fourierdlem46.i (𝜑𝐼 ∈ (0..^𝑀))
fourierdlem46.10 (𝜑 → (𝑄𝐼) < (𝑄‘(𝐼 + 1)))
fourierdlem46.qiss (𝜑 → ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (-π(,)π))
fourierdlem46.c (𝜑𝐶 ∈ ℝ)
fourierdlem46.h 𝐻 = ({-π, π, 𝐶} ∪ ((-π[,]π) ∖ dom 𝐹))
fourierdlem46.ranq (𝜑 → ran 𝑄 = 𝐻)
Assertion
Ref Expression
fourierdlem46 (𝜑 → (((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) ≠ ∅ ∧ ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅))
Distinct variable groups:   𝑥,𝐹   𝑥,𝐼   𝑥,𝑄   𝜑,𝑥
Allowed substitution hints:   𝐶(𝑥)   𝐻(𝑥)   𝑀(𝑥)

Proof of Theorem fourierdlem46
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem46.h . . . . . . . . 9 𝐻 = ({-π, π, 𝐶} ∪ ((-π[,]π) ∖ dom 𝐹))
2 pire 24409 . . . . . . . . . . . . 13 π ∈ ℝ
32a1i 11 . . . . . . . . . . . 12 (𝜑 → π ∈ ℝ)
43renegcld 10649 . . . . . . . . . . 11 (𝜑 → -π ∈ ℝ)
5 fourierdlem46.c . . . . . . . . . . 11 (𝜑𝐶 ∈ ℝ)
6 tpssi 4514 . . . . . . . . . . 11 ((-π ∈ ℝ ∧ π ∈ ℝ ∧ 𝐶 ∈ ℝ) → {-π, π, 𝐶} ⊆ ℝ)
74, 3, 5, 6syl3anc 1477 . . . . . . . . . 10 (𝜑 → {-π, π, 𝐶} ⊆ ℝ)
84, 3iccssred 40230 . . . . . . . . . . 11 (𝜑 → (-π[,]π) ⊆ ℝ)
98ssdifssd 3891 . . . . . . . . . 10 (𝜑 → ((-π[,]π) ∖ dom 𝐹) ⊆ ℝ)
107, 9unssd 3932 . . . . . . . . 9 (𝜑 → ({-π, π, 𝐶} ∪ ((-π[,]π) ∖ dom 𝐹)) ⊆ ℝ)
111, 10syl5eqss 3790 . . . . . . . 8 (𝜑𝐻 ⊆ ℝ)
12 fourierdlem46.qf . . . . . . . . 9 (𝜑𝑄:(0...𝑀)⟶𝐻)
13 fourierdlem46.i . . . . . . . . . 10 (𝜑𝐼 ∈ (0..^𝑀))
14 elfzofz 12679 . . . . . . . . . 10 (𝐼 ∈ (0..^𝑀) → 𝐼 ∈ (0...𝑀))
1513, 14syl 17 . . . . . . . . 9 (𝜑𝐼 ∈ (0...𝑀))
1612, 15ffvelrnd 6523 . . . . . . . 8 (𝜑 → (𝑄𝐼) ∈ 𝐻)
1711, 16sseldd 3745 . . . . . . 7 (𝜑 → (𝑄𝐼) ∈ ℝ)
1817adantr 472 . . . . . 6 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → (𝑄𝐼) ∈ ℝ)
19 fzofzp1 12759 . . . . . . . . . . 11 (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
2013, 19syl 17 . . . . . . . . . 10 (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
2112, 20ffvelrnd 6523 . . . . . . . . 9 (𝜑 → (𝑄‘(𝐼 + 1)) ∈ 𝐻)
2211, 21sseldd 3745 . . . . . . . 8 (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
2322rexrd 10281 . . . . . . 7 (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ*)
2423adantr 472 . . . . . 6 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈ ℝ*)
25 fourierdlem46.10 . . . . . . 7 (𝜑 → (𝑄𝐼) < (𝑄‘(𝐼 + 1)))
2625adantr 472 . . . . . 6 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → (𝑄𝐼) < (𝑄‘(𝐼 + 1)))
27 simpr 479 . . . . . . . . . . . . 13 (((𝑄𝐼) ∈ dom 𝐹𝑥 = (𝑄𝐼)) → 𝑥 = (𝑄𝐼))
28 simpl 474 . . . . . . . . . . . . 13 (((𝑄𝐼) ∈ dom 𝐹𝑥 = (𝑄𝐼)) → (𝑄𝐼) ∈ dom 𝐹)
2927, 28eqeltrd 2839 . . . . . . . . . . . 12 (((𝑄𝐼) ∈ dom 𝐹𝑥 = (𝑄𝐼)) → 𝑥 ∈ dom 𝐹)
3029adantll 752 . . . . . . . . . . 11 (((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) ∧ 𝑥 = (𝑄𝐼)) → 𝑥 ∈ dom 𝐹)
3130adantlr 753 . . . . . . . . . 10 ((((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 = (𝑄𝐼)) → 𝑥 ∈ dom 𝐹)
32 ssun2 3920 . . . . . . . . . . . . . . . . . . 19 ((-π[,]π) ∖ dom 𝐹) ⊆ ({-π, π, 𝐶} ∪ ((-π[,]π) ∖ dom 𝐹))
3332, 1sseqtr4i 3779 . . . . . . . . . . . . . . . . . 18 ((-π[,]π) ∖ dom 𝐹) ⊆ 𝐻
34 fourierdlem46.qiss . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (-π(,)π))
35 ioossicc 12452 . . . . . . . . . . . . . . . . . . . . . 22 (-π(,)π) ⊆ (-π[,]π)
3634, 35syl6ss 3756 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (-π[,]π))
3736sselda 3744 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ (-π[,]π))
3837adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ (-π[,]π))
39 simpr 479 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → ¬ 𝑥 ∈ dom 𝐹)
4038, 39eldifd 3726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ ((-π[,]π) ∖ dom 𝐹))
4133, 40sseldi 3742 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑥𝐻)
42 fourierdlem46.ranq . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran 𝑄 = 𝐻)
4342eqcomd 2766 . . . . . . . . . . . . . . . . . 18 (𝜑𝐻 = ran 𝑄)
4443ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝐻 = ran 𝑄)
4541, 44eleqtrd 2841 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ ran 𝑄)
46 simpr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ran 𝑄) → 𝑥 ∈ ran 𝑄)
47 ffn 6206 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑄:(0...𝑀)⟶𝐻𝑄 Fn (0...𝑀))
4812, 47syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑄 Fn (0...𝑀))
4948adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
50 fvelrnb 6405 . . . . . . . . . . . . . . . . . . . . 21 (𝑄 Fn (0...𝑀) → (𝑥 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = 𝑥))
5149, 50syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ran 𝑄) → (𝑥 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = 𝑥))
5246, 51mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = 𝑥)
5352adantlr 753 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = 𝑥)
54 elfzelz 12535 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
5554ad2antlr 765 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = 𝑥) → 𝑗 ∈ ℤ)
56 simplll 815 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = 𝑥) → 𝜑)
57 simplr 809 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = 𝑥) → 𝑗 ∈ (0...𝑀))
58 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ (𝑄𝑗) = 𝑥) → (𝑄𝑗) = 𝑥)
59 simplr 809 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ (𝑄𝑗) = 𝑥) → 𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))))
6058, 59eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ (𝑄𝑗) = 𝑥) → (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))))
6160adantlr 753 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = 𝑥) → (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))))
62 elfzoelz 12664 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐼 ∈ (0..^𝑀) → 𝐼 ∈ ℤ)
6313, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐼 ∈ ℤ)
6463ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝐼 ∈ ℤ)
6517rexrd 10281 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑄𝐼) ∈ ℝ*)
6665ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄𝐼) ∈ ℝ*)
6723ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘(𝐼 + 1)) ∈ ℝ*)
68 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))))
69 ioogtlb 40220 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑄𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄𝐼) < (𝑄𝑗))
7066, 67, 68, 69syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄𝐼) < (𝑄𝑗))
71 fourierdlem46.qiso . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑄 Isom < , < ((0...𝑀), 𝐻))
7271ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
7315ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝐼 ∈ (0...𝑀))
74 simplr 809 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑗 ∈ (0...𝑀))
75 isorel 6739 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝐼 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑀))) → (𝐼 < 𝑗 ↔ (𝑄𝐼) < (𝑄𝑗)))
7672, 73, 74, 75syl12anc 1475 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝐼 < 𝑗 ↔ (𝑄𝐼) < (𝑄𝑗)))
7770, 76mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝐼 < 𝑗)
78 iooltub 40238 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑄𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄𝑗) < (𝑄‘(𝐼 + 1)))
7966, 67, 68, 78syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄𝑗) < (𝑄‘(𝐼 + 1)))
8020ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝐼 + 1) ∈ (0...𝑀))
81 isorel 6739 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑗 ∈ (0...𝑀) ∧ (𝐼 + 1) ∈ (0...𝑀))) → (𝑗 < (𝐼 + 1) ↔ (𝑄𝑗) < (𝑄‘(𝐼 + 1))))
8272, 74, 80, 81syl12anc 1475 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑗 < (𝐼 + 1) ↔ (𝑄𝑗) < (𝑄‘(𝐼 + 1))))
8379, 82mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑗 < (𝐼 + 1))
84 btwnnz 11645 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐼 ∈ ℤ ∧ 𝐼 < 𝑗𝑗 < (𝐼 + 1)) → ¬ 𝑗 ∈ ℤ)
8564, 77, 83, 84syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → ¬ 𝑗 ∈ ℤ)
8656, 57, 61, 85syl21anc 1476 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = 𝑥) → ¬ 𝑗 ∈ ℤ)
8786adantllr 757 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = 𝑥) → ¬ 𝑗 ∈ ℤ)
8855, 87pm2.65da 601 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) → ¬ (𝑄𝑗) = 𝑥)
8988nrexdv 3139 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) → ¬ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = 𝑥)
9053, 89pm2.65da 601 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → ¬ 𝑥 ∈ ran 𝑄)
9190adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → ¬ 𝑥 ∈ ran 𝑄)
9245, 91condan 870 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ dom 𝐹)
9392ralrimiva 3104 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹)
94 dfss3 3733 . . . . . . . . . . . . . 14 (((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 ↔ ∀𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹)
9593, 94sylibr 224 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹)
9695ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄𝐼)) → ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹)
9765ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄𝐼)) → (𝑄𝐼) ∈ ℝ*)
9823ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄𝐼)) → (𝑄‘(𝐼 + 1)) ∈ ℝ*)
99 icossre 12447 . . . . . . . . . . . . . . . 16 (((𝑄𝐼) ∈ ℝ ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ*) → ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ ℝ)
10017, 23, 99syl2anc 696 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ ℝ)
101100sselda 3744 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ ℝ)
102101adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄𝐼)) → 𝑥 ∈ ℝ)
10317ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄𝐼)) → (𝑄𝐼) ∈ ℝ)
10465adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) → (𝑄𝐼) ∈ ℝ*)
10523adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) → (𝑄‘(𝐼 + 1)) ∈ ℝ*)
106 simpr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))))
107 icogelb 12418 . . . . . . . . . . . . . . . 16 (((𝑄𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ*𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) → (𝑄𝐼) ≤ 𝑥)
108104, 105, 106, 107syl3anc 1477 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) → (𝑄𝐼) ≤ 𝑥)
109108adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄𝐼)) → (𝑄𝐼) ≤ 𝑥)
110 neqne 2940 . . . . . . . . . . . . . . 15 𝑥 = (𝑄𝐼) → 𝑥 ≠ (𝑄𝐼))
111110adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄𝐼)) → 𝑥 ≠ (𝑄𝐼))
112103, 102, 109, 111leneltd 10383 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄𝐼)) → (𝑄𝐼) < 𝑥)
113 icoltub 40235 . . . . . . . . . . . . . . 15 (((𝑄𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ*𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 < (𝑄‘(𝐼 + 1)))
114104, 105, 106, 113syl3anc 1477 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 < (𝑄‘(𝐼 + 1)))
115114adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄𝐼)) → 𝑥 < (𝑄‘(𝐼 + 1)))
11697, 98, 102, 112, 115eliood 40223 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄𝐼)) → 𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))))
11796, 116sseldd 3745 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄𝐼)) → 𝑥 ∈ dom 𝐹)
118117adantllr 757 . . . . . . . . . 10 ((((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄𝐼)) → 𝑥 ∈ dom 𝐹)
11931, 118pm2.61dan 867 . . . . . . . . 9 (((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ dom 𝐹)
120119ralrimiva 3104 . . . . . . . 8 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → ∀𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹)
121 dfss3 3733 . . . . . . . 8 (((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 ↔ ∀𝑥 ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹)
122120, 121sylibr 224 . . . . . . 7 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹)
123 fourierdlem46.cn . . . . . . . 8 (𝜑𝐹 ∈ (dom 𝐹cn→ℂ))
124123adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → 𝐹 ∈ (dom 𝐹cn→ℂ))
125 rescncf 22901 . . . . . . 7 (((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 → (𝐹 ∈ (dom 𝐹cn→ℂ) → (𝐹 ↾ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∈ (((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))–cn→ℂ)))
126122, 124, 125sylc 65 . . . . . 6 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → (𝐹 ↾ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ∈ (((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))–cn→ℂ))
12718, 24, 26, 126icocncflimc 40605 . . . . 5 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄𝐼)) ∈ (((𝐹 ↾ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)))
12817leidd 10786 . . . . . . . . 9 (𝜑 → (𝑄𝐼) ≤ (𝑄𝐼))
12965, 23, 65, 128, 25elicod 12417 . . . . . . . 8 (𝜑 → (𝑄𝐼) ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))))
130 fvres 6368 . . . . . . . 8 ((𝑄𝐼) ∈ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))) → ((𝐹 ↾ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄𝐼)) = (𝐹‘(𝑄𝐼)))
131129, 130syl 17 . . . . . . 7 (𝜑 → ((𝐹 ↾ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄𝐼)) = (𝐹‘(𝑄𝐼)))
132131eqcomd 2766 . . . . . 6 (𝜑 → (𝐹‘(𝑄𝐼)) = ((𝐹 ↾ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄𝐼)))
133132adantr 472 . . . . 5 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → (𝐹‘(𝑄𝐼)) = ((𝐹 ↾ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄𝐼)))
134 ioossico 12455 . . . . . . . . 9 ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))
135134a1i 11 . . . . . . . 8 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1))))
136135resabs1d 5586 . . . . . . 7 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))))
137136eqcomd 2766 . . . . . 6 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → (𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) = ((𝐹 ↾ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))))
138137oveq1d 6828 . . . . 5 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) = (((𝐹 ↾ ((𝑄𝐼)[,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)))
139127, 133, 1383eltr4d 2854 . . . 4 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → (𝐹‘(𝑄𝐼)) ∈ ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)))
140 ne0i 4064 . . . 4 ((𝐹‘(𝑄𝐼)) ∈ ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) ≠ ∅)
141139, 140syl 17 . . 3 ((𝜑 ∧ (𝑄𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) ≠ ∅)
142 pnfxr 10284 . . . . . . . . 9 +∞ ∈ ℝ*
143142a1i 11 . . . . . . . . . 10 (𝜑 → +∞ ∈ ℝ*)
14422ltpnfd 12148 . . . . . . . . . 10 (𝜑 → (𝑄‘(𝐼 + 1)) < +∞)
14523, 143, 144xrltled 39985 . . . . . . . . 9 (𝜑 → (𝑄‘(𝐼 + 1)) ≤ +∞)
146 iooss2 12404 . . . . . . . . 9 ((+∞ ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ≤ +∞) → ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄𝐼)(,)+∞))
147142, 145, 146sylancr 698 . . . . . . . 8 (𝜑 → ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄𝐼)(,)+∞))
148147resabs1d 5586 . . . . . . 7 (𝜑 → ((𝐹 ↾ ((𝑄𝐼)(,)+∞)) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))))
149148oveq1d 6828 . . . . . 6 (𝜑 → (((𝐹 ↾ ((𝑄𝐼)(,)+∞)) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) = ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)))
150149eqcomd 2766 . . . . 5 (𝜑 → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) = (((𝐹 ↾ ((𝑄𝐼)(,)+∞)) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)))
151150adantr 472 . . . 4 ((𝜑 ∧ ¬ (𝑄𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) = (((𝐹 ↾ ((𝑄𝐼)(,)+∞)) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)))
152 limcresi 23848 . . . . 5 ((𝐹 ↾ ((𝑄𝐼)(,)+∞)) lim (𝑄𝐼)) ⊆ (((𝐹 ↾ ((𝑄𝐼)(,)+∞)) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼))
15317adantr 472 . . . . . 6 ((𝜑 ∧ ¬ (𝑄𝐼) ∈ dom 𝐹) → (𝑄𝐼) ∈ ℝ)
154 simpl 474 . . . . . . 7 ((𝜑 ∧ ¬ (𝑄𝐼) ∈ dom 𝐹) → 𝜑)
1552renegcli 10534 . . . . . . . . . . . 12 -π ∈ ℝ
156155rexri 10289 . . . . . . . . . . 11 -π ∈ ℝ*
157156a1i 11 . . . . . . . . . 10 (𝜑 → -π ∈ ℝ*)
1582rexri 10289 . . . . . . . . . . 11 π ∈ ℝ*
159158a1i 11 . . . . . . . . . 10 (𝜑 → π ∈ ℝ*)
1604, 3, 17, 22, 25, 34fourierdlem10 40837 . . . . . . . . . . 11 (𝜑 → (-π ≤ (𝑄𝐼) ∧ (𝑄‘(𝐼 + 1)) ≤ π))
161160simpld 477 . . . . . . . . . 10 (𝜑 → -π ≤ (𝑄𝐼))
162160simprd 482 . . . . . . . . . . 11 (𝜑 → (𝑄‘(𝐼 + 1)) ≤ π)
16317, 22, 3, 25, 162ltletrd 10389 . . . . . . . . . 10 (𝜑 → (𝑄𝐼) < π)
164157, 159, 65, 161, 163elicod 12417 . . . . . . . . 9 (𝜑 → (𝑄𝐼) ∈ (-π[,)π))
165164adantr 472 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑄𝐼) ∈ dom 𝐹) → (𝑄𝐼) ∈ (-π[,)π))
166 simpr 479 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑄𝐼) ∈ dom 𝐹) → ¬ (𝑄𝐼) ∈ dom 𝐹)
167165, 166eldifd 3726 . . . . . . 7 ((𝜑 ∧ ¬ (𝑄𝐼) ∈ dom 𝐹) → (𝑄𝐼) ∈ ((-π[,)π) ∖ dom 𝐹))
168154, 167jca 555 . . . . . 6 ((𝜑 ∧ ¬ (𝑄𝐼) ∈ dom 𝐹) → (𝜑 ∧ (𝑄𝐼) ∈ ((-π[,)π) ∖ dom 𝐹)))
169 eleq1 2827 . . . . . . . . 9 (𝑥 = (𝑄𝐼) → (𝑥 ∈ ((-π[,)π) ∖ dom 𝐹) ↔ (𝑄𝐼) ∈ ((-π[,)π) ∖ dom 𝐹)))
170169anbi2d 742 . . . . . . . 8 (𝑥 = (𝑄𝐼) → ((𝜑𝑥 ∈ ((-π[,)π) ∖ dom 𝐹)) ↔ (𝜑 ∧ (𝑄𝐼) ∈ ((-π[,)π) ∖ dom 𝐹))))
171 oveq1 6820 . . . . . . . . . . 11 (𝑥 = (𝑄𝐼) → (𝑥(,)+∞) = ((𝑄𝐼)(,)+∞))
172171reseq2d 5551 . . . . . . . . . 10 (𝑥 = (𝑄𝐼) → (𝐹 ↾ (𝑥(,)+∞)) = (𝐹 ↾ ((𝑄𝐼)(,)+∞)))
173 id 22 . . . . . . . . . 10 (𝑥 = (𝑄𝐼) → 𝑥 = (𝑄𝐼))
174172, 173oveq12d 6831 . . . . . . . . 9 (𝑥 = (𝑄𝐼) → ((𝐹 ↾ (𝑥(,)+∞)) lim 𝑥) = ((𝐹 ↾ ((𝑄𝐼)(,)+∞)) lim (𝑄𝐼)))
175174neeq1d 2991 . . . . . . . 8 (𝑥 = (𝑄𝐼) → (((𝐹 ↾ (𝑥(,)+∞)) lim 𝑥) ≠ ∅ ↔ ((𝐹 ↾ ((𝑄𝐼)(,)+∞)) lim (𝑄𝐼)) ≠ ∅))
176170, 175imbi12d 333 . . . . . . 7 (𝑥 = (𝑄𝐼) → (((𝜑𝑥 ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ (𝑥(,)+∞)) lim 𝑥) ≠ ∅) ↔ ((𝜑 ∧ (𝑄𝐼) ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ ((𝑄𝐼)(,)+∞)) lim (𝑄𝐼)) ≠ ∅)))
177 fourierdlem46.rlim . . . . . . 7 ((𝜑𝑥 ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ (𝑥(,)+∞)) lim 𝑥) ≠ ∅)
178176, 177vtoclg 3406 . . . . . 6 ((𝑄𝐼) ∈ ℝ → ((𝜑 ∧ (𝑄𝐼) ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ ((𝑄𝐼)(,)+∞)) lim (𝑄𝐼)) ≠ ∅))
179153, 168, 178sylc 65 . . . . 5 ((𝜑 ∧ ¬ (𝑄𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄𝐼)(,)+∞)) lim (𝑄𝐼)) ≠ ∅)
180 ssn0 4119 . . . . 5 ((((𝐹 ↾ ((𝑄𝐼)(,)+∞)) lim (𝑄𝐼)) ⊆ (((𝐹 ↾ ((𝑄𝐼)(,)+∞)) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) ∧ ((𝐹 ↾ ((𝑄𝐼)(,)+∞)) lim (𝑄𝐼)) ≠ ∅) → (((𝐹 ↾ ((𝑄𝐼)(,)+∞)) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) ≠ ∅)
181152, 179, 180sylancr 698 . . . 4 ((𝜑 ∧ ¬ (𝑄𝐼) ∈ dom 𝐹) → (((𝐹 ↾ ((𝑄𝐼)(,)+∞)) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) ≠ ∅)
182151, 181eqnetrd 2999 . . 3 ((𝜑 ∧ ¬ (𝑄𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) ≠ ∅)
183141, 182pm2.61dan 867 . 2 (𝜑 → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) ≠ ∅)
18465adantr 472 . . . . . 6 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄𝐼) ∈ ℝ*)
18522adantr 472 . . . . . 6 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
18625adantr 472 . . . . . 6 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄𝐼) < (𝑄‘(𝐼 + 1)))
187 simpr 479 . . . . . . . . . . . . 13 (((𝑄‘(𝐼 + 1)) ∈ dom 𝐹𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 = (𝑄‘(𝐼 + 1)))
188 simpl 474 . . . . . . . . . . . . 13 (((𝑄‘(𝐼 + 1)) ∈ dom 𝐹𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ dom 𝐹)
189187, 188eqeltrd 2839 . . . . . . . . . . . 12 (((𝑄‘(𝐼 + 1)) ∈ dom 𝐹𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹)
190189adantll 752 . . . . . . . . . . 11 (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) ∧ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹)
191190adantlr 753 . . . . . . . . . 10 ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹)
19295ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹)
19365ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄𝐼) ∈ ℝ*)
19423ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ*)
19565adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄𝐼) ∈ ℝ*)
19622adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
197 iocssre 12446 . . . . . . . . . . . . . . . 16 (((𝑄𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) → ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ ℝ)
198195, 196, 197syl2anc 696 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) → ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ ℝ)
199 simpr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))))
200198, 199sseldd 3745 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ∈ ℝ)
201200adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ ℝ)
20223adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄‘(𝐼 + 1)) ∈ ℝ*)
203 iocgtlb 40227 . . . . . . . . . . . . . . 15 (((𝑄𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ*𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄𝐼) < 𝑥)
204195, 202, 199, 203syl3anc 1477 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄𝐼) < 𝑥)
205204adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄𝐼) < 𝑥)
20622ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
207 iocleub 40228 . . . . . . . . . . . . . . . 16 (((𝑄𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ*𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ≤ (𝑄‘(𝐼 + 1)))
208195, 202, 199, 207syl3anc 1477 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ≤ (𝑄‘(𝐼 + 1)))
209208adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ≤ (𝑄‘(𝐼 + 1)))
210 neqne 2940 . . . . . . . . . . . . . . . 16 𝑥 = (𝑄‘(𝐼 + 1)) → 𝑥 ≠ (𝑄‘(𝐼 + 1)))
211210necomd 2987 . . . . . . . . . . . . . . 15 𝑥 = (𝑄‘(𝐼 + 1)) → (𝑄‘(𝐼 + 1)) ≠ 𝑥)
212211adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ≠ 𝑥)
213201, 206, 209, 212leneltd 10383 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 < (𝑄‘(𝐼 + 1)))
214193, 194, 201, 205, 213eliood 40223 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))))
215192, 214sseldd 3745 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹)
216215adantllr 757 . . . . . . . . . 10 ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹)
217191, 216pm2.61dan 867 . . . . . . . . 9 (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ∈ dom 𝐹)
218217ralrimiva 3104 . . . . . . . 8 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ∀𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹)
219 dfss3 3733 . . . . . . . 8 (((𝑄𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 ↔ ∀𝑥 ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹)
220218, 219sylibr 224 . . . . . . 7 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ dom 𝐹)
221123adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → 𝐹 ∈ (dom 𝐹cn→ℂ))
222 rescncf 22901 . . . . . . 7 (((𝑄𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 → (𝐹 ∈ (dom 𝐹cn→ℂ) → (𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∈ (((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))–cn→ℂ)))
223220, 221, 222sylc 65 . . . . . 6 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ∈ (((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))–cn→ℂ))
224184, 185, 186, 223ioccncflimc 40601 . . . . 5 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) ∈ (((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))))
22522leidd 10786 . . . . . . . . . 10 (𝜑 → (𝑄‘(𝐼 + 1)) ≤ (𝑄‘(𝐼 + 1)))
22665, 23, 23, 25, 225eliocd 40233 . . . . . . . . 9 (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))))
227 fvres 6368 . . . . . . . . 9 ((𝑄‘(𝐼 + 1)) ∈ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))) → ((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) = (𝐹‘(𝑄‘(𝐼 + 1))))
228226, 227syl 17 . . . . . . . 8 (𝜑 → ((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) = (𝐹‘(𝑄‘(𝐼 + 1))))
229228eqcomd 2766 . . . . . . 7 (𝜑 → (𝐹‘(𝑄‘(𝐼 + 1))) = ((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))))
230 ioossioc 40216 . . . . . . . . . . 11 ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))
231 resabs1 5585 . . . . . . . . . . 11 (((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))) → ((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))))
232230, 231ax-mp 5 . . . . . . . . . 10 ((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))))
233232eqcomi 2769 . . . . . . . . 9 (𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) = ((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))))
234233oveq1i 6823 . . . . . . . 8 ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) = (((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1)))
235234a1i 11 . . . . . . 7 (𝜑 → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) = (((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))))
236229, 235eleq12d 2833 . . . . . 6 (𝜑 → ((𝐹‘(𝑄‘(𝐼 + 1))) ∈ ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ↔ ((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) ∈ (((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1)))))
237236adantr 472 . . . . 5 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹‘(𝑄‘(𝐼 + 1))) ∈ ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ↔ ((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) ∈ (((𝐹 ↾ ((𝑄𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1)))))
238224, 237mpbird 247 . . . 4 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝐹‘(𝑄‘(𝐼 + 1))) ∈ ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))))
239 ne0i 4064 . . . 4 ((𝐹‘(𝑄‘(𝐼 + 1))) ∈ ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅)
240238, 239syl 17 . . 3 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅)
241 mnfxr 10288 . . . . . . . . 9 -∞ ∈ ℝ*
242241a1i 11 . . . . . . . . . 10 (𝜑 → -∞ ∈ ℝ*)
24317mnfltd 12151 . . . . . . . . . 10 (𝜑 → -∞ < (𝑄𝐼))
244242, 65, 243xrltled 39985 . . . . . . . . 9 (𝜑 → -∞ ≤ (𝑄𝐼))
245 iooss1 12403 . . . . . . . . 9 ((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑄𝐼)) → ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (-∞(,)(𝑄‘(𝐼 + 1))))
246241, 244, 245sylancr 698 . . . . . . . 8 (𝜑 → ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (-∞(,)(𝑄‘(𝐼 + 1))))
247246resabs1d 5586 . . . . . . 7 (𝜑 → ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))))
248247eqcomd 2766 . . . . . 6 (𝜑 → (𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) = ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))))
249248adantr 472 . . . . 5 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) = ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))))
250249oveq1d 6828 . . . 4 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) = (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))))
251 limcresi 23848 . . . . 5 ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ⊆ (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1)))
25222adantr 472 . . . . . 6 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
253 simpl 474 . . . . . . 7 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → 𝜑)
254156a1i 11 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → -π ∈ ℝ*)
255158a1i 11 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → π ∈ ℝ*)
25623adantr 472 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈ ℝ*)
2574, 17, 22, 161, 25lelttrd 10387 . . . . . . . . . 10 (𝜑 → -π < (𝑄‘(𝐼 + 1)))
258257adantr 472 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → -π < (𝑄‘(𝐼 + 1)))
259162adantr 472 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ≤ π)
260254, 255, 256, 258, 259eliocd 40233 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈ (-π(,]π))
261 simpr 479 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹)
262260, 261eldifd 3726 . . . . . . 7 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom 𝐹))
263253, 262jca 555 . . . . . 6 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom 𝐹)))
264 eleq1 2827 . . . . . . . . 9 (𝑥 = (𝑄‘(𝐼 + 1)) → (𝑥 ∈ ((-π(,]π) ∖ dom 𝐹) ↔ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom 𝐹)))
265264anbi2d 742 . . . . . . . 8 (𝑥 = (𝑄‘(𝐼 + 1)) → ((𝜑𝑥 ∈ ((-π(,]π) ∖ dom 𝐹)) ↔ (𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom 𝐹))))
266 oveq2 6821 . . . . . . . . . . 11 (𝑥 = (𝑄‘(𝐼 + 1)) → (-∞(,)𝑥) = (-∞(,)(𝑄‘(𝐼 + 1))))
267266reseq2d 5551 . . . . . . . . . 10 (𝑥 = (𝑄‘(𝐼 + 1)) → (𝐹 ↾ (-∞(,)𝑥)) = (𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))))
268 id 22 . . . . . . . . . 10 (𝑥 = (𝑄‘(𝐼 + 1)) → 𝑥 = (𝑄‘(𝐼 + 1)))
269267, 268oveq12d 6831 . . . . . . . . 9 (𝑥 = (𝑄‘(𝐼 + 1)) → ((𝐹 ↾ (-∞(,)𝑥)) lim 𝑥) = ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))))
270269neeq1d 2991 . . . . . . . 8 (𝑥 = (𝑄‘(𝐼 + 1)) → (((𝐹 ↾ (-∞(,)𝑥)) lim 𝑥) ≠ ∅ ↔ ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅))
271265, 270imbi12d 333 . . . . . . 7 (𝑥 = (𝑄‘(𝐼 + 1)) → (((𝜑𝑥 ∈ ((-π(,]π) ∖ dom 𝐹)) → ((𝐹 ↾ (-∞(,)𝑥)) lim 𝑥) ≠ ∅) ↔ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom 𝐹)) → ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅)))
272 fourierdlem46.llim . . . . . . 7 ((𝜑𝑥 ∈ ((-π(,]π) ∖ dom 𝐹)) → ((𝐹 ↾ (-∞(,)𝑥)) lim 𝑥) ≠ ∅)
273271, 272vtoclg 3406 . . . . . 6 ((𝑄‘(𝐼 + 1)) ∈ ℝ → ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom 𝐹)) → ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅))
274252, 263, 273sylc 65 . . . . 5 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅)
275 ssn0 4119 . . . . 5 ((((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ⊆ (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ∧ ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅) → (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅)
276251, 274, 275sylancr 698 . . . 4 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅)
277250, 276eqnetrd 2999 . . 3 ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅)
278240, 277pm2.61dan 867 . 2 (𝜑 → ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅)
279183, 278jca 555 1 (𝜑 → (((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄𝐼)) ≠ ∅ ∧ ((𝐹 ↾ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) lim (𝑄‘(𝐼 + 1))) ≠ ∅))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2139   ≠ wne 2932  ∀wral 3050  ∃wrex 3051   ∖ cdif 3712   ∪ cun 3713   ⊆ wss 3715  ∅c0 4058  {ctp 4325   class class class wbr 4804  dom cdm 5266  ran crn 5267   ↾ cres 5268   Fn wfn 6044  ⟶wf 6045  ‘cfv 6049   Isom wiso 6050  (class class class)co 6813  ℂcc 10126  ℝcr 10127  0cc0 10128  1c1 10129   + caddc 10131  +∞cpnf 10263  -∞cmnf 10264  ℝ*cxr 10265   < clt 10266   ≤ cle 10267  -cneg 10459  ℤcz 11569  (,)cioo 12368  (,]cioc 12369  [,)cico 12370  [,]cicc 12371  ...cfz 12519  ..^cfzo 12659  πcpi 14996  –cn→ccncf 22880   limℂ climc 23825 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206  ax-addf 10207  ax-mulf 10208 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-fi 8482  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-q 11982  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-ioo 12372  df-ioc 12373  df-ico 12374  df-icc 12375  df-fz 12520  df-fzo 12660  df-fl 12787  df-seq 12996  df-exp 13055  df-fac 13255  df-bc 13284  df-hash 13312  df-shft 14006  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-limsup 14401  df-clim 14418  df-rlim 14419  df-sum 14616  df-ef 14997  df-sin 14999  df-cos 15000  df-pi 15002  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-starv 16158  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-unif 16167  df-hom 16168  df-cco 16169  df-rest 16285  df-topn 16286  df-0g 16304  df-gsum 16305  df-topgen 16306  df-pt 16307  df-prds 16310  df-xrs 16364  df-qtop 16369  df-imas 16370  df-xps 16372  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17950  df-cmn 18395  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-fbas 19945  df-fg 19946  df-cnfld 19949  df-top 20901  df-topon 20918  df-topsp 20939  df-bases 20952  df-cld 21025  df-ntr 21026  df-cls 21027  df-nei 21104  df-lp 21142  df-perf 21143  df-cn 21233  df-cnp 21234  df-haus 21321  df-tx 21567  df-hmeo 21760  df-fil 21851  df-fm 21943  df-flim 21944  df-flf 21945  df-xms 22326  df-ms 22327  df-tms 22328  df-cncf 22882  df-limc 23829  df-dv 23830 This theorem is referenced by:  fourierdlem102  40928  fourierdlem114  40940
 Copyright terms: Public domain W3C validator