Proof of Theorem ovolval2lem
Step | Hyp | Ref
| Expression |
1 | | reex 10820 |
. . . . . . 7
⊢ ℝ
∈ V |
2 | 1, 1 | xpex 7538 |
. . . . . 6
⊢ (ℝ
× ℝ) ∈ V |
3 | | inss2 4144 |
. . . . . 6
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
4 | | mapss 8570 |
. . . . . 6
⊢
(((ℝ × ℝ) ∈ V ∧ ( ≤ ∩ (ℝ ×
ℝ)) ⊆ (ℝ × ℝ)) → (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ⊆ ((ℝ ×
ℝ) ↑m ℕ)) |
5 | 2, 3, 4 | mp2an 692 |
. . . . 5
⊢ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ) ⊆ ((ℝ
× ℝ) ↑m ℕ) |
6 | | ovolval2lem.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
7 | 2 | inex2 5211 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ( ≤ ∩ (ℝ
× ℝ)) ∈ V) |
9 | | nnex 11836 |
. . . . . . . 8
⊢ ℕ
∈ V |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℕ ∈
V) |
11 | 8, 10 | elmapd 8522 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ)))) |
12 | 6, 11 | mpbird 260 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) |
13 | 5, 12 | sseldi 3899 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((ℝ × ℝ)
↑m ℕ)) |
14 | | 1zzd 12208 |
. . . . 5
⊢ (𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 1 ∈ ℤ) |
15 | | nnuz 12477 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
16 | | elmapi 8530 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
17 | 16 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
18 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
19 | 17, 18 | fvovco 42405 |
. . . . . . . 8
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑘) = ((1st ‘(𝐹‘𝑘))[,)(2nd ‘(𝐹‘𝑘)))) |
20 | 19 | fveq2d 6721 |
. . . . . . 7
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (vol‘(([,)
∘ 𝐹)‘𝑘)) = (vol‘((1st
‘(𝐹‘𝑘))[,)(2nd
‘(𝐹‘𝑘))))) |
21 | 16 | ffvelrnda 6904 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (ℝ ×
ℝ)) |
22 | | xp1st 7793 |
. . . . . . . . 9
⊢ ((𝐹‘𝑘) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘𝑘)) ∈ ℝ) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐹‘𝑘)) ∈
ℝ) |
24 | | xp2nd 7794 |
. . . . . . . . 9
⊢ ((𝐹‘𝑘) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘𝑘)) ∈ ℝ) |
25 | 21, 24 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐹‘𝑘)) ∈
ℝ) |
26 | | volicore 43794 |
. . . . . . . 8
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ) →
(vol‘((1st ‘(𝐹‘𝑘))[,)(2nd ‘(𝐹‘𝑘)))) ∈ ℝ) |
27 | 23, 25, 26 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) →
(vol‘((1st ‘(𝐹‘𝑘))[,)(2nd ‘(𝐹‘𝑘)))) ∈ ℝ) |
28 | 20, 27 | eqeltrd 2838 |
. . . . . 6
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (vol‘(([,)
∘ 𝐹)‘𝑘)) ∈
ℝ) |
29 | 28 | recnd 10861 |
. . . . 5
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (vol‘(([,)
∘ 𝐹)‘𝑘)) ∈
ℂ) |
30 | | eqid 2737 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘))) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘))) |
31 | | eqid 2737 |
. . . . 5
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘(([,) ∘ 𝐹)‘𝑘)))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘(([,)
∘ 𝐹)‘𝑘)))) |
32 | 14, 15, 29, 30, 31 | fsumsermpt 42795 |
. . . 4
⊢ (𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘(([,)
∘ 𝐹)‘𝑘))))) |
33 | 13, 32 | syl 17 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘(([,)
∘ 𝐹)‘𝑘))))) |
34 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) |
35 | 34 | iftrued 4447 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → if((1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘)), ((2nd
‘(𝐹‘𝑘)) − (1st
‘(𝐹‘𝑘))), 0) = ((2nd
‘(𝐹‘𝑘)) − (1st
‘(𝐹‘𝑘)))) |
36 | 13, 23 | sylan 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐹‘𝑘)) ∈
ℝ) |
37 | 36 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (1st
‘(𝐹‘𝑘)) ∈
ℝ) |
38 | 13, 25 | sylan 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐹‘𝑘)) ∈
ℝ) |
39 | 38 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (2nd
‘(𝐹‘𝑘)) ∈
ℝ) |
40 | | ressxr 10877 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℝ* |
41 | 40, 37 | sseldi 3899 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (1st
‘(𝐹‘𝑘)) ∈
ℝ*) |
42 | 40, 39 | sseldi 3899 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (2nd
‘(𝐹‘𝑘)) ∈
ℝ*) |
43 | | xpss 5567 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℝ
× ℝ) ⊆ (V × V) |
44 | 43, 21 | sseldi 3899 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (V × V)) |
45 | | 1st2ndb 7801 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑘) ∈ (V × V) ↔ (𝐹‘𝑘) = 〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) |
46 | 44, 45 | sylib 221 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) |
47 | 13, 46 | sylan 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) |
48 | 47 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 〈(1st
‘(𝐹‘𝑘)), (2nd
‘(𝐹‘𝑘))〉 = (𝐹‘𝑘)) |
49 | | inss1 4143 |
. . . . . . . . . . . . . . . . 17
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ ≤ |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ( ≤ ∩ (ℝ
× ℝ)) ⊆ ≤ ) |
51 | 6, 50 | fssd 6563 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:ℕ⟶ ≤ ) |
52 | 51 | ffvelrnda 6904 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ≤ ) |
53 | 48, 52 | eqeltrd 2838 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 〈(1st
‘(𝐹‘𝑘)), (2nd
‘(𝐹‘𝑘))〉 ∈ ≤
) |
54 | | df-br 5054 |
. . . . . . . . . . . . 13
⊢
((1st ‘(𝐹‘𝑘)) ≤ (2nd ‘(𝐹‘𝑘)) ↔ 〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉 ∈ ≤ ) |
55 | 53, 54 | sylibr 237 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐹‘𝑘)) ≤ (2nd
‘(𝐹‘𝑘))) |
56 | 55 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (1st
‘(𝐹‘𝑘)) ≤ (2nd
‘(𝐹‘𝑘))) |
57 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) |
58 | 39, 37 | lenltd 10978 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → ((2nd
‘(𝐹‘𝑘)) ≤ (1st
‘(𝐹‘𝑘)) ↔ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘)))) |
59 | 57, 58 | mpbird 260 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (2nd
‘(𝐹‘𝑘)) ≤ (1st
‘(𝐹‘𝑘))) |
60 | 41, 42, 56, 59 | xrletrid 12745 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (1st
‘(𝐹‘𝑘)) = (2nd
‘(𝐹‘𝑘))) |
61 | | simp3 1140 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → (1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) |
62 | | simp1 1138 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → (1st ‘(𝐹‘𝑘)) ∈ ℝ) |
63 | | simp2 1139 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → (2nd ‘(𝐹‘𝑘)) ∈ ℝ) |
64 | 62, 63 | eqleltd 10976 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → ((1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘)) ↔ ((1st ‘(𝐹‘𝑘)) ≤ (2nd ‘(𝐹‘𝑘)) ∧ ¬ (1st ‘(𝐹‘𝑘)) < (2nd ‘(𝐹‘𝑘))))) |
65 | 61, 64 | mpbid 235 |
. . . . . . . . . . . . 13
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → ((1st ‘(𝐹‘𝑘)) ≤ (2nd ‘(𝐹‘𝑘)) ∧ ¬ (1st ‘(𝐹‘𝑘)) < (2nd ‘(𝐹‘𝑘)))) |
66 | 65 | simprd 499 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) |
67 | 66 | iffalsed 4450 |
. . . . . . . . . . 11
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → if((1st ‘(𝐹‘𝑘)) < (2nd ‘(𝐹‘𝑘)), ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘))), 0) = 0) |
68 | 63 | recnd 10861 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → (2nd ‘(𝐹‘𝑘)) ∈ ℂ) |
69 | 61 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → (2nd ‘(𝐹‘𝑘)) = (1st ‘(𝐹‘𝑘))) |
70 | 68, 69 | subeq0bd 11258 |
. . . . . . . . . . 11
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘))) = 0) |
71 | 67, 70 | eqtr4d 2780 |
. . . . . . . . . 10
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → if((1st ‘(𝐹‘𝑘)) < (2nd ‘(𝐹‘𝑘)), ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘))), 0) = ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘)))) |
72 | 37, 39, 60, 71 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → if((1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘)), ((2nd
‘(𝐹‘𝑘)) − (1st
‘(𝐹‘𝑘))), 0) = ((2nd
‘(𝐹‘𝑘)) − (1st
‘(𝐹‘𝑘)))) |
73 | 35, 72 | pm2.61dan 813 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if((1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘)), ((2nd
‘(𝐹‘𝑘)) − (1st
‘(𝐹‘𝑘))), 0) = ((2nd
‘(𝐹‘𝑘)) − (1st
‘(𝐹‘𝑘)))) |
74 | | volico 43199 |
. . . . . . . . 9
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ) →
(vol‘((1st ‘(𝐹‘𝑘))[,)(2nd ‘(𝐹‘𝑘)))) = if((1st ‘(𝐹‘𝑘)) < (2nd ‘(𝐹‘𝑘)), ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘))), 0)) |
75 | 36, 38, 74 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(vol‘((1st ‘(𝐹‘𝑘))[,)(2nd ‘(𝐹‘𝑘)))) = if((1st ‘(𝐹‘𝑘)) < (2nd ‘(𝐹‘𝑘)), ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘))), 0)) |
76 | 36, 38, 55 | abssuble0d 14996 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(abs‘((1st ‘(𝐹‘𝑘)) − (2nd ‘(𝐹‘𝑘)))) = ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘)))) |
77 | 73, 75, 76 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(vol‘((1st ‘(𝐹‘𝑘))[,)(2nd ‘(𝐹‘𝑘)))) = (abs‘((1st
‘(𝐹‘𝑘)) − (2nd
‘(𝐹‘𝑘))))) |
78 | 13 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹 ∈ ((ℝ × ℝ)
↑m ℕ)) |
79 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
80 | 78, 79, 20 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol‘(([,)
∘ 𝐹)‘𝑘)) = (vol‘((1st
‘(𝐹‘𝑘))[,)(2nd
‘(𝐹‘𝑘))))) |
81 | 46 | fveq2d 6721 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → ((abs ∘ −
)‘(𝐹‘𝑘)) = ((abs ∘ −
)‘〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉)) |
82 | | df-ov 7216 |
. . . . . . . . . . 11
⊢
((1st ‘(𝐹‘𝑘))(abs ∘ − )(2nd
‘(𝐹‘𝑘))) = ((abs ∘ −
)‘〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) |
83 | 82 | eqcomi 2746 |
. . . . . . . . . 10
⊢ ((abs
∘ − )‘〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) = ((1st ‘(𝐹‘𝑘))(abs ∘ − )(2nd
‘(𝐹‘𝑘))) |
84 | 83 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → ((abs ∘ −
)‘〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) = ((1st ‘(𝐹‘𝑘))(abs ∘ − )(2nd
‘(𝐹‘𝑘)))) |
85 | 23 | recnd 10861 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐹‘𝑘)) ∈
ℂ) |
86 | 25 | recnd 10861 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐹‘𝑘)) ∈
ℂ) |
87 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) = (abs ∘ − ) |
88 | 87 | cnmetdval 23668 |
. . . . . . . . . 10
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℂ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℂ) →
((1st ‘(𝐹‘𝑘))(abs ∘ − )(2nd
‘(𝐹‘𝑘))) =
(abs‘((1st ‘(𝐹‘𝑘)) − (2nd ‘(𝐹‘𝑘))))) |
89 | 85, 86, 88 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → ((1st
‘(𝐹‘𝑘))(abs ∘ −
)(2nd ‘(𝐹‘𝑘))) = (abs‘((1st
‘(𝐹‘𝑘)) − (2nd
‘(𝐹‘𝑘))))) |
90 | 81, 84, 89 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → ((abs ∘ −
)‘(𝐹‘𝑘)) = (abs‘((1st
‘(𝐹‘𝑘)) − (2nd
‘(𝐹‘𝑘))))) |
91 | 78, 79, 90 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs ∘ −
)‘(𝐹‘𝑘)) = (abs‘((1st
‘(𝐹‘𝑘)) − (2nd
‘(𝐹‘𝑘))))) |
92 | 77, 80, 91 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol‘(([,)
∘ 𝐹)‘𝑘)) = ((abs ∘ −
)‘(𝐹‘𝑘))) |
93 | 92 | mpteq2dva 5150 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ (vol‘(([,)
∘ 𝐹)‘𝑘))) = (𝑘 ∈ ℕ ↦ ((abs ∘ −
)‘(𝐹‘𝑘)))) |
94 | 13, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
95 | | rr2sscn2 42578 |
. . . . . . 7
⊢ (ℝ
× ℝ) ⊆ (ℂ × ℂ) |
96 | 95 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (ℝ × ℝ)
⊆ (ℂ × ℂ)) |
97 | | absf 14901 |
. . . . . . . 8
⊢
abs:ℂ⟶ℝ |
98 | | subf 11080 |
. . . . . . . 8
⊢ −
:(ℂ × ℂ)⟶ℂ |
99 | | fco 6569 |
. . . . . . . 8
⊢
((abs:ℂ⟶ℝ ∧ − :(ℂ ×
ℂ)⟶ℂ) → (abs ∘ − ):(ℂ ×
ℂ)⟶ℝ) |
100 | 97, 98, 99 | mp2an 692 |
. . . . . . 7
⊢ (abs
∘ − ):(ℂ × ℂ)⟶ℝ |
101 | 100 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (abs ∘ −
):(ℂ × ℂ)⟶ℝ) |
102 | 94, 96, 101 | fcomptss 42416 |
. . . . 5
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐹) = (𝑘 ∈ ℕ ↦ ((abs
∘ − )‘(𝐹‘𝑘)))) |
103 | 93, 102 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ (vol‘(([,)
∘ 𝐹)‘𝑘))) = ((abs ∘ − )
∘ 𝐹)) |
104 | 103 | seqeq3d 13582 |
. . 3
⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦
(vol‘(([,) ∘ 𝐹)‘𝑘)))) = seq1( + , ((abs ∘ − )
∘ 𝐹))) |
105 | 33, 104 | eqtr2d 2778 |
. 2
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐹)) =
(𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘)))) |
106 | 105 | rneqd 5807 |
1
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ 𝐹)) = ran (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘)))) |