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