Step | Hyp | Ref
| Expression |
1 | | lo1add.3 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) |
2 | | lo1add.4 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1)) |
3 | | reeanv 3279 |
. . . 4
⊢
(∃𝑚 ∈
ℝ ∃𝑛 ∈
ℝ (∃𝑐 ∈
ℝ ∀𝑥 ∈
𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)) ↔ (∃𝑚 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛))) |
4 | | o1add2.1 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
5 | 4 | ralrimiva 3105 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) |
6 | | dmmptg 6105 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
8 | | lo1dm 15080 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ℝ) |
9 | 1, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ℝ) |
10 | 7, 9 | eqsstrrd 3940 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
11 | 10 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐴 ⊆ ℝ) |
12 | | rexanre 14910 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ →
(∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛)) ↔ (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)))) |
13 | 11, 12 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛)) ↔ (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)))) |
14 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑚 ∈ ℝ) |
15 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝑛 ∈ ℝ) |
16 | | 0re 10835 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
17 | | ifcl 4484 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝑛, 𝑛, 0) ∈ ℝ) |
18 | 15, 16, 17 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → if(0 ≤ 𝑛, 𝑛, 0) ∈ ℝ) |
19 | 14, 18 | remulcld 10863 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝑚 · if(0 ≤ 𝑛, 𝑛, 0)) ∈ ℝ) |
20 | | simplrr 778 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → 𝑛 ∈ ℝ) |
21 | | max2 12777 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 𝑛
∈ ℝ) → 𝑛
≤ if(0 ≤ 𝑛, 𝑛, 0)) |
22 | 16, 20, 21 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → 𝑛 ≤ if(0 ≤ 𝑛, 𝑛, 0)) |
23 | | o1add2.2 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) |
24 | 23, 2 | lo1mptrcl 15183 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) |
25 | 24 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) |
26 | 20, 16, 17 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝑛, 𝑛, 0) ∈ ℝ) |
27 | | letr 10926 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ if(0 ≤
𝑛, 𝑛, 0) ∈ ℝ) → ((𝐶 ≤ 𝑛 ∧ 𝑛 ≤ if(0 ≤ 𝑛, 𝑛, 0)) → 𝐶 ≤ if(0 ≤ 𝑛, 𝑛, 0))) |
28 | 25, 20, 26, 27 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → ((𝐶 ≤ 𝑛 ∧ 𝑛 ≤ if(0 ≤ 𝑛, 𝑛, 0)) → 𝐶 ≤ if(0 ≤ 𝑛, 𝑛, 0))) |
29 | 22, 28 | mpan2d 694 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → (𝐶 ≤ 𝑛 → 𝐶 ≤ if(0 ≤ 𝑛, 𝑛, 0))) |
30 | 4, 1 | lo1mptrcl 15183 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
31 | 30 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
32 | | lo1mul.5 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) |
33 | 32 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) |
34 | 31, 33 | jca 515 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) |
35 | | simplrl 777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → 𝑚 ∈ ℝ) |
36 | | max1 12775 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ 𝑛
∈ ℝ) → 0 ≤ if(0 ≤ 𝑛, 𝑛, 0)) |
37 | 16, 20, 36 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝑛, 𝑛, 0)) |
38 | 26, 37 | jca 515 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝑛, 𝑛, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
𝑛, 𝑛, 0))) |
39 | | lemul12b 11689 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) ∧ 𝑚 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (if(0 ≤ 𝑛, 𝑛, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
𝑛, 𝑛, 0)))) → ((𝐵 ≤ 𝑚 ∧ 𝐶 ≤ if(0 ≤ 𝑛, 𝑛, 0)) → (𝐵 · 𝐶) ≤ (𝑚 · if(0 ≤ 𝑛, 𝑛, 0)))) |
40 | 34, 35, 25, 38, 39 | syl22anc 839 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ≤ 𝑚 ∧ 𝐶 ≤ if(0 ≤ 𝑛, 𝑛, 0)) → (𝐵 · 𝐶) ≤ (𝑚 · if(0 ≤ 𝑛, 𝑛, 0)))) |
41 | 29, 40 | sylan2d 608 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛) → (𝐵 · 𝐶) ≤ (𝑚 · if(0 ≤ 𝑛, 𝑛, 0)))) |
42 | 41 | imim2d 57 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → ((𝑐 ≤ 𝑥 → (𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛)) → (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ (𝑚 · if(0 ≤ 𝑛, 𝑛, 0))))) |
43 | 42 | ralimdva 3100 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛)) → ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ (𝑚 · if(0 ≤ 𝑛, 𝑛, 0))))) |
44 | | breq2 5057 |
. . . . . . . . . . 11
⊢ (𝑝 = (𝑚 · if(0 ≤ 𝑛, 𝑛, 0)) → ((𝐵 · 𝐶) ≤ 𝑝 ↔ (𝐵 · 𝐶) ≤ (𝑚 · if(0 ≤ 𝑛, 𝑛, 0)))) |
45 | 44 | imbi2d 344 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑚 · if(0 ≤ 𝑛, 𝑛, 0)) → ((𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ 𝑝) ↔ (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ (𝑚 · if(0 ≤ 𝑛, 𝑛, 0))))) |
46 | 45 | ralbidv 3118 |
. . . . . . . . 9
⊢ (𝑝 = (𝑚 · if(0 ≤ 𝑛, 𝑛, 0)) → (∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ 𝑝) ↔ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ (𝑚 · if(0 ≤ 𝑛, 𝑛, 0))))) |
47 | 46 | rspcev 3537 |
. . . . . . . 8
⊢ (((𝑚 · if(0 ≤ 𝑛, 𝑛, 0)) ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ (𝑚 · if(0 ≤ 𝑛, 𝑛, 0)))) → ∃𝑝 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ 𝑝)) |
48 | 19, 43, 47 | syl6an 684 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛)) → ∃𝑝 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ 𝑝))) |
49 | 48 | reximdv 3192 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛)) → ∃𝑐 ∈ ℝ ∃𝑝 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ 𝑝))) |
50 | 13, 49 | sylbird 263 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → ((∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)) → ∃𝑐 ∈ ℝ ∃𝑝 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ 𝑝))) |
51 | 50 | rexlimdvva 3213 |
. . . 4
⊢ (𝜑 → (∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)) → ∃𝑐 ∈ ℝ ∃𝑝 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ 𝑝))) |
52 | 3, 51 | syl5bir 246 |
. . 3
⊢ (𝜑 → ((∃𝑚 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)) → ∃𝑐 ∈ ℝ ∃𝑝 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ 𝑝))) |
53 | 10, 30 | ello1mpt 15082 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔
∃𝑐 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚))) |
54 | | rexcom 3268 |
. . . . 5
⊢
(∃𝑐 ∈
ℝ ∃𝑚 ∈
ℝ ∀𝑥 ∈
𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ↔ ∃𝑚 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚)) |
55 | 53, 54 | bitrdi 290 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔
∃𝑚 ∈ ℝ
∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚))) |
56 | 10, 24 | ello1mpt 15082 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1) ↔
∃𝑐 ∈ ℝ
∃𝑛 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛))) |
57 | | rexcom 3268 |
. . . . 5
⊢
(∃𝑐 ∈
ℝ ∃𝑛 ∈
ℝ ∀𝑥 ∈
𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛) ↔ ∃𝑛 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)) |
58 | 56, 57 | bitrdi 290 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1) ↔
∃𝑛 ∈ ℝ
∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛))) |
59 | 55, 58 | anbi12d 634 |
. . 3
⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1)) ↔
(∃𝑚 ∈ ℝ
∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)))) |
60 | 30, 24 | remulcld 10863 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 · 𝐶) ∈ ℝ) |
61 | 10, 60 | ello1mpt 15082 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∈ ≤𝑂(1) ↔
∃𝑐 ∈ ℝ
∃𝑝 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 · 𝐶) ≤ 𝑝))) |
62 | 52, 59, 61 | 3imtr4d 297 |
. 2
⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1)) → (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∈
≤𝑂(1))) |
63 | 1, 2, 62 | mp2and 699 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) ∈ ≤𝑂(1)) |