Metamath Proof Explorer

Theorem fourierdlem46

Description: The function F has a limit at the bounds of every interval induced by the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem46.cn ⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) )
fourierdlem46.rlim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
fourierdlem46.llim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
fourierdlem46.qiso ⊢ ( 𝜑 → 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) )
fourierdlem46.qf ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ 𝐻 )
fourierdlem46.i ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝑀 ) )
fourierdlem46.10 ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
fourierdlem46.qiss ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( - π (,) π ) )
fourierdlem46.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem46.h ⊢ 𝐻 = ( { - π , π , 𝐶 } ∪ ( ( - π [,] π ) ∖ dom 𝐹 ) )
fourierdlem46.ranq ⊢ ( 𝜑 → ran 𝑄 = 𝐻 )
Assertion fourierdlem46 ( 𝜑 → ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ≠ ∅ ∧ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 fourierdlem46.cn ⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) )
2 fourierdlem46.rlim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
3 fourierdlem46.llim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
4 fourierdlem46.qiso ⊢ ( 𝜑 → 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) )
5 fourierdlem46.qf ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ 𝐻 )
6 fourierdlem46.i ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝑀 ) )
7 fourierdlem46.10 ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
8 fourierdlem46.qiss ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( - π (,) π ) )
9 fourierdlem46.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
10 fourierdlem46.h ⊢ 𝐻 = ( { - π , π , 𝐶 } ∪ ( ( - π [,] π ) ∖ dom 𝐹 ) )
11 fourierdlem46.ranq ⊢ ( 𝜑 → ran 𝑄 = 𝐻 )
12 pire ⊢ π ∈ ℝ
13 12 a1i ⊢ ( 𝜑 → π ∈ ℝ )
14 13 renegcld ⊢ ( 𝜑 → - π ∈ ℝ )
15 tpssi ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ∧ 𝐶 ∈ ℝ ) → { - π , π , 𝐶 } ⊆ ℝ )
16 14 13 9 15 syl3anc ⊢ ( 𝜑 → { - π , π , 𝐶 } ⊆ ℝ )
17 14 13 iccssred ⊢ ( 𝜑 → ( - π [,] π ) ⊆ ℝ )
18 17 ssdifssd ⊢ ( 𝜑 → ( ( - π [,] π ) ∖ dom 𝐹 ) ⊆ ℝ )
19 16 18 unssd ⊢ ( 𝜑 → ( { - π , π , 𝐶 } ∪ ( ( - π [,] π ) ∖ dom 𝐹 ) ) ⊆ ℝ )
20 10 19 eqsstrid ⊢ ( 𝜑 → 𝐻 ⊆ ℝ )
21 elfzofz ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → 𝐼 ∈ ( 0 ... 𝑀 ) )
22 6 21 syl ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... 𝑀 ) )
23 5 22 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ 𝐻 )
24 20 23 sseldd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ℝ )
25 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( 𝑄 ‘ 𝐼 ) ∈ ℝ )
26 fzofzp1 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
27 6 26 syl ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
28 5 27 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ 𝐻 )
29 20 28 sseldd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
30 29 rexrd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
31 30 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
32 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( 𝑄 ‘ 𝐼 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
33 simpr ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ∧ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → 𝑥 = ( 𝑄 ‘ 𝐼 ) )
34 simpl ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ∧ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 )
35 33 34 eqeltrd ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ∧ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → 𝑥 ∈ dom 𝐹 )
36 35 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) ∧ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → 𝑥 ∈ dom 𝐹 )
37 36 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → 𝑥 ∈ dom 𝐹 )
38 ssun2 ⊢ ( ( - π [,] π ) ∖ dom 𝐹 ) ⊆ ( { - π , π , 𝐶 } ∪ ( ( - π [,] π ) ∖ dom 𝐹 ) )
39 38 10 sseqtrri ⊢ ( ( - π [,] π ) ∖ dom 𝐹 ) ⊆ 𝐻
40 ioossicc ⊢ ( - π (,) π ) ⊆ ( - π [,] π )
41 8 40 sstrdi ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( - π [,] π ) )
42 41 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ∈ ( - π [,] π ) )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ( - π [,] π ) )
44 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → ¬ 𝑥 ∈ dom 𝐹 )
45 43 44 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ( ( - π [,] π ) ∖ dom 𝐹 ) )
46 39 45 sselid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ 𝐻 )
47 11 eqcomd ⊢ ( 𝜑 → 𝐻 = ran 𝑄 )
48 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝐻 = ran 𝑄 )
49 46 48 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ran 𝑄 )
50 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ran 𝑄 )
51 ffn ⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ 𝐻 → 𝑄 Fn ( 0 ... 𝑀 ) )
52 5 51 syl ⊢ ( 𝜑 → 𝑄 Fn ( 0 ... 𝑀 ) )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝑄 ) → 𝑄 Fn ( 0 ... 𝑀 ) )
54 fvelrnb ⊢ ( 𝑄 Fn ( 0 ... 𝑀 ) → ( 𝑥 ∈ ran 𝑄 ↔ ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑗 ) = 𝑥 ) )
55 53 54 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝑄 ) → ( 𝑥 ∈ ran 𝑄 ↔ ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑗 ) = 𝑥 ) )
56 50 55 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝑄 ) → ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑗 ) = 𝑥 )
57 56 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ 𝑥 ∈ ran 𝑄 ) → ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑗 ) = 𝑥 )
58 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℤ )
59 58 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ 𝑥 ∈ ran 𝑄 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑥 ) → 𝑗 ∈ ℤ )
60 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑥 ) → 𝜑 )
61 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑥 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
62 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑥 ) → ( 𝑄 ‘ 𝑗 ) = 𝑥 )
63 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑥 ) → 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
64 62 63 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑥 ) → ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
65 64 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑥 ) → ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
66 elfzoelz ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → 𝐼 ∈ ℤ )
67 6 66 syl ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
68 67 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝐼 ∈ ℤ )
69 24 rexrd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ℝ* )
70 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐼 ) ∈ ℝ* )
71 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
72 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
73 ioogtlb ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐼 ) < ( 𝑄 ‘ 𝑗 ) )
74 70 71 72 73 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐼 ) < ( 𝑄 ‘ 𝑗 ) )
75 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) )
76 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝐼 ∈ ( 0 ... 𝑀 ) )
77 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
78 isorel ⊢ ( ( 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) ∧ ( 𝐼 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ) → ( 𝐼 < 𝑗 ↔ ( 𝑄 ‘ 𝐼 ) < ( 𝑄 ‘ 𝑗 ) ) )
79 75 76 77 78 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝐼 < 𝑗 ↔ ( 𝑄 ‘ 𝐼 ) < ( 𝑄 ‘ 𝑗 ) ) )
80 74 79 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝐼 < 𝑗 )
81 iooltub ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑗 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
82 70 71 72 81 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑗 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
83 27 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
84 isorel ⊢ ( ( 𝑄 Isom < , < ( ( 0 ... 𝑀 ) , 𝐻 ) ∧ ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) ) ) → ( 𝑗 < ( 𝐼 + 1 ) ↔ ( 𝑄 ‘ 𝑗 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
85 75 77 83 84 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑗 < ( 𝐼 + 1 ) ↔ ( 𝑄 ‘ 𝑗 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
86 82 85 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑗 < ( 𝐼 + 1 ) )
87 btwnnz ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝐼 < 𝑗 ∧ 𝑗 < ( 𝐼 + 1 ) ) → ¬ 𝑗 ∈ ℤ )
88 68 80 86 87 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ¬ 𝑗 ∈ ℤ )
89 60 61 65 88 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑥 ) → ¬ 𝑗 ∈ ℤ )
90 89 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ 𝑥 ∈ ran 𝑄 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑥 ) → ¬ 𝑗 ∈ ℤ )
91 59 90 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ 𝑥 ∈ ran 𝑄 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ¬ ( 𝑄 ‘ 𝑗 ) = 𝑥 )
92 91 nrexdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ 𝑥 ∈ ran 𝑄 ) → ¬ ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑗 ) = 𝑥 )
93 57 92 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ¬ 𝑥 ∈ ran 𝑄 )
94 93 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → ¬ 𝑥 ∈ ran 𝑄 )
95 49 94 condan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ∈ dom 𝐹 )
96 95 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) 𝑥 ∈ dom 𝐹 )
97 dfss3 ⊢ ( ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ dom 𝐹 ↔ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) 𝑥 ∈ dom 𝐹 )
98 96 97 sylibr ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ dom 𝐹 )
99 98 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ dom 𝐹 )
100 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → ( 𝑄 ‘ 𝐼 ) ∈ ℝ* )
101 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
102 icossre ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ) → ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ℝ )
103 24 30 102 syl2anc ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ℝ )
104 103 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ∈ ℝ )
105 104 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → 𝑥 ∈ ℝ )
106 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → ( 𝑄 ‘ 𝐼 ) ∈ ℝ )
107 69 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐼 ) ∈ ℝ* )
108 30 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
109 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
110 icogelb ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐼 ) ≤ 𝑥 )
111 107 108 109 110 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐼 ) ≤ 𝑥 )
112 111 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → ( 𝑄 ‘ 𝐼 ) ≤ 𝑥 )
113 neqne ⊢ ( ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) → 𝑥 ≠ ( 𝑄 ‘ 𝐼 ) )
114 113 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → 𝑥 ≠ ( 𝑄 ‘ 𝐼 ) )
115 106 105 112 114 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → ( 𝑄 ‘ 𝐼 ) < 𝑥 )
116 icoltub ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
117 107 108 109 116 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
118 117 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → 𝑥 < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
119 100 101 105 115 118 eliood ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
120 99 119 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → 𝑥 ∈ dom 𝐹 )
121 120 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ 𝐼 ) ) → 𝑥 ∈ dom 𝐹 )
122 37 121 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ∈ dom 𝐹 )
123 122 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) 𝑥 ∈ dom 𝐹 )
124 dfss3 ⊢ ( ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ dom 𝐹 ↔ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) 𝑥 ∈ dom 𝐹 )
125 123 124 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ dom 𝐹 )
126 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) )
127 rescncf ⊢ ( ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ dom 𝐹 → ( 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) –cn→ ℂ ) ) )
128 125 126 127 sylc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) –cn→ ℂ ) )
129 25 31 32 128 icocncflimc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ‘ ( 𝑄 ‘ 𝐼 ) ) ∈ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) )
130 24 leidd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ≤ ( 𝑄 ‘ 𝐼 ) )
131 69 30 69 130 7 elicod ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
132 fvres ⊢ ( ( 𝑄 ‘ 𝐼 ) ∈ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ‘ ( 𝑄 ‘ 𝐼 ) ) = ( 𝐹 ‘ ( 𝑄 ‘ 𝐼 ) ) )
133 131 132 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ‘ ( 𝑄 ‘ 𝐼 ) ) = ( 𝐹 ‘ ( 𝑄 ‘ 𝐼 ) ) )
134 133 eqcomd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑄 ‘ 𝐼 ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ‘ ( 𝑄 ‘ 𝐼 ) ) )
135 134 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( 𝐹 ‘ ( 𝑄 ‘ 𝐼 ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ‘ ( 𝑄 ‘ 𝐼 ) ) )
136 ioossico ⊢ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
137 136 a1i ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
138 137 resabs1d ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) = ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
139 138 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
140 139 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) = ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) [,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) )
141 129 135 140 3eltr4d ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( 𝐹 ‘ ( 𝑄 ‘ 𝐼 ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) )
142 141 ne0d ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ≠ ∅ )
143 pnfxr ⊢ +∞ ∈ ℝ*
144 143 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
145 29 ltpnfd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < +∞ )
146 30 144 145 xrltled ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ +∞ )
147 iooss2 ⊢ ( ( +∞ ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ +∞ ) → ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) )
148 143 146 147 sylancr ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) )
149 148 resabs1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) = ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
150 149 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) )
151 150 eqcomd ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) = ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) )
152 151 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) = ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) )
153 limcresi ⊢ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ⊆ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) )
154 24 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( 𝑄 ‘ 𝐼 ) ∈ ℝ )
155 simpl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → 𝜑 )
156 12 renegcli ⊢ - π ∈ ℝ
157 156 rexri ⊢ - π ∈ ℝ*
158 157 a1i ⊢ ( 𝜑 → - π ∈ ℝ* )
159 12 rexri ⊢ π ∈ ℝ*
160 159 a1i ⊢ ( 𝜑 → π ∈ ℝ* )
161 14 13 24 29 7 8 fourierdlem10 ⊢ ( 𝜑 → ( - π ≤ ( 𝑄 ‘ 𝐼 ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ π ) )
162 161 simpld ⊢ ( 𝜑 → - π ≤ ( 𝑄 ‘ 𝐼 ) )
163 161 simprd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ π )
164 24 29 13 7 163 ltletrd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) < π )
165 158 160 69 162 164 elicod ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ( - π [,) π ) )
166 165 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( 𝑄 ‘ 𝐼 ) ∈ ( - π [,) π ) )
167 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ¬ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 )
168 166 167 eldifd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( 𝑄 ‘ 𝐼 ) ∈ ( ( - π [,) π ) ∖ dom 𝐹 ) )
169 155 168 jca ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ ( ( - π [,) π ) ∖ dom 𝐹 ) ) )
170 eleq1 ⊢ ( 𝑥 = ( 𝑄 ‘ 𝐼 ) → ( 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐹 ) ↔ ( 𝑄 ‘ 𝐼 ) ∈ ( ( - π [,) π ) ∖ dom 𝐹 ) ) )
171 170 anbi2d ⊢ ( 𝑥 = ( 𝑄 ‘ 𝐼 ) → ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐹 ) ) ↔ ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ ( ( - π [,) π ) ∖ dom 𝐹 ) ) ) )
172 oveq1 ⊢ ( 𝑥 = ( 𝑄 ‘ 𝐼 ) → ( 𝑥 (,) +∞ ) = ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) )
173 172 reseq2d ⊢ ( 𝑥 = ( 𝑄 ‘ 𝐼 ) → ( 𝐹 ↾ ( 𝑥 (,) +∞ ) ) = ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) )
174 id ⊢ ( 𝑥 = ( 𝑄 ‘ 𝐼 ) → 𝑥 = ( 𝑄 ‘ 𝐼 ) )
175 173 174 oveq12d ⊢ ( 𝑥 = ( 𝑄 ‘ 𝐼 ) → ( ( 𝐹 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) )
176 175 neeq1d ⊢ ( 𝑥 = ( 𝑄 ‘ 𝐼 ) → ( ( ( 𝐹 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ ↔ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ≠ ∅ ) )
177 171 176 imbi12d ⊢ ( 𝑥 = ( 𝑄 ‘ 𝐼 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ ) ↔ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ ( ( - π [,) π ) ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ≠ ∅ ) ) )
178 177 2 vtoclg ⊢ ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ → ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐼 ) ∈ ( ( - π [,) π ) ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ≠ ∅ ) )
179 154 169 178 sylc ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ≠ ∅ )
180 ssn0 ⊢ ( ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ⊆ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ∧ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ≠ ∅ ) → ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ≠ ∅ )
181 153 179 180 sylancr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) +∞ ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ≠ ∅ )
182 152 181 eqnetrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ 𝐼 ) ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ≠ ∅ )
183 142 182 pm2.61dan ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ≠ ∅ )
184 69 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( 𝑄 ‘ 𝐼 ) ∈ ℝ* )
185 29 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
186 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( 𝑄 ‘ 𝐼 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
187 simpr ⊢ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ∧ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
188 simpl ⊢ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ∧ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 )
189 187 188 eqeltrd ⊢ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ∧ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝑥 ∈ dom 𝐹 )
190 189 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) ∧ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝑥 ∈ dom 𝐹 )
191 190 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝑥 ∈ dom 𝐹 )
192 98 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ dom 𝐹 )
193 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ 𝐼 ) ∈ ℝ* )
194 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
195 69 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐼 ) ∈ ℝ* )
196 29 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
197 iocssre ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) → ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ℝ )
198 195 196 197 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ℝ )
199 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
200 198 199 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ∈ ℝ )
201 200 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝑥 ∈ ℝ )
202 30 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
203 iocgtlb ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐼 ) < 𝑥 )
204 195 202 199 203 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐼 ) < 𝑥 )
205 204 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ 𝐼 ) < 𝑥 )
206 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
207 iocleub ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
208 195 202 199 207 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
209 208 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝑥 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
210 neqne ⊢ ( ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) → 𝑥 ≠ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
211 210 necomd ⊢ ( ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≠ 𝑥 )
212 211 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≠ 𝑥 )
213 201 206 209 212 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝑥 < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
214 193 194 201 205 213 eliood ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
215 192 214 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝑥 ∈ dom 𝐹 )
216 215 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝑥 ∈ dom 𝐹 )
217 191 216 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ∈ dom 𝐹 )
218 217 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) 𝑥 ∈ dom 𝐹 )
219 dfss3 ⊢ ( ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ dom 𝐹 ↔ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) 𝑥 ∈ dom 𝐹 )
220 218 219 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ dom 𝐹 )
221 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) )
222 rescncf ⊢ ( ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ dom 𝐹 → ( 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) –cn→ ℂ ) ) )
223 220 221 222 sylc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) –cn→ ℂ ) )
224 184 185 186 223 ioccncflimc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ‘ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ∈ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
225 29 leidd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
226 69 30 30 7 225 eliocd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
227 fvres ⊢ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ‘ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
228 226 227 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ‘ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
229 228 eqcomd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ‘ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
230 ioossioc ⊢ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
231 resabs1 ⊢ ( ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) = ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
232 230 231 ax-mp ⊢ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) = ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
233 232 eqcomi ⊢ ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
234 233 oveq1i ⊢ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) = ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
235 234 a1i ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) = ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
236 229 235 eleq12d ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ↔ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ‘ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ∈ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
237 236 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( ( 𝐹 ‘ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ↔ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ‘ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ∈ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
238 224 237 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( 𝐹 ‘ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
239 238 ne0d ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ≠ ∅ )
240 mnfxr ⊢ -∞ ∈ ℝ*
241 240 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
242 24 mnfltd ⊢ ( 𝜑 → -∞ < ( 𝑄 ‘ 𝐼 ) )
243 241 69 242 xrltled ⊢ ( 𝜑 → -∞ ≤ ( 𝑄 ‘ 𝐼 ) )
244 iooss1 ⊢ ( ( -∞ ∈ ℝ* ∧ -∞ ≤ ( 𝑄 ‘ 𝐼 ) ) → ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
245 240 243 244 sylancr ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
246 245 resabs1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) = ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
247 246 eqcomd ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) = ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
248 247 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) = ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
249 248 oveq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) = ( ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
250 limcresi ⊢ ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
251 29 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
252 simpl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → 𝜑 )
253 157 a1i ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → - π ∈ ℝ* )
254 159 a1i ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → π ∈ ℝ* )
255 30 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
256 14 24 29 162 7 lelttrd ⊢ ( 𝜑 → - π < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
257 256 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → - π < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
258 163 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ π )
259 253 254 255 257 258 eliocd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( - π (,] π ) )
260 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 )
261 259 260 eldifd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( ( - π (,] π ) ∖ dom 𝐹 ) )
262 252 261 jca ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( ( - π (,] π ) ∖ dom 𝐹 ) ) )
263 eleq1 ⊢ ( 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) → ( 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐹 ) ↔ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( ( - π (,] π ) ∖ dom 𝐹 ) ) )
264 263 anbi2d ⊢ ( 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) → ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐹 ) ) ↔ ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( ( - π (,] π ) ∖ dom 𝐹 ) ) ) )
265 oveq2 ⊢ ( 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) → ( -∞ (,) 𝑥 ) = ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
266 265 reseq2d ⊢ ( 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) → ( 𝐹 ↾ ( -∞ (,) 𝑥 ) ) = ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
267 id ⊢ ( 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) → 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
268 266 267 oveq12d ⊢ ( 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) → ( ( 𝐹 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) = ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
269 268 neeq1d ⊢ ( 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) → ( ( ( 𝐹 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ ↔ ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ≠ ∅ ) )
270 264 269 imbi12d ⊢ ( 𝑥 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ ) ↔ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( ( - π (,] π ) ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ≠ ∅ ) ) )
271 270 3 vtoclg ⊢ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ → ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( ( - π (,] π ) ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ≠ ∅ ) )
272 251 262 271 sylc ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ≠ ∅ )
273 ssn0 ⊢ ( ( ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ∧ ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ≠ ∅ ) → ( ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ≠ ∅ )
274 250 272 273 sylancr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( ( ( 𝐹 ↾ ( -∞ (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ≠ ∅ )
275 249 274 eqnetrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ≠ ∅ )
276 239 275 pm2.61dan ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ≠ ∅ )
277 183 276 jca ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝐼 ) ) ≠ ∅ ∧ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ≠ ∅ ) )