MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2seq Structured version   Visualization version   GIF version
Theorem itg2seq 25251
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 25264, 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 12215 . . . . . . . . . . . 12 (𝑛 ∈ β„• β†’ 𝑛 ∈ ℝ)
21ad2antlr 725 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ 𝑛 ∈ ℝ)
32ltpnfd 13097 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ 𝑛 < +∞)
4 iftrue 4533 . . . . . . . . . . 11 ((∫2β€˜πΉ) = +∞ β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = 𝑛)
54adantl 482 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = 𝑛)
6 simpr 485 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ (∫2β€˜πΉ) = +∞)
73, 5, 63brtr4d 5179 . . . . . . . . 9 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ))
8 iffalse 4536 . . . . . . . . . . 11 (Β¬ (∫2β€˜πΉ) = +∞ β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))
98adantl 482 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))
10 itg2cl 25241 . . . . . . . . . . . . . . 15 (𝐹:β„βŸΆ(0[,]+∞) β†’ (∫2β€˜πΉ) ∈ ℝ*)
11 xrrebnd 13143 . . . . . . . . . . . . . . 15 ((∫2β€˜πΉ) ∈ ℝ* β†’ ((∫2β€˜πΉ) ∈ ℝ ↔ (-∞ < (∫2β€˜πΉ) ∧ (∫2β€˜πΉ) < +∞)))
1210, 11syl 17 . . . . . . . . . . . . . 14 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((∫2β€˜πΉ) ∈ ℝ ↔ (-∞ < (∫2β€˜πΉ) ∧ (∫2β€˜πΉ) < +∞)))
13 itg2ge0 25244 . . . . . . . . . . . . . . . 16 (𝐹:β„βŸΆ(0[,]+∞) β†’ 0 ≀ (∫2β€˜πΉ))
14 mnflt0 13101 . . . . . . . . . . . . . . . . 17 -∞ < 0
15 mnfxr 11267 . . . . . . . . . . . . . . . . . 18 -∞ ∈ ℝ*
16 0xr 11257 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ*
17 xrltletr 13132 . . . . . . . . . . . . . . . . . 18 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ (∫2β€˜πΉ) ∈ ℝ*) β†’ ((-∞ < 0 ∧ 0 ≀ (∫2β€˜πΉ)) β†’ -∞ < (∫2β€˜πΉ)))
1815, 16, 10, 17mp3an12i 1465 . . . . . . . . . . . . . . . . 17 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((-∞ < 0 ∧ 0 ≀ (∫2β€˜πΉ)) β†’ -∞ < (∫2β€˜πΉ)))
1914, 18mpani 694 . . . . . . . . . . . . . . . 16 (𝐹:β„βŸΆ(0[,]+∞) β†’ (0 ≀ (∫2β€˜πΉ) β†’ -∞ < (∫2β€˜πΉ)))
2013, 19mpd 15 . . . . . . . . . . . . . . 15 (𝐹:β„βŸΆ(0[,]+∞) β†’ -∞ < (∫2β€˜πΉ))
2120biantrurd 533 . . . . . . . . . . . . . 14 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((∫2β€˜πΉ) < +∞ ↔ (-∞ < (∫2β€˜πΉ) ∧ (∫2β€˜πΉ) < +∞)))
22 nltpnft 13139 . . . . . . . . . . . . . . . 16 ((∫2β€˜πΉ) ∈ ℝ* β†’ ((∫2β€˜πΉ) = +∞ ↔ Β¬ (∫2β€˜πΉ) < +∞))
2310, 22syl 17 . . . . . . . . . . . . . . 15 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((∫2β€˜πΉ) = +∞ ↔ Β¬ (∫2β€˜πΉ) < +∞))
2423con2bid 354 . . . . . . . . . . . . . 14 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((∫2β€˜πΉ) < +∞ ↔ Β¬ (∫2β€˜πΉ) = +∞))
2512, 21, 243bitr2rd 307 . . . . . . . . . . . . 13 (𝐹:β„βŸΆ(0[,]+∞) β†’ (Β¬ (∫2β€˜πΉ) = +∞ ↔ (∫2β€˜πΉ) ∈ ℝ))
2625biimpa 477 . . . . . . . . . . . 12 ((𝐹:β„βŸΆ(0[,]+∞) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (∫2β€˜πΉ) ∈ ℝ)
2726adantlr 713 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (∫2β€˜πΉ) ∈ ℝ)
28 nnrp 12981 . . . . . . . . . . . . 13 (𝑛 ∈ β„• β†’ 𝑛 ∈ ℝ+)
2928rpreccld 13022 . . . . . . . . . . . 12 (𝑛 ∈ β„• β†’ (1 / 𝑛) ∈ ℝ+)
3029ad2antlr 725 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (1 / 𝑛) ∈ ℝ+)
3127, 30ltsubrpd 13044 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)) < (∫2β€˜πΉ))
329, 31eqbrtrd 5169 . . . . . . . . 9 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ))
337, 32pm2.61dan 811 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ))
34 nnrecre 12250 . . . . . . . . . . . . 13 (𝑛 ∈ β„• β†’ (1 / 𝑛) ∈ ℝ)
3534ad2antlr 725 . . . . . . . . . . . 12 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (1 / 𝑛) ∈ ℝ)
3627, 35resubcld 11638 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)) ∈ ℝ)
372, 36ifclda 4562 . . . . . . . . . 10 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ)
3837rexrd 11260 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*)
3910adantr 481 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ (∫2β€˜πΉ) ∈ ℝ*)
40 xrltnle 11277 . . . . . . . . 9 ((if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ* ∧ (∫2β€˜πΉ) ∈ ℝ*) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ) ↔ Β¬ (∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
4138, 39, 40syl2anc 584 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫2β€˜πΉ) ↔ Β¬ (∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
4233, 41mpbid 231 . . . . . . 7 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) β†’ Β¬ (∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
43 itg2leub 25243 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*) β†’ ((∫2β€˜πΉ) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ βˆ€π‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 β†’ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))))
4438, 43syldan 591 . . . . . . 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 3102 . . . . . 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 25193 . . . . . . . 8 (𝑓 ∈ dom ∫1 β†’ (∫1β€˜π‘“) ∈ ℝ)
49 ltnle 11289 . . . . . . . 8 ((if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ ∧ (∫1β€˜π‘“) ∈ ℝ) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“) ↔ Β¬ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
5037, 48, 49syl2an 596 . . . . . . 7 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ 𝑓 ∈ dom ∫1) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“) ↔ Β¬ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
5150anbi2d 629 . . . . . 6 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑛 ∈ β„•) ∧ 𝑓 ∈ dom ∫1) β†’ ((𝑓 ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“)) ↔ (𝑓 ∘r ≀ 𝐹 ∧ Β¬ (∫1β€˜π‘“) ≀ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))))
5251rexbidva 3176 . . . . 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 3146 . . 3 (𝐹:β„βŸΆ(0[,]+∞) β†’ βˆ€π‘› ∈ β„• βˆƒπ‘“ ∈ dom ∫1(𝑓 ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“)))
55 ovex 7438 . . . . 5 (ℝ ↑m ℝ) ∈ V
56 i1ff 25184 . . . . . . 7 (π‘₯ ∈ dom ∫1 β†’ π‘₯:β„βŸΆβ„)
57 reex 11197 . . . . . . . 8 ℝ ∈ V
5857, 57elmap 8861 . . . . . . 7 (π‘₯ ∈ (ℝ ↑m ℝ) ↔ π‘₯:β„βŸΆβ„)
5956, 58sylibr 233 . . . . . 6 (π‘₯ ∈ dom ∫1 β†’ π‘₯ ∈ (ℝ ↑m ℝ))
6059ssriv 3985 . . . . 5 dom ∫1 βŠ† (ℝ ↑m ℝ)
6155, 60ssexi 5321 . . . 4 dom ∫1 ∈ V
62 nnenom 13941 . . . 4 β„• β‰ˆ Ο‰
63 breq1 5150 . . . . 5 (𝑓 = (π‘”β€˜π‘›) β†’ (𝑓 ∘r ≀ 𝐹 ↔ (π‘”β€˜π‘›) ∘r ≀ 𝐹))
64 fveq2 6888 . . . . . 6 (𝑓 = (π‘”β€˜π‘›) β†’ (∫1β€˜π‘“) = (∫1β€˜(π‘”β€˜π‘›)))
6564breq2d 5159 . . . . 5 (𝑓 = (π‘”β€˜π‘›) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“) ↔ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))
6663, 65anbi12d 631 . . . 4 (𝑓 = (π‘”β€˜π‘›) β†’ ((𝑓 ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜π‘“)) ↔ ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›)))))
6761, 62, 66axcc4 10430 . . 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 483 . . . . . . 7 (((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ (π‘”β€˜π‘›) ∘r ≀ 𝐹)
7170ralimi 3083 . . . . . 6 (βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ βˆ€π‘› ∈ β„• (π‘”β€˜π‘›) ∘r ≀ 𝐹)
7271ad2antll 727 . . . . 5 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘› ∈ β„• (π‘”β€˜π‘›) ∘r ≀ 𝐹)
7310adantr 481 . . . . . 6 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (∫2β€˜πΉ) ∈ ℝ*)
74 ffvelcdm 7080 . . . . . . . . . . . 12 ((𝑔:β„•βŸΆdom ∫1 ∧ 𝑛 ∈ β„•) β†’ (π‘”β€˜π‘›) ∈ dom ∫1)
75 itg1cl 25193 . . . . . . . . . . . 12 ((π‘”β€˜π‘›) ∈ dom ∫1 β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ)
7674, 75syl 17 . . . . . . . . . . 11 ((𝑔:β„•βŸΆdom ∫1 ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ)
7776fmpttd 7111 . . . . . . . . . 10 (𝑔:β„•βŸΆdom ∫1 β†’ (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))):β„•βŸΆβ„)
7877ad2antrl 726 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))):β„•βŸΆβ„)
7978frnd 6722 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ)
80 ressxr 11254 . . . . . . . 8 ℝ βŠ† ℝ*
8179, 80sstrdi 3993 . . . . . . 7 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ*)
82 supxrcl 13290 . . . . . . 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 11260 . . . . . . . . . . . . 13 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ*)
87 xrltle 13124 . . . . . . . . . . . . 13 ((if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ* ∧ (∫1β€˜(π‘”β€˜π‘›)) ∈ ℝ*) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›)) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ (∫1β€˜(π‘”β€˜π‘›))))
8884, 86, 87syl2anc 584 . . . . . . . . . . . 12 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›)) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ (∫1β€˜(π‘”β€˜π‘›))))
89 2fveq3 6893 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘š β†’ (∫1β€˜(π‘”β€˜π‘›)) = (∫1β€˜(π‘”β€˜π‘š)))
9089cbvmptv 5260 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) = (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))
9190rneqi 5934 . . . . . . . . . . . . . . 15 ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) = ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))
9277adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))):β„•βŸΆβ„)
9392frnd 6722 . . . . . . . . . . . . . . . . 17 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ)
9493, 80sstrdi 3993 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ*)
9594adantr 481 . . . . . . . . . . . . . . 15 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ*)
9691, 95eqsstrrid 4030 . . . . . . . . . . . . . 14 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) βŠ† ℝ*)
97 2fveq3 6893 . . . . . . . . . . . . . . . . 17 (π‘š = 𝑛 β†’ (∫1β€˜(π‘”β€˜π‘š)) = (∫1β€˜(π‘”β€˜π‘›)))
98 eqid 2732 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) = (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))
99 fvex 6901 . . . . . . . . . . . . . . . . 17 (∫1β€˜(π‘”β€˜π‘›)) ∈ V
10097, 98, 99fvmpt 6995 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))β€˜π‘›) = (∫1β€˜(π‘”β€˜π‘›)))
101 fvex 6901 . . . . . . . . . . . . . . . . . 18 (∫1β€˜(π‘”β€˜π‘š)) ∈ V
102101, 98fnmpti 6690 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) Fn β„•
103 fnfvelrn 7079 . . . . . . . . . . . . . . . . 17 (((π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) Fn β„• ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))β€˜π‘›) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))))
104102, 103mpan 688 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))β€˜π‘›) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))))
105100, 104eqeltrrd 2834 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„• β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))))
106105adantl 482 . . . . . . . . . . . . . 14 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))))
107 supxrub 13299 . . . . . . . . . . . . . 14 ((ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))) βŠ† ℝ* ∧ (∫1β€˜(π‘”β€˜π‘›)) ∈ ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š)))) β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ))
10896, 106, 107syl2anc 584 . . . . . . . . . . . . 13 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ))
10991supeq1i 9438 . . . . . . . . . . . . . . 15 sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )
11095, 82syl 17 . . . . . . . . . . . . . . 15 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ∈ ℝ*)
111109, 110eqeltrrid 2838 . . . . . . . . . . . . . 14 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) ∈ ℝ*)
112 xrletr 13133 . . . . . . . . . . . . . 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 1371 . . . . . . . . . . . . 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 491 . . . . . . . . . 10 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
117116ralimdva 3167 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ (βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
118117impr 455 . . . . . . . 8 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ))
119 breq2 5151 . . . . . . . . . . 11 (π‘₯ = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ ↔ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
120119ralbidv 3177 . . . . . . . . . 10 (π‘₯ = sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) β†’ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ ↔ βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < )))
121 breq2 5151 . . . . . . . . . 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 13092 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ* ↔ (π‘₯ ∈ ℝ ∨ π‘₯ = +∞ ∨ π‘₯ = -∞))
124 simplrl 775 . . . . . . . . . . . . . . . . . . 19 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ π‘₯ ∈ ℝ)
125 arch 12465 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ ℝ β†’ βˆƒπ‘› ∈ β„• π‘₯ < 𝑛)
126124, 125syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ βˆƒπ‘› ∈ β„• π‘₯ < 𝑛)
1274adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = 𝑛)
128127breq2d 5159 . . . . . . . . . . . . . . . . . . 19 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ (∫2β€˜πΉ) = +∞) β†’ (π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ π‘₯ < 𝑛))
129128rexbidv 3178 . . . . . . . . . . . . . . . . . 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 11638 . . . . . . . . . . . . . . . . . . 19 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ ((∫2β€˜πΉ) βˆ’ π‘₯) ∈ ℝ)
134 simplrr 776 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ π‘₯ < (∫2β€˜πΉ))
135132, 131posdifd 11797 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ (π‘₯ < (∫2β€˜πΉ) ↔ 0 < ((∫2β€˜πΉ) βˆ’ π‘₯)))
136134, 135mpbid 231 . . . . . . . . . . . . . . . . . . 19 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ 0 < ((∫2β€˜πΉ) βˆ’ π‘₯))
137 nnrecl 12466 . . . . . . . . . . . . . . . . . . 19 ((((∫2β€˜πΉ) βˆ’ π‘₯) ∈ ℝ ∧ 0 < ((∫2β€˜πΉ) βˆ’ π‘₯)) β†’ βˆƒπ‘› ∈ β„• (1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯))
138133, 136, 137syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) β†’ βˆƒπ‘› ∈ β„• (1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯))
13934adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ (1 / 𝑛) ∈ ℝ)
140131adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ (∫2β€˜πΉ) ∈ ℝ)
141132adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ π‘₯ ∈ ℝ)
142 ltsub13 11691 . . . . . . . . . . . . . . . . . . . . 21 (((1 / 𝑛) ∈ ℝ ∧ (∫2β€˜πΉ) ∈ ℝ ∧ π‘₯ ∈ ℝ) β†’ ((1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯) ↔ π‘₯ < ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
143139, 140, 141, 142syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ ((1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯) ↔ π‘₯ < ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
1448ad2antlr 725 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) = ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))
145144breq2d 5159 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ (π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ π‘₯ < ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
146143, 145bitr4d 281 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∧ π‘₯ < (∫2β€˜πΉ))) ∧ Β¬ (∫2β€˜πΉ) = +∞) ∧ 𝑛 ∈ β„•) β†’ ((1 / 𝑛) < ((∫2β€˜πΉ) βˆ’ π‘₯) ↔ π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
147146rexbidva 3176 . . . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ < (∫2β€˜πΉ) β†’ βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛)))))
151 rexr 11256 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ β†’ π‘₯ ∈ ℝ*)
152 xrltnle 11277 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ ℝ* ∧ (∫2β€˜πΉ) ∈ ℝ*) β†’ (π‘₯ < (∫2β€˜πΉ) ↔ Β¬ (∫2β€˜πΉ) ≀ π‘₯))
153151, 10, 152syl2anr 597 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ < (∫2β€˜πΉ) ↔ Β¬ (∫2β€˜πΉ) ≀ π‘₯))
154151ad2antlr 725 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) ∧ 𝑛 ∈ β„•) β†’ π‘₯ ∈ ℝ*)
15538adantlr 713 . . . . . . . . . . . . . . . . . 18 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) ∧ 𝑛 ∈ β„•) β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*)
156 xrltnle 11277 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ ℝ* ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*) β†’ (π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
157154, 155, 156syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) ∧ 𝑛 ∈ β„•) β†’ (π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
158157rexbidva 3176 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ) β†’ (βˆƒπ‘› ∈ β„• π‘₯ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ βˆƒπ‘› ∈ β„• Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯))
159 rexnal 3100 . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ (∫2β€˜πΉ) ∈ ℝ*)
164 pnfge 13106 . . . . . . . . . . . . . . . 16 ((∫2β€˜πΉ) ∈ ℝ* β†’ (∫2β€˜πΉ) ≀ +∞)
165163, 164syl 17 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ (∫2β€˜πΉ) ≀ +∞)
166 simpr 485 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ π‘₯ = +∞)
167165, 166breqtrrd 5175 . . . . . . . . . . . . . 14 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ (∫2β€˜πΉ) ≀ π‘₯)
168167a1d 25 . . . . . . . . . . . . 13 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = +∞) β†’ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
169 1nn 12219 . . . . . . . . . . . . . . . 16 1 ∈ β„•
170169ne0ii 4336 . . . . . . . . . . . . . . 15 β„• β‰  βˆ…
171 r19.2z 4493 . . . . . . . . . . . . . . 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 13099 . . . . . . . . . . . . . . . . . . 19 (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ β†’ -∞ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))))
175 rexr 11256 . . . . . . . . . . . . . . . . . . . 20 (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ β†’ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*)
176 xrltnle 11277 . . . . . . . . . . . . . . . . . . . 20 ((-∞ ∈ ℝ* ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ∈ ℝ*) β†’ (-∞ < if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ↔ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ -∞))
17715, 175, 176sylancr 587 . . . . . . . . . . . . . . . . . . 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 5159 . . . . . . . . . . . . . . . . 17 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = -∞) ∧ 𝑛 ∈ β„•) β†’ (if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ ↔ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ -∞))
182179, 181mtbird 324 . . . . . . . . . . . . . . . 16 (((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ = -∞) ∧ 𝑛 ∈ β„•) β†’ Β¬ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯)
183182nrexdv 3149 . . . . . . . . . . . . . . 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 1430 . . . . . . . . . . . 12 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ∨ π‘₯ = +∞ ∨ π‘₯ = -∞)) β†’ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
187123, 186sylan2b 594 . . . . . . . . . . 11 ((𝐹:β„βŸΆ(0[,]+∞) ∧ π‘₯ ∈ ℝ*) β†’ (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
188187ralrimiva 3146 . . . . . . . . . 10 (𝐹:β„βŸΆ(0[,]+∞) β†’ βˆ€π‘₯ ∈ ℝ* (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
189188adantr 481 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘₯ ∈ ℝ* (βˆ€π‘› ∈ β„• if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) ≀ π‘₯ β†’ (∫2β€˜πΉ) ≀ π‘₯))
190109, 83eqeltrrid 2838 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ sup(ran (π‘š ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘š))), ℝ*, < ) ∈ ℝ*)
191122, 189, 190rspcdva 3613 . . . . . . . 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 5189 . . . . . 6 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (∫2β€˜πΉ) ≀ sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ))
194 itg2ub 25242 . . . . . . . . . . . . . . 15 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘”β€˜π‘›) ∈ dom ∫1 ∧ (π‘”β€˜π‘›) ∘r ≀ 𝐹) β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ))
1951943expia 1121 . . . . . . . . . . . . . 14 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘”β€˜π‘›) ∈ dom ∫1) β†’ ((π‘”β€˜π‘›) ∘r ≀ 𝐹 β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
19674, 195sylan2 593 . . . . . . . . . . . . 13 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ 𝑛 ∈ β„•)) β†’ ((π‘”β€˜π‘›) ∘r ≀ 𝐹 β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
197196anassrs 468 . . . . . . . . . . . 12 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ ((π‘”β€˜π‘›) ∘r ≀ 𝐹 β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
198197adantrd 492 . . . . . . . . . . 11 (((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) ∧ 𝑛 ∈ β„•) β†’ (((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
199198ralimdva 3167 . . . . . . . . . 10 ((𝐹:β„βŸΆ(0[,]+∞) ∧ 𝑔:β„•βŸΆdom ∫1) β†’ (βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))) β†’ βˆ€π‘› ∈ β„• (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ)))
200199impr 455 . . . . . . . . 9 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ βˆ€π‘› ∈ β„• (∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ))
201 eqid 2732 . . . . . . . . . . . . 13 (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) = (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))
20289, 201, 101fvmpt 6995 . . . . . . . . . . . 12 (π‘š ∈ β„• β†’ ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) = (∫1β€˜(π‘”β€˜π‘š)))
203202breq1d 5157 . . . . . . . . . . 11 (π‘š ∈ β„• β†’ (((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ) ↔ (∫1β€˜(π‘”β€˜π‘š)) ≀ (∫2β€˜πΉ)))
204203ralbiia 3091 . . . . . . . . . 10 (βˆ€π‘š ∈ β„• ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ) ↔ βˆ€π‘š ∈ β„• (∫1β€˜(π‘”β€˜π‘š)) ≀ (∫2β€˜πΉ))
20589breq1d 5157 . . . . . . . . . . 11 (𝑛 = π‘š β†’ ((∫1β€˜(π‘”β€˜π‘›)) ≀ (∫2β€˜πΉ) ↔ (∫1β€˜(π‘”β€˜π‘š)) ≀ (∫2β€˜πΉ)))
206205cbvralvw 3234 . . . . . . . . . 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 6714 . . . . . . . . 9 ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))):β„•βŸΆβ„ β†’ (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) Fn β„•)
210 breq1 5150 . . . . . . . . . 10 (𝑧 = ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) β†’ (𝑧 ≀ (∫2β€˜πΉ) ↔ ((𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))β€˜π‘š) ≀ (∫2β€˜πΉ)))
211210ralrn 7086 . . . . . . . . 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 13301 . . . . . . . 8 ((ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))) βŠ† ℝ* ∧ (∫2β€˜πΉ) ∈ ℝ*) β†’ (sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ) ≀ (∫2β€˜πΉ) ↔ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›)))𝑧 ≀ (∫2β€˜πΉ)))
21581, 73, 214syl2anc 584 . . . . . . 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 13130 . . . . 5 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (∫2β€˜πΉ) = sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ))
21869, 72, 2173jca 1128 . . . 4 ((𝐹:β„βŸΆ(0[,]+∞) ∧ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›))))) β†’ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• (π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ (∫2β€˜πΉ) = sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < )))
219218ex 413 . . 3 (𝐹:β„βŸΆ(0[,]+∞) β†’ ((𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• ((π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ if((∫2β€˜πΉ) = +∞, 𝑛, ((∫2β€˜πΉ) βˆ’ (1 / 𝑛))) < (∫1β€˜(π‘”β€˜π‘›)))) β†’ (𝑔:β„•βŸΆdom ∫1 ∧ βˆ€π‘› ∈ β„• (π‘”β€˜π‘›) ∘r ≀ 𝐹 ∧ (∫2β€˜πΉ) = sup(ran (𝑛 ∈ β„• ↦ (∫1β€˜(π‘”β€˜π‘›))), ℝ*, < ))))
220219eximdv 1920 . 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 396   ∨ w3o 1086   ∧ w3a 1087   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070   βŠ† wss 3947  βˆ…c0 4321  ifcif 4527   class class class wbr 5147   ↦ cmpt 5230  dom cdm 5675  ran crn 5676   Fn wfn 6535  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405   ∘r cofr 7665   ↑m cmap 8816  supcsup 9431  β„cr 11105  0cc0 11106  1c1 11107  +∞cpnf 11241  -∞cmnf 11242  β„*cxr 11243   < clt 11244   ≀ cle 11245   βˆ’ cmin 11440   / cdiv 11867  β„•cn 12208  β„+crp 12970  [,]cicc 13323  βˆ«1citg1 25123  βˆ«2citg2 25124
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cc 10426  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-ofr 7667  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-er 8699  df-map 8818  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-z 12555  df-uz 12819  df-q 12929  df-rp 12971  df-xadd 13089  df-ioo 13324  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-sum 15629  df-xmet 20929  df-met 20930  df-ovol 24972  df-vol 24973  df-mbf 25127  df-itg1 25128  df-itg2 25129
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator