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 46157

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 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ran 𝑄)
2		fourierdlem41.q	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
3		fourierdlem41.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4		fourierdlem41.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
5	4	fourierdlem2 46118	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	3, 5	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
7	2, 6	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
8	7	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
9		elmapi 8868	. . . . . . . . 9 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10		ffn 6711	. . . . . . . . 9 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
11	8, 9, 10	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
12	11	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
13		fvelrnb 6944	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
14	12, 13	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
15	1, 14	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋))
16		0zd 12605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ∈ ℤ)
17		elfzelz 13546	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18	17	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℤ)
19		1zzd 12628	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 1 ∈ ℤ)
20	18, 19	zsubcld 12707	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ ℤ)
21		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝜑)
22		elfzle1 13549	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
23	22	anim1i 615	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗))
24		0red 11243	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 ∈ ℝ)
25	17	zred 12702	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
26	25	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 ∈ ℝ)
27	24, 26	eqleltd 11384	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 = 𝑗 ↔ (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗)))
28	23, 27	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 = 𝑗)
29	28	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
30	29	adantll 714	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
31		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑄‘𝑗) = (𝑄‘0))
32	7	simprld 771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
33	32	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
34	31, 33	sylan9eqr 2793	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝑄‘𝑗) = 𝐴)
35	21, 30, 34	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) = 𝐴)
36	35	3adantl3 1169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) = 𝐴)
37		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝐸‘𝑋))
38		fourierdlem41.a	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ ℝ)
39	38	rexrd 11290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
40		fourierdlem41.b	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
41	40	rexrd 11290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
42		fourierdlem41.altb	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐴 < 𝐵)
43		fourierdlem41.t	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑇 = (𝐵 − 𝐴)
44		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
45	38, 40, 42, 43, 44	fourierdlem4 46120	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵))
46		fourierdlem41.e	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥)))
47	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))))
48		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
49	40	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
50	49, 48	resubcld 11670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ)
51	40, 38	resubcld 11670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
52	43, 51	eqeltrid 2839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝑇 ∈ ℝ)
53	52	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
54		0red 11243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 0 ∈ ℝ)
55	38, 40	posdifd 11829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
56	42, 55	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
57	43	eqcomi 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐵 − 𝐴) = 𝑇
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
59	56, 58	breqtrd 5150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 0 < 𝑇)
60	54, 59	gtned 11375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝑇 ≠ 0)
61	60	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0)
62	50, 53, 61	redivcld 12074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ)
63	62	flcld 13820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
64	63	zred 12702	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
65	64, 53	remulcld 11270	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
66		fourierdlem41.z	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
67	66	fvmpt2 7002	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ) → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
68	48, 65, 67	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
69	68	oveq2d 7426	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝑍‘𝑥)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
70	69	mpteq2dva 5219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
71	47, 70	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
72	71	feq1d 6695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐸:ℝ⟶(𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵)))
73	45, 72	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
74		fourierdlem41.x	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑋 ∈ ℝ)
75	73, 74	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (𝐴(,]𝐵))
76		iocgtlb 45511	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸‘𝑋))
77	39, 41, 75, 76	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < (𝐸‘𝑋))
78	38, 77	gtned 11375	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸‘𝑋) ≠ 𝐴)
79	78	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≠ 𝐴)
80	37, 79	eqnetrd 3000	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≠ 𝐴)
81	80	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) ≠ 𝐴)
82	81	3adantl2 1168	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) ≠ 𝐴)
83	82	neneqd 2938	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → ¬ (𝑄‘𝑗) = 𝐴)
84	36, 83	condan 817	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 < 𝑗)
85		zltlem1 12650	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
86	16, 18, 85	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
87	84, 86	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ≤ (𝑗 − 1))
88		eluz2 12863	. . . . . . . . . . 11 ⊢ ((𝑗 − 1) ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ ∧ 0 ≤ (𝑗 − 1)))
89	16, 20, 87, 88	syl3anbrc 1344	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (ℤ_≥‘0))
90		elfzel2 13544	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
91	90	3ad2ant2 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ∈ ℤ)
92		1red 11241	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 1 ∈ ℝ)
93	25, 92	resubcld 11670	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
94	90	zred 12702	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
95	25	ltm1d 12179	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
96		elfzle2 13550	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
97	93, 25, 94, 95, 96	ltletrd 11400	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
98	97	3ad2ant2 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) < 𝑀)
99		elfzo2 13684	. . . . . . . . . 10 ⊢ ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ_≥‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
100	89, 91, 98, 99	syl3anbrc 1344	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
101	8, 9	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
102	101	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
103	93, 94, 97	ltled 11388	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
104	103	3ad2ant2 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ≤ 𝑀)
105	16, 91, 20, 87, 104	elfzd 13537	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
106	102, 105	ffvelcdmd 7080	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
107	106	rexrd 11290	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ^*)
108	25	recnd 11268	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
109		1cnd 11235	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
110	108, 109	npcand 11603	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
111	110	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
112	111	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
113	101	ffvelcdmda 7079	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
114	113	rexrd 11290	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ^*)
115	112, 114	eqeltrd 2835	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ^*)
116	115	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ^*)
117		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
118		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑍‘𝑥) = (𝑍‘𝑋))
119	117, 118	oveq12d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝑍‘𝑥)) = (𝑋 + (𝑍‘𝑋)))
120	119	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + (𝑍‘𝑥)) = (𝑋 + (𝑍‘𝑋)))
121	66	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
122		oveq2 7418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑋 → (𝐵 − 𝑥) = (𝐵 − 𝑋))
123	122	oveq1d 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑋 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑋) / 𝑇))
124	123	fveq2d 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑋 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑋) / 𝑇)))
125	124	oveq1d 7425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑋 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
126	125	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
127	40, 74	resubcld 11670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
128	127, 52, 60	redivcld 12074	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
129	128	flcld 13820	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
130	129	zred 12702	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℝ)
131	130, 52	remulcld 11270	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
132	121, 126, 74, 131	fvmptd 6998	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑍‘𝑋) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
133	132, 131	eqeltrd 2835	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍‘𝑋) ∈ ℝ)
134	74, 133	readdcld 11269	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + (𝑍‘𝑋)) ∈ ℝ)
135	47, 120, 74, 134	fvmptd 6998	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
136	135, 134	eqeltrd 2835	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ)
137	136	rexrd 11290	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ^*)
138	137	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ^*)
139		simp1 1136	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝜑)
140		ovex 7443	. . . . . . . . . . . . . 14 ⊢ (𝑗 − 1) ∈ V
141		eleq1 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
142	141	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 − 1) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
143		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑄‘𝑖) = (𝑄‘(𝑗 − 1)))
144		oveq1 7417	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
145	144	fveq2d 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
146	143, 145	breq12d 5137	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
147	142, 146	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑗 − 1) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
148	7	simprrd 773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
149	148	r19.21bi 3238	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
150	140, 147, 149	vtocl 3542	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
151	139, 100, 150	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
152	111	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
153	151, 152	breqtrd 5150	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘𝑗))
154		simp3 1138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝐸‘𝑋))
155	153, 154	breqtrd 5150	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸‘𝑋))
156	136	leidd 11808	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
157	156	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
158	37	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) = (𝑄‘𝑗))
159	157, 158	breqtrd 5150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
160	159	3adant2 1131	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
161	110	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
162	161	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑄‘𝑗) = (𝑄‘((𝑗 − 1) + 1)))
163	162	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝑄‘((𝑗 − 1) + 1)))
164	160, 163	breqtrd 5150	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘((𝑗 − 1) + 1)))
165	107, 116, 138, 155, 164	eliocd 45516	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
166	143, 145	oveq12d 7428	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
167	166	eleq2d 2821	. . . . . . . . . 10 ⊢ (𝑖 = (𝑗 − 1) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
168	167	rspcev 3606	. . . . . . . . 9 ⊢ (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
169	100, 165, 168	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
170	169	3exp 1119	. . . . . . 7 ⊢ (𝜑 → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))))
171	170	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))))
172	171	rexlimdv 3140	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
173	15, 172	mpd 15	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
174	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
175	101	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
176		iocssicc 13459	. . . . . . . 8 ⊢ ((𝑄‘0)(,](𝑄‘𝑀)) ⊆ ((𝑄‘0)[,](𝑄‘𝑀))
177	32	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
178	33, 177	oveq12d 7428	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄‘0)(,](𝑄‘𝑀)) = (𝐴(,]𝐵))
179	75, 178	eleqtrrd 2838	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ((𝑄‘0)(,](𝑄‘𝑀)))
180	176, 179	sselid 3961	. . . . . . 7 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
181	180	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
182		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ¬ (𝐸‘𝑋) ∈ ran 𝑄)
183		fveq2 6881	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗))
184	183	breq1d 5134	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → ((𝑄‘𝑘) < (𝐸‘𝑋) ↔ (𝑄‘𝑗) < (𝐸‘𝑋)))
185	184	cbvrabv 3431	. . . . . . 7 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}
186	185	supeq1i 9464	. . . . . 6 ⊢ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}, ℝ, < )
187	174, 175, 181, 182, 186	fourierdlem25 46141	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
188		ioossioc 45501	. . . . . . . 8 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))
189	188	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
190	189	sseld 3962	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
191	190	reximdva 3154	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
192	187, 191	mpd 15	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
193	173, 192	pm2.61dan 812	. . 3 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
194	101	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
195		elfzofz 13697	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
196	195	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
197	194, 196	ffvelcdmd 7080	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
198	197	3adant3 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
199	133	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍‘𝑋) ∈ ℝ)
200	198, 199	resubcld 11670	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ)
201	136	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ)
202	198	rexrd 11290	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
203		fzofzp1 13785	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
204	203	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
205	194, 204	ffvelcdmd 7080	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
206	205	rexrd 11290	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
207	206	3adant3 1132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
208		simp3 1138	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
209		iocgtlb 45511	. . . . . . . . 9 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝐸‘𝑋))
210	202, 207, 208, 209	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝐸‘𝑋))
211	198, 201, 199, 210	ltsub1dd 11854	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < ((𝐸‘𝑋) − (𝑍‘𝑋)))
212	135	oveq1d 7425	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸‘𝑋) − (𝑍‘𝑋)) = ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)))
213	74	recnd 11268	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℂ)
214	133	recnd 11268	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍‘𝑋) ∈ ℂ)
215	213, 214	pncand 11600	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = 𝑋)
216	212, 215	eqtrd 2771	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
217	216	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
218	211, 217	breqtrd 5150	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋)
219		elioore 13397	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
220	132	oveq2d 7426	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 + (𝑍‘𝑋)) = (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
221	130	recnd 11268	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℂ)
222	52	recnd 11268	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇 ∈ ℂ)
223	221, 222	mulneg1d 11695	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
224	220, 223	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
225	224	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
226		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
227	131	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
228	226, 227	readdcld 11269	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
229	228	recnd 11268	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℂ)
230	227	recnd 11268	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
231	229, 230	negsubd 11605	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
232	226	recnd 11268	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
233	232, 230	pncand 11600	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = 𝑦)
234	225, 231, 233	3eqtrrd 2776	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
235	219, 234	sylan2 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
236	235	3ad2antl1 1186	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
237		simpl1 1192	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝜑)
238		fourierdlem41.qssd	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
239	238	3adant3 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
240	239	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
241	202	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ^*)
242	207	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
243	219	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
244	133	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
245	243, 244	readdcld 11269	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
246	245	3ad2antl1 1186	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
247	133	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℝ)
248	197, 247	resubcld 11670	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ)
249	248	rexrd 11290	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^*)
250	249	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^*)
251	74	rexrd 11290	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
252	251	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ^*)
253		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
254		ioogtlb 45504	. . . . . . . . . . . . . . 15 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑋 ∈ ℝ^* ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦)
255	250, 252, 253, 254	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦)
256	197	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ)
257	133	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
258	219	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
259	256, 257, 258	ltsubaddd 11838	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦 ↔ (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋))))
260	255, 259	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
261	260	3adantl3 1169	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
262	237, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐸‘𝑋) ∈ ℝ)
263	205	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
264	263	3adantl3 1169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
265	74	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
266		iooltub 45519	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑋 ∈ ℝ^* ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 < 𝑋)
267	250, 252, 253, 266	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 < 𝑋)
268	258, 265, 257, 267	ltadd1dd 11853	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝑋 + (𝑍‘𝑋)))
269	135	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
270	269	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
271	268, 270	breqtrd 5150	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝐸‘𝑋))
272	271	3adantl3 1169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝐸‘𝑋))
273		iocleub 45512	. . . . . . . . . . . . . . 15 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
274	202, 207, 208, 273	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
275	274	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
276	246, 262, 264, 272, 275	ltletrd 11400	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
277	241, 242, 246, 261, 276	eliood 45507	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
278	240, 277	sseldd 3964	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ 𝐷)
279	237, 128	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
280	279	flcld 13820	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
281	280	znegcld 12704	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
282		negex 11485	. . . . . . . . . . 11 ⊢ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ V
283		eleq1 2823	. . . . . . . . . . . . 13 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
284	283	3anbi3d 1444	. . . . . . . . . . . 12 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)))
285		oveq1 7417	. . . . . . . . . . . . . 14 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
286	285	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
287	286	eleq1d 2820	. . . . . . . . . . . 12 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
288	284, 287	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
289		ovex 7443	. . . . . . . . . . . 12 ⊢ (𝑦 + (𝑍‘𝑋)) ∈ V
290		eleq1 2823	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 ∈ 𝐷 ↔ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷))
291	290	3anbi2d 1443	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ)))
292		oveq1 7417	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)))
293	292	eleq1d 2820	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
294	291, 293	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
295		fourierdlem41.dper	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
296	289, 294, 295	vtocl 3542	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
297	282, 288, 296	vtocl 3542	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
298	237, 278, 281, 297	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
299	236, 298	eqeltrd 2835	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ 𝐷)
300	299	ralrimiva 3133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑦 ∈ 𝐷)
301		dfss3 3952	. . . . . . 7 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑦 ∈ 𝐷)
302	300, 301	sylibr 234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)
303		breq1 5127	. . . . . . . 8 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → (𝑦 < 𝑋 ↔ ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋))
304		oveq1 7417	. . . . . . . . 9 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → (𝑦(,)𝑋) = (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
305	304	sseq1d 3995	. . . . . . . 8 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → ((𝑦(,)𝑋) ⊆ 𝐷 ↔ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷))
306	303, 305	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → ((𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ↔ (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋 ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)))
307	306	rspcev 3606	. . . . . 6 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ ∧ (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋 ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
308	200, 218, 302, 307	syl12anc 836	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
309	308	3exp 1119	. . . 4 ⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))))
310	309	rexlimdv 3140	. . 3 ⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷)))
311	193, 310	mpd 15	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
312		0zd 12605	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
313	3	nnzd 12620	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
314		1zzd 12628	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℤ)
315		0le1 11765	. . . . . . . . 9 ⊢ 0 ≤ 1
316	315	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 1)
317	3	nnge1d 12293	. . . . . . . 8 ⊢ (𝜑 → 1 ≤ 𝑀)
318	312, 313, 314, 316, 317	elfzd 13537	. . . . . . 7 ⊢ (𝜑 → 1 ∈ (0...𝑀))
319	101, 318	ffvelcdmd 7080	. . . . . 6 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ)
320	133, 52	resubcld 11670	. . . . . 6 ⊢ (𝜑 → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
321	319, 320	resubcld 11670	. . . . 5 ⊢ (𝜑 → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
322	321	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
323	38	recnd 11268	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
324	323, 222	pncand 11600	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
325	324	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
326	43	oveq2i 7421	. . . . . . . . . . 11 ⊢ (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴))
327	326	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴)))
328	40	recnd 11268	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
329	323, 328	pncan3d 11602	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
330	329	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
331		id 22	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑋) = 𝐵 → (𝐸‘𝑋) = 𝐵)
332	331	eqcomd 2742	. . . . . . . . . . 11 ⊢ ((𝐸‘𝑋) = 𝐵 → 𝐵 = (𝐸‘𝑋))
333	332	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝐵 = (𝐸‘𝑋))
334	327, 330, 333	3eqtrrd 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐸‘𝑋) = (𝐴 + 𝑇))
335	334	oveq1d 7425	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐸‘𝑋) − 𝑇) = ((𝐴 + 𝑇) − 𝑇))
336	33	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = 𝐴)
337	325, 335, 336	3eqtr4rd 2782	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = ((𝐸‘𝑋) − 𝑇))
338	337	oveq1d 7425	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) = (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)))
339	136	recnd 11268	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℂ)
340	339, 214, 222	nnncan2d 11634	. . . . . . 7 ⊢ (𝜑 → (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)) = ((𝐸‘𝑋) − (𝑍‘𝑋)))
341	340	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)) = ((𝐸‘𝑋) − (𝑍‘𝑋)))
342	216	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
343	338, 341, 342	3eqtrrd 2776	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝑋 = ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)))
344	33, 38	eqeltrd 2835	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
345	3	nngt0d 12294	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
346		fzolb 13687	. . . . . . . . . 10 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
347	312, 313, 345, 346	syl3anbrc 1344	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
348		0re 11242	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
349		eleq1 2823	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
350	349	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
351		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
352		oveq1 7417	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
353	352	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
354	351, 353	breq12d 5137	. . . . . . . . . . . 12 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
355	350, 354	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
356	355, 149	vtoclg 3538	. . . . . . . . . 10 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
357	348, 356	ax-mp 5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
358	347, 357	mpdan 687	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
359		0p1e1 12367	. . . . . . . . . 10 ⊢ (0 + 1) = 1
360	359	fveq2i 6884	. . . . . . . . 9 ⊢ (𝑄‘(0 + 1)) = (𝑄‘1)
361	360	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
362	358, 361	breqtrd 5150	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘1))
363	344, 319, 320, 362	ltsub1dd 11854	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
364	363	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
365	343, 364	eqbrtrd 5146	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
366		elioore 13397	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) → 𝑦 ∈ ℝ)
367	132	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = (𝑍‘𝑋))
368	367	negeqd 11481	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -(𝑍‘𝑋))
369	223, 368	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -(𝑍‘𝑋))
370	222	mullidd 11258	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · 𝑇) = 𝑇)
371	369, 370	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)) = (-(𝑍‘𝑋) + 𝑇))
372	221	negcld 11586	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℂ)
373		1cnd 11235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
374	372, 373, 222	adddird 11265	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇) = ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)))
375	214, 222	negsubdid 11614	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝑍‘𝑋) − 𝑇) = (-(𝑍‘𝑋) + 𝑇))
376	371, 374, 375	3eqtr4d 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇) = -((𝑍‘𝑋) − 𝑇))
377	376	oveq2d 7426	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)))
378	377	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)))
379	320	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
380	226, 379	readdcld 11269	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
381	380	recnd 11268	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℂ)
382	379	recnd 11268	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑍‘𝑋) − 𝑇) ∈ ℂ)
383	381, 382	negsubd 11605	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) − ((𝑍‘𝑋) − 𝑇)))
384	232, 382	pncand 11600	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) − ((𝑍‘𝑋) − 𝑇)) = 𝑦)
385	378, 383, 384	3eqtrrd 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
386	366, 385	sylan2 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
387	386	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
388		simpll 766	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝜑)
389	361	eqcomd 2742	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘1) = (𝑄‘(0 + 1)))
390	389	oveq2d 7426	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
391	351, 353	oveq12d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 0 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
392	391	sseq1d 3995	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 0 → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷 ↔ ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
393	350, 392	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)))
394	393, 238	vtoclg 3538	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
395	348, 394	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
396	347, 395	mpdan 687	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
397	390, 396	eqsstrd 3998	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
398	397	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
399	33, 39	eqeltrd 2835	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ^*)
400	399	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) ∈ ℝ^*)
401	319	rexrd 11290	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ^*)
402	401	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ^*)
403	366, 380	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
404	403	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
405	339, 213, 214	subaddd 11617	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐸‘𝑋) − 𝑋) = (𝑍‘𝑋) ↔ (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋)))
406	269, 405	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸‘𝑋) − 𝑋) = (𝑍‘𝑋))
407		oveq1 7417	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸‘𝑋) = 𝐵 → ((𝐸‘𝑋) − 𝑋) = (𝐵 − 𝑋))
408	406, 407	sylan9req 2792	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑍‘𝑋) = (𝐵 − 𝑋))
409	408	oveq1d 7425	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑍‘𝑋) − 𝑇) = ((𝐵 − 𝑋) − 𝑇))
410	409	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) = (𝑋 + ((𝐵 − 𝑋) − 𝑇)))
411	127	recnd 11268	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℂ)
412	213, 411, 222	addsubassd 11619	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑋 + ((𝐵 − 𝑋) − 𝑇)))
413	412	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + ((𝐵 − 𝑋) − 𝑇)) = ((𝑋 + (𝐵 − 𝑋)) − 𝑇))
414	413	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋 + ((𝐵 − 𝑋) − 𝑇)) = ((𝑋 + (𝐵 − 𝑋)) − 𝑇))
415	328, 222, 323	subsub23d 45296	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 − 𝑇) = 𝐴 ↔ (𝐵 − 𝐴) = 𝑇))
416	58, 415	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 − 𝑇) = 𝐴)
417	213, 328	pncan3d 11602	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝐵 − 𝑋)) = 𝐵)
418	417	oveq1d 7425	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝐵 − 𝑇))
419	416, 418, 33	3eqtr4d 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑄‘0))
420	419	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑄‘0))
421	410, 414, 420	3eqtrrd 2776	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = (𝑋 + ((𝑍‘𝑋) − 𝑇)))
422	421	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) = (𝑋 + ((𝑍‘𝑋) − 𝑇)))
423	74	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 ∈ ℝ)
424	366	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ ℝ)
425	320	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
426	251	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 ∈ ℝ^*)
427	321	rexrd 11290	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^*)
428	427	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^*)
429		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
430		ioogtlb 45504	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 < 𝑦)
431	426, 428, 429, 430	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 < 𝑦)
432	423, 424, 425, 431	ltadd1dd 11853	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
433	432	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
434	422, 433	eqbrtrd 5146	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
435		iooltub 45519	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
436	426, 428, 429, 435	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
437	319	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ)
438	424, 425, 437	ltaddsubd 11842	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1) ↔ 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
439	436, 438	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1))
440	439	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1))
441	400, 402, 404, 434, 440	eliood 45507	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ((𝑄‘0)(,)(𝑄‘1)))
442	398, 441	sseldd 3964	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷)
443	129	znegcld 12704	. . . . . . . . . 10 ⊢ (𝜑 → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
444	443	peano2zd 12705	. . . . . . . . 9 ⊢ (𝜑 → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)
445	444	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)
446		ovex 7443	. . . . . . . . 9 ⊢ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ V
447		eleq1 2823	. . . . . . . . . . 11 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (𝑘 ∈ ℤ ↔ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ))
448	447	3anbi3d 1444	. . . . . . . . . 10 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)))
449		oveq1 7417	. . . . . . . . . . . 12 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (𝑘 · 𝑇) = ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇))
450	449	oveq2d 7426	. . . . . . . . . . 11 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
451	450	eleq1d 2820	. . . . . . . . . 10 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷))
452	448, 451	imbi12d 344	. . . . . . . . 9 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)))
453		ovex 7443	. . . . . . . . . 10 ⊢ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ V
454		eleq1 2823	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (𝑥 ∈ 𝐷 ↔ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷))
455	454	3anbi2d 1443	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ)))
456		oveq1 7417	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)))
457	456	eleq1d 2820	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷))
458	455, 457	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)))
459	453, 458, 295	vtocl 3542	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)
460	446, 452, 459	vtocl 3542	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
461	388, 442, 445, 460	syl3anc 1373	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
462	387, 461	eqeltrd 2835	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ 𝐷)
463	462	ralrimiva 3133	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))𝑦 ∈ 𝐷)
464		dfss3 3952	. . . . 5 ⊢ ((𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))𝑦 ∈ 𝐷)
465	463, 464	sylibr 234	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)
466		breq2 5128	. . . . . 6 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → (𝑋 < 𝑦 ↔ 𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
467		oveq2 7418	. . . . . . 7 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
468	467	sseq1d 3995	. . . . . 6 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷))
469	466, 468	anbi12d 632	. . . . 5 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)))
470	469	rspcev 3606	. . . 4 ⊢ ((((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ ∧ (𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
471	322, 365, 465, 470	syl12anc 836	. . 3 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
472	15	adantlr 715	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋))
473		simp2 1137	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ (0...𝑀))
474	25	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℝ)
475	94	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ∈ ℝ)
476	96	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ≤ 𝑀)
477		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝑄‘𝑗) = (𝐸‘𝑋))
478	477	eqcomd 2742	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝐸‘𝑋) = (𝑄‘𝑗))
479	478	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘𝑗) = (𝐸‘𝑋) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = (𝑄‘𝑗))
480	479	3ad2antl3 1188	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = (𝑄‘𝑗))
481		fveq2 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = 𝑗 → (𝑄‘𝑀) = (𝑄‘𝑗))
482	481	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 = 𝑗 → (𝑄‘𝑗) = (𝑄‘𝑀))
483	482	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝑄‘𝑗) = (𝑄‘𝑀))
484	177	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → (𝑄‘𝑀) = 𝐵)
485	484	3ad2antl1 1186	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝑄‘𝑀) = 𝐵)
486	480, 483, 485	3eqtrd 2775	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = 𝐵)
487		neneq 2939	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸‘𝑋) ≠ 𝐵 → ¬ (𝐸‘𝑋) = 𝐵)
488	487	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → ¬ (𝐸‘𝑋) = 𝐵)
489	488	3ad2antl1 1186	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → ¬ (𝐸‘𝑋) = 𝐵)
490	486, 489	pm2.65da 816	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ¬ 𝑀 = 𝑗)
491	490	neqned 2940	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ≠ 𝑗)
492	474, 475, 476, 491	leneltd 11394	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 < 𝑀)
493		elfzfzo 45285	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) ↔ (𝑗 ∈ (0...𝑀) ∧ 𝑗 < 𝑀))
494	473, 492, 493	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ (0..^𝑀))
495	114	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ^*)
496	495	3adant3 1132	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ∈ ℝ^*)
497		simp1l 1198	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝜑)
498	101	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
499		fzofzp1 13785	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
500	499	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
501	498, 500	ffvelcdmd 7080	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
502	501	rexrd 11290	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ^*)
503	497, 494, 502	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 + 1)) ∈ ℝ^*)
504	138	3adant1r 1178	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ^*)
505	37, 157	eqbrtrd 5146	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
506	505	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
507	506	3adant2 1131	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
508	478	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) = (𝑄‘𝑗))
509		eleq1 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
510	509	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0..^𝑀))))
511		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
512		oveq1 7417	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
513	512	fveq2d 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
514	511, 513	breq12d 5137	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑗) < (𝑄‘(𝑗 + 1))))
515	510, 514	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))))
516	515, 149	chvarvv 1989	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
517	497, 494, 516	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
518	508, 517	eqbrtrd 5146	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) < (𝑄‘(𝑗 + 1)))
519	496, 503, 504, 507, 518	elicod 13417	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1))))
520	511, 513	oveq12d 7428	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1))))
521	520	eleq2d 2821	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) ↔ (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1)))))
522	521	rspcev 3606	. . . . . . . . . 10 ⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
523	494, 519, 522	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
524	523	3exp 1119	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))))
525	524	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))))
526	525	rexlimdv 3140	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
527	472, 526	mpd 15	. . . . 5 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
528		ioossico 13460	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))
529		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
530	528, 529	sselid 3961	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
531	530	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
532	531	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
533	532	reximdva 3154	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
534	187, 533	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
535	534	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
536	527, 535	pm2.61dan 812	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
537	205, 247	resubcld 11670	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
538	537	3adant3 1132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
539	216	eqcomd 2742	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ((𝐸‘𝑋) − (𝑍‘𝑋)))
540	539	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 = ((𝐸‘𝑋) − (𝑍‘𝑋)))
541	136	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ)
542	205	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
543	133	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑍‘𝑋) ∈ ℝ)
544	197	rexrd 11290	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
545	544	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
546	206	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
547		simp3 1138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
548		icoltub 45517	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) < (𝑄‘(𝑖 + 1)))
549	545, 546, 547, 548	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) < (𝑄‘(𝑖 + 1)))
550	541, 542, 543, 549	ltsub1dd 11854	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝐸‘𝑋) − (𝑍‘𝑋)) < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
551	540, 550	eqbrtrd 5146	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
552		elioore 13397	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) → 𝑦 ∈ ℝ)
553	552, 234	sylan2 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
554	553	3ad2antl1 1186	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
555		simpl1 1192	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝜑)
556	238	3adant3 1132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
557	556	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
558	545	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ∈ ℝ^*)
559	546	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
560	552	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ ℝ)
561	133	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑍‘𝑋) ∈ ℝ)
562	560, 561	readdcld 11269	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
563	562	3ad2antl1 1186	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
564	197	3adant3 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
565	564	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ∈ ℝ)
566	555, 136	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) ∈ ℝ)
567		icogelb 13418	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
568	545, 546, 547, 567	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
569	568	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
570	135	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
571	74	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 ∈ ℝ)
572	552	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ ℝ)
573	133	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑍‘𝑋) ∈ ℝ)
574	251	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 ∈ ℝ^*)
575	537	rexrd 11290	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^*)
576	575	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^*)
577		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
578		ioogtlb 45504	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 < 𝑦)
579	574, 576, 577, 578	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 < 𝑦)
580	571, 572, 573, 579	ltadd1dd 11853	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑋 + (𝑍‘𝑋)) < (𝑦 + (𝑍‘𝑋)))
581	570, 580	eqbrtrd 5146	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) < (𝑦 + (𝑍‘𝑋)))
582	581	3adantl3 1169	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) < (𝑦 + (𝑍‘𝑋)))
583	565, 566, 563, 569, 582	lelttrd 11398	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
584	537	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
585		iooltub 45519	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
586	574, 576, 577, 585	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
587	572, 584, 573, 586	ltadd1dd 11853	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)))
588	205	recnd 11268	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
589	214	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℂ)
590	588, 589	npcand 11603	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)) = (𝑄‘(𝑖 + 1)))
591	590	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)) = (𝑄‘(𝑖 + 1)))
592	587, 591	breqtrd 5150	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
593	592	3adantl3 1169	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
594	558, 559, 563, 583, 593	eliood 45507	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
595	557, 594	sseldd 3964	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ 𝐷)
596	555, 443	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
597	555, 595, 596, 297	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
598	554, 597	eqeltrd 2835	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ 𝐷)
599	598	ralrimiva 3133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))𝑦 ∈ 𝐷)
600		dfss3 3952	. . . . . . . . 9 ⊢ ((𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))𝑦 ∈ 𝐷)
601	599, 600	sylibr 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)
602		breq2 5128	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → (𝑋 < 𝑦 ↔ 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
603		oveq2 7418	. . . . . . . . . . 11 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
604	603	sseq1d 3995	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷))
605	602, 604	anbi12d 632	. . . . . . . . 9 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)))
606	605	rspcev 3606	. . . . . . . 8 ⊢ ((((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ ∧ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
607	538, 551, 601, 606	syl12anc 836	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
608	607	3exp 1119	. . . . . 6 ⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
609	608	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
610	609	rexlimdv 3140	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
611	536, 610	mpd 15	. . 3 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
612	471, 611	pm2.61dane 3020	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
613	311, 612	jca 511	1 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 ∃wrex 3061 {crab 3420 ⊆ wss 3931 class class class wbr 5124 ↦ cmpt 5206 ran crn 5660 Fn wfn 6531 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ↑_m cmap 8845 supcsup 9457 ℂcc 11132 ℝcr 11133 0cc0 11134 1c1 11135 + caddc 11137 · cmul 11139 ℝ^*cxr 11273 < clt 11274 ≤ cle 11275 − cmin 11471 -cneg 11472 / cdiv 11899 ℕcn 12245 ℤcz 12593 ℤ_≥cuz 12857 (,)cioo 13367 (,]cioc 13368 [,)cico 13369 [,]cicc 13370 ...cfz 13529 ..^cfzo 13676 ⌊cfl 13812

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-er 8724 df-map 8847 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-sup 9459 df-inf 9460 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-n0 12507 df-z 12594 df-uz 12858 df-rp 13014 df-ioo 13371 df-ioc 13372 df-ico 13373 df-icc 13374 df-fz 13530 df-fzo 13677 df-fl 13814

This theorem is referenced by: fourierdlem113 46228

W3C validator