Metamath Proof Explorer

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 ffvelrnd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) )
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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 sseldi ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ( ( 𝑄 ‘ 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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 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 mulid2d ⊢ ( 𝜑 → ( 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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 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 ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ( 𝑦 < 𝑋 ∧ ( 𝑦 (,) 𝑋 ) ⊆ 𝐷 ) ∧ ∃ 𝑦 ∈ ℝ ( 𝑋 < 𝑦 ∧ ( 𝑋 (,) 𝑦 ) ⊆ 𝐷 ) ) )