Step | Hyp | Ref
| Expression |
1 | | nnre 11027 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
2 | 1 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ (∫2‘𝐹) = +∞) → 𝑛 ∈ ℝ) |
3 | | ltpnf 11954 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ → 𝑛 < +∞) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ (∫2‘𝐹) = +∞) → 𝑛 < +∞) |
5 | | iftrue 4092 |
. . . . . . . . . . 11
⊢
((∫2‘𝐹) = +∞ →
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛) |
6 | 5 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ (∫2‘𝐹) = +∞) →
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛) |
7 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ (∫2‘𝐹) = +∞) →
(∫2‘𝐹)
= +∞) |
8 | 4, 6, 7 | 3brtr4d 4685 |
. . . . . . . . 9
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ (∫2‘𝐹) = +∞) →
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹)) |
9 | | iffalse 4095 |
. . . . . . . . . . 11
⊢ (¬
(∫2‘𝐹)
= +∞ → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛))) |
10 | 9 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ ¬ (∫2‘𝐹) = +∞) →
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛))) |
11 | | itg2cl 23499 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ (∫2‘𝐹) ∈
ℝ*) |
12 | | xrrebnd 11999 |
. . . . . . . . . . . . . . 15
⊢
((∫2‘𝐹) ∈ ℝ* →
((∫2‘𝐹) ∈ ℝ ↔ (-∞ <
(∫2‘𝐹)
∧ (∫2‘𝐹) < +∞))) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ ((∫2‘𝐹) ∈ ℝ ↔ (-∞ <
(∫2‘𝐹)
∧ (∫2‘𝐹) < +∞))) |
14 | | itg2ge0 23502 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ 0 ≤ (∫2‘𝐹)) |
15 | | mnflt0 11959 |
. . . . . . . . . . . . . . . . 17
⊢ -∞
< 0 |
16 | | mnfxr 10096 |
. . . . . . . . . . . . . . . . . . 19
⊢ -∞
∈ ℝ* |
17 | | 0xr 10086 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ* |
18 | | xrltletr 11988 |
. . . . . . . . . . . . . . . . . . 19
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ (∫2‘𝐹) ∈ ℝ*) →
((-∞ < 0 ∧ 0 ≤ (∫2‘𝐹)) → -∞ <
(∫2‘𝐹))) |
19 | 16, 17, 18 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . 18
⊢
((∫2‘𝐹) ∈ ℝ* →
((-∞ < 0 ∧ 0 ≤ (∫2‘𝐹)) → -∞ <
(∫2‘𝐹))) |
20 | 11, 19 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ ((-∞ < 0 ∧ 0 ≤ (∫2‘𝐹)) → -∞ <
(∫2‘𝐹))) |
21 | 15, 20 | mpani 712 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ (0 ≤ (∫2‘𝐹) → -∞ <
(∫2‘𝐹))) |
22 | 14, 21 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ -∞ < (∫2‘𝐹)) |
23 | 22 | biantrurd 529 |
. . . . . . . . . . . . . 14
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ ((∫2‘𝐹) < +∞ ↔ (-∞ <
(∫2‘𝐹)
∧ (∫2‘𝐹) < +∞))) |
24 | | nltpnft 11995 |
. . . . . . . . . . . . . . . 16
⊢
((∫2‘𝐹) ∈ ℝ* →
((∫2‘𝐹) = +∞ ↔ ¬
(∫2‘𝐹)
< +∞)) |
25 | 11, 24 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ ((∫2‘𝐹) = +∞ ↔ ¬
(∫2‘𝐹)
< +∞)) |
26 | 25 | con2bid 344 |
. . . . . . . . . . . . . 14
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ ((∫2‘𝐹) < +∞ ↔ ¬
(∫2‘𝐹)
= +∞)) |
27 | 13, 23, 26 | 3bitr2rd 297 |
. . . . . . . . . . . . 13
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ (¬ (∫2‘𝐹) = +∞ ↔
(∫2‘𝐹)
∈ ℝ)) |
28 | 27 | biimpa 501 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ ¬ (∫2‘𝐹) = +∞) →
(∫2‘𝐹)
∈ ℝ) |
29 | 28 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ ¬ (∫2‘𝐹) = +∞) →
(∫2‘𝐹)
∈ ℝ) |
30 | | nnrp 11842 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
31 | 30 | rpreccld 11882 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ+) |
32 | 31 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ ¬ (∫2‘𝐹) = +∞) → (1 / 𝑛) ∈
ℝ+) |
33 | 29, 32 | ltsubrpd 11904 |
. . . . . . . . . 10
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ ¬ (∫2‘𝐹) = +∞) →
((∫2‘𝐹) − (1 / 𝑛)) < (∫2‘𝐹)) |
34 | 10, 33 | eqbrtrd 4675 |
. . . . . . . . 9
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ ¬ (∫2‘𝐹) = +∞) →
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹)) |
35 | 8, 34 | pm2.61dan 832 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹)) |
36 | | nnrecre 11057 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
37 | 36 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ ¬ (∫2‘𝐹) = +∞) → (1 / 𝑛) ∈ ℝ) |
38 | 29, 37 | resubcld 10458 |
. . . . . . . . . . 11
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ ¬ (∫2‘𝐹) = +∞) →
((∫2‘𝐹) − (1 / 𝑛)) ∈ ℝ) |
39 | 2, 38 | ifclda 4120 |
. . . . . . . . . 10
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ) |
40 | 39 | rexrd 10089 |
. . . . . . . . 9
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈
ℝ*) |
41 | 11 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (∫2‘𝐹) ∈
ℝ*) |
42 | | xrltnle 10105 |
. . . . . . . . 9
⊢
((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ* ∧
(∫2‘𝐹)
∈ ℝ*) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹) ↔ ¬
(∫2‘𝐹)
≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))) |
43 | 40, 41, 42 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫2‘𝐹) ↔ ¬
(∫2‘𝐹)
≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))) |
44 | 35, 43 | mpbid 222 |
. . . . . . 7
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ ¬ (∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))) |
45 | | itg2leub 23501 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*) →
((∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐹 →
(∫1‘𝑓)
≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))) |
46 | 40, 45 | syldan 487 |
. . . . . . 7
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ ((∫2‘𝐹) ≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐹 →
(∫1‘𝑓)
≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))) |
47 | 44, 46 | mtbid 314 |
. . . . . 6
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ ¬ ∀𝑓
∈ dom ∫1(𝑓 ∘𝑟 ≤ 𝐹 →
(∫1‘𝑓)
≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))) |
48 | | rexanali 2998 |
. . . . . 6
⊢
(∃𝑓 ∈ dom
∫1(𝑓
∘𝑟 ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))) ↔ ¬ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐹 →
(∫1‘𝑓)
≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))) |
49 | 47, 48 | sylibr 224 |
. . . . 5
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ ∃𝑓 ∈ dom
∫1(𝑓
∘𝑟 ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))) |
50 | | itg1cl 23452 |
. . . . . . . 8
⊢ (𝑓 ∈ dom ∫1
→ (∫1‘𝑓) ∈ ℝ) |
51 | | ltnle 10117 |
. . . . . . . 8
⊢
((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ ∧
(∫1‘𝑓)
∈ ℝ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓) ↔ ¬
(∫1‘𝑓)
≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))) |
52 | 39, 50, 51 | syl2an 494 |
. . . . . . 7
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑓 ∈ dom
∫1) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓) ↔ ¬
(∫1‘𝑓)
≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))) |
53 | 52 | anbi2d 740 |
. . . . . 6
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑓 ∈ dom
∫1) → ((𝑓 ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ (𝑓 ∘𝑟 ≤ 𝐹 ∧ ¬
(∫1‘𝑓)
≤ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))) |
54 | 53 | rexbidva 3049 |
. . . . 5
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (∃𝑓 ∈ dom
∫1(𝑓
∘𝑟 ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ ∃𝑓 ∈ dom
∫1(𝑓
∘𝑟 ≤ 𝐹 ∧ ¬ (∫1‘𝑓) ≤
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))))) |
55 | 49, 54 | mpbird 247 |
. . . 4
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ ∃𝑓 ∈ dom
∫1(𝑓
∘𝑟 ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓))) |
56 | 55 | ralrimiva 2966 |
. . 3
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ ∀𝑛 ∈
ℕ ∃𝑓 ∈ dom
∫1(𝑓
∘𝑟 ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓))) |
57 | | ovex 6678 |
. . . . 5
⊢ (ℝ
↑𝑚 ℝ) ∈ V |
58 | | i1ff 23443 |
. . . . . . 7
⊢ (𝑥 ∈ dom ∫1
→ 𝑥:ℝ⟶ℝ) |
59 | | reex 10027 |
. . . . . . . 8
⊢ ℝ
∈ V |
60 | 59, 59 | elmap 7886 |
. . . . . . 7
⊢ (𝑥 ∈ (ℝ
↑𝑚 ℝ) ↔ 𝑥:ℝ⟶ℝ) |
61 | 58, 60 | sylibr 224 |
. . . . . 6
⊢ (𝑥 ∈ dom ∫1
→ 𝑥 ∈ (ℝ
↑𝑚 ℝ)) |
62 | 61 | ssriv 3607 |
. . . . 5
⊢ dom
∫1 ⊆ (ℝ ↑𝑚
ℝ) |
63 | 57, 62 | ssexi 4803 |
. . . 4
⊢ dom
∫1 ∈ V |
64 | | nnenom 12779 |
. . . 4
⊢ ℕ
≈ ω |
65 | | breq1 4656 |
. . . . 5
⊢ (𝑓 = (𝑔‘𝑛) → (𝑓 ∘𝑟 ≤ 𝐹 ↔ (𝑔‘𝑛) ∘𝑟 ≤ 𝐹)) |
66 | | fveq2 6191 |
. . . . . 6
⊢ (𝑓 = (𝑔‘𝑛) → (∫1‘𝑓) =
(∫1‘(𝑔‘𝑛))) |
67 | 66 | breq2d 4665 |
. . . . 5
⊢ (𝑓 = (𝑔‘𝑛) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓) ↔
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)))) |
68 | 65, 67 | anbi12d 747 |
. . . 4
⊢ (𝑓 = (𝑔‘𝑛) → ((𝑓 ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) ↔ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) |
69 | 63, 64, 68 | axcc4 9261 |
. . 3
⊢
(∀𝑛 ∈
ℕ ∃𝑓 ∈ dom
∫1(𝑓
∘𝑟 ≤ 𝐹 ∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘𝑓)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
((𝑔‘𝑛) ∘𝑟
≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) |
70 | 56, 69 | syl 17 |
. 2
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ ∃𝑔(𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) |
71 | | simprl 794 |
. . . . 5
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → 𝑔:ℕ⟶dom
∫1) |
72 | | simpl 473 |
. . . . . . 7
⊢ (((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → (𝑔‘𝑛) ∘𝑟 ≤ 𝐹) |
73 | 72 | ralimi 2952 |
. . . . . 6
⊢
(∀𝑛 ∈
ℕ ((𝑔‘𝑛) ∘𝑟
≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘𝑟 ≤ 𝐹) |
74 | 73 | ad2antll 765 |
. . . . 5
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘𝑟 ≤ 𝐹) |
75 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚)) |
76 | 75 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → (∫1‘(𝑔‘𝑛)) = (∫1‘(𝑔‘𝑚))) |
77 | 76 | cbvmptv 4750 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) = (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))) |
78 | 77 | rneqi 5352 |
. . . . . . . . . 10
⊢ ran
(𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) = ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))) |
79 | 78 | supeq1i 8353 |
. . . . . . . . 9
⊢ sup(ran
(𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) = sup(ran
(𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
) |
80 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔:ℕ⟶dom
∫1 ∧ 𝑛
∈ ℕ) → (𝑔‘𝑛) ∈ dom
∫1) |
81 | | itg1cl 23452 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔‘𝑛) ∈ dom ∫1 →
(∫1‘(𝑔‘𝑛)) ∈ ℝ) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑔:ℕ⟶dom
∫1 ∧ 𝑛
∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ) |
83 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) = (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) |
84 | 82, 83 | fmptd 6385 |
. . . . . . . . . . . . 13
⊢ (𝑔:ℕ⟶dom
∫1 → (𝑛
∈ ℕ ↦ (∫1‘(𝑔‘𝑛))):ℕ⟶ℝ) |
85 | 84 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))):ℕ⟶ℝ) |
86 | | frn 6053 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))):ℕ⟶ℝ → ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) ⊆ ℝ) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) ⊆ ℝ) |
88 | | ressxr 10083 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℝ* |
89 | 87, 88 | syl6ss 3615 |
. . . . . . . . . 10
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) ⊆
ℝ*) |
90 | | supxrcl 12145 |
. . . . . . . . . 10
⊢ (ran
(𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) ⊆ ℝ* →
sup(ran (𝑛 ∈ ℕ
↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ∈
ℝ*) |
91 | 89, 90 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ∈
ℝ*) |
92 | 79, 91 | syl5eqelr 2706 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, < ) ∈
ℝ*) |
93 | | elxr 11950 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ*
↔ (𝑥 ∈ ℝ
∨ 𝑥 = +∞ ∨
𝑥 =
-∞)) |
94 | | simplrl 800 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → 𝑥 ∈
ℝ) |
95 | | arch 11289 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ →
∃𝑛 ∈ ℕ
𝑥 < 𝑛) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) →
∃𝑛 ∈ ℕ
𝑥 < 𝑛) |
97 | 5 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) →
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = 𝑛) |
98 | 97 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) → (𝑥 <
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ 𝑥 < 𝑛)) |
99 | 98 | rexbidv 3052 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) →
(∃𝑛 ∈ ℕ
𝑥 <
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∃𝑛 ∈ ℕ 𝑥 < 𝑛)) |
100 | 96, 99 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ (∫2‘𝐹) = +∞) →
∃𝑛 ∈ ℕ
𝑥 <
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))) |
101 | 28 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) → (∫2‘𝐹) ∈ ℝ) |
102 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) → 𝑥 ∈
ℝ) |
103 | 101, 102 | resubcld 10458 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) → ((∫2‘𝐹) − 𝑥) ∈ ℝ) |
104 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) → 𝑥 <
(∫2‘𝐹)) |
105 | 102, 101 | posdifd 10614 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) → (𝑥 <
(∫2‘𝐹)
↔ 0 < ((∫2‘𝐹) − 𝑥))) |
106 | 104, 105 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) → 0 < ((∫2‘𝐹) − 𝑥)) |
107 | | nnrecl 11290 |
. . . . . . . . . . . . . . . . . 18
⊢
((((∫2‘𝐹) − 𝑥) ∈ ℝ ∧ 0 <
((∫2‘𝐹) − 𝑥)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥)) |
108 | 103, 106,
107 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) → ∃𝑛
∈ ℕ (1 / 𝑛) <
((∫2‘𝐹) − 𝑥)) |
109 | 36 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) ∧ 𝑛 ∈
ℕ) → (1 / 𝑛)
∈ ℝ) |
110 | 101 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) ∧ 𝑛 ∈
ℕ) → (∫2‘𝐹) ∈ ℝ) |
111 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) ∧ 𝑛 ∈
ℕ) → 𝑥 ∈
ℝ) |
112 | | ltsub13 10509 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((1 /
𝑛) ∈ ℝ ∧
(∫2‘𝐹)
∈ ℝ ∧ 𝑥
∈ ℝ) → ((1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛)))) |
113 | 109, 110,
111, 112 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) ∧ 𝑛 ∈
ℕ) → ((1 / 𝑛)
< ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛)))) |
114 | 9 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) ∧ 𝑛 ∈
ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) = ((∫2‘𝐹) − (1 / 𝑛))) |
115 | 114 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) ∧ 𝑛 ∈
ℕ) → (𝑥 <
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ 𝑥 < ((∫2‘𝐹) − (1 / 𝑛)))) |
116 | 113, 115 | bitr4d 271 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) ∧ 𝑛 ∈
ℕ) → ((1 / 𝑛)
< ((∫2‘𝐹) − 𝑥) ↔ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))) |
117 | 116 | rexbidva 3049 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) → (∃𝑛 ∈ ℕ (1 / 𝑛) < ((∫2‘𝐹) − 𝑥) ↔ ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))) |
118 | 108, 117 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) ∧ ¬
(∫2‘𝐹)
= +∞) → ∃𝑛
∈ ℕ 𝑥 <
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))) |
119 | 100, 118 | pm2.61dan 832 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∧ 𝑥 <
(∫2‘𝐹))) → ∃𝑛 ∈ ℕ 𝑥 < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))) |
120 | 119 | expr 643 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
→ (𝑥 <
(∫2‘𝐹)
→ ∃𝑛 ∈
ℕ 𝑥 <
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))))) |
121 | | rexr 10085 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
122 | | xrltnle 10105 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ (∫2‘𝐹) ∈ ℝ*) → (𝑥 <
(∫2‘𝐹)
↔ ¬ (∫2‘𝐹) ≤ 𝑥)) |
123 | 121, 11, 122 | syl2anr 495 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
→ (𝑥 <
(∫2‘𝐹)
↔ ¬ (∫2‘𝐹) ≤ 𝑥)) |
124 | 121 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑛 ∈ ℕ)
→ 𝑥 ∈
ℝ*) |
125 | 40 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑛 ∈ ℕ)
→ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈
ℝ*) |
126 | | xrltnle 10105 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*) → (𝑥 <
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)) |
127 | 124, 125,
126 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑛 ∈ ℕ)
→ (𝑥 <
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)) |
128 | 127 | rexbidva 3049 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
→ (∃𝑛 ∈
ℕ 𝑥 <
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ∃𝑛 ∈ ℕ ¬
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)) |
129 | | rexnal 2995 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑛 ∈
ℕ ¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ ¬ ∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥) |
130 | 128, 129 | syl6bb 276 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
→ (∃𝑛 ∈
ℕ 𝑥 <
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬ ∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)) |
131 | 120, 123,
130 | 3imtr3d 282 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
→ (¬ (∫2‘𝐹) ≤ 𝑥 → ¬ ∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥)) |
132 | 131 | con4d 114 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
→ (∀𝑛 ∈
ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥)) |
133 | 11 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = +∞) →
(∫2‘𝐹)
∈ ℝ*) |
134 | | pnfge 11964 |
. . . . . . . . . . . . . . 15
⊢
((∫2‘𝐹) ∈ ℝ* →
(∫2‘𝐹)
≤ +∞) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = +∞) →
(∫2‘𝐹)
≤ +∞) |
136 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = +∞) →
𝑥 =
+∞) |
137 | 135, 136 | breqtrrd 4681 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = +∞) →
(∫2‘𝐹)
≤ 𝑥) |
138 | 137 | a1d 25 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = +∞) →
(∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥)) |
139 | | 1nn 11031 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℕ |
140 | 139 | ne0ii 3923 |
. . . . . . . . . . . . . 14
⊢ ℕ
≠ ∅ |
141 | | r19.2z 4060 |
. . . . . . . . . . . . . 14
⊢ ((ℕ
≠ ∅ ∧ ∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥) → ∃𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥) |
142 | 140, 141 | mpan 706 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → ∃𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥) |
143 | 39 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = -∞) ∧
𝑛 ∈ ℕ) →
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ) |
144 | | mnflt 11957 |
. . . . . . . . . . . . . . . . . 18
⊢
(if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → -∞ <
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛)))) |
145 | | rexr 10085 |
. . . . . . . . . . . . . . . . . . 19
⊢
(if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ →
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈
ℝ*) |
146 | | xrltnle 10105 |
. . . . . . . . . . . . . . . . . . 19
⊢
((-∞ ∈ ℝ* ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ*) →
(-∞ < if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞)) |
147 | 16, 145, 146 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
⊢
(if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → (-∞ <
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ↔ ¬
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞)) |
148 | 144, 147 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢
(if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ → ¬
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞) |
149 | 143, 148 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = -∞) ∧
𝑛 ∈ ℕ) →
¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞) |
150 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = -∞) ∧
𝑛 ∈ ℕ) →
𝑥 =
-∞) |
151 | 150 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = -∞) ∧
𝑛 ∈ ℕ) →
(if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ -∞)) |
152 | 149, 151 | mtbird 315 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = -∞) ∧
𝑛 ∈ ℕ) →
¬ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥) |
153 | 152 | nrexdv 3001 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = -∞) →
¬ ∃𝑛 ∈
ℕ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥) |
154 | 153 | pm2.21d 118 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = -∞) →
(∃𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥)) |
155 | 142, 154 | syl5 34 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 = -∞) →
(∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥)) |
156 | 132, 138,
155 | 3jaodan 1394 |
. . . . . . . . . . 11
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
∨ 𝑥 = +∞ ∨
𝑥 = -∞)) →
(∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥)) |
157 | 93, 156 | sylan2b 492 |
. . . . . . . . . 10
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈
ℝ*) → (∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥)) |
158 | 157 | ralrimiva 2966 |
. . . . . . . . 9
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ ∀𝑥 ∈
ℝ* (∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥)) |
159 | 158 | adantr 481 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑥 ∈ ℝ* (∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥)) |
160 | 40 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈
ℝ*) |
161 | 82 | adantll 750 |
. . . . . . . . . . . . . 14
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ℝ) |
162 | 161 | rexrd 10089 |
. . . . . . . . . . . . 13
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈
ℝ*) |
163 | | xrltle 11982 |
. . . . . . . . . . . . 13
⊢
((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ∈ ℝ* ∧
(∫1‘(𝑔‘𝑛)) ∈ ℝ*) →
(if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛)))) |
164 | 160, 162,
163 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛)))) |
165 | 84 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) → (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))):ℕ⟶ℝ) |
166 | 165, 86 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) → ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) ⊆ ℝ) |
167 | 166, 88 | syl6ss 3615 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) → ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) ⊆
ℝ*) |
168 | 167 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) ⊆
ℝ*) |
169 | 78, 168 | syl5eqssr 3650 |
. . . . . . . . . . . . . 14
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))) ⊆
ℝ*) |
170 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = 𝑛 → (𝑔‘𝑚) = (𝑔‘𝑛)) |
171 | 170 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑛 → (∫1‘(𝑔‘𝑚)) = (∫1‘(𝑔‘𝑛))) |
172 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))) = (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))) |
173 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
⊢
(∫1‘(𝑔‘𝑛)) ∈ V |
174 | 171, 172,
173 | fvmpt 6282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚)))‘𝑛) = (∫1‘(𝑔‘𝑛))) |
175 | | fvex 6201 |
. . . . . . . . . . . . . . . . . 18
⊢
(∫1‘(𝑔‘𝑚)) ∈ V |
176 | 175, 172 | fnmpti 6022 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))) Fn ℕ |
177 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))) Fn ℕ ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚)))‘𝑛) ∈ ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚)))) |
178 | 176, 177 | mpan 706 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚)))‘𝑛) ∈ ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚)))) |
179 | 174, 178 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
(∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚)))) |
180 | 179 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → (∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚)))) |
181 | | supxrub 12154 |
. . . . . . . . . . . . . 14
⊢ ((ran
(𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))) ⊆ ℝ* ∧
(∫1‘(𝑔‘𝑛)) ∈ ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚)))) → (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
)) |
182 | 169, 180,
181 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
)) |
183 | 168, 90 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ∈
ℝ*) |
184 | 79, 183 | syl5eqelr 2706 |
. . . . . . . . . . . . . 14
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, < ) ∈
ℝ*) |
185 | | xrletr 11989 |
. . . . . . . . . . . . . 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‘(𝑔‘𝑚))), ℝ*, <
))) |
186 | 160, 162,
184, 185 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → ((if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛)) ∧ (∫1‘(𝑔‘𝑛)) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, < )) →
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
))) |
187 | 182, 186 | mpan2d 710 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ (∫1‘(𝑔‘𝑛)) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
))) |
188 | 164, 187 | syld 47 |
. . . . . . . . . . 11
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → (if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
))) |
189 | 188 | adantld 483 |
. . . . . . . . . 10
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → (((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
))) |
190 | 189 | ralimdva 2962 |
. . . . . . . . 9
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) → (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
))) |
191 | 190 | impr 649 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
)) |
192 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, < ) →
(if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
))) |
193 | 192 | ralbidv 2986 |
. . . . . . . . . 10
⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, < ) →
(∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
))) |
194 | | breq2 4657 |
. . . . . . . . . 10
⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, < ) →
((∫2‘𝐹) ≤ 𝑥 ↔ (∫2‘𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
))) |
195 | 193, 194 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑥 = sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, < ) →
((∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥) ↔ (∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, < ) →
(∫2‘𝐹)
≤ sup(ran (𝑚 ∈
ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, <
)))) |
196 | 195 | rspcv 3305 |
. . . . . . . 8
⊢ (sup(ran
(𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, < ) ∈
ℝ* → (∀𝑥 ∈ ℝ* (∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ 𝑥 → (∫2‘𝐹) ≤ 𝑥) → (∀𝑛 ∈ ℕ
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, < ) →
(∫2‘𝐹)
≤ sup(ran (𝑚 ∈
ℕ ↦ (∫1‘(𝑔‘𝑚))), ℝ*, <
)))) |
197 | 92, 159, 191, 196 | syl3c 66 |
. . . . . . 7
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) ≤ sup(ran (𝑚 ∈ ℕ ↦
(∫1‘(𝑔‘𝑚))), ℝ*, <
)) |
198 | 197, 79 | syl6breqr 4695 |
. . . . . 6
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) ≤ sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, <
)) |
199 | | itg2ub 23500 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔‘𝑛) ∈ dom ∫1
∧ (𝑔‘𝑛) ∘𝑟
≤ 𝐹) →
(∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)) |
200 | 199 | 3expia 1267 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔‘𝑛) ∈ dom ∫1)
→ ((𝑔‘𝑛) ∘𝑟
≤ 𝐹 →
(∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))) |
201 | 80, 200 | sylan2 491 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ 𝑛
∈ ℕ)) → ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 →
(∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))) |
202 | 201 | anassrs 680 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 →
(∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))) |
203 | 202 | adantrd 484 |
. . . . . . . . . . 11
⊢ (((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) ∧ 𝑛
∈ ℕ) → (((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))) |
204 | 203 | ralimdva 2962 |
. . . . . . . . . 10
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) → (∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))) → ∀𝑛 ∈ ℕ
(∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹))) |
205 | 204 | impr 649 |
. . . . . . . . 9
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑛 ∈ ℕ
(∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)) |
206 | 76, 83, 175 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛)))‘𝑚) = (∫1‘(𝑔‘𝑚))) |
207 | 206 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔
(∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹))) |
208 | 207 | ralbiia 2979 |
. . . . . . . . . 10
⊢
(∀𝑚 ∈
ℕ ((𝑛 ∈ ℕ
↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ
(∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹)) |
209 | 76 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → ((∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹) ↔
(∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹))) |
210 | 209 | cbvralv 3171 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
ℕ (∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ
(∫1‘(𝑔‘𝑚)) ≤ (∫2‘𝐹)) |
211 | 208, 210 | bitr4i 267 |
. . . . . . . . 9
⊢
(∀𝑚 ∈
ℕ ((𝑛 ∈ ℕ
↦ (∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹) ↔ ∀𝑛 ∈ ℕ
(∫1‘(𝑔‘𝑛)) ≤ (∫2‘𝐹)) |
212 | 205, 211 | sylibr 224 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹)) |
213 | | ffn 6045 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) Fn ℕ) |
214 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛)))‘𝑚) → (𝑧 ≤ (∫2‘𝐹) ↔ ((𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹))) |
215 | 214 | ralrn 6362 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹))) |
216 | 85, 213, 215 | 3syl 18 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛)))‘𝑚) ≤ (∫2‘𝐹))) |
217 | 212, 216 | mpbird 247 |
. . . . . . 7
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹)) |
218 | 11 | adantr 481 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) ∈
ℝ*) |
219 | | supxrleub 12156 |
. . . . . . . 8
⊢ ((ran
(𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))) ⊆ ℝ* ∧
(∫2‘𝐹)
∈ ℝ*) → (sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤
(∫2‘𝐹)
↔ ∀𝑧 ∈ ran
(𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹))) |
220 | 89, 218, 219 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤
(∫2‘𝐹)
↔ ∀𝑧 ∈ ran
(𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛)))𝑧 ≤ (∫2‘𝐹))) |
221 | 217, 220 | mpbird 247 |
. . . . . 6
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤
(∫2‘𝐹)) |
222 | 11 | adantr 481 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) → (∫2‘𝐹) ∈
ℝ*) |
223 | 167, 90 | syl 17 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) → sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ∈
ℝ*) |
224 | | xrletri3 11985 |
. . . . . . . 8
⊢
(((∫2‘𝐹) ∈ ℝ* ∧ sup(ran
(𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ∈
ℝ*) → ((∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ↔
((∫2‘𝐹) ≤ sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ∧
sup(ran (𝑛 ∈ ℕ
↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤
(∫2‘𝐹)))) |
225 | 222, 223,
224 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ 𝑔:ℕ⟶dom
∫1) → ((∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ↔
((∫2‘𝐹) ≤ sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ∧
sup(ran (𝑛 ∈ ℕ
↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤
(∫2‘𝐹)))) |
226 | 225 | adantrr 753 |
. . . . . 6
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → ((∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ↔
((∫2‘𝐹) ≤ sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, < ) ∧
sup(ran (𝑛 ∈ ℕ
↦ (∫1‘(𝑔‘𝑛))), ℝ*, < ) ≤
(∫2‘𝐹)))) |
227 | 198, 221,
226 | mpbir2and 957 |
. . . . 5
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦
(∫1‘(𝑔‘𝑛))), ℝ*, <
)) |
228 | 71, 74, 227 | 3jca 1242 |
. . . 4
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ (𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛))))) → (𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
(∫2‘𝐹)
= sup(ran (𝑛 ∈ ℕ
↦ (∫1‘(𝑔‘𝑛))), ℝ*, <
))) |
229 | 228 | ex 450 |
. . 3
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ ((𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
((𝑔‘𝑛) ∘𝑟
≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)))) → (𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
(∫2‘𝐹)
= sup(ran (𝑛 ∈ ℕ
↦ (∫1‘(𝑔‘𝑛))), ℝ*, <
)))) |
230 | 229 | eximdv 1846 |
. 2
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ (∃𝑔(𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ ((𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
if((∫2‘𝐹) = +∞, 𝑛, ((∫2‘𝐹) − (1 / 𝑛))) < (∫1‘(𝑔‘𝑛)))) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
(∫2‘𝐹)
= sup(ran (𝑛 ∈ ℕ
↦ (∫1‘(𝑔‘𝑛))), ℝ*, <
)))) |
231 | 70, 230 | mpd 15 |
1
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ ∃𝑔(𝑔:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧
(∫2‘𝐹)
= sup(ran (𝑛 ∈ ℕ
↦ (∫1‘(𝑔‘𝑛))), ℝ*, <
))) |