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