Metamath Proof Explorer

Theorem ovolicc1

Description: The measure of a closed interval is lower bounded by its length. (Contributed by Mario Carneiro, 13-Jun-2014) (Proof shortened by Mario Carneiro, 25-Mar-2015)

Ref Expression
Hypotheses ovolicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ovolicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ovolicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ovolicc1.4 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 = 1 , ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 0 , 0 ⟩ ) )
Assertion ovolicc1 ( 𝜑 → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ≤ ( 𝐵 − 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ovolicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 ovolicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ovolicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 ovolicc1.4 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 = 1 , ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 0 , 0 ⟩ ) )
5 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
6 1 2 5 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
7 ovolcl ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ℝ* )
8 6 7 syl ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ℝ* )
9 df-br ⊢ ( 𝐴 ≤ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≤ )
10 3 9 sylib ⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ≤ )
11 1 2 opelxpd ⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ℝ × ℝ ) )
12 10 11 elind ⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
14 0le0 ⊢ 0 ≤ 0
15 df-br ⊢ ( 0 ≤ 0 ↔ ⟨ 0 , 0 ⟩ ∈ ≤ )
16 14 15 mpbi ⊢ ⟨ 0 , 0 ⟩ ∈ ≤
17 0re ⊢ 0 ∈ ℝ
18 opelxpi ⊢ ( ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) → ⟨ 0 , 0 ⟩ ∈ ( ℝ × ℝ ) )
19 17 17 18 mp2an ⊢ ⟨ 0 , 0 ⟩ ∈ ( ℝ × ℝ )
20 16 19 elini ⊢ ⟨ 0 , 0 ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) )
21 ifcl ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ⟨ 0 , 0 ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ) → if ( 𝑛 = 1 , ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 0 , 0 ⟩ ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
22 13 20 21 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( 𝑛 = 1 , ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 0 , 0 ⟩ ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
23 22 4 fmptd ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
24 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐺 )
25 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
26 24 25 ovolsf ⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
27 23 26 syl ⊢ ( 𝜑 → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
28 27 frnd ⊢ ( 𝜑 → ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ⊆ ( 0 [,) +∞ ) )
29 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
30 28 29 sstrdi ⊢ ( 𝜑 → ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ⊆ ℝ* )
31 supxrcl ⊢ ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ⊆ ℝ* → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ* , < ) ∈ ℝ* )
32 30 31 syl ⊢ ( 𝜑 → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ* , < ) ∈ ℝ* )
33 2 1 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
34 33 rexrd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ* )
35 1nn ⊢ 1 ∈ ℕ
36 35 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 1 ∈ ℕ )
37 op1stg ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
38 1 2 37 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
40 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
41 1 2 40 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
42 41 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
43 42 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑥 )
44 39 43 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≤ 𝑥 )
45 42 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
46 op2ndg ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
47 1 2 46 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
49 45 48 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
50 fveq2 ⊢ ( 𝑛 = 1 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 1 ) )
51 iftrue ⊢ ( 𝑛 = 1 → if ( 𝑛 = 1 , ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 0 , 0 ⟩ ) = ⟨ 𝐴 , 𝐵 ⟩ )
52 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
53 51 4 52 fvmpt ⊢ ( 1 ∈ ℕ → ( 𝐺 ‘ 1 ) = ⟨ 𝐴 , 𝐵 ⟩ )
54 35 53 ax-mp ⊢ ( 𝐺 ‘ 1 ) = ⟨ 𝐴 , 𝐵 ⟩
55 50 54 eqtrdi ⊢ ( 𝑛 = 1 → ( 𝐺 ‘ 𝑛 ) = ⟨ 𝐴 , 𝐵 ⟩ )
56 55 fveq2d ⊢ ( 𝑛 = 1 → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
57 56 breq1d ⊢ ( 𝑛 = 1 → ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≤ 𝑥 ) )
58 55 fveq2d ⊢ ( 𝑛 = 1 → ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
59 58 breq2d ⊢ ( 𝑛 = 1 → ( 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ 𝑥 ≤ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
60 57 59 anbi12d ⊢ ( 𝑛 = 1 → ( ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ↔ ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
61 60 rspcev ⊢ ( ( 1 ∈ ℕ ∧ ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
62 36 44 49 61 syl12anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
63 62 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
64 ovolficc ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ↔ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
65 6 23 64 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ↔ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
66 63 65 mpbird ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) )
67 25 ovollb2 ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ) → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ* , < ) )
68 23 66 67 syl2anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ* , < ) )
69 addid1 ⊢ ( 𝑘 ∈ ℂ → ( 𝑘 + 0 ) = 𝑘 )
70 69 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ℂ ) → ( 𝑘 + 0 ) = 𝑘 )
71 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
72 35 71 eleqtri ⊢ 1 ∈ ( ℤ≥ ‘ 1 )
73 72 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → 1 ∈ ( ℤ≥ ‘ 1 ) )
74 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℕ )
75 74 71 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ( ℤ≥ ‘ 1 ) )
76 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
77 27 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
78 ffvelrn ⊢ ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) : ℕ ⟶ ( 0 [,) +∞ ) ∧ 1 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 1 ) ∈ ( 0 [,) +∞ ) )
79 77 35 78 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 1 ) ∈ ( 0 [,) +∞ ) )
80 76 79 sseldi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 1 ) ∈ ℝ )
81 80 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 1 ) ∈ ℂ )
82 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
83 elfzuz ⊢ ( 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
84 83 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
85 df-2 ⊢ 2 = ( 1 + 1 )
86 85 fveq2i ⊢ ( ℤ≥ ‘ 2 ) = ( ℤ≥ ‘ ( 1 + 1 ) )
87 84 86 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 2 ) )
88 eluz2nn ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → 𝑘 ∈ ℕ )
89 87 88 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → 𝑘 ∈ ℕ )
90 24 ovolfsval ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑘 ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
91 82 89 90 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑘 ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
92 eqeq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 = 1 ↔ 𝑘 = 1 ) )
93 92 ifbid ⊢ ( 𝑛 = 𝑘 → if ( 𝑛 = 1 , ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 0 , 0 ⟩ ) = if ( 𝑘 = 1 , ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 0 , 0 ⟩ ) )
94 opex ⊢ ⟨ 0 , 0 ⟩ ∈ V
95 52 94 ifex ⊢ if ( 𝑘 = 1 , ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 0 , 0 ⟩ ) ∈ V
96 93 4 95 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) = if ( 𝑘 = 1 , ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 0 , 0 ⟩ ) )
97 89 96 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → ( 𝐺 ‘ 𝑘 ) = if ( 𝑘 = 1 , ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 0 , 0 ⟩ ) )
98 eluz2b3 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ≠ 1 ) )
99 98 simprbi ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → 𝑘 ≠ 1 )
100 87 99 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → 𝑘 ≠ 1 )
101 100 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → ¬ 𝑘 = 1 )
102 101 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → if ( 𝑘 = 1 , ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 0 , 0 ⟩ ) = ⟨ 0 , 0 ⟩ )
103 97 102 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → ( 𝐺 ‘ 𝑘 ) = ⟨ 0 , 0 ⟩ )
104 103 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 2nd ‘ ⟨ 0 , 0 ⟩ ) )
105 c0ex ⊢ 0 ∈ V
106 105 105 op2nd ⊢ ( 2nd ‘ ⟨ 0 , 0 ⟩ ) = 0
107 104 106 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) = 0 )
108 103 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 1st ‘ ⟨ 0 , 0 ⟩ ) )
109 105 105 op1st ⊢ ( 1st ‘ ⟨ 0 , 0 ⟩ ) = 0
110 108 109 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) = 0 )
111 107 110 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ) = ( 0 − 0 ) )
112 0m0e0 ⊢ ( 0 − 0 ) = 0
113 111 112 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ) = 0 )
114 91 113 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... 𝑥 ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑘 ) = 0 )
115 70 73 75 81 114 seqid2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 1 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑥 ) )
116 1z ⊢ 1 ∈ ℤ
117 23 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
118 24 ovolfsval ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 1 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 1 ) = ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) ) )
119 117 35 118 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 1 ) = ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) ) )
120 54 fveq2i ⊢ ( 2nd ‘ ( 𝐺 ‘ 1 ) ) = ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ )
121 47 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
122 120 121 syl5eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 1 ) ) = 𝐵 )
123 54 fveq2i ⊢ ( 1st ‘ ( 𝐺 ‘ 1 ) ) = ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ )
124 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
125 123 124 syl5eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 1 ) ) = 𝐴 )
126 122 125 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) ) = ( 𝐵 − 𝐴 ) )
127 119 126 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 1 ) = ( 𝐵 − 𝐴 ) )
128 116 127 seq1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 1 ) = ( 𝐵 − 𝐴 ) )
129 115 128 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑥 ) = ( 𝐵 − 𝐴 ) )
130 33 leidd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( 𝐵 − 𝐴 ) )
131 130 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( 𝐵 − 𝐴 ) ≤ ( 𝐵 − 𝐴 ) )
132 129 131 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑥 ) ≤ ( 𝐵 − 𝐴 ) )
133 132 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑥 ) ≤ ( 𝐵 − 𝐴 ) )
134 27 ffnd ⊢ ( 𝜑 → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) Fn ℕ )
135 breq1 ⊢ ( 𝑧 = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑥 ) → ( 𝑧 ≤ ( 𝐵 − 𝐴 ) ↔ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑥 ) ≤ ( 𝐵 − 𝐴 ) ) )
136 135 ralrn ⊢ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) Fn ℕ → ( ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) 𝑧 ≤ ( 𝐵 − 𝐴 ) ↔ ∀ 𝑥 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑥 ) ≤ ( 𝐵 − 𝐴 ) ) )
137 134 136 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) 𝑧 ≤ ( 𝐵 − 𝐴 ) ↔ ∀ 𝑥 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑥 ) ≤ ( 𝐵 − 𝐴 ) ) )
138 133 137 mpbird ⊢ ( 𝜑 → ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) 𝑧 ≤ ( 𝐵 − 𝐴 ) )
139 supxrleub ⊢ ( ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ⊆ ℝ* ∧ ( 𝐵 − 𝐴 ) ∈ ℝ* ) → ( sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ* , < ) ≤ ( 𝐵 − 𝐴 ) ↔ ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) 𝑧 ≤ ( 𝐵 − 𝐴 ) ) )
140 30 34 139 syl2anc ⊢ ( 𝜑 → ( sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ* , < ) ≤ ( 𝐵 − 𝐴 ) ↔ ∀ 𝑧 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) 𝑧 ≤ ( 𝐵 − 𝐴 ) ) )
141 138 140 mpbird ⊢ ( 𝜑 → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ* , < ) ≤ ( 𝐵 − 𝐴 ) )
142 8 32 34 68 141 xrletrd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ≤ ( 𝐵 − 𝐴 ) )