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

Theorem fourierdlem49 39048
Description: The given periodic function 𝐹 has a left limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem49.a (𝜑𝐴 ∈ ℝ)
fourierdlem49.b (𝜑𝐵 ∈ ℝ)
fourierdlem49.altb (𝜑𝐴 < 𝐵)
fourierdlem49.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem49.t 𝑇 = (𝐵𝐴)
fourierdlem49.m (𝜑𝑀 ∈ ℕ)
fourierdlem49.q (𝜑𝑄 ∈ (𝑃𝑀))
fourierdlem49.d (𝜑𝐷 ⊆ ℝ)
fourierdlem49.f (𝜑𝐹:𝐷⟶ℝ)
fourierdlem49.dper ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
fourierdlem49.per ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥))
fourierdlem49.cn ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
fourierdlem49.l ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
fourierdlem49.x (𝜑𝑋 ∈ ℝ)
fourierdlem49.z 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
fourierdlem49.e 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥)))
Assertion
Ref Expression
fourierdlem49 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ≠ ∅)
Distinct variable groups:   𝐴,𝑖,𝑚,𝑝   𝑥,𝐴,𝑖   𝐵,𝑖,𝑘   𝐵,𝑚,𝑝   𝑥,𝐵,𝑘   𝐷,𝑘,𝑥   𝑖,𝐸,𝑘,𝑥   𝑖,𝐹,𝑘,𝑥   𝑖,𝑀,𝑘   𝑚,𝑀,𝑝   𝑥,𝑀   𝑄,𝑖,𝑘   𝑄,𝑝   𝑥,𝑄   𝑇,𝑘,𝑥   𝑖,𝑋,𝑘,𝑥   𝑘,𝑍,𝑥   𝜑,𝑖,𝑘,𝑥
Allowed substitution hints:   𝜑(𝑚,𝑝)   𝐴(𝑘)   𝐷(𝑖,𝑚,𝑝)   𝑃(𝑥,𝑖,𝑘,𝑚,𝑝)   𝑄(𝑚)   𝑇(𝑖,𝑚,𝑝)   𝐸(𝑚,𝑝)   𝐹(𝑚,𝑝)   𝐿(𝑥,𝑖,𝑘,𝑚,𝑝)   𝑋(𝑚,𝑝)   𝑍(𝑖,𝑚,𝑝)

