ovolicc2lem5 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ovolicc2lem5		Structured version Visualization version GIF version

Theorem ovolicc2lem5 25270

Description: Lemma for ovolicc2 25271. (Contributed by Mario Carneiro, 14-Jun-2014.)

**Hypotheses**
Ref	Expression
ovolicc.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ovolicc.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
ovolicc.3	⊢ (𝜑 → 𝐴 ≤ 𝐵)
ovolicc2.4	⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
ovolicc2.5	⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
ovolicc2.6	⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
ovolicc2.7	⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)
ovolicc2.8	⊢ (𝜑 → 𝐺:𝑈⟶ℕ)
ovolicc2.9	⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)
ovolicc2.10	⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}

**Assertion**
Ref	Expression
ovolicc2lem5	⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ^*, < ))

Distinct variable groups: 𝑢,𝑡,𝐴 𝑡,𝐵,𝑢 𝑡,𝐹 𝑡,𝐺 𝜑,𝑡 𝑡,𝑇 𝑡,𝑈,𝑢 Allowed substitution hints: 𝜑(𝑢) 𝑆(𝑢,𝑡) 𝑇(𝑢) 𝐹(𝑢) 𝐺(𝑢)

Proof of Theorem ovolicc2lem5 Dummy variables ℎ 𝑚 𝑛 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovolicc2.7	. . . 4 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)
2		ovolicc.1	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	rexrd 11268	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
4		ovolicc.2	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5	4	rexrd 11268	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
6		ovolicc.3	. . . . 5 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
7		lbicc2 13445	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
8	3, 5, 6, 7	syl3anc 1369	. . . 4 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
9	1, 8	sseldd 3982	. . 3 ⊢ (𝜑 → 𝐴 ∈ ∪ 𝑈)
10		eluni2 4911	. . 3 ⊢ (𝐴 ∈ ∪ 𝑈 ↔ ∃𝑧 ∈ 𝑈 𝐴 ∈ 𝑧)
11	9, 10	sylib 217	. 2 ⊢ (𝜑 → ∃𝑧 ∈ 𝑈 𝐴 ∈ 𝑧)
12		ovolicc2.6	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
13	12	elin2d 4198	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ Fin)
14		ovolicc2.10	. . . . . . 7 ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
15	14	ssrab3 4079	. . . . . 6 ⊢ 𝑇 ⊆ 𝑈
16		ssfi 9175	. . . . . 6 ⊢ ((𝑈 ∈ Fin ∧ 𝑇 ⊆ 𝑈) → 𝑇 ∈ Fin)
17	13, 15, 16	sylancl 584	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ Fin)
18	1	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐴[,]𝐵) ⊆ ∪ 𝑈)
19		ovolicc2.8	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)
20		ineq1 4204	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑡 → (𝑢 ∩ (𝐴[,]𝐵)) = (𝑡 ∩ (𝐴[,]𝐵)))
21	20	neeq1d 2998	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑡 → ((𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ (𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅))
22	21, 14	elrab2 3685	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝑇 ↔ (𝑡 ∈ 𝑈 ∧ (𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅))
23	22	simplbi 496	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝑇 → 𝑡 ∈ 𝑈)
24		ffvelcdm 7082	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝑈⟶ℕ ∧ 𝑡 ∈ 𝑈) → (𝐺‘𝑡) ∈ ℕ)
25	19, 23, 24	syl2an 594	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐺‘𝑡) ∈ ℕ)
26		ovolicc2.5	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
27	26	ffvelcdmda 7085	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐺‘𝑡) ∈ ℕ) → (𝐹‘(𝐺‘𝑡)) ∈ ( ≤ ∩ (ℝ × ℝ)))
28	25, 27	syldan 589	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘(𝐺‘𝑡)) ∈ ( ≤ ∩ (ℝ × ℝ)))
29	28	elin2d 4198	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘(𝐺‘𝑡)) ∈ (ℝ × ℝ))
30		xp2nd 8010	. . . . . . . . . . . 12 ⊢ ((𝐹‘(𝐺‘𝑡)) ∈ (ℝ × ℝ) → (2^nd ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ)
31	29, 30	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (2^nd ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ)
32	4	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐵 ∈ ℝ)
33	31, 32	ifcld 4573	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ ℝ)
34	22	simprbi 495	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝑇 → (𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅)
35	34	adantl 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅)
36		n0 4345	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))
37	35, 36	sylib 217	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∃𝑦 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))
38	2	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝐴 ∈ ℝ)
39		simprr 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))
40	39	elin2d 4198	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ (𝐴[,]𝐵))
41	4	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝐵 ∈ ℝ)
42		elicc2 13393	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)))
43	2, 41, 42	syl2an2r 681	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)))
44	40, 43	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))
45	44	simp1d 1140	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ ℝ)
46	29	adantrr 713	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝐹‘(𝐺‘𝑡)) ∈ (ℝ × ℝ))
47	46, 30	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (2^nd ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ)
48	44	simp2d 1141	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝐴 ≤ 𝑦)
49	39	elin1d 4197	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ 𝑡)
50	25	adantrr 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝐺‘𝑡) ∈ ℕ)
51		fvco3 6989	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐺‘𝑡) ∈ ℕ) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = ((,)‘(𝐹‘(𝐺‘𝑡))))
52	26, 50, 51	syl2an2r 681	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = ((,)‘(𝐹‘(𝐺‘𝑡))))
53		ovolicc2.9	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)
54	23, 53	sylan2 591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)
55	54	adantrr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)
56		1st2nd2 8016	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘(𝐺‘𝑡)) ∈ (ℝ × ℝ) → (𝐹‘(𝐺‘𝑡)) = ⟨(1^st ‘(𝐹‘(𝐺‘𝑡))), (2^nd ‘(𝐹‘(𝐺‘𝑡)))⟩)
57	46, 56	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝐹‘(𝐺‘𝑡)) = ⟨(1^st ‘(𝐹‘(𝐺‘𝑡))), (2^nd ‘(𝐹‘(𝐺‘𝑡)))⟩)
58	57	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → ((,)‘(𝐹‘(𝐺‘𝑡))) = ((,)‘⟨(1^st ‘(𝐹‘(𝐺‘𝑡))), (2^nd ‘(𝐹‘(𝐺‘𝑡)))⟩))
59		df-ov 7414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1^st ‘(𝐹‘(𝐺‘𝑡)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑡)))) = ((,)‘⟨(1^st ‘(𝐹‘(𝐺‘𝑡))), (2^nd ‘(𝐹‘(𝐺‘𝑡)))⟩)
60	58, 59	eqtr4di 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → ((,)‘(𝐹‘(𝐺‘𝑡))) = ((1^st ‘(𝐹‘(𝐺‘𝑡)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑡)))))
61	52, 55, 60	3eqtr3d 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑡 = ((1^st ‘(𝐹‘(𝐺‘𝑡)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑡)))))
62	49, 61	eleqtrd 2833	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ ((1^st ‘(𝐹‘(𝐺‘𝑡)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑡)))))
63		xp1st 8009	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝐺‘𝑡)) ∈ (ℝ × ℝ) → (1^st ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ)
64	46, 63	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (1^st ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ)
65		rexr 11264	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ → (1^st ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ^*)
66		rexr 11264	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ → (2^nd ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ^*)
67		elioo2 13369	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1^st ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ^* ∧ (2^nd ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ^*) → (𝑦 ∈ ((1^st ‘(𝐹‘(𝐺‘𝑡)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑡)))) ↔ (𝑦 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘𝑡))) < 𝑦 ∧ 𝑦 < (2^nd ‘(𝐹‘(𝐺‘𝑡))))))
68	65, 66, 67	syl2an 594	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1^st ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ ∧ (2^nd ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ) → (𝑦 ∈ ((1^st ‘(𝐹‘(𝐺‘𝑡)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑡)))) ↔ (𝑦 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘𝑡))) < 𝑦 ∧ 𝑦 < (2^nd ‘(𝐹‘(𝐺‘𝑡))))))
69	64, 47, 68	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦 ∈ ((1^st ‘(𝐹‘(𝐺‘𝑡)))(,)(2^nd ‘(𝐹‘(𝐺‘𝑡)))) ↔ (𝑦 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘𝑡))) < 𝑦 ∧ 𝑦 < (2^nd ‘(𝐹‘(𝐺‘𝑡))))))
70	62, 69	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘𝑡))) < 𝑦 ∧ 𝑦 < (2^nd ‘(𝐹‘(𝐺‘𝑡)))))
71	70	simp3d 1142	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 < (2^nd ‘(𝐹‘(𝐺‘𝑡))))
72	45, 47, 71	ltled 11366	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ≤ (2^nd ‘(𝐹‘(𝐺‘𝑡))))
73	38, 45, 47, 48, 72	letrd 11375	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝐴 ≤ (2^nd ‘(𝐹‘(𝐺‘𝑡))))
74	73	expr 455	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)) → 𝐴 ≤ (2^nd ‘(𝐹‘(𝐺‘𝑡)))))
75	74	exlimdv 1934	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (∃𝑦 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)) → 𝐴 ≤ (2^nd ‘(𝐹‘(𝐺‘𝑡)))))
76	37, 75	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐴 ≤ (2^nd ‘(𝐹‘(𝐺‘𝑡))))
77	6	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐴 ≤ 𝐵)
78		breq2 5151	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(𝐹‘(𝐺‘𝑡))) = if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) → (𝐴 ≤ (2^nd ‘(𝐹‘(𝐺‘𝑡))) ↔ 𝐴 ≤ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵)))
79		breq2 5151	. . . . . . . . . . . 12 ⊢ (𝐵 = if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵)))
80	78, 79	ifboth 4566	. . . . . . . . . . 11 ⊢ ((𝐴 ≤ (2^nd ‘(𝐹‘(𝐺‘𝑡))) ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵))
81	76, 77, 80	syl2anc 582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐴 ≤ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵))
82		min2 13173	. . . . . . . . . . 11 ⊢ (((2^nd ‘(𝐹‘(𝐺‘𝑡))) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ≤ 𝐵)
83	31, 32, 82	syl2anc 582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ≤ 𝐵)
84		elicc2 13393	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐴[,]𝐵) ↔ (if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ ℝ ∧ 𝐴 ≤ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∧ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ≤ 𝐵)))
85	2, 4, 84	syl2anc 582	. . . . . . . . . . 11 ⊢ (𝜑 → (if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐴[,]𝐵) ↔ (if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ ℝ ∧ 𝐴 ≤ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∧ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ≤ 𝐵)))
86	85	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐴[,]𝐵) ↔ (if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ ℝ ∧ 𝐴 ≤ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∧ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ≤ 𝐵)))
87	33, 81, 83, 86	mpbir3and 1340	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐴[,]𝐵))
88	18, 87	sseldd 3982	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ ∪ 𝑈)
89		eluni2 4911	. . . . . . . 8 ⊢ (if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ ∪ 𝑈 ↔ ∃𝑥 ∈ 𝑈 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥)
90	88, 89	sylib 217	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∃𝑥 ∈ 𝑈 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥)
91		simprl 767	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑥 ∈ 𝑈 ∧ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥)) → 𝑥 ∈ 𝑈)
92		simprr 769	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑥 ∈ 𝑈 ∧ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥)) → if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥)
93	87	adantr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑥 ∈ 𝑈 ∧ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥)) → if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐴[,]𝐵))
94		inelcm 4463	. . . . . . . . 9 ⊢ ((if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥 ∧ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐴[,]𝐵)) → (𝑥 ∩ (𝐴[,]𝐵)) ≠ ∅)
95	92, 93, 94	syl2anc 582	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑥 ∈ 𝑈 ∧ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥)) → (𝑥 ∩ (𝐴[,]𝐵)) ≠ ∅)
96		ineq1 4204	. . . . . . . . . 10 ⊢ (𝑢 = 𝑥 → (𝑢 ∩ (𝐴[,]𝐵)) = (𝑥 ∩ (𝐴[,]𝐵)))
97	96	neeq1d 2998	. . . . . . . . 9 ⊢ (𝑢 = 𝑥 → ((𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ (𝑥 ∩ (𝐴[,]𝐵)) ≠ ∅))
98	97, 14	elrab2 3685	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑇 ↔ (𝑥 ∈ 𝑈 ∧ (𝑥 ∩ (𝐴[,]𝐵)) ≠ ∅))
99	91, 95, 98	sylanbrc 581	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑥 ∈ 𝑈 ∧ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥)) → 𝑥 ∈ 𝑇)
100	90, 99, 92	reximssdv 3170	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∃𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥)
101	100	ralrimiva 3144	. . . . 5 ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 ∃𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥)
102		eleq2 2820	. . . . . 6 ⊢ (𝑥 = (ℎ‘𝑡) → (if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥 ↔ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (ℎ‘𝑡)))
103	102	ac6sfi 9289	. . . . 5 ⊢ ((𝑇 ∈ Fin ∧ ∀𝑡 ∈ 𝑇 ∃𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ 𝑥) → ∃ℎ(ℎ:𝑇⟶𝑇 ∧ ∀𝑡 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (ℎ‘𝑡)))
104	17, 101, 103	syl2anc 582	. . . 4 ⊢ (𝜑 → ∃ℎ(ℎ:𝑇⟶𝑇 ∧ ∀𝑡 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (ℎ‘𝑡)))
105	104	adantr 479	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧)) → ∃ℎ(ℎ:𝑇⟶𝑇 ∧ ∀𝑡 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (ℎ‘𝑡)))
106		2fveq3 6895	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → (𝐹‘(𝐺‘𝑥)) = (𝐹‘(𝐺‘𝑡)))
107	106	fveq2d 6894	. . . . . . . . . 10 ⊢ (𝑥 = 𝑡 → (2^nd ‘(𝐹‘(𝐺‘𝑥))) = (2^nd ‘(𝐹‘(𝐺‘𝑡))))
108	107	breq1d 5157	. . . . . . . . 9 ⊢ (𝑥 = 𝑡 → ((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵 ↔ (2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵))
109	108, 107	ifbieq1d 4551	. . . . . . . 8 ⊢ (𝑥 = 𝑡 → if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) = if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵))
110		fveq2 6890	. . . . . . . 8 ⊢ (𝑥 = 𝑡 → (ℎ‘𝑥) = (ℎ‘𝑡))
111	109, 110	eleq12d 2825	. . . . . . 7 ⊢ (𝑥 = 𝑡 → (if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥) ↔ if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (ℎ‘𝑡)))
112	111	cbvralvw 3232	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥) ↔ ∀𝑡 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (ℎ‘𝑡))
113	2	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → 𝐴 ∈ ℝ)
114	4	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → 𝐵 ∈ ℝ)
115	6	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → 𝐴 ≤ 𝐵)
116		ovolicc2.4	. . . . . . . . 9 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
117	26	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
118	12	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
119	1	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → (𝐴[,]𝐵) ⊆ ∪ 𝑈)
120	19	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → 𝐺:𝑈⟶ℕ)
121	53	adantlr 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)
122		simprrl 777	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → ℎ:𝑇⟶𝑇)
123		simprrr 778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥))
124	111	rspccva 3610	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥) ∧ 𝑡 ∈ 𝑇) → if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (ℎ‘𝑡))
125	123, 124	sylan 578	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) ∧ 𝑡 ∈ 𝑇) → if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (ℎ‘𝑡))
126		simprlr 776	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → 𝐴 ∈ 𝑧)
127		simprll 775	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → 𝑧 ∈ 𝑈)
128	8	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → 𝐴 ∈ (𝐴[,]𝐵))
129		inelcm 4463	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑧 ∧ 𝐴 ∈ (𝐴[,]𝐵)) → (𝑧 ∩ (𝐴[,]𝐵)) ≠ ∅)
130	126, 128, 129	syl2anc 582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → (𝑧 ∩ (𝐴[,]𝐵)) ≠ ∅)
131		ineq1 4204	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑧 → (𝑢 ∩ (𝐴[,]𝐵)) = (𝑧 ∩ (𝐴[,]𝐵)))
132	131	neeq1d 2998	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑧 → ((𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ (𝑧 ∩ (𝐴[,]𝐵)) ≠ ∅))
133	132, 14	elrab2 3685	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑇 ↔ (𝑧 ∈ 𝑈 ∧ (𝑧 ∩ (𝐴[,]𝐵)) ≠ ∅))
134	127, 130, 133	sylanbrc 581	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → 𝑧 ∈ 𝑇)
135		eqid 2730	. . . . . . . . 9 ⊢ seq1((ℎ ∘ 1^st ), (ℕ × {𝑧})) = seq1((ℎ ∘ 1^st ), (ℕ × {𝑧}))
136		fveq2 6890	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (seq1((ℎ ∘ 1^st ), (ℕ × {𝑧}))‘𝑚) = (seq1((ℎ ∘ 1^st ), (ℕ × {𝑧}))‘𝑛))
137	136	eleq2d 2817	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (𝐵 ∈ (seq1((ℎ ∘ 1^st ), (ℕ × {𝑧}))‘𝑚) ↔ 𝐵 ∈ (seq1((ℎ ∘ 1^st ), (ℕ × {𝑧}))‘𝑛)))
138	137	cbvrabv 3440	. . . . . . . . 9 ⊢ {𝑚 ∈ ℕ ∣ 𝐵 ∈ (seq1((ℎ ∘ 1^st ), (ℕ × {𝑧}))‘𝑚)} = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (seq1((ℎ ∘ 1^st ), (ℕ × {𝑧}))‘𝑛)}
139		eqid 2730	. . . . . . . . 9 ⊢ inf({𝑚 ∈ ℕ ∣ 𝐵 ∈ (seq1((ℎ ∘ 1^st ), (ℕ × {𝑧}))‘𝑚)}, ℝ, < ) = inf({𝑚 ∈ ℕ ∣ 𝐵 ∈ (seq1((ℎ ∘ 1^st ), (ℕ × {𝑧}))‘𝑚)}, ℝ, < )
140	113, 114, 115, 116, 117, 118, 119, 120, 121, 14, 122, 125, 126, 134, 135, 138, 139	ovolicc2lem4 25269	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥)))) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ^*, < ))
141	140	anassrs 466	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧)) ∧ (ℎ:𝑇⟶𝑇 ∧ ∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥))) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ^*, < ))
142	141	expr 455	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧)) ∧ ℎ:𝑇⟶𝑇) → (∀𝑥 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑥))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑥))), 𝐵) ∈ (ℎ‘𝑥) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ^*, < )))
143	112, 142	biimtrrid 242	. . . . 5 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧)) ∧ ℎ:𝑇⟶𝑇) → (∀𝑡 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (ℎ‘𝑡) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ^*, < )))
144	143	expimpd 452	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧)) → ((ℎ:𝑇⟶𝑇 ∧ ∀𝑡 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (ℎ‘𝑡)) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ^*, < )))
145	144	exlimdv 1934	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧)) → (∃ℎ(ℎ:𝑇⟶𝑇 ∧ ∀𝑡 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (ℎ‘𝑡)) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ^*, < )))
146	105, 145	mpd 15	. 2 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧)) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ^*, < ))
147	11, 146	rexlimddv 3159	1 ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ^*, < ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1085 = wceq 1539 ∃wex 1779 ∈ wcel 2104 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 {crab 3430 ∩ cin 3946 ⊆ wss 3947 ∅c0 4321 ifcif 4527 𝒫 cpw 4601 {csn 4627 ⟨cop 4633 ∪ cuni 4907 class class class wbr 5147 × cxp 5673 ran crn 5676 ∘ ccom 5679 ⟶wf 6538 ‘cfv 6542 (class class class)co 7411 1^st c1st 7975 2^nd c2nd 7976 Fincfn 8941 supcsup 9437 infcinf 9438 ℝcr 11111 1c1 11113 + caddc 11115 ℝ^*cxr 11251 < clt 11252 ≤ cle 11253 − cmin 11448 ℕcn 12216 (,)cioo 13328 [,]cicc 13331 seqcseq 13970 abscabs 15185

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-inf2 9638 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9439 df-inf 9440 df-oi 9507 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-n0 12477 df-z 12563 df-uz 12827 df-rp 12979 df-ioo 13332 df-ico 13334 df-icc 13335 df-fz 13489 df-fzo 13632 df-seq 13971 df-exp 14032 df-hash 14295 df-cj 15050 df-re 15051 df-im 15052 df-sqrt 15186 df-abs 15187 df-clim 15436 df-sum 15637

This theorem is referenced by: ovolicc2 25271

W3C validator