Proof of Theorem cauappcvgprlemm
Step | Hyp | Ref
| Expression |
1 | | fveq2 5496 |
. . . . . . 7
⊢ (𝑝 = 1Q
→ (𝐹‘𝑝) = (𝐹‘1Q)) |
2 | 1 | breq2d 4001 |
. . . . . 6
⊢ (𝑝 = 1Q
→ (𝐴
<Q (𝐹‘𝑝) ↔ 𝐴 <Q (𝐹‘1Q))) |
3 | | cauappcvgpr.bnd |
. . . . . 6
⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) |
4 | | 1nq 7328 |
. . . . . . 7
⊢
1Q ∈ Q |
5 | 4 | a1i 9 |
. . . . . 6
⊢ (𝜑 →
1Q ∈ Q) |
6 | 2, 3, 5 | rspcdva 2839 |
. . . . 5
⊢ (𝜑 → 𝐴 <Q (𝐹‘1Q)) |
7 | | ltrelnq 7327 |
. . . . . . 7
⊢
<Q ⊆ (Q ×
Q) |
8 | 7 | brel 4663 |
. . . . . 6
⊢ (𝐴 <Q
(𝐹‘1Q) →
(𝐴 ∈ Q
∧ (𝐹‘1Q) ∈
Q)) |
9 | 8 | simpld 111 |
. . . . 5
⊢ (𝐴 <Q
(𝐹‘1Q) →
𝐴 ∈
Q) |
10 | 6, 9 | syl 14 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Q) |
11 | | halfnqq 7372 |
. . . 4
⊢ (𝐴 ∈ Q →
∃𝑠 ∈
Q (𝑠
+Q 𝑠) = 𝐴) |
12 | 10, 11 | syl 14 |
. . 3
⊢ (𝜑 → ∃𝑠 ∈ Q (𝑠 +Q 𝑠) = 𝐴) |
13 | | simplr 525 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → 𝑠 ∈ Q) |
14 | 3 | ad2antrr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) |
15 | | fveq2 5496 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑠 → (𝐹‘𝑝) = (𝐹‘𝑠)) |
16 | 15 | breq2d 4001 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑠 → (𝐴 <Q (𝐹‘𝑝) ↔ 𝐴 <Q (𝐹‘𝑠))) |
17 | 16 | rspcv 2830 |
. . . . . . . . . 10
⊢ (𝑠 ∈ Q →
(∀𝑝 ∈
Q 𝐴
<Q (𝐹‘𝑝) → 𝐴 <Q (𝐹‘𝑠))) |
18 | 17 | ad2antlr 486 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → (∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝) → 𝐴 <Q (𝐹‘𝑠))) |
19 | 14, 18 | mpd 13 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → 𝐴 <Q (𝐹‘𝑠)) |
20 | | breq1 3992 |
. . . . . . . . 9
⊢ ((𝑠 +Q
𝑠) = 𝐴 → ((𝑠 +Q 𝑠) <Q
(𝐹‘𝑠) ↔ 𝐴 <Q (𝐹‘𝑠))) |
21 | 20 | adantl 275 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → ((𝑠 +Q 𝑠) <Q
(𝐹‘𝑠) ↔ 𝐴 <Q (𝐹‘𝑠))) |
22 | 19, 21 | mpbird 166 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → (𝑠 +Q 𝑠) <Q
(𝐹‘𝑠)) |
23 | | oveq2 5861 |
. . . . . . . . 9
⊢ (𝑞 = 𝑠 → (𝑠 +Q 𝑞) = (𝑠 +Q 𝑠)) |
24 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑞 = 𝑠 → (𝐹‘𝑞) = (𝐹‘𝑠)) |
25 | 23, 24 | breq12d 4002 |
. . . . . . . 8
⊢ (𝑞 = 𝑠 → ((𝑠 +Q 𝑞) <Q
(𝐹‘𝑞) ↔ (𝑠 +Q 𝑠) <Q
(𝐹‘𝑠))) |
26 | 25 | rspcev 2834 |
. . . . . . 7
⊢ ((𝑠 ∈ Q ∧
(𝑠
+Q 𝑠) <Q (𝐹‘𝑠)) → ∃𝑞 ∈ Q (𝑠 +Q 𝑞) <Q
(𝐹‘𝑞)) |
27 | 13, 22, 26 | syl2anc 409 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → ∃𝑞 ∈ Q (𝑠 +Q 𝑞) <Q
(𝐹‘𝑞)) |
28 | | oveq1 5860 |
. . . . . . . . 9
⊢ (𝑙 = 𝑠 → (𝑙 +Q 𝑞) = (𝑠 +Q 𝑞)) |
29 | 28 | breq1d 3999 |
. . . . . . . 8
⊢ (𝑙 = 𝑠 → ((𝑙 +Q 𝑞) <Q
(𝐹‘𝑞) ↔ (𝑠 +Q 𝑞) <Q
(𝐹‘𝑞))) |
30 | 29 | rexbidv 2471 |
. . . . . . 7
⊢ (𝑙 = 𝑠 → (∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
(𝐹‘𝑞) ↔ ∃𝑞 ∈ Q (𝑠 +Q 𝑞) <Q
(𝐹‘𝑞))) |
31 | | cauappcvgpr.lim |
. . . . . . . . 9
⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢}〉 |
32 | 31 | fveq2i 5499 |
. . . . . . . 8
⊢
(1st ‘𝐿) = (1st ‘〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢}〉) |
33 | | nqex 7325 |
. . . . . . . . . 10
⊢
Q ∈ V |
34 | 33 | rabex 4133 |
. . . . . . . . 9
⊢ {𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q (𝐹‘𝑞)} ∈ V |
35 | 33 | rabex 4133 |
. . . . . . . . 9
⊢ {𝑢 ∈ Q ∣
∃𝑞 ∈
Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢} ∈
V |
36 | 34, 35 | op1st 6125 |
. . . . . . . 8
⊢
(1st ‘〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢}〉) = {𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q (𝐹‘𝑞)} |
37 | 32, 36 | eqtri 2191 |
. . . . . . 7
⊢
(1st ‘𝐿) = {𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q (𝐹‘𝑞)} |
38 | 30, 37 | elrab2 2889 |
. . . . . 6
⊢ (𝑠 ∈ (1st
‘𝐿) ↔ (𝑠 ∈ Q ∧
∃𝑞 ∈
Q (𝑠
+Q 𝑞) <Q (𝐹‘𝑞))) |
39 | 13, 27, 38 | sylanbrc 415 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → 𝑠 ∈ (1st ‘𝐿)) |
40 | 39 | ex 114 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ Q) → ((𝑠 +Q
𝑠) = 𝐴 → 𝑠 ∈ (1st ‘𝐿))) |
41 | 40 | reximdva 2572 |
. . 3
⊢ (𝜑 → (∃𝑠 ∈ Q (𝑠 +Q 𝑠) = 𝐴 → ∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿))) |
42 | 12, 41 | mpd 13 |
. 2
⊢ (𝜑 → ∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿)) |
43 | | cauappcvgpr.f |
. . . . . 6
⊢ (𝜑 → 𝐹:Q⟶Q) |
44 | 43, 5 | ffvelrnd 5632 |
. . . . 5
⊢ (𝜑 → (𝐹‘1Q) ∈
Q) |
45 | | addclnq 7337 |
. . . . 5
⊢ (((𝐹‘1Q) ∈
Q ∧ 1Q ∈ Q)
→ ((𝐹‘1Q)
+Q 1Q) ∈
Q) |
46 | 44, 5, 45 | syl2anc 409 |
. . . 4
⊢ (𝜑 → ((𝐹‘1Q)
+Q 1Q) ∈
Q) |
47 | | addclnq 7337 |
. . . 4
⊢ ((((𝐹‘1Q)
+Q 1Q) ∈ Q
∧ 1Q ∈ Q) → (((𝐹‘1Q)
+Q 1Q)
+Q 1Q) ∈
Q) |
48 | 46, 5, 47 | syl2anc 409 |
. . 3
⊢ (𝜑 → (((𝐹‘1Q)
+Q 1Q)
+Q 1Q) ∈
Q) |
49 | | ltaddnq 7369 |
. . . . . 6
⊢ ((((𝐹‘1Q)
+Q 1Q) ∈ Q
∧ 1Q ∈ Q) → ((𝐹‘1Q)
+Q 1Q)
<Q (((𝐹‘1Q)
+Q 1Q)
+Q 1Q)) |
50 | 46, 5, 49 | syl2anc 409 |
. . . . 5
⊢ (𝜑 → ((𝐹‘1Q)
+Q 1Q)
<Q (((𝐹‘1Q)
+Q 1Q)
+Q 1Q)) |
51 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑞 = 1Q
→ (𝐹‘𝑞) = (𝐹‘1Q)) |
52 | | id 19 |
. . . . . . . 8
⊢ (𝑞 = 1Q
→ 𝑞 =
1Q) |
53 | 51, 52 | oveq12d 5871 |
. . . . . . 7
⊢ (𝑞 = 1Q
→ ((𝐹‘𝑞) +Q
𝑞) = ((𝐹‘1Q)
+Q 1Q)) |
54 | 53 | breq1d 3999 |
. . . . . 6
⊢ (𝑞 = 1Q
→ (((𝐹‘𝑞) +Q
𝑞)
<Q (((𝐹‘1Q)
+Q 1Q)
+Q 1Q) ↔ ((𝐹‘1Q)
+Q 1Q)
<Q (((𝐹‘1Q)
+Q 1Q)
+Q 1Q))) |
55 | 54 | rspcev 2834 |
. . . . 5
⊢
((1Q ∈ Q ∧ ((𝐹‘1Q)
+Q 1Q)
<Q (((𝐹‘1Q)
+Q 1Q)
+Q 1Q)) → ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
(((𝐹‘1Q)
+Q 1Q)
+Q 1Q)) |
56 | 5, 50, 55 | syl2anc 409 |
. . . 4
⊢ (𝜑 → ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
(((𝐹‘1Q)
+Q 1Q)
+Q 1Q)) |
57 | | breq2 3993 |
. . . . . 6
⊢ (𝑢 = (((𝐹‘1Q)
+Q 1Q)
+Q 1Q) → (((𝐹‘𝑞) +Q 𝑞) <Q
𝑢 ↔ ((𝐹‘𝑞) +Q 𝑞) <Q
(((𝐹‘1Q)
+Q 1Q)
+Q 1Q))) |
58 | 57 | rexbidv 2471 |
. . . . 5
⊢ (𝑢 = (((𝐹‘1Q)
+Q 1Q)
+Q 1Q) → (∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢 ↔ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
(((𝐹‘1Q)
+Q 1Q)
+Q 1Q))) |
59 | 31 | fveq2i 5499 |
. . . . . 6
⊢
(2nd ‘𝐿) = (2nd ‘〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢}〉) |
60 | 34, 35 | op2nd 6126 |
. . . . . 6
⊢
(2nd ‘〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢}〉) = {𝑢 ∈ Q ∣
∃𝑞 ∈
Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢} |
61 | 59, 60 | eqtri 2191 |
. . . . 5
⊢
(2nd ‘𝐿) = {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢} |
62 | 58, 61 | elrab2 2889 |
. . . 4
⊢ ((((𝐹‘1Q)
+Q 1Q)
+Q 1Q) ∈ (2nd
‘𝐿) ↔ ((((𝐹‘1Q)
+Q 1Q)
+Q 1Q) ∈ Q
∧ ∃𝑞 ∈
Q ((𝐹‘𝑞) +Q 𝑞) <Q
(((𝐹‘1Q)
+Q 1Q)
+Q 1Q))) |
63 | 48, 56, 62 | sylanbrc 415 |
. . 3
⊢ (𝜑 → (((𝐹‘1Q)
+Q 1Q)
+Q 1Q) ∈ (2nd
‘𝐿)) |
64 | | eleq1 2233 |
. . . 4
⊢ (𝑟 = (((𝐹‘1Q)
+Q 1Q)
+Q 1Q) → (𝑟 ∈ (2nd
‘𝐿) ↔ (((𝐹‘1Q)
+Q 1Q)
+Q 1Q) ∈ (2nd
‘𝐿))) |
65 | 64 | rspcev 2834 |
. . 3
⊢
(((((𝐹‘1Q)
+Q 1Q)
+Q 1Q) ∈ Q
∧ (((𝐹‘1Q)
+Q 1Q)
+Q 1Q) ∈ (2nd
‘𝐿)) →
∃𝑟 ∈
Q 𝑟 ∈
(2nd ‘𝐿)) |
66 | 48, 63, 65 | syl2anc 409 |
. 2
⊢ (𝜑 → ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐿)) |
67 | 42, 66 | jca 304 |
1
⊢ (𝜑 → (∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd
‘𝐿))) |