MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolicc1 Structured version   Visualization version   GIF version

Theorem ovolicc1 24413
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.)
Hypotheses
Ref Expression
ovolicc.1 (𝜑𝐴 ∈ ℝ)
ovolicc.2 (𝜑𝐵 ∈ ℝ)
ovolicc.3 (𝜑𝐴𝐵)
ovolicc1.4 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩))
Assertion
Ref Expression
ovolicc1 (𝜑 → (vol*‘(𝐴[,]𝐵)) ≤ (𝐵𝐴))
Distinct variable groups:   𝐴,𝑛   𝐵,𝑛   𝑛,𝐺   𝜑,𝑛

Proof of Theorem ovolicc1
Dummy variables 𝑘 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovolicc.1 . . . 4 (𝜑𝐴 ∈ ℝ)
2 ovolicc.2 . . . 4 (𝜑𝐵 ∈ ℝ)
3 iccssre 13017 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
41, 2, 3syl2anc 587 . . 3 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
5 ovolcl 24375 . . 3 ((𝐴[,]𝐵) ⊆ ℝ → (vol*‘(𝐴[,]𝐵)) ∈ ℝ*)
64, 5syl 17 . 2 (𝜑 → (vol*‘(𝐴[,]𝐵)) ∈ ℝ*)
7 ovolicc.3 . . . . . . . . . . 11 (𝜑𝐴𝐵)
8 df-br 5054 . . . . . . . . . . 11 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≤ )
97, 8sylib 221 . . . . . . . . . 10 (𝜑 → ⟨𝐴, 𝐵⟩ ∈ ≤ )
101, 2opelxpd 5589 . . . . . . . . . 10 (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (ℝ × ℝ))
119, 10elind 4108 . . . . . . . . 9 (𝜑 → ⟨𝐴, 𝐵⟩ ∈ ( ≤ ∩ (ℝ × ℝ)))
1211adantr 484 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨𝐴, 𝐵⟩ ∈ ( ≤ ∩ (ℝ × ℝ)))
13 0le0 11931 . . . . . . . . . 10 0 ≤ 0
14 df-br 5054 . . . . . . . . . 10 (0 ≤ 0 ↔ ⟨0, 0⟩ ∈ ≤ )
1513, 14mpbi 233 . . . . . . . . 9 ⟨0, 0⟩ ∈ ≤
16 0re 10835 . . . . . . . . . 10 0 ∈ ℝ
17 opelxpi 5588 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 0 ∈ ℝ) → ⟨0, 0⟩ ∈ (ℝ × ℝ))
1816, 16, 17mp2an 692 . . . . . . . . 9 ⟨0, 0⟩ ∈ (ℝ × ℝ)
1915, 18elini 4107 . . . . . . . 8 ⟨0, 0⟩ ∈ ( ≤ ∩ (ℝ × ℝ))
20 ifcl 4484 . . . . . . . 8 ((⟨𝐴, 𝐵⟩ ∈ ( ≤ ∩ (ℝ × ℝ)) ∧ ⟨0, 0⟩ ∈ ( ≤ ∩ (ℝ × ℝ))) → if(𝑛 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩) ∈ ( ≤ ∩ (ℝ × ℝ)))
2112, 19, 20sylancl 589 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → if(𝑛 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩) ∈ ( ≤ ∩ (ℝ × ℝ)))
22 ovolicc1.4 . . . . . . 7 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩))
2321, 22fmptd 6931 . . . . . 6 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
24 eqid 2737 . . . . . . 7 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
25 eqid 2737 . . . . . . 7 seq1( + , ((abs ∘ − ) ∘ 𝐺)) = seq1( + , ((abs ∘ − ) ∘ 𝐺))
2624, 25ovolsf 24369 . . . . . 6 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞))
2723, 26syl 17 . . . . 5 (𝜑 → seq1( + , ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞))
2827frnd 6553 . . . 4 (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ (0[,)+∞))
29 icossxr 13020 . . . 4 (0[,)+∞) ⊆ ℝ*
3028, 29sstrdi 3913 . . 3 (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ*)
31 supxrcl 12905 . . 3 (ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈ ℝ*)
3230, 31syl 17 . 2 (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈ ℝ*)
332, 1resubcld 11260 . . 3 (𝜑 → (𝐵𝐴) ∈ ℝ)
3433rexrd 10883 . 2 (𝜑 → (𝐵𝐴) ∈ ℝ*)
35 1nn 11841 . . . . . . 7 1 ∈ ℕ
3635a1i 11 . . . . . 6 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 1 ∈ ℕ)
37 op1stg 7773 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)
381, 2, 37syl2anc 587 . . . . . . . 8 (𝜑 → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)
3938adantr 484 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)
40 elicc2 13000 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
411, 2, 40syl2anc 587 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
4241biimpa 480 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵))
4342simp2d 1145 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝐴𝑥)
4439, 43eqbrtrd 5075 . . . . . 6 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (1st ‘⟨𝐴, 𝐵⟩) ≤ 𝑥)
4542simp3d 1146 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝑥𝐵)
46 op2ndg 7774 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)
471, 2, 46syl2anc 587 . . . . . . . 8 (𝜑 → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)
4847adantr 484 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)
4945, 48breqtrrd 5081 . . . . . 6 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ (2nd ‘⟨𝐴, 𝐵⟩))
50 fveq2 6717 . . . . . . . . . . 11 (𝑛 = 1 → (𝐺𝑛) = (𝐺‘1))
51 iftrue 4445 . . . . . . . . . . . . 13 (𝑛 = 1 → if(𝑛 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩) = ⟨𝐴, 𝐵⟩)
52 opex 5348 . . . . . . . . . . . . 13 𝐴, 𝐵⟩ ∈ V
5351, 22, 52fvmpt 6818 . . . . . . . . . . . 12 (1 ∈ ℕ → (𝐺‘1) = ⟨𝐴, 𝐵⟩)
5435, 53ax-mp 5 . . . . . . . . . . 11 (𝐺‘1) = ⟨𝐴, 𝐵
5550, 54eqtrdi 2794 . . . . . . . . . 10 (𝑛 = 1 → (𝐺𝑛) = ⟨𝐴, 𝐵⟩)
5655fveq2d 6721 . . . . . . . . 9 (𝑛 = 1 → (1st ‘(𝐺𝑛)) = (1st ‘⟨𝐴, 𝐵⟩))
5756breq1d 5063 . . . . . . . 8 (𝑛 = 1 → ((1st ‘(𝐺𝑛)) ≤ 𝑥 ↔ (1st ‘⟨𝐴, 𝐵⟩) ≤ 𝑥))
5855fveq2d 6721 . . . . . . . . 9 (𝑛 = 1 → (2nd ‘(𝐺𝑛)) = (2nd ‘⟨𝐴, 𝐵⟩))
5958breq2d 5065 . . . . . . . 8 (𝑛 = 1 → (𝑥 ≤ (2nd ‘(𝐺𝑛)) ↔ 𝑥 ≤ (2nd ‘⟨𝐴, 𝐵⟩)))
6057, 59anbi12d 634 . . . . . . 7 (𝑛 = 1 → (((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛))) ↔ ((1st ‘⟨𝐴, 𝐵⟩) ≤ 𝑥𝑥 ≤ (2nd ‘⟨𝐴, 𝐵⟩))))
6160rspcev 3537 . . . . . 6 ((1 ∈ ℕ ∧ ((1st ‘⟨𝐴, 𝐵⟩) ≤ 𝑥𝑥 ≤ (2nd ‘⟨𝐴, 𝐵⟩))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛))))
6236, 44, 49, 61syl12anc 837 . . . . 5 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛))))
6362ralrimiva 3105 . . . 4 (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛))))
64 ovolficc 24365 . . . . 5 (((𝐴[,]𝐵) ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐴[,]𝐵) ⊆ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐴[,]𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
654, 23, 64syl2anc 587 . . . 4 (𝜑 → ((𝐴[,]𝐵) ⊆ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐴[,]𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) ≤ 𝑥𝑥 ≤ (2nd ‘(𝐺𝑛)))))
6663, 65mpbird 260 . . 3 (𝜑 → (𝐴[,]𝐵) ⊆ ran ([,] ∘ 𝐺))
6725ovollb2 24386 . . 3 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐴[,]𝐵) ⊆ ran ([,] ∘ 𝐺)) → (vol*‘(𝐴[,]𝐵)) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ))
6823, 66, 67syl2anc 587 . 2 (𝜑 → (vol*‘(𝐴[,]𝐵)) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ))
69 addid1 11012 . . . . . . . . 9 (𝑘 ∈ ℂ → (𝑘 + 0) = 𝑘)
7069adantl 485 . . . . . . . 8 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ℂ) → (𝑘 + 0) = 𝑘)
71 nnuz 12477 . . . . . . . . . 10 ℕ = (ℤ‘1)
7235, 71eleqtri 2836 . . . . . . . . 9 1 ∈ (ℤ‘1)
7372a1i 11 . . . . . . . 8 ((𝜑𝑥 ∈ ℕ) → 1 ∈ (ℤ‘1))
74 simpr 488 . . . . . . . . 9 ((𝜑𝑥 ∈ ℕ) → 𝑥 ∈ ℕ)
7574, 71eleqtrdi 2848 . . . . . . . 8 ((𝜑𝑥 ∈ ℕ) → 𝑥 ∈ (ℤ‘1))
76 rge0ssre 13044 . . . . . . . . . 10 (0[,)+∞) ⊆ ℝ
7727adantr 484 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℕ) → seq1( + , ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞))
78 ffvelrn 6902 . . . . . . . . . . 11 ((seq1( + , ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞) ∧ 1 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) ∈ (0[,)+∞))
7977, 35, 78sylancl 589 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) ∈ (0[,)+∞))
8076, 79sseldi 3899 . . . . . . . . 9 ((𝜑𝑥 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) ∈ ℝ)
8180recnd 10861 . . . . . . . 8 ((𝜑𝑥 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) ∈ ℂ)
8223ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
83 elfzuz 13108 . . . . . . . . . . . . 13 (𝑘 ∈ ((1 + 1)...𝑥) → 𝑘 ∈ (ℤ‘(1 + 1)))
8483adantl 485 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → 𝑘 ∈ (ℤ‘(1 + 1)))
85 df-2 11893 . . . . . . . . . . . . 13 2 = (1 + 1)
8685fveq2i 6720 . . . . . . . . . . . 12 (ℤ‘2) = (ℤ‘(1 + 1))
8784, 86eleqtrrdi 2849 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → 𝑘 ∈ (ℤ‘2))
88 eluz2nn 12480 . . . . . . . . . . 11 (𝑘 ∈ (ℤ‘2) → 𝑘 ∈ ℕ)
8987, 88syl 17 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → 𝑘 ∈ ℕ)
9024ovolfsval 24367 . . . . . . . . . 10 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑘) = ((2nd ‘(𝐺𝑘)) − (1st ‘(𝐺𝑘))))
9182, 89, 90syl2anc 587 . . . . . . . . 9 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (((abs ∘ − ) ∘ 𝐺)‘𝑘) = ((2nd ‘(𝐺𝑘)) − (1st ‘(𝐺𝑘))))
92 eqeq1 2741 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (𝑛 = 1 ↔ 𝑘 = 1))
9392ifbid 4462 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → if(𝑛 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩) = if(𝑘 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩))
94 opex 5348 . . . . . . . . . . . . . . . . 17 ⟨0, 0⟩ ∈ V
9552, 94ifex 4489 . . . . . . . . . . . . . . . 16 if(𝑘 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩) ∈ V
9693, 22, 95fvmpt 6818 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝐺𝑘) = if(𝑘 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩))
9789, 96syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (𝐺𝑘) = if(𝑘 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩))
98 eluz2b3 12518 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (ℤ‘2) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≠ 1))
9998simprbi 500 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ‘2) → 𝑘 ≠ 1)
10087, 99syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → 𝑘 ≠ 1)
101100neneqd 2945 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → ¬ 𝑘 = 1)
102101iffalsed 4450 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → if(𝑘 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩) = ⟨0, 0⟩)
10397, 102eqtrd 2777 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (𝐺𝑘) = ⟨0, 0⟩)
104103fveq2d 6721 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (2nd ‘(𝐺𝑘)) = (2nd ‘⟨0, 0⟩))
105 c0ex 10827 . . . . . . . . . . . . 13 0 ∈ V
106105, 105op2nd 7770 . . . . . . . . . . . 12 (2nd ‘⟨0, 0⟩) = 0
107104, 106eqtrdi 2794 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (2nd ‘(𝐺𝑘)) = 0)
108103fveq2d 6721 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (1st ‘(𝐺𝑘)) = (1st ‘⟨0, 0⟩))
109105, 105op1st 7769 . . . . . . . . . . . 12 (1st ‘⟨0, 0⟩) = 0
110108, 109eqtrdi 2794 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (1st ‘(𝐺𝑘)) = 0)
111107, 110oveq12d 7231 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → ((2nd ‘(𝐺𝑘)) − (1st ‘(𝐺𝑘))) = (0 − 0))
112 0m0e0 11950 . . . . . . . . . 10 (0 − 0) = 0
113111, 112eqtrdi 2794 . . . . . . . . 9 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → ((2nd ‘(𝐺𝑘)) − (1st ‘(𝐺𝑘))) = 0)
11491, 113eqtrd 2777 . . . . . . . 8 (((𝜑𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (((abs ∘ − ) ∘ 𝐺)‘𝑘) = 0)
11570, 73, 75, 81, 114seqid2 13622 . . . . . . 7 ((𝜑𝑥 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑥))
116 1z 12207 . . . . . . . 8 1 ∈ ℤ
11723adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
11824ovolfsval 24367 . . . . . . . . . 10 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
119117, 35, 118sylancl 589 . . . . . . . . 9 ((𝜑𝑥 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
12054fveq2i 6720 . . . . . . . . . . 11 (2nd ‘(𝐺‘1)) = (2nd ‘⟨𝐴, 𝐵⟩)
12147adantr 484 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℕ) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)
122120, 121syl5eq 2790 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℕ) → (2nd ‘(𝐺‘1)) = 𝐵)
12354fveq2i 6720 . . . . . . . . . . 11 (1st ‘(𝐺‘1)) = (1st ‘⟨𝐴, 𝐵⟩)
12438adantr 484 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℕ) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)
125123, 124syl5eq 2790 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℕ) → (1st ‘(𝐺‘1)) = 𝐴)
126122, 125oveq12d 7231 . . . . . . . . 9 ((𝜑𝑥 ∈ ℕ) → ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))) = (𝐵𝐴))
127119, 126eqtrd 2777 . . . . . . . 8 ((𝜑𝑥 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘1) = (𝐵𝐴))
128116, 127seq1i 13588 . . . . . . 7 ((𝜑𝑥 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) = (𝐵𝐴))
129115, 128eqtr3d 2779 . . . . . 6 ((𝜑𝑥 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑥) = (𝐵𝐴))
13033leidd 11398 . . . . . . 7 (𝜑 → (𝐵𝐴) ≤ (𝐵𝐴))
131130adantr 484 . . . . . 6 ((𝜑𝑥 ∈ ℕ) → (𝐵𝐴) ≤ (𝐵𝐴))
132129, 131eqbrtrd 5075 . . . . 5 ((𝜑𝑥 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑥) ≤ (𝐵𝐴))
133132ralrimiva 3105 . . . 4 (𝜑 → ∀𝑥 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑥) ≤ (𝐵𝐴))
13427ffnd 6546 . . . . 5 (𝜑 → seq1( + , ((abs ∘ − ) ∘ 𝐺)) Fn ℕ)
135 breq1 5056 . . . . . 6 (𝑧 = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑥) → (𝑧 ≤ (𝐵𝐴) ↔ (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑥) ≤ (𝐵𝐴)))
136135ralrn 6907 . . . . 5 (seq1( + , ((abs ∘ − ) ∘ 𝐺)) Fn ℕ → (∀𝑧 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑧 ≤ (𝐵𝐴) ↔ ∀𝑥 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑥) ≤ (𝐵𝐴)))
137134, 136syl 17 . . . 4 (𝜑 → (∀𝑧 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑧 ≤ (𝐵𝐴) ↔ ∀𝑥 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑥) ≤ (𝐵𝐴)))
138133, 137mpbird 260 . . 3 (𝜑 → ∀𝑧 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑧 ≤ (𝐵𝐴))
139 supxrleub 12916 . . . 4 ((ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* ∧ (𝐵𝐴) ∈ ℝ*) → (sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤ (𝐵𝐴) ↔ ∀𝑧 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑧 ≤ (𝐵𝐴)))
14030, 34, 139syl2anc 587 . . 3 (𝜑 → (sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤ (𝐵𝐴) ↔ ∀𝑧 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑧 ≤ (𝐵𝐴)))
141138, 140mpbird 260 . 2 (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤ (𝐵𝐴))
1426, 32, 34, 68, 141xrletrd 12752 1 (𝜑 → (vol*‘(𝐴[,]𝐵)) ≤ (𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wcel 2110  wne 2940  wral 3061  wrex 3062  cin 3865  wss 3866  ifcif 4439  cop 4547   cuni 4819   class class class wbr 5053  cmpt 5135   × cxp 5549  ran crn 5552  ccom 5555   Fn wfn 6375  wf 6376  cfv 6380  (class class class)co 7213  1st c1st 7759  2nd c2nd 7760  supcsup 9056  cc 10727  cr 10728  0cc0 10729  1c1 10730   + caddc 10732  +∞cpnf 10864  *cxr 10866   < clt 10867  cle 10868  cmin 11062  cn 11830  2c2 11885  cuz 12438  [,)cico 12937  [,]cicc 12938  ...cfz 13095  seqcseq 13574  abscabs 14797  vol*covol 24359
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-er 8391  df-map 8510  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-sup 9058  df-inf 9059  df-oi 9126  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-n0 12091  df-z 12177  df-uz 12439  df-q 12545  df-rp 12587  df-ioo 12939  df-ico 12941  df-icc 12942  df-fz 13096  df-fzo 13239  df-seq 13575  df-exp 13636  df-hash 13897  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-clim 15049  df-sum 15250  df-ovol 24361
This theorem is referenced by:  ovolicc  24420
  Copyright terms: Public domain W3C validator