Metamath Proof Explorer

Theorem itg2leub

Description: Any upper bound on the integrals of all simple functions G dominated by F is greater than ( S.2F ) , the least upper bound. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itg2leub ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐴 ∈ ℝ* ) → ( ( ∫2 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
2 1 itg2val ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐹 ) = sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )
3 2 adantr ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐴 ∈ ℝ* ) → ( ∫2 ‘ 𝐹 ) = sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )
4 3 breq1d ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐴 ∈ ℝ* ) → ( ( ∫2 ‘ 𝐹 ) ≤ 𝐴 ↔ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) ≤ 𝐴 ) )
5 1 itg2lcl ⊢ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } ⊆ ℝ*
6 supxrleub ⊢ ( ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } ⊆ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } 𝑧 ≤ 𝐴 ) )
7 5 6 mpan ⊢ ( 𝐴 ∈ ℝ* → ( sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } 𝑧 ≤ 𝐴 ) )
8 7 adantl ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐴 ∈ ℝ* ) → ( sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } 𝑧 ≤ 𝐴 ) )
9 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = ( ∫1 ‘ 𝑔 ) ↔ 𝑧 = ( ∫1 ‘ 𝑔 ) ) )
10 9 anbi2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) ↔ ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑧 = ( ∫1 ‘ 𝑔 ) ) ) )
11 10 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) ↔ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑧 = ( ∫1 ‘ 𝑔 ) ) ) )
12 11 ralab ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } 𝑧 ≤ 𝐴 ↔ ∀ 𝑧 ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑧 = ( ∫1 ‘ 𝑔 ) ) → 𝑧 ≤ 𝐴 ) )
13 r19.23v ⊢ ( ∀ 𝑔 ∈ dom ∫1 ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑧 = ( ∫1 ‘ 𝑔 ) ) → 𝑧 ≤ 𝐴 ) ↔ ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑧 = ( ∫1 ‘ 𝑔 ) ) → 𝑧 ≤ 𝐴 ) )
14 ancomst ⊢ ( ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑧 = ( ∫1 ‘ 𝑔 ) ) → 𝑧 ≤ 𝐴 ) ↔ ( ( 𝑧 = ( ∫1 ‘ 𝑔 ) ∧ 𝑔 ∘r ≤ 𝐹 ) → 𝑧 ≤ 𝐴 ) )
15 impexp ⊢ ( ( ( 𝑧 = ( ∫1 ‘ 𝑔 ) ∧ 𝑔 ∘r ≤ 𝐹 ) → 𝑧 ≤ 𝐴 ) ↔ ( 𝑧 = ( ∫1 ‘ 𝑔 ) → ( 𝑔 ∘r ≤ 𝐹 → 𝑧 ≤ 𝐴 ) ) )
16 14 15 bitri ⊢ ( ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑧 = ( ∫1 ‘ 𝑔 ) ) → 𝑧 ≤ 𝐴 ) ↔ ( 𝑧 = ( ∫1 ‘ 𝑔 ) → ( 𝑔 ∘r ≤ 𝐹 → 𝑧 ≤ 𝐴 ) ) )
17 16 ralbii ⊢ ( ∀ 𝑔 ∈ dom ∫1 ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑧 = ( ∫1 ‘ 𝑔 ) ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑧 = ( ∫1 ‘ 𝑔 ) → ( 𝑔 ∘r ≤ 𝐹 → 𝑧 ≤ 𝐴 ) ) )
18 13 17 bitr3i ⊢ ( ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑧 = ( ∫1 ‘ 𝑔 ) ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑧 = ( ∫1 ‘ 𝑔 ) → ( 𝑔 ∘r ≤ 𝐹 → 𝑧 ≤ 𝐴 ) ) )
19 18 albii ⊢ ( ∀ 𝑧 ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑧 = ( ∫1 ‘ 𝑔 ) ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑧 ∀ 𝑔 ∈ dom ∫1 ( 𝑧 = ( ∫1 ‘ 𝑔 ) → ( 𝑔 ∘r ≤ 𝐹 → 𝑧 ≤ 𝐴 ) ) )
20 ralcom4 ⊢ ( ∀ 𝑔 ∈ dom ∫1 ∀ 𝑧 ( 𝑧 = ( ∫1 ‘ 𝑔 ) → ( 𝑔 ∘r ≤ 𝐹 → 𝑧 ≤ 𝐴 ) ) ↔ ∀ 𝑧 ∀ 𝑔 ∈ dom ∫1 ( 𝑧 = ( ∫1 ‘ 𝑔 ) → ( 𝑔 ∘r ≤ 𝐹 → 𝑧 ≤ 𝐴 ) ) )
21 fvex ⊢ ( ∫1 ‘ 𝑔 ) ∈ V
22 breq1 ⊢ ( 𝑧 = ( ∫1 ‘ 𝑔 ) → ( 𝑧 ≤ 𝐴 ↔ ( ∫1 ‘ 𝑔 ) ≤ 𝐴 ) )
23 22 imbi2d ⊢ ( 𝑧 = ( ∫1 ‘ 𝑔 ) → ( ( 𝑔 ∘r ≤ 𝐹 → 𝑧 ≤ 𝐴 ) ↔ ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ 𝐴 ) ) )
24 21 23 ceqsalv ⊢ ( ∀ 𝑧 ( 𝑧 = ( ∫1 ‘ 𝑔 ) → ( 𝑔 ∘r ≤ 𝐹 → 𝑧 ≤ 𝐴 ) ) ↔ ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ 𝐴 ) )
25 24 ralbii ⊢ ( ∀ 𝑔 ∈ dom ∫1 ∀ 𝑧 ( 𝑧 = ( ∫1 ‘ 𝑔 ) → ( 𝑔 ∘r ≤ 𝐹 → 𝑧 ≤ 𝐴 ) ) ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ 𝐴 ) )
26 20 25 bitr3i ⊢ ( ∀ 𝑧 ∀ 𝑔 ∈ dom ∫1 ( 𝑧 = ( ∫1 ‘ 𝑔 ) → ( 𝑔 ∘r ≤ 𝐹 → 𝑧 ≤ 𝐴 ) ) ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ 𝐴 ) )
27 19 26 bitri ⊢ ( ∀ 𝑧 ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑧 = ( ∫1 ‘ 𝑔 ) ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ 𝐴 ) )
28 12 27 bitri ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } 𝑧 ≤ 𝐴 ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ 𝐴 ) )
29 8 28 bitrdi ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐴 ∈ ℝ* ) → ( sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ 𝐴 ) ) )
30 4 29 bitrd ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐴 ∈ ℝ* ) → ( ( ∫2 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ 𝐴 ) ) )