Step | Hyp | Ref
| Expression |
1 | | cauappcvgprlem.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Q) |
2 | | halfnqq 7372 |
. . . . 5
⊢ (𝑅 ∈ Q →
∃𝑥 ∈
Q (𝑥
+Q 𝑥) = 𝑅) |
3 | 1, 2 | syl 14 |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ Q (𝑥 +Q 𝑥) = 𝑅) |
4 | | simprl 526 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → 𝑥 ∈ Q) |
5 | | cauappcvgpr.app |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q
𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q
𝑞)))) |
6 | 5 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q
𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q
𝑞)))) |
7 | | cauappcvgprlem.q |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ Q) |
8 | 7 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → 𝑄 ∈ Q) |
9 | | fveq2 5496 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑄 → (𝐹‘𝑝) = (𝐹‘𝑄)) |
10 | | oveq1 5860 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑄 → (𝑝 +Q 𝑞) = (𝑄 +Q 𝑞)) |
11 | 10 | oveq2d 5869 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑄 → ((𝐹‘𝑞) +Q (𝑝 +Q
𝑞)) = ((𝐹‘𝑞) +Q (𝑄 +Q
𝑞))) |
12 | 9, 11 | breq12d 4002 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑄 → ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q
𝑞)) ↔ (𝐹‘𝑄) <Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑞)))) |
13 | 9, 10 | oveq12d 5871 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑄 → ((𝐹‘𝑝) +Q (𝑝 +Q
𝑞)) = ((𝐹‘𝑄) +Q (𝑄 +Q
𝑞))) |
14 | 13 | breq2d 4001 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑄 → ((𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q
𝑞)) ↔ (𝐹‘𝑞) <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑞)))) |
15 | 12, 14 | anbi12d 470 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑄 → (((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q
𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q
𝑞))) ↔ ((𝐹‘𝑄) <Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑞))))) |
16 | | fveq2 5496 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 𝑥 → (𝐹‘𝑞) = (𝐹‘𝑥)) |
17 | | oveq2 5861 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 𝑥 → (𝑄 +Q 𝑞) = (𝑄 +Q 𝑥)) |
18 | 16, 17 | oveq12d 5871 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑥 → ((𝐹‘𝑞) +Q (𝑄 +Q
𝑞)) = ((𝐹‘𝑥) +Q (𝑄 +Q
𝑥))) |
19 | 18 | breq2d 4001 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝑥 → ((𝐹‘𝑄) <Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑞)) ↔ (𝐹‘𝑄) <Q ((𝐹‘𝑥) +Q (𝑄 +Q
𝑥)))) |
20 | 17 | oveq2d 5869 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑥 → ((𝐹‘𝑄) +Q (𝑄 +Q
𝑞)) = ((𝐹‘𝑄) +Q (𝑄 +Q
𝑥))) |
21 | 16, 20 | breq12d 4002 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝑥 → ((𝐹‘𝑞) <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑞)) ↔ (𝐹‘𝑥) <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑥)))) |
22 | 19, 21 | anbi12d 470 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑥 → (((𝐹‘𝑄) <Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑞))) ↔ ((𝐹‘𝑄) <Q ((𝐹‘𝑥) +Q (𝑄 +Q
𝑥)) ∧ (𝐹‘𝑥) <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑥))))) |
23 | 15, 22 | rspc2v 2847 |
. . . . . . . . . . 11
⊢ ((𝑄 ∈ Q ∧
𝑥 ∈ Q)
→ (∀𝑝 ∈
Q ∀𝑞
∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q
𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q
𝑞))) → ((𝐹‘𝑄) <Q ((𝐹‘𝑥) +Q (𝑄 +Q
𝑥)) ∧ (𝐹‘𝑥) <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑥))))) |
24 | 8, 4, 23 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → (∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q
𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q
𝑞))) → ((𝐹‘𝑄) <Q ((𝐹‘𝑥) +Q (𝑄 +Q
𝑥)) ∧ (𝐹‘𝑥) <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑥))))) |
25 | 6, 24 | mpd 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → ((𝐹‘𝑄) <Q ((𝐹‘𝑥) +Q (𝑄 +Q
𝑥)) ∧ (𝐹‘𝑥) <Q ((𝐹‘𝑄) +Q (𝑄 +Q
𝑥)))) |
26 | 25 | simpld 111 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → (𝐹‘𝑄) <Q ((𝐹‘𝑥) +Q (𝑄 +Q
𝑥))) |
27 | | cauappcvgpr.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:Q⟶Q) |
28 | 27 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → 𝐹:Q⟶Q) |
29 | 28, 4 | ffvelrnd 5632 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → (𝐹‘𝑥) ∈ Q) |
30 | | addassnqg 7344 |
. . . . . . . . 9
⊢ (((𝐹‘𝑥) ∈ Q ∧ 𝑄 ∈ Q ∧
𝑥 ∈ Q)
→ (((𝐹‘𝑥) +Q
𝑄)
+Q 𝑥) = ((𝐹‘𝑥) +Q (𝑄 +Q
𝑥))) |
31 | 29, 8, 4, 30 | syl3anc 1233 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → (((𝐹‘𝑥) +Q 𝑄) +Q
𝑥) = ((𝐹‘𝑥) +Q (𝑄 +Q
𝑥))) |
32 | 26, 31 | breqtrrd 4017 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → (𝐹‘𝑄) <Q (((𝐹‘𝑥) +Q 𝑄) +Q
𝑥)) |
33 | | ltanqg 7362 |
. . . . . . . . 9
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → (𝑓
<Q 𝑔 ↔ (ℎ +Q 𝑓) <Q
(ℎ
+Q 𝑔))) |
34 | 33 | adantl 275 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧
ℎ ∈ Q))
→ (𝑓
<Q 𝑔 ↔ (ℎ +Q 𝑓) <Q
(ℎ
+Q 𝑔))) |
35 | 27, 7 | ffvelrnd 5632 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑄) ∈ Q) |
36 | 35 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → (𝐹‘𝑄) ∈ Q) |
37 | | addclnq 7337 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) ∈ Q ∧ 𝑄 ∈ Q) →
((𝐹‘𝑥) +Q
𝑄) ∈
Q) |
38 | 29, 8, 37 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → ((𝐹‘𝑥) +Q 𝑄) ∈
Q) |
39 | | addclnq 7337 |
. . . . . . . . 9
⊢ ((((𝐹‘𝑥) +Q 𝑄) ∈ Q ∧
𝑥 ∈ Q)
→ (((𝐹‘𝑥) +Q
𝑄)
+Q 𝑥) ∈ Q) |
40 | 38, 4, 39 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → (((𝐹‘𝑥) +Q 𝑄) +Q
𝑥) ∈
Q) |
41 | | addcomnqg 7343 |
. . . . . . . . 9
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (𝑓
+Q 𝑔) = (𝑔 +Q 𝑓)) |
42 | 41 | adantl 275 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q)) →
(𝑓
+Q 𝑔) = (𝑔 +Q 𝑓)) |
43 | 34, 36, 40, 4, 42 | caovord2d 6022 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → ((𝐹‘𝑄) <Q (((𝐹‘𝑥) +Q 𝑄) +Q
𝑥) ↔ ((𝐹‘𝑄) +Q 𝑥) <Q
((((𝐹‘𝑥) +Q
𝑄)
+Q 𝑥) +Q 𝑥))) |
44 | 32, 43 | mpbid 146 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → ((𝐹‘𝑄) +Q 𝑥) <Q
((((𝐹‘𝑥) +Q
𝑄)
+Q 𝑥) +Q 𝑥)) |
45 | | addassnqg 7344 |
. . . . . . . 8
⊢ ((((𝐹‘𝑥) +Q 𝑄) ∈ Q ∧
𝑥 ∈ Q
∧ 𝑥 ∈
Q) → ((((𝐹‘𝑥) +Q 𝑄) +Q
𝑥)
+Q 𝑥) = (((𝐹‘𝑥) +Q 𝑄) +Q
(𝑥
+Q 𝑥))) |
46 | 38, 4, 4, 45 | syl3anc 1233 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → ((((𝐹‘𝑥) +Q 𝑄) +Q
𝑥)
+Q 𝑥) = (((𝐹‘𝑥) +Q 𝑄) +Q
(𝑥
+Q 𝑥))) |
47 | | simprr 527 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → (𝑥 +Q 𝑥) = 𝑅) |
48 | 47 | oveq2d 5869 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → (((𝐹‘𝑥) +Q 𝑄) +Q
(𝑥
+Q 𝑥)) = (((𝐹‘𝑥) +Q 𝑄) +Q
𝑅)) |
49 | 1 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → 𝑅 ∈ Q) |
50 | | addassnqg 7344 |
. . . . . . . 8
⊢ (((𝐹‘𝑥) ∈ Q ∧ 𝑄 ∈ Q ∧
𝑅 ∈ Q)
→ (((𝐹‘𝑥) +Q
𝑄)
+Q 𝑅) = ((𝐹‘𝑥) +Q (𝑄 +Q
𝑅))) |
51 | 29, 8, 49, 50 | syl3anc 1233 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → (((𝐹‘𝑥) +Q 𝑄) +Q
𝑅) = ((𝐹‘𝑥) +Q (𝑄 +Q
𝑅))) |
52 | 46, 48, 51 | 3eqtrd 2207 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → ((((𝐹‘𝑥) +Q 𝑄) +Q
𝑥)
+Q 𝑥) = ((𝐹‘𝑥) +Q (𝑄 +Q
𝑅))) |
53 | 44, 52 | breqtrd 4015 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → ((𝐹‘𝑄) +Q 𝑥) <Q
((𝐹‘𝑥) +Q
(𝑄
+Q 𝑅))) |
54 | | oveq2 5861 |
. . . . . . 7
⊢ (𝑞 = 𝑥 → ((𝐹‘𝑄) +Q 𝑞) = ((𝐹‘𝑄) +Q 𝑥)) |
55 | 16 | oveq1d 5868 |
. . . . . . 7
⊢ (𝑞 = 𝑥 → ((𝐹‘𝑞) +Q (𝑄 +Q
𝑅)) = ((𝐹‘𝑥) +Q (𝑄 +Q
𝑅))) |
56 | 54, 55 | breq12d 4002 |
. . . . . 6
⊢ (𝑞 = 𝑥 → (((𝐹‘𝑄) +Q 𝑞) <Q
((𝐹‘𝑞) +Q
(𝑄
+Q 𝑅)) ↔ ((𝐹‘𝑄) +Q 𝑥) <Q
((𝐹‘𝑥) +Q
(𝑄
+Q 𝑅)))) |
57 | 56 | rspcev 2834 |
. . . . 5
⊢ ((𝑥 ∈ Q ∧
((𝐹‘𝑄) +Q 𝑥) <Q
((𝐹‘𝑥) +Q
(𝑄
+Q 𝑅))) → ∃𝑞 ∈ Q ((𝐹‘𝑄) +Q 𝑞) <Q
((𝐹‘𝑞) +Q
(𝑄
+Q 𝑅))) |
58 | 4, 53, 57 | syl2anc 409 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥) = 𝑅)) → ∃𝑞 ∈ Q ((𝐹‘𝑄) +Q 𝑞) <Q
((𝐹‘𝑞) +Q
(𝑄
+Q 𝑅))) |
59 | 3, 58 | rexlimddv 2592 |
. . 3
⊢ (𝜑 → ∃𝑞 ∈ Q ((𝐹‘𝑄) +Q 𝑞) <Q
((𝐹‘𝑞) +Q
(𝑄
+Q 𝑅))) |
60 | | cauappcvgpr.bnd |
. . . . . . . 8
⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) |
61 | | cauappcvgpr.lim |
. . . . . . . 8
⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢}〉 |
62 | | addclnq 7337 |
. . . . . . . . 9
⊢ ((𝑄 ∈ Q ∧
𝑅 ∈ Q)
→ (𝑄
+Q 𝑅) ∈ Q) |
63 | 7, 1, 62 | syl2anc 409 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 +Q 𝑅) ∈
Q) |
64 | 27, 5, 60, 61, 63 | cauappcvgprlemladd 7620 |
. . . . . . 7
⊢ (𝜑 → (𝐿 +P 〈{𝑙 ∣ 𝑙 <Q (𝑄 +Q
𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉) = 〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑅))}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
(𝑄
+Q 𝑅)) <Q 𝑢}〉) |
65 | 64 | fveq2d 5500 |
. . . . . 6
⊢ (𝜑 → (1st
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q (𝑄 +Q
𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉)) =
(1st ‘〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑅))}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
(𝑄
+Q 𝑅)) <Q 𝑢}〉)) |
66 | | nqex 7325 |
. . . . . . . 8
⊢
Q ∈ V |
67 | 66 | rabex 4133 |
. . . . . . 7
⊢ {𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑅))} ∈
V |
68 | 66 | rabex 4133 |
. . . . . . 7
⊢ {𝑢 ∈ Q ∣
∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q
(𝑄
+Q 𝑅)) <Q 𝑢} ∈ V |
69 | 67, 68 | op1st 6125 |
. . . . . 6
⊢
(1st ‘〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑅))}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
(𝑄
+Q 𝑅)) <Q 𝑢}〉) = {𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑅))} |
70 | 65, 69 | eqtrdi 2219 |
. . . . 5
⊢ (𝜑 → (1st
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q (𝑄 +Q
𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉)) = {𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑅))}) |
71 | 70 | eleq2d 2240 |
. . . 4
⊢ (𝜑 → ((𝐹‘𝑄) ∈ (1st ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
(𝑄
+Q 𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉)) ↔ (𝐹‘𝑄) ∈ {𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑅))})) |
72 | | oveq1 5860 |
. . . . . . . 8
⊢ (𝑙 = (𝐹‘𝑄) → (𝑙 +Q 𝑞) = ((𝐹‘𝑄) +Q 𝑞)) |
73 | 72 | breq1d 3999 |
. . . . . . 7
⊢ (𝑙 = (𝐹‘𝑄) → ((𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
(𝑄
+Q 𝑅)) ↔ ((𝐹‘𝑄) +Q 𝑞) <Q
((𝐹‘𝑞) +Q
(𝑄
+Q 𝑅)))) |
74 | 73 | rexbidv 2471 |
. . . . . 6
⊢ (𝑙 = (𝐹‘𝑄) → (∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
(𝑄
+Q 𝑅)) ↔ ∃𝑞 ∈ Q ((𝐹‘𝑄) +Q 𝑞) <Q
((𝐹‘𝑞) +Q
(𝑄
+Q 𝑅)))) |
75 | 74 | elrab3 2887 |
. . . . 5
⊢ ((𝐹‘𝑄) ∈ Q → ((𝐹‘𝑄) ∈ {𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑅))} ↔ ∃𝑞 ∈ Q ((𝐹‘𝑄) +Q 𝑞) <Q
((𝐹‘𝑞) +Q
(𝑄
+Q 𝑅)))) |
76 | 35, 75 | syl 14 |
. . . 4
⊢ (𝜑 → ((𝐹‘𝑄) ∈ {𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q ((𝐹‘𝑞) +Q (𝑄 +Q
𝑅))} ↔ ∃𝑞 ∈ Q ((𝐹‘𝑄) +Q 𝑞) <Q
((𝐹‘𝑞) +Q
(𝑄
+Q 𝑅)))) |
77 | 71, 76 | bitrd 187 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑄) ∈ (1st ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
(𝑄
+Q 𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉)) ↔
∃𝑞 ∈
Q ((𝐹‘𝑄) +Q 𝑞) <Q
((𝐹‘𝑞) +Q
(𝑄
+Q 𝑅)))) |
78 | 59, 77 | mpbird 166 |
. 2
⊢ (𝜑 → (𝐹‘𝑄) ∈ (1st ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
(𝑄
+Q 𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉))) |
79 | 27, 5, 60, 61 | cauappcvgprlemcl 7615 |
. . . 4
⊢ (𝜑 → 𝐿 ∈ P) |
80 | | nqprlu 7509 |
. . . . 5
⊢ ((𝑄 +Q
𝑅) ∈ Q
→ 〈{𝑙 ∣
𝑙
<Q (𝑄 +Q 𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉 ∈
P) |
81 | 63, 80 | syl 14 |
. . . 4
⊢ (𝜑 → 〈{𝑙 ∣ 𝑙 <Q (𝑄 +Q
𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉 ∈
P) |
82 | | addclpr 7499 |
. . . 4
⊢ ((𝐿 ∈ P ∧
〈{𝑙 ∣ 𝑙 <Q
(𝑄
+Q 𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉 ∈
P) → (𝐿
+P 〈{𝑙 ∣ 𝑙 <Q (𝑄 +Q
𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉) ∈
P) |
83 | 79, 81, 82 | syl2anc 409 |
. . 3
⊢ (𝜑 → (𝐿 +P 〈{𝑙 ∣ 𝑙 <Q (𝑄 +Q
𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉) ∈
P) |
84 | | nqprl 7513 |
. . 3
⊢ (((𝐹‘𝑄) ∈ Q ∧ (𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
(𝑄
+Q 𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉) ∈
P) → ((𝐹‘𝑄) ∈ (1st ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
(𝑄
+Q 𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉)) ↔
〈{𝑙 ∣ 𝑙 <Q
(𝐹‘𝑄)}, {𝑢 ∣ (𝐹‘𝑄) <Q 𝑢}〉<P (𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
(𝑄
+Q 𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉))) |
85 | 35, 83, 84 | syl2anc 409 |
. 2
⊢ (𝜑 → ((𝐹‘𝑄) ∈ (1st ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
(𝑄
+Q 𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉)) ↔
〈{𝑙 ∣ 𝑙 <Q
(𝐹‘𝑄)}, {𝑢 ∣ (𝐹‘𝑄) <Q 𝑢}〉<P (𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
(𝑄
+Q 𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉))) |
86 | 78, 85 | mpbid 146 |
1
⊢ (𝜑 → 〈{𝑙 ∣ 𝑙 <Q (𝐹‘𝑄)}, {𝑢 ∣ (𝐹‘𝑄) <Q 𝑢}〉<P (𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
(𝑄
+Q 𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q
𝑢}〉)) |