Step | Hyp | Ref
| Expression |
1 | | cauappcvgprlem.q |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ Q) |
2 | | cauappcvgprlem.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Q) |
3 | | ltaddnq 7369 |
. . . . 5
⊢ ((𝑄 ∈ Q ∧
𝑅 ∈ Q)
→ 𝑄
<Q (𝑄 +Q 𝑅)) |
4 | 1, 2, 3 | syl2anc 409 |
. . . 4
⊢ (𝜑 → 𝑄 <Q (𝑄 +Q
𝑅)) |
5 | | cauappcvgpr.f |
. . . . 5
⊢ (𝜑 → 𝐹:Q⟶Q) |
6 | 5, 1 | ffvelrnd 5632 |
. . . 4
⊢ (𝜑 → (𝐹‘𝑄) ∈ Q) |
7 | | ltanqi 7364 |
. . . 4
⊢ ((𝑄 <Q
(𝑄
+Q 𝑅) ∧ (𝐹‘𝑄) ∈ Q) → ((𝐹‘𝑄) +Q 𝑄) <Q
((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))) |
8 | 4, 6, 7 | syl2anc 409 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑄) +Q 𝑄) <Q
((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))) |
9 | | ltbtwnnqq 7377 |
. . 3
⊢ (((𝐹‘𝑄) +Q 𝑄) <Q
((𝐹‘𝑄) +Q (𝑄 +Q
𝑅)) ↔ ∃𝑥 ∈ Q (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅)))) |
10 | 8, 9 | sylib 121 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ Q (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅)))) |
11 | | simprl 526 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → 𝑥 ∈
Q) |
12 | 1 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → 𝑄 ∈
Q) |
13 | | simprrl 534 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → ((𝐹‘𝑄) +Q 𝑄) <Q
𝑥) |
14 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑞 = 𝑄 → (𝐹‘𝑞) = (𝐹‘𝑄)) |
15 | | id 19 |
. . . . . . . . 9
⊢ (𝑞 = 𝑄 → 𝑞 = 𝑄) |
16 | 14, 15 | oveq12d 5871 |
. . . . . . . 8
⊢ (𝑞 = 𝑄 → ((𝐹‘𝑞) +Q 𝑞) = ((𝐹‘𝑄) +Q 𝑄)) |
17 | 16 | breq1d 3999 |
. . . . . . 7
⊢ (𝑞 = 𝑄 → (((𝐹‘𝑞) +Q 𝑞) <Q
𝑥 ↔ ((𝐹‘𝑄) +Q 𝑄) <Q
𝑥)) |
18 | 17 | rspcev 2834 |
. . . . . 6
⊢ ((𝑄 ∈ Q ∧
((𝐹‘𝑄) +Q 𝑄) <Q
𝑥) → ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑥) |
19 | 12, 13, 18 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑥) |
20 | | breq2 3993 |
. . . . . . 7
⊢ (𝑢 = 𝑥 → (((𝐹‘𝑞) +Q 𝑞) <Q
𝑢 ↔ ((𝐹‘𝑞) +Q 𝑞) <Q
𝑥)) |
21 | 20 | rexbidv 2471 |
. . . . . 6
⊢ (𝑢 = 𝑥 → (∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢 ↔ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑥)) |
22 | | cauappcvgpr.lim |
. . . . . . . 8
⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢}〉 |
23 | 22 | fveq2i 5499 |
. . . . . . 7
⊢
(2nd ‘𝐿) = (2nd ‘〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢}〉) |
24 | | nqex 7325 |
. . . . . . . . 9
⊢
Q ∈ V |
25 | 24 | rabex 4133 |
. . . . . . . 8
⊢ {𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q (𝐹‘𝑞)} ∈ V |
26 | 24 | rabex 4133 |
. . . . . . . 8
⊢ {𝑢 ∈ Q ∣
∃𝑞 ∈
Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢} ∈
V |
27 | 25, 26 | op2nd 6126 |
. . . . . . 7
⊢
(2nd ‘〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢}〉) = {𝑢 ∈ Q ∣
∃𝑞 ∈
Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢} |
28 | 23, 27 | eqtri 2191 |
. . . . . 6
⊢
(2nd ‘𝐿) = {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢} |
29 | 21, 28 | elrab2 2889 |
. . . . 5
⊢ (𝑥 ∈ (2nd
‘𝐿) ↔ (𝑥 ∈ Q ∧
∃𝑞 ∈
Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑥)) |
30 | 11, 19, 29 | sylanbrc 415 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → 𝑥 ∈ (2nd
‘𝐿)) |
31 | | simprrr 535 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → 𝑥 <Q
((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))) |
32 | | vex 2733 |
. . . . . . 7
⊢ 𝑥 ∈ V |
33 | | breq1 3992 |
. . . . . . 7
⊢ (𝑙 = 𝑥 → (𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅)) ↔ 𝑥 <Q
((𝐹‘𝑄) +Q (𝑄 +Q
𝑅)))) |
34 | 32, 33 | elab 2874 |
. . . . . 6
⊢ (𝑥 ∈ {𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))} ↔ 𝑥 <Q
((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))) |
35 | 31, 34 | sylibr 133 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → 𝑥 ∈ {𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}) |
36 | | ltnqex 7511 |
. . . . . 6
⊢ {𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))} ∈
V |
37 | | gtnqex 7512 |
. . . . . 6
⊢ {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢} ∈ V |
38 | 36, 37 | op1st 6125 |
. . . . 5
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉) = {𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))} |
39 | 35, 38 | eleqtrrdi 2264 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉)) |
40 | | rspe 2519 |
. . . 4
⊢ ((𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘𝐿) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉))) → ∃𝑥 ∈ Q (𝑥 ∈ (2nd ‘𝐿) ∧ 𝑥 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉))) |
41 | 11, 30, 39, 40 | syl12anc 1231 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘𝐿) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉))) |
42 | | cauappcvgpr.app |
. . . . . 6
⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q
𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q
𝑞)))) |
43 | | cauappcvgpr.bnd |
. . . . . 6
⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) |
44 | 5, 42, 43, 22 | cauappcvgprlemcl 7615 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ P) |
45 | 44 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → 𝐿 ∈
P) |
46 | | addclnq 7337 |
. . . . . . . 8
⊢ ((𝑄 ∈ Q ∧
𝑅 ∈ Q)
→ (𝑄
+Q 𝑅) ∈ Q) |
47 | 1, 2, 46 | syl2anc 409 |
. . . . . . 7
⊢ (𝜑 → (𝑄 +Q 𝑅) ∈
Q) |
48 | | addclnq 7337 |
. . . . . . 7
⊢ (((𝐹‘𝑄) ∈ Q ∧ (𝑄 +Q
𝑅) ∈ Q)
→ ((𝐹‘𝑄) +Q
(𝑄
+Q 𝑅)) ∈ Q) |
49 | 6, 47, 48 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅)) ∈
Q) |
50 | | nqprlu 7509 |
. . . . . 6
⊢ (((𝐹‘𝑄) +Q (𝑄 +Q
𝑅)) ∈ Q
→ 〈{𝑙 ∣
𝑙
<Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉 ∈
P) |
51 | 49, 50 | syl 14 |
. . . . 5
⊢ (𝜑 → 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉 ∈
P) |
52 | 51 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉 ∈
P) |
53 | | ltdfpr 7468 |
. . . 4
⊢ ((𝐿 ∈ P ∧
〈{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉 ∈ P) → (𝐿<P
〈{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉 ↔ ∃𝑥 ∈ Q (𝑥 ∈ (2nd ‘𝐿) ∧ 𝑥 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉)))) |
54 | 45, 52, 53 | syl2anc 409 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → (𝐿<P
〈{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉 ↔ ∃𝑥 ∈ Q (𝑥 ∈ (2nd ‘𝐿) ∧ 𝑥 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉)))) |
55 | 41, 54 | mpbird 166 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝑄) +Q 𝑄) <Q
𝑥 ∧ 𝑥 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))))) → 𝐿<P
〈{𝑙 ∣ 𝑙 <Q
((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉) |
56 | 10, 55 | rexlimddv 2592 |
1
⊢ (𝜑 → 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q
𝑅))
<Q 𝑢}〉) |