Theorem fourierdlem41

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)

	Ref	Expression
Hypotheses	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	fourierdlem41	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ( 𝑦 < 𝑋 ∧ ( 𝑦 (,) 𝑋 ) ⊆ 𝐷 ) ∧ ∃ 𝑦 ∈ ℝ ( 𝑋 < 𝑦 ∧ ( 𝑋 (,) 𝑦 ) ⊆ 𝐷 ) ) )

Proof

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