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

Theorem itg2seq 24355
 Description: Definitional property of the ∫2 integral: for any function 𝐹 there is a countable sequence 𝑔 of simple functions less than 𝐹 whose integrals converge to the integral of 𝐹. (This theorem is for the most part unnecessary in lieu of itg2i1fseq 24368, but unlike that theorem this one doesn't require 𝐹 to be measurable.) (Contributed by Mario Carneiro, 14-Aug-2014.)
Assertion
Ref Expression
itg2seq (𝐹:ℝ⟶(0[,]+∞) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∘r𝐹 ∧ (∫2𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < )))
Distinct variable group:   𝑔,𝑛,𝐹

Proof of Theorem itg2seq
Dummy variables 𝑓 𝑚 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnre 11643 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
21ad2antlr 726 . . . . . . . . . . 11 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2𝐹) = +∞) → 𝑛 ∈ ℝ)
32ltpnfd 12515 . . . . . . . . . 10 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2𝐹) = +∞) → 𝑛 < +∞)
4 iftrue 4456 . . . . . . . . . . 11 ((∫2𝐹) = +∞ → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) = 𝑛)
54adantl 485 . . . . . . . . . 10 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2𝐹) = +∞) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) = 𝑛)
6 simpr 488 . . . . . . . . . 10 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2𝐹) = +∞) → (∫2𝐹) = +∞)
73, 5, 63brtr4d 5085 . . . . . . . . 9 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ (∫2𝐹) = +∞) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫2𝐹))
8 iffalse 4459 . . . . . . . . . . 11 (¬ (∫2𝐹) = +∞ → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) = ((∫2𝐹) − (1 / 𝑛)))
98adantl 485 . . . . . . . . . 10 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2𝐹) = +∞) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) = ((∫2𝐹) − (1 / 𝑛)))
10 itg2cl 24345 . . . . . . . . . . . . . . 15 (𝐹:ℝ⟶(0[,]+∞) → (∫2𝐹) ∈ ℝ*)
11 xrrebnd 12560 . . . . . . . . . . . . . . 15 ((∫2𝐹) ∈ ℝ* → ((∫2𝐹) ∈ ℝ ↔ (-∞ < (∫2𝐹) ∧ (∫2𝐹) < +∞)))
1210, 11syl 17 . . . . . . . . . . . . . 14 (𝐹:ℝ⟶(0[,]+∞) → ((∫2𝐹) ∈ ℝ ↔ (-∞ < (∫2𝐹) ∧ (∫2𝐹) < +∞)))
13 itg2ge0 24348 . . . . . . . . . . . . . . . 16 (𝐹:ℝ⟶(0[,]+∞) → 0 ≤ (∫2𝐹))
14 mnflt0 12519 . . . . . . . . . . . . . . . . 17 -∞ < 0
15 mnfxr 10698 . . . . . . . . . . . . . . . . . 18 -∞ ∈ ℝ*
16 0xr 10688 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ*
17 xrltletr 12549 . . . . . . . . . . . . . . . . . 18 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (∫2𝐹) ∈ ℝ*) → ((-∞ < 0 ∧ 0 ≤ (∫2𝐹)) → -∞ < (∫2𝐹)))
1815, 16, 10, 17mp3an12i 1462 . . . . . . . . . . . . . . . . 17 (𝐹:ℝ⟶(0[,]+∞) → ((-∞ < 0 ∧ 0 ≤ (∫2𝐹)) → -∞ < (∫2𝐹)))
1914, 18mpani 695 . . . . . . . . . . . . . . . 16 (𝐹:ℝ⟶(0[,]+∞) → (0 ≤ (∫2𝐹) → -∞ < (∫2𝐹)))
2013, 19mpd 15 . . . . . . . . . . . . . . 15 (𝐹:ℝ⟶(0[,]+∞) → -∞ < (∫2𝐹))
2120biantrurd 536 . . . . . . . . . . . . . 14 (𝐹:ℝ⟶(0[,]+∞) → ((∫2𝐹) < +∞ ↔ (-∞ < (∫2𝐹) ∧ (∫2𝐹) < +∞)))
22 nltpnft 12556 . . . . . . . . . . . . . . . 16 ((∫2𝐹) ∈ ℝ* → ((∫2𝐹) = +∞ ↔ ¬ (∫2𝐹) < +∞))
2310, 22syl 17 . . . . . . . . . . . . . . 15 (𝐹:ℝ⟶(0[,]+∞) → ((∫2𝐹) = +∞ ↔ ¬ (∫2𝐹) < +∞))
2423con2bid 358 . . . . . . . . . . . . . 14 (𝐹:ℝ⟶(0[,]+∞) → ((∫2𝐹) < +∞ ↔ ¬ (∫2𝐹) = +∞))
2512, 21, 243bitr2rd 311 . . . . . . . . . . . . 13 (𝐹:ℝ⟶(0[,]+∞) → (¬ (∫2𝐹) = +∞ ↔ (∫2𝐹) ∈ ℝ))
2625biimpa 480 . . . . . . . . . . . 12 ((𝐹:ℝ⟶(0[,]+∞) ∧ ¬ (∫2𝐹) = +∞) → (∫2𝐹) ∈ ℝ)
2726adantlr 714 . . . . . . . . . . 11 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2𝐹) = +∞) → (∫2𝐹) ∈ ℝ)
28 nnrp 12399 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
2928rpreccld 12440 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ+)
3029ad2antlr 726 . . . . . . . . . . 11 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2𝐹) = +∞) → (1 / 𝑛) ∈ ℝ+)
3127, 30ltsubrpd 12462 . . . . . . . . . 10 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2𝐹) = +∞) → ((∫2𝐹) − (1 / 𝑛)) < (∫2𝐹))
329, 31eqbrtrd 5075 . . . . . . . . 9 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2𝐹) = +∞) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫2𝐹))
337, 32pm2.61dan 812 . . . . . . . 8 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫2𝐹))
34 nnrecre 11678 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
3534ad2antlr 726 . . . . . . . . . . . 12 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2𝐹) = +∞) → (1 / 𝑛) ∈ ℝ)
3627, 35resubcld 11068 . . . . . . . . . . 11 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ ¬ (∫2𝐹) = +∞) → ((∫2𝐹) − (1 / 𝑛)) ∈ ℝ)
372, 36ifclda 4484 . . . . . . . . . 10 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ)
3837rexrd 10691 . . . . . . . . 9 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ*)
3910adantr 484 . . . . . . . . 9 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (∫2𝐹) ∈ ℝ*)
40 xrltnle 10708 . . . . . . . . 9 ((if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ* ∧ (∫2𝐹) ∈ ℝ*) → (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫2𝐹) ↔ ¬ (∫2𝐹) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛)))))
4138, 39, 40syl2anc 587 . . . . . . . 8 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫2𝐹) ↔ ¬ (∫2𝐹) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛)))))
4233, 41mpbid 235 . . . . . . 7 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ¬ (∫2𝐹) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))))
43 itg2leub 24347 . . . . . . . 8 ((𝐹:ℝ⟶(0[,]+∞) ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ*) → ((∫2𝐹) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ↔ ∀𝑓 ∈ dom ∫1(𝑓r𝐹 → (∫1𝑓) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))))))
4438, 43syldan 594 . . . . . . 7 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ((∫2𝐹) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ↔ ∀𝑓 ∈ dom ∫1(𝑓r𝐹 → (∫1𝑓) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))))))
4542, 44mtbid 327 . . . . . 6 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ¬ ∀𝑓 ∈ dom ∫1(𝑓r𝐹 → (∫1𝑓) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛)))))
46 rexanali 3257 . . . . . 6 (∃𝑓 ∈ dom ∫1(𝑓r𝐹 ∧ ¬ (∫1𝑓) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛)))) ↔ ¬ ∀𝑓 ∈ dom ∫1(𝑓r𝐹 → (∫1𝑓) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛)))))
4745, 46sylibr 237 . . . . 5 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ∃𝑓 ∈ dom ∫1(𝑓r𝐹 ∧ ¬ (∫1𝑓) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛)))))
48 itg1cl 24298 . . . . . . . 8 (𝑓 ∈ dom ∫1 → (∫1𝑓) ∈ ℝ)
49 ltnle 10720 . . . . . . . 8 ((if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ ∧ (∫1𝑓) ∈ ℝ) → (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1𝑓) ↔ ¬ (∫1𝑓) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛)))))
5037, 48, 49syl2an 598 . . . . . . 7 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑓 ∈ dom ∫1) → (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1𝑓) ↔ ¬ (∫1𝑓) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛)))))
5150anbi2d 631 . . . . . 6 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑓 ∈ dom ∫1) → ((𝑓r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1𝑓)) ↔ (𝑓r𝐹 ∧ ¬ (∫1𝑓) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))))))
5251rexbidva 3288 . . . . 5 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (∃𝑓 ∈ dom ∫1(𝑓r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1𝑓)) ↔ ∃𝑓 ∈ dom ∫1(𝑓r𝐹 ∧ ¬ (∫1𝑓) ≤ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))))))
5347, 52mpbird 260 . . . 4 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ∃𝑓 ∈ dom ∫1(𝑓r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1𝑓)))
5453ralrimiva 3177 . . 3 (𝐹:ℝ⟶(0[,]+∞) → ∀𝑛 ∈ ℕ ∃𝑓 ∈ dom ∫1(𝑓r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1𝑓)))
55 ovex 7184 . . . . 5 (ℝ ↑m ℝ) ∈ V
56 i1ff 24289 . . . . . . 7 (𝑥 ∈ dom ∫1𝑥:ℝ⟶ℝ)
57 reex 10628 . . . . . . . 8 ℝ ∈ V
5857, 57elmap 8433 . . . . . . 7 (𝑥 ∈ (ℝ ↑m ℝ) ↔ 𝑥:ℝ⟶ℝ)
5956, 58sylibr 237 . . . . . 6 (𝑥 ∈ dom ∫1𝑥 ∈ (ℝ ↑m ℝ))
6059ssriv 3957 . . . . 5 dom ∫1 ⊆ (ℝ ↑m ℝ)
6155, 60ssexi 5213 . . . 4 dom ∫1 ∈ V
62 nnenom 13354 . . . 4 ℕ ≈ ω
63 breq1 5056 . . . . 5 (𝑓 = (𝑔𝑛) → (𝑓r𝐹 ↔ (𝑔𝑛) ∘r𝐹))
64 fveq2 6663 . . . . . 6 (𝑓 = (𝑔𝑛) → (∫1𝑓) = (∫1‘(𝑔𝑛)))
6564breq2d 5065 . . . . 5 (𝑓 = (𝑔𝑛) → (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1𝑓) ↔ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))
6663, 65anbi12d 633 . . . 4 (𝑓 = (𝑔𝑛) → ((𝑓r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1𝑓)) ↔ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛)))))
6761, 62, 66axcc4 9861 . . 3 (∀𝑛 ∈ ℕ ∃𝑓 ∈ dom ∫1(𝑓r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1𝑓)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛)))))
6854, 67syl 17 . 2 (𝐹:ℝ⟶(0[,]+∞) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛)))))
69 simprl 770 . . . . 5 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → 𝑔:ℕ⟶dom ∫1)
70 simpl 486 . . . . . . 7 (((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))) → (𝑔𝑛) ∘r𝐹)
7170ralimi 3155 . . . . . 6 (∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))) → ∀𝑛 ∈ ℕ (𝑔𝑛) ∘r𝐹)
7271ad2antll 728 . . . . 5 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → ∀𝑛 ∈ ℕ (𝑔𝑛) ∘r𝐹)
7310adantr 484 . . . . . 6 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → (∫2𝐹) ∈ ℝ*)
74 ffvelrn 6842 . . . . . . . . . . . 12 ((𝑔:ℕ⟶dom ∫1𝑛 ∈ ℕ) → (𝑔𝑛) ∈ dom ∫1)
75 itg1cl 24298 . . . . . . . . . . . 12 ((𝑔𝑛) ∈ dom ∫1 → (∫1‘(𝑔𝑛)) ∈ ℝ)
7674, 75syl 17 . . . . . . . . . . 11 ((𝑔:ℕ⟶dom ∫1𝑛 ∈ ℕ) → (∫1‘(𝑔𝑛)) ∈ ℝ)
7776fmpttd 6872 . . . . . . . . . 10 (𝑔:ℕ⟶dom ∫1 → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))):ℕ⟶ℝ)
7877ad2antrl 727 . . . . . . . . 9 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))):ℕ⟶ℝ)
7978frnd 6512 . . . . . . . 8 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))) ⊆ ℝ)
80 ressxr 10685 . . . . . . . 8 ℝ ⊆ ℝ*
8179, 80sstrdi 3965 . . . . . . 7 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))) ⊆ ℝ*)
82 supxrcl 12707 . . . . . . 7 (ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))) ⊆ ℝ* → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < ) ∈ ℝ*)
8381, 82syl 17 . . . . . 6 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < ) ∈ ℝ*)
8438adantlr 714 . . . . . . . . . . . . 13 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ*)
8576adantll 713 . . . . . . . . . . . . . 14 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔𝑛)) ∈ ℝ)
8685rexrd 10691 . . . . . . . . . . . . 13 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔𝑛)) ∈ ℝ*)
87 xrltle 12541 . . . . . . . . . . . . 13 ((if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ* ∧ (∫1‘(𝑔𝑛)) ∈ ℝ*) → (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛)) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔𝑛))))
8884, 86, 87syl2anc 587 . . . . . . . . . . . 12 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛)) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔𝑛))))
89 2fveq3 6668 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → (∫1‘(𝑔𝑛)) = (∫1‘(𝑔𝑚)))
9089cbvmptv 5156 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))) = (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚)))
9190rneqi 5795 . . . . . . . . . . . . . . 15 ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))) = ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚)))
9277adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))):ℕ⟶ℝ)
9392frnd 6512 . . . . . . . . . . . . . . . . 17 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))) ⊆ ℝ)
9493, 80sstrdi 3965 . . . . . . . . . . . . . . . 16 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))) ⊆ ℝ*)
9594adantr 484 . . . . . . . . . . . . . . 15 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))) ⊆ ℝ*)
9691, 95eqsstrrid 4002 . . . . . . . . . . . . . 14 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))) ⊆ ℝ*)
97 2fveq3 6668 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (∫1‘(𝑔𝑚)) = (∫1‘(𝑔𝑛)))
98 eqid 2824 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))) = (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚)))
99 fvex 6676 . . . . . . . . . . . . . . . . 17 (∫1‘(𝑔𝑛)) ∈ V
10097, 98, 99fvmpt 6761 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚)))‘𝑛) = (∫1‘(𝑔𝑛)))
101 fvex 6676 . . . . . . . . . . . . . . . . . 18 (∫1‘(𝑔𝑚)) ∈ V
102101, 98fnmpti 6482 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))) Fn ℕ
103 fnfvelrn 6841 . . . . . . . . . . . . . . . . 17 (((𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))) Fn ℕ ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚)))‘𝑛) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))))
104102, 103mpan 689 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚)))‘𝑛) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))))
105100, 104eqeltrrd 2917 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (∫1‘(𝑔𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))))
106105adantl 485 . . . . . . . . . . . . . 14 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))))
107 supxrub 12716 . . . . . . . . . . . . . 14 ((ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))) ⊆ ℝ* ∧ (∫1‘(𝑔𝑛)) ∈ ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚)))) → (∫1‘(𝑔𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ))
10896, 106, 107syl2anc 587 . . . . . . . . . . . . 13 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (∫1‘(𝑔𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ))
10991supeq1i 8910 . . . . . . . . . . . . . . 15 sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < ) = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )
11095, 82syl 17 . . . . . . . . . . . . . . 15 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < ) ∈ ℝ*)
111109, 110eqeltrrid 2921 . . . . . . . . . . . . . 14 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ) ∈ ℝ*)
112 xrletr 12550 . . . . . . . . . . . . . 14 ((if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ* ∧ (∫1‘(𝑔𝑛)) ∈ ℝ* ∧ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ) ∈ ℝ*) → ((if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔𝑛)) ∧ (∫1‘(𝑔𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )))
11384, 86, 111, 112syl3anc 1368 . . . . . . . . . . . . 13 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ((if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔𝑛)) ∧ (∫1‘(𝑔𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )))
114108, 113mpan2d 693 . . . . . . . . . . . 12 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔𝑛)) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )))
11588, 114syld 47 . . . . . . . . . . 11 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛)) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )))
116115adantld 494 . . . . . . . . . 10 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )))
117116ralimdva 3172 . . . . . . . . 9 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))) → ∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )))
118117impr 458 . . . . . . . 8 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → ∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ))
119 breq2 5057 . . . . . . . . . . 11 (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ) → (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )))
120119ralbidv 3192 . . . . . . . . . 10 (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ) → (∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )))
121 breq2 5057 . . . . . . . . . 10 (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ) → ((∫2𝐹) ≤ 𝑥 ↔ (∫2𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )))
122120, 121imbi12d 348 . . . . . . . . 9 (𝑥 = sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ) → ((∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2𝐹) ≤ 𝑥) ↔ (∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ) → (∫2𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ))))
123 elxr 12510 . . . . . . . . . . . 12 (𝑥 ∈ ℝ* ↔ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞))
124 simplrl 776 . . . . . . . . . . . . . . . . . . 19 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ (∫2𝐹) = +∞) → 𝑥 ∈ ℝ)
125 arch 11893 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → ∃𝑛 ∈ ℕ 𝑥 < 𝑛)
126124, 125syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ (∫2𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < 𝑛)
1274adantl 485 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ (∫2𝐹) = +∞) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) = 𝑛)
128127breq2d 5065 . . . . . . . . . . . . . . . . . . 19 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ (∫2𝐹) = +∞) → (𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ↔ 𝑥 < 𝑛))
129128rexbidv 3289 . . . . . . . . . . . . . . . . . 18 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ (∫2𝐹) = +∞) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ↔ ∃𝑛 ∈ ℕ 𝑥 < 𝑛))
130126, 129mpbird 260 . . . . . . . . . . . . . . . . 17 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ (∫2𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))))
13126adantlr 714 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) → (∫2𝐹) ∈ ℝ)
132 simplrl 776 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) → 𝑥 ∈ ℝ)
133131, 132resubcld 11068 . . . . . . . . . . . . . . . . . . 19 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) → ((∫2𝐹) − 𝑥) ∈ ℝ)
134 simplrr 777 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) → 𝑥 < (∫2𝐹))
135132, 131posdifd 11227 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) → (𝑥 < (∫2𝐹) ↔ 0 < ((∫2𝐹) − 𝑥)))
136134, 135mpbid 235 . . . . . . . . . . . . . . . . . . 19 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) → 0 < ((∫2𝐹) − 𝑥))
137 nnrecl 11894 . . . . . . . . . . . . . . . . . . 19 ((((∫2𝐹) − 𝑥) ∈ ℝ ∧ 0 < ((∫2𝐹) − 𝑥)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2𝐹) − 𝑥))
138133, 136, 137syl2anc 587 . . . . . . . . . . . . . . . . . 18 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) → ∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2𝐹) − 𝑥))
13934adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
140131adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (∫2𝐹) ∈ ℝ)
141132adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
142 ltsub13 11121 . . . . . . . . . . . . . . . . . . . . 21 (((1 / 𝑛) ∈ ℝ ∧ (∫2𝐹) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((1 / 𝑛) < ((∫2𝐹) − 𝑥) ↔ 𝑥 < ((∫2𝐹) − (1 / 𝑛))))
143139, 140, 141, 142syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) < ((∫2𝐹) − 𝑥) ↔ 𝑥 < ((∫2𝐹) − (1 / 𝑛))))
1448ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) = ((∫2𝐹) − (1 / 𝑛)))
145144breq2d 5065 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → (𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ↔ 𝑥 < ((∫2𝐹) − (1 / 𝑛))))
146143, 145bitr4d 285 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) < ((∫2𝐹) − 𝑥) ↔ 𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛)))))
147146rexbidva 3288 . . . . . . . . . . . . . . . . . 18 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) → (∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2𝐹) − 𝑥) ↔ ∃𝑛 ∈ ℕ 𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛)))))
148138, 147mpbid 235 . . . . . . . . . . . . . . . . 17 (((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) ∧ ¬ (∫2𝐹) = +∞) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))))
149130, 148pm2.61dan 812 . . . . . . . . . . . . . . . 16 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (∫2𝐹))) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))))
150149expr 460 . . . . . . . . . . . . . . 15 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝑥 < (∫2𝐹) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛)))))
151 rexr 10687 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
152 xrltnle 10708 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ* ∧ (∫2𝐹) ∈ ℝ*) → (𝑥 < (∫2𝐹) ↔ ¬ (∫2𝐹) ≤ 𝑥))
153151, 10, 152syl2anr 599 . . . . . . . . . . . . . . 15 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝑥 < (∫2𝐹) ↔ ¬ (∫2𝐹) ≤ 𝑥))
154151ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ*)
15538adantlr 714 . . . . . . . . . . . . . . . . . 18 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ*)
156 xrltnle 10708 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ* ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ*) → (𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥))
157154, 155, 156syl2anc 587 . . . . . . . . . . . . . . . . 17 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥))
158157rexbidva 3288 . . . . . . . . . . . . . . . 16 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ↔ ∃𝑛 ∈ ℕ ¬ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥))
159 rexnal 3232 . . . . . . . . . . . . . . . 16 (∃𝑛 ∈ ℕ ¬ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ ¬ ∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥)
160158, 159syl6bb 290 . . . . . . . . . . . . . . 15 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∃𝑛 ∈ ℕ 𝑥 < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ↔ ¬ ∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥))
161150, 153, 1603imtr3d 296 . . . . . . . . . . . . . 14 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (¬ (∫2𝐹) ≤ 𝑥 → ¬ ∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥))
162161con4d 115 . . . . . . . . . . . . 13 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2𝐹) ≤ 𝑥))
16310adantr 484 . . . . . . . . . . . . . . . 16 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2𝐹) ∈ ℝ*)
164 pnfge 12524 . . . . . . . . . . . . . . . 16 ((∫2𝐹) ∈ ℝ* → (∫2𝐹) ≤ +∞)
165163, 164syl 17 . . . . . . . . . . . . . . 15 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2𝐹) ≤ +∞)
166 simpr 488 . . . . . . . . . . . . . . 15 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → 𝑥 = +∞)
167165, 166breqtrrd 5081 . . . . . . . . . . . . . 14 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∫2𝐹) ≤ 𝑥)
168167a1d 25 . . . . . . . . . . . . 13 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = +∞) → (∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2𝐹) ≤ 𝑥))
169 1nn 11647 . . . . . . . . . . . . . . . 16 1 ∈ ℕ
170169ne0ii 4286 . . . . . . . . . . . . . . 15 ℕ ≠ ∅
171 r19.2z 4423 . . . . . . . . . . . . . . 15 ((ℕ ≠ ∅ ∧ ∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥) → ∃𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥)
172170, 171mpan 689 . . . . . . . . . . . . . 14 (∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 → ∃𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥)
17337adantlr 714 . . . . . . . . . . . . . . . . . 18 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ)
174 mnflt 12517 . . . . . . . . . . . . . . . . . . 19 (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ → -∞ < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))))
175 rexr 10687 . . . . . . . . . . . . . . . . . . . 20 (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ → if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ*)
176 xrltnle 10708 . . . . . . . . . . . . . . . . . . . 20 ((-∞ ∈ ℝ* ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ*) → (-∞ < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ -∞))
17715, 175, 176sylancr 590 . . . . . . . . . . . . . . . . . . 19 (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ → (-∞ < if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ↔ ¬ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ -∞))
178174, 177mpbid 235 . . . . . . . . . . . . . . . . . 18 (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ∈ ℝ → ¬ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ -∞)
179173, 178syl 17 . . . . . . . . . . . . . . . . 17 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → ¬ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ -∞)
180 simplr 768 . . . . . . . . . . . . . . . . . 18 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → 𝑥 = -∞)
181180breq2d 5065 . . . . . . . . . . . . . . . . 17 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → (if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ -∞))
182179, 181mtbird 328 . . . . . . . . . . . . . . . 16 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) ∧ 𝑛 ∈ ℕ) → ¬ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥)
183182nrexdv 3262 . . . . . . . . . . . . . . 15 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) → ¬ ∃𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥)
184183pm2.21d 121 . . . . . . . . . . . . . 14 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) → (∃𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2𝐹) ≤ 𝑥))
185172, 184syl5 34 . . . . . . . . . . . . 13 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 = -∞) → (∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2𝐹) ≤ 𝑥))
186162, 168, 1853jaodan 1427 . . . . . . . . . . . 12 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞)) → (∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2𝐹) ≤ 𝑥))
187123, 186sylan2b 596 . . . . . . . . . . 11 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ*) → (∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2𝐹) ≤ 𝑥))
188187ralrimiva 3177 . . . . . . . . . 10 (𝐹:ℝ⟶(0[,]+∞) → ∀𝑥 ∈ ℝ* (∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2𝐹) ≤ 𝑥))
189188adantr 484 . . . . . . . . 9 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → ∀𝑥 ∈ ℝ* (∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2𝐹) ≤ 𝑥))
190109, 83eqeltrrid 2921 . . . . . . . . 9 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ) ∈ ℝ*)
191122, 189, 190rspcdva 3611 . . . . . . . 8 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → (∀𝑛 ∈ ℕ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ) → (∫2𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < )))
192118, 191mpd 15 . . . . . . 7 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → (∫2𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦ (∫1‘(𝑔𝑚))), ℝ*, < ))
193192, 109breqtrrdi 5095 . . . . . 6 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → (∫2𝐹) ≤ sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < ))
194 itg2ub 24346 . . . . . . . . . . . . . . 15 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔𝑛) ∈ dom ∫1 ∧ (𝑔𝑛) ∘r𝐹) → (∫1‘(𝑔𝑛)) ≤ (∫2𝐹))
1951943expia 1118 . . . . . . . . . . . . . 14 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔𝑛) ∈ dom ∫1) → ((𝑔𝑛) ∘r𝐹 → (∫1‘(𝑔𝑛)) ≤ (∫2𝐹)))
19674, 195sylan2 595 . . . . . . . . . . . . 13 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1𝑛 ∈ ℕ)) → ((𝑔𝑛) ∘r𝐹 → (∫1‘(𝑔𝑛)) ≤ (∫2𝐹)))
197196anassrs 471 . . . . . . . . . . . 12 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → ((𝑔𝑛) ∘r𝐹 → (∫1‘(𝑔𝑛)) ≤ (∫2𝐹)))
198197adantrd 495 . . . . . . . . . . 11 (((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) ∧ 𝑛 ∈ ℕ) → (((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))) → (∫1‘(𝑔𝑛)) ≤ (∫2𝐹)))
199198ralimdva 3172 . . . . . . . . . 10 ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝑔:ℕ⟶dom ∫1) → (∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))) → ∀𝑛 ∈ ℕ (∫1‘(𝑔𝑛)) ≤ (∫2𝐹)))
200199impr 458 . . . . . . . . 9 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → ∀𝑛 ∈ ℕ (∫1‘(𝑔𝑛)) ≤ (∫2𝐹))
201 eqid 2824 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))) = (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))
20289, 201, 101fvmpt 6761 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))‘𝑚) = (∫1‘(𝑔𝑚)))
203202breq1d 5063 . . . . . . . . . . 11 (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))‘𝑚) ≤ (∫2𝐹) ↔ (∫1‘(𝑔𝑚)) ≤ (∫2𝐹)))
204203ralbiia 3159 . . . . . . . . . 10 (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))‘𝑚) ≤ (∫2𝐹) ↔ ∀𝑚 ∈ ℕ (∫1‘(𝑔𝑚)) ≤ (∫2𝐹))
20589breq1d 5063 . . . . . . . . . . 11 (𝑛 = 𝑚 → ((∫1‘(𝑔𝑛)) ≤ (∫2𝐹) ↔ (∫1‘(𝑔𝑚)) ≤ (∫2𝐹)))
206205cbvralvw 3434 . . . . . . . . . 10 (∀𝑛 ∈ ℕ (∫1‘(𝑔𝑛)) ≤ (∫2𝐹) ↔ ∀𝑚 ∈ ℕ (∫1‘(𝑔𝑚)) ≤ (∫2𝐹))
207204, 206bitr4i 281 . . . . . . . . 9 (∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))‘𝑚) ≤ (∫2𝐹) ↔ ∀𝑛 ∈ ℕ (∫1‘(𝑔𝑛)) ≤ (∫2𝐹))
208200, 207sylibr 237 . . . . . . . 8 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))‘𝑚) ≤ (∫2𝐹))
209 ffn 6505 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))) Fn ℕ)
210 breq1 5056 . . . . . . . . . 10 (𝑧 = ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))‘𝑚) → (𝑧 ≤ (∫2𝐹) ↔ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))‘𝑚) ≤ (∫2𝐹)))
211210ralrn 6847 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))𝑧 ≤ (∫2𝐹) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))‘𝑚) ≤ (∫2𝐹)))
21278, 209, 2113syl 18 . . . . . . . 8 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))𝑧 ≤ (∫2𝐹) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))‘𝑚) ≤ (∫2𝐹)))
213208, 212mpbird 260 . . . . . . 7 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))𝑧 ≤ (∫2𝐹))
214 supxrleub 12718 . . . . . . . 8 ((ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))) ⊆ ℝ* ∧ (∫2𝐹) ∈ ℝ*) → (sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < ) ≤ (∫2𝐹) ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))𝑧 ≤ (∫2𝐹)))
21581, 73, 214syl2anc 587 . . . . . . 7 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → (sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < ) ≤ (∫2𝐹) ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛)))𝑧 ≤ (∫2𝐹)))
216213, 215mpbird 260 . . . . . 6 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < ) ≤ (∫2𝐹))
21773, 83, 193, 216xrletrid 12547 . . . . 5 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → (∫2𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < ))
21869, 72, 2173jca 1125 . . . 4 ((𝐹:ℝ⟶(0[,]+∞) ∧ (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛))))) → (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∘r𝐹 ∧ (∫2𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < )))
219218ex 416 . . 3 (𝐹:ℝ⟶(0[,]+∞) → ((𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛)))) → (𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∘r𝐹 ∧ (∫2𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < ))))
220219eximdv 1919 . 2 (𝐹:ℝ⟶(0[,]+∞) → (∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔𝑛) ∘r𝐹 ∧ if((∫2𝐹) = +∞, 𝑛, ((∫2𝐹) − (1 / 𝑛))) < (∫1‘(𝑔𝑛)))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∘r𝐹 ∧ (∫2𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < ))))
22168, 220mpd 15 1 (𝐹:ℝ⟶(0[,]+∞) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∘r𝐹 ∧ (∫2𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔𝑛))), ℝ*, < )))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ w3o 1083   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2115   ≠ wne 3014  ∀wral 3133  ∃wrex 3134   ⊆ wss 3919  ∅c0 4276  ifcif 4450   class class class wbr 5053   ↦ cmpt 5133  dom cdm 5543  ran crn 5544   Fn wfn 6340  ⟶wf 6341  ‘cfv 6345  (class class class)co 7151   ∘r cofr 7404   ↑m cmap 8404  supcsup 8903  ℝcr 10536  0cc0 10537  1c1 10538  +∞cpnf 10672  -∞cmnf 10673  ℝ*cxr 10674   < clt 10675   ≤ cle 10676   − cmin 10870   / cdiv 11297  ℕcn 11636  ℝ+crp 12388  [,]cicc 12740  ∫1citg1 24228  ∫2citg2 24229 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457  ax-inf2 9103  ax-cc 9857  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614  ax-pre-sup 10615 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-se 5503  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6137  df-ord 6183  df-on 6184  df-lim 6185  df-suc 6186  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-f1 6350  df-fo 6351  df-f1o 6352  df-fv 6353  df-isom 6354  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7405  df-ofr 7406  df-om 7577  df-1st 7686  df-2nd 7687  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-2o 8101  df-oadd 8104  df-er 8287  df-map 8406  df-pm 8407  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-sup 8905  df-inf 8906  df-oi 8973  df-dju 9329  df-card 9367  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298  df-nn 11637  df-2 11699  df-3 11700  df-n0 11897  df-z 11981  df-uz 12243  df-q 12348  df-rp 12389  df-xadd 12507  df-ioo 12741  df-ico 12743  df-icc 12744  df-fz 12897  df-fzo 13040  df-fl 13168  df-seq 13376  df-exp 13437  df-hash 13698  df-cj 14460  df-re 14461  df-im 14462  df-sqrt 14596  df-abs 14597  df-clim 14847  df-sum 15045  df-xmet 20093  df-met 20094  df-ovol 24077  df-vol 24078  df-mbf 24232  df-itg1 24233  df-itg2 24234 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator