Proof of Theorem ovolval2lem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | reex 11247 | . . . . . . 7
⊢ ℝ
∈ V | 
| 2 | 1, 1 | xpex 7774 | . . . . . 6
⊢ (ℝ
× ℝ) ∈ V | 
| 3 |  | inss2 4237 | . . . . . 6
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) | 
| 4 |  | mapss 8930 | . . . . . 6
⊢
(((ℝ × ℝ) ∈ V ∧ ( ≤ ∩ (ℝ ×
ℝ)) ⊆ (ℝ × ℝ)) → (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ⊆ ((ℝ ×
ℝ) ↑m ℕ)) | 
| 5 | 2, 3, 4 | mp2an 692 | . . . . 5
⊢ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ) ⊆ ((ℝ
× ℝ) ↑m ℕ) | 
| 6 |  | ovolval2lem.1 | . . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 7 | 2 | inex2 5317 | . . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V | 
| 8 | 7 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ( ≤ ∩ (ℝ
× ℝ)) ∈ V) | 
| 9 |  | nnex 12273 | . . . . . . . 8
⊢ ℕ
∈ V | 
| 10 | 9 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ℕ ∈
V) | 
| 11 | 8, 10 | elmapd 8881 | . . . . . 6
⊢ (𝜑 → (𝐹 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ)))) | 
| 12 | 6, 11 | mpbird 257 | . . . . 5
⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) | 
| 13 | 5, 12 | sselid 3980 | . . . 4
⊢ (𝜑 → 𝐹 ∈ ((ℝ × ℝ)
↑m ℕ)) | 
| 14 |  | 1zzd 12650 | . . . . 5
⊢ (𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 1 ∈ ℤ) | 
| 15 |  | nnuz 12922 | . . . . 5
⊢ ℕ =
(ℤ≥‘1) | 
| 16 |  | elmapi 8890 | . . . . . . . . . 10
⊢ (𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝐹:ℕ⟶(ℝ ×
ℝ)) | 
| 17 | 16 | adantr 480 | . . . . . . . . 9
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(ℝ ×
ℝ)) | 
| 18 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) | 
| 19 | 17, 18 | fvovco 45203 | . . . . . . . 8
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑘) = ((1st ‘(𝐹‘𝑘))[,)(2nd ‘(𝐹‘𝑘)))) | 
| 20 | 19 | fveq2d 6909 | . . . . . . 7
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (vol‘(([,)
∘ 𝐹)‘𝑘)) = (vol‘((1st
‘(𝐹‘𝑘))[,)(2nd
‘(𝐹‘𝑘))))) | 
| 21 | 16 | ffvelcdmda 7103 | . . . . . . . . 9
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (ℝ ×
ℝ)) | 
| 22 |  | xp1st 8047 | . . . . . . . . 9
⊢ ((𝐹‘𝑘) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘𝑘)) ∈ ℝ) | 
| 23 | 21, 22 | syl 17 | . . . . . . . 8
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐹‘𝑘)) ∈
ℝ) | 
| 24 |  | xp2nd 8048 | . . . . . . . . 9
⊢ ((𝐹‘𝑘) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘𝑘)) ∈ ℝ) | 
| 25 | 21, 24 | syl 17 | . . . . . . . 8
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐹‘𝑘)) ∈
ℝ) | 
| 26 |  | volicore 46601 | . . . . . . . 8
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ) →
(vol‘((1st ‘(𝐹‘𝑘))[,)(2nd ‘(𝐹‘𝑘)))) ∈ ℝ) | 
| 27 | 23, 25, 26 | syl2anc 584 | . . . . . . 7
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) →
(vol‘((1st ‘(𝐹‘𝑘))[,)(2nd ‘(𝐹‘𝑘)))) ∈ ℝ) | 
| 28 | 20, 27 | eqeltrd 2840 | . . . . . 6
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (vol‘(([,)
∘ 𝐹)‘𝑘)) ∈
ℝ) | 
| 29 | 28 | recnd 11290 | . . . . 5
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (vol‘(([,)
∘ 𝐹)‘𝑘)) ∈
ℂ) | 
| 30 |  | eqid 2736 | . . . . 5
⊢ (𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘))) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘))) | 
| 31 |  | eqid 2736 | . . . . 5
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
(vol‘(([,) ∘ 𝐹)‘𝑘)))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘(([,)
∘ 𝐹)‘𝑘)))) | 
| 32 | 14, 15, 29, 30, 31 | fsumsermpt 45599 | . . . 4
⊢ (𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘(([,)
∘ 𝐹)‘𝑘))))) | 
| 33 | 13, 32 | syl 17 | . . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘))) = seq1( + , (𝑘 ∈ ℕ ↦ (vol‘(([,)
∘ 𝐹)‘𝑘))))) | 
| 34 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) | 
| 35 | 34 | iftrued 4532 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → if((1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘)), ((2nd
‘(𝐹‘𝑘)) − (1st
‘(𝐹‘𝑘))), 0) = ((2nd
‘(𝐹‘𝑘)) − (1st
‘(𝐹‘𝑘)))) | 
| 36 | 13, 23 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐹‘𝑘)) ∈
ℝ) | 
| 37 | 36 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (1st
‘(𝐹‘𝑘)) ∈
ℝ) | 
| 38 | 13, 25 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐹‘𝑘)) ∈
ℝ) | 
| 39 | 38 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (2nd
‘(𝐹‘𝑘)) ∈
ℝ) | 
| 40 |  | ressxr 11306 | . . . . . . . . . . . 12
⊢ ℝ
⊆ ℝ* | 
| 41 | 40, 37 | sselid 3980 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (1st
‘(𝐹‘𝑘)) ∈
ℝ*) | 
| 42 | 40, 39 | sselid 3980 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (2nd
‘(𝐹‘𝑘)) ∈
ℝ*) | 
| 43 |  | xpss 5700 | . . . . . . . . . . . . . . . . . 18
⊢ (ℝ
× ℝ) ⊆ (V × V) | 
| 44 | 43, 21 | sselid 3980 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (V × V)) | 
| 45 |  | 1st2ndb 8055 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑘) ∈ (V × V) ↔ (𝐹‘𝑘) = 〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) | 
| 46 | 44, 45 | sylib 218 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) | 
| 47 | 13, 46 | sylan 580 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) | 
| 48 | 47 | eqcomd 2742 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 〈(1st
‘(𝐹‘𝑘)), (2nd
‘(𝐹‘𝑘))〉 = (𝐹‘𝑘)) | 
| 49 |  | inss1 4236 | . . . . . . . . . . . . . . . . 17
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ ≤ | 
| 50 | 49 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ( ≤ ∩ (ℝ
× ℝ)) ⊆ ≤ ) | 
| 51 | 6, 50 | fssd 6752 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:ℕ⟶ ≤ ) | 
| 52 | 51 | ffvelcdmda 7103 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ≤ ) | 
| 53 | 48, 52 | eqeltrd 2840 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 〈(1st
‘(𝐹‘𝑘)), (2nd
‘(𝐹‘𝑘))〉 ∈ ≤
) | 
| 54 |  | df-br 5143 | . . . . . . . . . . . . 13
⊢
((1st ‘(𝐹‘𝑘)) ≤ (2nd ‘(𝐹‘𝑘)) ↔ 〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉 ∈ ≤ ) | 
| 55 | 53, 54 | sylibr 234 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐹‘𝑘)) ≤ (2nd
‘(𝐹‘𝑘))) | 
| 56 | 55 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (1st
‘(𝐹‘𝑘)) ≤ (2nd
‘(𝐹‘𝑘))) | 
| 57 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) | 
| 58 | 39, 37 | lenltd 11408 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → ((2nd
‘(𝐹‘𝑘)) ≤ (1st
‘(𝐹‘𝑘)) ↔ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘)))) | 
| 59 | 57, 58 | mpbird 257 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (2nd
‘(𝐹‘𝑘)) ≤ (1st
‘(𝐹‘𝑘))) | 
| 60 | 41, 42, 56, 59 | xrletrid 13198 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → (1st
‘(𝐹‘𝑘)) = (2nd
‘(𝐹‘𝑘))) | 
| 61 |  | simp3 1138 | . . . . . . . . . . . . . 14
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → (1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) | 
| 62 |  | simp1 1136 | . . . . . . . . . . . . . . 15
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → (1st ‘(𝐹‘𝑘)) ∈ ℝ) | 
| 63 |  | simp2 1137 | . . . . . . . . . . . . . . 15
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → (2nd ‘(𝐹‘𝑘)) ∈ ℝ) | 
| 64 | 62, 63 | eqleltd 11406 | . . . . . . . . . . . . . 14
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → ((1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘)) ↔ ((1st ‘(𝐹‘𝑘)) ≤ (2nd ‘(𝐹‘𝑘)) ∧ ¬ (1st ‘(𝐹‘𝑘)) < (2nd ‘(𝐹‘𝑘))))) | 
| 65 | 61, 64 | mpbid 232 | . . . . . . . . . . . . 13
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → ((1st ‘(𝐹‘𝑘)) ≤ (2nd ‘(𝐹‘𝑘)) ∧ ¬ (1st ‘(𝐹‘𝑘)) < (2nd ‘(𝐹‘𝑘)))) | 
| 66 | 65 | simprd 495 | . . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) | 
| 67 | 66 | iffalsed 4535 | . . . . . . . . . . 11
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → if((1st ‘(𝐹‘𝑘)) < (2nd ‘(𝐹‘𝑘)), ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘))), 0) = 0) | 
| 68 | 63 | recnd 11290 | . . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → (2nd ‘(𝐹‘𝑘)) ∈ ℂ) | 
| 69 | 61 | eqcomd 2742 | . . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → (2nd ‘(𝐹‘𝑘)) = (1st ‘(𝐹‘𝑘))) | 
| 70 | 68, 69 | subeq0bd 11690 | . . . . . . . . . . 11
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘))) = 0) | 
| 71 | 67, 70 | eqtr4d 2779 | . . . . . . . . . 10
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑘)) = (2nd ‘(𝐹‘𝑘))) → if((1st ‘(𝐹‘𝑘)) < (2nd ‘(𝐹‘𝑘)), ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘))), 0) = ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘)))) | 
| 72 | 37, 39, 60, 71 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘))) → if((1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘)), ((2nd
‘(𝐹‘𝑘)) − (1st
‘(𝐹‘𝑘))), 0) = ((2nd
‘(𝐹‘𝑘)) − (1st
‘(𝐹‘𝑘)))) | 
| 73 | 35, 72 | pm2.61dan 812 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if((1st
‘(𝐹‘𝑘)) < (2nd
‘(𝐹‘𝑘)), ((2nd
‘(𝐹‘𝑘)) − (1st
‘(𝐹‘𝑘))), 0) = ((2nd
‘(𝐹‘𝑘)) − (1st
‘(𝐹‘𝑘)))) | 
| 74 |  | volico 46003 | . . . . . . . . 9
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℝ) →
(vol‘((1st ‘(𝐹‘𝑘))[,)(2nd ‘(𝐹‘𝑘)))) = if((1st ‘(𝐹‘𝑘)) < (2nd ‘(𝐹‘𝑘)), ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘))), 0)) | 
| 75 | 36, 38, 74 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(vol‘((1st ‘(𝐹‘𝑘))[,)(2nd ‘(𝐹‘𝑘)))) = if((1st ‘(𝐹‘𝑘)) < (2nd ‘(𝐹‘𝑘)), ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘))), 0)) | 
| 76 | 36, 38, 55 | abssuble0d 15472 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(abs‘((1st ‘(𝐹‘𝑘)) − (2nd ‘(𝐹‘𝑘)))) = ((2nd ‘(𝐹‘𝑘)) − (1st ‘(𝐹‘𝑘)))) | 
| 77 | 73, 75, 76 | 3eqtr4d 2786 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(vol‘((1st ‘(𝐹‘𝑘))[,)(2nd ‘(𝐹‘𝑘)))) = (abs‘((1st
‘(𝐹‘𝑘)) − (2nd
‘(𝐹‘𝑘))))) | 
| 78 | 13 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹 ∈ ((ℝ × ℝ)
↑m ℕ)) | 
| 79 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) | 
| 80 | 78, 79, 20 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol‘(([,)
∘ 𝐹)‘𝑘)) = (vol‘((1st
‘(𝐹‘𝑘))[,)(2nd
‘(𝐹‘𝑘))))) | 
| 81 | 46 | fveq2d 6909 | . . . . . . . . 9
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → ((abs ∘ −
)‘(𝐹‘𝑘)) = ((abs ∘ −
)‘〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉)) | 
| 82 |  | df-ov 7435 | . . . . . . . . . . 11
⊢
((1st ‘(𝐹‘𝑘))(abs ∘ − )(2nd
‘(𝐹‘𝑘))) = ((abs ∘ −
)‘〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) | 
| 83 | 82 | eqcomi 2745 | . . . . . . . . . 10
⊢ ((abs
∘ − )‘〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) = ((1st ‘(𝐹‘𝑘))(abs ∘ − )(2nd
‘(𝐹‘𝑘))) | 
| 84 | 83 | a1i 11 | . . . . . . . . 9
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → ((abs ∘ −
)‘〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) = ((1st ‘(𝐹‘𝑘))(abs ∘ − )(2nd
‘(𝐹‘𝑘)))) | 
| 85 | 23 | recnd 11290 | . . . . . . . . . 10
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐹‘𝑘)) ∈
ℂ) | 
| 86 | 25 | recnd 11290 | . . . . . . . . . 10
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐹‘𝑘)) ∈
ℂ) | 
| 87 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (abs
∘ − ) = (abs ∘ − ) | 
| 88 | 87 | cnmetdval 24792 | . . . . . . . . . 10
⊢
(((1st ‘(𝐹‘𝑘)) ∈ ℂ ∧ (2nd
‘(𝐹‘𝑘)) ∈ ℂ) →
((1st ‘(𝐹‘𝑘))(abs ∘ − )(2nd
‘(𝐹‘𝑘))) =
(abs‘((1st ‘(𝐹‘𝑘)) − (2nd ‘(𝐹‘𝑘))))) | 
| 89 | 85, 86, 88 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → ((1st
‘(𝐹‘𝑘))(abs ∘ −
)(2nd ‘(𝐹‘𝑘))) = (abs‘((1st
‘(𝐹‘𝑘)) − (2nd
‘(𝐹‘𝑘))))) | 
| 90 | 81, 84, 89 | 3eqtrd 2780 | . . . . . . . 8
⊢ ((𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑘 ∈ ℕ) → ((abs ∘ −
)‘(𝐹‘𝑘)) = (abs‘((1st
‘(𝐹‘𝑘)) − (2nd
‘(𝐹‘𝑘))))) | 
| 91 | 78, 79, 90 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs ∘ −
)‘(𝐹‘𝑘)) = (abs‘((1st
‘(𝐹‘𝑘)) − (2nd
‘(𝐹‘𝑘))))) | 
| 92 | 77, 80, 91 | 3eqtr4d 2786 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol‘(([,)
∘ 𝐹)‘𝑘)) = ((abs ∘ −
)‘(𝐹‘𝑘))) | 
| 93 | 92 | mpteq2dva 5241 | . . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ (vol‘(([,)
∘ 𝐹)‘𝑘))) = (𝑘 ∈ ℕ ↦ ((abs ∘ −
)‘(𝐹‘𝑘)))) | 
| 94 | 13, 16 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ)) | 
| 95 |  | rr2sscn2 45382 | . . . . . . 7
⊢ (ℝ
× ℝ) ⊆ (ℂ × ℂ) | 
| 96 | 95 | a1i 11 | . . . . . 6
⊢ (𝜑 → (ℝ × ℝ)
⊆ (ℂ × ℂ)) | 
| 97 |  | absf 15377 | . . . . . . . 8
⊢
abs:ℂ⟶ℝ | 
| 98 |  | subf 11511 | . . . . . . . 8
⊢  −
:(ℂ × ℂ)⟶ℂ | 
| 99 |  | fco 6759 | . . . . . . . 8
⊢
((abs:ℂ⟶ℝ ∧ − :(ℂ ×
ℂ)⟶ℂ) → (abs ∘ − ):(ℂ ×
ℂ)⟶ℝ) | 
| 100 | 97, 98, 99 | mp2an 692 | . . . . . . 7
⊢ (abs
∘ − ):(ℂ × ℂ)⟶ℝ | 
| 101 | 100 | a1i 11 | . . . . . 6
⊢ (𝜑 → (abs ∘ −
):(ℂ × ℂ)⟶ℝ) | 
| 102 | 94, 96, 101 | fcomptss 45213 | . . . . 5
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐹) = (𝑘 ∈ ℕ ↦ ((abs
∘ − )‘(𝐹‘𝑘)))) | 
| 103 | 93, 102 | eqtr4d 2779 | . . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ (vol‘(([,)
∘ 𝐹)‘𝑘))) = ((abs ∘ − )
∘ 𝐹)) | 
| 104 | 103 | seqeq3d 14051 | . . 3
⊢ (𝜑 → seq1( + , (𝑘 ∈ ℕ ↦
(vol‘(([,) ∘ 𝐹)‘𝑘)))) = seq1( + , ((abs ∘ − )
∘ 𝐹))) | 
| 105 | 33, 104 | eqtr2d 2777 | . 2
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐹)) =
(𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘)))) | 
| 106 | 105 | rneqd 5948 | 1
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ 𝐹)) = ran (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘)))) |