Metamath Proof Explorer

Theorem fourierdlem70

Description: A piecewise continuous function is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem70.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem70.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem70.aleb ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
fourierdlem70.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
fourierdlem70.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem70.q ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
fourierdlem70.q0 ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
fourierdlem70.qm ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
fourierdlem70.qlt ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
fourierdlem70.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem70.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
fourierdlem70.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
fourierdlem70.i ⊢ 𝐼 = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
Assertion fourierdlem70 ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑥 )

Proof

Step Hyp Ref Expression
1 fourierdlem70.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem70.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem70.aleb ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 fourierdlem70.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
5 fourierdlem70.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
6 fourierdlem70.q ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
7 fourierdlem70.q0 ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
8 fourierdlem70.qm ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
9 fourierdlem70.qlt ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
10 fourierdlem70.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
11 fourierdlem70.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
12 fourierdlem70.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
13 fourierdlem70.i ⊢ 𝐼 = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
14 prfi ⊢ { ran 𝑄 , ∪ ran 𝐼 } ∈ Fin
15 14 a1i ⊢ ( 𝜑 → { ran 𝑄 , ∪ ran 𝐼 } ∈ Fin )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ { ran 𝑄 , ∪ ran 𝐼 } ) → 𝑠 ∈ ∪ { ran 𝑄 , ∪ ran 𝐼 } )
17 ovex ⊢ ( 0 ... 𝑀 ) ∈ V
18 fex ⊢ ( ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ ∧ ( 0 ... 𝑀 ) ∈ V ) → 𝑄 ∈ V )
19 6 17 18 sylancl ⊢ ( 𝜑 → 𝑄 ∈ V )
20 rnexg ⊢ ( 𝑄 ∈ V → ran 𝑄 ∈ V )
21 19 20 syl ⊢ ( 𝜑 → ran 𝑄 ∈ V )
22 fzofi ⊢ ( 0 ..^ 𝑀 ) ∈ Fin
23 13 rnmptfi ⊢ ( ( 0 ..^ 𝑀 ) ∈ Fin → ran 𝐼 ∈ Fin )
24 22 23 ax-mp ⊢ ran 𝐼 ∈ Fin
25 24 elexi ⊢ ran 𝐼 ∈ V
26 25 uniex ⊢ ∪ ran 𝐼 ∈ V
27 uniprg ⊢ ( ( ran 𝑄 ∈ V ∧ ∪ ran 𝐼 ∈ V ) → ∪ { ran 𝑄 , ∪ ran 𝐼 } = ( ran 𝑄 ∪ ∪ ran 𝐼 ) )
28 21 26 27 sylancl ⊢ ( 𝜑 → ∪ { ran 𝑄 , ∪ ran 𝐼 } = ( ran 𝑄 ∪ ∪ ran 𝐼 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ { ran 𝑄 , ∪ ran 𝐼 } ) → ∪ { ran 𝑄 , ∪ ran 𝐼 } = ( ran 𝑄 ∪ ∪ ran 𝐼 ) )
30 16 29 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ { ran 𝑄 , ∪ ran 𝐼 } ) → 𝑠 ∈ ( ran 𝑄 ∪ ∪ ran 𝐼 ) )
31 eqid ⊢ ( 𝑦 ∈ ℕ ↦ { 𝑣 ∈ ( ℝ ↑m ( 0 ... 𝑦 ) ) ∣ ( ( ( 𝑣 ‘ 0 ) = 𝐴 ∧ ( 𝑣 ‘ 𝑦 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑦 ) ( 𝑣 ‘ 𝑖 ) < ( 𝑣 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑦 ∈ ℕ ↦ { 𝑣 ∈ ( ℝ ↑m ( 0 ... 𝑦 ) ) ∣ ( ( ( 𝑣 ‘ 0 ) = 𝐴 ∧ ( 𝑣 ‘ 𝑦 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑦 ) ( 𝑣 ‘ 𝑖 ) < ( 𝑣 ‘ ( 𝑖 + 1 ) ) ) } )
32 reex ⊢ ℝ ∈ V
33 32 17 elmap ⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ↔ 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
34 6 33 sylibr ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
35 7 8 jca ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) )
36 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
37 34 35 36 jca32 ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
38 31 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( ( 𝑦 ∈ ℕ ↦ { 𝑣 ∈ ( ℝ ↑m ( 0 ... 𝑦 ) ) ∣ ( ( ( 𝑣 ‘ 0 ) = 𝐴 ∧ ( 𝑣 ‘ 𝑦 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑦 ) ( 𝑣 ‘ 𝑖 ) < ( 𝑣 ‘ ( 𝑖 + 1 ) ) ) } ) ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
39 5 38 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( ( 𝑦 ∈ ℕ ↦ { 𝑣 ∈ ( ℝ ↑m ( 0 ... 𝑦 ) ) ∣ ( ( ( 𝑣 ‘ 0 ) = 𝐴 ∧ ( 𝑣 ‘ 𝑦 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑦 ) ( 𝑣 ‘ 𝑖 ) < ( 𝑣 ‘ ( 𝑖 + 1 ) ) ) } ) ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
40 37 39 mpbird ⊢ ( 𝜑 → 𝑄 ∈ ( ( 𝑦 ∈ ℕ ↦ { 𝑣 ∈ ( ℝ ↑m ( 0 ... 𝑦 ) ) ∣ ( ( ( 𝑣 ‘ 0 ) = 𝐴 ∧ ( 𝑣 ‘ 𝑦 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑦 ) ( 𝑣 ‘ 𝑖 ) < ( 𝑣 ‘ ( 𝑖 + 1 ) ) ) } ) ‘ 𝑀 ) )
41 31 5 40 fourierdlem15 ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
42 41 frnd ⊢ ( 𝜑 → ran 𝑄 ⊆ ( 𝐴 [,] 𝐵 ) )
43 42 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ran 𝑄 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
44 43 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ran 𝑄 ∪ ∪ ran 𝐼 ) ) ∧ 𝑠 ∈ ran 𝑄 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
45 simpll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ran 𝑄 ∪ ∪ ran 𝐼 ) ) ∧ ¬ 𝑠 ∈ ran 𝑄 ) → 𝜑 )
46 elunnel1 ⊢ ( ( 𝑠 ∈ ( ran 𝑄 ∪ ∪ ran 𝐼 ) ∧ ¬ 𝑠 ∈ ran 𝑄 ) → 𝑠 ∈ ∪ ran 𝐼 )
47 46 adantll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ran 𝑄 ∪ ∪ ran 𝐼 ) ) ∧ ¬ 𝑠 ∈ ran 𝑄 ) → 𝑠 ∈ ∪ ran 𝐼 )
48 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ran 𝐼 ) → 𝑠 ∈ ∪ ran 𝐼 )
49 13 funmpt2 ⊢ Fun 𝐼
50 elunirn ⊢ ( Fun 𝐼 → ( 𝑠 ∈ ∪ ran 𝐼 ↔ ∃ 𝑖 ∈ dom 𝐼 𝑠 ∈ ( 𝐼 ‘ 𝑖 ) ) )
51 49 50 mp1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ran 𝐼 ) → ( 𝑠 ∈ ∪ ran 𝐼 ↔ ∃ 𝑖 ∈ dom 𝐼 𝑠 ∈ ( 𝐼 ‘ 𝑖 ) ) )
52 48 51 mpbid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ran 𝐼 ) → ∃ 𝑖 ∈ dom 𝐼 𝑠 ∈ ( 𝐼 ‘ 𝑖 ) )
53 id ⊢ ( 𝑖 ∈ dom 𝐼 → 𝑖 ∈ dom 𝐼 )
54 ovex ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ V
55 54 13 dmmpti ⊢ dom 𝐼 = ( 0 ..^ 𝑀 )
56 53 55 eleqtrdi ⊢ ( 𝑖 ∈ dom 𝐼 → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
57 13 fvmpt2 ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ V ) → ( 𝐼 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
58 56 54 57 sylancl ⊢ ( 𝑖 ∈ dom 𝐼 → ( 𝐼 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
60 ioossicc ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
61 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → 𝐴 ∈ ℝ* )
63 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → 𝐵 ∈ ℝ* )
65 41 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
66 56 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
67 62 64 65 66 fourierdlem8 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
68 60 67 sstrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
69 59 68 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑖 ) ⊆ ( 𝐴 [,] 𝐵 ) )
70 69 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑠 ∈ ( 𝐼 ‘ 𝑖 ) ) → ( 𝐼 ‘ 𝑖 ) ⊆ ( 𝐴 [,] 𝐵 ) )
71 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑠 ∈ ( 𝐼 ‘ 𝑖 ) ) → 𝑠 ∈ ( 𝐼 ‘ 𝑖 ) )
72 70 71 sseldd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑠 ∈ ( 𝐼 ‘ 𝑖 ) ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
73 72 3exp ⊢ ( 𝜑 → ( 𝑖 ∈ dom 𝐼 → ( 𝑠 ∈ ( 𝐼 ‘ 𝑖 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ) )
74 73 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ran 𝐼 ) → ( 𝑖 ∈ dom 𝐼 → ( 𝑠 ∈ ( 𝐼 ‘ 𝑖 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ) )
75 74 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ran 𝐼 ) → ( ∃ 𝑖 ∈ dom 𝐼 𝑠 ∈ ( 𝐼 ‘ 𝑖 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) )
76 52 75 mpd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ran 𝐼 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
77 45 47 76 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ran 𝑄 ∪ ∪ ran 𝐼 ) ) ∧ ¬ 𝑠 ∈ ran 𝑄 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
78 44 77 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ran 𝑄 ∪ ∪ ran 𝐼 ) ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
79 30 78 syldan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ { ran 𝑄 , ∪ ran 𝐼 } ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
80 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑠 ) ∈ ℝ )
81 79 80 syldan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ { ran 𝑄 , ∪ ran 𝐼 } ) → ( 𝐹 ‘ 𝑠 ) ∈ ℝ )
82 81 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ { ran 𝑄 , ∪ ran 𝐼 } ) → ( 𝐹 ‘ 𝑠 ) ∈ ℂ )
83 82 abscld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ { ran 𝑄 , ∪ ran 𝐼 } ) → ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ∈ ℝ )
84 simpr ⊢ ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) → 𝑤 = ran 𝑄 )
85 6 adantr ⊢ ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
86 fzfid ⊢ ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) → ( 0 ... 𝑀 ) ∈ Fin )
87 rnffi ⊢ ( ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ ∧ ( 0 ... 𝑀 ) ∈ Fin ) → ran 𝑄 ∈ Fin )
88 85 86 87 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) → ran 𝑄 ∈ Fin )
89 84 88 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) → 𝑤 ∈ Fin )
90 89 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ran 𝑄 , ∪ ran 𝐼 } ) ∧ 𝑤 = ran 𝑄 ) → 𝑤 ∈ Fin )
91 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) ∧ 𝑠 ∈ 𝑤 ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
92 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) ∧ 𝑠 ∈ 𝑤 ) → 𝜑 )
93 simpr ⊢ ( ( 𝑤 = ran 𝑄 ∧ 𝑠 ∈ 𝑤 ) → 𝑠 ∈ 𝑤 )
94 simpl ⊢ ( ( 𝑤 = ran 𝑄 ∧ 𝑠 ∈ 𝑤 ) → 𝑤 = ran 𝑄 )
95 93 94 eleqtrd ⊢ ( ( 𝑤 = ran 𝑄 ∧ 𝑠 ∈ 𝑤 ) → 𝑠 ∈ ran 𝑄 )
96 95 adantll ⊢ ( ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) ∧ 𝑠 ∈ 𝑤 ) → 𝑠 ∈ ran 𝑄 )
97 92 96 43 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) ∧ 𝑠 ∈ 𝑤 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
98 91 97 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) ∧ 𝑠 ∈ 𝑤 ) → ( 𝐹 ‘ 𝑠 ) ∈ ℝ )
99 98 recnd ⊢ ( ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) ∧ 𝑠 ∈ 𝑤 ) → ( 𝐹 ‘ 𝑠 ) ∈ ℂ )
100 99 abscld ⊢ ( ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) ∧ 𝑠 ∈ 𝑤 ) → ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ∈ ℝ )
101 100 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑤 = ran 𝑄 ) → ∀ 𝑠 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ∈ ℝ )
102 101 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ran 𝑄 , ∪ ran 𝐼 } ) ∧ 𝑤 = ran 𝑄 ) → ∀ 𝑠 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ∈ ℝ )
103 fimaxre3 ⊢ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑠 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ∈ ℝ ) → ∃ 𝑧 ∈ ℝ ∀ 𝑠 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑧 )
104 90 102 103 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ran 𝑄 , ∪ ran 𝐼 } ) ∧ 𝑤 = ran 𝑄 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑠 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑧 )
105 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ran 𝑄 , ∪ ran 𝐼 } ) ∧ ¬ 𝑤 = ran 𝑄 ) → 𝜑 )
106 neqne ⊢ ( ¬ 𝑤 = ran 𝑄 → 𝑤 ≠ ran 𝑄 )
107 elprn1 ⊢ ( ( 𝑤 ∈ { ran 𝑄 , ∪ ran 𝐼 } ∧ 𝑤 ≠ ran 𝑄 ) → 𝑤 = ∪ ran 𝐼 )
108 106 107 sylan2 ⊢ ( ( 𝑤 ∈ { ran 𝑄 , ∪ ran 𝐼 } ∧ ¬ 𝑤 = ran 𝑄 ) → 𝑤 = ∪ ran 𝐼 )
109 108 adantll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ran 𝑄 , ∪ ran 𝐼 } ) ∧ ¬ 𝑤 = ran 𝑄 ) → 𝑤 = ∪ ran 𝐼 )
110 22 23 mp1i ⊢ ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) → ran 𝐼 ∈ Fin )
111 ax-resscn ⊢ ℝ ⊆ ℂ
112 111 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
113 4 112 fssd ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
114 113 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) ∧ 𝑠 ∈ ∪ ran 𝐼 ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
115 76 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) ∧ 𝑠 ∈ ∪ ran 𝐼 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
116 114 115 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) ∧ 𝑠 ∈ ∪ ran 𝐼 ) → ( 𝐹 ‘ 𝑠 ) ∈ ℂ )
117 116 abscld ⊢ ( ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) ∧ 𝑠 ∈ ∪ ran 𝐼 ) → ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ∈ ℝ )
118 54 13 fnmpti ⊢ 𝐼 Fn ( 0 ..^ 𝑀 )
119 fvelrnb ⊢ ( 𝐼 Fn ( 0 ..^ 𝑀 ) → ( 𝑡 ∈ ran 𝐼 ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 ) )
120 118 119 ax-mp ⊢ ( 𝑡 ∈ ran 𝐼 ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 )
121 120 bilani ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐼 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 )
122 6 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
123 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
124 123 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
125 122 124 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
126 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
127 126 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
128 122 127 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
129 125 128 10 12 11 cncfioobd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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 129 135 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 )
137 136 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 )
138 54 57 mpan2 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
139 138 eqcomd ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐼 ‘ 𝑖 ) )
140 139 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐼 ‘ 𝑖 ) )
141 simpr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( 𝐼 ‘ 𝑖 ) = 𝑡 )
142 140 141 eqtrd ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = 𝑡 )
143 142 raleqdv ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 ↔ ∀ 𝑠 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 ) )
144 143 rexbidv ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 ↔ ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 ) )
145 144 3adant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 ↔ ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 ) )
146 137 145 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 )
147 146 3exp ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝐼 ‘ 𝑖 ) = 𝑡 → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 ) ) )
148 147 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐼 ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝐼 ‘ 𝑖 ) = 𝑡 → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 ) ) )
149 148 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐼 ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 ) )
150 121 149 mpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐼 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 )
151 150 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) ∧ 𝑡 ∈ ran 𝐼 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑏 )
152 eqimss ⊢ ( 𝑤 = ∪ ran 𝐼 → 𝑤 ⊆ ∪ ran 𝐼 )
153 152 adantl ⊢ ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) → 𝑤 ⊆ ∪ ran 𝐼 )
154 110 117 151 153 ssfiunibd ⊢ ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑠 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑧 )
155 105 109 154 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ran 𝑄 , ∪ ran 𝐼 } ) ∧ ¬ 𝑤 = ran 𝑄 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑠 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑧 )
156 104 155 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { ran 𝑄 , ∪ ran 𝐼 } ) → ∃ 𝑧 ∈ ℝ ∀ 𝑠 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑧 )
157 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑡 ∈ ran 𝑄 ) → 𝑀 ∈ ℕ )
158 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑡 ∈ ran 𝑄 ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
159 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑡 ∈ ( 𝐴 [,] 𝐵 ) )
160 7 eqcomd ⊢ ( 𝜑 → 𝐴 = ( 𝑄 ‘ 0 ) )
161 8 eqcomd ⊢ ( 𝜑 → 𝐵 = ( 𝑄 ‘ 𝑀 ) )
162 160 161 oveq12d ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) = ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) )
163 162 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) = ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) )
164 159 163 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) )
165 164 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑡 ∈ ran 𝑄 ) → 𝑡 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) )
166 simpr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑡 ∈ ran 𝑄 ) → ¬ 𝑡 ∈ ran 𝑄 )
167 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 𝑗 ) )
168 167 breq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑄 ‘ 𝑘 ) < 𝑡 ↔ ( 𝑄 ‘ 𝑗 ) < 𝑡 ) )
169 168 cbvrabv ⊢ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝑡 } = { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) < 𝑡 }
170 169 supeq1i ⊢ sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝑡 } , ℝ , < ) = sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) < 𝑡 } , ℝ , < )
171 157 158 165 166 170 fourierdlem25 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑡 ∈ ran 𝑄 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
172 138 eleq2d ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑡 ∈ ( 𝐼 ‘ 𝑖 ) ↔ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
173 172 rexbiia ⊢ ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑡 ∈ ( 𝐼 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
174 171 173 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑡 ∈ ran 𝑄 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑡 ∈ ( 𝐼 ‘ 𝑖 ) )
175 55 eqcomi ⊢ ( 0 ..^ 𝑀 ) = dom 𝐼
176 175 rexeqi ⊢ ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑡 ∈ ( 𝐼 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ dom 𝐼 𝑡 ∈ ( 𝐼 ‘ 𝑖 ) )
177 174 176 sylib ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑡 ∈ ran 𝑄 ) → ∃ 𝑖 ∈ dom 𝐼 𝑡 ∈ ( 𝐼 ‘ 𝑖 ) )
178 elunirn ⊢ ( Fun 𝐼 → ( 𝑡 ∈ ∪ ran 𝐼 ↔ ∃ 𝑖 ∈ dom 𝐼 𝑡 ∈ ( 𝐼 ‘ 𝑖 ) ) )
179 49 178 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑡 ∈ ran 𝑄 ) → ( 𝑡 ∈ ∪ ran 𝐼 ↔ ∃ 𝑖 ∈ dom 𝐼 𝑡 ∈ ( 𝐼 ‘ 𝑖 ) ) )
180 177 179 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑡 ∈ ran 𝑄 ) → 𝑡 ∈ ∪ ran 𝐼 )
181 180 ex ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ¬ 𝑡 ∈ ran 𝑄 → 𝑡 ∈ ∪ ran 𝐼 ) )
182 181 orrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ran 𝑄 ∨ 𝑡 ∈ ∪ ran 𝐼 ) )
183 elun ⊢ ( 𝑡 ∈ ( ran 𝑄 ∪ ∪ ran 𝐼 ) ↔ ( 𝑡 ∈ ran 𝑄 ∨ 𝑡 ∈ ∪ ran 𝐼 ) )
184 182 183 sylibr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑡 ∈ ( ran 𝑄 ∪ ∪ ran 𝐼 ) )
185 184 ralrimiva ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑡 ∈ ( ran 𝑄 ∪ ∪ ran 𝐼 ) )
186 dfss3 ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ( ran 𝑄 ∪ ∪ ran 𝐼 ) ↔ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) 𝑡 ∈ ( ran 𝑄 ∪ ∪ ran 𝐼 ) )
187 185 186 sylibr ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( ran 𝑄 ∪ ∪ ran 𝐼 ) )
188 187 28 sseqtrrd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ { ran 𝑄 , ∪ ran 𝐼 } )
189 15 83 156 188 ssfiunibd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑠 ) ) ≤ 𝑥 )