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