This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem71

Description: A periodic piecewise continuous function, possibly undefined on a finite set in each periodic interval, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem71.dmf ⊢ ( 𝜑 → dom 𝐹 ⊆ ℝ )
fourierdlem71.f ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
fourierdlem71.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem71.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem71.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem71.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem71.7 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem71.q ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
fourierdlem71.q0 ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
fourierdlem71.10 ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
fourierdlem71.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem71.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
fourierdlem71.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
fourierdlem71.xpt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ dom 𝐹 )
fourierdlem71.fxpt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
fourierdlem71.i ⊢ 𝐼 = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
fourierdlem71.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
Assertion fourierdlem71 ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )

Proof

Step Hyp Ref Expression
1 fourierdlem71.dmf ⊢ ( 𝜑 → dom 𝐹 ⊆ ℝ )
2 fourierdlem71.f ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
3 fourierdlem71.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4 fourierdlem71.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5 fourierdlem71.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
6 fourierdlem71.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
7 fourierdlem71.7 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
8 fourierdlem71.q ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
9 fourierdlem71.q0 ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
10 fourierdlem71.10 ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
11 fourierdlem71.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
12 fourierdlem71.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
13 fourierdlem71.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
14 fourierdlem71.xpt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ dom 𝐹 )
15 fourierdlem71.fxpt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
16 fourierdlem71.i ⊢ 𝐼 = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
17 fourierdlem71.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
18 prfi ⊢ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ∈ Fin
19 18 a1i ⊢ ( 𝜑 → { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ∈ Fin )
20 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → 𝐹 : dom 𝐹 ⟶ ℝ )
21 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → 𝜑 )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } )
23 ovex ⊢ ( 0 ... 𝑀 ) ∈ V
24 23 a1i ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ V )
25 8 24 fexd ⊢ ( 𝜑 → 𝑄 ∈ V )
26 rnexg ⊢ ( 𝑄 ∈ V → ran 𝑄 ∈ V )
27 inex1g ⊢ ( ran 𝑄 ∈ V → ( ran 𝑄 ∩ dom 𝐹 ) ∈ V )
28 25 26 27 3syl ⊢ ( 𝜑 → ( ran 𝑄 ∩ dom 𝐹 ) ∈ V )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ( ran 𝑄 ∩ dom 𝐹 ) ∈ V )
30 ovex ⊢ ( 0 ..^ 𝑀 ) ∈ V
31 30 mptex ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ V
32 16 31 eqeltri ⊢ 𝐼 ∈ V
33 32 rnex ⊢ ran 𝐼 ∈ V
34 33 a1i ⊢ ( 𝜑 → ran 𝐼 ∈ V )
35 34 uniexd ⊢ ( 𝜑 → ∪ ran 𝐼 ∈ V )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ∪ ran 𝐼 ∈ V )
37 uniprg ⊢ ( ( ( ran 𝑄 ∩ dom 𝐹 ) ∈ V ∧ ∪ ran 𝐼 ∈ V ) → ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } = ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
38 29 36 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } = ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
39 22 38 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
40 elinel2 ⊢ ( 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) → 𝑥 ∈ dom 𝐹 )
41 40 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ) ∧ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑥 ∈ dom 𝐹 )
42 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ) ∧ ¬ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝜑 )
43 elunnel1 ⊢ ( ( 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ∧ ¬ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑥 ∈ ∪ ran 𝐼 )
44 43 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ) ∧ ¬ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑥 ∈ ∪ ran 𝐼 )
45 16 funmpt2 ⊢ Fun 𝐼
46 elunirn ⊢ ( Fun 𝐼 → ( 𝑥 ∈ ∪ ran 𝐼 ↔ ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) )
47 45 46 ax-mp ⊢ ( 𝑥 ∈ ∪ ran 𝐼 ↔ ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
48 47 bilani ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
49 id ⊢ ( 𝑖 ∈ dom 𝐼 → 𝑖 ∈ dom 𝐼 )
50 ovex ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ V
51 50 16 dmmpti ⊢ dom 𝐼 = ( 0 ..^ 𝑀 )
52 49 51 eleqtrdi ⊢ ( 𝑖 ∈ dom 𝐼 → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
54 50 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ V )
55 16 fvmpt2 ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ V ) → ( 𝐼 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
56 53 54 55 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
57 cncff ⊢ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
58 fdm ⊢ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ → dom ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
59 11 57 58 3syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
60 52 59 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → dom ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
61 ssdmres ⊢ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
62 60 61 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 )
63 56 62 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑖 ) ⊆ dom 𝐹 )
64 63 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) → ( 𝐼 ‘ 𝑖 ) ⊆ dom 𝐹 )
65 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) → 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
66 64 65 sseldd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) → 𝑥 ∈ dom 𝐹 )
67 66 3exp ⊢ ( 𝜑 → ( 𝑖 ∈ dom 𝐼 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) → 𝑥 ∈ dom 𝐹 ) ) )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ( 𝑖 ∈ dom 𝐼 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) → 𝑥 ∈ dom 𝐹 ) ) )
69 68 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ( ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) → 𝑥 ∈ dom 𝐹 ) )
70 48 69 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → 𝑥 ∈ dom 𝐹 )
71 42 44 70 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ) ∧ ¬ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑥 ∈ dom 𝐹 )
72 41 71 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ) → 𝑥 ∈ dom 𝐹 )
73 21 39 72 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → 𝑥 ∈ dom 𝐹 )
74 20 73 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
75 74 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
76 75 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
77 simpr ⊢ ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) )
78 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
79 rnffi ⊢ ( ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ ∧ ( 0 ... 𝑀 ) ∈ Fin ) → ran 𝑄 ∈ Fin )
80 8 78 79 syl2anc ⊢ ( 𝜑 → ran 𝑄 ∈ Fin )
81 infi ⊢ ( ran 𝑄 ∈ Fin → ( ran 𝑄 ∩ dom 𝐹 ) ∈ Fin )
82 80 81 syl ⊢ ( 𝜑 → ( ran 𝑄 ∩ dom 𝐹 ) ∈ Fin )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → ( ran 𝑄 ∩ dom 𝐹 ) ∈ Fin )
84 77 83 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑤 ∈ Fin )
85 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ 𝑤 ) → 𝜑 )
86 simpr ⊢ ( ( 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ∧ 𝑥 ∈ 𝑤 ) → 𝑥 ∈ 𝑤 )
87 simpl ⊢ ( ( 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ∧ 𝑥 ∈ 𝑤 ) → 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) )
88 86 87 eleqtrd ⊢ ( ( 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ∧ 𝑥 ∈ 𝑤 ) → 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) )
89 88 adantll ⊢ ( ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ 𝑤 ) → 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) )
90 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝐹 : dom 𝐹 ⟶ ℝ )
91 40 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑥 ∈ dom 𝐹 )
92 90 91 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
93 92 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
94 93 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
95 85 89 94 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ 𝑤 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
96 95 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
97 fimaxre3 ⊢ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
98 84 96 97 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
99 98 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
100 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) ∧ ¬ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝜑 )
101 neqne ⊢ ( ¬ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) → 𝑤 ≠ ( ran 𝑄 ∩ dom 𝐹 ) )
102 elprn1 ⊢ ( ( 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ∧ 𝑤 ≠ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑤 = ∪ ran 𝐼 )
103 101 102 sylan2 ⊢ ( ( 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ∧ ¬ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑤 = ∪ ran 𝐼 )
104 103 adantll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) ∧ ¬ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑤 = ∪ ran 𝐼 )
105 fzofi ⊢ ( 0 ..^ 𝑀 ) ∈ Fin
106 16 rnmptfi ⊢ ( ( 0 ..^ 𝑀 ) ∈ Fin → ran 𝐼 ∈ Fin )
107 105 106 ax-mp ⊢ ran 𝐼 ∈ Fin
108 107 a1i ⊢ ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) → ran 𝐼 ∈ Fin )
109 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → 𝐹 : dom 𝐹 ⟶ ℝ )
110 109 70 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
111 110 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
112 111 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
113 112 abscld ⊢ ( ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
114 50 16 fnmpti ⊢ 𝐼 Fn ( 0 ..^ 𝑀 )
115 fvelrnb ⊢ ( 𝐼 Fn ( 0 ..^ 𝑀 ) → ( 𝑡 ∈ ran 𝐼 ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 ) )
116 114 115 ax-mp ⊢ ( 𝑡 ∈ ran 𝐼 ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 )
117 116 bilani ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐼 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 )
118 8 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
119 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
120 119 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
121 118 120 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
122 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
123 122 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
124 118 123 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
125 121 124 11 13 12 cncfioobd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 )
126 125 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 )
127 fvres ⊢ ( 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
128 127 fveq2d ⊢ ( 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
129 128 breq1d ⊢ ( 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 ↔ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
130 129 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 ↔ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
131 130 ralbidva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
132 131 rexbidv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
133 132 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
134 50 55 mpan2 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
135 id ⊢ ( ( 𝐼 ‘ 𝑖 ) = 𝑡 → ( 𝐼 ‘ 𝑖 ) = 𝑡 )
136 134 135 sylan9req ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = 𝑡 )
137 136 3adant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = 𝑡 )
138 137 raleqdv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
139 138 rexbidv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
140 133 139 bitrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
141 126 140 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
142 141 3exp ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝐼 ‘ 𝑖 ) = 𝑡 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) ) )
143 142 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐼 ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝐼 ‘ 𝑖 ) = 𝑡 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) ) )
144 143 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐼 ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
145 117 144 mpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐼 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
146 145 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) ∧ 𝑡 ∈ ran 𝐼 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
147 eqimss ⊢ ( 𝑤 = ∪ ran 𝐼 → 𝑤 ⊆ ∪ ran 𝐼 )
148 147 adantl ⊢ ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) → 𝑤 ⊆ ∪ ran 𝐼 )
149 108 113 146 148 ssfiunibd ⊢ ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
150 100 104 149 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) ∧ ¬ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
151 99 150 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
152 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ran 𝑄 )
153 elinel2 ⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) → 𝑥 ∈ dom 𝐹 )
154 153 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ dom 𝐹 )
155 152 154 elind ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) )
156 elun1 ⊢ ( 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) → 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
157 155 156 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
158 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → 𝑀 ∈ ℕ )
159 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
160 elinel1 ⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
161 160 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
162 9 eqcomd ⊢ ( 𝜑 → 𝐴 = ( 𝑄 ‘ 0 ) )
163 162 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → 𝐴 = ( 𝑄 ‘ 0 ) )
164 10 eqcomd ⊢ ( 𝜑 → 𝐵 = ( 𝑄 ‘ 𝑀 ) )
165 164 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → 𝐵 = ( 𝑄 ‘ 𝑀 ) )
166 163 165 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → ( 𝐴 [,] 𝐵 ) = ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) )
167 161 166 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → 𝑥 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) )
168 167 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) )
169 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → ¬ 𝑥 ∈ ran 𝑄 )
170 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 𝑗 ) )
171 170 breq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑄 ‘ 𝑘 ) < 𝑥 ↔ ( 𝑄 ‘ 𝑗 ) < 𝑥 ) )
172 171 cbvrabv ⊢ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝑥 } = { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) < 𝑥 }
173 172 supeq1i ⊢ sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝑥 } , ℝ , < ) = sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) < 𝑥 } , ℝ , < )
174 158 159 168 169 173 fourierdlem25 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
175 52 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
176 simprr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) ) → 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
177 175 134 syl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) ) → ( 𝐼 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
178 176 177 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) ) → 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
179 175 178 jca ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
180 id ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
181 180 51 eleqtrrdi ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ dom 𝐼 )
182 181 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) → 𝑖 ∈ dom 𝐼 )
183 simprr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) → 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
184 134 eqcomd ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐼 ‘ 𝑖 ) )
185 184 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐼 ‘ 𝑖 ) )
186 183 185 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) → 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
187 182 186 jca ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) )
188 179 187 impbida ⊢ ( 𝜑 → ( ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
189 188 rexbidv2 ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
190 189 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → ( ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
191 174 190 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
192 191 47 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ∪ ran 𝐼 )
193 elun2 ⊢ ( 𝑥 ∈ ∪ ran 𝐼 → 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
194 192 193 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
195 157 194 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
196 195 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
197 dfss3 ⊢ ( ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ⊆ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ↔ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
198 196 197 sylibr ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ⊆ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
199 28 35 37 syl2anc ⊢ ( 𝜑 → ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } = ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
200 198 199 sseqtrrd ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ⊆ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } )
201 19 76 151 200 ssfiunibd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
202 nfv ⊢ Ⅎ 𝑥 𝜑
203 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦
204 202 203 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
205 1 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ℝ )
206 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐵 ∈ ℝ )
207 206 205 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐵 − 𝑥 ) ∈ ℝ )
208 4 3 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
209 6 208 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
210 209 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑇 ∈ ℝ )
211 3 4 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
212 5 211 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
213 212 6 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑇 )
214 213 gt0ne0d ⊢ ( 𝜑 → 𝑇 ≠ 0 )
215 214 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑇 ≠ 0 )
216 207 210 215 redivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) ∈ ℝ )
217 216 flcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ )
218 217 zred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℝ )
219 218 210 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
220 205 219 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
221 17 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
222 205 220 221 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
223 222 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
224 fvex ⊢ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ V
225 eleq1 ⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑘 ∈ ℤ ↔ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) )
226 225 anbi2d ⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ) )
227 oveq1 ⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑘 · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
228 227 oveq2d ⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
229 228 fveq2d ⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
230 229 eqeq1d ⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) ) )
231 226 230 imbi12d ⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) ) ) )
232 224 231 15 vtocl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
233 217 232 mpdan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
234 223 233 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) )
235 234 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) ) )
236 235 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) ) )
237 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
238 237 fveq2d ⊢ ( 𝑥 = 𝑤 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) )
239 238 breq1d ⊢ ( 𝑥 = 𝑤 → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ↔ ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ≤ 𝑦 ) )
240 239 cbvralvw ⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ↔ ∀ 𝑤 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ≤ 𝑦 )
241 240 biimpi ⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 → ∀ 𝑤 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ≤ 𝑦 )
242 241 ad2antlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑥 ∈ dom 𝐹 ) → ∀ 𝑤 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ≤ 𝑦 )
243 iocssicc ⊢ ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
244 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐴 ∈ ℝ )
245 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐴 < 𝐵 )
246 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
247 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 − 𝑥 ) = ( 𝐵 − 𝑦 ) )
248 247 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − 𝑦 ) / 𝑇 ) )
249 248 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) )
250 249 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) )
251 246 250 oveq12d ⊢ ( 𝑥 = 𝑦 → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) )
252 251 cbvmptv ⊢ ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) )
253 17 252 eqtri ⊢ 𝐸 = ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) )
254 244 206 245 6 253 fourierdlem4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
255 254 205 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) )
256 243 255 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 [,] 𝐵 ) )
257 228 eleq1d ⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ dom 𝐹 ↔ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ dom 𝐹 ) )
258 226 257 imbi12d ⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ dom 𝐹 ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ dom 𝐹 ) ) )
259 224 258 14 vtocl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ dom 𝐹 )
260 217 259 mpdan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ dom 𝐹 )
261 222 260 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐸 ‘ 𝑥 ) ∈ dom 𝐹 )
262 256 261 elind ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐸 ‘ 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) )
263 262 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐸 ‘ 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) )
264 fveq2 ⊢ ( 𝑤 = ( 𝐸 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) )
265 264 fveq2d ⊢ ( 𝑤 = ( 𝐸 ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) ) )
266 265 breq1d ⊢ ( 𝑤 = ( 𝐸 ‘ 𝑥 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ≤ 𝑦 ↔ ( abs ‘ ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) ) ≤ 𝑦 ) )
267 266 rspccva ⊢ ( ( ∀ 𝑤 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ≤ 𝑦 ∧ ( 𝐸 ‘ 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) ) ≤ 𝑦 )
268 242 263 267 syl2anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( abs ‘ ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) ) ≤ 𝑦 )
269 236 268 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
270 269 ex ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) → ( 𝑥 ∈ dom 𝐹 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
271 204 270 ralrimi ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) → ∀ 𝑥 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
272 271 ex ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 → ∀ 𝑥 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
273 272 reximdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
274 201 273 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )