Step | Hyp | Ref
| Expression |
1 | | ovolicc.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | ovolicc.2 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | iccssre 12255 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
4 | 1, 2, 3 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
5 | | ovolcl 23246 |
. . 3
⊢ ((𝐴[,]𝐵) ⊆ ℝ → (vol*‘(𝐴[,]𝐵)) ∈
ℝ*) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝜑 → (vol*‘(𝐴[,]𝐵)) ∈
ℝ*) |
7 | | ovolicc.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
8 | | df-br 4654 |
. . . . . . . . . . 11
⊢ (𝐴 ≤ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≤ ) |
9 | 7, 8 | sylib 208 |
. . . . . . . . . 10
⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ ≤ ) |
10 | | opelxpi 5148 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
〈𝐴, 𝐵〉 ∈ (ℝ ×
ℝ)) |
11 | 1, 2, 10 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ (ℝ ×
ℝ)) |
12 | 9, 11 | elind 3798 |
. . . . . . . . 9
⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
13 | 12 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈𝐴, 𝐵〉 ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
14 | | 0le0 11110 |
. . . . . . . . . 10
⊢ 0 ≤
0 |
15 | | df-br 4654 |
. . . . . . . . . 10
⊢ (0 ≤ 0
↔ 〈0, 0〉 ∈ ≤ ) |
16 | 14, 15 | mpbi 220 |
. . . . . . . . 9
⊢ 〈0,
0〉 ∈ ≤ |
17 | | 0re 10040 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
18 | | opelxpi 5148 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 0 ∈ ℝ) → 〈0, 0〉 ∈ (ℝ
× ℝ)) |
19 | 17, 17, 18 | mp2an 708 |
. . . . . . . . 9
⊢ 〈0,
0〉 ∈ (ℝ × ℝ) |
20 | | elin 3796 |
. . . . . . . . 9
⊢ (〈0,
0〉 ∈ ( ≤ ∩ (ℝ × ℝ)) ↔ (〈0, 0〉
∈ ≤ ∧ 〈0, 0〉 ∈ (ℝ ×
ℝ))) |
21 | 16, 19, 20 | mpbir2an 955 |
. . . . . . . 8
⊢ 〈0,
0〉 ∈ ( ≤ ∩ (ℝ × ℝ)) |
22 | | ifcl 4130 |
. . . . . . . 8
⊢
((〈𝐴, 𝐵〉 ∈ ( ≤ ∩
(ℝ × ℝ)) ∧ 〈0, 0〉 ∈ ( ≤ ∩ (ℝ
× ℝ))) → if(𝑛 = 1, 〈𝐴, 𝐵〉, 〈0, 0〉) ∈ ( ≤
∩ (ℝ × ℝ))) |
23 | 13, 21, 22 | sylancl 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑛 = 1, 〈𝐴, 𝐵〉, 〈0, 0〉) ∈ ( ≤
∩ (ℝ × ℝ))) |
24 | | ovolicc1.4 |
. . . . . . 7
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, 〈𝐴, 𝐵〉, 〈0, 0〉)) |
25 | 23, 24 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
26 | | eqid 2622 |
. . . . . . 7
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) |
27 | | eqid 2622 |
. . . . . . 7
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝐺)) = seq1( + , ((abs ∘ − )
∘ 𝐺)) |
28 | 26, 27 | ovolsf 23241 |
. . . . . 6
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘
𝐺)):ℕ⟶(0[,)+∞)) |
29 | 25, 28 | syl 17 |
. . . . 5
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐺)):ℕ⟶(0[,)+∞)) |
30 | | frn 6053 |
. . . . 5
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞) → ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ (0[,)+∞)) |
31 | 29, 30 | syl 17 |
. . . 4
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ 𝐺)) ⊆ (0[,)+∞)) |
32 | | icossxr 12258 |
. . . 4
⊢
(0[,)+∞) ⊆ ℝ* |
33 | 31, 32 | syl6ss 3615 |
. . 3
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ 𝐺)) ⊆
ℝ*) |
34 | | supxrcl 12145 |
. . 3
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* →
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈
ℝ*) |
35 | 33, 34 | syl 17 |
. 2
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ∈
ℝ*) |
36 | 2, 1 | resubcld 10458 |
. . 3
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
37 | 36 | rexrd 10089 |
. 2
⊢ (𝜑 → (𝐵 − 𝐴) ∈
ℝ*) |
38 | | 1nn 11031 |
. . . . . . 7
⊢ 1 ∈
ℕ |
39 | 38 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 1 ∈ ℕ) |
40 | | op1stg 7180 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(1st ‘〈𝐴, 𝐵〉) = 𝐴) |
41 | 1, 2, 40 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘〈𝐴, 𝐵〉) = 𝐴) |
42 | 41 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) |
43 | | elicc2 12238 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
44 | 1, 2, 43 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
45 | 44 | biimpa 501 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
46 | 45 | simp2d 1074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥) |
47 | 42, 46 | eqbrtrd 4675 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (1st ‘〈𝐴, 𝐵〉) ≤ 𝑥) |
48 | 45 | simp3d 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵) |
49 | | op2ndg 7181 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(2nd ‘〈𝐴, 𝐵〉) = 𝐵) |
50 | 1, 2, 49 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘〈𝐴, 𝐵〉) = 𝐵) |
51 | 50 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) |
52 | 48, 51 | breqtrrd 4681 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ (2nd ‘〈𝐴, 𝐵〉)) |
53 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → (𝐺‘𝑛) = (𝐺‘1)) |
54 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → if(𝑛 = 1, 〈𝐴, 𝐵〉, 〈0, 0〉) = 〈𝐴, 𝐵〉) |
55 | | opex 4932 |
. . . . . . . . . . . . 13
⊢
〈𝐴, 𝐵〉 ∈ V |
56 | 54, 24, 55 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℕ → (𝐺‘1)
= 〈𝐴, 𝐵〉) |
57 | 38, 56 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐺‘1) = 〈𝐴, 𝐵〉 |
58 | 53, 57 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → (𝐺‘𝑛) = 〈𝐴, 𝐵〉) |
59 | 58 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑛 = 1 → (1st
‘(𝐺‘𝑛)) = (1st
‘〈𝐴, 𝐵〉)) |
60 | 59 | breq1d 4663 |
. . . . . . . 8
⊢ (𝑛 = 1 → ((1st
‘(𝐺‘𝑛)) ≤ 𝑥 ↔ (1st ‘〈𝐴, 𝐵〉) ≤ 𝑥)) |
61 | 58 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑛 = 1 → (2nd
‘(𝐺‘𝑛)) = (2nd
‘〈𝐴, 𝐵〉)) |
62 | 61 | breq2d 4665 |
. . . . . . . 8
⊢ (𝑛 = 1 → (𝑥 ≤ (2nd ‘(𝐺‘𝑛)) ↔ 𝑥 ≤ (2nd ‘〈𝐴, 𝐵〉))) |
63 | 60, 62 | anbi12d 747 |
. . . . . . 7
⊢ (𝑛 = 1 → (((1st
‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛))) ↔ ((1st
‘〈𝐴, 𝐵〉) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘〈𝐴, 𝐵〉)))) |
64 | 63 | rspcev 3309 |
. . . . . 6
⊢ ((1
∈ ℕ ∧ ((1st ‘〈𝐴, 𝐵〉) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘〈𝐴, 𝐵〉))) → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))) |
65 | 39, 47, 52, 64 | syl12anc 1324 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))) |
66 | 65 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))) |
67 | | ovolficc 23237 |
. . . . 5
⊢ (((𝐴[,]𝐵) ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) → ((𝐴[,]𝐵) ⊆ ∪ ran
([,] ∘ 𝐺) ↔
∀𝑥 ∈ (𝐴[,]𝐵)∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛))))) |
68 | 4, 25, 67 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((𝐴[,]𝐵) ⊆ ∪ ran
([,] ∘ 𝐺) ↔
∀𝑥 ∈ (𝐴[,]𝐵)∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛))))) |
69 | 66, 68 | mpbird 247 |
. . 3
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ ran
([,] ∘ 𝐺)) |
70 | 27 | ovollb2 23257 |
. . 3
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝐴[,]𝐵) ⊆ ∪ ran
([,] ∘ 𝐺)) →
(vol*‘(𝐴[,]𝐵)) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, <
)) |
71 | 25, 69, 70 | syl2anc 693 |
. 2
⊢ (𝜑 → (vol*‘(𝐴[,]𝐵)) ≤ sup(ran seq1( + , ((abs ∘
− ) ∘ 𝐺)),
ℝ*, < )) |
72 | | addid1 10216 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℂ → (𝑘 + 0) = 𝑘) |
73 | 72 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ℂ) → (𝑘 + 0) = 𝑘) |
74 | | nnuz 11723 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
75 | 38, 74 | eleqtri 2699 |
. . . . . . . . 9
⊢ 1 ∈
(ℤ≥‘1) |
76 | 75 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 1 ∈
(ℤ≥‘1)) |
77 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℕ) |
78 | 77, 74 | syl6eleq 2711 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈
(ℤ≥‘1)) |
79 | | rge0ssre 12280 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
80 | 29 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → seq1( + , ((abs
∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞)) |
81 | | ffvelrn 6357 |
. . . . . . . . . . 11
⊢ ((seq1( +
, ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞) ∧ 1
∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) ∈
(0[,)+∞)) |
82 | 80, 38, 81 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘1) ∈
(0[,)+∞)) |
83 | 79, 82 | sseldi 3601 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘1) ∈ ℝ) |
84 | 83 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘1) ∈ ℂ) |
85 | 25 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
86 | | elfzuz 12338 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((1 + 1)...𝑥) → 𝑘 ∈ (ℤ≥‘(1 +
1))) |
87 | 86 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → 𝑘 ∈ (ℤ≥‘(1 +
1))) |
88 | | df-2 11079 |
. . . . . . . . . . . . 13
⊢ 2 = (1 +
1) |
89 | 88 | fveq2i 6194 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘2) = (ℤ≥‘(1 +
1)) |
90 | 87, 89 | syl6eleqr 2712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → 𝑘 ∈
(ℤ≥‘2)) |
91 | | eluz2nn 11726 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(ℤ≥‘2) → 𝑘 ∈ ℕ) |
92 | 90, 91 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → 𝑘 ∈ ℕ) |
93 | 26 | ovolfsval 23239 |
. . . . . . . . . 10
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑘) = ((2nd ‘(𝐺‘𝑘)) − (1st ‘(𝐺‘𝑘)))) |
94 | 85, 92, 93 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (((abs ∘ − ) ∘
𝐺)‘𝑘) = ((2nd ‘(𝐺‘𝑘)) − (1st ‘(𝐺‘𝑘)))) |
95 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (𝑛 = 1 ↔ 𝑘 = 1)) |
96 | 95 | ifbid 4108 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → if(𝑛 = 1, 〈𝐴, 𝐵〉, 〈0, 0〉) = if(𝑘 = 1, 〈𝐴, 𝐵〉, 〈0, 0〉)) |
97 | | opex 4932 |
. . . . . . . . . . . . . . . . 17
⊢ 〈0,
0〉 ∈ V |
98 | 55, 97 | ifex 4156 |
. . . . . . . . . . . . . . . 16
⊢ if(𝑘 = 1, 〈𝐴, 𝐵〉, 〈0, 0〉) ∈
V |
99 | 96, 24, 98 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = if(𝑘 = 1, 〈𝐴, 𝐵〉, 〈0, 0〉)) |
100 | 92, 99 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (𝐺‘𝑘) = if(𝑘 = 1, 〈𝐴, 𝐵〉, 〈0, 0〉)) |
101 | | eluz2b3 11762 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈
(ℤ≥‘2) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≠ 1)) |
102 | 101 | simprbi 480 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘2) → 𝑘 ≠ 1) |
103 | 90, 102 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → 𝑘 ≠ 1) |
104 | 103 | neneqd 2799 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → ¬ 𝑘 = 1) |
105 | 104 | iffalsed 4097 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → if(𝑘 = 1, 〈𝐴, 𝐵〉, 〈0, 0〉) = 〈0,
0〉) |
106 | 100, 105 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (𝐺‘𝑘) = 〈0, 0〉) |
107 | 106 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (2nd ‘(𝐺‘𝑘)) = (2nd ‘〈0,
0〉)) |
108 | | c0ex 10034 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
109 | 108, 108 | op2nd 7177 |
. . . . . . . . . . . 12
⊢
(2nd ‘〈0, 0〉) = 0 |
110 | 107, 109 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (2nd ‘(𝐺‘𝑘)) = 0) |
111 | 106 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (1st ‘(𝐺‘𝑘)) = (1st ‘〈0,
0〉)) |
112 | 108, 108 | op1st 7176 |
. . . . . . . . . . . 12
⊢
(1st ‘〈0, 0〉) = 0 |
113 | 111, 112 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (1st ‘(𝐺‘𝑘)) = 0) |
114 | 110, 113 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → ((2nd ‘(𝐺‘𝑘)) − (1st ‘(𝐺‘𝑘))) = (0 − 0)) |
115 | | 0m0e0 11130 |
. . . . . . . . . 10
⊢ (0
− 0) = 0 |
116 | 114, 115 | syl6eq 2672 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → ((2nd ‘(𝐺‘𝑘)) − (1st ‘(𝐺‘𝑘))) = 0) |
117 | 94, 116 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 ∈ ((1 + 1)...𝑥)) → (((abs ∘ − ) ∘
𝐺)‘𝑘) = 0) |
118 | 73, 76, 78, 84, 117 | seqid2 12847 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘1) = (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑥)) |
119 | | 1z 11407 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
120 | 25 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
121 | 26 | ovolfsval 23239 |
. . . . . . . . . 10
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1)))) |
122 | 120, 38, 121 | sylancl 694 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1)))) |
123 | 57 | fveq2i 6194 |
. . . . . . . . . . 11
⊢
(2nd ‘(𝐺‘1)) = (2nd
‘〈𝐴, 𝐵〉) |
124 | 50 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (2nd
‘〈𝐴, 𝐵〉) = 𝐵) |
125 | 123, 124 | syl5eq 2668 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (2nd
‘(𝐺‘1)) = 𝐵) |
126 | 57 | fveq2i 6194 |
. . . . . . . . . . 11
⊢
(1st ‘(𝐺‘1)) = (1st
‘〈𝐴, 𝐵〉) |
127 | 41 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1st
‘〈𝐴, 𝐵〉) = 𝐴) |
128 | 126, 127 | syl5eq 2668 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1st
‘(𝐺‘1)) = 𝐴) |
129 | 125, 128 | oveq12d 6668 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((2nd
‘(𝐺‘1)) −
(1st ‘(𝐺‘1))) = (𝐵 − 𝐴)) |
130 | 122, 129 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘1) = (𝐵 − 𝐴)) |
131 | 119, 130 | seq1i 12815 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘1) = (𝐵 − 𝐴)) |
132 | 118, 131 | eqtr3d 2658 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘𝑥) = (𝐵 − 𝐴)) |
133 | 36 | leidd 10594 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ≤ (𝐵 − 𝐴)) |
134 | 133 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐵 − 𝐴) ≤ (𝐵 − 𝐴)) |
135 | 132, 134 | eqbrtrd 4675 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘𝑥) ≤ (𝐵 − 𝐴)) |
136 | 135 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑥) ≤ (𝐵 − 𝐴)) |
137 | | ffn 6045 |
. . . . . 6
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞) →
seq1( + , ((abs ∘ − ) ∘ 𝐺)) Fn ℕ) |
138 | 29, 137 | syl 17 |
. . . . 5
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐺)) Fn
ℕ) |
139 | | breq1 4656 |
. . . . . 6
⊢ (𝑧 = (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑥) → (𝑧 ≤ (𝐵 − 𝐴) ↔ (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑥) ≤ (𝐵 − 𝐴))) |
140 | 139 | ralrn 6362 |
. . . . 5
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝐺)) Fn ℕ → (∀𝑧 ∈ ran seq1( + , ((abs
∘ − ) ∘ 𝐺))𝑧 ≤ (𝐵 − 𝐴) ↔ ∀𝑥 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑥) ≤ (𝐵 − 𝐴))) |
141 | 138, 140 | syl 17 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ran seq1( + , ((abs
∘ − ) ∘ 𝐺))𝑧 ≤ (𝐵 − 𝐴) ↔ ∀𝑥 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑥) ≤ (𝐵 − 𝐴))) |
142 | 136, 141 | mpbird 247 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ ran seq1( + , ((abs ∘ − )
∘ 𝐺))𝑧 ≤ (𝐵 − 𝐴)) |
143 | | supxrleub 12156 |
. . . 4
⊢ ((ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* ∧ (𝐵 − 𝐴) ∈ ℝ*) →
(sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤ (𝐵 − 𝐴) ↔ ∀𝑧 ∈ ran seq1( + , ((abs ∘ − )
∘ 𝐺))𝑧 ≤ (𝐵 − 𝐴))) |
144 | 33, 37, 143 | syl2anc 693 |
. . 3
⊢ (𝜑 → (sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ≤ (𝐵 − 𝐴) ↔ ∀𝑧 ∈ ran seq1( + , ((abs ∘ − )
∘ 𝐺))𝑧 ≤ (𝐵 − 𝐴))) |
145 | 142, 144 | mpbird 247 |
. 2
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ≤ (𝐵 − 𝐴)) |
146 | 6, 35, 37, 71, 145 | xrletrd 11993 |
1
⊢ (𝜑 → (vol*‘(𝐴[,]𝐵)) ≤ (𝐵 − 𝐴)) |