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

Theorem ovolicc2lem5 24266
Description: Lemma for ovolicc2 24267. (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.
StepHypRef Expression
1 ovolicc2.7 . . . 4 (𝜑 → (𝐴[,]𝐵) ⊆ 𝑈)
2 ovolicc.1 . . . . . 6 (𝜑𝐴 ∈ ℝ)
32rexrd 10762 . . . . 5 (𝜑𝐴 ∈ ℝ*)
4 ovolicc.2 . . . . . 6 (𝜑𝐵 ∈ ℝ)
54rexrd 10762 . . . . 5 (𝜑𝐵 ∈ ℝ*)
6 ovolicc.3 . . . . 5 (𝜑𝐴𝐵)
7 lbicc2 12931 . . . . 5 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
83, 5, 6, 7syl3anc 1372 . . . 4 (𝜑𝐴 ∈ (𝐴[,]𝐵))
91, 8sseldd 3876 . . 3 (𝜑𝐴 𝑈)
10 eluni2 4797 . . 3 (𝐴 𝑈 ↔ ∃𝑧𝑈 𝐴𝑧)
119, 10sylib 221 . 2 (𝜑 → ∃𝑧𝑈 𝐴𝑧)
12 ovolicc2.6 . . . . . . 7 (𝜑𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
1312elin2d 4087 . . . . . 6 (𝜑𝑈 ∈ Fin)
14 ovolicc2.10 . . . . . . 7 𝑇 = {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
1514ssrab3 3969 . . . . . 6 𝑇𝑈
16 ssfi 8765 . . . . . 6 ((𝑈 ∈ Fin ∧ 𝑇𝑈) → 𝑇 ∈ Fin)
1713, 15, 16sylancl 589 . . . . 5 (𝜑𝑇 ∈ Fin)
181adantr 484 . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐴[,]𝐵) ⊆ 𝑈)
19 ovolicc2.8 . . . . . . . . . . . . . . 15 (𝜑𝐺:𝑈⟶ℕ)
20 ineq1 4094 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑡 → (𝑢 ∩ (𝐴[,]𝐵)) = (𝑡 ∩ (𝐴[,]𝐵)))
2120neeq1d 2993 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑡 → ((𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ (𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅))
2221, 14elrab2 3588 . . . . . . . . . . . . . . . 16 (𝑡𝑇 ↔ (𝑡𝑈 ∧ (𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅))
2322simplbi 501 . . . . . . . . . . . . . . 15 (𝑡𝑇𝑡𝑈)
24 ffvelrn 6853 . . . . . . . . . . . . . . 15 ((𝐺:𝑈⟶ℕ ∧ 𝑡𝑈) → (𝐺𝑡) ∈ ℕ)
2519, 23, 24syl2an 599 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐺𝑡) ∈ ℕ)
26 ovolicc2.5 . . . . . . . . . . . . . . 15 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2726ffvelrnda 6855 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐺𝑡) ∈ ℕ) → (𝐹‘(𝐺𝑡)) ∈ ( ≤ ∩ (ℝ × ℝ)))
2825, 27syldan 594 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → (𝐹‘(𝐺𝑡)) ∈ ( ≤ ∩ (ℝ × ℝ)))
2928elin2d 4087 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (𝐹‘(𝐺𝑡)) ∈ (ℝ × ℝ))
30 xp2nd 7740 . . . . . . . . . . . 12 ((𝐹‘(𝐺𝑡)) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ)
3129, 30syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → (2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ)
324adantr 484 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 𝐵 ∈ ℝ)
3331, 32ifcld 4457 . . . . . . . . . 10 ((𝜑𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ ℝ)
3422simprbi 500 . . . . . . . . . . . . . 14 (𝑡𝑇 → (𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅)
3534adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → (𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅)
36 n0 4233 . . . . . . . . . . . . 13 ((𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))
3735, 36sylib 221 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → ∃𝑦 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))
382adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝐴 ∈ ℝ)
39 simprr 773 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))
4039elin2d 4087 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ (𝐴[,]𝐵))
414adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝐵 ∈ ℝ)
42 elicc2 12879 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵)))
432, 41, 42syl2an2r 685 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵)))
4440, 43mpbid 235 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵))
4544simp1d 1143 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ ℝ)
4629adantrr 717 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝐹‘(𝐺𝑡)) ∈ (ℝ × ℝ))
4746, 30syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ)
4844simp2d 1144 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝐴𝑦)
4939elin1d 4086 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦𝑡)
5025adantrr 717 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝐺𝑡) ∈ ℕ)
51 fvco3 6761 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐺𝑡) ∈ ℕ) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = ((,)‘(𝐹‘(𝐺𝑡))))
5226, 50, 51syl2an2r 685 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = ((,)‘(𝐹‘(𝐺𝑡))))
53 ovolicc2.9 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
5423, 53sylan2 596 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡𝑇) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
5554adantrr 717 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
56 1st2nd2 7746 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹‘(𝐺𝑡)) ∈ (ℝ × ℝ) → (𝐹‘(𝐺𝑡)) = ⟨(1st ‘(𝐹‘(𝐺𝑡))), (2nd ‘(𝐹‘(𝐺𝑡)))⟩)
5746, 56syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝐹‘(𝐺𝑡)) = ⟨(1st ‘(𝐹‘(𝐺𝑡))), (2nd ‘(𝐹‘(𝐺𝑡)))⟩)
5857fveq2d 6672 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → ((,)‘(𝐹‘(𝐺𝑡))) = ((,)‘⟨(1st ‘(𝐹‘(𝐺𝑡))), (2nd ‘(𝐹‘(𝐺𝑡)))⟩))
59 df-ov 7167 . . . . . . . . . . . . . . . . . . . . 21 ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))) = ((,)‘⟨(1st ‘(𝐹‘(𝐺𝑡))), (2nd ‘(𝐹‘(𝐺𝑡)))⟩)
6058, 59eqtr4di 2791 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → ((,)‘(𝐹‘(𝐺𝑡))) = ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))))
6152, 55, 603eqtr3d 2781 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑡 = ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))))
6249, 61eleqtrd 2835 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))))
63 xp1st 7739 . . . . . . . . . . . . . . . . . . . 20 ((𝐹‘(𝐺𝑡)) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺𝑡))) ∈ ℝ)
6446, 63syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (1st ‘(𝐹‘(𝐺𝑡))) ∈ ℝ)
65 rexr 10758 . . . . . . . . . . . . . . . . . . . 20 ((1st ‘(𝐹‘(𝐺𝑡))) ∈ ℝ → (1st ‘(𝐹‘(𝐺𝑡))) ∈ ℝ*)
66 rexr 10758 . . . . . . . . . . . . . . . . . . . 20 ((2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ → (2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ*)
67 elioo2 12855 . . . . . . . . . . . . . . . . . . . 20 (((1st ‘(𝐹‘(𝐺𝑡))) ∈ ℝ* ∧ (2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ*) → (𝑦 ∈ ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))) ↔ (𝑦 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑡))) < 𝑦𝑦 < (2nd ‘(𝐹‘(𝐺𝑡))))))
6865, 66, 67syl2an 599 . . . . . . . . . . . . . . . . . . 19 (((1st ‘(𝐹‘(𝐺𝑡))) ∈ ℝ ∧ (2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ) → (𝑦 ∈ ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))) ↔ (𝑦 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑡))) < 𝑦𝑦 < (2nd ‘(𝐹‘(𝐺𝑡))))))
6964, 47, 68syl2anc 587 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦 ∈ ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))) ↔ (𝑦 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑡))) < 𝑦𝑦 < (2nd ‘(𝐹‘(𝐺𝑡))))))
7062, 69mpbid 235 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑡))) < 𝑦𝑦 < (2nd ‘(𝐹‘(𝐺𝑡)))))
7170simp3d 1145 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 < (2nd ‘(𝐹‘(𝐺𝑡))))
7245, 47, 71ltled 10859 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ≤ (2nd ‘(𝐹‘(𝐺𝑡))))
7338, 45, 47, 48, 72letrd 10868 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝐴 ≤ (2nd ‘(𝐹‘(𝐺𝑡))))
7473expr 460 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → (𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)) → 𝐴 ≤ (2nd ‘(𝐹‘(𝐺𝑡)))))
7574exlimdv 1939 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (∃𝑦 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)) → 𝐴 ≤ (2nd ‘(𝐹‘(𝐺𝑡)))))
7637, 75mpd 15 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 𝐴 ≤ (2nd ‘(𝐹‘(𝐺𝑡))))
776adantr 484 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 𝐴𝐵)
78 breq2 5031 . . . . . . . . . . . 12 ((2nd ‘(𝐹‘(𝐺𝑡))) = if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) → (𝐴 ≤ (2nd ‘(𝐹‘(𝐺𝑡))) ↔ 𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵)))
79 breq2 5031 . . . . . . . . . . . 12 (𝐵 = if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) → (𝐴𝐵𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵)))
8078, 79ifboth 4450 . . . . . . . . . . 11 ((𝐴 ≤ (2nd ‘(𝐹‘(𝐺𝑡))) ∧ 𝐴𝐵) → 𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵))
8176, 77, 80syl2anc 587 . . . . . . . . . 10 ((𝜑𝑡𝑇) → 𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵))
82 min2 12659 . . . . . . . . . . 11 (((2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ≤ 𝐵)
8331, 32, 82syl2anc 587 . . . . . . . . . 10 ((𝜑𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ≤ 𝐵)
84 elicc2 12879 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐴[,]𝐵) ↔ (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ ℝ ∧ 𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ≤ 𝐵)))
852, 4, 84syl2anc 587 . . . . . . . . . . 11 (𝜑 → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐴[,]𝐵) ↔ (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ ℝ ∧ 𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ≤ 𝐵)))
8685adantr 484 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐴[,]𝐵) ↔ (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ ℝ ∧ 𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ≤ 𝐵)))
8733, 81, 83, 86mpbir3and 1343 . . . . . . . . 9 ((𝜑𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐴[,]𝐵))
8818, 87sseldd 3876 . . . . . . . 8 ((𝜑𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑈)
89 eluni2 4797 . . . . . . . 8 (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑈 ↔ ∃𝑥𝑈 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)
9088, 89sylib 221 . . . . . . 7 ((𝜑𝑡𝑇) → ∃𝑥𝑈 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)
91 simprl 771 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ (𝑥𝑈 ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)) → 𝑥𝑈)
92 simprr 773 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ (𝑥𝑈 ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)
9387adantr 484 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ (𝑥𝑈 ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐴[,]𝐵))
94 inelcm 4351 . . . . . . . . 9 ((if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥 ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐴[,]𝐵)) → (𝑥 ∩ (𝐴[,]𝐵)) ≠ ∅)
9592, 93, 94syl2anc 587 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ (𝑥𝑈 ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)) → (𝑥 ∩ (𝐴[,]𝐵)) ≠ ∅)
96 ineq1 4094 . . . . . . . . . 10 (𝑢 = 𝑥 → (𝑢 ∩ (𝐴[,]𝐵)) = (𝑥 ∩ (𝐴[,]𝐵)))
9796neeq1d 2993 . . . . . . . . 9 (𝑢 = 𝑥 → ((𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ (𝑥 ∩ (𝐴[,]𝐵)) ≠ ∅))
9897, 14elrab2 3588 . . . . . . . 8 (𝑥𝑇 ↔ (𝑥𝑈 ∧ (𝑥 ∩ (𝐴[,]𝐵)) ≠ ∅))
9991, 95, 98sylanbrc 586 . . . . . . 7 (((𝜑𝑡𝑇) ∧ (𝑥𝑈 ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)) → 𝑥𝑇)
10090, 99, 92reximssdv 3185 . . . . . 6 ((𝜑𝑡𝑇) → ∃𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)
101100ralrimiva 3096 . . . . 5 (𝜑 → ∀𝑡𝑇𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)
102 eleq2 2821 . . . . . 6 (𝑥 = (𝑡) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥 ↔ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)))
103102ac6sfi 8829 . . . . 5 ((𝑇 ∈ Fin ∧ ∀𝑡𝑇𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥) → ∃(:𝑇𝑇 ∧ ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)))
10417, 101, 103syl2anc 587 . . . 4 (𝜑 → ∃(:𝑇𝑇 ∧ ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)))
105104adantr 484 . . 3 ((𝜑 ∧ (𝑧𝑈𝐴𝑧)) → ∃(:𝑇𝑇 ∧ ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)))
106 2fveq3 6673 . . . . . . . . . . 11 (𝑥 = 𝑡 → (𝐹‘(𝐺𝑥)) = (𝐹‘(𝐺𝑡)))
107106fveq2d 6672 . . . . . . . . . 10 (𝑥 = 𝑡 → (2nd ‘(𝐹‘(𝐺𝑥))) = (2nd ‘(𝐹‘(𝐺𝑡))))
108107breq1d 5037 . . . . . . . . 9 (𝑥 = 𝑡 → ((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵))
109108, 107ifbieq1d 4435 . . . . . . . 8 (𝑥 = 𝑡 → if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) = if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵))
110 fveq2 6668 . . . . . . . 8 (𝑥 = 𝑡 → (𝑥) = (𝑡))
111109, 110eleq12d 2827 . . . . . . 7 (𝑥 = 𝑡 → (if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥) ↔ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)))
112111cbvralvw 3348 . . . . . 6 (∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥) ↔ ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡))
1132adantr 484 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐴 ∈ ℝ)
1144adantr 484 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐵 ∈ ℝ)
1156adantr 484 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐴𝐵)
116 ovolicc2.4 . . . . . . . . 9 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
11726adantr 484 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
11812adantr 484 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
1191adantr 484 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → (𝐴[,]𝐵) ⊆ 𝑈)
12019adantr 484 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐺:𝑈⟶ℕ)
12153adantlr 715 . . . . . . . . 9 (((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) ∧ 𝑡𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
122 simprrl 781 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → :𝑇𝑇)
123 simprrr 782 . . . . . . . . . 10 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥))
124111rspccva 3523 . . . . . . . . . 10 ((∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥) ∧ 𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡))
125123, 124sylan 583 . . . . . . . . 9 (((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) ∧ 𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡))
126 simprlr 780 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐴𝑧)
127 simprll 779 . . . . . . . . . 10 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝑧𝑈)
1288adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐴 ∈ (𝐴[,]𝐵))
129 inelcm 4351 . . . . . . . . . . 11 ((𝐴𝑧𝐴 ∈ (𝐴[,]𝐵)) → (𝑧 ∩ (𝐴[,]𝐵)) ≠ ∅)
130126, 128, 129syl2anc 587 . . . . . . . . . 10 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → (𝑧 ∩ (𝐴[,]𝐵)) ≠ ∅)
131 ineq1 4094 . . . . . . . . . . . 12 (𝑢 = 𝑧 → (𝑢 ∩ (𝐴[,]𝐵)) = (𝑧 ∩ (𝐴[,]𝐵)))
132131neeq1d 2993 . . . . . . . . . . 11 (𝑢 = 𝑧 → ((𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ (𝑧 ∩ (𝐴[,]𝐵)) ≠ ∅))
133132, 14elrab2 3588 . . . . . . . . . 10 (𝑧𝑇 ↔ (𝑧𝑈 ∧ (𝑧 ∩ (𝐴[,]𝐵)) ≠ ∅))
134127, 130, 133sylanbrc 586 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝑧𝑇)
135 eqid 2738 . . . . . . . . 9 seq1(( ∘ 1st ), (ℕ × {𝑧})) = seq1(( ∘ 1st ), (ℕ × {𝑧}))
136 fveq2 6668 . . . . . . . . . . 11 (𝑚 = 𝑛 → (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑚) = (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑛))
137136eleq2d 2818 . . . . . . . . . 10 (𝑚 = 𝑛 → (𝐵 ∈ (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑚) ↔ 𝐵 ∈ (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑛)))
138137cbvrabv 3392 . . . . . . . . 9 {𝑚 ∈ ℕ ∣ 𝐵 ∈ (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑚)} = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑛)}
139 eqid 2738 . . . . . . . . 9 inf({𝑚 ∈ ℕ ∣ 𝐵 ∈ (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑚)}, ℝ, < ) = inf({𝑚 ∈ ℕ ∣ 𝐵 ∈ (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑚)}, ℝ, < )
140113, 114, 115, 116, 117, 118, 119, 120, 121, 14, 122, 125, 126, 134, 135, 138, 139ovolicc2lem4 24265 . . . . . . . 8 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
141140anassrs 471 . . . . . . 7 (((𝜑 ∧ (𝑧𝑈𝐴𝑧)) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥))) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
142141expr 460 . . . . . 6 (((𝜑 ∧ (𝑧𝑈𝐴𝑧)) ∧ :𝑇𝑇) → (∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < )))
143112, 142syl5bir 246 . . . . 5 (((𝜑 ∧ (𝑧𝑈𝐴𝑧)) ∧ :𝑇𝑇) → (∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < )))
144143expimpd 457 . . . 4 ((𝜑 ∧ (𝑧𝑈𝐴𝑧)) → ((:𝑇𝑇 ∧ ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < )))
145144exlimdv 1939 . . 3 ((𝜑 ∧ (𝑧𝑈𝐴𝑧)) → (∃(:𝑇𝑇 ∧ ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < )))
146105, 145mpd 15 . 2 ((𝜑 ∧ (𝑧𝑈𝐴𝑧)) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
14711, 146rexlimddv 3200 1 (𝜑 → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1088   = wceq 1542  wex 1786  wcel 2113  wne 2934  wral 3053  wrex 3054  {crab 3057  cin 3840  wss 3841  c0 4209  ifcif 4411  𝒫 cpw 4485  {csn 4513  cop 4519   cuni 4793   class class class wbr 5027   × cxp 5517  ran crn 5520  ccom 5523  wf 6329  cfv 6333  (class class class)co 7164  1st c1st 7705  2nd c2nd 7706  Fincfn 8548  supcsup 8970  infcinf 8971  cr 10607  1c1 10609   + caddc 10611  *cxr 10745   < clt 10746  cle 10747  cmin 10941  cn 11709  (,)cioo 12814  [,]cicc 12817  seqcseq 13453  abscabs 14676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-inf2 9170  ax-cnex 10664  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684  ax-pre-mulgt0 10685  ax-pre-sup 10686
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-isom 6342  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-om 7594  df-1st 7707  df-2nd 7708  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-1o 8124  df-er 8313  df-en 8549  df-dom 8550  df-sdom 8551  df-fin 8552  df-sup 8972  df-inf 8973  df-oi 9040  df-card 9434  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752  df-sub 10943  df-neg 10944  df-div 11369  df-nn 11710  df-2 11772  df-3 11773  df-n0 11970  df-z 12056  df-uz 12318  df-rp 12466  df-ioo 12818  df-ico 12820  df-icc 12821  df-fz 12975  df-fzo 13118  df-seq 13454  df-exp 13515  df-hash 13776  df-cj 14541  df-re 14542  df-im 14543  df-sqrt 14677  df-abs 14678  df-clim 14928  df-sum 15129
This theorem is referenced by:  ovolicc2  24267
  Copyright terms: Public domain W3C validator