Step | Hyp | Ref
| Expression |
1 | | cauappcvgpr.f |
. . 3
⊢ (𝜑 → 𝐹:Q⟶Q) |
2 | | cauappcvgpr.app |
. . 3
⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q
𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q
𝑞)))) |
3 | | cauappcvgpr.bnd |
. . 3
⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) |
4 | | oveq2 5885 |
. . . . . . . 8
⊢ (𝑧 = 𝑞 → (𝑙 +Q 𝑧) = (𝑙 +Q 𝑞)) |
5 | | fveq2 5517 |
. . . . . . . 8
⊢ (𝑧 = 𝑞 → (𝐹‘𝑧) = (𝐹‘𝑞)) |
6 | 4, 5 | breq12d 4018 |
. . . . . . 7
⊢ (𝑧 = 𝑞 → ((𝑙 +Q 𝑧) <Q
(𝐹‘𝑧) ↔ (𝑙 +Q 𝑞) <Q
(𝐹‘𝑞))) |
7 | 6 | cbvrexv 2706 |
. . . . . 6
⊢
(∃𝑧 ∈
Q (𝑙
+Q 𝑧) <Q (𝐹‘𝑧) ↔ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
(𝐹‘𝑞)) |
8 | 7 | a1i 9 |
. . . . 5
⊢ (𝑙 ∈ Q →
(∃𝑧 ∈
Q (𝑙
+Q 𝑧) <Q (𝐹‘𝑧) ↔ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
(𝐹‘𝑞))) |
9 | 8 | rabbiia 2724 |
. . . 4
⊢ {𝑙 ∈ Q ∣
∃𝑧 ∈
Q (𝑙
+Q 𝑧) <Q (𝐹‘𝑧)} = {𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q (𝐹‘𝑞)} |
10 | | id 19 |
. . . . . . . . 9
⊢ (𝑧 = 𝑞 → 𝑧 = 𝑞) |
11 | 5, 10 | oveq12d 5895 |
. . . . . . . 8
⊢ (𝑧 = 𝑞 → ((𝐹‘𝑧) +Q 𝑧) = ((𝐹‘𝑞) +Q 𝑞)) |
12 | 11 | breq1d 4015 |
. . . . . . 7
⊢ (𝑧 = 𝑞 → (((𝐹‘𝑧) +Q 𝑧) <Q
𝑢 ↔ ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢)) |
13 | 12 | cbvrexv 2706 |
. . . . . 6
⊢
(∃𝑧 ∈
Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢 ↔ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢) |
14 | 13 | a1i 9 |
. . . . 5
⊢ (𝑢 ∈ Q →
(∃𝑧 ∈
Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢 ↔ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢)) |
15 | 14 | rabbiia 2724 |
. . . 4
⊢ {𝑢 ∈ Q ∣
∃𝑧 ∈
Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢} = {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢} |
16 | 9, 15 | opeq12i 3785 |
. . 3
⊢
⟨{𝑙 ∈
Q ∣ ∃𝑧 ∈ Q (𝑙 +Q 𝑧) <Q
(𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩ = ⟨{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢}⟩ |
17 | 1, 2, 3, 16 | cauappcvgprlemcl 7654 |
. 2
⊢ (𝜑 → ⟨{𝑙 ∈ Q ∣ ∃𝑧 ∈ Q (𝑙 +Q
𝑧)
<Q (𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩ ∈
P) |
18 | 1, 2, 3, 16 | cauappcvgprlemlim 7662 |
. 2
⊢ (𝜑 → ∀𝑞 ∈ Q ∀𝑟 ∈ Q
(⟨{𝑙 ∣ 𝑙 <Q
(𝐹‘𝑞)}, {𝑢 ∣ (𝐹‘𝑞) <Q 𝑢}⟩<P
(⟨{𝑙 ∈
Q ∣ ∃𝑧 ∈ Q (𝑙 +Q 𝑧) <Q
(𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q (𝑞 +Q
𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q
𝑢}⟩) ∧
⟨{𝑙 ∈
Q ∣ ∃𝑧 ∈ Q (𝑙 +Q 𝑧) <Q
(𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩<P
⟨{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑞) +Q
(𝑞
+Q 𝑟))}, {𝑢 ∣ ((𝐹‘𝑞) +Q (𝑞 +Q
𝑟))
<Q 𝑢}⟩)) |
19 | | oveq1 5884 |
. . . . . 6
⊢ (𝑦 = ⟨{𝑙 ∈ Q ∣ ∃𝑧 ∈ Q (𝑙 +Q
𝑧)
<Q (𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩ → (𝑦 +P
⟨{𝑙 ∣ 𝑙 <Q
(𝑞
+Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q
𝑢}⟩) = (⟨{𝑙 ∈ Q ∣
∃𝑧 ∈
Q (𝑙
+Q 𝑧) <Q (𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q (𝑞 +Q
𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q
𝑢}⟩)) |
20 | 19 | breq2d 4017 |
. . . . 5
⊢ (𝑦 = ⟨{𝑙 ∈ Q ∣ ∃𝑧 ∈ Q (𝑙 +Q
𝑧)
<Q (𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩ →
(⟨{𝑙 ∣ 𝑙 <Q
(𝐹‘𝑞)}, {𝑢 ∣ (𝐹‘𝑞) <Q 𝑢}⟩<P (𝑦 +P
⟨{𝑙 ∣ 𝑙 <Q
(𝑞
+Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q
𝑢}⟩) ↔
⟨{𝑙 ∣ 𝑙 <Q
(𝐹‘𝑞)}, {𝑢 ∣ (𝐹‘𝑞) <Q 𝑢}⟩<P
(⟨{𝑙 ∈
Q ∣ ∃𝑧 ∈ Q (𝑙 +Q 𝑧) <Q
(𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q (𝑞 +Q
𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q
𝑢}⟩))) |
21 | | breq1 4008 |
. . . . 5
⊢ (𝑦 = ⟨{𝑙 ∈ Q ∣ ∃𝑧 ∈ Q (𝑙 +Q
𝑧)
<Q (𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩ → (𝑦<P
⟨{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑞) +Q
(𝑞
+Q 𝑟))}, {𝑢 ∣ ((𝐹‘𝑞) +Q (𝑞 +Q
𝑟))
<Q 𝑢}⟩ ↔ ⟨{𝑙 ∈ Q ∣ ∃𝑧 ∈ Q (𝑙 +Q
𝑧)
<Q (𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩<P
⟨{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑞) +Q
(𝑞
+Q 𝑟))}, {𝑢 ∣ ((𝐹‘𝑞) +Q (𝑞 +Q
𝑟))
<Q 𝑢}⟩)) |
22 | 20, 21 | anbi12d 473 |
. . . 4
⊢ (𝑦 = ⟨{𝑙 ∈ Q ∣ ∃𝑧 ∈ Q (𝑙 +Q
𝑧)
<Q (𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩ →
((⟨{𝑙 ∣ 𝑙 <Q
(𝐹‘𝑞)}, {𝑢 ∣ (𝐹‘𝑞) <Q 𝑢}⟩<P (𝑦 +P
⟨{𝑙 ∣ 𝑙 <Q
(𝑞
+Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q
𝑢}⟩) ∧ 𝑦<P
⟨{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑞) +Q
(𝑞
+Q 𝑟))}, {𝑢 ∣ ((𝐹‘𝑞) +Q (𝑞 +Q
𝑟))
<Q 𝑢}⟩) ↔ (⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝑞)}, {𝑢 ∣ (𝐹‘𝑞) <Q 𝑢}⟩<P
(⟨{𝑙 ∈
Q ∣ ∃𝑧 ∈ Q (𝑙 +Q 𝑧) <Q
(𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q (𝑞 +Q
𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q
𝑢}⟩) ∧
⟨{𝑙 ∈
Q ∣ ∃𝑧 ∈ Q (𝑙 +Q 𝑧) <Q
(𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩<P
⟨{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑞) +Q
(𝑞
+Q 𝑟))}, {𝑢 ∣ ((𝐹‘𝑞) +Q (𝑞 +Q
𝑟))
<Q 𝑢}⟩))) |
23 | 22 | 2ralbidv 2501 |
. . 3
⊢ (𝑦 = ⟨{𝑙 ∈ Q ∣ ∃𝑧 ∈ Q (𝑙 +Q
𝑧)
<Q (𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩ →
(∀𝑞 ∈
Q ∀𝑟
∈ Q (⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝑞)}, {𝑢 ∣ (𝐹‘𝑞) <Q 𝑢}⟩<P (𝑦 +P
⟨{𝑙 ∣ 𝑙 <Q
(𝑞
+Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q
𝑢}⟩) ∧ 𝑦<P
⟨{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑞) +Q
(𝑞
+Q 𝑟))}, {𝑢 ∣ ((𝐹‘𝑞) +Q (𝑞 +Q
𝑟))
<Q 𝑢}⟩) ↔ ∀𝑞 ∈ Q ∀𝑟 ∈ Q
(⟨{𝑙 ∣ 𝑙 <Q
(𝐹‘𝑞)}, {𝑢 ∣ (𝐹‘𝑞) <Q 𝑢}⟩<P
(⟨{𝑙 ∈
Q ∣ ∃𝑧 ∈ Q (𝑙 +Q 𝑧) <Q
(𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q (𝑞 +Q
𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q
𝑢}⟩) ∧
⟨{𝑙 ∈
Q ∣ ∃𝑧 ∈ Q (𝑙 +Q 𝑧) <Q
(𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩<P
⟨{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑞) +Q
(𝑞
+Q 𝑟))}, {𝑢 ∣ ((𝐹‘𝑞) +Q (𝑞 +Q
𝑟))
<Q 𝑢}⟩))) |
24 | 23 | rspcev 2843 |
. 2
⊢
((⟨{𝑙 ∈
Q ∣ ∃𝑧 ∈ Q (𝑙 +Q 𝑧) <Q
(𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩ ∈
P ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q
(⟨{𝑙 ∣ 𝑙 <Q
(𝐹‘𝑞)}, {𝑢 ∣ (𝐹‘𝑞) <Q 𝑢}⟩<P
(⟨{𝑙 ∈
Q ∣ ∃𝑧 ∈ Q (𝑙 +Q 𝑧) <Q
(𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q (𝑞 +Q
𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q
𝑢}⟩) ∧
⟨{𝑙 ∈
Q ∣ ∃𝑧 ∈ Q (𝑙 +Q 𝑧) <Q
(𝐹‘𝑧)}, {𝑢 ∈ Q ∣ ∃𝑧 ∈ Q ((𝐹‘𝑧) +Q 𝑧) <Q
𝑢}⟩<P
⟨{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑞) +Q
(𝑞
+Q 𝑟))}, {𝑢 ∣ ((𝐹‘𝑞) +Q (𝑞 +Q
𝑟))
<Q 𝑢}⟩)) → ∃𝑦 ∈ P ∀𝑞 ∈ Q
∀𝑟 ∈
Q (⟨{𝑙
∣ 𝑙
<Q (𝐹‘𝑞)}, {𝑢 ∣ (𝐹‘𝑞) <Q 𝑢}⟩<P (𝑦 +P
⟨{𝑙 ∣ 𝑙 <Q
(𝑞
+Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q
𝑢}⟩) ∧ 𝑦<P
⟨{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑞) +Q
(𝑞
+Q 𝑟))}, {𝑢 ∣ ((𝐹‘𝑞) +Q (𝑞 +Q
𝑟))
<Q 𝑢}⟩)) |
25 | 17, 18, 24 | syl2anc 411 |
1
⊢ (𝜑 → ∃𝑦 ∈ P ∀𝑞 ∈ Q
∀𝑟 ∈
Q (⟨{𝑙
∣ 𝑙
<Q (𝐹‘𝑞)}, {𝑢 ∣ (𝐹‘𝑞) <Q 𝑢}⟩<P (𝑦 +P
⟨{𝑙 ∣ 𝑙 <Q
(𝑞
+Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q
𝑢}⟩) ∧ 𝑦<P
⟨{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑞) +Q
(𝑞
+Q 𝑟))}, {𝑢 ∣ ((𝐹‘𝑞) +Q (𝑞 +Q
𝑟))
<Q 𝑢}⟩)) |