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 40844
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 473 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ran 𝑄)
2 fourierdlem41.q . . . . . . . . . . 11 (𝜑𝑄 ∈ (𝑃𝑀))
3 fourierdlem41.m . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
4 fourierdlem41.p . . . . . . . . . . . . 13 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
54fourierdlem2 40805 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
63, 5syl 17 . . . . . . . . . . 11 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
72, 6mpbid 223 . . . . . . . . . 10 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
87simpld 484 . . . . . . . . 9 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
9 elmapi 8114 . . . . . . . . 9 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10 ffn 6256 . . . . . . . . 9 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
118, 9, 103syl 18 . . . . . . . 8 (𝜑𝑄 Fn (0...𝑀))
1211adantr 468 . . . . . . 7 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
13 fvelrnb 6464 . . . . . . 7 (𝑄 Fn (0...𝑀) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
1412, 13syl 17 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
151, 14mpbid 223 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
16 0zd 11655 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ∈ ℤ)
17 elfzelz 12565 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18173ad2ant2 1157 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℤ)
19 1zzd 11674 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ∈ ℤ)
2018, 19zsubcld 11753 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℤ)
21 simpll 774 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝜑)
22 elfzle1 12567 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
2322anim1i 604 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗))
24 0red 10328 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 ∈ ℝ)
2517zred 11748 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
2625adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 ∈ ℝ)
2724, 26eqleltd 10466 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 = 𝑗 ↔ (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗)))
2823, 27mpbird 248 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 = 𝑗)
2928eqcomd 2812 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
3029adantll 696 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
31 fveq2 6408 . . . . . . . . . . . . . . . 16 (𝑗 = 0 → (𝑄𝑗) = (𝑄‘0))
327simprld 779 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
3332simpld 484 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
3431, 33sylan9eqr 2862 . . . . . . . . . . . . . . 15 ((𝜑𝑗 = 0) → (𝑄𝑗) = 𝐴)
3521, 30, 34syl2anc 575 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) = 𝐴)
36353adantl3 1202 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) = 𝐴)
37 simpr 473 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
38 fourierdlem41.a . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ)
3938rexrd 10374 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ*)
40 fourierdlem41.b . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ ℝ)
4140rexrd 10374 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℝ*)
42 fourierdlem41.altb . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 < 𝐵)
43 fourierdlem41.t . . . . . . . . . . . . . . . . . . . . . . 23 𝑇 = (𝐵𝐴)
44 eqid 2806 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
4538, 40, 42, 43, 44fourierdlem4 40807 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵))
46 fourierdlem41.e . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥)))
4746a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))))
48 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
4940adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
5049, 48resubcld 10743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → (𝐵𝑥) ∈ ℝ)
5140, 38resubcld 10743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝐵𝐴) ∈ ℝ)
5243, 51syl5eqel 2889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝑇 ∈ ℝ)
5352adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
54 0red 10328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 0 ∈ ℝ)
5538, 40posdifd 10899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
5642, 55mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → 0 < (𝐵𝐴))
5743eqcomi 2815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝐵𝐴) = 𝑇
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (𝐵𝐴) = 𝑇)
5956, 58breqtrd 4870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 0 < 𝑇)
6054, 59gtned 10457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝑇 ≠ 0)
6160adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → 𝑇 ≠ 0)
6250, 53, 61redivcld 11138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑥 ∈ ℝ) → ((𝐵𝑥) / 𝑇) ∈ ℝ)
6362flcld 12823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ)
6463zred 11748 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℝ)
6564, 53remulcld 10355 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ ℝ) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
66 fourierdlem41.z . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6766fvmpt2 6512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6848, 65, 67syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ ℝ) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6968oveq2d 6890 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ ℝ) → (𝑥 + (𝑍𝑥)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
7069mpteq2dva 4938 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
7147, 70eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
7271feq1d 6241 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐸:ℝ⟶(𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵)))
7345, 72mpbird 248 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
74 fourierdlem41.x . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ)
7573, 74ffvelrnd 6582 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸𝑋) ∈ (𝐴(,]𝐵))
76 iocgtlb 40208 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
7739, 41, 75, 76syl3anc 1483 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 < (𝐸𝑋))
7838, 77gtned 10457 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐸𝑋) ≠ 𝐴)
7978adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≠ 𝐴)
8037, 79eqnetrd 3045 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≠ 𝐴)
8180adantr 468 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) ≠ 𝐴)
82813adantl2 1201 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) ≠ 𝐴)
8382neneqd 2983 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → ¬ (𝑄𝑗) = 𝐴)
8436, 83condan 843 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 < 𝑗)
85 zltlem1 11696 . . . . . . . . . . . . 13 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
8616, 18, 85syl2anc 575 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
8784, 86mpbid 223 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ (𝑗 − 1))
88 eluz2 11910 . . . . . . . . . . 11 ((𝑗 − 1) ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ ∧ 0 ≤ (𝑗 − 1)))
8916, 20, 87, 88syl3anbrc 1436 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (ℤ‘0))
90 elfzel2 12563 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
91903ad2ant2 1157 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℤ)
92 1red 10326 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 1 ∈ ℝ)
9325, 92resubcld 10743 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
9490zred 11748 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
9525ltm1d 11241 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
96 elfzle2 12568 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → 𝑗𝑀)
9793, 25, 94, 95, 96ltletrd 10482 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
98973ad2ant2 1157 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) < 𝑀)
99 elfzo2 12697 . . . . . . . . . 10 ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
10089, 91, 98, 99syl3anbrc 1436 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
1018, 9syl 17 . . . . . . . . . . . . 13 (𝜑𝑄:(0...𝑀)⟶ℝ)
1021013ad2ant1 1156 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
10316, 91, 203jca 1151 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ))
10493, 94, 97ltled 10470 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
1051043ad2ant2 1157 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ≤ 𝑀)
106103, 87, 105jca32 507 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
107 elfz2 12556 . . . . . . . . . . . . 13 ((𝑗 − 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
108106, 107sylibr 225 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
109102, 108ffvelrnd 6582 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
110109rexrd 10374 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
11125recnd 10353 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
112 1cnd 10320 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
113111, 112npcand 10681 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
114113fveq2d 6412 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
115114adantl 469 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
116101ffvelrnda 6581 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ)
117116rexrd 10374 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
118115, 117eqeltrd 2885 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ*)
1191183adant3 1155 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ*)
120 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋𝑥 = 𝑋)
121 fveq2 6408 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑍𝑥) = (𝑍𝑋))
122120, 121oveq12d 6892 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
123122adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑥 = 𝑋) → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
12466a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
125 oveq2 6882 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
126125oveq1d 6889 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑋) / 𝑇))
127126fveq2d 6412 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑋) / 𝑇)))
128127oveq1d 6889 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
129128adantl 469 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 = 𝑋) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
13040, 74resubcld 10743 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵𝑋) ∈ ℝ)
131130, 52, 60redivcld 11138 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐵𝑋) / 𝑇) ∈ ℝ)
132131flcld 12823 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
133132zred 11748 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℝ)
134133, 52remulcld 10355 . . . . . . . . . . . . . . . . 17 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
135124, 129, 74, 134fvmptd 6509 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑍𝑋) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
136135, 134eqeltrd 2885 . . . . . . . . . . . . . . 15 (𝜑 → (𝑍𝑋) ∈ ℝ)
13774, 136readdcld 10354 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℝ)
13847, 123, 74, 137fvmptd 6509 . . . . . . . . . . . . 13 (𝜑 → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
139138, 137eqeltrd 2885 . . . . . . . . . . . 12 (𝜑 → (𝐸𝑋) ∈ ℝ)
140139rexrd 10374 . . . . . . . . . . 11 (𝜑 → (𝐸𝑋) ∈ ℝ*)
1411403ad2ant1 1156 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
142 simp1 1159 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
143 ovex 6906 . . . . . . . . . . . . . 14 (𝑗 − 1) ∈ V
144 eleq1 2873 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
145144anbi2d 616 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 − 1) → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
146 fveq2 6408 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑄𝑖) = (𝑄‘(𝑗 − 1)))
147 oveq1 6881 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
148147fveq2d 6412 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
149146, 148breq12d 4857 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 − 1) → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
150145, 149imbi12d 335 . . . . . . . . . . . . . 14 (𝑖 = (𝑗 − 1) → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
1517simprrd 781 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
152151r19.21bi 3120 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
153143, 150, 152vtocl 3452 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
154142, 100, 153syl2anc 575 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
1551143ad2ant2 1157 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
156154, 155breqtrd 4870 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄𝑗))
157 simp3 1161 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
158156, 157breqtrd 4870 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸𝑋))
159139leidd 10879 . . . . . . . . . . . . . 14 (𝜑 → (𝐸𝑋) ≤ (𝐸𝑋))
160159adantr 468 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝐸𝑋))
16137eqcomd 2812 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
162160, 161breqtrd 4870 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
1631623adant2 1154 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
164113eqcomd 2812 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
165164fveq2d 6412 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
1661653ad2ant2 1157 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
167163, 166breqtrd 4870 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄‘((𝑗 − 1) + 1)))
168110, 119, 141, 158, 167eliocd 40214 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
169146, 148oveq12d 6892 . . . . . . . . . . 11 (𝑖 = (𝑗 − 1) → ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
170169eleq2d 2871 . . . . . . . . . 10 (𝑖 = (𝑗 − 1) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
171170rspcev 3502 . . . . . . . . 9 (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
172100, 168, 171syl2anc 575 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
1731723exp 1141 . . . . . . 7 (𝜑 → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))))
174173adantr 468 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))))
175174rexlimdv 3218 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
17615, 175mpd 15 . . . 4 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
1773adantr 468 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
178101adantr 468 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
179 iocssicc 12480 . . . . . . . 8 ((𝑄‘0)(,](𝑄𝑀)) ⊆ ((𝑄‘0)[,](𝑄𝑀))
18032simprd 485 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = 𝐵)
18133, 180oveq12d 6892 . . . . . . . . 9 (𝜑 → ((𝑄‘0)(,](𝑄𝑀)) = (𝐴(,]𝐵))
18275, 181eleqtrrd 2888 . . . . . . . 8 (𝜑 → (𝐸𝑋) ∈ ((𝑄‘0)(,](𝑄𝑀)))
183179, 182sseldi 3796 . . . . . . 7 (𝜑 → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
184183adantr 468 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
185 simpr 473 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ¬ (𝐸𝑋) ∈ ran 𝑄)
186 fveq2 6408 . . . . . . . . 9 (𝑘 = 𝑗 → (𝑄𝑘) = (𝑄𝑗))
187186breq1d 4854 . . . . . . . 8 (𝑘 = 𝑗 → ((𝑄𝑘) < (𝐸𝑋) ↔ (𝑄𝑗) < (𝐸𝑋)))
188187cbvrabv 3389 . . . . . . 7 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}
189188supeq1i 8592 . . . . . 6 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}, ℝ, < )
190177, 178, 184, 185, 189fourierdlem25 40828 . . . . 5 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
191 ioossioc 40197 . . . . . . . 8 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))
192191a1i 11 . . . . . . 7 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
193192sseld 3797 . . . . . 6 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
194193reximdva 3204 . . . . 5 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
195190, 194mpd 15 . . . 4 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
196176, 195pm2.61dan 838 . . 3 (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
197101adantr 468 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
198 elfzofz 12709 . . . . . . . . . 10 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
199198adantl 469 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
200197, 199ffvelrnd 6582 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
2012003adant3 1155 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
2021363ad2ant1 1156 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
203201, 202resubcld 10743 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
2041393ad2ant1 1156 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
205201rexrd 10374 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
206 fzofzp1 12789 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
207206adantl 469 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
208197, 207ffvelrnd 6582 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209208rexrd 10374 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2102093adant3 1155 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
211 simp3 1161 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
212 iocgtlb 40208 . . . . . . . . 9 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
213205, 210, 211, 212syl3anc 1483 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
214201, 204, 202, 213ltsub1dd 10924 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < ((𝐸𝑋) − (𝑍𝑋)))
215138oveq1d 6889 . . . . . . . . 9 (𝜑 → ((𝐸𝑋) − (𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)))
21674recnd 10353 . . . . . . . . . 10 (𝜑𝑋 ∈ ℂ)
217136recnd 10353 . . . . . . . . . 10 (𝜑 → (𝑍𝑋) ∈ ℂ)
218216, 217pncand 10678 . . . . . . . . 9 (𝜑 → ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑋)
219215, 218eqtrd 2840 . . . . . . . 8 (𝜑 → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
2202193ad2ant1 1156 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
221214, 220breqtrd 4870 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑋)
222 elioore 12423 . . . . . . . . . . 11 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
223135oveq2d 6890 . . . . . . . . . . . . . 14 (𝜑 → (𝑦 + (𝑍𝑋)) = (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
224133recnd 10353 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
22552recnd 10353 . . . . . . . . . . . . . . 15 (𝜑𝑇 ∈ ℂ)
226224, 225mulneg1d 10768 . . . . . . . . . . . . . 14 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
227223, 226oveq12d 6892 . . . . . . . . . . . . 13 (𝜑 → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
228227adantr 468 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
229 simpr 473 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
230134adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
231229, 230readdcld 10354 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
232231recnd 10353 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ ℂ)
233230recnd 10353 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
234232, 233negsubd 10683 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
235229recnd 10353 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
236235, 233pncand 10678 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = 𝑦)
237228, 234, 2363eqtrrd 2845 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
238222, 237sylan2 582 . . . . . . . . . 10 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
2392383ad2antl1 1229 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
240 simpl1 1235 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
241 fourierdlem41.qssd . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
2422413adant3 1155 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
243242adantr 468 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
244205adantr 468 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ*)
245210adantr 468 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
246222adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
247136adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
248246, 247readdcld 10354 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
2492483ad2antl1 1229 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
250136adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℝ)
251200, 250resubcld 10743 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
252251rexrd 10374 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
253252adantr 468 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
25474rexrd 10374 . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℝ*)
255254ad2antrr 708 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
256 simpr 473 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
257 ioogtlb 40201 . . . . . . . . . . . . . . 15 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
258253, 255, 256, 257syl3anc 1483 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
259200adantr 468 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ)
260136ad2antrr 708 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
261222adantl 469 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
262259, 260, 261ltsubaddd 10908 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑦 ↔ (𝑄𝑖) < (𝑦 + (𝑍𝑋))))
263258, 262mpbid 223 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
2642633adantl3 1202 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
265240, 139syl 17 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ∈ ℝ)
266208adantr 468 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2672663adantl3 1202 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
26874ad2antrr 708 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
269 iooltub 40217 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
270253, 255, 256, 269syl3anc 1483 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
271261, 268, 260, 270ltadd1dd 10923 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑋 + (𝑍𝑋)))
272138eqcomd 2812 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
273272ad2antrr 708 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
274271, 273breqtrd 4870 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
2752743adantl3 1202 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
276 iocleub 40209 . . . . . . . . . . . . . . 15 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
277205, 210, 211, 276syl3anc 1483 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
278277adantr 468 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
279249, 265, 267, 275, 278ltletrd 10482 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
280244, 245, 249, 264, 279eliood 40204 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
281243, 280sseldd 3799 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
282240, 131syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝐵𝑋) / 𝑇) ∈ ℝ)
283282flcld 12823 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
284283znegcld 11750 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
285 negex 10564 . . . . . . . . . . 11 -(⌊‘((𝐵𝑋) / 𝑇)) ∈ V
286 eleq1 2873 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
2872863anbi3d 1559 . . . . . . . . . . . 12 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
288 oveq1 6881 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
289288oveq2d 6890 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
290289eleq1d 2870 . . . . . . . . . . . 12 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
291287, 290imbi12d 335 . . . . . . . . . . 11 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
292 ovex 6906 . . . . . . . . . . . 12 (𝑦 + (𝑍𝑋)) ∈ V
293 eleq1 2873 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥𝐷 ↔ (𝑦 + (𝑍𝑋)) ∈ 𝐷))
2942933anbi2d 1558 . . . . . . . . . . . . 13 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ)))
295 oveq1 6881 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)))
296295eleq1d 2870 . . . . . . . . . . . . 13 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
297294, 296imbi12d 335 . . . . . . . . . . . 12 (𝑥 = (𝑦 + (𝑍𝑋)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
298 fourierdlem41.dper . . . . . . . . . . . 12 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
299292, 297, 298vtocl 3452 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
300285, 291, 299vtocl 3452 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
301240, 281, 284, 300syl3anc 1483 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
302239, 301eqeltrd 2885 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦𝐷)
303302ralrimiva 3154 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
304 dfss3 3787 . . . . . . 7 ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
305303, 304sylibr 225 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)
306 breq1 4847 . . . . . . . 8 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → (𝑦 < 𝑋 ↔ ((𝑄𝑖) − (𝑍𝑋)) < 𝑋))
307 oveq1 6881 . . . . . . . . 9 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → (𝑦(,)𝑋) = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
308307sseq1d 3829 . . . . . . . 8 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → ((𝑦(,)𝑋) ⊆ 𝐷 ↔ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷))
309306, 308anbi12d 618 . . . . . . 7 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → ((𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ↔ (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ∧ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)))
310309rspcev 3502 . . . . . 6 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ ∧ (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ∧ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
311203, 221, 305, 310syl12anc 856 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
3123113exp 1141 . . . 4 (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))))
313312rexlimdv 3218 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷)))
314196, 313mpd 15 . 2 (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
315 0zd 11655 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
3163nnzd 11747 . . . . . . . . . 10 (𝜑𝑀 ∈ ℤ)
317 1zzd 11674 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
318315, 316, 3173jca 1151 . . . . . . . . 9 (𝜑 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ))
319 0le1 10836 . . . . . . . . . 10 0 ≤ 1
320319a1i 11 . . . . . . . . 9 (𝜑 → 0 ≤ 1)
3213nnge1d 11349 . . . . . . . . 9 (𝜑 → 1 ≤ 𝑀)
322318, 320, 321jca32 507 . . . . . . . 8 (𝜑 → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
323 elfz2 12556 . . . . . . . 8 (1 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
324322, 323sylibr 225 . . . . . . 7 (𝜑 → 1 ∈ (0...𝑀))
325101, 324ffvelrnd 6582 . . . . . 6 (𝜑 → (𝑄‘1) ∈ ℝ)
326136, 52resubcld 10743 . . . . . 6 (𝜑 → ((𝑍𝑋) − 𝑇) ∈ ℝ)
327325, 326resubcld 10743 . . . . 5 (𝜑 → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ)
328327adantr 468 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ)
32938recnd 10353 . . . . . . . . . 10 (𝜑𝐴 ∈ ℂ)
330329, 225pncand 10678 . . . . . . . . 9 (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
331330adantr 468 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
33243oveq2i 6885 . . . . . . . . . . 11 (𝐴 + 𝑇) = (𝐴 + (𝐵𝐴))
333332a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐴 + 𝑇) = (𝐴 + (𝐵𝐴)))
33440recnd 10353 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
335329, 334pncan3d 10680 . . . . . . . . . . 11 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
336335adantr 468 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐴 + (𝐵𝐴)) = 𝐵)
337 id 22 . . . . . . . . . . . 12 ((𝐸𝑋) = 𝐵 → (𝐸𝑋) = 𝐵)
338337eqcomd 2812 . . . . . . . . . . 11 ((𝐸𝑋) = 𝐵𝐵 = (𝐸𝑋))
339338adantl 469 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝐵 = (𝐸𝑋))
340333, 336, 3393eqtrrd 2845 . . . . . . . . 9 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐸𝑋) = (𝐴 + 𝑇))
341340oveq1d 6889 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐸𝑋) − 𝑇) = ((𝐴 + 𝑇) − 𝑇))
34233adantr 468 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = 𝐴)
343331, 341, 3423eqtr4rd 2851 . . . . . . 7 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = ((𝐸𝑋) − 𝑇))
344343oveq1d 6889 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) = (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)))
345139recnd 10353 . . . . . . . 8 (𝜑 → (𝐸𝑋) ∈ ℂ)
346345, 217, 225nnncan2d 10712 . . . . . . 7 (𝜑 → (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)) = ((𝐸𝑋) − (𝑍𝑋)))
347346adantr 468 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)) = ((𝐸𝑋) − (𝑍𝑋)))
348219adantr 468 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
349344, 347, 3483eqtrrd 2845 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝑋 = ((𝑄‘0) − ((𝑍𝑋) − 𝑇)))
35033, 38eqeltrd 2885 . . . . . . 7 (𝜑 → (𝑄‘0) ∈ ℝ)
3513nngt0d 11350 . . . . . . . . . 10 (𝜑 → 0 < 𝑀)
352 fzolb 12700 . . . . . . . . . 10 (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
353315, 316, 351, 352syl3anbrc 1436 . . . . . . . . 9 (𝜑 → 0 ∈ (0..^𝑀))
354 0re 10327 . . . . . . . . . 10 0 ∈ ℝ
355 eleq1 2873 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
356355anbi2d 616 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
357 fveq2 6408 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
358 oveq1 6881 . . . . . . . . . . . . . 14 (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
359358fveq2d 6412 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
360357, 359breq12d 4857 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
361356, 360imbi12d 335 . . . . . . . . . . 11 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
362361, 152vtoclg 3459 . . . . . . . . . 10 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
363354, 362ax-mp 5 . . . . . . . . 9 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
364353, 363mpdan 670 . . . . . . . 8 (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
365 0p1e1 11414 . . . . . . . . . 10 (0 + 1) = 1
366365fveq2i 6411 . . . . . . . . 9 (𝑄‘(0 + 1)) = (𝑄‘1)
367366a1i 11 . . . . . . . 8 (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
368364, 367breqtrd 4870 . . . . . . 7 (𝜑 → (𝑄‘0) < (𝑄‘1))
369350, 325, 326, 368ltsub1dd 10924 . . . . . 6 (𝜑 → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
370369adantr 468 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
371349, 370eqbrtrd 4866 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
372 elioore 12423 . . . . . . . . 9 (𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) → 𝑦 ∈ ℝ)
373135eqcomd 2812 . . . . . . . . . . . . . . . 16 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = (𝑍𝑋))
374373negeqd 10560 . . . . . . . . . . . . . . 15 (𝜑 → -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -(𝑍𝑋))
375226, 374eqtrd 2840 . . . . . . . . . . . . . 14 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -(𝑍𝑋))
376225mulid2d 10343 . . . . . . . . . . . . . 14 (𝜑 → (1 · 𝑇) = 𝑇)
377375, 376oveq12d 6892 . . . . . . . . . . . . 13 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)) = (-(𝑍𝑋) + 𝑇))
378224negcld 10664 . . . . . . . . . . . . . 14 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
379 1cnd 10320 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
380378, 379, 225adddird 10350 . . . . . . . . . . . . 13 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇) = ((-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)))
381217, 225negsubdid 10692 . . . . . . . . . . . . 13 (𝜑 → -((𝑍𝑋) − 𝑇) = (-(𝑍𝑋) + 𝑇))
382377, 380, 3813eqtr4d 2850 . . . . . . . . . . . 12 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇) = -((𝑍𝑋) − 𝑇))
383382oveq2d 6890 . . . . . . . . . . 11 (𝜑 → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)))
384383adantr 468 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)))
385326adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → ((𝑍𝑋) − 𝑇) ∈ ℝ)
386229, 385readdcld 10354 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
387386recnd 10353 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℂ)
388385recnd 10353 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((𝑍𝑋) − 𝑇) ∈ ℂ)
389387, 388negsubd 10683 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) − ((𝑍𝑋) − 𝑇)))
390235, 388pncand 10678 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) − ((𝑍𝑋) − 𝑇)) = 𝑦)
391384, 389, 3903eqtrrd 2845 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
392372, 391sylan2 582 . . . . . . . 8 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
393392adantlr 697 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
394 simpll 774 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝜑)
395367eqcomd 2812 . . . . . . . . . . . 12 (𝜑 → (𝑄‘1) = (𝑄‘(0 + 1)))
396395oveq2d 6890 . . . . . . . . . . 11 (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
397357, 359oveq12d 6892 . . . . . . . . . . . . . . . 16 (𝑖 = 0 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
398397sseq1d 3829 . . . . . . . . . . . . . . 15 (𝑖 = 0 → (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷 ↔ ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
399356, 398imbi12d 335 . . . . . . . . . . . . . 14 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)))
400399, 241vtoclg 3459 . . . . . . . . . . . . 13 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
401354, 400ax-mp 5 . . . . . . . . . . . 12 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
402353, 401mpdan 670 . . . . . . . . . . 11 (𝜑 → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
403396, 402eqsstrd 3836 . . . . . . . . . 10 (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
404403ad2antrr 708 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
40533, 39eqeltrd 2885 . . . . . . . . . . 11 (𝜑 → (𝑄‘0) ∈ ℝ*)
406405ad2antrr 708 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) ∈ ℝ*)
407325rexrd 10374 . . . . . . . . . . 11 (𝜑 → (𝑄‘1) ∈ ℝ*)
408407ad2antrr 708 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ*)
409372, 386sylan2 582 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
410409adantlr 697 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
411345, 216, 217subaddd 10695 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐸𝑋) − 𝑋) = (𝑍𝑋) ↔ (𝑋 + (𝑍𝑋)) = (𝐸𝑋)))
412272, 411mpbird 248 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑋) − 𝑋) = (𝑍𝑋))
413 oveq1 6881 . . . . . . . . . . . . . . . 16 ((𝐸𝑋) = 𝐵 → ((𝐸𝑋) − 𝑋) = (𝐵𝑋))
414412, 413sylan9req 2861 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑍𝑋) = (𝐵𝑋))
415414oveq1d 6889 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑍𝑋) − 𝑇) = ((𝐵𝑋) − 𝑇))
416415oveq2d 6890 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋 + ((𝑍𝑋) − 𝑇)) = (𝑋 + ((𝐵𝑋) − 𝑇)))
417130recnd 10353 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝑋) ∈ ℂ)
418216, 417, 225addsubassd 10697 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑋 + ((𝐵𝑋) − 𝑇)))
419418eqcomd 2812 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + ((𝐵𝑋) − 𝑇)) = ((𝑋 + (𝐵𝑋)) − 𝑇))
420419adantr 468 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋 + ((𝐵𝑋) − 𝑇)) = ((𝑋 + (𝐵𝑋)) − 𝑇))
421334, 225, 329subsub23d 39981 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝑇) = 𝐴 ↔ (𝐵𝐴) = 𝑇))
42258, 421mpbird 248 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵𝑇) = 𝐴)
423216, 334pncan3d 10680 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 + (𝐵𝑋)) = 𝐵)
424423oveq1d 6889 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝐵𝑇))
425422, 424, 333eqtr4d 2850 . . . . . . . . . . . . . 14 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑄‘0))
426425adantr 468 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑄‘0))
427416, 420, 4263eqtrrd 2845 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = (𝑋 + ((𝑍𝑋) − 𝑇)))
428427adantr 468 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) = (𝑋 + ((𝑍𝑋) − 𝑇)))
42974adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 ∈ ℝ)
430372adantl 469 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 ∈ ℝ)
431326adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑍𝑋) − 𝑇) ∈ ℝ)
432254adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 ∈ ℝ*)
433327rexrd 10374 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*)
434433adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*)
435 simpr 473 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
436 ioogtlb 40201 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ* ∧ ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 < 𝑦)
437432, 434, 435, 436syl3anc 1483 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 < 𝑦)
438429, 430, 431, 437ltadd1dd 10923 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑋 + ((𝑍𝑋) − 𝑇)) < (𝑦 + ((𝑍𝑋) − 𝑇)))
439438adantlr 697 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑋 + ((𝑍𝑋) − 𝑇)) < (𝑦 + ((𝑍𝑋) − 𝑇)))
440428, 439eqbrtrd 4866 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) < (𝑦 + ((𝑍𝑋) − 𝑇)))
441 iooltub 40217 . . . . . . . . . . . . 13 ((𝑋 ∈ ℝ* ∧ ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
442432, 434, 435, 441syl3anc 1483 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
443325adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ)
444430, 431, 443ltaddsubd 10912 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1) ↔ 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
445442, 444mpbird 248 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1))
446445adantlr 697 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1))
447406, 408, 410, 440, 446eliood 40204 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ((𝑄‘0)(,)(𝑄‘1)))
448404, 447sseldd 3799 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷)
449132znegcld 11750 . . . . . . . . . 10 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
450449peano2zd 11751 . . . . . . . . 9 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)
451450ad2antrr 708 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)
452 ovex 6906 . . . . . . . . 9 (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ V
453 eleq1 2873 . . . . . . . . . . 11 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (𝑘 ∈ ℤ ↔ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ))
4544533anbi3d 1559 . . . . . . . . . 10 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)))
455 oveq1 6881 . . . . . . . . . . . 12 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (𝑘 · 𝑇) = ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇))
456455oveq2d 6890 . . . . . . . . . . 11 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
457456eleq1d 2870 . . . . . . . . . 10 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷))
458454, 457imbi12d 335 . . . . . . . . 9 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)))
459 ovex 6906 . . . . . . . . . 10 (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ V
460 eleq1 2873 . . . . . . . . . . . 12 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (𝑥𝐷 ↔ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷))
4614603anbi2d 1558 . . . . . . . . . . 11 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ)))
462 oveq1 6881 . . . . . . . . . . . 12 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)))
463462eleq1d 2870 . . . . . . . . . . 11 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷))
464461, 463imbi12d 335 . . . . . . . . . 10 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)))
465459, 464, 298vtocl 3452 . . . . . . . . 9 ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)
466452, 458, 465vtocl 3452 . . . . . . . 8 ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
467394, 448, 451, 466syl3anc 1483 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
468393, 467eqeltrd 2885 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦𝐷)
469468ralrimiva 3154 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))𝑦𝐷)
470 dfss3 3787 . . . . 5 ((𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))𝑦𝐷)
471469, 470sylibr 225 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)
472 breq2 4848 . . . . . 6 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → (𝑋 < 𝑦𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
473 oveq2 6882 . . . . . . 7 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
474473sseq1d 3829 . . . . . 6 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷))
475472, 474anbi12d 618 . . . . 5 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)))
476475rspcev 3502 . . . 4 ((((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ ∧ (𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
477328, 371, 471, 476syl12anc 856 . . 3 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
47815adantlr 697 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
479 simp2 1160 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (0...𝑀))
480253ad2ant2 1157 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℝ)
481943ad2ant2 1157 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℝ)
482963ad2ant2 1157 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗𝑀)
483 id 22 . . . . . . . . . . . . . . . . . 18 ((𝑄𝑗) = (𝐸𝑋) → (𝑄𝑗) = (𝐸𝑋))
484483eqcomd 2812 . . . . . . . . . . . . . . . . 17 ((𝑄𝑗) = (𝐸𝑋) → (𝐸𝑋) = (𝑄𝑗))
485484adantr 468 . . . . . . . . . . . . . . . 16 (((𝑄𝑗) = (𝐸𝑋) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = (𝑄𝑗))
4864853ad2antl3 1231 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = (𝑄𝑗))
487 fveq2 6408 . . . . . . . . . . . . . . . . 17 (𝑀 = 𝑗 → (𝑄𝑀) = (𝑄𝑗))
488487eqcomd 2812 . . . . . . . . . . . . . . . 16 (𝑀 = 𝑗 → (𝑄𝑗) = (𝑄𝑀))
489488adantl 469 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝑄𝑗) = (𝑄𝑀))
490180ad2antrr 708 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → (𝑄𝑀) = 𝐵)
4914903ad2antl1 1229 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝑄𝑀) = 𝐵)
492486, 489, 4913eqtrd 2844 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = 𝐵)
493 neneq 2984 . . . . . . . . . . . . . . . 16 ((𝐸𝑋) ≠ 𝐵 → ¬ (𝐸𝑋) = 𝐵)
494493ad2antlr 709 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → ¬ (𝐸𝑋) = 𝐵)
4954943ad2antl1 1229 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → ¬ (𝐸𝑋) = 𝐵)
496492, 495pm2.65da 842 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ¬ 𝑀 = 𝑗)
497496neqned 2985 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀𝑗)
498480, 481, 482, 497leneltd 10476 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 < 𝑀)
499 elfzfzo 39970 . . . . . . . . . . 11 (𝑗 ∈ (0..^𝑀) ↔ (𝑗 ∈ (0...𝑀) ∧ 𝑗 < 𝑀))
500479, 498, 499sylanbrc 574 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (0..^𝑀))
501117adantlr 697 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
5025013adant3 1155 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ∈ ℝ*)
503 simp1l 1247 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
504101adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
505 fzofzp1 12789 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
506505adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
507504, 506ffvelrnd 6582 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
508507rexrd 10374 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ*)
509503, 500, 508syl2anc 575 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 + 1)) ∈ ℝ*)
5101413adant1r 1216 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
51137, 160eqbrtrd 4866 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
512511adantlr 697 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
5135123adant2 1154 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
5144843ad2ant3 1158 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
515 eleq1 2873 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
516515anbi2d 616 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑𝑗 ∈ (0..^𝑀))))
517 fveq2 6408 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑄𝑖) = (𝑄𝑗))
518 oveq1 6881 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
519518fveq2d 6412 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
520517, 519breq12d 4857 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄𝑗) < (𝑄‘(𝑗 + 1))))
521516, 520imbi12d 335 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))))
522521, 152chvarv 2437 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))
523503, 500, 522syl2anc 575 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))
524514, 523eqbrtrd 4866 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) < (𝑄‘(𝑗 + 1)))
525502, 509, 510, 513, 524elicod 12442 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1))))
526517, 519oveq12d 6892 . . . . . . . . . . . 12 (𝑖 = 𝑗 → ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1))))
527526eleq2d 2871 . . . . . . . . . . 11 (𝑖 = 𝑗 → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1)))))
528527rspcev 3502 . . . . . . . . . 10 ((𝑗 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
529500, 525, 528syl2anc 575 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
5305293exp 1141 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))))
531530adantr 468 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))))
532531rexlimdv 3218 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
533478, 532mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
534 ioossico 12481 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))
535 simpr 473 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
536534, 535sseldi 3796 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
537536ex 399 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
538537adantlr 697 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
539538reximdva 3204 . . . . . . 7 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
540190, 539mpd 15 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
541540adantlr 697 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
542533, 541pm2.61dan 838 . . . 4 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
543208, 250resubcld 10743 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
5445433adant3 1155 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
545219eqcomd 2812 . . . . . . . . . 10 (𝜑𝑋 = ((𝐸𝑋) − (𝑍𝑋)))
5465453ad2ant1 1156 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 = ((𝐸𝑋) − (𝑍𝑋)))
5471393ad2ant1 1156 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
5482083adant3 1155 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
5491363ad2ant1 1156 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
550200rexrd 10374 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
5515503adant3 1155 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
5522093adant3 1155 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
553 simp3 1161 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
554 icoltub 40215 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < (𝑄‘(𝑖 + 1)))
555551, 552, 553, 554syl3anc 1483 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < (𝑄‘(𝑖 + 1)))
556547, 548, 549, 555ltsub1dd 10924 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝐸𝑋) − (𝑍𝑋)) < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
557546, 556eqbrtrd 4866 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
558 elioore 12423 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) → 𝑦 ∈ ℝ)
559558, 237sylan2 582 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
5605593ad2antl1 1229 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
561 simpl1 1235 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝜑)
5622413adant3 1155 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
563562adantr 468 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
564551adantr 468 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ∈ ℝ*)
565552adantr 468 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
566558adantl 469 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ ℝ)
567136adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑍𝑋) ∈ ℝ)
568566, 567readdcld 10354 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
5695683ad2antl1 1229 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
5702003adant3 1155 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
571570adantr 468 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ∈ ℝ)
572561, 139syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) ∈ ℝ)
573 icogelb 12443 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ≤ (𝐸𝑋))
574551, 552, 553, 573syl3anc 1483 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ≤ (𝐸𝑋))
575574adantr 468 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ≤ (𝐸𝑋))
576138ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
57774ad2antrr 708 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 ∈ ℝ)
578558adantl 469 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ ℝ)
579136ad2antrr 708 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑍𝑋) ∈ ℝ)
580254ad2antrr 708 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 ∈ ℝ*)
581543rexrd 10374 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*)
582581adantr 468 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*)
583 simpr 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
584 ioogtlb 40201 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 < 𝑦)
585580, 582, 583, 584syl3anc 1483 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 < 𝑦)
586577, 578, 579, 585ltadd1dd 10923 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑋 + (𝑍𝑋)) < (𝑦 + (𝑍𝑋)))
587576, 586eqbrtrd 4866 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) < (𝑦 + (𝑍𝑋)))
5885873adantl3 1202 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) < (𝑦 + (𝑍𝑋)))
589571, 572, 569, 575, 588lelttrd 10480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
590543adantr 468 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
591 iooltub 40217 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
592580, 582, 583, 591syl3anc 1483 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
593578, 590, 579, 592ltadd1dd 10923 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)))
594208recnd 10353 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
595217adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℂ)
596594, 595npcand 10681 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄‘(𝑖 + 1)))
597596adantr 468 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄‘(𝑖 + 1)))
598593, 597breqtrd 4870 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
5995983adantl3 1202 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
600564, 565, 569, 589, 599eliood 40204 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
601563, 600sseldd 3799 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
602561, 449syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
603561, 601, 602, 300syl3anc 1483 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
604560, 603eqeltrd 2885 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦𝐷)
605604ralrimiva 3154 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))𝑦𝐷)
606 dfss3 3787 . . . . . . . . 9 ((𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))𝑦𝐷)
607605, 606sylibr 225 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)
608 breq2 4848 . . . . . . . . . 10 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → (𝑋 < 𝑦𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
609 oveq2 6882 . . . . . . . . . . 11 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
610609sseq1d 3829 . . . . . . . . . 10 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷))
611608, 610anbi12d 618 . . . . . . . . 9 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)))
612611rspcev 3502 . . . . . . . 8 ((((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ ∧ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
613544, 557, 607, 612syl12anc 856 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
6146133exp 1141 . . . . . 6 (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
615614adantr 468 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
616615rexlimdv 3218 . . . 4 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
617542, 616mpd 15 . . 3 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
618477, 617pm2.61dane 3065 . 2 (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
619314, 618jca 503 1 (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wne 2978  wral 3096  wrex 3097  {crab 3100  wss 3769   class class class wbr 4844  cmpt 4923  ran crn 5312   Fn wfn 6096  wf 6097  cfv 6101  (class class class)co 6874  𝑚 cmap 8092  supcsup 8585  cc 10219  cr 10220  0cc0 10221  1c1 10222   + caddc 10224   · cmul 10226  *cxr 10358   < clt 10359  cle 10360  cmin 10551  -cneg 10552   / cdiv 10969  cn 11305  cz 11643  cuz 11904  (,)cioo 12393  (,]cioc 12394  [,)cico 12395  [,]cicc 12396  ...cfz 12549  ..^cfzo 12689  cfl 12815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298  ax-pre-sup 10299
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-er 7979  df-map 8094  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-sup 8587  df-inf 8588  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-div 10970  df-nn 11306  df-n0 11560  df-z 11644  df-uz 11905  df-rp 12047  df-ioo 12397  df-ioc 12398  df-ico 12399  df-icc 12400  df-fz 12550  df-fzo 12690  df-fl 12817
This theorem is referenced by:  fourierdlem113  40915
  Copyright terms: Public domain W3C validator