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

Theorem fourierdlem41 40882
Description: Lemma used to prove that every real is a limit point for the domain of the derivative of the periodic function to be approximated. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem41.a (𝜑𝐴 ∈ ℝ)
fourierdlem41.b (𝜑𝐵 ∈ ℝ)
fourierdlem41.altb (𝜑𝐴 < 𝐵)
fourierdlem41.t 𝑇 = (𝐵𝐴)
fourierdlem41.dper ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
fourierdlem41.x (𝜑𝑋 ∈ ℝ)
fourierdlem41.z 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
fourierdlem41.e 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥)))
fourierdlem41.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem41.m (𝜑𝑀 ∈ ℕ)
fourierdlem41.q (𝜑𝑄 ∈ (𝑃𝑀))
fourierdlem41.qssd ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
Assertion
Ref Expression
fourierdlem41 (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
Distinct variable groups:   𝐴,𝑚,𝑝   𝑥,𝐴   𝐵,𝑖,𝑘   𝐵,𝑚,𝑝,𝑖   𝑥,𝐵,𝑦,𝑘   𝐷,𝑖,𝑘,𝑦   𝑥,𝐷   𝑖,𝐸,𝑘,𝑦   𝑖,𝑀,𝑘   𝑚,𝑀,𝑝   𝑦,𝑀   𝑄,𝑖,𝑘   𝑄,𝑝   𝑦,𝑄   𝑇,𝑘,𝑥,𝑦   𝑖,𝑋,𝑘   𝑥,𝑋,𝑦   𝑘,𝑍,𝑥,𝑦   𝜑,𝑖,𝑘   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑚,𝑝)   𝐴(𝑦,𝑖,𝑘)   𝐷(𝑚,𝑝)   𝑃(𝑥,𝑦,𝑖,𝑘,𝑚,𝑝)   𝑄(𝑥,𝑚)   𝑇(𝑖,𝑚,𝑝)   𝐸(𝑥,𝑚,𝑝)   𝑀(𝑥)   𝑋(𝑚,𝑝)   𝑍(𝑖,𝑚,𝑝)

