ovolval5lem2

Description: |- ( ( ph /\ n e. NN ) -> <. ( ( 1st( Fn ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd( Fn ) ) >. e. ( RR X. RR ) ) . (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovolval5lem2.q	⊢ 𝑄 = { 𝑧 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
	ovolval5lem2.y	⊢ ( 𝜑 → 𝑌 = ( Σ^{^} ‘ ( ( vol ∘ [,) ) ∘ 𝐹 ) ) )
	ovolval5lem2.z	⊢ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) )
	ovolval5lem2.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
	ovolval5lem2.s	⊢ ( 𝜑 → 𝐴 ⊆ ∪ ran ( [,) ∘ 𝐹 ) )
	ovolval5lem2.w	⊢ ( 𝜑 → 𝑊 ∈ ℝ⁺ )
	ovolval5lem2.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
Assertion	ovolval5lem2	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑌 +_𝑒 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		ovolval5lem2.q	⊢ 𝑄 = { 𝑧 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
2		ovolval5lem2.y	⊢ ( 𝜑 → 𝑌 = ( Σ^{^} ‘ ( ( vol ∘ [,) ) ∘ 𝐹 ) ) )
3		ovolval5lem2.z	⊢ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) )
4		ovolval5lem2.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
5		ovolval5lem2.s	⊢ ( 𝜑 → 𝐴 ⊆ ∪ ran ( [,) ∘ 𝐹 ) )
6		ovolval5lem2.w	⊢ ( 𝜑 → 𝑊 ∈ ℝ⁺ )
7		ovolval5lem2.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
8	3	a1i	⊢ ( 𝜑 → 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) )
9		nnex	⊢ ℕ ∈ V
10	9	a1i	⊢ ( 𝜑 → ℕ ∈ V )
11		volioof	⊢ ( vol ∘ (,) ) : ( ℝ^* × ℝ^* ) ⟶ ( 0 [,] +∞ )
12	11	a1i	⊢ ( 𝜑 → ( vol ∘ (,) ) : ( ℝ^* × ℝ^* ) ⟶ ( 0 [,] +∞ ) )
13		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* )
14	13	a1i	⊢ ( 𝜑 → ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* ) )
15	4	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
16		xp1st	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
17	15 16	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
18	6	rpred	⊢ ( 𝜑 → 𝑊 ∈ ℝ )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ ℝ )
20		2nn	⊢ 2 ∈ ℕ
21	20	a1i	⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℕ )
22		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀ )
23	21 22	nnexpcld	⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℕ )
24	23	nnred	⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℝ )
25	24	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ∈ ℝ )
26	23	nnne0d	⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ≠ 0 )
27	26	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ≠ 0 )
28	19 25 27	redivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑊 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
29	17 28	resubcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
30		xp2nd	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
31	15 30	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
32	29 31	opelxpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ∈ ( ℝ × ℝ ) )
33	32 7	fmptd	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ℝ × ℝ ) )
34	12 14 33	fcoss	⊢ ( 𝜑 → ( ( vol ∘ (,) ) ∘ 𝐺 ) : ℕ ⟶ ( 0 [,] +∞ ) )
35	10 34	sge0xrcl	⊢ ( 𝜑 → ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ∈ ℝ^* )
36	8 35	eqeltrd	⊢ ( 𝜑 → 𝑍 ∈ ℝ^* )
37		reex	⊢ ℝ ∈ V
38	37 37	xpex	⊢ ( ℝ × ℝ ) ∈ V
39	38	a1i	⊢ ( 𝜑 → ( ℝ × ℝ ) ∈ V )
40	39 10	elmapd	⊢ ( 𝜑 → ( 𝐺 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ↔ 𝐺 : ℕ ⟶ ( ℝ × ℝ ) ) )
41	33 40	mpbird	⊢ ( 𝜑 → 𝐺 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) )
42	33	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
43		xp1st	⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
44	42 43	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
45	44	rexrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ^* )
46		xp2nd	⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
47	42 46	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ )
48	47	rexrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ^* )
49	6	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ ℝ⁺ )
50	23	nnrpd	⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℝ⁺ )
51	50	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ∈ ℝ⁺ )
52	49 51	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑊 / ( 2 ↑ 𝑛 ) ) ∈ ℝ⁺ )
53	17 52	ltsubrpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) < ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) )
54		id	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ )
55		opex	⊢ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ∈ V
56	55	a1i	⊢ ( 𝑛 ∈ ℕ → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ∈ V )
57	7	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ ∧ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ∈ V ) → ( 𝐺 ‘ 𝑛 ) = ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
58	54 56 57	syl2anc	⊢ ( 𝑛 ∈ ℕ → ( 𝐺 ‘ 𝑛 ) = ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
59	58	fveq2d	⊢ ( 𝑛 ∈ ℕ → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) )
60		ovex	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ V
61		fvex	⊢ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ V
62		op1stg	⊢ ( ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ V ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ V ) → ( 1^st ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
63	60 61 62	mp2an	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) )
64	63	a1i	⊢ ( 𝑛 ∈ ℕ → ( 1^st ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
65	59 64	eqtrd	⊢ ( 𝑛 ∈ ℕ → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
66	65	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
67	66	breq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) < ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
68	53 67	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) )
69	58	fveq2d	⊢ ( 𝑛 ∈ ℕ → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) )
70	60 61	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) )
71	70	a1i	⊢ ( 𝑛 ∈ ℕ → ( 2^nd ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) )
72	69 71	eqtrd	⊢ ( 𝑛 ∈ ℕ → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) )
73	72	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) )
74	73	eqcomd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) = ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
75	31 74	eqled	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) )
76		icossioo	⊢ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ^* ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ^* ) ∧ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
77	45 48 68 75 76	syl22anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
78		1st2nd2	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
79	15 78	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
80	79	fveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( [,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) )
81		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( [,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
82	81	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( [,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) )
83	80 82	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
84		1st2nd2	⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 𝐺 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ )
85	42 84	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ )
86	85	fveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ ) )
87		df-ov	⊢ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ )
88	87	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ⟩ ) )
89	86 88	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
90	83 89	sseq12d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
91	77 90	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) )
92	91	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) )
93		ss2iun	⊢ ( ∀ 𝑛 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) → ∪ 𝑛 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ∪ 𝑛 ∈ ℕ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) )
94	92 93	syl	⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ∪ 𝑛 ∈ ℕ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) )
95		fvex	⊢ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ V
96	95	rgenw	⊢ ∀ 𝑛 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ V
97	96	a1i	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ V )
98		dfiun3g	⊢ ( ∀ 𝑛 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ V → ∪ 𝑛 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ∪ ran ( 𝑛 ∈ ℕ ↦ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
99	97 98	syl	⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ∪ ran ( 𝑛 ∈ ℕ ↦ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
100		icof	⊢ [,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^*
101	100	a1i	⊢ ( 𝜑 → [,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^* )
102	4 14 101	fcomptss	⊢ ( 𝜑 → ( [,) ∘ 𝐹 ) = ( 𝑛 ∈ ℕ ↦ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
103	102	eqcomd	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( [,) ∘ 𝐹 ) )
104	103	rneqd	⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ran ( [,) ∘ 𝐹 ) )
105	104	unieqd	⊢ ( 𝜑 → ∪ ran ( 𝑛 ∈ ℕ ↦ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ∪ ran ( [,) ∘ 𝐹 ) )
106	99 105	eqtr2d	⊢ ( 𝜑 → ∪ ran ( [,) ∘ 𝐹 ) = ∪ 𝑛 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) )
107		fvex	⊢ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ V
108	107	rgenw	⊢ ∀ 𝑛 ∈ ℕ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ V
109	108	a1i	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ V )
110		dfiun3g	⊢ ( ∀ 𝑛 ∈ ℕ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ V → ∪ 𝑛 ∈ ℕ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) = ∪ ran ( 𝑛 ∈ ℕ ↦ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
111	109 110	syl	⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) = ∪ ran ( 𝑛 ∈ ℕ ↦ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
112		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
113	112	a1i	⊢ ( 𝜑 → (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ )
114	33 14 113	fcomptss	⊢ ( 𝜑 → ( (,) ∘ 𝐺 ) = ( 𝑛 ∈ ℕ ↦ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
115	114	eqcomd	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( (,) ∘ 𝐺 ) )
116	115	rneqd	⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ran ( (,) ∘ 𝐺 ) )
117	116	unieqd	⊢ ( 𝜑 → ∪ ran ( 𝑛 ∈ ℕ ↦ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ∪ ran ( (,) ∘ 𝐺 ) )
118	111 117	eqtr2d	⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐺 ) = ∪ 𝑛 ∈ ℕ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) )
119	106 118	sseq12d	⊢ ( 𝜑 → ( ∪ ran ( [,) ∘ 𝐹 ) ⊆ ∪ ran ( (,) ∘ 𝐺 ) ↔ ∪ 𝑛 ∈ ℕ ( [,) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ∪ 𝑛 ∈ ℕ ( (,) ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
120	94 119	mpbird	⊢ ( 𝜑 → ∪ ran ( [,) ∘ 𝐹 ) ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
121	5 120	sstrd	⊢ ( 𝜑 → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
122	121 8	jca	⊢ ( 𝜑 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ) )
123		coeq2	⊢ ( 𝑓 = 𝐺 → ( (,) ∘ 𝑓 ) = ( (,) ∘ 𝐺 ) )
124	123	rneqd	⊢ ( 𝑓 = 𝐺 → ran ( (,) ∘ 𝑓 ) = ran ( (,) ∘ 𝐺 ) )
125	124	unieqd	⊢ ( 𝑓 = 𝐺 → ∪ ran ( (,) ∘ 𝑓 ) = ∪ ran ( (,) ∘ 𝐺 ) )
126	125	sseq2d	⊢ ( 𝑓 = 𝐺 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ↔ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ) )
127		coeq2	⊢ ( 𝑓 = 𝐺 → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( ( vol ∘ (,) ) ∘ 𝐺 ) )
128	127	fveq2d	⊢ ( 𝑓 = 𝐺 → ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) )
129	128	eqeq2d	⊢ ( 𝑓 = 𝐺 → ( 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ↔ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ) )
130	126 129	anbi12d	⊢ ( 𝑓 = 𝐺 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ) ) )
131	130	rspcev	⊢ ( ( 𝐺 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
132	41 122 131	syl2anc	⊢ ( 𝜑 → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
133	36 132	jca	⊢ ( 𝜑 → ( 𝑍 ∈ ℝ^* ∧ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
134		eqeq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ↔ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
135	134	anbi2d	⊢ ( 𝑧 = 𝑍 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
136	135	rexbidv	⊢ ( 𝑧 = 𝑍 → ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
137	136 1	elrab2	⊢ ( 𝑍 ∈ 𝑄 ↔ ( 𝑍 ∈ ℝ^* ∧ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑍 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
138	133 137	sylibr	⊢ ( 𝜑 → 𝑍 ∈ 𝑄 )
139		2fveq3	⊢ ( 𝑚 = 𝑛 → ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) = ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) )
140		2fveq3	⊢ ( 𝑚 = 𝑛 → ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) )
141	139 140	breq12d	⊢ ( 𝑚 = 𝑛 → ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
142	141	cbvrabv	⊢ { 𝑚 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) } = { 𝑛 ∈ ℕ ∣ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) }
143	17 31 6 142	ovolval5lem1	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) ≤ ( ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) +_𝑒 𝑊 ) )
144		nfcv	⊢ Ⅎ 𝑛 𝐺
145	33 14	fssd	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
146	144 145	volioofmpt	⊢ ( 𝜑 → ( ( vol ∘ (,) ) ∘ 𝐺 ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) )
147	66 73	oveq12d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
148	147	fveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) = ( vol ‘ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
149	148	mpteq2dva	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) )
150	146 149	eqtrd	⊢ ( 𝜑 → ( ( vol ∘ (,) ) ∘ 𝐺 ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) )
151	150	fveq2d	⊢ ( 𝜑 → ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) = ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) )
152	8 151	eqtrd	⊢ ( 𝜑 → 𝑍 = ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) )
153		nfcv	⊢ Ⅎ 𝑛 𝐹
154		ressxr	⊢ ℝ ⊆ ℝ^*
155		xpss2	⊢ ( ℝ ⊆ ℝ^* → ( ℝ × ℝ ) ⊆ ( ℝ × ℝ^* ) )
156	154 155	ax-mp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ × ℝ^* )
157	156	a1i	⊢ ( 𝜑 → ( ℝ × ℝ ) ⊆ ( ℝ × ℝ^* ) )
158	4 157	fssd	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ^* ) )
159	153 158	volicofmpt	⊢ ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) )
160	159	fveq2d	⊢ ( 𝜑 → ( Σ^{^} ‘ ( ( vol ∘ [,) ) ∘ 𝐹 ) ) = ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) )
161	2 160	eqtrd	⊢ ( 𝜑 → 𝑌 = ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) )
162	161	oveq1d	⊢ ( 𝜑 → ( 𝑌 +_𝑒 𝑊 ) = ( ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) +_𝑒 𝑊 ) )
163	152 162	breq12d	⊢ ( 𝜑 → ( 𝑍 ≤ ( 𝑌 +_𝑒 𝑊 ) ↔ ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) ≤ ( ( Σ^{^} ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) [,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) +_𝑒 𝑊 ) ) )
164	143 163	mpbird	⊢ ( 𝜑 → 𝑍 ≤ ( 𝑌 +_𝑒 𝑊 ) )
165		breq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 ≤ ( 𝑌 +_𝑒 𝑊 ) ↔ 𝑍 ≤ ( 𝑌 +_𝑒 𝑊 ) ) )
166	165	rspcev	⊢ ( ( 𝑍 ∈ 𝑄 ∧ 𝑍 ≤ ( 𝑌 +_𝑒 𝑊 ) ) → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑌 +_𝑒 𝑊 ) )
167	138 164 166	syl2anc	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑄 𝑧 ≤ ( 𝑌 +_𝑒 𝑊 ) )

Metamath Proof Explorer

Theorem ovolval5lem2

Proof