MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2seq Structured version   Visualization version   GIF version
Theorem itg2seq 25692
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 25705, 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 12257 . . . . . . . . . . . 12 (𝑛 ∈ β„• β†’ 𝑛 ∈ ℝ)
21ad2antlr 725 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ 𝑛 ∈ ℝ)
32ltpnfd 13141 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ 𝑛 < +∞)
4 iftrue 4538 . . . . . . . . . . 11 ((∫2β€˜πΉ) = +∞ β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = 𝑛)
54adantl 480 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = 𝑛)
6 simpr 483 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ (∫2β€˜πΉ) = +∞)
73, 5, 63brtr4d 5184 . . . . . . . . 9 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ))
8 iffalse 4541 . . . . . . . . . . 11 (Β¬ (∫2β€˜πΉ) = +∞ β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))
98adantl 480 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))
10 itg2cl 25682 . . . . . . . . . . . . . . 15 (𝐹:β„βŸΆ(0[,]+∞) β†’ (∫2β€˜πΉ) ∈ ℝ*)
11 xrrebnd 13187 . . . . . . . . . . . . . . 15 ((∫2β€˜πΉ) ∈ ℝ* β†’ ((∫2β€˜πΉ) ∈ ℝ ↔ (-∞ < (∫2β€˜πΉ) ∧ (∫2β€˜πΉ) < +∞)))
1210, 11syl 17 . . . . . . . . . . . . . 14 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((∫2β€˜πΉ) ∈ ℝ ↔ (-∞ < (∫2β€˜πΉ) ∧ (∫2β€˜πΉ) < +∞)))
13 itg2ge0 25685 . . . . . . . . . . . . . . . 16 (𝐹:β„βŸΆ(0[,]+∞) β†’ 0 ≀ (∫2β€˜πΉ))
14 mnflt0 13145 . . . . . . . . . . . . . . . . 17 -∞ < 0
15 mnfxr 11309 . . . . . . . . . . . . . . . . . 18 -∞ ∈ ℝ*
16 0xr 11299 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ*
17 xrltletr 13176 . . . . . . . . . . . . . . . . . 18 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (∫2β€˜πΉ) ∈ ℝ*) β†’ ((-∞ < 0 ∧ 0 ≀ (∫2β€˜πΉ)) β†’ -∞ < (∫2β€˜πΉ)))
1815, 16, 10, 17mp3an12i 1461 . . . . . . . . . . . . . . . . 17 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((-∞ < 0 ∧ 0 ≀ (∫2β€˜πΉ)) β†’ -∞ < (∫2β€˜πΉ)))
1914, 18mpani 694 . . . . . . . . . . . . . . . 16 (𝐹:β„βŸΆ(0[,]+∞) β†’ (0 ≀ (∫2β€˜πΉ) β†’ -∞ < (∫2β€˜πΉ)))
2013, 19mpd 15 . . . . . . . . . . . . . . 15 (𝐹:β„βŸΆ(0[,]+∞) β†’ -∞ < (∫2β€˜πΉ))
2120biantrurd 531 . . . . . . . . . . . . . 14 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((∫2β€˜πΉ) < +∞ ↔ (-∞ < (∫2β€˜πΉ) ∧ (∫2β€˜πΉ) < +∞)))
22 nltpnft 13183 . . . . . . . . . . . . . . . 16 ((∫2β€˜πΉ) ∈ ℝ* β†’ ((∫2β€˜πΉ) = +∞ ↔ Β¬ (∫2β€˜πΉ) < +∞))
2310, 22syl 17 . . . . . . . . . . . . . . 15 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((∫2β€˜πΉ) = +∞ ↔ Β¬ (∫2β€˜πΉ) < +∞))
2423con2bid 353 . . . . . . . . . . . . . 14 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((∫2β€˜πΉ) < +∞ ↔ Β¬ (∫2β€˜πΉ) = +∞))
2512, 21, 243bitr2rd 307 . . . . . . . . . . . . 13 (𝐹:β„βŸΆ(0[,]+∞) β†’ (Β¬ (∫2β€˜πΉ) = +∞ ↔ (∫2β€˜πΉ) ∈ ℝ))
2625biimpa 475 . . . . . . . . . . . 12 ((𝐹:β„βŸΆ(0[,]+∞) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (∫2β€˜πΉ) ∈ ℝ)
2726adantlr 713 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (∫2β€˜πΉ) ∈ ℝ)
28 nnrp 13025 . . . . . . . . . . . . 13 (𝑛 ∈ β„• β†’ 𝑛 ∈ ℝ+)
2928rpreccld 13066 . . . . . . . . . . . 12 (𝑛 ∈ β„• β†’ (1 / 𝑛) ∈ ℝ+)
3029ad2antlr 725 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (1 / 𝑛) ∈ ℝ+)
3127, 30ltsubrpd 13088 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)) < (∫2β€˜πΉ))
329, 31eqbrtrd 5174 . . . . . . . . 9 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ))
337, 32pm2.61dan 811 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ))
34 nnrecre 12292 . . . . . . . . . . . . 13 (𝑛 ∈ β„• β†’ (1 / 𝑛) ∈ ℝ)
3534ad2antlr 725 . . . . . . . . . . . 12 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (1 / 𝑛) ∈ ℝ)
3627, 35resubcld 11680 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)) ∈ ℝ)
372, 36ifclda 4567 . . . . . . . . . 10 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ)
3837rexrd 11302 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*)
3910adantr 479 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ (∫2β€˜πΉ) ∈ ℝ*)
40 xrltnle 11319 . . . . . . . . 9 ((if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ* ∧ (∫2β€˜πΉ) ∈ ℝ*) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ) ↔ Β¬ (∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
4138, 39, 40syl2anc 582 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ) ↔ Β¬ (∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
4233, 41mpbid 231 . . . . . . 7 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ Β¬ (∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
43 itg2leub 25684 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*) β†’ ((∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ βˆ€π‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 β†’ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))))
4438, 43syldan 589 . . . . . . 7 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ ((∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ βˆ€π‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 β†’ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))))
4542, 44mtbid 323 . . . . . 6 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ Β¬ βˆ€π‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 β†’ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
46 rexanali 3099 . . . . . 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 25634 . . . . . . . 8 (𝑓 ∈ dom ∫1 β†’ (∫1β€˜π‘“) ∈ ℝ)
49 ltnle 11331 . . . . . . . 8 ((if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ ∧ (∫1β€˜π‘“) ∈ ℝ) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“) ↔ Β¬ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
5037, 48, 49syl2an 594 . . . . . . 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 3174 . . . . 5 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ (βˆƒπ‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“)) ↔ βˆƒπ‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 ∧ Β¬ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))))
5347, 52mpbird 256 . . . 4 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ βˆƒπ‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“)))
5453ralrimiva 3143 . . 3 (𝐹:β„βŸΆ(0[,]+∞) β†’ βˆ€π‘› ∈ β„• βˆƒπ‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“)))
55 ovex 7459 . . . . 5 (ℝ ↑m ℝ) ∈ V
56 i1ff 25625 . . . . . . 7 (π‘₯ ∈ dom ∫1 β†’ π‘₯:β„βŸΆβ„)
57 reex 11237 . . . . . . . 8 ℝ ∈ V
5857, 57elmap 8896 . . . . . . 7 (π‘₯ ∈ (ℝ ↑m ℝ) ↔ π‘₯:β„βŸΆβ„)
5956, 58sylibr 233 . . . . . 6 (π‘₯ ∈ dom ∫1 β†’ π‘₯ ∈ (ℝ ↑m ℝ))
6059ssriv 3986 . . . . 5 dom ∫1 βŠ† (ℝ ↑m ℝ)
6155, 60ssexi 5326 . . . 4 dom ∫1 ∈ V
62 nnenom 13985 . . . 4 β„• β‰ˆ Ο‰
63 breq1 5155 . . . . 5 (𝑓 = (π‘”β€˜π‘›) β†’ (𝑓 ∘r ≀ 𝐹 ↔ (π‘”β€˜π‘›) ∘r ≀ 𝐹))
64 fveq2 6902 . . . . . 6 (𝑓 = (π‘”β€˜π‘›) β†’ (∫1β€˜π‘“) = (∫1β€˜(π‘”β€˜π‘›)))
6564breq2d 5164 . . . . 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 10470 . . 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 769 . . . . 5 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ 𝑔:β„•βŸΆdom ∫1)
70 simpl 481 . . . . . . 7 (((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ (π‘”β€˜π‘›) ∘r ≀ 𝐹)
7170ralimi 3080 . . . . . 6 (βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ βˆ€π‘› ∈ β„• (π‘”β€˜π‘›) ∘r ≀ 𝐹)
7271ad2antll 727 . . . . 5 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘› ∈ β„• (π‘”β€˜π‘›) ∘r ≀ 𝐹)
7310adantr 479 . . . . . 6 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (∫2β€˜πΉ) ∈ ℝ*)
74 ffvelcdm 7096 . . . . . . . . . . . 12 ((𝑔:β„•βŸΆdom ∫1 ∧ 𝑛 ∈ β„•) β†’ (π‘”β€˜π‘›) ∈ dom ∫1)
75 itg1cl 25634 . . . . . . . . . . . 12 ((π‘”β€˜π‘›) ∈ dom ∫1 β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ)
7674, 75syl 17 . . . . . . . . . . 11 ((𝑔:β„•βŸΆdom ∫1 ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ)
7776fmpttd 7130 . . . . . . . . . 10 (𝑔:β„•βŸΆdom ∫1 β†’ (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))):β„•βŸΆβ„)
7877ad2antrl 726 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))):β„•βŸΆβ„)
7978frnd 6735 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ)
80 ressxr 11296 . . . . . . . 8 ℝ βŠ† ℝ*
8179, 80sstrdi 3994 . . . . . . 7 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ*)
82 supxrcl 13334 . . . . . . 7 (ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ* β†’ sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ∈ ℝ*)
8381, 82syl 17 . . . . . 6 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ∈ ℝ*)
8438adantlr 713 . . . . . . . . . . . . 13 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*)
8576adantll 712 . . . . . . . . . . . . . 14 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ)
8685rexrd 11302 . . . . . . . . . . . . 13 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ*)
87 xrltle 13168 . . . . . . . . . . . . 13 ((if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ* ∧ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ*) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›)) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ (∫1β€˜(π‘”β€˜π‘›))))
8884, 86, 87syl2anc 582 . . . . . . . . . . . 12 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›)) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ (∫1β€˜(π‘”β€˜π‘›))))
89 2fveq3 6907 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘š β†’ (∫1β€˜(π‘”β€˜π‘›)) = (∫1β€˜(π‘”β€˜π‘š)))
9089cbvmptv 5265 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) = (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))
9190rneqi 5943 . . . . . . . . . . . . . . 15 ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) = ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))
9277adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))):β„•βŸΆβ„)
9392frnd 6735 . . . . . . . . . . . . . . . . 17 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ)
9493, 80sstrdi 3994 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ*)
9594adantr 479 . . . . . . . . . . . . . . 15 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ*)
9691, 95eqsstrrid 4031 . . . . . . . . . . . . . 14 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) βŠ† ℝ*)
97 2fveq3 6907 . . . . . . . . . . . . . . . . 17 (π‘š = 𝑛 β†’ (∫1β€˜(π‘”β€˜π‘š)) = (∫1β€˜(π‘”β€˜π‘›)))
98 eqid 2728 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) = (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))
99 fvex 6915 . . . . . . . . . . . . . . . . 17 (∫1β€˜(π‘”β€˜π‘›)) ∈ V
10097, 98, 99fvmpt 7010 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))β€˜π‘›) = (∫1β€˜(π‘”β€˜π‘›)))
101 fvex 6915 . . . . . . . . . . . . . . . . . 18 (∫1β€˜(π‘”β€˜π‘š)) ∈ V
102101, 98fnmpti 6703 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) Fn β„•
103 fnfvelrn 7095 . . . . . . . . . . . . . . . . 17 (((π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) Fn β„• ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))β€˜π‘›) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))))
104102, 103mpan 688 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))β€˜π‘›) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))))
105100, 104eqeltrrd 2830 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„• β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))))
106105adantl 480 . . . . . . . . . . . . . 14 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))))
107 supxrub 13343 . . . . . . . . . . . . . 14 ((ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) βŠ† ℝ* ∧ (∫1β€˜(π‘”β€˜π‘›)) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))) β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ))
10896, 106, 107syl2anc 582 . . . . . . . . . . . . 13 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ))
10991supeq1i 9478 . . . . . . . . . . . . . . 15 sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )
11095, 82syl 17 . . . . . . . . . . . . . . 15 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ∈ ℝ*)
111109, 110eqeltrrid 2834 . . . . . . . . . . . . . 14 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) ∈ ℝ*)
112 xrletr 13177 . . . . . . . . . . . . . 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 692 . . . . . . . . . . . 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 489 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
117116ralimdva 3164 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ (βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
118117impr 453 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ))
119 breq2 5156 . . . . . . . . . . 11 (π‘₯ = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ ↔ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
120119ralbidv 3175 . . . . . . . . . 10 (π‘₯ = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) β†’ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ ↔ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
121 breq2 5156 . . . . . . . . . 10 (π‘₯ = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) β†’ ((∫2β€˜πΉ) ≀ π‘₯ ↔ (∫2β€˜πΉ) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
122120, 121imbi12d 343 . . . . . . . . 9 (π‘₯ = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) β†’ ((βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯) ↔ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) β†’ (∫2β€˜πΉ) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ))))
123 elxr 13136 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ* ↔ (π‘₯ ∈ ℝ ∨ π‘₯ = +∞ ∨ π‘₯ = -∞))
124 simplrl 775 . . . . . . . . . . . . . . . . . . 19 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ π‘₯ ∈ ℝ)
125 arch 12507 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ ℝ β†’ βˆƒπ‘› ∈ β„• π‘₯ < 𝑛)
126124, 125syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ βˆƒπ‘› ∈ β„• π‘₯ < 𝑛)
1274adantl 480 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = 𝑛)
128127breq2d 5164 . . . . . . . . . . . . . . . . . . 19 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ (π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ π‘₯ < 𝑛))
129128rexbidv 3176 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ (βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ βˆƒπ‘› ∈ β„• π‘₯ < 𝑛))
130126, 129mpbird 256 . . . . . . . . . . . . . . . . 17 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
13126adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (∫2β€˜πΉ) ∈ ℝ)
132 simplrl 775 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ π‘₯ ∈ ℝ)
133131, 132resubcld 11680 . . . . . . . . . . . . . . . . . . 19 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ ((∫2β€˜πΉ) βˆ’ π‘₯) ∈ ℝ)
134 simplrr 776 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ π‘₯ < (∫2β€˜πΉ))
135132, 131posdifd 11839 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (π‘₯ < (∫2β€˜πΉ) ↔ 0 < ((∫2β€˜πΉ) βˆ’ π‘₯)))
136134, 135mpbid 231 . . . . . . . . . . . . . . . . . . 19 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ 0 < ((∫2β€˜πΉ) βˆ’ π‘₯))
137 nnrecl 12508 . . . . . . . . . . . . . . . . . . 19 ((((∫2β€˜πΉ) βˆ’ π‘₯) ∈ ℝ ∧ 0 < ((∫2β€˜πΉ) βˆ’ π‘₯)) β†’ βˆƒπ‘› ∈ β„• (1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯))
138133, 136, 137syl2anc 582 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ βˆƒπ‘› ∈ β„• (1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯))
13934adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ (1 / 𝑛) ∈ ℝ)
140131adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ (∫2β€˜πΉ) ∈ ℝ)
141132adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ π‘₯ ∈ ℝ)
142 ltsub13 11733 . . . . . . . . . . . . . . . . . . . . 21 (((1 / 𝑛) ∈ ℝ ∧ (∫2β€˜πΉ) ∈ ℝ ∧ π‘₯ ∈ ℝ) β†’ ((1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯) ↔ π‘₯ < ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
143139, 140, 141, 142syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ ((1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯) ↔ π‘₯ < ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
1448ad2antlr 725 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))
145144breq2d 5164 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ (π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ π‘₯ < ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
146143, 145bitr4d 281 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ ((1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯) ↔ π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
147146rexbidva 3174 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (βˆƒπ‘› ∈ β„• (1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯) ↔ βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
148138, 147mpbid 231 . . . . . . . . . . . . . . . . 17 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
149130, 148pm2.61dan 811 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) β†’ βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
150149expr 455 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ < (∫2β€˜πΉ) β†’ βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
151 rexr 11298 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ β†’ π‘₯ ∈ ℝ*)
152 xrltnle 11319 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ ℝ* ∧ (∫2β€˜πΉ) ∈ ℝ*) β†’ (π‘₯ < (∫2β€˜πΉ) ↔ Β¬ (∫2β€˜πΉ) ≀ π‘₯))
153151, 10, 152syl2anr 595 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ < (∫2β€˜πΉ) ↔ Β¬ (∫2β€˜πΉ) ≀ π‘₯))
154151ad2antlr 725 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) ∧ 𝑛 ∈ β„•) β†’ π‘₯ ∈ ℝ*)
15538adantlr 713 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*)
156 xrltnle 11319 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ ℝ* ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*) β†’ (π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
157154, 155, 156syl2anc 582 . . . . . . . . . . . . . . . . 17 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) ∧ 𝑛 ∈ β„•) β†’ (π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
158157rexbidva 3174 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ βˆƒπ‘› ∈ β„• Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
159 rexnal 3097 . . . . . . . . . . . . . . . 16 (βˆƒπ‘› ∈ β„• Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ ↔ Β¬ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯)
160158, 159bitrdi 286 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ Β¬ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
161150, 153, 1603imtr3d 292 . . . . . . . . . . . . . 14 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (Β¬ (∫2β€˜πΉ) ≀ π‘₯ β†’ Β¬ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
162161con4d 115 . . . . . . . . . . . . 13 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
16310adantr 479 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ (∫2β€˜πΉ) ∈ ℝ*)
164 pnfge 13150 . . . . . . . . . . . . . . . 16 ((∫2β€˜πΉ) ∈ ℝ* β†’ (∫2β€˜πΉ) ≀ +∞)
165163, 164syl 17 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ (∫2β€˜πΉ) ≀ +∞)
166 simpr 483 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ π‘₯ = +∞)
167165, 166breqtrrd 5180 . . . . . . . . . . . . . 14 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ (∫2β€˜πΉ) ≀ π‘₯)
168167a1d 25 . . . . . . . . . . . . 13 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
169 1nn 12261 . . . . . . . . . . . . . . . 16 1 ∈ β„•
170169ne0ii 4341 . . . . . . . . . . . . . . 15 β„• β‰  βˆ…
171 r19.2z 4498 . . . . . . . . . . . . . . 15 ((β„• β‰  βˆ… ∧ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯) β†’ βˆƒπ‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯)
172170, 171mpan 688 . . . . . . . . . . . . . 14 (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ βˆƒπ‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯)
17337adantlr 713 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = -∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ)
174 mnflt 13143 . . . . . . . . . . . . . . . . . . 19 (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ β†’ -∞ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
175 rexr 11298 . . . . . . . . . . . . . . . . . . . 20 (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*)
176 xrltnle 11319 . . . . . . . . . . . . . . . . . . . 20 ((-∞ ∈ ℝ* ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*) β†’ (-∞ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ -∞))
17715, 175, 176sylancr 585 . . . . . . . . . . . . . . . . . . 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 767 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = -∞) ∧ 𝑛 ∈ β„•) β†’ π‘₯ = -∞)
181180breq2d 5164 . . . . . . . . . . . . . . . . 17 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = -∞) ∧ 𝑛 ∈ β„•) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ ↔ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ -∞))
182179, 181mtbird 324 . . . . . . . . . . . . . . . 16 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = -∞) ∧ 𝑛 ∈ β„•) β†’ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯)
183182nrexdv 3146 . . . . . . . . . . . . . . 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 592 . . . . . . . . . . 11 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ*) β†’ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
188187ralrimiva 3143 . . . . . . . . . 10 (𝐹:β„βŸΆ(0[,]+∞) β†’ βˆ€π‘₯ ∈ ℝ* (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
189188adantr 479 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘₯ ∈ ℝ* (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
190109, 83eqeltrrid 2834 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) ∈ ℝ*)
191122, 189, 190rspcdva 3612 . . . . . . . 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 5194 . . . . . 6 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (∫2β€˜πΉ) ≀ sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ))
194 itg2ub 25683 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘”β€˜π‘›) ∈ dom ∫1 ∧ (π‘”β€˜π‘›) ∘r ≀ 𝐹) β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ))
1951943expia 1118 . . . . . . . . . . . . . 14 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘”β€˜π‘›) ∈ dom ∫1) β†’ ((π‘”β€˜π‘›) ∘r ≀ 𝐹 β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
19674, 195sylan2 591 . . . . . . . . . . . . 13 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ 𝑛 ∈ β„•)) β†’ ((π‘”β€˜π‘›) ∘r ≀ 𝐹 β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
197196anassrs 466 . . . . . . . . . . . 12 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ ((π‘”β€˜π‘›) ∘r ≀ 𝐹 β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
198197adantrd 490 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
199198ralimdva 3164 . . . . . . . . . 10 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ (βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ βˆ€π‘› ∈ β„• (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
200199impr 453 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘› ∈ β„• (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ))
201 eqid 2728 . . . . . . . . . . . . 13 (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) = (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))
20289, 201, 101fvmpt 7010 . . . . . . . . . . . 12 (π‘š ∈ β„• β†’ ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) = (∫1β€˜(π‘”β€˜π‘š)))
203202breq1d 5162 . . . . . . . . . . 11 (π‘š ∈ β„• β†’ (((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ) ↔ (∫1β€˜(π‘”β€˜π‘š)) ≀ (∫2β€˜πΉ)))
204203ralbiia 3088 . . . . . . . . . 10 (βˆ€π‘š ∈ β„• ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ) ↔ βˆ€π‘š ∈ β„• (∫1β€˜(π‘”β€˜π‘š)) ≀ (∫2β€˜πΉ))
20589breq1d 5162 . . . . . . . . . . 11 (𝑛 = π‘š β†’ ((∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ) ↔ (∫1β€˜(π‘”β€˜π‘š)) ≀ (∫2β€˜πΉ)))
206205cbvralvw 3232 . . . . . . . . . 10 (βˆ€π‘› ∈ β„• (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ) ↔ βˆ€π‘š ∈ β„• (∫1β€˜(π‘”β€˜π‘š)) ≀ (∫2β€˜πΉ))
207204, 206bitr4i 277 . . . . . . . . 9 (βˆ€π‘š ∈ β„• ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ) ↔ βˆ€π‘› ∈ β„• (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ))
208200, 207sylibr 233 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘š ∈ β„• ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ))
209 ffn 6727 . . . . . . . . 9 ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))):β„•βŸΆβ„ β†’ (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) Fn β„•)
210 breq1 5155 . . . . . . . . . 10 (𝑧 = ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) β†’ (𝑧 ≀ (∫2β€˜πΉ) ↔ ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ)))
211210ralrn 7103 . . . . . . . . 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 256 . . . . . . 7 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))𝑧 ≀ (∫2β€˜πΉ))
214 supxrleub 13345 . . . . . . . 8 ((ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ* ∧ (∫2β€˜πΉ) ∈ ℝ*) β†’ (sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ≀ (∫2β€˜πΉ) ↔ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))𝑧 ≀ (∫2β€˜πΉ)))
21581, 73, 214syl2anc 582 . . . . . . 7 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ≀ (∫2β€˜πΉ) ↔ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))𝑧 ≀ (∫2β€˜πΉ)))
216213, 215mpbird 256 . . . . . 6 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ≀ (∫2β€˜πΉ))
21773, 83, 193, 216xrletrid 13174 . . . . 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 411 . . 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 394   ∨ w3o 1083   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098   β‰  wne 2937  βˆ€wral 3058  βˆƒwrex 3067   βŠ† wss 3949  βˆ…c0 4326  ifcif 4532   class class class wbr 5152   ↦ cmpt 5235  dom cdm 5682  ran crn 5683   Fn wfn 6548  βŸΆwf 6549  β€˜cfv 6553  (class class class)co 7426   ∘r cofr 7690   ↑m cmap 8851  supcsup 9471  β„cr 11145  0cc0 11146  1c1 11147  +∞cpnf 11283  -∞cmnf 11284  β„*cxr 11285   < clt 11286   ≀ cle 11287   βˆ’ cmin 11482   / cdiv 11909  β„•cn 12250  β„+crp 13014  [,]cicc 13367  βˆ«1citg1 25564  βˆ«2citg2 25565
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 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9672  ax-cc 10466  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7691  df-ofr 7692  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-2o 8494  df-er 8731  df-map 8853  df-pm 8854  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-sup 9473  df-inf 9474  df-oi 9541  df-dju 9932  df-card 9970  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-n0 12511  df-z 12597  df-uz 12861  df-q 12971  df-rp 13015  df-xadd 13133  df-ioo 13368  df-ico 13370  df-icc 13371  df-fz 13525  df-fzo 13668  df-fl 13797  df-seq 14007  df-exp 14067  df-hash 14330  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-clim 15472  df-sum 15673  df-xmet 21279  df-met 21280  df-ovol 25413  df-vol 25414  df-mbf 25568  df-itg1 25569  df-itg2 25570
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator