MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2seq Structured version   Visualization version   GIF version
Theorem itg2seq 25622
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 25635, 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 12220 . . . . . . . . . . . 12 (𝑛 ∈ β„• β†’ 𝑛 ∈ ℝ)
21ad2antlr 724 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ 𝑛 ∈ ℝ)
32ltpnfd 13104 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ 𝑛 < +∞)
4 iftrue 4529 . . . . . . . . . . 11 ((∫2β€˜πΉ) = +∞ β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = 𝑛)
54adantl 481 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = 𝑛)
6 simpr 484 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ (∫2β€˜πΉ) = +∞)
73, 5, 63brtr4d 5173 . . . . . . . . 9 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ))
8 iffalse 4532 . . . . . . . . . . 11 (Β¬ (∫2β€˜πΉ) = +∞ β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))
98adantl 481 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))
10 itg2cl 25612 . . . . . . . . . . . . . . 15 (𝐹:β„βŸΆ(0[,]+∞) β†’ (∫2β€˜πΉ) ∈ ℝ*)
11 xrrebnd 13150 . . . . . . . . . . . . . . 15 ((∫2β€˜πΉ) ∈ ℝ* β†’ ((∫2β€˜πΉ) ∈ ℝ ↔ (-∞ < (∫2β€˜πΉ) ∧ (∫2β€˜πΉ) < +∞)))
1210, 11syl 17 . . . . . . . . . . . . . 14 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((∫2β€˜πΉ) ∈ ℝ ↔ (-∞ < (∫2β€˜πΉ) ∧ (∫2β€˜πΉ) < +∞)))
13 itg2ge0 25615 . . . . . . . . . . . . . . . 16 (𝐹:β„βŸΆ(0[,]+∞) β†’ 0 ≀ (∫2β€˜πΉ))
14 mnflt0 13108 . . . . . . . . . . . . . . . . 17 -∞ < 0
15 mnfxr 11272 . . . . . . . . . . . . . . . . . 18 -∞ ∈ ℝ*
16 0xr 11262 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ*
17 xrltletr 13139 . . . . . . . . . . . . . . . . . 18 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (∫2β€˜πΉ) ∈ ℝ*) β†’ ((-∞ < 0 ∧ 0 ≀ (∫2β€˜πΉ)) β†’ -∞ < (∫2β€˜πΉ)))
1815, 16, 10, 17mp3an12i 1461 . . . . . . . . . . . . . . . . 17 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((-∞ < 0 ∧ 0 ≀ (∫2β€˜πΉ)) β†’ -∞ < (∫2β€˜πΉ)))
1914, 18mpani 693 . . . . . . . . . . . . . . . 16 (𝐹:β„βŸΆ(0[,]+∞) β†’ (0 ≀ (∫2β€˜πΉ) β†’ -∞ < (∫2β€˜πΉ)))
2013, 19mpd 15 . . . . . . . . . . . . . . 15 (𝐹:β„βŸΆ(0[,]+∞) β†’ -∞ < (∫2β€˜πΉ))
2120biantrurd 532 . . . . . . . . . . . . . 14 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((∫2β€˜πΉ) < +∞ ↔ (-∞ < (∫2β€˜πΉ) ∧ (∫2β€˜πΉ) < +∞)))
22 nltpnft 13146 . . . . . . . . . . . . . . . 16 ((∫2β€˜πΉ) ∈ ℝ* β†’ ((∫2β€˜πΉ) = +∞ ↔ Β¬ (∫2β€˜πΉ) < +∞))
2310, 22syl 17 . . . . . . . . . . . . . . 15 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((∫2β€˜πΉ) = +∞ ↔ Β¬ (∫2β€˜πΉ) < +∞))
2423con2bid 354 . . . . . . . . . . . . . 14 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((∫2β€˜πΉ) < +∞ ↔ Β¬ (∫2β€˜πΉ) = +∞))
2512, 21, 243bitr2rd 308 . . . . . . . . . . . . 13 (𝐹:β„βŸΆ(0[,]+∞) β†’ (Β¬ (∫2β€˜πΉ) = +∞ ↔ (∫2β€˜πΉ) ∈ ℝ))
2625biimpa 476 . . . . . . . . . . . 12 ((𝐹:β„βŸΆ(0[,]+∞) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (∫2β€˜πΉ) ∈ ℝ)
2726adantlr 712 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (∫2β€˜πΉ) ∈ ℝ)
28 nnrp 12988 . . . . . . . . . . . . 13 (𝑛 ∈ β„• β†’ 𝑛 ∈ ℝ+)
2928rpreccld 13029 . . . . . . . . . . . 12 (𝑛 ∈ β„• β†’ (1 / 𝑛) ∈ ℝ+)
3029ad2antlr 724 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (1 / 𝑛) ∈ ℝ+)
3127, 30ltsubrpd 13051 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)) < (∫2β€˜πΉ))
329, 31eqbrtrd 5163 . . . . . . . . 9 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ))
337, 32pm2.61dan 810 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ))
34 nnrecre 12255 . . . . . . . . . . . . 13 (𝑛 ∈ β„• β†’ (1 / 𝑛) ∈ ℝ)
3534ad2antlr 724 . . . . . . . . . . . 12 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (1 / 𝑛) ∈ ℝ)
3627, 35resubcld 11643 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)) ∈ ℝ)
372, 36ifclda 4558 . . . . . . . . . 10 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ)
3837rexrd 11265 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*)
3910adantr 480 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ (∫2β€˜πΉ) ∈ ℝ*)
40 xrltnle 11282 . . . . . . . . 9 ((if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ* ∧ (∫2β€˜πΉ) ∈ ℝ*) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ) ↔ Β¬ (∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
4138, 39, 40syl2anc 583 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ) ↔ Β¬ (∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
4233, 41mpbid 231 . . . . . . 7 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ Β¬ (∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
43 itg2leub 25614 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*) β†’ ((∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ βˆ€π‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 β†’ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))))
4438, 43syldan 590 . . . . . . 7 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ ((∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ βˆ€π‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 β†’ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))))
4542, 44mtbid 324 . . . . . 6 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ Β¬ βˆ€π‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 β†’ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
46 rexanali 3096 . . . . . 6 (βˆƒπ‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 ∧ Β¬ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))) ↔ Β¬ βˆ€π‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 β†’ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
4745, 46sylibr 233 . . . . 5 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ βˆƒπ‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 ∧ Β¬ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
48 itg1cl 25564 . . . . . . . 8 (𝑓 ∈ dom ∫1 β†’ (∫1β€˜π‘“) ∈ ℝ)
49 ltnle 11294 . . . . . . . 8 ((if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ ∧ (∫1β€˜π‘“) ∈ ℝ) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“) ↔ Β¬ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
5037, 48, 49syl2an 595 . . . . . . 7 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ 𝑓 ∈ dom ∫1) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“) ↔ Β¬ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
5150anbi2d 628 . . . . . 6 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ 𝑓 ∈ dom ∫1) β†’ ((𝑓 ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“)) ↔ (𝑓 ∘r ≀ 𝐹 ∧ Β¬ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))))
5251rexbidva 3170 . . . . 5 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ (βˆƒπ‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“)) ↔ βˆƒπ‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 ∧ Β¬ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))))
5347, 52mpbird 257 . . . 4 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ βˆƒπ‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“)))
5453ralrimiva 3140 . . 3 (𝐹:β„βŸΆ(0[,]+∞) β†’ βˆ€π‘› ∈ β„• βˆƒπ‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“)))
55 ovex 7437 . . . . 5 (ℝ ↑m ℝ) ∈ V
56 i1ff 25555 . . . . . . 7 (π‘₯ ∈ dom ∫1 β†’ π‘₯:β„βŸΆβ„)
57 reex 11200 . . . . . . . 8 ℝ ∈ V
5857, 57elmap 8864 . . . . . . 7 (π‘₯ ∈ (ℝ ↑m ℝ) ↔ π‘₯:β„βŸΆβ„)
5956, 58sylibr 233 . . . . . 6 (π‘₯ ∈ dom ∫1 β†’ π‘₯ ∈ (ℝ ↑m ℝ))
6059ssriv 3981 . . . . 5 dom ∫1 βŠ† (ℝ ↑m ℝ)
6155, 60ssexi 5315 . . . 4 dom ∫1 ∈ V
62 nnenom 13948 . . . 4 β„• β‰ˆ Ο‰
63 breq1 5144 . . . . 5 (𝑓 = (π‘”β€˜π‘›) β†’ (𝑓 ∘r ≀ 𝐹 ↔ (π‘”β€˜π‘›) ∘r ≀ 𝐹))
64 fveq2 6884 . . . . . 6 (𝑓 = (π‘”β€˜π‘›) β†’ (∫1β€˜π‘“) = (∫1β€˜(π‘”β€˜π‘›)))
6564breq2d 5153 . . . . 5 (𝑓 = (π‘”β€˜π‘›) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“) ↔ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))
6663, 65anbi12d 630 . . . 4 (𝑓 = (π‘”β€˜π‘›) β†’ ((𝑓 ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“)) ↔ ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›)))))
6761, 62, 66axcc4 10433 . . 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 768 . . . . 5 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ 𝑔:β„•βŸΆdom ∫1)
70 simpl 482 . . . . . . 7 (((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ (π‘”β€˜π‘›) ∘r ≀ 𝐹)
7170ralimi 3077 . . . . . 6 (βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ βˆ€π‘› ∈ β„• (π‘”β€˜π‘›) ∘r ≀ 𝐹)
7271ad2antll 726 . . . . 5 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘› ∈ β„• (π‘”β€˜π‘›) ∘r ≀ 𝐹)
7310adantr 480 . . . . . 6 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (∫2β€˜πΉ) ∈ ℝ*)
74 ffvelcdm 7076 . . . . . . . . . . . 12 ((𝑔:β„•βŸΆdom ∫1 ∧ 𝑛 ∈ β„•) β†’ (π‘”β€˜π‘›) ∈ dom ∫1)
75 itg1cl 25564 . . . . . . . . . . . 12 ((π‘”β€˜π‘›) ∈ dom ∫1 β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ)
7674, 75syl 17 . . . . . . . . . . 11 ((𝑔:β„•βŸΆdom ∫1 ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ)
7776fmpttd 7109 . . . . . . . . . 10 (𝑔:β„•βŸΆdom ∫1 β†’ (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))):β„•βŸΆβ„)
7877ad2antrl 725 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))):β„•βŸΆβ„)
7978frnd 6718 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ)
80 ressxr 11259 . . . . . . . 8 ℝ βŠ† ℝ*
8179, 80sstrdi 3989 . . . . . . 7 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ*)
82 supxrcl 13297 . . . . . . 7 (ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ* β†’ sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ∈ ℝ*)
8381, 82syl 17 . . . . . 6 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ∈ ℝ*)
8438adantlr 712 . . . . . . . . . . . . 13 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*)
8576adantll 711 . . . . . . . . . . . . . 14 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ)
8685rexrd 11265 . . . . . . . . . . . . 13 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ*)
87 xrltle 13131 . . . . . . . . . . . . 13 ((if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ* ∧ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ*) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›)) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ (∫1β€˜(π‘”β€˜π‘›))))
8884, 86, 87syl2anc 583 . . . . . . . . . . . 12 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›)) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ (∫1β€˜(π‘”β€˜π‘›))))
89 2fveq3 6889 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘š β†’ (∫1β€˜(π‘”β€˜π‘›)) = (∫1β€˜(π‘”β€˜π‘š)))
9089cbvmptv 5254 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) = (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))
9190rneqi 5929 . . . . . . . . . . . . . . 15 ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) = ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))
9277adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))):β„•βŸΆβ„)
9392frnd 6718 . . . . . . . . . . . . . . . . 17 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ)
9493, 80sstrdi 3989 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ*)
9594adantr 480 . . . . . . . . . . . . . . 15 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ*)
9691, 95eqsstrrid 4026 . . . . . . . . . . . . . 14 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) βŠ† ℝ*)
97 2fveq3 6889 . . . . . . . . . . . . . . . . 17 (π‘š = 𝑛 β†’ (∫1β€˜(π‘”β€˜π‘š)) = (∫1β€˜(π‘”β€˜π‘›)))
98 eqid 2726 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) = (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))
99 fvex 6897 . . . . . . . . . . . . . . . . 17 (∫1β€˜(π‘”β€˜π‘›)) ∈ V
10097, 98, 99fvmpt 6991 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))β€˜π‘›) = (∫1β€˜(π‘”β€˜π‘›)))
101 fvex 6897 . . . . . . . . . . . . . . . . . 18 (∫1β€˜(π‘”β€˜π‘š)) ∈ V
102101, 98fnmpti 6686 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) Fn β„•
103 fnfvelrn 7075 . . . . . . . . . . . . . . . . 17 (((π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) Fn β„• ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))β€˜π‘›) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))))
104102, 103mpan 687 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))β€˜π‘›) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))))
105100, 104eqeltrrd 2828 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„• β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))))
106105adantl 481 . . . . . . . . . . . . . 14 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))))
107 supxrub 13306 . . . . . . . . . . . . . 14 ((ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) βŠ† ℝ* ∧ (∫1β€˜(π‘”β€˜π‘›)) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))) β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ))
10896, 106, 107syl2anc 583 . . . . . . . . . . . . 13 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ))
10991supeq1i 9441 . . . . . . . . . . . . . . 15 sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )
11095, 82syl 17 . . . . . . . . . . . . . . 15 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ∈ ℝ*)
111109, 110eqeltrrid 2832 . . . . . . . . . . . . . 14 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) ∈ ℝ*)
112 xrletr 13140 . . . . . . . . . . . . . 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 691 . . . . . . . . . . . 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 490 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
117116ralimdva 3161 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ (βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
118117impr 454 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ))
119 breq2 5145 . . . . . . . . . . 11 (π‘₯ = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ ↔ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
120119ralbidv 3171 . . . . . . . . . 10 (π‘₯ = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) β†’ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ ↔ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
121 breq2 5145 . . . . . . . . . 10 (π‘₯ = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) β†’ ((∫2β€˜πΉ) ≀ π‘₯ ↔ (∫2β€˜πΉ) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
122120, 121imbi12d 344 . . . . . . . . 9 (π‘₯ = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) β†’ ((βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯) ↔ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) β†’ (∫2β€˜πΉ) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ))))
123 elxr 13099 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ* ↔ (π‘₯ ∈ ℝ ∨ π‘₯ = +∞ ∨ π‘₯ = -∞))
124 simplrl 774 . . . . . . . . . . . . . . . . . . 19 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ π‘₯ ∈ ℝ)
125 arch 12470 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ ℝ β†’ βˆƒπ‘› ∈ β„• π‘₯ < 𝑛)
126124, 125syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ βˆƒπ‘› ∈ β„• π‘₯ < 𝑛)
1274adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = 𝑛)
128127breq2d 5153 . . . . . . . . . . . . . . . . . . 19 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ (π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ π‘₯ < 𝑛))
129128rexbidv 3172 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ (βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ βˆƒπ‘› ∈ β„• π‘₯ < 𝑛))
130126, 129mpbird 257 . . . . . . . . . . . . . . . . 17 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
13126adantlr 712 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (∫2β€˜πΉ) ∈ ℝ)
132 simplrl 774 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ π‘₯ ∈ ℝ)
133131, 132resubcld 11643 . . . . . . . . . . . . . . . . . . 19 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ ((∫2β€˜πΉ) βˆ’ π‘₯) ∈ ℝ)
134 simplrr 775 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ π‘₯ < (∫2β€˜πΉ))
135132, 131posdifd 11802 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (π‘₯ < (∫2β€˜πΉ) ↔ 0 < ((∫2β€˜πΉ) βˆ’ π‘₯)))
136134, 135mpbid 231 . . . . . . . . . . . . . . . . . . 19 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ 0 < ((∫2β€˜πΉ) βˆ’ π‘₯))
137 nnrecl 12471 . . . . . . . . . . . . . . . . . . 19 ((((∫2β€˜πΉ) βˆ’ π‘₯) ∈ ℝ ∧ 0 < ((∫2β€˜πΉ) βˆ’ π‘₯)) β†’ βˆƒπ‘› ∈ β„• (1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯))
138133, 136, 137syl2anc 583 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ βˆƒπ‘› ∈ β„• (1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯))
13934adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ (1 / 𝑛) ∈ ℝ)
140131adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ (∫2β€˜πΉ) ∈ ℝ)
141132adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ π‘₯ ∈ ℝ)
142 ltsub13 11696 . . . . . . . . . . . . . . . . . . . . 21 (((1 / 𝑛) ∈ ℝ ∧ (∫2β€˜πΉ) ∈ ℝ ∧ π‘₯ ∈ ℝ) β†’ ((1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯) ↔ π‘₯ < ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
143139, 140, 141, 142syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ ((1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯) ↔ π‘₯ < ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
1448ad2antlr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))
145144breq2d 5153 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ (π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ π‘₯ < ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
146143, 145bitr4d 282 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ ((1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯) ↔ π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
147146rexbidva 3170 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (βˆƒπ‘› ∈ β„• (1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯) ↔ βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
148138, 147mpbid 231 . . . . . . . . . . . . . . . . 17 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
149130, 148pm2.61dan 810 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) β†’ βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
150149expr 456 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ < (∫2β€˜πΉ) β†’ βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
151 rexr 11261 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ β†’ π‘₯ ∈ ℝ*)
152 xrltnle 11282 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ ℝ* ∧ (∫2β€˜πΉ) ∈ ℝ*) β†’ (π‘₯ < (∫2β€˜πΉ) ↔ Β¬ (∫2β€˜πΉ) ≀ π‘₯))
153151, 10, 152syl2anr 596 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ < (∫2β€˜πΉ) ↔ Β¬ (∫2β€˜πΉ) ≀ π‘₯))
154151ad2antlr 724 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) ∧ 𝑛 ∈ β„•) β†’ π‘₯ ∈ ℝ*)
15538adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*)
156 xrltnle 11282 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ ℝ* ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*) β†’ (π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
157154, 155, 156syl2anc 583 . . . . . . . . . . . . . . . . 17 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) ∧ 𝑛 ∈ β„•) β†’ (π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
158157rexbidva 3170 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ βˆƒπ‘› ∈ β„• Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
159 rexnal 3094 . . . . . . . . . . . . . . . 16 (βˆƒπ‘› ∈ β„• Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ ↔ Β¬ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯)
160158, 159bitrdi 287 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ Β¬ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
161150, 153, 1603imtr3d 293 . . . . . . . . . . . . . 14 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (Β¬ (∫2β€˜πΉ) ≀ π‘₯ β†’ Β¬ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
162161con4d 115 . . . . . . . . . . . . 13 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
16310adantr 480 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ (∫2β€˜πΉ) ∈ ℝ*)
164 pnfge 13113 . . . . . . . . . . . . . . . 16 ((∫2β€˜πΉ) ∈ ℝ* β†’ (∫2β€˜πΉ) ≀ +∞)
165163, 164syl 17 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ (∫2β€˜πΉ) ≀ +∞)
166 simpr 484 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ π‘₯ = +∞)
167165, 166breqtrrd 5169 . . . . . . . . . . . . . 14 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ (∫2β€˜πΉ) ≀ π‘₯)
168167a1d 25 . . . . . . . . . . . . 13 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
169 1nn 12224 . . . . . . . . . . . . . . . 16 1 ∈ β„•
170169ne0ii 4332 . . . . . . . . . . . . . . 15 β„• β‰  βˆ…
171 r19.2z 4489 . . . . . . . . . . . . . . 15 ((β„• β‰  βˆ… ∧ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯) β†’ βˆƒπ‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯)
172170, 171mpan 687 . . . . . . . . . . . . . 14 (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ βˆƒπ‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯)
17337adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = -∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ)
174 mnflt 13106 . . . . . . . . . . . . . . . . . . 19 (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ β†’ -∞ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
175 rexr 11261 . . . . . . . . . . . . . . . . . . . 20 (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*)
176 xrltnle 11282 . . . . . . . . . . . . . . . . . . . 20 ((-∞ ∈ ℝ* ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*) β†’ (-∞ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ -∞))
17715, 175, 176sylancr 586 . . . . . . . . . . . . . . . . . . 19 (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ β†’ (-∞ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ -∞))
178174, 177mpbid 231 . . . . . . . . . . . . . . . . . 18 (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ β†’ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ -∞)
179173, 178syl 17 . . . . . . . . . . . . . . . . 17 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = -∞) ∧ 𝑛 ∈ β„•) β†’ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ -∞)
180 simplr 766 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = -∞) ∧ 𝑛 ∈ β„•) β†’ π‘₯ = -∞)
181180breq2d 5153 . . . . . . . . . . . . . . . . 17 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = -∞) ∧ 𝑛 ∈ β„•) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ ↔ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ -∞))
182179, 181mtbird 325 . . . . . . . . . . . . . . . 16 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = -∞) ∧ 𝑛 ∈ β„•) β†’ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯)
183182nrexdv 3143 . . . . . . . . . . . . . . 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 593 . . . . . . . . . . 11 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ*) β†’ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
188187ralrimiva 3140 . . . . . . . . . 10 (𝐹:β„βŸΆ(0[,]+∞) β†’ βˆ€π‘₯ ∈ ℝ* (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
189188adantr 480 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘₯ ∈ ℝ* (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
190109, 83eqeltrrid 2832 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) ∈ ℝ*)
191122, 189, 190rspcdva 3607 . . . . . . . 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 5183 . . . . . 6 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (∫2β€˜πΉ) ≀ sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ))
194 itg2ub 25613 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘”β€˜π‘›) ∈ dom ∫1 ∧ (π‘”β€˜π‘›) ∘r ≀ 𝐹) β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ))
1951943expia 1118 . . . . . . . . . . . . . 14 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘”β€˜π‘›) ∈ dom ∫1) β†’ ((π‘”β€˜π‘›) ∘r ≀ 𝐹 β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
19674, 195sylan2 592 . . . . . . . . . . . . 13 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ 𝑛 ∈ β„•)) β†’ ((π‘”β€˜π‘›) ∘r ≀ 𝐹 β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
197196anassrs 467 . . . . . . . . . . . 12 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ ((π‘”β€˜π‘›) ∘r ≀ 𝐹 β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
198197adantrd 491 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
199198ralimdva 3161 . . . . . . . . . 10 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ (βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ βˆ€π‘› ∈ β„• (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
200199impr 454 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘› ∈ β„• (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ))
201 eqid 2726 . . . . . . . . . . . . 13 (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) = (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))
20289, 201, 101fvmpt 6991 . . . . . . . . . . . 12 (π‘š ∈ β„• β†’ ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) = (∫1β€˜(π‘”β€˜π‘š)))
203202breq1d 5151 . . . . . . . . . . 11 (π‘š ∈ β„• β†’ (((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ) ↔ (∫1β€˜(π‘”β€˜π‘š)) ≀ (∫2β€˜πΉ)))
204203ralbiia 3085 . . . . . . . . . 10 (βˆ€π‘š ∈ β„• ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ) ↔ βˆ€π‘š ∈ β„• (∫1β€˜(π‘”β€˜π‘š)) ≀ (∫2β€˜πΉ))
20589breq1d 5151 . . . . . . . . . . 11 (𝑛 = π‘š β†’ ((∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ) ↔ (∫1β€˜(π‘”β€˜π‘š)) ≀ (∫2β€˜πΉ)))
206205cbvralvw 3228 . . . . . . . . . 10 (βˆ€π‘› ∈ β„• (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ) ↔ βˆ€π‘š ∈ β„• (∫1β€˜(π‘”β€˜π‘š)) ≀ (∫2β€˜πΉ))
207204, 206bitr4i 278 . . . . . . . . 9 (βˆ€π‘š ∈ β„• ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ) ↔ βˆ€π‘› ∈ β„• (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ))
208200, 207sylibr 233 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘š ∈ β„• ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ))
209 ffn 6710 . . . . . . . . 9 ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))):β„•βŸΆβ„ β†’ (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) Fn β„•)
210 breq1 5144 . . . . . . . . . 10 (𝑧 = ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) β†’ (𝑧 ≀ (∫2β€˜πΉ) ↔ ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ)))
211210ralrn 7082 . . . . . . . . 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 257 . . . . . . 7 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))𝑧 ≀ (∫2β€˜πΉ))
214 supxrleub 13308 . . . . . . . 8 ((ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ* ∧ (∫2β€˜πΉ) ∈ ℝ*) β†’ (sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ≀ (∫2β€˜πΉ) ↔ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))𝑧 ≀ (∫2β€˜πΉ)))
21581, 73, 214syl2anc 583 . . . . . . 7 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ≀ (∫2β€˜πΉ) ↔ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))𝑧 ≀ (∫2β€˜πΉ)))
216213, 215mpbird 257 . . . . . 6 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ≀ (∫2β€˜πΉ))
21773, 83, 193, 216xrletrid 13137 . . . . 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 412 . . 3 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›)))) β†’ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• (π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ (∫2β€˜πΉ) = sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ))))
220219eximdv 1912 . 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 205   ∧ wa 395   ∨ w3o 1083   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098   β‰  wne 2934  βˆ€wral 3055  βˆƒwrex 3064   βŠ† wss 3943  βˆ…c0 4317  ifcif 4523   class class class wbr 5141   ↦ cmpt 5224  dom cdm 5669  ran crn 5670   Fn wfn 6531  βŸΆwf 6532  β€˜cfv 6536  (class class class)co 7404   ∘r cofr 7665   ↑m cmap 8819  supcsup 9434  β„cr 11108  0cc0 11109  1c1 11110  +∞cpnf 11246  -∞cmnf 11247  β„*cxr 11248   < clt 11249   ≀ cle 11250   βˆ’ cmin 11445   / cdiv 11872  β„•cn 12213  β„+crp 12977  [,]cicc 13330  βˆ«1citg1 25494  βˆ«2citg2 25495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-inf2 9635  ax-cc 10429  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7666  df-ofr 7667  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-rdg 8408  df-1o 8464  df-2o 8465  df-er 8702  df-map 8821  df-pm 8822  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-sup 9436  df-inf 9437  df-oi 9504  df-dju 9895  df-card 9933  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11447  df-neg 11448  df-div 11873  df-nn 12214  df-2 12276  df-3 12277  df-n0 12474  df-z 12560  df-uz 12824  df-q 12934  df-rp 12978  df-xadd 13096  df-ioo 13331  df-ico 13333  df-icc 13334  df-fz 13488  df-fzo 13631  df-fl 13760  df-seq 13970  df-exp 14030  df-hash 14293  df-cj 15049  df-re 15050  df-im 15051  df-sqrt 15185  df-abs 15186  df-clim 15435  df-sum 15636  df-xmet 21228  df-met 21229  df-ovol 25343  df-vol 25344  df-mbf 25498  df-itg1 25499  df-itg2 25500
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator