fourierdlem41 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem41 47297

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	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (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.

Step	Hyp	Ref	Expression
1		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ran 𝑄)
2		fourierdlem41.q	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
3		fourierdlem41.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4		fourierdlem41.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
5	4	fourierdlem2 47258	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	3, 5	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
7	2, 6	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
8	7	simpld 500	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
9		elmapi 8880	. . . . . . . . 9 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10		ffn 6717	. . . . . . . . 9 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
11	8, 9, 10	3syl 19	. . . . . . . 8 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
12	11	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
13		fvelrnb 6953	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
14	12, 13	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
15	1, 14	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋))
16		0zd 12715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ∈ ℤ)
17		elfzelz 13666	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18	17	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℤ)
19		1zzd 12737	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 1 ∈ ℤ)
20	18, 19	zsubcld 12818	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ ℤ)
21		simpll 779	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝜑)
22		elfzle1 13670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
23	22	anim1i 627	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗))
24		0red 11321	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 ∈ ℝ)
25	17	zred 12813	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
26	25	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 ∈ ℝ)
27	24, 26	eqleltd 11464	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 = 𝑗 ↔ (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗)))
28	23, 27	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 = 𝑗)
29	28	eqcomd 2769	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
30	29	adantll 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
31		fveq2 6893	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑄‘𝑗) = (𝑄‘0))
32	7	simprld 784	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
33	32	simpld 500	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
34	31, 33	sylan9eqr 2820	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝑄‘𝑗) = 𝐴)
35	21, 30, 34	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) = 𝐴)
36	35	3adantl3 1187	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) = 𝐴)
37		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝐸‘𝑋))
38		fourierdlem41.a	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ ℝ)
39	38	rexrd 11369	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
40		fourierdlem41.b	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
41	40	rexrd 11369	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
42		fourierdlem41.altb	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐴 < 𝐵)
43		fourierdlem41.t	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑇 = (𝐵 − 𝐴)
44		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
45	38, 40, 42, 43, 44	fourierdlem4 47260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵))
46		fourierdlem41.e	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥)))
47	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))))
48		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
49	40	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
50	49, 48	resubcld 11754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ)
51	40, 38	resubcld 11754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
52	43, 51	eqeltrid 2867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝑇 ∈ ℝ)
53	52	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
54		0red 11321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 0 ∈ ℝ)
55	38, 40	posdifd 11913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
56	42, 55	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
57	43	eqcomi 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐵 − 𝐴) = 𝑇
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
59	56, 58	breqtrd 5133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 0 < 𝑇)
60	54, 59	gtned 11455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝑇 ≠ 0)
61	60	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0)
62	50, 53, 61	redivcld 12155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ)
63	62	flcld 13948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
64	63	zred 12813	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
65	64, 53	remulcld 11349	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
66		fourierdlem41.z	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
67	66	fvmpt2 7013	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ) → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
68	48, 65, 67	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
69	68	oveq2d 7443	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝑍‘𝑥)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
70	69	mpteq2dva 5200	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
71	47, 70	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
72	71	feq1d 6699	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐸:ℝ⟶(𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵)))
73	45, 72	mpbird 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
74		fourierdlem41.x	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑋 ∈ ℝ)
75	73, 74	ffvelcdmd 7093	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (𝐴(,]𝐵))
76		iocgtlb 46653	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸‘𝑋))
77	39, 41, 75, 76	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < (𝐸‘𝑋))
78	38, 77	gtned 11455	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸‘𝑋) ≠ 𝐴)
79	78	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≠ 𝐴)
80	37, 79	eqnetrd 3025	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≠ 𝐴)
81	80	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) ≠ 𝐴)
82	81	3adantl2 1186	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) ≠ 𝐴)
83	82	neneqd 2963	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → ¬ (𝑄‘𝑗) = 𝐴)
84	36, 83	condan 830	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 < 𝑗)
85		zltlem1 12759	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
86	16, 18, 85	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
87	84, 86	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ≤ (𝑗 − 1))
88		eluz2 12981	. . . . . . . . . . 11 ⊢ ((𝑗 − 1) ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ ∧ 0 ≤ (𝑗 − 1)))
89	16, 20, 87, 88	syl3anbrc 1362	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (ℤ_≥‘0))
90		elfzel2 13664	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
91	90	3ad2ant2 1152	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ∈ ℤ)
92		1red 11319	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 1 ∈ ℝ)
93	25, 92	resubcld 11754	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
94	90	zred 12813	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
95	25	ltm1d 12259	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
96		elfzle2 13671	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
97	93, 25, 94, 95, 96	ltletrd 11480	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
98	97	3ad2ant2 1152	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) < 𝑀)
99		elfzo2 13806	. . . . . . . . . 10 ⊢ ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ_≥‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
100	89, 91, 98, 99	syl3anbrc 1362	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
101	8, 9	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
102	101	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
103	93, 94, 97	ltled 11468	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
104	103	3ad2ant2 1152	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ≤ 𝑀)
105	16, 91, 20, 87, 104	elfzd 13657	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
106	102, 105	ffvelcdmd 7093	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
107	106	rexrd 11369	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ^*)
108	25	recnd 11347	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
109		1cnd 11312	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
110	108, 109	npcand 11683	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
111	110	fveq2d 6897	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
112	111	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
113	101	ffvelcdmda 7092	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
114	113	rexrd 11369	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ^*)
115	112, 114	eqeltrd 2863	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ^*)
116	115	3adant3 1150	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ^*)
117		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
118		fveq2 6893	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑍‘𝑥) = (𝑍‘𝑋))
119	117, 118	oveq12d 7445	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝑍‘𝑥)) = (𝑋 + (𝑍‘𝑋)))
120	119	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + (𝑍‘𝑥)) = (𝑋 + (𝑍‘𝑋)))
121	66	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
122		oveq2 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑋 → (𝐵 − 𝑥) = (𝐵 − 𝑋))
123	122	oveq1d 7442	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑋 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑋) / 𝑇))
124	123	fveq2d 6897	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑋 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑋) / 𝑇)))
125	124	oveq1d 7442	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑋 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
126	125	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
127	40, 74	resubcld 11754	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
128	127, 52, 60	redivcld 12155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
129	128	flcld 13948	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
130	129	zred 12813	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℝ)
131	130, 52	remulcld 11349	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
132	121, 126, 74, 131	fvmptd 7009	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑍‘𝑋) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
133	132, 131	eqeltrd 2863	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍‘𝑋) ∈ ℝ)
134	74, 133	readdcld 11348	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + (𝑍‘𝑋)) ∈ ℝ)
135	47, 120, 74, 134	fvmptd 7009	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
136	135, 134	eqeltrd 2863	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ)
137	136	rexrd 11369	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ^*)
138	137	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ^*)
139		simp1 1154	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝜑)
140		ovex 7460	. . . . . . . . . . . . . 14 ⊢ (𝑗 − 1) ∈ V
141		eleq1 2851	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
142	141	anbi2d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 − 1) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
143		fveq2 6893	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑄‘𝑖) = (𝑄‘(𝑗 − 1)))
144		oveq1 7434	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
145	144	fveq2d 6897	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
146	143, 145	breq12d 5118	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
147	142, 146	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑗 − 1) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
148	7	simprrd 786	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
149	148	r19.21bi 3257	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
150	140, 147, 149	vtocl 3523	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
151	139, 100, 150	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
152	111	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
153	151, 152	breqtrd 5133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘𝑗))
154		simp3 1156	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝐸‘𝑋))
155	153, 154	breqtrd 5133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸‘𝑋))
156	136	leidd 11892	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
157	156	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
158	37	eqcomd 2769	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) = (𝑄‘𝑗))
159	157, 158	breqtrd 5133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
160	159	3adant2 1149	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
161	110	eqcomd 2769	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
162	161	fveq2d 6897	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑄‘𝑗) = (𝑄‘((𝑗 − 1) + 1)))
163	162	3ad2ant2 1152	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝑄‘((𝑗 − 1) + 1)))
164	160, 163	breqtrd 5133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘((𝑗 − 1) + 1)))
165	107, 116, 138, 155, 164	eliocd 46658	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
166	143, 145	oveq12d 7445	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
167	166	eleq2d 2849	. . . . . . . . . 10 ⊢ (𝑖 = (𝑗 − 1) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
168	167	rspcev 3579	. . . . . . . . 9 ⊢ (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
169	100, 165, 168	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
170	169	3exp 1137	. . . . . . 7 ⊢ (𝜑 → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))))
171	170	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))))
172	171	rexlimdv 3164	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
173	15, 172	mpd 16	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
174	3	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
175	101	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
176		iocssicc 13578	. . . . . . . 8 ⊢ ((𝑄‘0)(,](𝑄‘𝑀)) ⊆ ((𝑄‘0)[,](𝑄‘𝑀))
177	32	simprd 501	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
178	33, 177	oveq12d 7445	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄‘0)(,](𝑄‘𝑀)) = (𝐴(,]𝐵))
179	75, 178	eleqtrrd 2866	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ((𝑄‘0)(,](𝑄‘𝑀)))
180	176, 179	sselid 3910	. . . . . . 7 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
181	180	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
182		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ¬ (𝐸‘𝑋) ∈ ran 𝑄)
183		fveq2 6893	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗))
184	183	breq1d 5115	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → ((𝑄‘𝑘) < (𝐸‘𝑋) ↔ (𝑄‘𝑗) < (𝐸‘𝑋)))
185	184	cbvrabv 3425	. . . . . . 7 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}
186	185	supeq1i 9449	. . . . . 6 ⊢ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}, ℝ, < )
187	174, 175, 181, 182, 186	fourierdlem25 47281	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
188		ioossioc 46643	. . . . . . . 8 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))
189	188	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
190	189	sseld 3911	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
191	190	reximdva 3178	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
192	187, 191	mpd 16	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
193	173, 192	pm2.61dan 825	. . 3 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
194	101	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
195		elfzofz 13820	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
196	195	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
197	194, 196	ffvelcdmd 7093	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
198	197	3adant3 1150	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
199	133	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍‘𝑋) ∈ ℝ)
200	198, 199	resubcld 11754	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ)
201	136	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ)
202	198	rexrd 11369	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
203		fzofzp1 13909	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
204	203	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
205	194, 204	ffvelcdmd 7093	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
206	205	rexrd 11369	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
207	206	3adant3 1150	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
208		simp3 1156	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
209		iocgtlb 46653	. . . . . . . . 9 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝐸‘𝑋))
210	202, 207, 208, 209	syl3anc 1398	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝐸‘𝑋))
211	198, 201, 199, 210	ltsub1dd 11938	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < ((𝐸‘𝑋) − (𝑍‘𝑋)))
212	135	oveq1d 7442	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸‘𝑋) − (𝑍‘𝑋)) = ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)))
213	74	recnd 11347	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℂ)
214	133	recnd 11347	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍‘𝑋) ∈ ℂ)
215	213, 214	pncand 11680	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = 𝑋)
216	212, 215	eqtrd 2798	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
217	216	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
218	211, 217	breqtrd 5133	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋)
219		elioore 13516	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
220	132	oveq2d 7443	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 + (𝑍‘𝑋)) = (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
221	130	recnd 11347	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℂ)
222	52	recnd 11347	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇 ∈ ℂ)
223	221, 222	mulneg1d 11779	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
224	220, 223	oveq12d 7445	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
225	224	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
226		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
227	131	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
228	226, 227	readdcld 11348	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
229	228	recnd 11347	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℂ)
230	227	recnd 11347	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
231	229, 230	negsubd 11685	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
232	226	recnd 11347	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
233	232, 230	pncand 11680	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = 𝑦)
234	225, 231, 233	3eqtrrd 2803	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
235	219, 234	sylan2 605	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
236	235	3ad2antl1 1204	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
237		simpl1 1210	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝜑)
238		fourierdlem41.qssd	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
239	238	3adant3 1150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
240	239	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
241	202	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ^*)
242	207	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
243	219	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
244	133	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
245	243, 244	readdcld 11348	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
246	245	3ad2antl1 1204	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
247	133	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℝ)
248	197, 247	resubcld 11754	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ)
249	248	rexrd 11369	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^*)
250	249	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^*)
251	74	rexrd 11369	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
252	251	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ^*)
253		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
254		ioogtlb 46646	. . . . . . . . . . . . . . 15 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑋 ∈ ℝ^* ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦)
255	250, 252, 253, 254	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦)
256	197	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ)
257	133	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
258	219	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
259	256, 257, 258	ltsubaddd 11922	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦 ↔ (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋))))
260	255, 259	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
261	260	3adantl3 1187	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
262	237, 136	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐸‘𝑋) ∈ ℝ)
263	205	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
264	263	3adantl3 1187	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
265	74	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
266		iooltub 46661	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑋 ∈ ℝ^* ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 < 𝑋)
267	250, 252, 253, 266	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 < 𝑋)
268	258, 265, 257, 267	ltadd1dd 11937	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝑋 + (𝑍‘𝑋)))
269	135	eqcomd 2769	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
270	269	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
271	268, 270	breqtrd 5133	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝐸‘𝑋))
272	271	3adantl3 1187	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝐸‘𝑋))
273		iocleub 46654	. . . . . . . . . . . . . . 15 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
274	202, 207, 208, 273	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
275	274	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
276	246, 262, 264, 272, 275	ltletrd 11480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
277	241, 242, 246, 261, 276	eliood 46649	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
278	240, 277	sseldd 3913	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ 𝐷)
279	237, 128	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
280	279	flcld 13948	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
281	280	znegcld 12815	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
282		negex 11565	. . . . . . . . . . 11 ⊢ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ V
283		eleq1 2851	. . . . . . . . . . . . 13 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
284	283	3anbi3d 1470	. . . . . . . . . . . 12 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)))
285		oveq1 7434	. . . . . . . . . . . . . 14 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 · 𝑇) = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
286	285	oveq2d 7443	. . . . . . . . . . . . 13 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
287	286	eleq1d 2848	. . . . . . . . . . . 12 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
288	284, 287	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
289		ovex 7460	. . . . . . . . . . . 12 ⊢ (𝑦 + (𝑍‘𝑋)) ∈ V
290		eleq1 2851	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 ∈ 𝐷 ↔ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷))
291	290	3anbi2d 1469	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ)))
292		oveq1 7434	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)))
293	292	eleq1d 2848	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
294	291, 293	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
295		fourierdlem41.dper	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
296	289, 294, 295	vtocl 3523	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
297	282, 288, 296	vtocl 3523	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
298	237, 278, 281, 297	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
299	236, 298	eqeltrd 2863	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ 𝐷)
300	299	ralrimiva 3157	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑦 ∈ 𝐷)
301		dfss3 3901	. . . . . . 7 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑦 ∈ 𝐷)
302	300, 301	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)
303		breq1 5108	. . . . . . . 8 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → (𝑦 < 𝑋 ↔ ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋))
304		oveq1 7434	. . . . . . . . 9 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → (𝑦(,)𝑋) = (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
305	304	sseq1d 3943	. . . . . . . 8 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → ((𝑦(,)𝑋) ⊆ 𝐷 ↔ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷))
306	303, 305	anbi12d 644	. . . . . . 7 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → ((𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ↔ (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋 ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)))
307	306	rspcev 3579	. . . . . 6 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ ∧ (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋 ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
308	200, 218, 302, 307	syl12anc 850	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
309	308	3exp 1137	. . . 4 ⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))))
310	309	rexlimdv 3164	. . 3 ⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷)))
311	193, 310	mpd 16	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
312		0zd 12715	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
313	3	nnzd 12729	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
314		1zzd 12737	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℤ)
315		0le1 11849	. . . . . . . . 9 ⊢ 0 ≤ 1
316	315	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 1)
317	3	nnge1d 12396	. . . . . . . 8 ⊢ (𝜑 → 1 ≤ 𝑀)
318	312, 313, 314, 316, 317	elfzd 13657	. . . . . . 7 ⊢ (𝜑 → 1 ∈ (0...𝑀))
319	101, 318	ffvelcdmd 7093	. . . . . 6 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ)
320	133, 52	resubcld 11754	. . . . . 6 ⊢ (𝜑 → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
321	319, 320	resubcld 11754	. . . . 5 ⊢ (𝜑 → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
322	321	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
323	38	recnd 11347	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
324	323, 222	pncand 11680	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
325	324	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
326	43	oveq2i 7438	. . . . . . . . . . 11 ⊢ (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴))
327	326	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴)))
328	40	recnd 11347	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
329	323, 328	pncan3d 11682	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
330	329	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
331		id 23	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑋) = 𝐵 → (𝐸‘𝑋) = 𝐵)
332	331	eqcomd 2769	. . . . . . . . . . 11 ⊢ ((𝐸‘𝑋) = 𝐵 → 𝐵 = (𝐸‘𝑋))
333	332	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝐵 = (𝐸‘𝑋))
334	327, 330, 333	3eqtrrd 2803	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐸‘𝑋) = (𝐴 + 𝑇))
335	334	oveq1d 7442	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐸‘𝑋) − 𝑇) = ((𝐴 + 𝑇) − 𝑇))
336	33	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = 𝐴)
337	325, 335, 336	3eqtr4rd 2809	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = ((𝐸‘𝑋) − 𝑇))
338	337	oveq1d 7442	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) = (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)))
339	136	recnd 11347	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℂ)
340	339, 214, 222	nnncan2d 11714	. . . . . . 7 ⊢ (𝜑 → (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)) = ((𝐸‘𝑋) − (𝑍‘𝑋)))
341	340	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)) = ((𝐸‘𝑋) − (𝑍‘𝑋)))
342	216	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
343	338, 341, 342	3eqtrrd 2803	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝑋 = ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)))
344	33, 38	eqeltrd 2863	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
345	3	nngt0d 12397	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
346		fzolb 13810	. . . . . . . . . 10 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
347	312, 313, 345, 346	syl3anbrc 1362	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
348		0re 11320	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
349		eleq1 2851	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
350	349	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
351		fveq2 6893	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
352		oveq1 7434	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
353	352	fveq2d 6897	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
354	351, 353	breq12d 5118	. . . . . . . . . . . 12 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
355	350, 354	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
356	355, 149	vtoclg 3520	. . . . . . . . . 10 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
357	348, 356	ax-mp 5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
358	347, 357	mpdan 700	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
359		0p1e1 12473	. . . . . . . . . 10 ⊢ (0 + 1) = 1
360	359	fveq2i 6896	. . . . . . . . 9 ⊢ (𝑄‘(0 + 1)) = (𝑄‘1)
361	360	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
362	358, 361	breqtrd 5133	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘1))
363	344, 319, 320, 362	ltsub1dd 11938	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
364	363	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
365	343, 364	eqbrtrd 5129	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
366		elioore 13516	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) → 𝑦 ∈ ℝ)
367	132	eqcomd 2769	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = (𝑍‘𝑋))
368	367	negeqd 11561	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -(𝑍‘𝑋))
369	223, 368	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -(𝑍‘𝑋))
370	222	mullidd 11337	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · 𝑇) = 𝑇)
371	369, 370	oveq12d 7445	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)) = ( -(𝑍‘𝑋) + 𝑇))
372	221	negcld 11666	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℂ)
373		1cnd 11312	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
374	372, 373, 222	adddird 11344	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇) = (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)))
375	214, 222	negsubdid 11694	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝑍‘𝑋) − 𝑇) = ( -(𝑍‘𝑋) + 𝑇))
376	371, 374, 375	3eqtr4d 2808	. . . . . . . . . . . 12 ⊢ (𝜑 → (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇) = -((𝑍‘𝑋) − 𝑇))
377	376	oveq2d 7443	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)))
378	377	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)))
379	320	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
380	226, 379	readdcld 11348	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
381	380	recnd 11347	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℂ)
382	379	recnd 11347	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑍‘𝑋) − 𝑇) ∈ ℂ)
383	381, 382	negsubd 11685	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) − ((𝑍‘𝑋) − 𝑇)))
384	232, 382	pncand 11680	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) − ((𝑍‘𝑋) − 𝑇)) = 𝑦)
385	378, 383, 384	3eqtrrd 2803	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
386	366, 385	sylan2 605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
387	386	adantlr 728	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
388		simpll 779	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝜑)
389	361	eqcomd 2769	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘1) = (𝑄‘(0 + 1)))
390	389	oveq2d 7443	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
391	351, 353	oveq12d 7445	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 0 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
392	391	sseq1d 3943	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 0 → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷 ↔ ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
393	350, 392	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)))
394	393, 238	vtoclg 3520	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
395	348, 394	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
396	347, 395	mpdan 700	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
397	390, 396	eqsstrd 3946	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
398	397	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
399	33, 39	eqeltrd 2863	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ^*)
400	399	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) ∈ ℝ^*)
401	319	rexrd 11369	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ^*)
402	401	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ^*)
403	366, 380	sylan2 605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
404	403	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
405	339, 213, 214	subaddd 11697	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐸‘𝑋) − 𝑋) = (𝑍‘𝑋) ↔ (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋)))
406	269, 405	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸‘𝑋) − 𝑋) = (𝑍‘𝑋))
407		oveq1 7434	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸‘𝑋) = 𝐵 → ((𝐸‘𝑋) − 𝑋) = (𝐵 − 𝑋))
408	406, 407	sylan9req 2819	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑍‘𝑋) = (𝐵 − 𝑋))
409	408	oveq1d 7442	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑍‘𝑋) − 𝑇) = ((𝐵 − 𝑋) − 𝑇))
410	409	oveq2d 7443	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) = (𝑋 + ((𝐵 − 𝑋) − 𝑇)))
411	127	recnd 11347	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℂ)
412	213, 411, 222	addsubassd 11699	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑋 + ((𝐵 − 𝑋) − 𝑇)))
413	412	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + ((𝐵 − 𝑋) − 𝑇)) = ((𝑋 + (𝐵 − 𝑋)) − 𝑇))
414	413	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋 + ((𝐵 − 𝑋) − 𝑇)) = ((𝑋 + (𝐵 − 𝑋)) − 𝑇))
415	328, 222, 323	subsub23d 46442	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 − 𝑇) = 𝐴 ↔ (𝐵 − 𝐴) = 𝑇))
416	58, 415	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 − 𝑇) = 𝐴)
417	213, 328	pncan3d 11682	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝐵 − 𝑋)) = 𝐵)
418	417	oveq1d 7442	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝐵 − 𝑇))
419	416, 418, 33	3eqtr4d 2808	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑄‘0))
420	419	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑄‘0))
421	410, 414, 420	3eqtrrd 2803	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = (𝑋 + ((𝑍‘𝑋) − 𝑇)))
422	421	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) = (𝑋 + ((𝑍‘𝑋) − 𝑇)))
423	74	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 ∈ ℝ)
424	366	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ ℝ)
425	320	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
426	251	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 ∈ ℝ^*)
427	321	rexrd 11369	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^*)
428	427	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^*)
429		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
430		ioogtlb 46646	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 < 𝑦)
431	426, 428, 429, 430	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 < 𝑦)
432	423, 424, 425, 431	ltadd1dd 11937	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
433	432	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
434	422, 433	eqbrtrd 5129	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
435		iooltub 46661	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
436	426, 428, 429, 435	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
437	319	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ)
438	424, 425, 437	ltaddsubd 11926	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1) ↔ 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
439	436, 438	mpbird 260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1))
440	439	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1))
441	400, 402, 404, 434, 440	eliood 46649	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ((𝑄‘0)(,)(𝑄‘1)))
442	398, 441	sseldd 3913	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷)
443	129	znegcld 12815	. . . . . . . . . 10 ⊢ (𝜑 → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
444	443	peano2zd 12816	. . . . . . . . 9 ⊢ (𝜑 → ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)
445	444	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)
446		ovex 7460	. . . . . . . . 9 ⊢ ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ V
447		eleq1 2851	. . . . . . . . . . 11 ⊢ (𝑘 = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (𝑘 ∈ ℤ ↔ ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ))
448	447	3anbi3d 1470	. . . . . . . . . 10 ⊢ (𝑘 = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)))
449		oveq1 7434	. . . . . . . . . . . 12 ⊢ (𝑘 = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (𝑘 · 𝑇) = (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇))
450	449	oveq2d 7443	. . . . . . . . . . 11 ⊢ (𝑘 = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
451	450	eleq1d 2848	. . . . . . . . . 10 ⊢ (𝑘 = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷))
452	448, 451	imbi12d 347	. . . . . . . . 9 ⊢ (𝑘 = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)))
453		ovex 7460	. . . . . . . . . 10 ⊢ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ V
454		eleq1 2851	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (𝑥 ∈ 𝐷 ↔ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷))
455	454	3anbi2d 1469	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ)))
456		oveq1 7434	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)))
457	456	eleq1d 2848	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷))
458	455, 457	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)))
459	453, 458, 295	vtocl 3523	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)
460	446, 452, 459	vtocl 3523	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
461	388, 442, 445, 460	syl3anc 1398	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (( -(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
462	387, 461	eqeltrd 2863	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ 𝐷)
463	462	ralrimiva 3157	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))𝑦 ∈ 𝐷)
464		dfss3 3901	. . . . 5 ⊢ ((𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))𝑦 ∈ 𝐷)
465	463, 464	sylibr 237	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)
466		breq2 5109	. . . . . 6 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → (𝑋 < 𝑦 ↔ 𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
467		oveq2 7435	. . . . . . 7 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
468	467	sseq1d 3943	. . . . . 6 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷))
469	466, 468	anbi12d 644	. . . . 5 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)))
470	469	rspcev 3579	. . . 4 ⊢ ((((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ ∧ (𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
471	322, 365, 465, 470	syl12anc 850	. . 3 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
472	15	adantlr 728	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋))
473		simp2 1155	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ (0...𝑀))
474	25	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℝ)
475	94	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ∈ ℝ)
476	96	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ≤ 𝑀)
477		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝑄‘𝑗) = (𝐸‘𝑋))
478	477	eqcomd 2769	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝐸‘𝑋) = (𝑄‘𝑗))
479	478	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘𝑗) = (𝐸‘𝑋) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = (𝑄‘𝑗))
480	479	3ad2antl3 1206	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = (𝑄‘𝑗))
481		fveq2 6893	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = 𝑗 → (𝑄‘𝑀) = (𝑄‘𝑗))
482	481	eqcomd 2769	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 = 𝑗 → (𝑄‘𝑗) = (𝑄‘𝑀))
483	482	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝑄‘𝑗) = (𝑄‘𝑀))
484	177	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → (𝑄‘𝑀) = 𝐵)
485	484	3ad2antl1 1204	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝑄‘𝑀) = 𝐵)
486	480, 483, 485	3eqtrd 2802	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = 𝐵)
487		neneq 2964	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸‘𝑋) ≠ 𝐵 → ¬ (𝐸‘𝑋) = 𝐵)
488	487	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → ¬ (𝐸‘𝑋) = 𝐵)
489	488	3ad2antl1 1204	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → ¬ (𝐸‘𝑋) = 𝐵)
490	486, 489	pm2.65da 829	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ¬ 𝑀 = 𝑗)
491	490	neqned 2965	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ≠ 𝑗)
492	474, 475, 476, 491	leneltd 11474	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 < 𝑀)
493		elfzfzo 46432	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) ↔ (𝑗 ∈ (0...𝑀) ∧ 𝑗 < 𝑀))
494	473, 492, 493	sylanbrc 595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ (0..^𝑀))
495	114	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ^*)
496	495	3adant3 1150	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ∈ ℝ^*)
497		simp1l 1216	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝜑)
498	101	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
499		fzofzp1 13909	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
500	499	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
501	498, 500	ffvelcdmd 7093	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
502	501	rexrd 11369	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ^*)
503	497, 494, 502	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 + 1)) ∈ ℝ^*)
504	138	3adant1r 1196	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ^*)
505	37, 157	eqbrtrd 5129	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
506	505	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
507	506	3adant2 1149	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
508	478	3ad2ant3 1153	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) = (𝑄‘𝑗))
509		eleq1 2851	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
510	509	anbi2d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0..^𝑀))))
511		fveq2 6893	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
512		oveq1 7434	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
513	512	fveq2d 6897	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
514	511, 513	breq12d 5118	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑗) < (𝑄‘(𝑗 + 1))))
515	510, 514	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))))
516	515, 149	chvarvv 2023	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
517	497, 494, 516	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
518	508, 517	eqbrtrd 5129	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) < (𝑄‘(𝑗 + 1)))
519	496, 503, 504, 507, 518	elicod 13536	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1))))
520	511, 513	oveq12d 7445	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1))))
521	520	eleq2d 2849	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) ↔ (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1)))))
522	521	rspcev 3579	. . . . . . . . . 10 ⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
523	494, 519, 522	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
524	523	3exp 1137	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))))
525	524	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))))
526	525	rexlimdv 3164	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
527	472, 526	mpd 16	. . . . 5 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
528		ioossico 13579	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))
529		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
530	528, 529	sselid 3910	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
531	530	ex 418	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
532	531	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
533	532	reximdva 3178	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
534	187, 533	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
535	534	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
536	527, 535	pm2.61dan 825	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
537	205, 247	resubcld 11754	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
538	537	3adant3 1150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
539	216	eqcomd 2769	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ((𝐸‘𝑋) − (𝑍‘𝑋)))
540	539	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 = ((𝐸‘𝑋) − (𝑍‘𝑋)))
541	136	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ)
542	205	3adant3 1150	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
543	133	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑍‘𝑋) ∈ ℝ)
544	197	rexrd 11369	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
545	544	3adant3 1150	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
546	206	3adant3 1150	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
547		simp3 1156	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
548		icoltub 46659	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) < (𝑄‘(𝑖 + 1)))
549	545, 546, 547, 548	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) < (𝑄‘(𝑖 + 1)))
550	541, 542, 543, 549	ltsub1dd 11938	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝐸‘𝑋) − (𝑍‘𝑋)) < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
551	540, 550	eqbrtrd 5129	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
552		elioore 13516	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) → 𝑦 ∈ ℝ)
553	552, 234	sylan2 605	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
554	553	3ad2antl1 1204	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
555		simpl1 1210	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝜑)
556	238	3adant3 1150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
557	556	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
558	545	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ∈ ℝ^*)
559	546	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
560	552	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ ℝ)
561	133	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑍‘𝑋) ∈ ℝ)
562	560, 561	readdcld 11348	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
563	562	3ad2antl1 1204	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
564	197	3adant3 1150	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
565	564	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ∈ ℝ)
566	555, 136	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) ∈ ℝ)
567		icogelb 13537	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
568	545, 546, 547, 567	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
569	568	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
570	135	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
571	74	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 ∈ ℝ)
572	552	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ ℝ)
573	133	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑍‘𝑋) ∈ ℝ)
574	251	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 ∈ ℝ^*)
575	537	rexrd 11369	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^*)
576	575	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^*)
577		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
578		ioogtlb 46646	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 < 𝑦)
579	574, 576, 577, 578	syl3anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 < 𝑦)
580	571, 572, 573, 579	ltadd1dd 11937	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑋 + (𝑍‘𝑋)) < (𝑦 + (𝑍‘𝑋)))
581	570, 580	eqbrtrd 5129	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) < (𝑦 + (𝑍‘𝑋)))
582	581	3adantl3 1187	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) < (𝑦 + (𝑍‘𝑋)))
583	565, 566, 563, 569, 582	lelttrd 11478	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
584	537	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
585		iooltub 46661	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
586	574, 576, 577, 585	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
587	572, 584, 573, 586	ltadd1dd 11937	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)))
588	205	recnd 11347	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
589	214	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℂ)
590	588, 589	npcand 11683	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)) = (𝑄‘(𝑖 + 1)))
591	590	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)) = (𝑄‘(𝑖 + 1)))
592	587, 591	breqtrd 5133	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
593	592	3adantl3 1187	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
594	558, 559, 563, 583, 593	eliood 46649	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
595	557, 594	sseldd 3913	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ 𝐷)
596	555, 443	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
597	555, 595, 596, 297	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
598	554, 597	eqeltrd 2863	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ 𝐷)
599	598	ralrimiva 3157	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))𝑦 ∈ 𝐷)
600		dfss3 3901	. . . . . . . . 9 ⊢ ((𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))𝑦 ∈ 𝐷)
601	599, 600	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)
602		breq2 5109	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → (𝑋 < 𝑦 ↔ 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
603		oveq2 7435	. . . . . . . . . . 11 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
604	603	sseq1d 3943	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷))
605	602, 604	anbi12d 644	. . . . . . . . 9 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)))
606	605	rspcev 3579	. . . . . . . 8 ⊢ ((((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ ∧ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
607	538, 551, 601, 606	syl12anc 850	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
608	607	3exp 1137	. . . . . 6 ⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
609	608	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
610	609	rexlimdv 3164	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
611	536, 610	mpd 16	. . 3 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
612	471, 611	pm2.61dane 3045	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
613	311, 612	jca 521	1 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2146 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 {crab 3415 ⊆ wss 3899 class class class wbr 5105 ↦ cmpt 5188 ran crn 5655 Fn wfn 6541 ⟶wf 6542 ‘cfv 6546 (class class class)co 7427 ↑_m cmap 8858 supcsup 9442 ℂcc 11208 ℝcr 11209 0cc0 11210 1c1 11211 + caddc 11213 · cmul 11215 ℝ^*cxr 11352 < clt 11353 ≤ cle 11354 − cmin 11551 -cneg 11552 / cdiv 11983 ℕcn 12345 ℤcz 12703 ℤ_≥cuz 12975 (,)cioo 13486 (,]cioc 13487 [,)cico 13488 [,]cicc 13489 ...cfz 13649 ..^cfzo 13798 ⌊cfl 13940

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-sep 5251 ax-nul 5262 ax-pow 5330 ax-pr 5394 ax-un 7758 ax-cnex 11266 ax-resscn 11267 ax-1cn 11268 ax-icn 11269 ax-addcl 11270 ax-addrcl 11271 ax-mulcl 11272 ax-mulrcl 11273 ax-mulcom 11274 ax-addass 11275 ax-mulass 11276 ax-distr 11277 ax-i2m1 11278 ax-1ne0 11279 ax-1rid 11280 ax-rnegex 11281 ax-rrecex 11282 ax-cnre 11283 ax-pre-lttri 11284 ax-pre-lttrn 11285 ax-pre-ltadd 11286 ax-pre-mulgt0 11287 ax-pre-sup 11288

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3455 df-sbc 3742 df-csb 3851 df-ss 3900 df-pss 4016 df-dif 4049 df-in 4093 df-un 4153 df-nul 4281 df-if 4485 df-pw 4561 df-sn 4588 df-pr 4590 df-op 4838 df-uni 4870 df-iun 4955 df-br 5106 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5549 df-eprel 5554 df-po 5562 df-so 5563 df-fr 5607 df-we 5609 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6310 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6500 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-riota 7384 df-ov 7430 df-oprab 7431 df-mpo 7432 df-om 7885 df-1st 8008 df-2nd 8009 df-frecs 8310 df-wrecs 8341 df-recs 8390 df-rdg 8429 df-1o 8487 df-er 8728 df-map 8860 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-sup 9444 df-inf 9445 df-pnf 11355 df-mnf 11356 df-xr 11357 df-ltxr 11358 df-le 11359 df-sub 11553 df-neg 11554 df-div 11984 df-nn 12346 df-n0 12617 df-z 12704 df-uz 12976 df-rp 13131 df-ioo 13490 df-ioc 13491 df-ico 13492 df-icc 13493 df-fz 13650 df-fzo 13799 df-fl 13942

This theorem is used by: fourierdlem113 47368

W3C validator