Proof of Theorem ioombl1lem1
Step | Hyp | Ref
| Expression |
1 | | ioombl1.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | 1 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ) |
3 | | ioombl1.p |
. . . . . . . 8
⊢ 𝑃 = (1st ‘(𝐹‘𝑛)) |
4 | | ioombl1.f1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
5 | | ovolfcl 23681 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
6 | 4, 5 | sylan 575 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
7 | 6 | simp1d 1133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) |
8 | 3, 7 | syl5eqel 2863 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ) |
9 | 2, 8 | ifcld 4352 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ) |
10 | | ioombl1.q |
. . . . . . 7
⊢ 𝑄 = (2nd ‘(𝐹‘𝑛)) |
11 | 6 | simp2d 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) |
12 | 10, 11 | syl5eqel 2863 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ) |
13 | | min2 12338 |
. . . . . 6
⊢
((if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ ∧ 𝑄 ∈ ℝ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ 𝑄) |
14 | 9, 12, 13 | syl2anc 579 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ 𝑄) |
15 | | df-br 4889 |
. . . . 5
⊢
(if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ 𝑄 ↔ 〈if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉 ∈ ≤ ) |
16 | 14, 15 | sylib 210 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉 ∈ ≤ ) |
17 | 9, 12 | ifcld 4352 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) |
18 | | opelxpi 5394 |
. . . . 5
⊢
((if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → 〈if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉 ∈ (ℝ ×
ℝ)) |
19 | 17, 12, 18 | syl2anc 579 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉 ∈ (ℝ ×
ℝ)) |
20 | 16, 19 | elind 4021 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉 ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
21 | | ioombl1.g |
. . 3
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉) |
22 | 20, 21 | fmptd 6650 |
. 2
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
23 | | max1 12333 |
. . . . . . 7
⊢ ((𝑃 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 𝑃 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃)) |
24 | 8, 2, 23 | syl2anc 579 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃)) |
25 | 6 | simp3d 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) |
26 | 25, 3, 10 | 3brtr4g 4922 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ≤ 𝑄) |
27 | | breq2 4892 |
. . . . . . 7
⊢ (if(𝑃 ≤ 𝐴, 𝐴, 𝑃) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) → (𝑃 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ↔ 𝑃 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))) |
28 | | breq2 4892 |
. . . . . . 7
⊢ (𝑄 = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) → (𝑃 ≤ 𝑄 ↔ 𝑃 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))) |
29 | 27, 28 | ifboth 4345 |
. . . . . 6
⊢ ((𝑃 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∧ 𝑃 ≤ 𝑄) → 𝑃 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)) |
30 | 24, 26, 29 | syl2anc 579 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)) |
31 | | df-br 4889 |
. . . . 5
⊢ (𝑃 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ↔ 〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉 ∈ ≤ ) |
32 | 30, 31 | sylib 210 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉 ∈ ≤ ) |
33 | | opelxpi 5394 |
. . . . 5
⊢ ((𝑃 ∈ ℝ ∧
if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → 〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉 ∈ (ℝ ×
ℝ)) |
34 | 8, 17, 33 | syl2anc 579 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉 ∈ (ℝ ×
ℝ)) |
35 | 32, 34 | elind 4021 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉 ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
36 | | ioombl1.h |
. . 3
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ 〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉) |
37 | 35, 36 | fmptd 6650 |
. 2
⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
38 | 22, 37 | jca 507 |
1
⊢ (𝜑 → (𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ)))) |