Proof of Theorem fourierdlem41
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 simpr 471 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ran 𝑄)
2 fourierdlem41.q . . . . . . . . . . 11 (𝜑𝑄 ∈ (𝑃𝑀))
3 fourierdlem41.m . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
4 fourierdlem41.p . . . . . . . . . . . . 13 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
54fourierdlem2 40843 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
63, 5syl 17 . . . . . . . . . . 11 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
72, 6mpbid 222 . . . . . . . . . 10 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
87simpld 482 . . . . . . . . 9 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
9 elmapi 8031 . . . . . . . . 9 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10 ffn 6185 . . . . . . . . 9 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
118, 9, 103syl 18 . . . . . . . 8 (𝜑𝑄 Fn (0...𝑀))
1211adantr 466 . . . . . . 7 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
13 fvelrnb 6385 . . . . . . 7 (𝑄 Fn (0...𝑀) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
1412, 13syl 17 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
151, 14mpbid 222 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
16 0zd 11591 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ∈ ℤ)
17 elfzelz 12549 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18173ad2ant2 1128 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℤ)
19 1zzd 11610 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ∈ ℤ)
2018, 19zsubcld 11689 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℤ)
21 simpll 750 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝜑)
22 elfzle1 12551 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
2322anim1i 602 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗))
24 0red 10243 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 ∈ ℝ)
2517zred 11684 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
2625adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 ∈ ℝ)
2724, 26eqleltd 10383 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 = 𝑗 ↔ (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗)))
2823, 27mpbird 247 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 = 𝑗)
2928eqcomd 2777 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
3029adantll 693 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
31 fveq2 6332 . . . . . . . . . . . . . . . 16 (𝑗 = 0 → (𝑄𝑗) = (𝑄‘0))
327simprld 755 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
3332simpld 482 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
3431, 33sylan9eqr 2827 . . . . . . . . . . . . . . 15 ((𝜑𝑗 = 0) → (𝑄𝑗) = 𝐴)
3521, 30, 34syl2anc 573 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) = 𝐴)
36353adantl3 1173 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) = 𝐴)
37 simpr 471 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
38 fourierdlem41.a . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ)
3938rexrd 10291 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ*)
40 fourierdlem41.b . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ ℝ)
4140rexrd 10291 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℝ*)
42 fourierdlem41.altb . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 < 𝐵)
43 fourierdlem41.t . . . . . . . . . . . . . . . . . . . . . . 23 𝑇 = (𝐵𝐴)
44 eqid 2771 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
4538, 40, 42, 43, 44fourierdlem4 40845 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵))
46 fourierdlem41.e . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥)))
4746a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))))
48 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
4940adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
5049, 48resubcld 10660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → (𝐵𝑥) ∈ ℝ)
5140, 38resubcld 10660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝐵𝐴) ∈ ℝ)
5243, 51syl5eqel 2854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝑇 ∈ ℝ)
5352adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
54 0red 10243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 0 ∈ ℝ)
5538, 40posdifd 10816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
5642, 55mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → 0 < (𝐵𝐴))
5743eqcomi 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝐵𝐴) = 𝑇
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (𝐵𝐴) = 𝑇)
5956, 58breqtrd 4812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 0 < 𝑇)
6054, 59gtned 10374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝑇 ≠ 0)
6160adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → 𝑇 ≠ 0)
6250, 53, 61redivcld 11055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑥 ∈ ℝ) → ((𝐵𝑥) / 𝑇) ∈ ℝ)
6362flcld 12807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ)
6463zred 11684 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℝ)
6564, 53remulcld 10272 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ ℝ) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
66 fourierdlem41.z . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6766fvmpt2 6433 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6848, 65, 67syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ ℝ) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6968oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ ℝ) → (𝑥 + (𝑍𝑥)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
7069mpteq2dva 4878 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
7147, 70eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
7271feq1d 6170 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐸:ℝ⟶(𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵)))
7345, 72mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
74 fourierdlem41.x . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ)
7573, 74ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸𝑋) ∈ (𝐴(,]𝐵))
76 iocgtlb 40245 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
7739, 41, 75, 76syl3anc 1476 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 < (𝐸𝑋))
7838, 77gtned 10374 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐸𝑋) ≠ 𝐴)
7978adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≠ 𝐴)
8037, 79eqnetrd 3010 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≠ 𝐴)
8180adantr 466 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) ≠ 𝐴)
82813adantl2 1172 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) ≠ 𝐴)
8382neneqd 2948 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → ¬ (𝑄𝑗) = 𝐴)
8436, 83condan 819 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 < 𝑗)
85 zltlem1 11632 . . . . . . . . . . . . 13 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
8616, 18, 85syl2anc 573 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
8784, 86mpbid 222 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ (𝑗 − 1))
88 eluz2 11894 . . . . . . . . . . 11 ((𝑗 − 1) ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ ∧ 0 ≤ (𝑗 − 1)))
8916, 20, 87, 88syl3anbrc 1428 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (ℤ‘0))
90 elfzel2 12547 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
91903ad2ant2 1128 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℤ)
92 1red 10257 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 1 ∈ ℝ)
9325, 92resubcld 10660 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
9490zred 11684 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
9525ltm1d 11158 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
96 elfzle2 12552 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → 𝑗𝑀)
9793, 25, 94, 95, 96ltletrd 10399 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
98973ad2ant2 1128 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) < 𝑀)
99 elfzo2 12681 . . . . . . . . . 10 ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
10089, 91, 98, 99syl3anbrc 1428 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
1018, 9syl 17 . . . . . . . . . . . . 13 (𝜑𝑄:(0...𝑀)⟶ℝ)
1021013ad2ant1 1127 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
10316, 91, 203jca 1122 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ))
10493, 94, 97ltled 10387 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
1051043ad2ant2 1128 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ≤ 𝑀)
106103, 87, 105jca32 505 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
107 elfz2 12540 . . . . . . . . . . . . 13 ((𝑗 − 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
108106, 107sylibr 224 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
109102, 108ffvelrnd 6503 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
110109rexrd 10291 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
11125recnd 10270 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
112 1cnd 10258 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
113111, 112npcand 10598 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
114113fveq2d 6336 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
115114adantl 467 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
116101ffvelrnda 6502 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ)
117116rexrd 10291 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
118115, 117eqeltrd 2850 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ*)
1191183adant3 1126 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ*)
120 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋𝑥 = 𝑋)
121 fveq2 6332 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑍𝑥) = (𝑍𝑋))
122120, 121oveq12d 6811 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
123122adantl 467 . . . . . . . . . . . . . 14 ((𝜑𝑥 = 𝑋) → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
12466a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
125 oveq2 6801 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
126125oveq1d 6808 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑋) / 𝑇))
127126fveq2d 6336 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑋) / 𝑇)))
128127oveq1d 6808 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
129128adantl 467 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 = 𝑋) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
13040, 74resubcld 10660 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵𝑋) ∈ ℝ)
131130, 52, 60redivcld 11055 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐵𝑋) / 𝑇) ∈ ℝ)
132131flcld 12807 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
133132zred 11684 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℝ)
134133, 52remulcld 10272 . . . . . . . . . . . . . . . . 17 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
135124, 129, 74, 134fvmptd 6430 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑍𝑋) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
136135, 134eqeltrd 2850 . . . . . . . . . . . . . . 15 (𝜑 → (𝑍𝑋) ∈ ℝ)
13774, 136readdcld 10271 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℝ)
13847, 123, 74, 137fvmptd 6430 . . . . . . . . . . . . 13 (𝜑 → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
139138, 137eqeltrd 2850 . . . . . . . . . . . 12 (𝜑 → (𝐸𝑋) ∈ ℝ)
140139rexrd 10291 . . . . . . . . . . 11 (𝜑 → (𝐸𝑋) ∈ ℝ*)
1411403ad2ant1 1127 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
142 simp1 1130 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
143 ovex 6823 . . . . . . . . . . . . . 14 (𝑗 − 1) ∈ V
144 eleq1 2838 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
145144anbi2d 614 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 − 1) → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
146 fveq2 6332 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑄𝑖) = (𝑄‘(𝑗 − 1)))
147 oveq1 6800 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
148147fveq2d 6336 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
149146, 148breq12d 4799 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 − 1) → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
150145, 149imbi12d 333 . . . . . . . . . . . . . 14 (𝑖 = (𝑗 − 1) → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
1517simprrd 757 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
152151r19.21bi 3081 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
153143, 150, 152vtocl 3410 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
154142, 100, 153syl2anc 573 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
1551143ad2ant2 1128 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
156154, 155breqtrd 4812 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄𝑗))
157 simp3 1132 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
158156, 157breqtrd 4812 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸𝑋))
159139leidd 10796 . . . . . . . . . . . . . 14 (𝜑 → (𝐸𝑋) ≤ (𝐸𝑋))
160159adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝐸𝑋))
16137eqcomd 2777 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
162160, 161breqtrd 4812 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
1631623adant2 1125 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
164113eqcomd 2777 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
165164fveq2d 6336 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
1661653ad2ant2 1128 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
167163, 166breqtrd 4812 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄‘((𝑗 − 1) + 1)))
168110, 119, 141, 158, 167eliocd 40251 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
169146, 148oveq12d 6811 . . . . . . . . . . 11 (𝑖 = (𝑗 − 1) → ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
170169eleq2d 2836 . . . . . . . . . 10 (𝑖 = (𝑗 − 1) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
171170rspcev 3460 . . . . . . . . 9 (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
172100, 168, 171syl2anc 573 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
1731723exp 1112 . . . . . . 7 (𝜑 → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))))
174173adantr 466 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))))
175174rexlimdv 3178 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
17615, 175mpd 15 . . . 4 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
1773adantr 466 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
178101adantr 466 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
179 iocssicc 12467 . . . . . . . 8 ((𝑄‘0)(,](𝑄𝑀)) ⊆ ((𝑄‘0)[,](𝑄𝑀))
18032simprd 483 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = 𝐵)
18133, 180oveq12d 6811 . . . . . . . . 9 (𝜑 → ((𝑄‘0)(,](𝑄𝑀)) = (𝐴(,]𝐵))
18275, 181eleqtrrd 2853 . . . . . . . 8 (𝜑 → (𝐸𝑋) ∈ ((𝑄‘0)(,](𝑄𝑀)))
183179, 182sseldi 3750 . . . . . . 7 (𝜑 → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
184183adantr 466 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
185 simpr 471 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ¬ (𝐸𝑋) ∈ ran 𝑄)
186 fveq2 6332 . . . . . . . . 9 (𝑘 = 𝑗 → (𝑄𝑘) = (𝑄𝑗))
187186breq1d 4796 . . . . . . . 8 (𝑘 = 𝑗 → ((𝑄𝑘) < (𝐸𝑋) ↔ (𝑄𝑗) < (𝐸𝑋)))
188187cbvrabv 3349 . . . . . . 7 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}
189188supeq1i 8509 . . . . . 6 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}, ℝ, < )
190177, 178, 184, 185, 189fourierdlem25 40866 . . . . 5 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
191 ioossioc 40234 . . . . . . . 8 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))
192191a1i 11 . . . . . . 7 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
193192sseld 3751 . . . . . 6 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
194193reximdva 3165 . . . . 5 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
195190, 194mpd 15 . . . 4 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
196176, 195pm2.61dan 814 . . 3 (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
197101adantr 466 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
198 elfzofz 12693 . . . . . . . . . 10 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
199198adantl 467 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
200197, 199ffvelrnd 6503 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
2012003adant3 1126 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
2021363ad2ant1 1127 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
203201, 202resubcld 10660 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
2041393ad2ant1 1127 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
205201rexrd 10291 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
206 fzofzp1 12773 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
207206adantl 467 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
208197, 207ffvelrnd 6503 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209208rexrd 10291 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2102093adant3 1126 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
211 simp3 1132 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
212 iocgtlb 40245 . . . . . . . . 9 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
213205, 210, 211, 212syl3anc 1476 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
214201, 204, 202, 213ltsub1dd 10841 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < ((𝐸𝑋) − (𝑍𝑋)))
215138oveq1d 6808 . . . . . . . . 9 (𝜑 → ((𝐸𝑋) − (𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)))
21674recnd 10270 . . . . . . . . . 10 (𝜑𝑋 ∈ ℂ)
217136recnd 10270 . . . . . . . . . 10 (𝜑 → (𝑍𝑋) ∈ ℂ)
218216, 217pncand 10595 . . . . . . . . 9 (𝜑 → ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑋)
219215, 218eqtrd 2805 . . . . . . . 8 (𝜑 → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
2202193ad2ant1 1127 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
221214, 220breqtrd 4812 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑋)
222 elioore 12410 . . . . . . . . . . 11 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
223135oveq2d 6809 . . . . . . . . . . . . . 14 (𝜑 → (𝑦 + (𝑍𝑋)) = (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
224133recnd 10270 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
22552recnd 10270 . . . . . . . . . . . . . . 15 (𝜑𝑇 ∈ ℂ)
226224, 225mulneg1d 10685 . . . . . . . . . . . . . 14 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
227223, 226oveq12d 6811 . . . . . . . . . . . . 13 (𝜑 → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
228227adantr 466 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
229 simpr 471 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
230134adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
231229, 230readdcld 10271 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
232231recnd 10270 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ ℂ)
233230recnd 10270 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
234232, 233negsubd 10600 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
235229recnd 10270 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
236235, 233pncand 10595 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = 𝑦)
237228, 234, 2363eqtrrd 2810 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
238222, 237sylan2 580 . . . . . . . . . 10 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
2392383ad2antl1 1200 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
240 simpl1 1227 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
241 fourierdlem41.qssd . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
2422413adant3 1126 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
243242adantr 466 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
244205adantr 466 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ*)
245210adantr 466 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
246222adantl 467 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
247136adantr 466 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
248246, 247readdcld 10271 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
2492483ad2antl1 1200 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
250136adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℝ)
251200, 250resubcld 10660 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
252251rexrd 10291 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
253252adantr 466 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
25474rexrd 10291 . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℝ*)
255254ad2antrr 705 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
256 simpr 471 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
257 ioogtlb 40238 . . . . . . . . . . . . . . 15 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
258253, 255, 256, 257syl3anc 1476 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
259200adantr 466 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ)
260136ad2antrr 705 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
261222adantl 467 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
262259, 260, 261ltsubaddd 10825 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑦 ↔ (𝑄𝑖) < (𝑦 + (𝑍𝑋))))
263258, 262mpbid 222 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
2642633adantl3 1173 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
265240, 139syl 17 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ∈ ℝ)
266208adantr 466 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2672663adantl3 1173 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
26874ad2antrr 705 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
269 iooltub 40255 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
270253, 255, 256, 269syl3anc 1476 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
271261, 268, 260, 270ltadd1dd 10840 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑋 + (𝑍𝑋)))
272138eqcomd 2777 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
273272ad2antrr 705 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
274271, 273breqtrd 4812 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
2752743adantl3 1173 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
276 iocleub 40246 . . . . . . . . . . . . . . 15 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
277205, 210, 211, 276syl3anc 1476 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
278277adantr 466 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
279249, 265, 267, 275, 278ltletrd 10399 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
280244, 245, 249, 264, 279eliood 40241 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
281243, 280sseldd 3753 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
282240, 131syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝐵𝑋) / 𝑇) ∈ ℝ)
283282flcld 12807 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
284283znegcld 11686 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
285 negex 10481 . . . . . . . . . . 11 -(⌊‘((𝐵𝑋) / 𝑇)) ∈ V
286 eleq1 2838 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
2872863anbi3d 1553 . . . . . . . . . . . 12 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
288 oveq1 6800 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
289288oveq2d 6809 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
290289eleq1d 2835 . . . . . . . . . . . 12 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
291287, 290imbi12d 333 . . . . . . . . . . 11 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
292 ovex 6823 . . . . . . . . . . . 12 (𝑦 + (𝑍𝑋)) ∈ V
293 eleq1 2838 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥𝐷 ↔ (𝑦 + (𝑍𝑋)) ∈ 𝐷))
2942933anbi2d 1552 . . . . . . . . . . . . 13 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ)))
295 oveq1 6800 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)))
296295eleq1d 2835 . . . . . . . . . . . . 13 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
297294, 296imbi12d 333 . . . . . . . . . . . 12 (𝑥 = (𝑦 + (𝑍𝑋)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
298 fourierdlem41.dper . . . . . . . . . . . 12 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
299292, 297, 298vtocl 3410 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
300285, 291, 299vtocl 3410 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
301240, 281, 284, 300syl3anc 1476 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
302239, 301eqeltrd 2850 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦𝐷)
303302ralrimiva 3115 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
304 dfss3 3741 . . . . . . 7 ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
305303, 304sylibr 224 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)
306 breq1 4789 . . . . . . . 8 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → (𝑦 < 𝑋 ↔ ((𝑄𝑖) − (𝑍𝑋)) < 𝑋))
307 oveq1 6800 . . . . . . . . 9 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → (𝑦(,)𝑋) = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
308307sseq1d 3781 . . . . . . . 8 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → ((𝑦(,)𝑋) ⊆ 𝐷 ↔ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷))
309306, 308anbi12d 616 . . . . . . 7 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → ((𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ↔ (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ∧ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)))
310309rspcev 3460 . . . . . 6 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ ∧ (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ∧ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
311203, 221, 305, 310syl12anc 1474 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
3123113exp 1112 . . . 4 (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))))
313312rexlimdv 3178 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷)))
314196, 313mpd 15 . 2 (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
315 0zd 11591 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
3163nnzd 11683 . . . . . . . . . 10 (𝜑𝑀 ∈ ℤ)
317 1zzd 11610 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
318315, 316, 3173jca 1122 . . . . . . . . 9 (𝜑 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ))
319 0le1 10753 . . . . . . . . . 10 0 ≤ 1
320319a1i 11 . . . . . . . . 9 (𝜑 → 0 ≤ 1)
3213nnge1d 11265 . . . . . . . . 9 (𝜑 → 1 ≤ 𝑀)
322318, 320, 321jca32 505 . . . . . . . 8 (𝜑 → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
323 elfz2 12540 . . . . . . . 8 (1 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
324322, 323sylibr 224 . . . . . . 7 (𝜑 → 1 ∈ (0...𝑀))
325101, 324ffvelrnd 6503 . . . . . 6 (𝜑 → (𝑄‘1) ∈ ℝ)
326136, 52resubcld 10660 . . . . . 6 (𝜑 → ((𝑍𝑋) − 𝑇) ∈ ℝ)
327325, 326resubcld 10660 . . . . 5 (𝜑 → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ)
328327adantr 466 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ)
32938recnd 10270 . . . . . . . . . 10 (𝜑𝐴 ∈ ℂ)
330329, 225pncand 10595 . . . . . . . . 9 (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
331330adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
33243oveq2i 6804 . . . . . . . . . . 11 (𝐴 + 𝑇) = (𝐴 + (𝐵𝐴))
333332a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐴 + 𝑇) = (𝐴 + (𝐵𝐴)))
33440recnd 10270 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
335329, 334pncan3d 10597 . . . . . . . . . . 11 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
336335adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐴 + (𝐵𝐴)) = 𝐵)
337 id 22 . . . . . . . . . . . 12 ((𝐸𝑋) = 𝐵 → (𝐸𝑋) = 𝐵)
338337eqcomd 2777 . . . . . . . . . . 11 ((𝐸𝑋) = 𝐵𝐵 = (𝐸𝑋))
339338adantl 467 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝐵 = (𝐸𝑋))
340333, 336, 3393eqtrrd 2810 . . . . . . . . 9 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐸𝑋) = (𝐴 + 𝑇))
341340oveq1d 6808 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐸𝑋) − 𝑇) = ((𝐴 + 𝑇) − 𝑇))
34233adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = 𝐴)
343331, 341, 3423eqtr4rd 2816 . . . . . . 7 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = ((𝐸𝑋) − 𝑇))
344343oveq1d 6808 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) = (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)))
345139recnd 10270 . . . . . . . 8 (𝜑 → (𝐸𝑋) ∈ ℂ)
346345, 217, 225nnncan2d 10629 . . . . . . 7 (𝜑 → (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)) = ((𝐸𝑋) − (𝑍𝑋)))
347346adantr 466 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)) = ((𝐸𝑋) − (𝑍𝑋)))
348219adantr 466 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
349344, 347, 3483eqtrrd 2810 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝑋 = ((𝑄‘0) − ((𝑍𝑋) − 𝑇)))
35033, 38eqeltrd 2850 . . . . . . 7 (𝜑 → (𝑄‘0) ∈ ℝ)
3513nngt0d 11266 . . . . . . . . . 10 (𝜑 → 0 < 𝑀)
352 fzolb 12684 . . . . . . . . . 10 (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
353315, 316, 351, 352syl3anbrc 1428 . . . . . . . . 9 (𝜑 → 0 ∈ (0..^𝑀))
354 0re 10242 . . . . . . . . . 10 0 ∈ ℝ
355 eleq1 2838 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
356355anbi2d 614 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
357 fveq2 6332 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
358 oveq1 6800 . . . . . . . . . . . . . 14 (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
359358fveq2d 6336 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
360357, 359breq12d 4799 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
361356, 360imbi12d 333 . . . . . . . . . . 11 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
362361, 152vtoclg 3417 . . . . . . . . . 10 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
363354, 362ax-mp 5 . . . . . . . . 9 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
364353, 363mpdan 667 . . . . . . . 8 (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
365 0p1e1 11334 . . . . . . . . . 10 (0 + 1) = 1
366365fveq2i 6335 . . . . . . . . 9 (𝑄‘(0 + 1)) = (𝑄‘1)
367366a1i 11 . . . . . . . 8 (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
368364, 367breqtrd 4812 . . . . . . 7 (𝜑 → (𝑄‘0) < (𝑄‘1))
369350, 325, 326, 368ltsub1dd 10841 . . . . . 6 (𝜑 → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
370369adantr 466 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
371349, 370eqbrtrd 4808 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
372 elioore 12410 . . . . . . . . 9 (𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) → 𝑦 ∈ ℝ)
373135eqcomd 2777 . . . . . . . . . . . . . . . 16 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = (𝑍𝑋))
374373negeqd 10477 . . . . . . . . . . . . . . 15 (𝜑 → -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -(𝑍𝑋))
375226, 374eqtrd 2805 . . . . . . . . . . . . . 14 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -(𝑍𝑋))
376225mulid2d 10260 . . . . . . . . . . . . . 14 (𝜑 → (1 · 𝑇) = 𝑇)
377375, 376oveq12d 6811 . . . . . . . . . . . . 13 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)) = (-(𝑍𝑋) + 𝑇))
378224negcld 10581 . . . . . . . . . . . . . 14 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
379 1cnd 10258 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
380378, 379, 225adddird 10267 . . . . . . . . . . . . 13 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇) = ((-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)))
381217, 225negsubdid 10609 . . . . . . . . . . . . 13 (𝜑 → -((𝑍𝑋) − 𝑇) = (-(𝑍𝑋) + 𝑇))
382377, 380, 3813eqtr4d 2815 . . . . . . . . . . . 12 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇) = -((𝑍𝑋) − 𝑇))
383382oveq2d 6809 . . . . . . . . . . 11 (𝜑 → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)))
384383adantr 466 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)))
385326adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → ((𝑍𝑋) − 𝑇) ∈ ℝ)
386229, 385readdcld 10271 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
387386recnd 10270 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℂ)
388385recnd 10270 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((𝑍𝑋) − 𝑇) ∈ ℂ)
389387, 388negsubd 10600 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) − ((𝑍𝑋) − 𝑇)))
390235, 388pncand 10595 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) − ((𝑍𝑋) − 𝑇)) = 𝑦)
391384, 389, 3903eqtrrd 2810 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
392372, 391sylan2 580 . . . . . . . 8 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
393392adantlr 694 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
394 simpll 750 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝜑)
395367eqcomd 2777 . . . . . . . . . . . 12 (𝜑 → (𝑄‘1) = (𝑄‘(0 + 1)))
396395oveq2d 6809 . . . . . . . . . . 11 (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
397357, 359oveq12d 6811 . . . . . . . . . . . . . . . 16 (𝑖 = 0 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
398397sseq1d 3781 . . . . . . . . . . . . . . 15 (𝑖 = 0 → (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷 ↔ ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
399356, 398imbi12d 333 . . . . . . . . . . . . . 14 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)))
400399, 241vtoclg 3417 . . . . . . . . . . . . 13 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
401354, 400ax-mp 5 . . . . . . . . . . . 12 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
402353, 401mpdan 667 . . . . . . . . . . 11 (𝜑 → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
403396, 402eqsstrd 3788 . . . . . . . . . 10 (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
404403ad2antrr 705 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
40533, 39eqeltrd 2850 . . . . . . . . . . 11 (𝜑 → (𝑄‘0) ∈ ℝ*)
406405ad2antrr 705 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) ∈ ℝ*)
407325rexrd 10291 . . . . . . . . . . 11 (𝜑 → (𝑄‘1) ∈ ℝ*)
408407ad2antrr 705 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ*)
409372, 386sylan2 580 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
410409adantlr 694 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
411345, 216, 217subaddd 10612 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐸𝑋) − 𝑋) = (𝑍𝑋) ↔ (𝑋 + (𝑍𝑋)) = (𝐸𝑋)))
412272, 411mpbird 247 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑋) − 𝑋) = (𝑍𝑋))
413 oveq1 6800 . . . . . . . . . . . . . . . 16 ((𝐸𝑋) = 𝐵 → ((𝐸𝑋) − 𝑋) = (𝐵𝑋))
414412, 413sylan9req 2826 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑍𝑋) = (𝐵𝑋))
415414oveq1d 6808 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑍𝑋) − 𝑇) = ((𝐵𝑋) − 𝑇))
416415oveq2d 6809 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋 + ((𝑍𝑋) − 𝑇)) = (𝑋 + ((𝐵𝑋) − 𝑇)))
417130recnd 10270 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝑋) ∈ ℂ)
418216, 417, 225addsubassd 10614 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑋 + ((𝐵𝑋) − 𝑇)))
419418eqcomd 2777 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + ((𝐵𝑋) − 𝑇)) = ((𝑋 + (𝐵𝑋)) − 𝑇))
420419adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋 + ((𝐵𝑋) − 𝑇)) = ((𝑋 + (𝐵𝑋)) − 𝑇))
421334, 225, 329subsub23d 40017 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝑇) = 𝐴 ↔ (𝐵𝐴) = 𝑇))
42258, 421mpbird 247 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵𝑇) = 𝐴)
423216, 334pncan3d 10597 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 + (𝐵𝑋)) = 𝐵)
424423oveq1d 6808 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝐵𝑇))
425422, 424, 333eqtr4d 2815 . . . . . . . . . . . . . 14 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑄‘0))
426425adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑄‘0))
427416, 420, 4263eqtrrd 2810 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = (𝑋 + ((𝑍𝑋) − 𝑇)))
428427adantr 466 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) = (𝑋 + ((𝑍𝑋) − 𝑇)))
42974adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 ∈ ℝ)
430372adantl 467 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 ∈ ℝ)
431326adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑍𝑋) − 𝑇) ∈ ℝ)
432254adantr 466 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 ∈ ℝ*)
433327rexrd 10291 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*)
434433adantr 466 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*)
435 simpr 471 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
436 ioogtlb 40238 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ* ∧ ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 < 𝑦)
437432, 434, 435, 436syl3anc 1476 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 < 𝑦)
438429, 430, 431, 437ltadd1dd 10840 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑋 + ((𝑍𝑋) − 𝑇)) < (𝑦 + ((𝑍𝑋) − 𝑇)))
439438adantlr 694 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑋 + ((𝑍𝑋) − 𝑇)) < (𝑦 + ((𝑍𝑋) − 𝑇)))
440428, 439eqbrtrd 4808 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) < (𝑦 + ((𝑍𝑋) − 𝑇)))
441 iooltub 40255 . . . . . . . . . . . . 13 ((𝑋 ∈ ℝ* ∧ ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
442432, 434, 435, 441syl3anc 1476 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
443325adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ)
444430, 431, 443ltaddsubd 10829 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1) ↔ 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
445442, 444mpbird 247 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1))
446445adantlr 694 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1))
447406, 408, 410, 440, 446eliood 40241 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ((𝑄‘0)(,)(𝑄‘1)))
448404, 447sseldd 3753 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷)
449132znegcld 11686 . . . . . . . . . 10 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
450449peano2zd 11687 . . . . . . . . 9 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)
451450ad2antrr 705 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)
452 ovex 6823 . . . . . . . . 9 (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ V
453 eleq1 2838 . . . . . . . . . . 11 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (𝑘 ∈ ℤ ↔ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ))
4544533anbi3d 1553 . . . . . . . . . 10 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)))
455 oveq1 6800 . . . . . . . . . . . 12 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (𝑘 · 𝑇) = ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇))
456455oveq2d 6809 . . . . . . . . . . 11 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
457456eleq1d 2835 . . . . . . . . . 10 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷))
458454, 457imbi12d 333 . . . . . . . . 9 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)))
459 ovex 6823 . . . . . . . . . 10 (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ V
460 eleq1 2838 . . . . . . . . . . . 12 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (𝑥𝐷 ↔ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷))
4614603anbi2d 1552 . . . . . . . . . . 11 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ)))
462 oveq1 6800 . . . . . . . . . . . 12 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)))
463462eleq1d 2835 . . . . . . . . . . 11 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷))
464461, 463imbi12d 333 . . . . . . . . . 10 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)))
465459, 464, 298vtocl 3410 . . . . . . . . 9 ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)
466452, 458, 465vtocl 3410 . . . . . . . 8 ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
467394, 448, 451, 466syl3anc 1476 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
468393, 467eqeltrd 2850 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦𝐷)
469468ralrimiva 3115 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))𝑦𝐷)
470 dfss3 3741 . . . . 5 ((𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))𝑦𝐷)
471469, 470sylibr 224 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)
472 breq2 4790 . . . . . 6 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → (𝑋 < 𝑦𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
473 oveq2 6801 . . . . . . 7 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
474473sseq1d 3781 . . . . . 6 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷))
475472, 474anbi12d 616 . . . . 5 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)))
476475rspcev 3460 . . . 4 ((((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ ∧ (𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
477328, 371, 471, 476syl12anc 1474 . . 3 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
47815adantlr 694 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
479 simp2 1131 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (0...𝑀))
480253ad2ant2 1128 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℝ)
481943ad2ant2 1128 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℝ)
482963ad2ant2 1128 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗𝑀)
483 id 22 . . . . . . . . . . . . . . . . . 18 ((𝑄𝑗) = (𝐸𝑋) → (𝑄𝑗) = (𝐸𝑋))
484483eqcomd 2777 . . . . . . . . . . . . . . . . 17 ((𝑄𝑗) = (𝐸𝑋) → (𝐸𝑋) = (𝑄𝑗))
485484adantr 466 . . . . . . . . . . . . . . . 16 (((𝑄𝑗) = (𝐸𝑋) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = (𝑄𝑗))
4864853ad2antl3 1202 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = (𝑄𝑗))
487 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑀 = 𝑗 → (𝑄𝑀) = (𝑄𝑗))
488487eqcomd 2777 . . . . . . . . . . . . . . . 16 (𝑀 = 𝑗 → (𝑄𝑗) = (𝑄𝑀))
489488adantl 467 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝑄𝑗) = (𝑄𝑀))
490180ad2antrr 705 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → (𝑄𝑀) = 𝐵)
4914903ad2antl1 1200 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝑄𝑀) = 𝐵)
492486, 489, 4913eqtrd 2809 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = 𝐵)
493 neneq 2949 . . . . . . . . . . . . . . . 16 ((𝐸𝑋) ≠ 𝐵 → ¬ (𝐸𝑋) = 𝐵)
494493ad2antlr 706 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → ¬ (𝐸𝑋) = 𝐵)
4954943ad2antl1 1200 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → ¬ (𝐸𝑋) = 𝐵)
496492, 495pm2.65da 818 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ¬ 𝑀 = 𝑗)
497496neqned 2950 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀𝑗)
498480, 481, 482, 497leneltd 10393 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 < 𝑀)
499 elfzfzo 40006 . . . . . . . . . . 11 (𝑗 ∈ (0..^𝑀) ↔ (𝑗 ∈ (0...𝑀) ∧ 𝑗 < 𝑀))
500479, 498, 499sylanbrc 572 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (0..^𝑀))
501117adantlr 694 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
5025013adant3 1126 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ∈ ℝ*)
503 simp1l 1239 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
504101adantr 466 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
505 fzofzp1 12773 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
506505adantl 467 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
507504, 506ffvelrnd 6503 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
508507rexrd 10291 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ*)
509503, 500, 508syl2anc 573 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 + 1)) ∈ ℝ*)
5101413adant1r 1187 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
51137, 160eqbrtrd 4808 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
512511adantlr 694 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
5135123adant2 1125 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
5144843ad2ant3 1129 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
515 eleq1 2838 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
516515anbi2d 614 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑𝑗 ∈ (0..^𝑀))))
517 fveq2 6332 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑄𝑖) = (𝑄𝑗))
518 oveq1 6800 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
519518fveq2d 6336 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
520517, 519breq12d 4799 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄𝑗) < (𝑄‘(𝑗 + 1))))
521516, 520imbi12d 333 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))))
522521, 152chvarv 2425 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))
523503, 500, 522syl2anc 573 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))
524514, 523eqbrtrd 4808 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) < (𝑄‘(𝑗 + 1)))
525502, 509, 510, 513, 524elicod 12429 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1))))
526517, 519oveq12d 6811 . . . . . . . . . . . 12 (𝑖 = 𝑗 → ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1))))
527526eleq2d 2836 . . . . . . . . . . 11 (𝑖 = 𝑗 → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1)))))
528527rspcev 3460 . . . . . . . . . 10 ((𝑗 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
529500, 525, 528syl2anc 573 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
5305293exp 1112 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))))
531530adantr 466 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))))
532531rexlimdv 3178 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
533478, 532mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
534 ioossico 12468 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))
535 simpr 471 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
536534, 535sseldi 3750 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
537536ex 397 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
538537adantlr 694 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
539538reximdva 3165 . . . . . . 7 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
540190, 539mpd 15 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
541540adantlr 694 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
542533, 541pm2.61dan 814 . . . 4 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
543208, 250resubcld 10660 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
5445433adant3 1126 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
545219eqcomd 2777 . . . . . . . . . 10 (𝜑𝑋 = ((𝐸𝑋) − (𝑍𝑋)))
5465453ad2ant1 1127 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 = ((𝐸𝑋) − (𝑍𝑋)))
5471393ad2ant1 1127 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
5482083adant3 1126 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
5491363ad2ant1 1127 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
550200rexrd 10291 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
5515503adant3 1126 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
5522093adant3 1126 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
553 simp3 1132 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
554 icoltub 40253 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < (𝑄‘(𝑖 + 1)))
555551, 552, 553, 554syl3anc 1476 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < (𝑄‘(𝑖 + 1)))
556547, 548, 549, 555ltsub1dd 10841 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝐸𝑋) − (𝑍𝑋)) < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
557546, 556eqbrtrd 4808 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
558 elioore 12410 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) → 𝑦 ∈ ℝ)
559558, 237sylan2 580 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
5605593ad2antl1 1200 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
561 simpl1 1227 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝜑)
5622413adant3 1126 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
563562adantr 466 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
564551adantr 466 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ∈ ℝ*)
565552adantr 466 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
566558adantl 467 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ ℝ)
567136adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑍𝑋) ∈ ℝ)
568566, 567readdcld 10271 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
5695683ad2antl1 1200 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
5702003adant3 1126 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
571570adantr 466 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ∈ ℝ)
572561, 139syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) ∈ ℝ)
573 icogelb 12430 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ≤ (𝐸𝑋))
574551, 552, 553, 573syl3anc 1476 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ≤ (𝐸𝑋))
575574adantr 466 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ≤ (𝐸𝑋))
576138ad2antrr 705 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
57774ad2antrr 705 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 ∈ ℝ)
578558adantl 467 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ ℝ)
579136ad2antrr 705 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑍𝑋) ∈ ℝ)
580254ad2antrr 705 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 ∈ ℝ*)
581543rexrd 10291 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*)
582581adantr 466 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*)
583 simpr 471 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
584 ioogtlb 40238 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 < 𝑦)
585580, 582, 583, 584syl3anc 1476 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 < 𝑦)
586577, 578, 579, 585ltadd1dd 10840 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑋 + (𝑍𝑋)) < (𝑦 + (𝑍𝑋)))
587576, 586eqbrtrd 4808 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) < (𝑦 + (𝑍𝑋)))
5885873adantl3 1173 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) < (𝑦 + (𝑍𝑋)))
589571, 572, 569, 575, 588lelttrd 10397 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
590543adantr 466 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
591 iooltub 40255 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
592580, 582, 583, 591syl3anc 1476 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
593578, 590, 579, 592ltadd1dd 10840 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)))
594208recnd 10270 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
595217adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℂ)
596594, 595npcand 10598 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄‘(𝑖 + 1)))
597596adantr 466 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄‘(𝑖 + 1)))
598593, 597breqtrd 4812 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
5995983adantl3 1173 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
600564, 565, 569, 589, 599eliood 40241 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
601563, 600sseldd 3753 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
602561, 449syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
603561, 601, 602, 300syl3anc 1476 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
604560, 603eqeltrd 2850 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦𝐷)
605604ralrimiva 3115 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))𝑦𝐷)
606 dfss3 3741 . . . . . . . . 9 ((𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))𝑦𝐷)
607605, 606sylibr 224 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)
608 breq2 4790 . . . . . . . . . 10 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → (𝑋 < 𝑦𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
609 oveq2 6801 . . . . . . . . . . 11 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
610609sseq1d 3781 . . . . . . . . . 10 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷))
611608, 610anbi12d 616 . . . . . . . . 9 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)))
612611rspcev 3460 . . . . . . . 8 ((((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ ∧ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
613544, 557, 607, 612syl12anc 1474 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
6146133exp 1112 . . . . . 6 (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
615614adantr 466 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
616615rexlimdv 3178 . . . 4 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
617542, 616mpd 15 . . 3 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
618477, 617pm2.61dane 3030 . 2 (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
619314, 618jca 501 1 (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  wss 3723   class class class wbr 4786  cmpt 4863  ran crn 5250   Fn wfn 6026  wf 6027  cfv 6031  (class class class)co 6793  𝑚 cmap 8009  supcsup 8502  cc 10136  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143  *cxr 10275   < clt 10276  cle 10277  cmin 10468  -cneg 10469   / cdiv 10886  cn 11222  cz 11579  cuz 11888  (,)cioo 12380  (,]cioc 12381  [,)cico 12382  [,]cicc 12383  ...cfz 12533  ..^cfzo 12673  cfl 12799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-er 7896  df-map 8011  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8504  df-inf 8505  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-n0 11495  df-z 11580  df-uz 11889  df-rp 12036  df-ioo 12384  df-ioc 12385  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-fl 12801
This theorem is referenced by:  fourierdlem113  40953
  Copyright terms: Public domain W3C validator