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 39693
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 477 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ran 𝑄)
2 fourierdlem41.q . . . . . . . . . . 11 (𝜑𝑄 ∈ (𝑃𝑀))
3 fourierdlem41.m . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
4 fourierdlem41.p . . . . . . . . . . . . 13 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
54fourierdlem2 39654 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
63, 5syl 17 . . . . . . . . . . 11 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
72, 6mpbid 222 . . . . . . . . . 10 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
87simpld 475 . . . . . . . . 9 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
9 elmapi 7830 . . . . . . . . 9 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10 ffn 6007 . . . . . . . . 9 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
118, 9, 103syl 18 . . . . . . . 8 (𝜑𝑄 Fn (0...𝑀))
1211adantr 481 . . . . . . 7 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
13 fvelrnb 6205 . . . . . . 7 (𝑄 Fn (0...𝑀) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
1412, 13syl 17 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
151, 14mpbid 222 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
16 0zd 11340 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ∈ ℤ)
17 elfzelz 12291 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18173ad2ant2 1081 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℤ)
19 1zzd 11359 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ∈ ℤ)
2018, 19zsubcld 11438 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℤ)
21 simpll 789 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝜑)
22 elfzle1 12293 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
2322anim1i 591 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗))
24 0red 9992 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 ∈ ℝ)
2517zred 11433 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
2625adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 ∈ ℝ)
2724, 26eqleltd 10132 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 = 𝑗 ↔ (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗)))
2823, 27mpbird 247 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 = 𝑗)
2928eqcomd 2627 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
3029adantll 749 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
31 fveq2 6153 . . . . . . . . . . . . . . . 16 (𝑗 = 0 → (𝑄𝑗) = (𝑄‘0))
327simprld 794 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
3332simpld 475 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
3431, 33sylan9eqr 2677 . . . . . . . . . . . . . . 15 ((𝜑𝑗 = 0) → (𝑄𝑗) = 𝐴)
3521, 30, 34syl2anc 692 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) = 𝐴)
36353adantl3 1217 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) = 𝐴)
37 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
38 fourierdlem41.a . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ)
3938rexrd 10040 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ*)
40 fourierdlem41.b . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ ℝ)
4140rexrd 10040 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℝ*)
42 fourierdlem41.altb . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 < 𝐵)
43 fourierdlem41.t . . . . . . . . . . . . . . . . . . . . . . 23 𝑇 = (𝐵𝐴)
44 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
4538, 40, 42, 43, 44fourierdlem4 39656 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵))
46 fourierdlem41.e . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥)))
4746a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))))
48 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
4940adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
5049, 48resubcld 10409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → (𝐵𝑥) ∈ ℝ)
5140, 38resubcld 10409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝐵𝐴) ∈ ℝ)
5243, 51syl5eqel 2702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝑇 ∈ ℝ)
5352adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
54 0red 9992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 0 ∈ ℝ)
5538, 40posdifd 10565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
5642, 55mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → 0 < (𝐵𝐴))
5743eqcomi 2630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝐵𝐴) = 𝑇
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (𝐵𝐴) = 𝑇)
5956, 58breqtrd 4644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 0 < 𝑇)
6054, 59gtned 10123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝑇 ≠ 0)
6160adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → 𝑇 ≠ 0)
6250, 53, 61redivcld 10804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑥 ∈ ℝ) → ((𝐵𝑥) / 𝑇) ∈ ℝ)
6362flcld 12546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ)
6463zred 11433 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℝ)
6564, 53remulcld 10021 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ ℝ) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
66 fourierdlem41.z . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6766fvmpt2 6253 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6848, 65, 67syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ ℝ) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6968oveq2d 6626 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ ℝ) → (𝑥 + (𝑍𝑥)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
7069mpteq2dva 4709 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
7147, 70eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
7271feq1d 5992 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐸:ℝ⟶(𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵)))
7345, 72mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
74 fourierdlem41.x . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ)
7573, 74ffvelrnd 6321 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸𝑋) ∈ (𝐴(,]𝐵))
76 iocgtlb 39158 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
7739, 41, 75, 76syl3anc 1323 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 < (𝐸𝑋))
7838, 77gtned 10123 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐸𝑋) ≠ 𝐴)
7978adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≠ 𝐴)
8037, 79eqnetrd 2857 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≠ 𝐴)
8180adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) ≠ 𝐴)
82813adantl2 1216 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) ≠ 𝐴)
8382neneqd 2795 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → ¬ (𝑄𝑗) = 𝐴)
8436, 83condan 834 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 < 𝑗)
85 zltlem1 11381 . . . . . . . . . . . . 13 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
8616, 18, 85syl2anc 692 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
8784, 86mpbid 222 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ (𝑗 − 1))
88 eluz2 11644 . . . . . . . . . . 11 ((𝑗 − 1) ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ ∧ 0 ≤ (𝑗 − 1)))
8916, 20, 87, 88syl3anbrc 1244 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (ℤ‘0))
90 elfzel2 12289 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
91903ad2ant2 1081 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℤ)
92 1red 10006 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 1 ∈ ℝ)
9325, 92resubcld 10409 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
9490zred 11433 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
9525ltm1d 10907 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
96 elfzle2 12294 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → 𝑗𝑀)
9793, 25, 94, 95, 96ltletrd 10148 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
98973ad2ant2 1081 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) < 𝑀)
99 elfzo2 12421 . . . . . . . . . 10 ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
10089, 91, 98, 99syl3anbrc 1244 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
1018, 9syl 17 . . . . . . . . . . . . 13 (𝜑𝑄:(0...𝑀)⟶ℝ)
1021013ad2ant1 1080 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
10316, 91, 203jca 1240 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ))
10493, 94, 97ltled 10136 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
1051043ad2ant2 1081 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ≤ 𝑀)
106103, 87, 105jca32 557 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
107 elfz2 12282 . . . . . . . . . . . . 13 ((𝑗 − 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
108106, 107sylibr 224 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
109102, 108ffvelrnd 6321 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
110109rexrd 10040 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
11125recnd 10019 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
112 1cnd 10007 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
113111, 112npcand 10347 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
114113fveq2d 6157 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
115114adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
116101ffvelrnda 6320 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ)
117116rexrd 10040 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
118115, 117eqeltrd 2698 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ*)
1191183adant3 1079 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ*)
120 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋𝑥 = 𝑋)
121 fveq2 6153 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑍𝑥) = (𝑍𝑋))
122120, 121oveq12d 6628 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
123122adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑥 = 𝑋) → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
12466a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
125 oveq2 6618 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
126125oveq1d 6625 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑋) / 𝑇))
127126fveq2d 6157 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑋) / 𝑇)))
128127oveq1d 6625 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
129128adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 = 𝑋) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
13040, 74resubcld 10409 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵𝑋) ∈ ℝ)
131130, 52, 60redivcld 10804 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐵𝑋) / 𝑇) ∈ ℝ)
132131flcld 12546 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
133132zred 11433 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℝ)
134133, 52remulcld 10021 . . . . . . . . . . . . . . . . 17 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
135124, 129, 74, 134fvmptd 6250 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑍𝑋) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
136135, 134eqeltrd 2698 . . . . . . . . . . . . . . 15 (𝜑 → (𝑍𝑋) ∈ ℝ)
13774, 136readdcld 10020 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℝ)
13847, 123, 74, 137fvmptd 6250 . . . . . . . . . . . . 13 (𝜑 → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
139138, 137eqeltrd 2698 . . . . . . . . . . . 12 (𝜑 → (𝐸𝑋) ∈ ℝ)
140139rexrd 10040 . . . . . . . . . . 11 (𝜑 → (𝐸𝑋) ∈ ℝ*)
1411403ad2ant1 1080 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
142 simp1 1059 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
143 ovex 6638 . . . . . . . . . . . . . 14 (𝑗 − 1) ∈ V
144 eleq1 2686 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
145144anbi2d 739 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 − 1) → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
146 fveq2 6153 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑄𝑖) = (𝑄‘(𝑗 − 1)))
147 oveq1 6617 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
148147fveq2d 6157 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
149146, 148breq12d 4631 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 − 1) → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
150145, 149imbi12d 334 . . . . . . . . . . . . . 14 (𝑖 = (𝑗 − 1) → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
1517simprrd 796 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
152151r19.21bi 2927 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
153143, 150, 152vtocl 3248 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
154142, 100, 153syl2anc 692 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
1551143ad2ant2 1081 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
156154, 155breqtrd 4644 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄𝑗))
157 simp3 1061 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
158156, 157breqtrd 4644 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸𝑋))
159139leidd 10545 . . . . . . . . . . . . . 14 (𝜑 → (𝐸𝑋) ≤ (𝐸𝑋))
160159adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝐸𝑋))
16137eqcomd 2627 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
162160, 161breqtrd 4644 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
1631623adant2 1078 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
164113eqcomd 2627 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
165164fveq2d 6157 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
1661653ad2ant2 1081 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
167163, 166breqtrd 4644 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄‘((𝑗 − 1) + 1)))
168110, 119, 141, 158, 167eliocd 39164 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
169146, 148oveq12d 6628 . . . . . . . . . . 11 (𝑖 = (𝑗 − 1) → ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
170169eleq2d 2684 . . . . . . . . . 10 (𝑖 = (𝑗 − 1) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
171170rspcev 3298 . . . . . . . . 9 (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
172100, 168, 171syl2anc 692 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
1731723exp 1261 . . . . . . 7 (𝜑 → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))))
174173adantr 481 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))))
175174rexlimdv 3024 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
17615, 175mpd 15 . . . 4 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
1773adantr 481 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
178101adantr 481 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
179 iocssicc 12210 . . . . . . . 8 ((𝑄‘0)(,](𝑄𝑀)) ⊆ ((𝑄‘0)[,](𝑄𝑀))
18032simprd 479 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = 𝐵)
18133, 180oveq12d 6628 . . . . . . . . 9 (𝜑 → ((𝑄‘0)(,](𝑄𝑀)) = (𝐴(,]𝐵))
18275, 181eleqtrrd 2701 . . . . . . . 8 (𝜑 → (𝐸𝑋) ∈ ((𝑄‘0)(,](𝑄𝑀)))
183179, 182sseldi 3585 . . . . . . 7 (𝜑 → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
184183adantr 481 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
185 simpr 477 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ¬ (𝐸𝑋) ∈ ran 𝑄)
186 fveq2 6153 . . . . . . . . 9 (𝑘 = 𝑗 → (𝑄𝑘) = (𝑄𝑗))
187186breq1d 4628 . . . . . . . 8 (𝑘 = 𝑗 → ((𝑄𝑘) < (𝐸𝑋) ↔ (𝑄𝑗) < (𝐸𝑋)))
188187cbvrabv 3188 . . . . . . 7 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}
189188supeq1i 8304 . . . . . 6 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}, ℝ, < )
190177, 178, 184, 185, 189fourierdlem25 39677 . . . . 5 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
191 ioossioc 39147 . . . . . . . 8 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))
192191a1i 11 . . . . . . 7 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
193192sseld 3586 . . . . . 6 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
194193reximdva 3012 . . . . 5 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
195190, 194mpd 15 . . . 4 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
196176, 195pm2.61dan 831 . . 3 (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
197101adantr 481 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
198 elfzofz 12433 . . . . . . . . . 10 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
199198adantl 482 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
200197, 199ffvelrnd 6321 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
2012003adant3 1079 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
2021363ad2ant1 1080 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
203201, 202resubcld 10409 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
2041393ad2ant1 1080 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
205201rexrd 10040 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
206 fzofzp1 12513 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
207206adantl 482 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
208197, 207ffvelrnd 6321 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209208rexrd 10040 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2102093adant3 1079 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
211 simp3 1061 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
212 iocgtlb 39158 . . . . . . . . 9 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
213205, 210, 211, 212syl3anc 1323 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
214201, 204, 202, 213ltsub1dd 10590 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < ((𝐸𝑋) − (𝑍𝑋)))
215138oveq1d 6625 . . . . . . . . 9 (𝜑 → ((𝐸𝑋) − (𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)))
21674recnd 10019 . . . . . . . . . 10 (𝜑𝑋 ∈ ℂ)
217136recnd 10019 . . . . . . . . . 10 (𝜑 → (𝑍𝑋) ∈ ℂ)
218216, 217pncand 10344 . . . . . . . . 9 (𝜑 → ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑋)
219215, 218eqtrd 2655 . . . . . . . 8 (𝜑 → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
2202193ad2ant1 1080 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
221214, 220breqtrd 4644 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑋)
222 elioore 12154 . . . . . . . . . . 11 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
223135oveq2d 6626 . . . . . . . . . . . . . 14 (𝜑 → (𝑦 + (𝑍𝑋)) = (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
224133recnd 10019 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
22552recnd 10019 . . . . . . . . . . . . . . 15 (𝜑𝑇 ∈ ℂ)
226224, 225mulneg1d 10434 . . . . . . . . . . . . . 14 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
227223, 226oveq12d 6628 . . . . . . . . . . . . 13 (𝜑 → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
228227adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
229 simpr 477 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
230134adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
231229, 230readdcld 10020 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
232231recnd 10019 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ ℂ)
233230recnd 10019 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
234232, 233negsubd 10349 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
235229recnd 10019 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
236235, 233pncand 10344 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = 𝑦)
237228, 234, 2363eqtrrd 2660 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
238222, 237sylan2 491 . . . . . . . . . 10 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
2392383ad2antl1 1221 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
240 simpl1 1062 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
241 fourierdlem41.qssd . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
2422413adant3 1079 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
243242adantr 481 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
244205adantr 481 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ*)
245210adantr 481 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
246222adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
247136adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
248246, 247readdcld 10020 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
2492483ad2antl1 1221 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
250136adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℝ)
251200, 250resubcld 10409 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
252251rexrd 10040 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
253252adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
25474rexrd 10040 . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℝ*)
255254ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
256 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
257 ioogtlb 39151 . . . . . . . . . . . . . . 15 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
258253, 255, 256, 257syl3anc 1323 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
259200adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ)
260136ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
261222adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
262259, 260, 261ltsubaddd 10574 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑦 ↔ (𝑄𝑖) < (𝑦 + (𝑍𝑋))))
263258, 262mpbid 222 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
2642633adantl3 1217 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
265240, 139syl 17 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ∈ ℝ)
266208adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2672663adantl3 1217 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
26874ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
269 iooltub 39169 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
270253, 255, 256, 269syl3anc 1323 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
271261, 268, 260, 270ltadd1dd 10589 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑋 + (𝑍𝑋)))
272138eqcomd 2627 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
273272ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
274271, 273breqtrd 4644 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
2752743adantl3 1217 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
276 iocleub 39159 . . . . . . . . . . . . . . 15 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
277205, 210, 211, 276syl3anc 1323 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
278277adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
279249, 265, 267, 275, 278ltletrd 10148 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
280244, 245, 249, 264, 279eliood 39154 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
281243, 280sseldd 3588 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
282240, 131syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝐵𝑋) / 𝑇) ∈ ℝ)
283282flcld 12546 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
284283znegcld 11435 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
285 negex 10230 . . . . . . . . . . 11 -(⌊‘((𝐵𝑋) / 𝑇)) ∈ V
286 eleq1 2686 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
2872863anbi3d 1402 . . . . . . . . . . . 12 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
288 oveq1 6617 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
289288oveq2d 6626 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
290289eleq1d 2683 . . . . . . . . . . . 12 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
291287, 290imbi12d 334 . . . . . . . . . . 11 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
292 ovex 6638 . . . . . . . . . . . 12 (𝑦 + (𝑍𝑋)) ∈ V
293 eleq1 2686 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥𝐷 ↔ (𝑦 + (𝑍𝑋)) ∈ 𝐷))
2942933anbi2d 1401 . . . . . . . . . . . . 13 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ)))
295 oveq1 6617 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)))
296295eleq1d 2683 . . . . . . . . . . . . 13 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
297294, 296imbi12d 334 . . . . . . . . . . . 12 (𝑥 = (𝑦 + (𝑍𝑋)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
298 fourierdlem41.dper . . . . . . . . . . . 12 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
299292, 297, 298vtocl 3248 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
300285, 291, 299vtocl 3248 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
301240, 281, 284, 300syl3anc 1323 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
302239, 301eqeltrd 2698 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦𝐷)
303302ralrimiva 2961 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
304 dfss3 3577 . . . . . . 7 ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
305303, 304sylibr 224 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)
306 breq1 4621 . . . . . . . 8 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → (𝑦 < 𝑋 ↔ ((𝑄𝑖) − (𝑍𝑋)) < 𝑋))
307 oveq1 6617 . . . . . . . . 9 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → (𝑦(,)𝑋) = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
308307sseq1d 3616 . . . . . . . 8 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → ((𝑦(,)𝑋) ⊆ 𝐷 ↔ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷))
309306, 308anbi12d 746 . . . . . . 7 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → ((𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ↔ (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ∧ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)))
310309rspcev 3298 . . . . . 6 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ ∧ (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ∧ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
311203, 221, 305, 310syl12anc 1321 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
3123113exp 1261 . . . 4 (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))))
313312rexlimdv 3024 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷)))
314196, 313mpd 15 . 2 (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
315 0zd 11340 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
3163nnzd 11432 . . . . . . . . . 10 (𝜑𝑀 ∈ ℤ)
317 1zzd 11359 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
318315, 316, 3173jca 1240 . . . . . . . . 9 (𝜑 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ))
319 0le1 10502 . . . . . . . . . 10 0 ≤ 1
320319a1i 11 . . . . . . . . 9 (𝜑 → 0 ≤ 1)
3213nnge1d 11014 . . . . . . . . 9 (𝜑 → 1 ≤ 𝑀)
322318, 320, 321jca32 557 . . . . . . . 8 (𝜑 → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
323 elfz2 12282 . . . . . . . 8 (1 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
324322, 323sylibr 224 . . . . . . 7 (𝜑 → 1 ∈ (0...𝑀))
325101, 324ffvelrnd 6321 . . . . . 6 (𝜑 → (𝑄‘1) ∈ ℝ)
326136, 52resubcld 10409 . . . . . 6 (𝜑 → ((𝑍𝑋) − 𝑇) ∈ ℝ)
327325, 326resubcld 10409 . . . . 5 (𝜑 → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ)
328327adantr 481 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ)
32938recnd 10019 . . . . . . . . . 10 (𝜑𝐴 ∈ ℂ)
330329, 225pncand 10344 . . . . . . . . 9 (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
331330adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
33243oveq2i 6621 . . . . . . . . . . 11 (𝐴 + 𝑇) = (𝐴 + (𝐵𝐴))
333332a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐴 + 𝑇) = (𝐴 + (𝐵𝐴)))
33440recnd 10019 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
335329, 334pncan3d 10346 . . . . . . . . . . 11 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
336335adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐴 + (𝐵𝐴)) = 𝐵)
337 id 22 . . . . . . . . . . . 12 ((𝐸𝑋) = 𝐵 → (𝐸𝑋) = 𝐵)
338337eqcomd 2627 . . . . . . . . . . 11 ((𝐸𝑋) = 𝐵𝐵 = (𝐸𝑋))
339338adantl 482 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝐵 = (𝐸𝑋))
340333, 336, 3393eqtrrd 2660 . . . . . . . . 9 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐸𝑋) = (𝐴 + 𝑇))
341340oveq1d 6625 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐸𝑋) − 𝑇) = ((𝐴 + 𝑇) − 𝑇))
34233adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = 𝐴)
343331, 341, 3423eqtr4rd 2666 . . . . . . 7 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = ((𝐸𝑋) − 𝑇))
344343oveq1d 6625 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) = (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)))
345139recnd 10019 . . . . . . . 8 (𝜑 → (𝐸𝑋) ∈ ℂ)
346345, 217, 225nnncan2d 10378 . . . . . . 7 (𝜑 → (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)) = ((𝐸𝑋) − (𝑍𝑋)))
347346adantr 481 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)) = ((𝐸𝑋) − (𝑍𝑋)))
348219adantr 481 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
349344, 347, 3483eqtrrd 2660 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝑋 = ((𝑄‘0) − ((𝑍𝑋) − 𝑇)))
35033, 38eqeltrd 2698 . . . . . . 7 (𝜑 → (𝑄‘0) ∈ ℝ)
3513nngt0d 11015 . . . . . . . . . 10 (𝜑 → 0 < 𝑀)
352 fzolb 12424 . . . . . . . . . 10 (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
353315, 316, 351, 352syl3anbrc 1244 . . . . . . . . 9 (𝜑 → 0 ∈ (0..^𝑀))
354 0re 9991 . . . . . . . . . 10 0 ∈ ℝ
355 eleq1 2686 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
356355anbi2d 739 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
357 fveq2 6153 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
358 oveq1 6617 . . . . . . . . . . . . . 14 (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
359358fveq2d 6157 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
360357, 359breq12d 4631 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
361356, 360imbi12d 334 . . . . . . . . . . 11 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
362361, 152vtoclg 3255 . . . . . . . . . 10 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
363354, 362ax-mp 5 . . . . . . . . 9 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
364353, 363mpdan 701 . . . . . . . 8 (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
365 0p1e1 11083 . . . . . . . . . 10 (0 + 1) = 1
366365fveq2i 6156 . . . . . . . . 9 (𝑄‘(0 + 1)) = (𝑄‘1)
367366a1i 11 . . . . . . . 8 (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
368364, 367breqtrd 4644 . . . . . . 7 (𝜑 → (𝑄‘0) < (𝑄‘1))
369350, 325, 326, 368ltsub1dd 10590 . . . . . 6 (𝜑 → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
370369adantr 481 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
371349, 370eqbrtrd 4640 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
372 elioore 12154 . . . . . . . . 9 (𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) → 𝑦 ∈ ℝ)
373135eqcomd 2627 . . . . . . . . . . . . . . . 16 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = (𝑍𝑋))
374373negeqd 10226 . . . . . . . . . . . . . . 15 (𝜑 → -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -(𝑍𝑋))
375226, 374eqtrd 2655 . . . . . . . . . . . . . 14 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -(𝑍𝑋))
376225mulid2d 10009 . . . . . . . . . . . . . 14 (𝜑 → (1 · 𝑇) = 𝑇)
377375, 376oveq12d 6628 . . . . . . . . . . . . 13 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)) = (-(𝑍𝑋) + 𝑇))
378224negcld 10330 . . . . . . . . . . . . . 14 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
379 1cnd 10007 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
380378, 379, 225adddird 10016 . . . . . . . . . . . . 13 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇) = ((-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)))
381217, 225negsubdid 10358 . . . . . . . . . . . . 13 (𝜑 → -((𝑍𝑋) − 𝑇) = (-(𝑍𝑋) + 𝑇))
382377, 380, 3813eqtr4d 2665 . . . . . . . . . . . 12 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇) = -((𝑍𝑋) − 𝑇))
383382oveq2d 6626 . . . . . . . . . . 11 (𝜑 → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)))
384383adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)))
385326adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → ((𝑍𝑋) − 𝑇) ∈ ℝ)
386229, 385readdcld 10020 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
387386recnd 10019 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℂ)
388385recnd 10019 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((𝑍𝑋) − 𝑇) ∈ ℂ)
389387, 388negsubd 10349 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) − ((𝑍𝑋) − 𝑇)))
390235, 388pncand 10344 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) − ((𝑍𝑋) − 𝑇)) = 𝑦)
391384, 389, 3903eqtrrd 2660 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
392372, 391sylan2 491 . . . . . . . 8 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
393392adantlr 750 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
394 simpll 789 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝜑)
395367eqcomd 2627 . . . . . . . . . . . 12 (𝜑 → (𝑄‘1) = (𝑄‘(0 + 1)))
396395oveq2d 6626 . . . . . . . . . . 11 (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
397357, 359oveq12d 6628 . . . . . . . . . . . . . . . 16 (𝑖 = 0 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
398397sseq1d 3616 . . . . . . . . . . . . . . 15 (𝑖 = 0 → (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷 ↔ ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
399356, 398imbi12d 334 . . . . . . . . . . . . . 14 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)))
400399, 241vtoclg 3255 . . . . . . . . . . . . 13 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
401354, 400ax-mp 5 . . . . . . . . . . . 12 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
402353, 401mpdan 701 . . . . . . . . . . 11 (𝜑 → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
403396, 402eqsstrd 3623 . . . . . . . . . 10 (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
404403ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
40533, 39eqeltrd 2698 . . . . . . . . . . 11 (𝜑 → (𝑄‘0) ∈ ℝ*)
406405ad2antrr 761 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) ∈ ℝ*)
407325rexrd 10040 . . . . . . . . . . 11 (𝜑 → (𝑄‘1) ∈ ℝ*)
408407ad2antrr 761 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ*)
409372, 386sylan2 491 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
410409adantlr 750 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
411345, 216, 217subaddd 10361 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐸𝑋) − 𝑋) = (𝑍𝑋) ↔ (𝑋 + (𝑍𝑋)) = (𝐸𝑋)))
412272, 411mpbird 247 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑋) − 𝑋) = (𝑍𝑋))
413 oveq1 6617 . . . . . . . . . . . . . . . 16 ((𝐸𝑋) = 𝐵 → ((𝐸𝑋) − 𝑋) = (𝐵𝑋))
414412, 413sylan9req 2676 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑍𝑋) = (𝐵𝑋))
415414oveq1d 6625 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑍𝑋) − 𝑇) = ((𝐵𝑋) − 𝑇))
416415oveq2d 6626 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋 + ((𝑍𝑋) − 𝑇)) = (𝑋 + ((𝐵𝑋) − 𝑇)))
417130recnd 10019 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝑋) ∈ ℂ)
418216, 417, 225addsubassd 10363 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑋 + ((𝐵𝑋) − 𝑇)))
419418eqcomd 2627 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + ((𝐵𝑋) − 𝑇)) = ((𝑋 + (𝐵𝑋)) − 𝑇))
420419adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋 + ((𝐵𝑋) − 𝑇)) = ((𝑋 + (𝐵𝑋)) − 𝑇))
421334, 225, 329subsub23d 38986 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝑇) = 𝐴 ↔ (𝐵𝐴) = 𝑇))
42258, 421mpbird 247 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵𝑇) = 𝐴)
423216, 334pncan3d 10346 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 + (𝐵𝑋)) = 𝐵)
424423oveq1d 6625 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝐵𝑇))
425422, 424, 333eqtr4d 2665 . . . . . . . . . . . . . 14 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑄‘0))
426425adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑄‘0))
427416, 420, 4263eqtrrd 2660 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = (𝑋 + ((𝑍𝑋) − 𝑇)))
428427adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) = (𝑋 + ((𝑍𝑋) − 𝑇)))
42974adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 ∈ ℝ)
430372adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 ∈ ℝ)
431326adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑍𝑋) − 𝑇) ∈ ℝ)
432254adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 ∈ ℝ*)
433327rexrd 10040 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*)
434433adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*)
435 simpr 477 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
436 ioogtlb 39151 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ* ∧ ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 < 𝑦)
437432, 434, 435, 436syl3anc 1323 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 < 𝑦)
438429, 430, 431, 437ltadd1dd 10589 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑋 + ((𝑍𝑋) − 𝑇)) < (𝑦 + ((𝑍𝑋) − 𝑇)))
439438adantlr 750 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑋 + ((𝑍𝑋) − 𝑇)) < (𝑦 + ((𝑍𝑋) − 𝑇)))
440428, 439eqbrtrd 4640 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) < (𝑦 + ((𝑍𝑋) − 𝑇)))
441 iooltub 39169 . . . . . . . . . . . . 13 ((𝑋 ∈ ℝ* ∧ ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
442432, 434, 435, 441syl3anc 1323 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
443325adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ)
444430, 431, 443ltaddsubd 10578 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1) ↔ 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
445442, 444mpbird 247 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1))
446445adantlr 750 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1))
447406, 408, 410, 440, 446eliood 39154 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ((𝑄‘0)(,)(𝑄‘1)))
448404, 447sseldd 3588 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷)
449132znegcld 11435 . . . . . . . . . 10 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
450449peano2zd 11436 . . . . . . . . 9 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)
451450ad2antrr 761 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)
452 ovex 6638 . . . . . . . . 9 (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ V
453 eleq1 2686 . . . . . . . . . . 11 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (𝑘 ∈ ℤ ↔ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ))
4544533anbi3d 1402 . . . . . . . . . 10 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)))
455 oveq1 6617 . . . . . . . . . . . 12 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (𝑘 · 𝑇) = ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇))
456455oveq2d 6626 . . . . . . . . . . 11 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
457456eleq1d 2683 . . . . . . . . . 10 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷))
458454, 457imbi12d 334 . . . . . . . . 9 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)))
459 ovex 6638 . . . . . . . . . 10 (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ V
460 eleq1 2686 . . . . . . . . . . . 12 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (𝑥𝐷 ↔ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷))
4614603anbi2d 1401 . . . . . . . . . . 11 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ)))
462 oveq1 6617 . . . . . . . . . . . 12 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)))
463462eleq1d 2683 . . . . . . . . . . 11 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷))
464461, 463imbi12d 334 . . . . . . . . . 10 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)))
465459, 464, 298vtocl 3248 . . . . . . . . 9 ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)
466452, 458, 465vtocl 3248 . . . . . . . 8 ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
467394, 448, 451, 466syl3anc 1323 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
468393, 467eqeltrd 2698 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦𝐷)
469468ralrimiva 2961 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))𝑦𝐷)
470 dfss3 3577 . . . . 5 ((𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))𝑦𝐷)
471469, 470sylibr 224 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)
472 breq2 4622 . . . . . 6 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → (𝑋 < 𝑦𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
473 oveq2 6618 . . . . . . 7 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
474473sseq1d 3616 . . . . . 6 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷))
475472, 474anbi12d 746 . . . . 5 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)))
476475rspcev 3298 . . . 4 ((((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ ∧ (𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
477328, 371, 471, 476syl12anc 1321 . . 3 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
47815adantlr 750 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
479 simp2 1060 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (0...𝑀))
480253ad2ant2 1081 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℝ)
481943ad2ant2 1081 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℝ)
482963ad2ant2 1081 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗𝑀)
483 id 22 . . . . . . . . . . . . . . . . . 18 ((𝑄𝑗) = (𝐸𝑋) → (𝑄𝑗) = (𝐸𝑋))
484483eqcomd 2627 . . . . . . . . . . . . . . . . 17 ((𝑄𝑗) = (𝐸𝑋) → (𝐸𝑋) = (𝑄𝑗))
485484adantr 481 . . . . . . . . . . . . . . . 16 (((𝑄𝑗) = (𝐸𝑋) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = (𝑄𝑗))
4864853ad2antl3 1223 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = (𝑄𝑗))
487 fveq2 6153 . . . . . . . . . . . . . . . . 17 (𝑀 = 𝑗 → (𝑄𝑀) = (𝑄𝑗))
488487eqcomd 2627 . . . . . . . . . . . . . . . 16 (𝑀 = 𝑗 → (𝑄𝑗) = (𝑄𝑀))
489488adantl 482 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝑄𝑗) = (𝑄𝑀))
490180ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → (𝑄𝑀) = 𝐵)
4914903ad2antl1 1221 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝑄𝑀) = 𝐵)
492486, 489, 4913eqtrd 2659 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = 𝐵)
493 neneq 2796 . . . . . . . . . . . . . . . 16 ((𝐸𝑋) ≠ 𝐵 → ¬ (𝐸𝑋) = 𝐵)
494493ad2antlr 762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → ¬ (𝐸𝑋) = 𝐵)
4954943ad2antl1 1221 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → ¬ (𝐸𝑋) = 𝐵)
496492, 495pm2.65da 599 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ¬ 𝑀 = 𝑗)
497496neqned 2797 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀𝑗)
498480, 481, 482, 497leneltd 10142 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 < 𝑀)
499 elfzfzo 38975 . . . . . . . . . . 11 (𝑗 ∈ (0..^𝑀) ↔ (𝑗 ∈ (0...𝑀) ∧ 𝑗 < 𝑀))
500479, 498, 499sylanbrc 697 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (0..^𝑀))
501117adantlr 750 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
5025013adant3 1079 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ∈ ℝ*)
503 simp1l 1083 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
504101adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
505 fzofzp1 12513 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
506505adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
507504, 506ffvelrnd 6321 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
508507rexrd 10040 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ*)
509503, 500, 508syl2anc 692 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 + 1)) ∈ ℝ*)
5101413adant1r 1316 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
51137, 160eqbrtrd 4640 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
512511adantlr 750 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
5135123adant2 1078 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
5144843ad2ant3 1082 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
515 eleq1 2686 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
516515anbi2d 739 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑𝑗 ∈ (0..^𝑀))))
517 fveq2 6153 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑄𝑖) = (𝑄𝑗))
518 oveq1 6617 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
519518fveq2d 6157 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
520517, 519breq12d 4631 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄𝑗) < (𝑄‘(𝑗 + 1))))
521516, 520imbi12d 334 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))))
522521, 152chvarv 2262 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))
523503, 500, 522syl2anc 692 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))
524514, 523eqbrtrd 4640 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) < (𝑄‘(𝑗 + 1)))
525502, 509, 510, 513, 524elicod 12173 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1))))
526517, 519oveq12d 6628 . . . . . . . . . . . 12 (𝑖 = 𝑗 → ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1))))
527526eleq2d 2684 . . . . . . . . . . 11 (𝑖 = 𝑗 → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1)))))
528527rspcev 3298 . . . . . . . . . 10 ((𝑗 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
529500, 525, 528syl2anc 692 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
5305293exp 1261 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))))
531530adantr 481 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))))
532531rexlimdv 3024 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
533478, 532mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
534 ioossico 12211 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))
535 simpr 477 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
536534, 535sseldi 3585 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
537536ex 450 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
538537adantlr 750 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
539538reximdva 3012 . . . . . . 7 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
540190, 539mpd 15 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
541540adantlr 750 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
542533, 541pm2.61dan 831 . . . 4 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
543208, 250resubcld 10409 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
5445433adant3 1079 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
545219eqcomd 2627 . . . . . . . . . 10 (𝜑𝑋 = ((𝐸𝑋) − (𝑍𝑋)))
5465453ad2ant1 1080 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 = ((𝐸𝑋) − (𝑍𝑋)))
5471393ad2ant1 1080 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
5482083adant3 1079 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
5491363ad2ant1 1080 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
550200rexrd 10040 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
5515503adant3 1079 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
5522093adant3 1079 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
553 simp3 1061 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
554 icoltub 39166 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < (𝑄‘(𝑖 + 1)))
555551, 552, 553, 554syl3anc 1323 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < (𝑄‘(𝑖 + 1)))
556547, 548, 549, 555ltsub1dd 10590 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝐸𝑋) − (𝑍𝑋)) < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
557546, 556eqbrtrd 4640 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
558 elioore 12154 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) → 𝑦 ∈ ℝ)
559558, 237sylan2 491 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
5605593ad2antl1 1221 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
561 simpl1 1062 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝜑)
5622413adant3 1079 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
563562adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
564551adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ∈ ℝ*)
565552adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
566558adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ ℝ)
567136adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑍𝑋) ∈ ℝ)
568566, 567readdcld 10020 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
5695683ad2antl1 1221 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
5702003adant3 1079 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
571570adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ∈ ℝ)
572561, 139syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) ∈ ℝ)
573 icogelb 12174 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ≤ (𝐸𝑋))
574551, 552, 553, 573syl3anc 1323 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ≤ (𝐸𝑋))
575574adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ≤ (𝐸𝑋))
576138ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
57774ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 ∈ ℝ)
578558adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ ℝ)
579136ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑍𝑋) ∈ ℝ)
580254ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 ∈ ℝ*)
581543rexrd 10040 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*)
582581adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*)
583 simpr 477 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
584 ioogtlb 39151 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 < 𝑦)
585580, 582, 583, 584syl3anc 1323 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 < 𝑦)
586577, 578, 579, 585ltadd1dd 10589 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑋 + (𝑍𝑋)) < (𝑦 + (𝑍𝑋)))
587576, 586eqbrtrd 4640 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) < (𝑦 + (𝑍𝑋)))
5885873adantl3 1217 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) < (𝑦 + (𝑍𝑋)))
589571, 572, 569, 575, 588lelttrd 10146 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
590543adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
591 iooltub 39169 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
592580, 582, 583, 591syl3anc 1323 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
593578, 590, 579, 592ltadd1dd 10589 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)))
594208recnd 10019 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
595217adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℂ)
596594, 595npcand 10347 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄‘(𝑖 + 1)))
597596adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄‘(𝑖 + 1)))
598593, 597breqtrd 4644 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
5995983adantl3 1217 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
600564, 565, 569, 589, 599eliood 39154 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
601563, 600sseldd 3588 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
602561, 449syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
603561, 601, 602, 300syl3anc 1323 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
604560, 603eqeltrd 2698 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦𝐷)
605604ralrimiva 2961 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))𝑦𝐷)
606 dfss3 3577 . . . . . . . . 9 ((𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))𝑦𝐷)
607605, 606sylibr 224 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)
608 breq2 4622 . . . . . . . . . 10 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → (𝑋 < 𝑦𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
609 oveq2 6618 . . . . . . . . . . 11 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
610609sseq1d 3616 . . . . . . . . . 10 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷))
611608, 610anbi12d 746 . . . . . . . . 9 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)))
612611rspcev 3298 . . . . . . . 8 ((((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ ∧ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
613544, 557, 607, 612syl12anc 1321 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
6146133exp 1261 . . . . . 6 (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
615614adantr 481 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
616615rexlimdv 3024 . . . 4 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
617542, 616mpd 15 . . 3 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
618477, 617pm2.61dane 2877 . 2 (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
619314, 618jca 554 1 (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  wss 3559   class class class wbr 4618  cmpt 4678  ran crn 5080   Fn wfn 5847  wf 5848  cfv 5852  (class class class)co 6610  𝑚 cmap 7809  supcsup 8297  cc 9885  cr 9886  0cc0 9887  1c1 9888   + caddc 9890   · cmul 9892  *cxr 10024   < clt 10025  cle 10026  cmin 10217  -cneg 10218   / cdiv 10635  cn 10971  cz 11328  cuz 11638  (,)cioo 12124  (,]cioc 12125  [,)cico 12126  [,]cicc 12127  ...cfz 12275  ..^cfzo 12413  cfl 12538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-er 7694  df-map 7811  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-sup 8299  df-inf 8300  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-n0 11244  df-z 11329  df-uz 11639  df-rp 11784  df-ioo 12128  df-ioc 12129  df-ico 12130  df-icc 12131  df-fz 12276  df-fzo 12414  df-fl 12540
This theorem is referenced by:  fourierdlem113  39764
  Copyright terms: Public domain W3C validator