Proof of Theorem fourierdlem49
Dummy variables 𝑗 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem49.a . . . . . 6 (𝜑𝐴 ∈ ℝ)
2 fourierdlem49.b . . . . . 6 (𝜑𝐵 ∈ ℝ)
3 fourierdlem49.altb . . . . . 6 (𝜑𝐴 < 𝐵)
4 fourierdlem49.t . . . . . 6 𝑇 = (𝐵𝐴)
5 fourierdlem49.e . . . . . . 7 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥)))
6 ovex 6577 . . . . . . . . . 10 ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ V
7 fourierdlem49.z . . . . . . . . . . 11 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
87fvmpt2 6200 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ V) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
96, 8mpan2 703 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
109oveq2d 6565 . . . . . . . 8 (𝑥 ∈ ℝ → (𝑥 + (𝑍𝑥)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
1110mpteq2ia 4668 . . . . . . 7 (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
125, 11eqtri 2632 . . . . . 6 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
131, 2, 3, 4, 12fourierdlem4 39004 . . . . 5 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
14 fourierdlem49.x . . . . 5 (𝜑𝑋 ∈ ℝ)
1513, 14ffvelrnd 6268 . . . 4 (𝜑 → (𝐸𝑋) ∈ (𝐴(,]𝐵))
16 simpr 476 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ran 𝑄)
17 fourierdlem49.q . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (𝑃𝑀))
18 fourierdlem49.m . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℕ)
19 fourierdlem49.p . . . . . . . . . . . . . . 15 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
2019fourierdlem2 39002 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
2118, 20syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
2217, 21mpbid 221 . . . . . . . . . . . 12 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
2322simpld 474 . . . . . . . . . . 11 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
24 elmapi 7765 . . . . . . . . . . 11 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
2523, 24syl 17 . . . . . . . . . 10 (𝜑𝑄:(0...𝑀)⟶ℝ)
26 ffn 5958 . . . . . . . . . 10 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
2725, 26syl 17 . . . . . . . . 9 (𝜑𝑄 Fn (0...𝑀))
2827ad2antrr 758 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
29 fvelrnb 6153 . . . . . . . 8 (𝑄 Fn (0...𝑀) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
3028, 29syl 17 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
3116, 30mpbid 221 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
32 1zzd 11285 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ∈ ℤ)
33 elfzelz 12213 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
3433ad2antlr 759 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℤ)
35 1e0p1 11428 . . . . . . . . . . . . . . . . 17 1 = (0 + 1)
3635a1i 11 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 = (0 + 1))
3734zred 11358 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℝ)
38 elfzle1 12215 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
3938ad2antlr 759 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ 𝑗)
40 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄𝑗) = (𝐸𝑋) → (𝑄𝑗) = (𝐸𝑋))
4140eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄𝑗) = (𝐸𝑋) → (𝐸𝑋) = (𝑄𝑗))
4241ad2antlr 759 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = (𝑄𝑗))
43 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 0 → (𝑄𝑗) = (𝑄‘0))
4443adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝑄𝑗) = (𝑄‘0))
4522simprld 791 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
4645simpld 474 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑄‘0) = 𝐴)
4746ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝑄‘0) = 𝐴)
4842, 44, 473eqtrd 2648 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
4948adantllr 751 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
5049adantllr 751 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
511adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ)
521rexrd 9968 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ∈ ℝ*)
5352adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ*)
542rexrd 9968 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ∈ ℝ*)
5554adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐵 ∈ ℝ*)
56 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ (𝐴(,]𝐵))
57 iocgtlb 38571 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
5853, 55, 56, 57syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
5951, 58gtned 10051 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ≠ 𝐴)
6059neneqd 2787 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → ¬ (𝐸𝑋) = 𝐴)
6160ad3antrrr 762 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → ¬ (𝐸𝑋) = 𝐴)
6250, 61pm2.65da 598 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ¬ 𝑗 = 0)
6362neqned 2789 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ≠ 0)
6437, 39, 63ne0gt0d 10053 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 < 𝑗)
65 0zd 11266 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ∈ ℤ)
66 zltp1le 11304 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
6765, 34, 66syl2anc 691 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
6864, 67mpbid 221 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 + 1) ≤ 𝑗)
6936, 68eqbrtrd 4605 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ≤ 𝑗)
70 eluz2 11569 . . . . . . . . . . . . . . 15 (𝑗 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
7132, 34, 69, 70syl3anbrc 1239 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (ℤ‘1))
72 nnuz 11599 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
7371, 72syl6eleqr 2699 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℕ)
74 nnm1nn0 11211 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
7573, 74syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℕ0)
76 nn0uz 11598 . . . . . . . . . . . . 13 0 = (ℤ‘0)
7776a1i 11 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ℕ0 = (ℤ‘0))
7875, 77eleqtrd 2690 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (ℤ‘0))
7918nnzd 11357 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℤ)
8079ad3antrrr 762 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℤ)
81 peano2zm 11297 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
8233, 81syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℤ)
8382zred 11358 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
8433zred 11358 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
85 elfzel2 12211 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
8685zred 11358 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
8784ltm1d 10835 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
88 elfzle2 12216 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗𝑀)
8983, 84, 86, 87, 88ltletrd 10076 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
9089ad2antlr 759 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) < 𝑀)
91 elfzo2 12342 . . . . . . . . . . 11 ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
9278, 80, 90, 91syl3anbrc 1239 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
9325ad3antrrr 762 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
9434, 81syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℤ)
9565, 80, 943jca 1235 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ))
9675nn0ge0d 11231 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ (𝑗 − 1))
9783, 86, 89ltled 10064 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
9897ad2antlr 759 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ≤ 𝑀)
9995, 96, 98jca32 556 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
100 elfz2 12204 . . . . . . . . . . . . . . 15 ((𝑗 − 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
10199, 100sylibr 223 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
10293, 101ffvelrnd 6268 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
103102rexrd 9968 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
10425ffvelrnda 6267 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ)
105104rexrd 9968 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
106105adantlr 747 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
107106adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ∈ ℝ*)
108 iocssre 12124 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
10952, 2, 108syl2anc 691 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
110109sselda 3568 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ℝ)
111110rexrd 9968 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ℝ*)
112111ad2antrr 758 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
113 simplll 794 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
114 ovex 6577 . . . . . . . . . . . . . . . 16 (𝑗 − 1) ∈ V
115 eleq1 2676 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
116115anbi2d 736 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
117 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑄𝑖) = (𝑄‘(𝑗 − 1)))
118 oveq1 6556 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
119118fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
120117, 119breq12d 4596 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
121116, 120imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
12222simprrd 793 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
123122r19.21bi 2916 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
124114, 121, 123vtocl 3232 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
125113, 92, 124syl2anc 691 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
12633zcnd 11359 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
127 1cnd 9935 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
128126, 127npcand 10275 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
129128eqcomd 2616 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
130129fveq2d 6107 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
131130eqcomd 2616 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
132131ad2antlr 759 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
133125, 132breqtrd 4609 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄𝑗))
134 simpr 476 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
135133, 134breqtrd 4609 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸𝑋))
136109, 15sseldd 3569 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸𝑋) ∈ ℝ)
137136leidd 10473 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸𝑋) ≤ (𝐸𝑋))
138137ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝐸𝑋))
13941adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
140138, 139breqtrd 4609 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
141140adantllr 751 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
142103, 107, 112, 135, 141eliocd 38577 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)))
143130oveq2d 6565 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
144143ad2antlr 759 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
145142, 144eleqtrd 2690 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
146117, 119oveq12d 6567 . . . . . . . . . . . 12 (𝑖 = (𝑗 − 1) → ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
147146eleq2d 2673 . . . . . . . . . . 11 (𝑖 = (𝑗 − 1) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
148147rspcev 3282 . . . . . . . . . 10 (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
14992, 145, 148syl2anc 691 . . . . . . . . 9 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
150149ex 449 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
151150adantlr 747 . . . . . . 7 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
152151rexlimdva 3013 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
15331, 152mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
15418ad2antrr 758 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
15525ad2antrr 758 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
156 iocssicc 12132 . . . . . . . . . 10 (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
15746eqcomd 2616 . . . . . . . . . . 11 (𝜑𝐴 = (𝑄‘0))
15845simprd 478 . . . . . . . . . . . 12 (𝜑 → (𝑄𝑀) = 𝐵)
159158eqcomd 2616 . . . . . . . . . . 11 (𝜑𝐵 = (𝑄𝑀))
160157, 159oveq12d 6567 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄𝑀)))
161156, 160syl5sseq 3616 . . . . . . . . 9 (𝜑 → (𝐴(,]𝐵) ⊆ ((𝑄‘0)[,](𝑄𝑀)))
162161sselda 3568 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
163162adantr 480 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
164 simpr 476 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ¬ (𝐸𝑋) ∈ ran 𝑄)
165 fveq2 6103 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑄𝑘) = (𝑄𝑗))
166165breq1d 4593 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝑄𝑘) < (𝐸𝑋) ↔ (𝑄𝑗) < (𝐸𝑋)))
167166cbvrabv 3172 . . . . . . . 8 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}
168167supeq1i 8236 . . . . . . 7 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}, ℝ, < )
169154, 155, 163, 164, 168fourierdlem25 39025 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
170 ioossioc 38560 . . . . . . . . 9 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))
171170sseli 3564 . . . . . . . 8 ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
172171a1i 11 . . . . . . 7 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
173172reximdva 3000 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
174169, 173mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
175153, 174pm2.61dan 828 . . . 4 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
17615, 175mpdan 699 . . 3 (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
177 fourierdlem49.f . . . . . . . . . . 11 (𝜑𝐹:𝐷⟶ℝ)
178 frel 5963 . . . . . . . . . . 11 (𝐹:𝐷⟶ℝ → Rel 𝐹)
179177, 178syl 17 . . . . . . . . . 10 (𝜑 → Rel 𝐹)
180 resindm 5364 . . . . . . . . . . 11 (Rel 𝐹 → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)(𝐸𝑋))))
181180eqcomd 2616 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)))
182179, 181syl 17 . . . . . . . . 9 (𝜑 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)))
183 fdm 5964 . . . . . . . . . . . 12 (𝐹:𝐷⟶ℝ → dom 𝐹 = 𝐷)
184177, 183syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝐷)
185184ineq2d 3776 . . . . . . . . . 10 (𝜑 → ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹) = ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
186185reseq2d 5317 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
187182, 186eqtrd 2644 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
1881873ad2ant1 1075 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
189188oveq1d 6564 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) lim (𝐸𝑋)))
190 ax-resscn 9872 . . . . . . . . . . 11 ℝ ⊆ ℂ
191190a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
192177, 191fssd 5970 . . . . . . . . 9 (𝜑𝐹:𝐷⟶ℂ)
1931923ad2ant1 1075 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐹:𝐷⟶ℂ)
194 inss2 3796 . . . . . . . . 9 ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ 𝐷
195194a1i 11 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ 𝐷)
196193, 195fssresd 5984 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)):((-∞(,)(𝐸𝑋)) ∩ 𝐷)⟶ℂ)
197 mnfxr 9975 . . . . . . . . . 10 -∞ ∈ ℝ*
198197a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ∈ ℝ*)
19925adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
200 elfzofz 12354 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
201200adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
202199, 201ffvelrnd 6268 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
203202rexrd 9968 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
204202mnfltd 11834 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < (𝑄𝑖))
205198, 203, 204xrltled 38427 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑄𝑖))
206 iooss1 12081 . . . . . . . . . 10 ((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑄𝑖)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
207197, 205, 206sylancr 694 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
2082073adant3 1074 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
209 fzofzp1 12431 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
210209adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
211199, 210ffvelrnd 6268 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2122113adant3 1074 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
213212rexrd 9968 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2142023adant3 1074 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
215214rexrd 9968 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
216 simp3 1056 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
217 iocleub 38572 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
218215, 213, 216, 217syl3anc 1318 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
219 iooss2 12082 . . . . . . . . . 10 (((𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
220213, 218, 219syl2anc 691 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
221 fourierdlem49.cn . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
222 cncff 22504 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
223 fdm 5964 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
224221, 222, 2233syl 18 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
225 ssdmres 5340 . . . . . . . . . . . 12 (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
226224, 225sylibr 223 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
227184adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → dom 𝐹 = 𝐷)
228226, 227sseqtrd 3604 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
2292283adant3 1074 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
230220, 229sstrd 3578 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ 𝐷)
231208, 230ssind 3799 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
232 fourierdlem49.d . . . . . . . . . 10 (𝜑𝐷 ⊆ ℝ)
233232, 191sstrd 3578 . . . . . . . . 9 (𝜑𝐷 ⊆ ℂ)
2342333ad2ant1 1075 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 ⊆ ℂ)
235194, 234syl5ss 3579 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℂ)
236 eqid 2610 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
237 eqid 2610 . . . . . . 7 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
2381363ad2ant1 1075 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
239238rexrd 9968 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ*)
240 iocgtlb 38571 . . . . . . . . . 10 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
241215, 213, 216, 240syl3anc 1318 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
242238leidd 10473 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝐸𝑋))
243215, 239, 239, 241, 242eliocd 38577 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝐸𝑋)))
244 snunioo2 38578 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ* ∧ (𝑄𝑖) < (𝐸𝑋)) → (((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)}) = ((𝑄𝑖)(,](𝐸𝑋)))
245215, 239, 241, 244syl3anc 1318 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)}) = ((𝑄𝑖)(,](𝐸𝑋)))
246245fveq2d 6107 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))))
247236cnfldtop 22397 . . . . . . . . . . 11 (TopOpen‘ℂfld) ∈ Top
248 ovex 6577 . . . . . . . . . . . . 13 (-∞(,)(𝐸𝑋)) ∈ V
249248inex1 4727 . . . . . . . . . . . 12 ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∈ V
250 snex 4835 . . . . . . . . . . . 12 {(𝐸𝑋)} ∈ V
251249, 250unex 6854 . . . . . . . . . . 11 (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V
252 resttop 20774 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top)
253247, 251, 252mp2an 704 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top
254 retop 22375 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ Top
255254a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (topGen‘ran (,)) ∈ Top)
256251a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V)
257 iooretop 22379 . . . . . . . . . . . . 13 ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,))
258257a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,)))
259 elrestr 15912 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V ∧ ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,))) → (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
260255, 256, 258, 259syl3anc 1318 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
261 simpr 476 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸𝑋)) → 𝑥 = (𝐸𝑋))
262 pnfxr 9971 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
263262a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → +∞ ∈ ℝ*)
264238ltpnfd 11831 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < +∞)
265215, 263, 238, 241, 264eliood 38567 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,)+∞))
266 snidg 4153 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑋) ∈ ℝ → (𝐸𝑋) ∈ {(𝐸𝑋)})
267 elun2 3743 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑋) ∈ {(𝐸𝑋)} → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
268266, 267syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐸𝑋) ∈ ℝ → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
269136, 268syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
2702693ad2ant1 1075 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
271265, 270elind 3760 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
272271adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
273261, 272eqeltrd 2688 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
274273adantlr 747 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
275215adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) ∈ ℝ*)
276262a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → +∞ ∈ ℝ*)
277203adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) ∈ ℝ*)
278136adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐸𝑋) ∈ ℝ)
279278adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝐸𝑋) ∈ ℝ)
280 iocssre 12124 . . . . . . . . . . . . . . . . . . . 20 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ) → ((𝑄𝑖)(,](𝐸𝑋)) ⊆ ℝ)
281277, 279, 280syl2anc 691 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → ((𝑄𝑖)(,](𝐸𝑋)) ⊆ ℝ)
282 simpr 476 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)))
283281, 282sseldd 3569 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ℝ)
2842833adantl3 1212 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ℝ)
285279rexrd 9968 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝐸𝑋) ∈ ℝ*)
286 iocgtlb 38571 . . . . . . . . . . . . . . . . . . 19 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
287277, 285, 282, 286syl3anc 1318 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
2882873adantl3 1212 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
289284ltpnfd 11831 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 < +∞)
290275, 276, 284, 288, 289eliood 38567 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
291290adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
292197a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → -∞ ∈ ℝ*)
293285adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
294283adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ℝ)
295294mnfltd 11834 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → -∞ < 𝑥)
296136ad3antrrr 762 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ)
297 iocleub 38572 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
298277, 285, 282, 297syl3anc 1318 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
299298adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ≤ (𝐸𝑋))
300 neqne 2790 . . . . . . . . . . . . . . . . . . . . . 22 𝑥 = (𝐸𝑋) → 𝑥 ≠ (𝐸𝑋))
301300necomd 2837 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = (𝐸𝑋) → (𝐸𝑋) ≠ 𝑥)
302301adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ≠ 𝑥)
303294, 296, 299, 302leneltd 10070 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝐸𝑋))
304292, 293, 294, 295, 303eliood 38567 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
3053043adantll3 38226 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
306229ad2antrr 758 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
307275adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄𝑖) ∈ ℝ*)
308213ad2antrr 758 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
309284adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ℝ)
310288adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄𝑖) < 𝑥)
311238ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ)
312212ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
3133033adantll3 38226 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝐸𝑋))
314218ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
315309, 311, 312, 313, 314ltletrd 10076 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝑄‘(𝑖 + 1)))
316307, 308, 309, 310, 315eliood 38567 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
317306, 316sseldd 3569 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥𝐷)
318305, 317elind 3760 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
319 elun1 3742 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
320318, 319syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
321291, 320elind 3760 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
322274, 321pm2.61dan 828 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
323215adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) ∈ ℝ*)
324239adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝐸𝑋) ∈ ℝ*)
325 elinel1 3761 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
326 elioore 12076 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝑄𝑖)(,)+∞) → 𝑥 ∈ ℝ)
327326rexrd 9968 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((𝑄𝑖)(,)+∞) → 𝑥 ∈ ℝ*)
328325, 327syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ ℝ*)
329328adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ℝ*)
330203adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) ∈ ℝ*)
331262a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → +∞ ∈ ℝ*)
332325adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
333 ioogtlb 38564 . . . . . . . . . . . . . . . 16 (((𝑄𝑖) ∈ ℝ* ∧ +∞ ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,)+∞)) → (𝑄𝑖) < 𝑥)
334330, 331, 332, 333syl3anc 1318 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) < 𝑥)
3353343adantl3 1212 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) < 𝑥)
336 elinel2 3762 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
337 elsni 4142 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {(𝐸𝑋)} → 𝑥 = (𝐸𝑋))
338337adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → 𝑥 = (𝐸𝑋))
339137adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → (𝐸𝑋) ≤ (𝐸𝑋))
340338, 339eqbrtrd 4605 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
341340adantlr 747 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
342 simpll 786 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝜑)
343 elunnel2 38221 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
344343adantll 746 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
345 elinel1 3761 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
346 elioore 12076 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-∞(,)(𝐸𝑋)) → 𝑥 ∈ ℝ)
347346adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ∈ ℝ)
348136adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → (𝐸𝑋) ∈ ℝ)
349197a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → -∞ ∈ ℝ*)
350348rexrd 9968 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → (𝐸𝑋) ∈ ℝ*)
351 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
352 iooltub 38582 . . . . . . . . . . . . . . . . . . . . . 22 ((-∞ ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 < (𝐸𝑋))
353349, 350, 351, 352syl3anc 1318 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 < (𝐸𝑋))
354347, 348, 353ltled 10064 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
355345, 354sylan2 490 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) → 𝑥 ≤ (𝐸𝑋))
356342, 344, 355syl2anc 691 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
357341, 356pm2.61dan 828 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ≤ (𝐸𝑋))
358357adantlr 747 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ≤ (𝐸𝑋))
359336, 358sylan2 490 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ≤ (𝐸𝑋))
3603593adantl3 1212 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ≤ (𝐸𝑋))
361323, 324, 329, 335, 360eliocd 38577 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)))
362322, 361impbida 873 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)) ↔ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))))
363362eqrdv 2608 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) = (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
364 ioossre 12106 . . . . . . . . . . . . . 14 (-∞(,)(𝐸𝑋)) ⊆ ℝ
365 ssinss1 3803 . . . . . . . . . . . . . 14 ((-∞(,)(𝐸𝑋)) ⊆ ℝ → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℝ)
366364, 365mp1i 13 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℝ)
367238snssd 4281 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {(𝐸𝑋)} ⊆ ℝ)
368366, 367unssd 3751 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ⊆ ℝ)
369 eqid 2610 . . . . . . . . . . . . 13 (topGen‘ran (,)) = (topGen‘ran (,))
370236, 369tgiooss 38580 . . . . . . . . . . . 12 ((((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
371368, 370syl 17 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
372260, 363, 3713eltr4d 2703 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
373 isopn3i 20696 . . . . . . . . . 10 ((((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top ∧ ((𝑄𝑖)(,](𝐸𝑋)) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))) = ((𝑄𝑖)(,](𝐸𝑋)))
374253, 372, 373sylancr 694 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))) = ((𝑄𝑖)(,](𝐸𝑋)))
375246, 374eqtr2d 2645 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})))
376243, 375eleqtrd 2690 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})))
377196, 231, 235, 236, 237, 376limcres 23456 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) lim (𝐸𝑋)))
378231resabs1d 5348 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
379378oveq1d 6564 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
380189, 377, 3793eqtr2d 2650 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
381184feq2d 5944 . . . . . . . . . . . 12 (𝜑 → (𝐹:dom 𝐹⟶ℂ ↔ 𝐹:𝐷⟶ℂ))
382192, 381mpbird 246 . . . . . . . . . . 11 (𝜑𝐹:dom 𝐹⟶ℂ)
383382adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝐹:dom 𝐹⟶ℂ)
3843833ad2antl1 1216 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝐹:dom 𝐹⟶ℂ)
385 ioosscn 38563 . . . . . . . . . 10 ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ℂ
386385a1i 11 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ℂ)
387184eqcomd 2616 . . . . . . . . . . . 12 (𝜑𝐷 = dom 𝐹)
3883873ad2ant1 1075 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 = dom 𝐹)
389230, 388sseqtrd 3604 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ dom 𝐹)
390389adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ dom 𝐹)
3917a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
392 oveq2 6557 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
393392oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑋) / 𝑇))
394393fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑋) / 𝑇)))
395394oveq1d 6564 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
396395adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 𝑋) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
3972, 14resubcld 10337 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵𝑋) ∈ ℝ)
3982, 1resubcld 10337 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐵𝐴) ∈ ℝ)
3994, 398syl5eqel 2692 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ ℝ)
4001, 2posdifd 10493 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
4013, 400mpbid 221 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 < (𝐵𝐴))
4024eqcomi 2619 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵𝐴) = 𝑇
403402a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵𝐴) = 𝑇)
404401, 403breqtrd 4609 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < 𝑇)
405404gt0ne0d 10471 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ≠ 0)
406397, 399, 405redivcld 10732 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵𝑋) / 𝑇) ∈ ℝ)
407406flcld 12461 . . . . . . . . . . . . . . . . 17 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
408407zred 11358 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℝ)
409408, 399remulcld 9949 . . . . . . . . . . . . . . 15 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
410391, 396, 14, 409fvmptd 6197 . . . . . . . . . . . . . 14 (𝜑 → (𝑍𝑋) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
411410, 409eqeltrd 2688 . . . . . . . . . . . . 13 (𝜑 → (𝑍𝑋) ∈ ℝ)
412411recnd 9947 . . . . . . . . . . . 12 (𝜑 → (𝑍𝑋) ∈ ℂ)
413412adantr 480 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → (𝑍𝑋) ∈ ℂ)
4144133ad2antl1 1216 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → (𝑍𝑋) ∈ ℂ)
415414negcld 10258 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → -(𝑍𝑋) ∈ ℂ)
416 eqid 2610 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}
417 ioosscn 38563 . . . . . . . . . . . . . . . . . . 19 (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ℂ
418417sseli 3564 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℂ)
419418adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℂ)
420412adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℂ)
421419, 420pncand 10272 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑦)
422421eqcomd 2616 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)))
4234223ad2antl1 1216 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)))
424410oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
425424adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
426419, 420addcld 9938 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℂ)
427409recnd 9947 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
428427adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
429426, 428negsubd 10277 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
430407zcnd 11359 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
431399recnd 9947 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇 ∈ ℂ)
432430, 431mulneg1d 10362 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
433432eqcomd 2616 . . . . . . . . . . . . . . . . . . 19 (𝜑 → -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
434433oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
435434adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
436425, 429, 4353eqtr2d 2650 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
4374363ad2antl1 1216 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
438407znegcld 11360 . . . . . . . . . . . . . . . . . 18 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
439438adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
4404393ad2antl1 1216 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
441 simpl1 1057 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
442230adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ 𝐷)
443203adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ*)
444136rexrd 9968 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸𝑋) ∈ ℝ*)
445444ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ∈ ℝ*)
446 elioore 12076 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
447446adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
448411adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
449447, 448readdcld 9948 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
450449adantlr 747 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
451411adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℝ)
452202, 451resubcld 10337 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
453452rexrd 9968 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
454453adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
45514rexrd 9968 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋 ∈ ℝ*)
456455ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
457 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
458 ioogtlb 38564 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
459454, 456, 457, 458syl3anc 1318 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
460202adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ)
461451adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
462446adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
463460, 461, 462ltsubaddd 10502 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑦 ↔ (𝑄𝑖) < (𝑦 + (𝑍𝑋))))
464459, 463mpbid 221 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
46514ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
466 iooltub 38582 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
467454, 456, 457, 466syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
468462, 465, 461, 467ltadd1dd 10517 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑋 + (𝑍𝑋)))
4695a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))))
470 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑋𝑥 = 𝑋)
471 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑋 → (𝑍𝑥) = (𝑍𝑋))
472470, 471oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑋 → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
473472adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 = 𝑋) → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
47414, 411readdcld 9948 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℝ)
475469, 473, 14, 474fvmptd 6197 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
476475eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
477476ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
478468, 477breqtrd 4609 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
479443, 445, 450, 464, 478eliood 38567 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝐸𝑋)))
4804793adantl3 1212 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝐸𝑋)))
481442, 480sseldd 3569 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
482441, 481, 4403jca 1235 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
483 eleq1 2676 . . . . . . . . . . . . . . . . . . 19 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
4844833anbi3d 1397 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
485 oveq1 6556 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
486485oveq2d 6565 . . . . . . . . . . . . . . . . . . 19 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
487486eleq1d 2672 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
488484, 487imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
489 ovex 6577 . . . . . . . . . . . . . . . . . 18 (𝑦 + (𝑍𝑋)) ∈ V
490 eleq1 2676 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥𝐷 ↔ (𝑦 + (𝑍𝑋)) ∈ 𝐷))
4914903anbi2d 1396 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ)))
492 oveq1 6556 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)))
493492eleq1d 2672 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
494491, 493imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑦 + (𝑍𝑋)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
495 fourierdlem49.dper . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
496489, 494, 495vtocl 3232 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
497488, 496vtoclg 3239 . . . . . . . . . . . . . . . 16 (-(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
498440, 482, 497sylc 63 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
499437, 498eqeltrd 2688 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) ∈ 𝐷)
500423, 499eqeltrd 2688 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦𝐷)
501500ralrimiva 2949 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
502 dfss3 3558 . . . . . . . . . . . 12 ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
503501, 502sylibr 223 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)
504202recnd 9947 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
505412adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℂ)
506504, 505negsubd 10277 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + -(𝑍𝑋)) = ((𝑄𝑖) − (𝑍𝑋)))
507506eqcomd 2616 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) = ((𝑄𝑖) + -(𝑍𝑋)))
508475oveq1d 6564 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑋) + -(𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) + -(𝑍𝑋)))
509474recnd 9947 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℂ)
510509, 412negsubd 10277 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍𝑋)) + -(𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)))
51114recnd 9947 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ ℂ)
512511, 412pncand 10272 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑋)
513508, 510, 5123eqtrrd 2649 . . . . . . . . . . . . . . 15 (𝜑𝑋 = ((𝐸𝑋) + -(𝑍𝑋)))
514513adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 = ((𝐸𝑋) + -(𝑍𝑋)))
515507, 514oveq12d 6567 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) = (((𝑄𝑖) + -(𝑍𝑋))(,)((𝐸𝑋) + -(𝑍𝑋))))
516451renegcld 10336 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → -(𝑍𝑋) ∈ ℝ)
517202, 278, 516iooshift 38595 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + -(𝑍𝑋))(,)((𝐸𝑋) + -(𝑍𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))})
518515, 517eqtr2d 2645 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
5195183adant3 1074 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
5201843ad2ant1 1075 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → dom 𝐹 = 𝐷)
521503, 519, 5203sstr4d 3611 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} ⊆ dom 𝐹)
522521adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} ⊆ dom 𝐹)
523410negeqd 10154 . . . . . . . . . . . . . . . 16 (𝜑 → -(𝑍𝑋) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
524523, 433eqtrd 2644 . . . . . . . . . . . . . . 15 (𝜑 → -(𝑍𝑋) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
525524oveq2d 6565 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + -(𝑍𝑋)) = (𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
526525fveq2d 6107 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
527526adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
5285273ad2antl1 1216 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
529438adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
5305293ad2antl1 1216 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
531 simpl1 1057 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → 𝜑)
532230sselda 3568 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → 𝑥𝐷)
533531, 532, 5303jca 1235 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
5344833anbi3d 1397 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
535485oveq2d 6565 . . . . . . . . . . . . . . . 16 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
536535fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
537536eqeq1d 2612 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥) ↔ (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
538534, 537imbi12d 333 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥)) ↔ ((𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))))
539 fourierdlem49.per . . . . . . . . . . . . 13 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥))
540538, 539vtoclg 3239 . . . . . . . . . . . 12 (-(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
541530, 533, 540sylc 63 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))
542528, 541eqtrd 2644 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹𝑥))
543542adantlr 747 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹𝑥))
544 simpr 476 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
545384, 386, 390, 415, 416, 522, 543, 544limcperiod 38695 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))))
546518reseq2d 5317 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) = (𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)))
547514eqcomd 2616 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) + -(𝑍𝑋)) = 𝑋)
548546, 547oveq12d 6567 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
5495483adant3 1074 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
550549adantr 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
551545, 550eleqtrd 2690 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
552382adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝐹:dom 𝐹⟶ℂ)
5535523ad2antl1 1216 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝐹:dom 𝐹⟶ℂ)
554417a1i 11 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ℂ)
555503, 520sseqtr4d 3605 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ dom 𝐹)
556555adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ dom 𝐹)
557412adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (𝑍𝑋) ∈ ℂ)
5585573ad2antl1 1216 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (𝑍𝑋) ∈ ℂ)
559 eqid 2610 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}
560504, 505npcand 10275 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄𝑖))
561560eqcomd 2616 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = (((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋)))
562475adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
563561, 562oveq12d 6567 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝐸𝑋)) = ((((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋))(,)(𝑋 + (𝑍𝑋))))
56414adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
565452, 564, 451iooshift 38595 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋))(,)(𝑋 + (𝑍𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))})
566563, 565eqtr2d 2645 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = ((𝑄𝑖)(,)(𝐸𝑋)))
5675663adant3 1074 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = ((𝑄𝑖)(,)(𝐸𝑋)))
568230, 567, 5203sstr4d 3611 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} ⊆ dom 𝐹)
569568adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} ⊆ dom 𝐹)
570410oveq2d 6565 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + (𝑍𝑋)) = (𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
571570fveq2d 6107 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
572571adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
5735723ad2antl1 1216 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
574407adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
5755743ad2antl1 1216 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
576 simpl1 1057 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
577503sselda 3568 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥𝐷)
578576, 577, 5753jca 1235 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
579 eleq1 2676 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
5805793anbi3d 1397 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
581 oveq1 6556 . . . . . . . . . . . . . . . . 17 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
582581oveq2d 6565 . . . . . . . . . . . . . . . 16 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
583582fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
584583eqeq1d 2612 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥) ↔ (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
585580, 584imbi12d 333 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥)) ↔ ((𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))))
586585, 539vtoclg 3239 . . . . . . . . . . . 12 ((⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
587575, 578, 586sylc 63 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))
588573, 587eqtrd 2644 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹𝑥))
589588adantlr 747 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹𝑥))
590 simpr 476 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
591553, 554, 556, 558, 559, 569, 589, 590limcperiod 38695 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))))
592566reseq2d 5317 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
593476adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
594592, 593oveq12d 6567 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
5955943adant3 1074 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
596595adantr 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
597591, 596eleqtrd 2690 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
598551, 597impbida 873 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ↔ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)))
599598eqrdv 2608 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
600 resindm 5364 . . . . . . . . . . 11 (Rel 𝐹 → (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)𝑋)))
601600eqcomd 2616 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)))
602179, 601syl 17 . . . . . . . . 9 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)))
603184ineq2d 3776 . . . . . . . . . 10 (𝜑 → ((-∞(,)𝑋) ∩ dom 𝐹) = ((-∞(,)𝑋) ∩ 𝐷))
604603reseq2d 5317 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
605602, 604eqtrd 2644 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
606605oveq1d 6564 . . . . . . 7 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
6076063ad2ant1 1075 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
608 inss2 3796 . . . . . . . . . 10 ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷
609608a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷)
610193, 609fssresd 5984 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)):((-∞(,)𝑋) ∩ 𝐷)⟶ℂ)
611452mnfltd 11834 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < ((𝑄𝑖) − (𝑍𝑋)))
612198, 453, 611xrltled 38427 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ ((𝑄𝑖) − (𝑍𝑋)))
613 iooss1 12081 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ -∞ ≤ ((𝑄𝑖) − (𝑍𝑋))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
614197, 612, 613sylancr 694 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
6156143adant3 1074 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
616615, 503ssind 3799 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ 𝐷))
617608, 234syl5ss 3579 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℂ)
618 eqid 2610 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
6194533adant3 1074 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
6204553ad2ant1 1075 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ*)
6214753ad2ant1 1075 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
622241, 621breqtrd 4609 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑋 + (𝑍𝑋)))
6234113ad2ant1 1075 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
624143ad2ant1 1075 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
625214, 623, 624ltsubaddd 10502 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ↔ (𝑄𝑖) < (𝑋 + (𝑍𝑋))))
626622, 625mpbird 246 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑋)
62714leidd 10473 . . . . . . . . . . 11 (𝜑𝑋𝑋)
6286273ad2ant1 1075 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋𝑋)
629619, 620, 620, 626, 628eliocd 38577 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
630 snunioo2 38578 . . . . . . . . . . . 12 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ* ∧ ((𝑄𝑖) − (𝑍𝑋)) < 𝑋) → ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
631619, 620, 626, 630syl3anc 1318 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
632631fveq2d 6107 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)))
633 ovex 6577 . . . . . . . . . . . . . 14 (-∞(,)𝑋) ∈ V
634633inex1 4727 . . . . . . . . . . . . 13 ((-∞(,)𝑋) ∩ 𝐷) ∈ V
635 snex 4835 . . . . . . . . . . . . 13 {𝑋} ∈ V
636634, 635unex 6854 . . . . . . . . . . . 12 (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V
637 resttop 20774 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top)
638247, 636, 637mp2an 704 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top
639636a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V)
640 iooretop 22379 . . . . . . . . . . . . . 14 (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,))
641640a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,)))
642 elrestr 15912 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ Top ∧ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V ∧ (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,))) → ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
643255, 639, 641, 642syl3anc 1318 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
644453adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
645262a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → +∞ ∈ ℝ*)
64614ad2antrr 758 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑋 ∈ ℝ)
647 iocssre 12124 . . . . . . . . . . . . . . . . . . 19 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ⊆ ℝ)
648644, 646, 647syl2anc 691 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ⊆ ℝ)
649 simpr 476 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
650648, 649sseldd 3569 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ ℝ)
651455ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑋 ∈ ℝ*)
652 iocgtlb 38571 . . . . . . . . . . . . . . . . . 18 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
653644, 651, 649, 652syl3anc 1318 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
654650ltpnfd 11831 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 < +∞)
655644, 645, 650, 653, 654eliood 38567 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
6566553adantl3 1212 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
657 eqvisset 3184 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋𝑋 ∈ V)
658 snidg 4153 . . . . . . . . . . . . . . . . . . . 20 (𝑋 ∈ V → 𝑋 ∈ {𝑋})
659657, 658syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋𝑋 ∈ {𝑋})
660470, 659eqeltrd 2688 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋𝑥 ∈ {𝑋})
661 elun2 3743 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑋} → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
662660, 661syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
663662adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ 𝑥 = 𝑋) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
664 simpll 786 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → (𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
665644adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
666455ad3antrrr 762 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋 ∈ ℝ*)
667650adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ ℝ)
668653adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
66914ad3antrrr 762 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋 ∈ ℝ)
670 iocleub 38572 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥𝑋)
671644, 651, 649, 670syl3anc 1318 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥𝑋)
672671adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥𝑋)
673470eqcoms 2618 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = 𝑥𝑥 = 𝑋)
674673necon3bi 2808 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = 𝑋𝑋𝑥)
675674adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋𝑥)
676667, 669, 672, 675leneltd 10070 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 < 𝑋)
677665, 666, 667, 668, 676eliood 38567 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
6786773adantll3 38226 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
679616sselda 3568 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
680 elun1 3742 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
681679, 680syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
682664, 678, 681syl2anc 691 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
683663, 682pm2.61dan 828 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
684656, 683elind 3760 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
685619adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
686620adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑋 ∈ ℝ*)
687 elinel1 3761 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
688 elioore 12076 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞) → 𝑥 ∈ ℝ)
689687, 688syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ)
690689rexrd 9968 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ*)
691690adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ ℝ*)
692453adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
693262a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → +∞ ∈ ℝ*)
694687adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
695 ioogtlb 38564 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ* ∧ +∞ ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
696692, 693, 694, 695syl3anc 1318 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
6976963adantl3 1212 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
698 elinel2 3762 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
699 elsni 4142 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑋} → 𝑥 = 𝑋)
700699adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {𝑋}) → 𝑥 = 𝑋)
701627adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {𝑋}) → 𝑋𝑋)
702700, 701eqbrtrd 4605 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ {𝑋}) → 𝑥𝑋)
703702adantlr 747 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ 𝑥 ∈ {𝑋}) → 𝑥𝑋)
704 simpll 786 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝜑)
705 elunnel2 38221 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
706705adantll 746 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
707 elinel1 3761 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷) → 𝑥 ∈ (-∞(,)𝑋))
708706, 707syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ (-∞(,)𝑋))
709 elioore 12076 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-∞(,)𝑋) → 𝑥 ∈ ℝ)
710709adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ ℝ)
71114adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ)
712197a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → -∞ ∈ ℝ*)
713455adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ*)
714 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ (-∞(,)𝑋))
715 iooltub 38582 . . . . . . . . . . . . . . . . . . . . 21 ((-∞ ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (-∞(,)𝑋)) → 𝑥 < 𝑋)
716712, 713, 714, 715syl3anc 1318 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 < 𝑋)
717710, 711, 716ltled 10064 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥𝑋)
718704, 708, 717syl2anc 691 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥𝑋)
719703, 718pm2.61dan 828 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥𝑋)
720698, 719sylan2 490 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥𝑋)
7217203ad2antl1 1216 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥𝑋)
722685, 686, 691, 697, 721eliocd 38577 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
723684, 722impbida 873 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ↔ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))))
724723eqrdv 2608 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) = ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
725608, 232syl5ss 3579 . . . . . . . . . . . . . . 15 (𝜑 → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℝ)
72614snssd 4281 . . . . . . . . . . . . . . 15 (𝜑 → {𝑋} ⊆ ℝ)
727725, 726unssd 3751 . . . . . . . . . . . . . 14 (𝜑 → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
7287273ad2ant1 1075 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
729236, 369tgiooss 38580 . . . . . . . . . . . . 13 ((((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
730728, 729syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
731643, 724, 7303eltr4d 2703 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
732 isopn3i 20696 . . . . . . . . . . 11 ((((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top ∧ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
733638, 731, 732sylancr 694 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
734632, 733eqtr2d 2645 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})))
735629, 734eleqtrd 2690 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})))
736610, 616, 617, 236, 618, 735limcres 23456 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
737736eqcomd 2616 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋) = (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
738616resabs1d 5348 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) = (𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)))
739738oveq1d 6564 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
740607, 737, 7393eqtrrd 2649 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋))
741380, 599, 7403eqtrrd 2649 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)))
742741rexlimdv3a 3015 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋))))
743176, 742mpd 15 . 2 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)))
7441233adant3 1074 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
7452213adant3 1074 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
746 fourierdlem49.l . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
7477463adant3 1074 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
748 eqid 2610 . . . . . . . 8 if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) = if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋)))
749 eqid 2610 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
750214, 212, 744, 745, 747, 214, 238, 241, 220, 748, 749fourierdlem33 39033 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
751220resabs1d 5348 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
752751oveq1d 6564 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
753750, 752eleqtrd 2690 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
754 ne0i 3880 . . . . . 6 (if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
755753, 754syl 17 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
756380, 755eqnetrd 2849 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
757756rexlimdv3a 3015 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅))
758176, 757mpd 15 . 2 (𝜑 → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
759743, 758eqnetrd 2849 1 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wne 2780  wral 2896  wrex 2897  {crab 2900  Vcvv 3173  cun 3538  cin 3539  wss 3540  c0 3874  ifcif 4036  {csn 4125   class class class wbr 4583  cmpt 4643  dom cdm 5038  ran crn 5039  cres 5040  Rel wrel 5043   Fn wfn 5799  wf 5800  cfv 5804  (class class class)co 6549  𝑚 cmap 7744  supcsup 8229  cc 9813  cr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  +∞cpnf 9950  -∞cmnf 9951  *cxr 9952   < clt 9953  cle 9954  cmin 10145  -cneg 10146   / cdiv 10563  cn 10897  0cn0 11169  cz 11254  cuz 11563  (,)cioo 12046  (,]cioc 12047  [,]cicc 12049  ...cfz 12197  ..^cfzo 12334  cfl 12453  t crest 15904  TopOpenctopn 15905  topGenctg 15921  fldccnfld 19567  Topctop 20517  intcnt 20631  cnccncf 22487   lim climc 23432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-plusg 15781  df-mulr 15782  df-starv 15783  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-rest 15906  df-topn 15907  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-ntr 20634  df-cn 20841  df-cnp 20842  df-xms 21935  df-ms 21936  df-cncf 22489  df-limc 23436
This theorem is referenced by:  fourierdlem94  39093  fourierdlem113  39112
  Copyright terms: Public domain W3C validator