ovolval2lem

Description: The value of the Lebesgue outer measure for subsets of the reals, expressed using sum^ . (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Hypothesis	ovolval2lem.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
	Assertion	ovolval2lem	⊢ ( 𝜑 → ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) = ran ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ovolval2lem.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2		reex	⊢ ℝ ∈ V
3	2 2	xpex	⊢ ( ℝ × ℝ ) ∈ V
4		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
5		mapss	⊢ ( ( ( ℝ × ℝ ) ∈ V ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) ) → ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ⊆ ( ( ℝ × ℝ ) ↑_m ℕ ) )
6	3 4 5	mp2an	⊢ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ⊆ ( ( ℝ × ℝ ) ↑_m ℕ )
7	3	inex2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ∈ V
8	7	a1i	⊢ ( 𝜑 → ( ≤ ∩ ( ℝ × ℝ ) ) ∈ V )
9		nnex	⊢ ℕ ∈ V
10	9	a1i	⊢ ( 𝜑 → ℕ ∈ V )
11	8 10	elmapd	⊢ ( 𝜑 → ( 𝐹 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ↔ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) )
12	1 11	mpbird	⊢ ( 𝜑 → 𝐹 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
13	6 12	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) )
14		1zzd	⊢ ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 1 ∈ ℤ )
15		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
16		elmapi	⊢ ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
17	16	adantr	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
18		simpr	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
19	17 18	fvovco	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
20	19	fveq2d	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) = ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
21	16	ffvelcdmda	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℝ × ℝ ) )
22		xp1st	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
23	21 22	syl	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
24		xp2nd	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
25	21 24	syl	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
26		volicore	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ )
27	23 25 26	syl2anc	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ )
28	20 27	eqeltrd	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ∈ ℝ )
29	28	recnd	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ∈ ℂ )
30		eqid	⊢ ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) )
31		eqid	⊢ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) ) = seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) )
32	14 15 29 30 31	fsumsermpt	⊢ ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) = seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) ) )
33	13 32	syl	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) = seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) ) )
34		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) )
35	34	iftrued	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → if ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) , 0 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
36	13 23	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
37	36	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
38	13 25	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
39	38	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
40		ressxr	⊢ ℝ ⊆ ℝ^*
41	40 37	sselid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ^* )
42	40 39	sselid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ^* )
43		xpss	⊢ ( ℝ × ℝ ) ⊆ ( V × V )
44	43 21	sselid	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ( V × V ) )
45		1st2ndb	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( V × V ) ↔ ( 𝐹 ‘ 𝑘 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ )
46	44 45	sylib	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ )
47	13 46	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ )
48	47	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ = ( 𝐹 ‘ 𝑘 ) )
49		inss1	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ≤
50	49	a1i	⊢ ( 𝜑 → ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ≤ )
51	1 50	fssd	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ≤ )
52	51	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ≤ )
53	48 52	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ ∈ ≤ )
54		df-br	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ ∈ ≤ )
55	53 54	sylibr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) )
56	55	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) )
57		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) )
58	39 37	lenltd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
59	57 58	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) )
60	41 42 56 59	xrletrid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) )
61		simp3	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) )
62		simp1	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
63		simp2	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
64	62 63	eqleltd	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
65	61 64	mpbid	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
66	65	simprd	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) )
67	66	iffalsed	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → if ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) , 0 ) = 0 )
68	63	recnd	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ )
69	61	eqcomd	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) )
70	68 69	subeq0bd	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) = 0 )
71	67 70	eqtr4d	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → if ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) , 0 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
72	37 39 60 71	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) → if ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) , 0 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
73	35 72	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → if ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) , 0 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
74		volico	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) → ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = if ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) , 0 ) )
75	36 38 74	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = if ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) , 0 ) )
76	36 38 55	abssuble0d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
77	73 75 76	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( abs ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
78	13	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) )
79		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
80	78 79 20	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) = ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
81	46	fveq2d	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( abs ∘ − ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ ) )
82		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( abs ∘ − ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ )
83	82	eqcomi	⊢ ( ( abs ∘ − ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) )
84	83	a1i	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
85	23	recnd	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ )
86	25	recnd	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ )
87		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
88	87	cnmetdval	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( abs ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
89	85 86 88	syl2anc	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( abs ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
90	81 84 89	3eqtrd	⊢ ( ( 𝐹 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( abs ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
91	78 79 90	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( abs ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) − ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
92	77 80 91	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) = ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
93	92	mpteq2dva	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
94	13 16	syl	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
95		rr2sscn2	⊢ ( ℝ × ℝ ) ⊆ ( ℂ × ℂ )
96	95	a1i	⊢ ( 𝜑 → ( ℝ × ℝ ) ⊆ ( ℂ × ℂ ) )
97		absf	⊢ abs : ℂ ⟶ ℝ
98		subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
99		fco	⊢ ( ( abs : ℂ ⟶ ℝ ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
100	97 98 99	mp2an	⊢ ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ
101	100	a1i	⊢ ( 𝜑 → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
102	94 96 101	fcomptss	⊢ ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐹 ) = ( 𝑘 ∈ ℕ ↦ ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
103	93 102	eqtr4d	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) = ( ( abs ∘ − ) ∘ 𝐹 ) )
104	103	seqeq3d	⊢ ( 𝜑 → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) )
105	33 104	eqtr2d	⊢ ( 𝜑 → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) )
106	105	rneqd	⊢ ( 𝜑 → ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) = ran ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( vol ‘ ( ( [,) ∘ 𝐹 ) ‘ 𝑘 ) ) ) )

Metamath Proof Explorer

Theorem ovolval2lem

Proof