Metamath Proof Explorer

Theorem fourierdlem64

Description: The partition V is finer than Q , when Q is moved on the same interval where V lies. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem64.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem64.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem64.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem64.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem64.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem64.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
fourierdlem64.cltd ⊢ ( 𝜑 → 𝐶 < 𝐷 )
fourierdlem64.h ⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
fourierdlem64.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
fourierdlem64.v ⊢ 𝑉 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
fourierdlem64.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
fourierdlem64.l ⊢ 𝐿 = sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < )
fourierdlem64.i ⊢ 𝐼 = sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < )
Assertion fourierdlem64 ( 𝜑 → ( ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐿 ∈ ℤ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑙 ∈ ℤ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem64.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
2 fourierdlem64.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
3 fourierdlem64.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 fourierdlem64.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5 fourierdlem64.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6 fourierdlem64.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
7 fourierdlem64.cltd ⊢ ( 𝜑 → 𝐶 < 𝐷 )
8 fourierdlem64.h ⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
9 fourierdlem64.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
10 fourierdlem64.v ⊢ 𝑉 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
11 fourierdlem64.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
12 fourierdlem64.l ⊢ 𝐿 = sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < )
13 fourierdlem64.i ⊢ 𝐼 = sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < )
14 ssrab2 ⊢ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ( 0 ..^ 𝑀 )
15 fzossfz ⊢ ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
16 fzssz ⊢ ( 0 ... 𝑀 ) ⊆ ℤ
17 15 16 sstri ⊢ ( 0 ..^ 𝑀 ) ⊆ ℤ
18 14 17 sstri ⊢ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ℤ
19 18 a1i ⊢ ( 𝜑 → { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ℤ )
20 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
21 3 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
22 3 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
23 fzolb ⊢ ( 0 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
24 20 21 22 23 syl3anbrc ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑀 ) )
25 ssrab2 ⊢ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ℤ
26 25 a1i ⊢ ( 𝜑 → { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ℤ )
27 prssi ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → { 𝐶 , 𝐷 } ⊆ ℝ )
28 5 6 27 syl2anc ⊢ ( 𝜑 → { 𝐶 , 𝐷 } ⊆ ℝ )
29 ssrab2 ⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ⊆ ( 𝐶 [,] 𝐷 )
30 29 a1i ⊢ ( 𝜑 → { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ⊆ ( 𝐶 [,] 𝐷 ) )
31 5 6 iccssred ⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℝ )
32 30 31 sstrd ⊢ ( 𝜑 → { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ⊆ ℝ )
33 28 32 unssd ⊢ ( 𝜑 → ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ⊆ ℝ )
34 8 33 eqsstrid ⊢ ( 𝜑 → 𝐻 ⊆ ℝ )
35 eqid ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
36 1 2 3 4 5 6 7 35 8 9 10 fourierdlem54 ⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑉 ∈ ( ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) ‘ 𝑁 ) ) ∧ 𝑉 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) )
37 36 simprd ⊢ ( 𝜑 → 𝑉 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
38 isof1o ⊢ ( 𝑉 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) → 𝑉 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 )
39 f1of ⊢ ( 𝑉 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 → 𝑉 : ( 0 ... 𝑁 ) ⟶ 𝐻 )
40 37 38 39 3syl ⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑁 ) ⟶ 𝐻 )
41 elfzofz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
42 11 41 syl ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑁 ) )
43 40 42 ffvelrnd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝐽 ) ∈ 𝐻 )
44 34 43 sseldd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝐽 ) ∈ ℝ )
45 2 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
46 3 45 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
47 4 46 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
48 47 simpld ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
49 elmapi ⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
50 48 49 syl ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
51 3 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
52 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
53 51 52 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
54 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
55 53 54 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
56 50 55 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
57 44 56 resubcld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) ∈ ℝ )
58 2 3 4 fourierdlem11 ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
59 58 simp2d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
60 58 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
61 59 60 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
62 1 61 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
63 58 simp3d ⊢ ( 𝜑 → 𝐴 < 𝐵 )
64 60 59 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
65 63 64 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
66 65 1 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑇 )
67 66 gt0ne0d ⊢ ( 𝜑 → 𝑇 ≠ 0 )
68 57 62 67 redivcld ⊢ ( 𝜑 → ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ∈ ℝ )
69 btwnz ⊢ ( ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ∈ ℝ → ( ∃ 𝑘 ∈ ℤ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ∧ ∃ 𝑧 ∈ ℤ ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) < 𝑧 ) )
70 68 69 syl ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℤ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ∧ ∃ 𝑧 ∈ ℤ ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) < 𝑧 ) )
71 70 simpld ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℤ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) )
72 zre ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
73 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → ( 𝑄 ‘ 0 ) ∈ ℝ )
74 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → 𝑘 ∈ ℝ )
75 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → 𝑇 ∈ ℝ )
76 74 75 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
77 73 76 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ∈ ℝ )
78 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → ( 𝑉 ‘ 𝐽 ) ∈ ℝ )
79 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) )
80 57 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) ∈ ℝ )
81 62 66 elrpd ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
82 81 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → 𝑇 ∈ ℝ+ )
83 74 80 82 ltmuldivd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → ( ( 𝑘 · 𝑇 ) < ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) ↔ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) )
84 79 83 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → ( 𝑘 · 𝑇 ) < ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) )
85 56 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( 𝑄 ‘ 0 ) ∈ ℝ )
86 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → 𝑘 ∈ ℝ )
87 62 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → 𝑇 ∈ ℝ )
88 86 87 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
89 44 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( 𝑉 ‘ 𝐽 ) ∈ ℝ )
90 85 88 89 ltaddsub2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) < ( 𝑉 ‘ 𝐽 ) ↔ ( 𝑘 · 𝑇 ) < ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) ) )
91 90 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → ( ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) < ( 𝑉 ‘ 𝐽 ) ↔ ( 𝑘 · 𝑇 ) < ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) ) )
92 84 91 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) < ( 𝑉 ‘ 𝐽 ) )
93 77 78 92 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
94 93 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) → ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
95 72 94 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) → ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
96 95 reximdva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℤ 𝑘 < ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) → ∃ 𝑘 ∈ ℤ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
97 71 96 mpd ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℤ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
98 rabn0 ⊢ ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ≠ ∅ ↔ ∃ 𝑘 ∈ ℤ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
99 97 98 sylibr ⊢ ( 𝜑 → { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ≠ ∅ )
100 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ) → 𝜑 )
101 26 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ) → 𝑗 ∈ ℤ )
102 oveq1 ⊢ ( 𝑘 = 𝑗 → ( 𝑘 · 𝑇 ) = ( 𝑗 · 𝑇 ) )
103 102 oveq2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) = ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) )
104 103 breq1d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ↔ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
105 104 elrab ⊢ ( 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ↔ ( 𝑗 ∈ ℤ ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
106 105 simprbi ⊢ ( 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } → ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
107 106 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ) → ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
108 zre ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ℝ )
109 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
110 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( 𝑄 ‘ 0 ) ∈ ℝ )
111 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) → 𝑗 ∈ ℝ )
112 62 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) → 𝑇 ∈ ℝ )
113 111 112 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) → ( 𝑗 · 𝑇 ) ∈ ℝ )
114 113 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( 𝑗 · 𝑇 ) ∈ ℝ )
115 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( 𝑉 ‘ 𝐽 ) ∈ ℝ )
116 110 114 115 leaddsub2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ↔ ( 𝑗 · 𝑇 ) ≤ ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) ) )
117 109 116 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( 𝑗 · 𝑇 ) ≤ ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) )
118 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → 𝑗 ∈ ℝ )
119 57 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) ∈ ℝ )
120 81 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → 𝑇 ∈ ℝ+ )
121 118 119 120 lemuldivd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( ( 𝑗 · 𝑇 ) ≤ ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) ↔ 𝑗 ≤ ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) )
122 117 121 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → 𝑗 ≤ ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) )
123 108 122 sylanl2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝑗 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → 𝑗 ≤ ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) )
124 100 101 107 123 syl21anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ) → 𝑗 ≤ ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) )
125 124 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑗 ≤ ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) )
126 breq2 ⊢ ( 𝑏 = ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) → ( 𝑗 ≤ 𝑏 ↔ 𝑗 ≤ ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) )
127 126 ralbidv ⊢ ( 𝑏 = ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) → ( ∀ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑗 ≤ 𝑏 ↔ ∀ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑗 ≤ ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) )
128 127 rspcev ⊢ ( ( ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ∈ ℝ ∧ ∀ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑗 ≤ ( ( ( 𝑉 ‘ 𝐽 ) − ( 𝑄 ‘ 0 ) ) / 𝑇 ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑗 ≤ 𝑏 )
129 68 125 128 syl2anc ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑗 ≤ 𝑏 )
130 suprzcl ⊢ ( ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ℤ ∧ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ≠ ∅ ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑗 ≤ 𝑏 ) → sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } )
131 26 99 129 130 syl3anc ⊢ ( 𝜑 → sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } )
132 12 131 eqeltrid ⊢ ( 𝜑 → 𝐿 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } )
133 oveq1 ⊢ ( 𝑘 = 𝐿 → ( 𝑘 · 𝑇 ) = ( 𝐿 · 𝑇 ) )
134 133 oveq2d ⊢ ( 𝑘 = 𝐿 → ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) = ( ( 𝑄 ‘ 0 ) + ( 𝐿 · 𝑇 ) ) )
135 134 breq1d ⊢ ( 𝑘 = 𝐿 → ( ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ↔ ( ( 𝑄 ‘ 0 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
136 135 elrab ⊢ ( 𝐿 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ↔ ( 𝐿 ∈ ℤ ∧ ( ( 𝑄 ‘ 0 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
137 132 136 sylib ⊢ ( 𝜑 → ( 𝐿 ∈ ℤ ∧ ( ( 𝑄 ‘ 0 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
138 137 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
139 fveq2 ⊢ ( 𝑗 = 0 → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 0 ) )
140 139 oveq1d ⊢ ( 𝑗 = 0 → ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) = ( ( 𝑄 ‘ 0 ) + ( 𝐿 · 𝑇 ) ) )
141 140 breq1d ⊢ ( 𝑗 = 0 → ( ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ↔ ( ( 𝑄 ‘ 0 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
142 141 elrab ⊢ ( 0 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ↔ ( 0 ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑄 ‘ 0 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
143 24 138 142 sylanbrc ⊢ ( 𝜑 → 0 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } )
144 ne0i ⊢ ( 0 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } → { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ≠ ∅ )
145 143 144 syl ⊢ ( 𝜑 → { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ≠ ∅ )
146 3 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
147 14 a1i ⊢ ( 𝜑 → { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ( 0 ..^ 𝑀 ) )
148 147 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) )
149 elfzoelz ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑀 ) → 𝑘 ∈ ℤ )
150 149 zred ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑀 ) → 𝑘 ∈ ℝ )
151 150 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → 𝑘 ∈ ℝ )
152 146 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → 𝑀 ∈ ℝ )
153 elfzolt2 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑀 ) → 𝑘 < 𝑀 )
154 153 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → 𝑘 < 𝑀 )
155 151 152 154 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → 𝑘 ≤ 𝑀 )
156 148 155 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ) → 𝑘 ≤ 𝑀 )
157 156 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑘 ≤ 𝑀 )
158 breq2 ⊢ ( 𝑏 = 𝑀 → ( 𝑘 ≤ 𝑏 ↔ 𝑘 ≤ 𝑀 ) )
159 158 ralbidv ⊢ ( 𝑏 = 𝑀 → ( ∀ 𝑘 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑘 ≤ 𝑏 ↔ ∀ 𝑘 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑘 ≤ 𝑀 ) )
160 159 rspcev ⊢ ( ( 𝑀 ∈ ℝ ∧ ∀ 𝑘 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑘 ≤ 𝑀 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑘 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑘 ≤ 𝑏 )
161 146 157 160 syl2anc ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑘 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑘 ≤ 𝑏 )
162 suprzcl ⊢ ( ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ℤ ∧ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ≠ ∅ ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑘 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑘 ≤ 𝑏 ) → sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } )
163 19 145 161 162 syl3anc ⊢ ( 𝜑 → sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } )
164 14 163 sselid ⊢ ( 𝜑 → sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) ∈ ( 0 ..^ 𝑀 ) )
165 13 164 eqeltrid ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝑀 ) )
166 25 131 sselid ⊢ ( 𝜑 → sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) ∈ ℤ )
167 12 166 eqeltrid ⊢ ( 𝜑 → 𝐿 ∈ ℤ )
168 15 165 sselid ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... 𝑀 ) )
169 50 168 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ℝ )
170 167 zred ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
171 170 62 remulcld ⊢ ( 𝜑 → ( 𝐿 · 𝑇 ) ∈ ℝ )
172 169 171 readdcld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ )
173 172 rexrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ* )
174 173 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ* )
175 fzofzp1 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
176 165 175 syl ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
177 50 176 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
178 177 171 readdcld ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ )
179 178 rexrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ* )
180 179 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ* )
181 elioore ⊢ ( 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) → 𝑥 ∈ ℝ )
182 181 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑥 ∈ ℝ )
183 172 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ )
184 44 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑉 ‘ 𝐽 ) ∈ ℝ )
185 13 163 eqeltrid ⊢ ( 𝜑 → 𝐼 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } )
186 fveq2 ⊢ ( 𝑗 = 𝐼 → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 𝐼 ) )
187 186 oveq1d ⊢ ( 𝑗 = 𝐼 → ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) = ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) )
188 187 breq1d ⊢ ( 𝑗 = 𝐼 → ( ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ↔ ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
189 188 elrab ⊢ ( 𝐼 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ↔ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
190 185 189 sylib ⊢ ( 𝜑 → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
191 190 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
192 191 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
193 184 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑉 ‘ 𝐽 ) ∈ ℝ* )
194 fzofzp1 ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
195 11 194 syl ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
196 40 195 ffvelrnd ⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∈ 𝐻 )
197 34 196 sseldd ⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
198 197 rexrd ⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* )
199 198 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* )
200 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) )
201 ioogtlb ⊢ ( ( ( 𝑉 ‘ 𝐽 ) ∈ ℝ* ∧ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑉 ‘ 𝐽 ) < 𝑥 )
202 193 199 200 201 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑉 ‘ 𝐽 ) < 𝑥 )
203 183 184 182 192 202 lelttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) < 𝑥 )
204 zssre ⊢ ℤ ⊆ ℝ
205 25 204 sstri ⊢ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ℝ
206 205 a1i ⊢ ( ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ℝ )
207 99 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ≠ ∅ )
208 129 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑗 ≤ 𝑏 )
209 167 peano2zd ⊢ ( 𝜑 → ( 𝐿 + 1 ) ∈ ℤ )
210 209 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( 𝐿 + 1 ) ∈ ℤ )
211 oveq1 ⊢ ( 𝐼 = ( 𝑀 − 1 ) → ( 𝐼 + 1 ) = ( ( 𝑀 − 1 ) + 1 ) )
212 146 recnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
213 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
214 212 213 npcand ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
215 211 214 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) → ( 𝐼 + 1 ) = 𝑀 )
216 215 fveq2d ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑄 ‘ 𝑀 ) )
217 47 simprd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
218 217 simpld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) )
219 218 simprd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
220 219 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
221 59 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
222 60 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
223 221 222 npcand ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) + 𝐴 ) = 𝐵 )
224 223 eqcomd ⊢ ( 𝜑 → 𝐵 = ( ( 𝐵 − 𝐴 ) + 𝐴 ) )
225 1 eqcomi ⊢ ( 𝐵 − 𝐴 ) = 𝑇
226 225 a1i ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = 𝑇 )
227 226 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) + 𝐴 ) = ( 𝑇 + 𝐴 ) )
228 218 simpld ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
229 228 eqcomd ⊢ ( 𝜑 → 𝐴 = ( 𝑄 ‘ 0 ) )
230 229 oveq2d ⊢ ( 𝜑 → ( 𝑇 + 𝐴 ) = ( 𝑇 + ( 𝑄 ‘ 0 ) ) )
231 224 227 230 3eqtrd ⊢ ( 𝜑 → 𝐵 = ( 𝑇 + ( 𝑄 ‘ 0 ) ) )
232 231 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) → 𝐵 = ( 𝑇 + ( 𝑄 ‘ 0 ) ) )
233 216 220 232 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑇 + ( 𝑄 ‘ 0 ) ) )
234 62 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
235 228 222 eqeltrd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℂ )
236 234 235 addcomd ⊢ ( 𝜑 → ( 𝑇 + ( 𝑄 ‘ 0 ) ) = ( ( 𝑄 ‘ 0 ) + 𝑇 ) )
237 236 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) → ( 𝑇 + ( 𝑄 ‘ 0 ) ) = ( ( 𝑄 ‘ 0 ) + 𝑇 ) )
238 233 237 eqtrd ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( ( 𝑄 ‘ 0 ) + 𝑇 ) )
239 238 oveq1d ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) = ( ( ( 𝑄 ‘ 0 ) + 𝑇 ) + ( 𝐿 · 𝑇 ) ) )
240 171 recnd ⊢ ( 𝜑 → ( 𝐿 · 𝑇 ) ∈ ℂ )
241 235 234 240 addassd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) + 𝑇 ) + ( 𝐿 · 𝑇 ) ) = ( ( 𝑄 ‘ 0 ) + ( 𝑇 + ( 𝐿 · 𝑇 ) ) ) )
242 234 mulid2d ⊢ ( 𝜑 → ( 1 · 𝑇 ) = 𝑇 )
243 242 234 eqeltrd ⊢ ( 𝜑 → ( 1 · 𝑇 ) ∈ ℂ )
244 243 240 addcomd ⊢ ( 𝜑 → ( ( 1 · 𝑇 ) + ( 𝐿 · 𝑇 ) ) = ( ( 𝐿 · 𝑇 ) + ( 1 · 𝑇 ) ) )
245 242 eqcomd ⊢ ( 𝜑 → 𝑇 = ( 1 · 𝑇 ) )
246 245 oveq1d ⊢ ( 𝜑 → ( 𝑇 + ( 𝐿 · 𝑇 ) ) = ( ( 1 · 𝑇 ) + ( 𝐿 · 𝑇 ) ) )
247 170 recnd ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
248 247 213 234 adddird ⊢ ( 𝜑 → ( ( 𝐿 + 1 ) · 𝑇 ) = ( ( 𝐿 · 𝑇 ) + ( 1 · 𝑇 ) ) )
249 244 246 248 3eqtr4d ⊢ ( 𝜑 → ( 𝑇 + ( 𝐿 · 𝑇 ) ) = ( ( 𝐿 + 1 ) · 𝑇 ) )
250 249 oveq2d ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) + ( 𝑇 + ( 𝐿 · 𝑇 ) ) ) = ( ( 𝑄 ‘ 0 ) + ( ( 𝐿 + 1 ) · 𝑇 ) ) )
251 241 250 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) + 𝑇 ) + ( 𝐿 · 𝑇 ) ) = ( ( 𝑄 ‘ 0 ) + ( ( 𝐿 + 1 ) · 𝑇 ) ) )
252 251 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) → ( ( ( 𝑄 ‘ 0 ) + 𝑇 ) + ( 𝐿 · 𝑇 ) ) = ( ( 𝑄 ‘ 0 ) + ( ( 𝐿 + 1 ) · 𝑇 ) ) )
253 239 252 eqtr2d ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) → ( ( 𝑄 ‘ 0 ) + ( ( 𝐿 + 1 ) · 𝑇 ) ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
254 253 adantr ⊢ ( ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( ( 𝑄 ‘ 0 ) + ( ( 𝐿 + 1 ) · 𝑇 ) ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
255 simpr ⊢ ( ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
256 254 255 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( ( 𝑄 ‘ 0 ) + ( ( 𝐿 + 1 ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
257 oveq1 ⊢ ( 𝑘 = ( 𝐿 + 1 ) → ( 𝑘 · 𝑇 ) = ( ( 𝐿 + 1 ) · 𝑇 ) )
258 257 oveq2d ⊢ ( 𝑘 = ( 𝐿 + 1 ) → ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) = ( ( 𝑄 ‘ 0 ) + ( ( 𝐿 + 1 ) · 𝑇 ) ) )
259 258 breq1d ⊢ ( 𝑘 = ( 𝐿 + 1 ) → ( ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ↔ ( ( 𝑄 ‘ 0 ) + ( ( 𝐿 + 1 ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
260 259 elrab ⊢ ( ( 𝐿 + 1 ) ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ↔ ( ( 𝐿 + 1 ) ∈ ℤ ∧ ( ( 𝑄 ‘ 0 ) + ( ( 𝐿 + 1 ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
261 210 256 260 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( 𝐿 + 1 ) ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } )
262 suprub ⊢ ( ( ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ℝ ∧ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ≠ ∅ ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑗 ≤ 𝑏 ) ∧ ( 𝐿 + 1 ) ∈ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ) → ( 𝐿 + 1 ) ≤ sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) )
263 206 207 208 261 262 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( 𝐿 + 1 ) ≤ sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) )
264 263 12 breqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( 𝐿 + 1 ) ≤ 𝐿 )
265 170 ltp1d ⊢ ( 𝜑 → 𝐿 < ( 𝐿 + 1 ) )
266 peano2re ⊢ ( 𝐿 ∈ ℝ → ( 𝐿 + 1 ) ∈ ℝ )
267 170 266 syl ⊢ ( 𝜑 → ( 𝐿 + 1 ) ∈ ℝ )
268 170 267 ltnled ⊢ ( 𝜑 → ( 𝐿 < ( 𝐿 + 1 ) ↔ ¬ ( 𝐿 + 1 ) ≤ 𝐿 ) )
269 265 268 mpbid ⊢ ( 𝜑 → ¬ ( 𝐿 + 1 ) ≤ 𝐿 )
270 269 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ¬ ( 𝐿 + 1 ) ≤ 𝐿 )
271 264 270 pm2.65da ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝑀 − 1 ) ) → ¬ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
272 17 165 sselid ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
273 272 zred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
274 273 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = ( 𝑀 − 1 ) ) → 𝐼 ∈ ℝ )
275 peano2rem ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 1 ) ∈ ℝ )
276 146 275 syl ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℝ )
277 276 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = ( 𝑀 − 1 ) ) → ( 𝑀 − 1 ) ∈ ℝ )
278 elfzolt2 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → 𝐼 < 𝑀 )
279 elfzoelz ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → 𝐼 ∈ ℤ )
280 elfzoel2 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → 𝑀 ∈ ℤ )
281 zltlem1 ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐼 < 𝑀 ↔ 𝐼 ≤ ( 𝑀 − 1 ) ) )
282 279 280 281 syl2anc ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 < 𝑀 ↔ 𝐼 ≤ ( 𝑀 − 1 ) ) )
283 278 282 mpbid ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → 𝐼 ≤ ( 𝑀 − 1 ) )
284 165 283 syl ⊢ ( 𝜑 → 𝐼 ≤ ( 𝑀 − 1 ) )
285 284 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = ( 𝑀 − 1 ) ) → 𝐼 ≤ ( 𝑀 − 1 ) )
286 neqne ⊢ ( ¬ 𝐼 = ( 𝑀 − 1 ) → 𝐼 ≠ ( 𝑀 − 1 ) )
287 286 necomd ⊢ ( ¬ 𝐼 = ( 𝑀 − 1 ) → ( 𝑀 − 1 ) ≠ 𝐼 )
288 287 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = ( 𝑀 − 1 ) ) → ( 𝑀 − 1 ) ≠ 𝐼 )
289 274 277 285 288 leneltd ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = ( 𝑀 − 1 ) ) → 𝐼 < ( 𝑀 − 1 ) )
290 18 204 sstri ⊢ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ℝ
291 290 a1i ⊢ ( ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ℝ )
292 145 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ≠ ∅ )
293 161 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑘 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑘 ≤ 𝑏 )
294 176 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
295 273 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) → 𝐼 ∈ ℝ )
296 276 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) → ( 𝑀 − 1 ) ∈ ℝ )
297 1red ⊢ ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) → 1 ∈ ℝ )
298 simpr ⊢ ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) → 𝐼 < ( 𝑀 − 1 ) )
299 295 296 297 298 ltadd1dd ⊢ ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) → ( 𝐼 + 1 ) < ( ( 𝑀 − 1 ) + 1 ) )
300 214 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
301 299 300 breqtrd ⊢ ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) → ( 𝐼 + 1 ) < 𝑀 )
302 elfzfzo ⊢ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ↔ ( ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) ∧ ( 𝐼 + 1 ) < 𝑀 ) )
303 294 301 302 sylanbrc ⊢ ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) )
304 303 anim1i ⊢ ( ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
305 fveq2 ⊢ ( 𝑗 = ( 𝐼 + 1 ) → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
306 305 oveq1d ⊢ ( 𝑗 = ( 𝐼 + 1 ) → ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
307 306 breq1d ⊢ ( 𝑗 = ( 𝐼 + 1 ) → ( ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ↔ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
308 307 elrab ⊢ ( ( 𝐼 + 1 ) ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ↔ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
309 304 308 sylibr ⊢ ( ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( 𝐼 + 1 ) ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } )
310 suprub ⊢ ( ( ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ⊆ ℝ ∧ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ≠ ∅ ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑘 ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } 𝑘 ≤ 𝑏 ) ∧ ( 𝐼 + 1 ) ∈ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } ) → ( 𝐼 + 1 ) ≤ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) )
311 291 292 293 309 310 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( 𝐼 + 1 ) ≤ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) )
312 311 13 breqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ( 𝐼 + 1 ) ≤ 𝐼 )
313 273 ltp1d ⊢ ( 𝜑 → 𝐼 < ( 𝐼 + 1 ) )
314 peano2re ⊢ ( 𝐼 ∈ ℝ → ( 𝐼 + 1 ) ∈ ℝ )
315 273 314 syl ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ℝ )
316 273 315 ltnled ⊢ ( 𝜑 → ( 𝐼 < ( 𝐼 + 1 ) ↔ ¬ ( 𝐼 + 1 ) ≤ 𝐼 ) )
317 313 316 mpbid ⊢ ( 𝜑 → ¬ ( 𝐼 + 1 ) ≤ 𝐼 )
318 317 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) → ¬ ( 𝐼 + 1 ) ≤ 𝐼 )
319 312 318 pm2.65da ⊢ ( ( 𝜑 ∧ 𝐼 < ( 𝑀 − 1 ) ) → ¬ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
320 289 319 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = ( 𝑀 − 1 ) ) → ¬ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
321 271 320 pm2.61dan ⊢ ( 𝜑 → ¬ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) )
322 44 178 ltnled ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ↔ ¬ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
323 321 322 mpbird ⊢ ( 𝜑 → ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
324 197 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
325 6 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝐷 ∈ ℝ )
326 178 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ )
327 5 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
328 6 rexrd ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
329 5 6 7 ltled ⊢ ( 𝜑 → 𝐶 ≤ 𝐷 )
330 lbicc2 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 ≤ 𝐷 ) → 𝐶 ∈ ( 𝐶 [,] 𝐷 ) )
331 327 328 329 330 syl3anc ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐶 [,] 𝐷 ) )
332 ubicc2 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 ≤ 𝐷 ) → 𝐷 ∈ ( 𝐶 [,] 𝐷 ) )
333 327 328 329 332 syl3anc ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 [,] 𝐷 ) )
334 331 333 jca ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐶 [,] 𝐷 ) ∧ 𝐷 ∈ ( 𝐶 [,] 𝐷 ) ) )
335 prssg ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝐶 ∈ ( 𝐶 [,] 𝐷 ) ∧ 𝐷 ∈ ( 𝐶 [,] 𝐷 ) ) ↔ { 𝐶 , 𝐷 } ⊆ ( 𝐶 [,] 𝐷 ) ) )
336 5 6 335 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 ∈ ( 𝐶 [,] 𝐷 ) ∧ 𝐷 ∈ ( 𝐶 [,] 𝐷 ) ) ↔ { 𝐶 , 𝐷 } ⊆ ( 𝐶 [,] 𝐷 ) ) )
337 334 336 mpbid ⊢ ( 𝜑 → { 𝐶 , 𝐷 } ⊆ ( 𝐶 [,] 𝐷 ) )
338 337 30 unssd ⊢ ( 𝜑 → ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ⊆ ( 𝐶 [,] 𝐷 ) )
339 8 338 eqsstrid ⊢ ( 𝜑 → 𝐻 ⊆ ( 𝐶 [,] 𝐷 ) )
340 339 196 sseldd ⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∈ ( 𝐶 [,] 𝐷 ) )
341 iccleub ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∈ ( 𝐶 [,] 𝐷 ) ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ 𝐷 )
342 327 328 340 341 syl3anc ⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ 𝐷 )
343 342 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ 𝐷 )
344 simpr ⊢ ( ( 𝜑 ∧ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
345 324 325 326 343 344 letrd ⊢ ( ( 𝜑 ∧ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
346 345 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
347 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ¬ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
348 178 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ )
349 6 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝐷 ∈ ℝ )
350 348 349 ltnled ⊢ ( ( 𝜑 ∧ ¬ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ↔ ¬ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) )
351 347 350 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 )
352 351 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ¬ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 )
353 simpll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) ∧ ¬ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) )
354 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ¬ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
355 178 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ )
356 197 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
357 355 356 ltnled ⊢ ( ( 𝜑 ∧ ¬ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ↔ ¬ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) )
358 354 357 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) )
359 358 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) ∧ ¬ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) )
360 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → 𝐶 ∈ ℝ )
361 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → 𝐷 ∈ ℝ )
362 178 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ )
363 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝐶 ∈ ℝ )
364 178 adantr ⊢ ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ )
365 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ 𝐽 ) ∈ ℝ )
366 339 43 sseldd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝐽 ) ∈ ( 𝐶 [,] 𝐷 ) )
367 iccgelb ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ ( 𝑉 ‘ 𝐽 ) ∈ ( 𝐶 [,] 𝐷 ) ) → 𝐶 ≤ ( 𝑉 ‘ 𝐽 ) )
368 327 328 366 367 syl3anc ⊢ ( 𝜑 → 𝐶 ≤ ( 𝑉 ‘ 𝐽 ) )
369 368 adantr ⊢ ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝐶 ≤ ( 𝑉 ‘ 𝐽 ) )
370 simpr ⊢ ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
371 363 365 364 369 370 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝐶 < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
372 363 364 371 ltled ⊢ ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝐶 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
373 372 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → 𝐶 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
374 178 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ )
375 6 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → 𝐷 ∈ ℝ )
376 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 )
377 374 375 376 ltled ⊢ ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ 𝐷 )
378 377 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ≤ 𝐷 )
379 360 361 362 373 378 eliccd ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ( 𝐶 [,] 𝐷 ) )
380 167 znegcld ⊢ ( 𝜑 → - 𝐿 ∈ ℤ )
381 247 234 mulneg1d ⊢ ( 𝜑 → ( - 𝐿 · 𝑇 ) = - ( 𝐿 · 𝑇 ) )
382 381 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( - 𝐿 · 𝑇 ) ) = ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + - ( 𝐿 · 𝑇 ) ) )
383 178 recnd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ℂ )
384 383 240 negsubd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + - ( 𝐿 · 𝑇 ) ) = ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) − ( 𝐿 · 𝑇 ) ) )
385 177 recnd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℂ )
386 385 240 pncand ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) − ( 𝐿 · 𝑇 ) ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
387 382 384 386 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( - 𝐿 · 𝑇 ) ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
388 ffn ⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ → 𝑄 Fn ( 0 ... 𝑀 ) )
389 50 388 syl ⊢ ( 𝜑 → 𝑄 Fn ( 0 ... 𝑀 ) )
390 fnfvelrn ⊢ ( ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ran 𝑄 )
391 389 176 390 syl2anc ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ran 𝑄 )
392 387 391 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( - 𝐿 · 𝑇 ) ) ∈ ran 𝑄 )
393 oveq1 ⊢ ( 𝑘 = - 𝐿 → ( 𝑘 · 𝑇 ) = ( - 𝐿 · 𝑇 ) )
394 393 oveq2d ⊢ ( 𝑘 = - 𝐿 → ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) = ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( - 𝐿 · 𝑇 ) ) )
395 394 eleq1d ⊢ ( 𝑘 = - 𝐿 → ( ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( - 𝐿 · 𝑇 ) ) ∈ ran 𝑄 ) )
396 395 rspcev ⊢ ( ( - 𝐿 ∈ ℤ ∧ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( - 𝐿 · 𝑇 ) ) ∈ ran 𝑄 ) → ∃ 𝑘 ∈ ℤ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 )
397 380 392 396 syl2anc ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℤ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 )
398 397 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → ∃ 𝑘 ∈ ℤ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 )
399 oveq1 ⊢ ( 𝑦 = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) → ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) )
400 399 eleq1d ⊢ ( 𝑦 = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) → ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
401 400 rexbidv ⊢ ( 𝑦 = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
402 401 elrab ⊢ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ↔ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ( 𝐶 [,] 𝐷 ) ∧ ∃ 𝑘 ∈ ℤ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
403 379 398 402 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
404 elun2 ⊢ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
405 403 404 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
406 8 eqcomi ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = 𝐻
407 405 406 eleqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ 𝐻 )
408 407 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) ∧ ¬ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ 𝐻 )
409 f1ofo ⊢ ( 𝑉 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 → 𝑉 : ( 0 ... 𝑁 ) –onto→ 𝐻 )
410 37 38 409 3syl ⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑁 ) –onto→ 𝐻 )
411 foelrn ⊢ ( ( 𝑉 : ( 0 ... 𝑁 ) –onto→ 𝐻 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ 𝐻 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) = ( 𝑉 ‘ 𝑗 ) )
412 410 411 sylan ⊢ ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ 𝐻 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) = ( 𝑉 ‘ 𝑗 ) )
413 id ⊢ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) = ( 𝑉 ‘ 𝑗 ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) = ( 𝑉 ‘ 𝑗 ) )
414 413 eqcomd ⊢ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) = ( 𝑉 ‘ 𝑗 ) → ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
415 414 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ 𝐻 ) → ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) = ( 𝑉 ‘ 𝑗 ) → ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) )
416 415 reximdv ⊢ ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ 𝐻 ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) = ( 𝑉 ‘ 𝑗 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) )
417 412 416 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ 𝐻 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
418 417 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ 𝐻 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
419 simpl ⊢ ( ( ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
420 413 eqcoms ⊢ ( ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) = ( 𝑉 ‘ 𝑗 ) )
421 420 adantl ⊢ ( ( ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) = ( 𝑉 ‘ 𝑗 ) )
422 419 421 breqtrd ⊢ ( ( ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ 𝐽 ) < ( 𝑉 ‘ 𝑗 ) )
423 422 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ 𝐽 ) < ( 𝑉 ‘ 𝑗 ) )
424 423 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ 𝐽 ) < ( 𝑉 ‘ 𝑗 ) )
425 37 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝑉 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
426 42 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
427 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
428 isorel ⊢ ( ( 𝑉 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ∧ ( 𝐽 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝐽 < 𝑗 ↔ ( 𝑉 ‘ 𝐽 ) < ( 𝑉 ‘ 𝑗 ) ) )
429 425 426 427 428 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝐽 < 𝑗 ↔ ( 𝑉 ‘ 𝐽 ) < ( 𝑉 ‘ 𝑗 ) ) )
430 424 429 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝐽 < 𝑗 )
431 430 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝐽 < 𝑗 )
432 simpr ⊢ ( ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
433 simpl ⊢ ( ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) )
434 432 433 eqbrtrd ⊢ ( ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ 𝑗 ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) )
435 434 adantll ⊢ ( ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ 𝑗 ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) )
436 435 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ 𝑗 ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) )
437 37 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝑉 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
438 simplr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
439 195 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
440 isorel ⊢ ( ( 𝑉 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑗 < ( 𝐽 + 1 ) ↔ ( 𝑉 ‘ 𝑗 ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) )
441 437 438 439 440 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑗 < ( 𝐽 + 1 ) ↔ ( 𝑉 ‘ 𝑗 ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) )
442 436 441 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝑗 < ( 𝐽 + 1 ) )
443 442 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝑗 < ( 𝐽 + 1 ) )
444 431 443 jca ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
445 444 ex ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) → ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) )
446 445 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ 𝐻 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) → ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) )
447 446 reximdva ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ 𝐻 ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑗 ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) )
448 418 447 mpd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ 𝐻 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
449 353 359 408 448 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) ∧ ¬ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
450 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℤ )
451 450 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) → 𝑗 ∈ ℤ )
452 elfzelz ⊢ ( 𝐽 ∈ ( 0 ... 𝑁 ) → 𝐽 ∈ ℤ )
453 42 452 syl ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
454 453 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) → 𝐽 ∈ ℤ )
455 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) → 𝐽 < 𝑗 )
456 simprr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) → 𝑗 < ( 𝐽 + 1 ) )
457 btwnnz ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) → ¬ 𝑗 ∈ ℤ )
458 454 455 456 457 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) → ¬ 𝑗 ∈ ℤ )
459 451 458 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ¬ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
460 459 nrexdv ⊢ ( 𝜑 → ¬ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
461 460 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) ∧ ¬ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ¬ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
462 449 461 condan ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) < 𝐷 ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
463 352 462 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ∧ ¬ 𝐷 ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
464 346 463 pm2.61dan ⊢ ( ( 𝜑 ∧ ( 𝑉 ‘ 𝐽 ) < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
465 323 464 mpdan ⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
466 465 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
467 182 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ∧ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝑥 ∈ ℝ )
468 197 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ∧ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
469 178 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ∧ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ∈ ℝ )
470 iooltub ⊢ ( ( ( 𝑉 ‘ 𝐽 ) ∈ ℝ* ∧ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑥 < ( 𝑉 ‘ ( 𝐽 + 1 ) ) )
471 193 199 200 470 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑥 < ( 𝑉 ‘ ( 𝐽 + 1 ) ) )
472 471 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ∧ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝑥 < ( 𝑉 ‘ ( 𝐽 + 1 ) ) )
473 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ∧ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
474 467 468 469 472 473 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ∧ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ≤ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) → 𝑥 < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
475 466 474 mpdan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑥 < ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
476 174 180 182 203 475 eliood ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑥 ∈ ( ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) )
477 476 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) 𝑥 ∈ ( ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) )
478 dfss3 ⊢ ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ↔ ∀ 𝑥 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) 𝑥 ∈ ( ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) )
479 477 478 sylibr ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) )
480 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝐼 ) )
481 480 oveq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) = ( ( 𝑄 ‘ 𝐼 ) + ( 𝑙 · 𝑇 ) ) )
482 oveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 + 1 ) = ( 𝐼 + 1 ) )
483 482 fveq2d ⊢ ( 𝑖 = 𝐼 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
484 483 oveq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝑙 · 𝑇 ) ) )
485 481 484 oveq12d ⊢ ( 𝑖 = 𝐼 → ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) = ( ( ( 𝑄 ‘ 𝐼 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
486 485 sseq2d ⊢ ( 𝑖 = 𝐼 → ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ↔ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝐼 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) )
487 oveq1 ⊢ ( 𝑙 = 𝐿 → ( 𝑙 · 𝑇 ) = ( 𝐿 · 𝑇 ) )
488 487 oveq2d ⊢ ( 𝑙 = 𝐿 → ( ( 𝑄 ‘ 𝐼 ) + ( 𝑙 · 𝑇 ) ) = ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) )
489 487 oveq2d ⊢ ( 𝑙 = 𝐿 → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝑙 · 𝑇 ) ) = ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) )
490 488 489 oveq12d ⊢ ( 𝑙 = 𝐿 → ( ( ( 𝑄 ‘ 𝐼 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) = ( ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) )
491 490 sseq2d ⊢ ( 𝑙 = 𝐿 → ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝐼 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ↔ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ) )
492 486 491 rspc2ev ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐿 ∈ ℤ ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝐼 ) + ( 𝐿 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) + ( 𝐿 · 𝑇 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑙 ∈ ℤ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
493 165 167 479 492 syl3anc ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑙 ∈ ℤ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
494 165 167 493 jca31 ⊢ ( 𝜑 → ( ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐿 ∈ ℤ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑙 ∈ ℤ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) )