Metamath Proof Explorer

Theorem fourierdlem50

Description: Continuity of O and its limits with respect to the S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem50.xre ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem50.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem50.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem50.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem50.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem50.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem50.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem50.ab ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
fourierdlem50.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
fourierdlem50.t ⊢ 𝑇 = ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
fourierdlem50.n ⊢ 𝑁 = ( ( ♯ ‘ 𝑇 ) − 1 )
fourierdlem50.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
fourierdlem50.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
fourierdlem50.u ⊢ 𝑈 = ( ℩ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
fourierdlem50.ch ⊢ ( 𝜒 ↔ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) )
Assertion fourierdlem50 ( 𝜑 → ( 𝑈 ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem50.xre ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2 fourierdlem50.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
3 fourierdlem50.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 fourierdlem50.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
5 fourierdlem50.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6 fourierdlem50.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
7 fourierdlem50.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
8 fourierdlem50.ab ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
9 fourierdlem50.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
10 fourierdlem50.t ⊢ 𝑇 = ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
11 fourierdlem50.n ⊢ 𝑁 = ( ( ♯ ‘ 𝑇 ) − 1 )
12 fourierdlem50.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
13 fourierdlem50.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
14 fourierdlem50.u ⊢ 𝑈 = ( ℩ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
15 fourierdlem50.ch ⊢ ( 𝜒 ↔ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) )
16 5 6 7 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
17 2 3 4 fourierdlem15 ⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
18 pire ⊢ π ∈ ℝ
19 18 renegcli ⊢ - π ∈ ℝ
20 19 a1i ⊢ ( 𝜑 → - π ∈ ℝ )
21 20 1 readdcld ⊢ ( 𝜑 → ( - π + 𝑋 ) ∈ ℝ )
22 18 a1i ⊢ ( 𝜑 → π ∈ ℝ )
23 22 1 readdcld ⊢ ( 𝜑 → ( π + 𝑋 ) ∈ ℝ )
24 21 23 iccssred ⊢ ( 𝜑 → ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ⊆ ℝ )
25 17 24 fssd ⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
26 25 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
27 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ∈ ℝ )
28 26 27 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ )
29 28 9 fmptd ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
30 9 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) )
31 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 0 ) )
32 31 oveq1d ⊢ ( 𝑖 = 0 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 0 ) − 𝑋 ) )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 0 ) − 𝑋 ) )
34 nnssnn0 ⊢ ℕ ⊆ ℕ0
35 34 a1i ⊢ ( 𝜑 → ℕ ⊆ ℕ0 )
36 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
37 35 36 sseqtrdi ⊢ ( 𝜑 → ℕ ⊆ ( ℤ≥ ‘ 0 ) )
38 37 3 sseldd ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
39 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
40 38 39 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
41 25 40 ffvelrnd ⊢ ( 𝜑 → ( 𝑉 ‘ 0 ) ∈ ℝ )
42 41 1 resubcld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 0 ) − 𝑋 ) ∈ ℝ )
43 30 33 40 42 fvmptd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = ( ( 𝑉 ‘ 0 ) − 𝑋 ) )
44 2 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
45 3 44 syl ⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
46 4 45 mpbid ⊢ ( 𝜑 → ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) )
47 46 simprd ⊢ ( 𝜑 → ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
48 47 simpld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) )
49 48 simpld ⊢ ( 𝜑 → ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) )
50 49 oveq1d ⊢ ( 𝜑 → ( ( 𝑉 ‘ 0 ) − 𝑋 ) = ( ( - π + 𝑋 ) − 𝑋 ) )
51 20 recnd ⊢ ( 𝜑 → - π ∈ ℂ )
52 1 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
53 51 52 pncand ⊢ ( 𝜑 → ( ( - π + 𝑋 ) − 𝑋 ) = - π )
54 43 50 53 3eqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = - π )
55 20 rexrd ⊢ ( 𝜑 → - π ∈ ℝ* )
56 22 rexrd ⊢ ( 𝜑 → π ∈ ℝ* )
57 5 leidd ⊢ ( 𝜑 → 𝐴 ≤ 𝐴 )
58 5 6 5 57 16 eliccd ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
59 8 58 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( - π [,] π ) )
60 iccgelb ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐴 ∈ ( - π [,] π ) ) → - π ≤ 𝐴 )
61 55 56 59 60 syl3anc ⊢ ( 𝜑 → - π ≤ 𝐴 )
62 54 61 eqbrtrd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ≤ 𝐴 )
63 6 leidd ⊢ ( 𝜑 → 𝐵 ≤ 𝐵 )
64 5 6 6 16 63 eliccd ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
65 8 64 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ( - π [,] π ) )
66 iccleub ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐵 ∈ ( - π [,] π ) ) → 𝐵 ≤ π )
67 55 56 65 66 syl3anc ⊢ ( 𝜑 → 𝐵 ≤ π )
68 fveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑀 ) )
69 68 oveq1d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) )
70 69 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 𝑀 ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) )
71 eluzfz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 𝑀 ∈ ( 0 ... 𝑀 ) )
72 38 71 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
73 25 72 ffvelrnd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑀 ) ∈ ℝ )
74 73 1 resubcld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) ∈ ℝ )
75 30 70 72 74 fvmptd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) )
76 48 simprd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) )
77 76 oveq1d ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑀 ) − 𝑋 ) = ( ( π + 𝑋 ) − 𝑋 ) )
78 22 recnd ⊢ ( 𝜑 → π ∈ ℂ )
79 78 52 pncand ⊢ ( 𝜑 → ( ( π + 𝑋 ) − 𝑋 ) = π )
80 75 77 79 3eqtrrd ⊢ ( 𝜑 → π = ( 𝑄 ‘ 𝑀 ) )
81 67 80 breqtrd ⊢ ( 𝜑 → 𝐵 ≤ ( 𝑄 ‘ 𝑀 ) )
82 prfi ⊢ { 𝐴 , 𝐵 } ∈ Fin
83 82 a1i ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ Fin )
84 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
85 9 rnmptfi ⊢ ( ( 0 ... 𝑀 ) ∈ Fin → ran 𝑄 ∈ Fin )
86 84 85 syl ⊢ ( 𝜑 → ran 𝑄 ∈ Fin )
87 infi ⊢ ( ran 𝑄 ∈ Fin → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ∈ Fin )
88 86 87 syl ⊢ ( 𝜑 → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ∈ Fin )
89 unfi ⊢ ( ( { 𝐴 , 𝐵 } ∈ Fin ∧ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ∈ Fin ) → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ∈ Fin )
90 83 88 89 syl2anc ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ∈ Fin )
91 10 90 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ Fin )
92 5 6 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
93 prssg ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ↔ { 𝐴 , 𝐵 } ⊆ ℝ ) )
94 5 6 93 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ↔ { 𝐴 , 𝐵 } ⊆ ℝ ) )
95 92 94 mpbid ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ℝ )
96 inss2 ⊢ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 (,) 𝐵 )
97 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
98 96 97 sstri ⊢ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ℝ
99 98 a1i ⊢ ( 𝜑 → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ℝ )
100 95 99 unssd ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ⊆ ℝ )
101 10 100 eqsstrid ⊢ ( 𝜑 → 𝑇 ⊆ ℝ )
102 91 101 12 11 fourierdlem36 ⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
103 eqid ⊢ sup ( { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑥 ) ≤ ( 𝑆 ‘ 𝐽 ) } , ℝ , < ) = sup ( { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑥 ) ≤ ( 𝑆 ‘ 𝐽 ) } , ℝ , < )
104 3 5 6 16 29 62 81 13 10 102 103 fourierdlem20 ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
105 15 biimpi ⊢ ( 𝜒 → ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) )
106 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) → 𝜑 )
107 105 106 syl ⊢ ( 𝜒 → 𝜑 )
108 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) )
109 105 108 syl ⊢ ( 𝜒 → 𝑘 ∈ ( 0 ..^ 𝑀 ) )
110 107 109 jca ⊢ ( 𝜒 → ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) )
111 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
112 105 111 syl ⊢ ( 𝜒 → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
113 elfzofz ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑀 ) → 𝑘 ∈ ( 0 ... 𝑀 ) )
114 113 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑘 ∈ ( 0 ... 𝑀 ) )
115 105 114 syl ⊢ ( 𝜒 → 𝑘 ∈ ( 0 ... 𝑀 ) )
116 107 25 syl ⊢ ( 𝜒 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
117 116 115 ffvelrnd ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑘 ) ∈ ℝ )
118 107 1 syl ⊢ ( 𝜒 → 𝑋 ∈ ℝ )
119 117 118 resubcld ⊢ ( 𝜒 → ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) ∈ ℝ )
120 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑘 ) )
121 120 oveq1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) )
122 121 9 fvmptg ⊢ ( ( 𝑘 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) ∈ ℝ ) → ( 𝑄 ‘ 𝑘 ) = ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) )
123 115 119 122 syl2anc ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑘 ) = ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) )
124 123 119 eqeltrd ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑘 ) ∈ ℝ )
125 29 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
126 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
127 126 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
128 125 127 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
129 107 112 128 syl2anc ⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
130 isof1o ⊢ ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 )
131 102 130 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 )
132 f1of ⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
133 131 132 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
134 fzofzp1 ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
135 13 134 syl ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
136 133 135 ffvelrnd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ 𝑇 )
137 101 136 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
138 107 137 syl ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
139 elfzofz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
140 13 139 syl ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑁 ) )
141 133 140 ffvelrnd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ 𝑇 )
142 101 141 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℝ )
143 107 142 syl ⊢ ( 𝜒 → ( 𝑆 ‘ 𝐽 ) ∈ ℝ )
144 105 simprd ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) )
145 124 rexrd ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑘 ) ∈ ℝ* )
146 29 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
147 fzofzp1 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑀 ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝑀 ) )
148 147 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝑀 ) )
149 146 148 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
150 149 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑘 + 1 ) ) ∈ ℝ* )
151 110 150 syl ⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑘 + 1 ) ) ∈ ℝ* )
152 143 rexrd ⊢ ( 𝜒 → ( 𝑆 ‘ 𝐽 ) ∈ ℝ* )
153 138 rexrd ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* )
154 elfzoelz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
155 154 zred ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℝ )
156 155 ltp1d ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 < ( 𝐽 + 1 ) )
157 13 156 syl ⊢ ( 𝜑 → 𝐽 < ( 𝐽 + 1 ) )
158 isoeq5 ⊢ ( 𝑇 = ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) → ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) ↔ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ) ) )
159 10 158 ax-mp ⊢ ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) ↔ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ) )
160 102 159 sylib ⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ) )
161 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ) ∧ ( 𝐽 ∈ ( 0 ... 𝑁 ) ∧ ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝐽 < ( 𝐽 + 1 ) ↔ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
162 160 140 135 161 syl12anc ⊢ ( 𝜑 → ( 𝐽 < ( 𝐽 + 1 ) ↔ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
163 157 162 mpbid ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
164 107 163 syl ⊢ ( 𝜒 → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
165 145 151 152 153 164 ioossioobi ⊢ ( 𝜒 → ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) )
166 144 165 mpbid ⊢ ( 𝜒 → ( ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) )
167 166 simpld ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) )
168 124 143 138 167 164 lelttrd ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑘 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
169 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
170 169 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
171 170 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
172 105 171 syl ⊢ ( 𝜒 → 𝑖 ∈ ( 0 ... 𝑀 ) )
173 107 172 28 syl2anc ⊢ ( 𝜒 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ )
174 9 fvmpt2 ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
175 172 173 174 syl2anc ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
176 175 173 eqeltrd ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
177 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) → ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
178 105 177 syl ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
179 176 129 143 138 164 178 fourierdlem10 ⊢ ( 𝜒 → ( ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑆 ‘ 𝐽 ) ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
180 179 simprd ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
181 124 138 129 168 180 ltletrd ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑘 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
182 124 129 118 181 ltadd2dd ⊢ ( 𝜒 → ( 𝑋 + ( 𝑄 ‘ 𝑘 ) ) < ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
183 123 oveq2d ⊢ ( 𝜒 → ( 𝑋 + ( 𝑄 ‘ 𝑘 ) ) = ( 𝑋 + ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) ) )
184 107 52 syl ⊢ ( 𝜒 → 𝑋 ∈ ℂ )
185 117 recnd ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑘 ) ∈ ℂ )
186 184 185 pncan3d ⊢ ( 𝜒 → ( 𝑋 + ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) ) = ( 𝑉 ‘ 𝑘 ) )
187 183 186 eqtr2d ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑘 ) = ( 𝑋 + ( 𝑄 ‘ 𝑘 ) ) )
188 112 126 syl ⊢ ( 𝜒 → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
189 25 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
190 189 127 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
191 107 112 190 syl2anc ⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
192 191 118 resubcld ⊢ ( 𝜒 → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ )
193 188 192 jca ⊢ ( 𝜒 → ( ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ ) )
194 eleq1 ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( 𝑘 ∈ ( 0 ... 𝑀 ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) ) )
195 fveq2 ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( 𝑉 ‘ 𝑘 ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
196 195 oveq1d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
197 196 eleq1d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) ∈ ℝ ↔ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ ) )
198 194 197 anbi12d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ( 𝑘 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) ∈ ℝ ) ↔ ( ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ ) ) )
199 fveq2 ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
200 199 196 eqeq12d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ( 𝑄 ‘ 𝑘 ) = ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) ↔ ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
201 198 200 imbi12d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ( ( 𝑘 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) ∈ ℝ ) → ( 𝑄 ‘ 𝑘 ) = ( ( 𝑉 ‘ 𝑘 ) − 𝑋 ) ) ↔ ( ( ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) )
202 201 122 vtoclg ⊢ ( ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) → ( ( ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
203 188 193 202 sylc ⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
204 203 oveq2d ⊢ ( 𝜒 → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑋 + ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
205 191 recnd ⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
206 184 205 pncan3d ⊢ ( 𝜒 → ( 𝑋 + ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
207 204 206 eqtr2d ⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) = ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
208 182 187 207 3brtr4d ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑘 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
209 eleq1w ⊢ ( 𝑙 = 𝑖 → ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) )
210 209 anbi2d ⊢ ( 𝑙 = 𝑖 → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ) )
211 oveq1 ⊢ ( 𝑙 = 𝑖 → ( 𝑙 + 1 ) = ( 𝑖 + 1 ) )
212 211 fveq2d ⊢ ( 𝑙 = 𝑖 → ( 𝑉 ‘ ( 𝑙 + 1 ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
213 212 breq2d ⊢ ( 𝑙 = 𝑖 → ( ( 𝑉 ‘ 𝑘 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ↔ ( 𝑉 ‘ 𝑘 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
214 210 213 anbi12d ⊢ ( 𝑙 = 𝑖 → ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑘 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑘 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) )
215 fveq2 ⊢ ( 𝑙 = 𝑖 → ( 𝑉 ‘ 𝑙 ) = ( 𝑉 ‘ 𝑖 ) )
216 215 breq2d ⊢ ( 𝑙 = 𝑖 → ( ( 𝑉 ‘ 𝑘 ) ≤ ( 𝑉 ‘ 𝑙 ) ↔ ( 𝑉 ‘ 𝑘 ) ≤ ( 𝑉 ‘ 𝑖 ) ) )
217 214 216 imbi12d ⊢ ( 𝑙 = 𝑖 → ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑘 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ( 𝑉 ‘ 𝑘 ) ≤ ( 𝑉 ‘ 𝑙 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑘 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑉 ‘ 𝑘 ) ≤ ( 𝑉 ‘ 𝑖 ) ) ) )
218 eleq1w ⊢ ( ℎ = 𝑘 → ( ℎ ∈ ( 0 ..^ 𝑀 ) ↔ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) )
219 218 anbi2d ⊢ ( ℎ = 𝑘 → ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ) )
220 219 anbi1d ⊢ ( ℎ = 𝑘 → ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ) )
221 fveq2 ⊢ ( ℎ = 𝑘 → ( 𝑉 ‘ ℎ ) = ( 𝑉 ‘ 𝑘 ) )
222 221 breq1d ⊢ ( ℎ = 𝑘 → ( ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ↔ ( 𝑉 ‘ 𝑘 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) )
223 220 222 anbi12d ⊢ ( ℎ = 𝑘 → ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑘 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ) )
224 221 breq1d ⊢ ( ℎ = 𝑘 → ( ( 𝑉 ‘ ℎ ) ≤ ( 𝑉 ‘ 𝑙 ) ↔ ( 𝑉 ‘ 𝑘 ) ≤ ( 𝑉 ‘ 𝑙 ) ) )
225 223 224 imbi12d ⊢ ( ℎ = 𝑘 → ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ( 𝑉 ‘ ℎ ) ≤ ( 𝑉 ‘ 𝑙 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑘 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ( 𝑉 ‘ 𝑘 ) ≤ ( 𝑉 ‘ 𝑙 ) ) ) )
226 elfzoelz ⊢ ( ℎ ∈ ( 0 ..^ 𝑀 ) → ℎ ∈ ℤ )
227 226 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ℎ ∈ ℤ )
228 elfzoelz ⊢ ( 𝑙 ∈ ( 0 ..^ 𝑀 ) → 𝑙 ∈ ℤ )
229 228 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → 𝑙 ∈ ℤ )
230 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ∧ ¬ ℎ < ( 𝑙 + 1 ) ) → ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) )
231 25 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
232 fzofzp1 ⊢ ( 𝑙 ∈ ( 0 ..^ 𝑀 ) → ( 𝑙 + 1 ) ∈ ( 0 ... 𝑀 ) )
233 232 adantl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑙 + 1 ) ∈ ( 0 ... 𝑀 ) )
234 231 233 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑙 + 1 ) ) ∈ ℝ )
235 234 adantlr ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑙 + 1 ) ) ∈ ℝ )
236 235 adantr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ℎ < ( 𝑙 + 1 ) ) → ( 𝑉 ‘ ( 𝑙 + 1 ) ) ∈ ℝ )
237 25 adantr ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
238 elfzofz ⊢ ( ℎ ∈ ( 0 ..^ 𝑀 ) → ℎ ∈ ( 0 ... 𝑀 ) )
239 238 adantl ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) → ℎ ∈ ( 0 ... 𝑀 ) )
240 237 239 ffvelrnd ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ℎ ) ∈ ℝ )
241 240 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ℎ < ( 𝑙 + 1 ) ) → ( 𝑉 ‘ ℎ ) ∈ ℝ )
242 228 zred ⊢ ( 𝑙 ∈ ( 0 ..^ 𝑀 ) → 𝑙 ∈ ℝ )
243 peano2re ⊢ ( 𝑙 ∈ ℝ → ( 𝑙 + 1 ) ∈ ℝ )
244 242 243 syl ⊢ ( 𝑙 ∈ ( 0 ..^ 𝑀 ) → ( 𝑙 + 1 ) ∈ ℝ )
245 244 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ℎ < ( 𝑙 + 1 ) ) → ( 𝑙 + 1 ) ∈ ℝ )
246 226 zred ⊢ ( ℎ ∈ ( 0 ..^ 𝑀 ) → ℎ ∈ ℝ )
247 246 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ℎ < ( 𝑙 + 1 ) ) → ℎ ∈ ℝ )
248 simpr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ℎ < ( 𝑙 + 1 ) ) → ¬ ℎ < ( 𝑙 + 1 ) )
249 245 247 248 nltled ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ℎ < ( 𝑙 + 1 ) ) → ( 𝑙 + 1 ) ≤ ℎ )
250 228 peano2zd ⊢ ( 𝑙 ∈ ( 0 ..^ 𝑀 ) → ( 𝑙 + 1 ) ∈ ℤ )
251 250 ad2antlr ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑙 + 1 ) ≤ ℎ ) → ( 𝑙 + 1 ) ∈ ℤ )
252 226 ad2antrr ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑙 + 1 ) ≤ ℎ ) → ℎ ∈ ℤ )
253 simpr ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑙 + 1 ) ≤ ℎ ) → ( 𝑙 + 1 ) ≤ ℎ )
254 eluz2 ⊢ ( ℎ ∈ ( ℤ≥ ‘ ( 𝑙 + 1 ) ) ↔ ( ( 𝑙 + 1 ) ∈ ℤ ∧ ℎ ∈ ℤ ∧ ( 𝑙 + 1 ) ≤ ℎ ) )
255 251 252 253 254 syl3anbrc ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑙 + 1 ) ≤ ℎ ) → ℎ ∈ ( ℤ≥ ‘ ( 𝑙 + 1 ) ) )
256 255 adantlll ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑙 + 1 ) ≤ ℎ ) → ℎ ∈ ( ℤ≥ ‘ ( 𝑙 + 1 ) ) )
257 simplll ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝜑 )
258 0zd ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 0 ∈ ℤ )
259 elfzoel2 ⊢ ( ℎ ∈ ( 0 ..^ 𝑀 ) → 𝑀 ∈ ℤ )
260 259 ad2antrr ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑀 ∈ ℤ )
261 elfzelz ⊢ ( 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) → 𝑖 ∈ ℤ )
262 261 adantl ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑖 ∈ ℤ )
263 0red ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 0 ∈ ℝ )
264 261 zred ⊢ ( 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) → 𝑖 ∈ ℝ )
265 264 adantl ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑖 ∈ ℝ )
266 242 adantr ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑙 ∈ ℝ )
267 elfzole1 ⊢ ( 𝑙 ∈ ( 0 ..^ 𝑀 ) → 0 ≤ 𝑙 )
268 267 adantr ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 0 ≤ 𝑙 )
269 266 243 syl ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → ( 𝑙 + 1 ) ∈ ℝ )
270 266 ltp1d ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑙 < ( 𝑙 + 1 ) )
271 elfzle1 ⊢ ( 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) → ( 𝑙 + 1 ) ≤ 𝑖 )
272 271 adantl ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → ( 𝑙 + 1 ) ≤ 𝑖 )
273 266 269 265 270 272 ltletrd ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑙 < 𝑖 )
274 263 266 265 268 273 lelttrd ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 0 < 𝑖 )
275 263 265 274 ltled ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 0 ≤ 𝑖 )
276 275 adantll ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 0 ≤ 𝑖 )
277 264 adantl ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑖 ∈ ℝ )
278 259 zred ⊢ ( ℎ ∈ ( 0 ..^ 𝑀 ) → 𝑀 ∈ ℝ )
279 278 adantr ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑀 ∈ ℝ )
280 246 adantr ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → ℎ ∈ ℝ )
281 elfzle2 ⊢ ( 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) → 𝑖 ≤ ℎ )
282 281 adantl ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑖 ≤ ℎ )
283 elfzolt2 ⊢ ( ℎ ∈ ( 0 ..^ 𝑀 ) → ℎ < 𝑀 )
284 283 adantr ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → ℎ < 𝑀 )
285 277 280 279 282 284 lelttrd ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑖 < 𝑀 )
286 277 279 285 ltled ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑖 ≤ 𝑀 )
287 286 adantlr ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑖 ≤ 𝑀 )
288 258 260 262 276 287 elfzd ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
289 288 adantlll ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
290 257 289 26 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
291 290 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑙 + 1 ) ≤ ℎ ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ℎ ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
292 simplll ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝜑 )
293 0zd ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 0 ∈ ℤ )
294 elfzelz ⊢ ( 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) → 𝑖 ∈ ℤ )
295 294 adantl ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑖 ∈ ℤ )
296 0red ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 0 ∈ ℝ )
297 295 zred ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑖 ∈ ℝ )
298 242 adantr ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑙 ∈ ℝ )
299 267 adantr ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 0 ≤ 𝑙 )
300 298 243 syl ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → ( 𝑙 + 1 ) ∈ ℝ )
301 298 ltp1d ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑙 < ( 𝑙 + 1 ) )
302 elfzle1 ⊢ ( 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) → ( 𝑙 + 1 ) ≤ 𝑖 )
303 302 adantl ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → ( 𝑙 + 1 ) ≤ 𝑖 )
304 298 300 297 301 303 ltletrd ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑙 < 𝑖 )
305 296 298 297 299 304 lelttrd ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 0 < 𝑖 )
306 296 297 305 ltled ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 0 ≤ 𝑖 )
307 eluz2 ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 0 ) ↔ ( 0 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 0 ≤ 𝑖 ) )
308 293 295 306 307 syl3anbrc ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
309 308 adantll ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
310 elfzoel2 ⊢ ( 𝑙 ∈ ( 0 ..^ 𝑀 ) → 𝑀 ∈ ℤ )
311 310 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑀 ∈ ℤ )
312 294 zred ⊢ ( 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) → 𝑖 ∈ ℝ )
313 312 adantl ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑖 ∈ ℝ )
314 peano2rem ⊢ ( ℎ ∈ ℝ → ( ℎ − 1 ) ∈ ℝ )
315 246 314 syl ⊢ ( ℎ ∈ ( 0 ..^ 𝑀 ) → ( ℎ − 1 ) ∈ ℝ )
316 315 adantr ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → ( ℎ − 1 ) ∈ ℝ )
317 278 adantr ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑀 ∈ ℝ )
318 elfzle2 ⊢ ( 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) → 𝑖 ≤ ( ℎ − 1 ) )
319 318 adantl ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑖 ≤ ( ℎ − 1 ) )
320 246 ltm1d ⊢ ( ℎ ∈ ( 0 ..^ 𝑀 ) → ( ℎ − 1 ) < ℎ )
321 315 246 278 320 283 lttrd ⊢ ( ℎ ∈ ( 0 ..^ 𝑀 ) → ( ℎ − 1 ) < 𝑀 )
322 321 adantr ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → ( ℎ − 1 ) < 𝑀 )
323 313 316 317 319 322 lelttrd ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑖 < 𝑀 )
324 323 adantll ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑖 < 𝑀 )
325 324 adantlr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑖 < 𝑀 )
326 elfzo2 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑖 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) )
327 309 311 325 326 syl3anbrc ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
328 169 26 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
329 47 simprd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
330 329 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
331 328 190 330 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
332 292 327 331 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
333 332 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑙 + 1 ) ≤ ℎ ) ∧ 𝑖 ∈ ( ( 𝑙 + 1 ) ... ( ℎ − 1 ) ) ) → ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
334 256 291 333 monoord ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑙 + 1 ) ≤ ℎ ) → ( 𝑉 ‘ ( 𝑙 + 1 ) ) ≤ ( 𝑉 ‘ ℎ ) )
335 249 334 syldan ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ℎ < ( 𝑙 + 1 ) ) → ( 𝑉 ‘ ( 𝑙 + 1 ) ) ≤ ( 𝑉 ‘ ℎ ) )
336 236 241 335 lensymd ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ℎ < ( 𝑙 + 1 ) ) → ¬ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) )
337 336 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ∧ ¬ ℎ < ( 𝑙 + 1 ) ) → ¬ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) )
338 230 337 condan ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ℎ < ( 𝑙 + 1 ) )
339 zleltp1 ⊢ ( ( ℎ ∈ ℤ ∧ 𝑙 ∈ ℤ ) → ( ℎ ≤ 𝑙 ↔ ℎ < ( 𝑙 + 1 ) ) )
340 227 229 339 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ( ℎ ≤ 𝑙 ↔ ℎ < ( 𝑙 + 1 ) ) )
341 338 340 mpbird ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ℎ ≤ 𝑙 )
342 eluz2 ⊢ ( 𝑙 ∈ ( ℤ≥ ‘ ℎ ) ↔ ( ℎ ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ ℎ ≤ 𝑙 ) )
343 227 229 341 342 syl3anbrc ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → 𝑙 ∈ ( ℤ≥ ‘ ℎ ) )
344 25 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
345 0zd ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 0 ∈ ℤ )
346 259 ad2antrr ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑀 ∈ ℤ )
347 elfzelz ⊢ ( 𝑖 ∈ ( ℎ ... 𝑙 ) → 𝑖 ∈ ℤ )
348 347 adantl ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑖 ∈ ℤ )
349 0red ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 0 ∈ ℝ )
350 246 adantr ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → ℎ ∈ ℝ )
351 347 zred ⊢ ( 𝑖 ∈ ( ℎ ... 𝑙 ) → 𝑖 ∈ ℝ )
352 351 adantl ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑖 ∈ ℝ )
353 elfzole1 ⊢ ( ℎ ∈ ( 0 ..^ 𝑀 ) → 0 ≤ ℎ )
354 353 adantr ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 0 ≤ ℎ )
355 elfzle1 ⊢ ( 𝑖 ∈ ( ℎ ... 𝑙 ) → ℎ ≤ 𝑖 )
356 355 adantl ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → ℎ ≤ 𝑖 )
357 349 350 352 354 356 letrd ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 0 ≤ 𝑖 )
358 357 adantlr ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 0 ≤ 𝑖 )
359 351 adantl ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑖 ∈ ℝ )
360 310 zred ⊢ ( 𝑙 ∈ ( 0 ..^ 𝑀 ) → 𝑀 ∈ ℝ )
361 360 adantr ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑀 ∈ ℝ )
362 242 adantr ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑙 ∈ ℝ )
363 elfzle2 ⊢ ( 𝑖 ∈ ( ℎ ... 𝑙 ) → 𝑖 ≤ 𝑙 )
364 363 adantl ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑖 ≤ 𝑙 )
365 elfzolt2 ⊢ ( 𝑙 ∈ ( 0 ..^ 𝑀 ) → 𝑙 < 𝑀 )
366 365 adantr ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑙 < 𝑀 )
367 359 362 361 364 366 lelttrd ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑖 < 𝑀 )
368 359 361 367 ltled ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑖 ≤ 𝑀 )
369 368 adantll ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑖 ≤ 𝑀 )
370 345 346 348 358 369 elfzd ⊢ ( ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
371 370 adantlll ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
372 344 371 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
373 372 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ∧ 𝑖 ∈ ( ℎ ... 𝑙 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
374 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝜑 )
375 0zd ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 0 ∈ ℤ )
376 elfzelz ⊢ ( 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) → 𝑖 ∈ ℤ )
377 376 adantl ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑖 ∈ ℤ )
378 0red ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 0 ∈ ℝ )
379 246 adantr ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → ℎ ∈ ℝ )
380 377 zred ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑖 ∈ ℝ )
381 353 adantr ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 0 ≤ ℎ )
382 elfzle1 ⊢ ( 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) → ℎ ≤ 𝑖 )
383 382 adantl ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → ℎ ≤ 𝑖 )
384 378 379 380 381 383 letrd ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 0 ≤ 𝑖 )
385 375 377 384 307 syl3anbrc ⊢ ( ( ℎ ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
386 385 adantll ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
387 386 ad4ant14 ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
388 310 ad3antlr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑀 ∈ ℤ )
389 376 zred ⊢ ( 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) → 𝑖 ∈ ℝ )
390 389 adantl ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑖 ∈ ℝ )
391 242 adantr ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑙 ∈ ℝ )
392 360 adantr ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑀 ∈ ℝ )
393 elfzle2 ⊢ ( 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) → 𝑖 ≤ ( 𝑙 − 1 ) )
394 393 adantl ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑖 ≤ ( 𝑙 − 1 ) )
395 zltlem1 ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑙 ∈ ℤ ) → ( 𝑖 < 𝑙 ↔ 𝑖 ≤ ( 𝑙 − 1 ) ) )
396 376 228 395 syl2anr ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → ( 𝑖 < 𝑙 ↔ 𝑖 ≤ ( 𝑙 − 1 ) ) )
397 394 396 mpbird ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑖 < 𝑙 )
398 365 adantr ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑙 < 𝑀 )
399 390 391 392 397 398 lttrd ⊢ ( ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑖 < 𝑀 )
400 399 adantll ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑖 < 𝑀 )
401 400 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑖 < 𝑀 )
402 387 388 401 326 syl3anbrc ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
403 374 402 331 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ∧ 𝑖 ∈ ( ℎ ... ( 𝑙 − 1 ) ) ) → ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
404 343 373 403 monoord ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ( 𝑉 ‘ ℎ ) ≤ ( 𝑉 ‘ 𝑙 ) )
405 225 404 chvarvv ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑘 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ( 𝑉 ‘ 𝑘 ) ≤ ( 𝑉 ‘ 𝑙 ) )
406 217 405 chvarvv ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑘 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑉 ‘ 𝑘 ) ≤ ( 𝑉 ‘ 𝑖 ) )
407 110 112 208 406 syl21anc ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑘 ) ≤ ( 𝑉 ‘ 𝑖 ) )
408 107 112 jca ⊢ ( 𝜒 → ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) )
409 110 149 syl ⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
410 179 simpld ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑆 ‘ 𝐽 ) )
411 176 143 138 410 164 lelttrd ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
412 166 simprd ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑘 + 1 ) ) )
413 176 138 409 411 412 ltletrd ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑘 + 1 ) ) )
414 176 409 118 413 ltadd2dd ⊢ ( 𝜒 → ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) < ( 𝑋 + ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) )
415 175 oveq2d ⊢ ( 𝜒 → ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) = ( 𝑋 + ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) )
416 107 172 26 syl2anc ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
417 416 recnd ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) ∈ ℂ )
418 184 417 pncan3d ⊢ ( 𝜒 → ( 𝑋 + ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) = ( 𝑉 ‘ 𝑖 ) )
419 415 418 eqtr2d ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) = ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) )
420 9 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) )
421 fveq2 ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ ( 𝑘 + 1 ) ) )
422 421 oveq1d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑘 + 1 ) ) − 𝑋 ) )
423 422 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 = ( 𝑘 + 1 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑘 + 1 ) ) − 𝑋 ) )
424 25 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
425 424 148 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
426 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℝ )
427 425 426 resubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ ( 𝑘 + 1 ) ) − 𝑋 ) ∈ ℝ )
428 420 423 148 427 fvmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑘 + 1 ) ) − 𝑋 ) )
429 107 109 428 syl2anc ⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑘 + 1 ) ) − 𝑋 ) )
430 429 oveq2d ⊢ ( 𝜒 → ( 𝑋 + ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) = ( 𝑋 + ( ( 𝑉 ‘ ( 𝑘 + 1 ) ) − 𝑋 ) ) )
431 110 425 syl ⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
432 431 recnd ⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
433 184 432 pncan3d ⊢ ( 𝜒 → ( 𝑋 + ( ( 𝑉 ‘ ( 𝑘 + 1 ) ) − 𝑋 ) ) = ( 𝑉 ‘ ( 𝑘 + 1 ) ) )
434 430 433 eqtr2d ⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑘 + 1 ) ) = ( 𝑋 + ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) )
435 414 419 434 3brtr4d ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑘 + 1 ) ) )
436 eleq1w ⊢ ( 𝑙 = 𝑘 → ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) )
437 436 anbi2d ⊢ ( 𝑙 = 𝑘 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ) )
438 oveq1 ⊢ ( 𝑙 = 𝑘 → ( 𝑙 + 1 ) = ( 𝑘 + 1 ) )
439 438 fveq2d ⊢ ( 𝑙 = 𝑘 → ( 𝑉 ‘ ( 𝑙 + 1 ) ) = ( 𝑉 ‘ ( 𝑘 + 1 ) ) )
440 439 breq2d ⊢ ( 𝑙 = 𝑘 → ( ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ↔ ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑘 + 1 ) ) ) )
441 437 440 anbi12d ⊢ ( 𝑙 = 𝑘 → ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑘 + 1 ) ) ) ) )
442 fveq2 ⊢ ( 𝑙 = 𝑘 → ( 𝑉 ‘ 𝑙 ) = ( 𝑉 ‘ 𝑘 ) )
443 442 breq2d ⊢ ( 𝑙 = 𝑘 → ( ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ 𝑙 ) ↔ ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ 𝑘 ) ) )
444 441 443 imbi12d ⊢ ( 𝑙 = 𝑘 → ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ 𝑙 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑘 + 1 ) ) ) → ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ 𝑘 ) ) ) )
445 eleq1w ⊢ ( ℎ = 𝑖 → ( ℎ ∈ ( 0 ..^ 𝑀 ) ↔ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) )
446 445 anbi2d ⊢ ( ℎ = 𝑖 → ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ) )
447 446 anbi1d ⊢ ( ℎ = 𝑖 → ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ) )
448 fveq2 ⊢ ( ℎ = 𝑖 → ( 𝑉 ‘ ℎ ) = ( 𝑉 ‘ 𝑖 ) )
449 448 breq1d ⊢ ( ℎ = 𝑖 → ( ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ↔ ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) )
450 447 449 anbi12d ⊢ ( ℎ = 𝑖 → ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) ) )
451 448 breq1d ⊢ ( ℎ = 𝑖 → ( ( 𝑉 ‘ ℎ ) ≤ ( 𝑉 ‘ 𝑙 ) ↔ ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ 𝑙 ) ) )
452 450 451 imbi12d ⊢ ( ℎ = 𝑖 → ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ℎ ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ( 𝑉 ‘ ℎ ) ≤ ( 𝑉 ‘ 𝑙 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ 𝑙 ) ) ) )
453 452 404 chvarvv ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑙 + 1 ) ) ) → ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ 𝑙 ) )
454 444 453 chvarvv ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑘 + 1 ) ) ) → ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ 𝑘 ) )
455 408 109 435 454 syl21anc ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ 𝑘 ) )
456 117 416 letri3d ⊢ ( 𝜒 → ( ( 𝑉 ‘ 𝑘 ) = ( 𝑉 ‘ 𝑖 ) ↔ ( ( 𝑉 ‘ 𝑘 ) ≤ ( 𝑉 ‘ 𝑖 ) ∧ ( 𝑉 ‘ 𝑖 ) ≤ ( 𝑉 ‘ 𝑘 ) ) ) )
457 407 455 456 mpbir2and ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑘 ) = ( 𝑉 ‘ 𝑖 ) )
458 2 3 4 fourierdlem34 ⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) –1-1→ ℝ )
459 107 458 syl ⊢ ( 𝜒 → 𝑉 : ( 0 ... 𝑀 ) –1-1→ ℝ )
460 f1fveq ⊢ ( ( 𝑉 : ( 0 ... 𝑀 ) –1-1→ ℝ ∧ ( 𝑘 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ) → ( ( 𝑉 ‘ 𝑘 ) = ( 𝑉 ‘ 𝑖 ) ↔ 𝑘 = 𝑖 ) )
461 459 115 172 460 syl12anc ⊢ ( 𝜒 → ( ( 𝑉 ‘ 𝑘 ) = ( 𝑉 ‘ 𝑖 ) ↔ 𝑘 = 𝑖 ) )
462 457 461 mpbid ⊢ ( 𝜒 → 𝑘 = 𝑖 )
463 15 462 sylbir ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑘 = 𝑖 )
464 463 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) → 𝑘 = 𝑖 ) )
465 simpl ⊢ ( ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑘 = 𝑖 ) → ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
466 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 𝑖 ) )
467 oveq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 + 1 ) = ( 𝑖 + 1 ) )
468 467 fveq2d ⊢ ( 𝑘 = 𝑖 → ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
469 466 468 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
470 469 eqcomd ⊢ ( 𝑘 = 𝑖 → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) )
471 470 adantl ⊢ ( ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑘 = 𝑖 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) )
472 465 471 sseqtrd ⊢ ( ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑘 = 𝑖 ) → ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) )
473 472 ex ⊢ ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑘 = 𝑖 → ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) )
474 473 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑘 = 𝑖 → ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) )
475 464 474 impbid ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ↔ 𝑘 = 𝑖 ) )
476 475 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ 𝑀 ) ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ↔ 𝑘 = 𝑖 ) )
477 476 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ 𝑀 ) ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ↔ 𝑘 = 𝑖 ) ) )
478 477 reximdva ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∀ 𝑘 ∈ ( 0 ..^ 𝑀 ) ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ↔ 𝑘 = 𝑖 ) ) )
479 104 478 mpd ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∀ 𝑘 ∈ ( 0 ..^ 𝑀 ) ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ↔ 𝑘 = 𝑖 ) )
480 reu6 ⊢ ( ∃! 𝑘 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∀ 𝑘 ∈ ( 0 ..^ 𝑀 ) ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ↔ 𝑘 = 𝑖 ) )
481 479 480 sylibr ⊢ ( 𝜑 → ∃! 𝑘 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) )
482 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑘 ) )
483 oveq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 + 1 ) = ( 𝑘 + 1 ) )
484 483 fveq2d ⊢ ( 𝑖 = 𝑘 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) )
485 482 484 oveq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) )
486 485 sseq2d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) ) )
487 486 cbvreuvw ⊢ ( ∃! 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ∃! 𝑘 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑘 ) (,) ( 𝑄 ‘ ( 𝑘 + 1 ) ) ) )
488 481 487 sylibr ⊢ ( 𝜑 → ∃! 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
489 riotacl ⊢ ( ∃! 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ℩ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( 0 ..^ 𝑀 ) )
490 488 489 syl ⊢ ( 𝜑 → ( ℩ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( 0 ..^ 𝑀 ) )
491 14 490 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ ( 0 ..^ 𝑀 ) )
492 14 eqcomi ⊢ ( ℩ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = 𝑈
493 492 a1i ⊢ ( 𝜑 → ( ℩ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = 𝑈 )
494 fveq2 ⊢ ( 𝑖 = 𝑈 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑈 ) )
495 oveq1 ⊢ ( 𝑖 = 𝑈 → ( 𝑖 + 1 ) = ( 𝑈 + 1 ) )
496 495 fveq2d ⊢ ( 𝑖 = 𝑈 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) )
497 494 496 oveq12d ⊢ ( 𝑖 = 𝑈 → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) )
498 497 sseq2d ⊢ ( 𝑖 = 𝑈 → ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ) )
499 498 riota2 ⊢ ( ( 𝑈 ∈ ( 0 ..^ 𝑀 ) ∧ ∃! 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ↔ ( ℩ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = 𝑈 ) )
500 491 488 499 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ↔ ( ℩ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = 𝑈 ) )
501 493 500 mpbird ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) )
502 491 501 jca ⊢ ( 𝜑 → ( 𝑈 ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ) )