Step | Hyp | Ref
| Expression |
1 | | breq2 3759 |
. . . . 5
⊢ (u = 𝑟 → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u ↔ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟)) |
2 | 1 | rexbidv 2321 |
. . . 4
⊢ (u = 𝑟 → (∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u ↔ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟)) |
3 | | nqex 6347 |
. . . . . 6
⊢
Q ∈ V |
4 | 3 | rabex 3892 |
. . . . 5
⊢ {𝑙 ∈ Q ∣ ∃𝑞 ∈
Q (𝑙
+Q 𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)} ∈ V |
5 | 3 | rabex 3892 |
. . . . 5
⊢ {u ∈
Q ∣ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u} ∈
V |
6 | 4, 5 | op2nd 5716 |
. . . 4
⊢
(2nd ‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈
Q (𝑙
+Q 𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈
Q ∣ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u}〉) = {u ∈
Q ∣ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u} |
7 | 2, 6 | elrab2 2694 |
. . 3
⊢ (𝑟 ∈ (2nd ‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈
Q (𝑙
+Q 𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈
Q ∣ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u}〉) ↔ (𝑟 ∈
Q ∧ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟)) |
8 | | cauappcvgpr.f |
. . . . . . . . . . . . 13
⊢ (φ → 𝐹:Q⟶Q) |
9 | | cauappcvgpr.app |
. . . . . . . . . . . . 13
⊢ (φ → ∀𝑝 ∈
Q ∀𝑞 ∈
Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) |
10 | | cauappcvgpr.bnd |
. . . . . . . . . . . . 13
⊢ (φ → ∀𝑝 ∈
Q A
<Q (𝐹‘𝑝)) |
11 | | cauappcvgpr.lim |
. . . . . . . . . . . . 13
⊢ 𝐿 = 〈{𝑙 ∈
Q ∣ ∃𝑞 ∈
Q (𝑙
+Q 𝑞)
<Q (𝐹‘𝑞)}, {u
∈ Q ∣ ∃𝑞 ∈
Q ((𝐹‘𝑞) +Q 𝑞) <Q u}〉 |
12 | | cauappcvgprlemladd.s |
. . . . . . . . . . . . 13
⊢ (φ → 𝑆 ∈
Q) |
13 | 8, 9, 10, 11, 12 | cauappcvgprlemladdfl 6627 |
. . . . . . . . . . . 12
⊢ (φ → (1st ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {u ∣ 𝑆 <Q u}〉)) ⊆ (1st
‘〈{𝑙 ∈ Q ∣ ∃𝑞 ∈
Q (𝑙
+Q 𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈
Q ∣ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u}〉)) |
14 | | oveq2 5463 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 = v → (𝑙 +Q 𝑞) = (𝑙 +Q v)) |
15 | | fveq2 5121 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 = v → (𝐹‘𝑞) = (𝐹‘v)) |
16 | 15 | oveq1d 5470 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 = v → ((𝐹‘𝑞) +Q 𝑆) = ((𝐹‘v) +Q 𝑆)) |
17 | 14, 16 | breq12d 3768 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 = v → ((𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆) ↔ (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆))) |
18 | 17 | cbvrexv 2528 |
. . . . . . . . . . . . . . . 16
⊢ (∃𝑞 ∈
Q (𝑙
+Q 𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆) ↔ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)) |
19 | 18 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ Q → (∃𝑞 ∈
Q (𝑙
+Q 𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆) ↔ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆))) |
20 | 19 | rabbiia 2541 |
. . . . . . . . . . . . . 14
⊢ {𝑙 ∈ Q ∣ ∃𝑞 ∈
Q (𝑙
+Q 𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)} = {𝑙 ∈
Q ∣ ∃v ∈
Q (𝑙
+Q v)
<Q ((𝐹‘v) +Q 𝑆)} |
21 | | id 19 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 = v → 𝑞 = v) |
22 | 15, 21 | oveq12d 5473 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 = v → ((𝐹‘𝑞) +Q 𝑞) = ((𝐹‘v) +Q v)) |
23 | 22 | oveq1d 5470 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 = v → (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) = (((𝐹‘v) +Q v) +Q 𝑆)) |
24 | 23 | breq1d 3765 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 = v → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u ↔ (((𝐹‘v) +Q v) +Q 𝑆) <Q u)) |
25 | 24 | cbvrexv 2528 |
. . . . . . . . . . . . . . . 16
⊢ (∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u ↔ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u) |
26 | 25 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ (u ∈
Q → (∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u ↔ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u)) |
27 | 26 | rabbiia 2541 |
. . . . . . . . . . . . . 14
⊢ {u ∈
Q ∣ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u} = {u
∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u} |
28 | 20, 27 | opeq12i 3545 |
. . . . . . . . . . . . 13
⊢
〈{𝑙 ∈ Q ∣ ∃𝑞 ∈
Q (𝑙
+Q 𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈
Q ∣ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u}〉 = 〈{𝑙 ∈
Q ∣ ∃v ∈
Q (𝑙
+Q v)
<Q ((𝐹‘v) +Q 𝑆)}, {u
∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}〉 |
29 | 28 | fveq2i 5124 |
. . . . . . . . . . . 12
⊢
(1st ‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈
Q (𝑙
+Q 𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈
Q ∣ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u}〉) = (1st
‘〈{𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)}, {u
∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}〉) |
30 | 13, 29 | syl6sseq 2985 |
. . . . . . . . . . 11
⊢ (φ → (1st ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {u ∣ 𝑆 <Q u}〉)) ⊆ (1st
‘〈{𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)}, {u
∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}〉)) |
31 | 30 | adantr 261 |
. . . . . . . . . 10
⊢ ((φ ∧ 𝑞 ∈ Q) → (1st
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)) ⊆ (1st
‘〈{𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)}, {u
∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}〉)) |
32 | 8 | ad2antrr 457 |
. . . . . . . . . . . . . . . . . 18
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → 𝐹:Q⟶Q) |
33 | | simplr 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → 𝑞 ∈
Q) |
34 | 32, 33 | ffvelrnd 5246 |
. . . . . . . . . . . . . . . . 17
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (𝐹‘𝑞) ∈
Q) |
35 | | simpr 103 |
. . . . . . . . . . . . . . . . 17
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → v ∈
Q) |
36 | | addassnqg 6366 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑞) ∈
Q ∧ 𝑞 ∈
Q ∧ v ∈
Q) → (((𝐹‘𝑞) +Q 𝑞) +Q v) = ((𝐹‘𝑞) +Q (𝑞 +Q
v))) |
37 | 34, 33, 35, 36 | syl3anc 1134 |
. . . . . . . . . . . . . . . 16
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (((𝐹‘𝑞) +Q 𝑞) +Q v) = ((𝐹‘𝑞) +Q (𝑞 +Q
v))) |
38 | | addclnq 6359 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑞) ∈
Q ∧ 𝑞 ∈
Q) → ((𝐹‘𝑞) +Q 𝑞) ∈
Q) |
39 | 34, 33, 38 | syl2anc 391 |
. . . . . . . . . . . . . . . . 17
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((𝐹‘𝑞) +Q 𝑞) ∈
Q) |
40 | | addclnq 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑞) +Q 𝑞) ∈
Q ∧ v ∈
Q) → (((𝐹‘𝑞) +Q 𝑞) +Q v) ∈
Q) |
41 | 39, 40 | sylancom 397 |
. . . . . . . . . . . . . . . 16
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (((𝐹‘𝑞) +Q 𝑞) +Q v) ∈
Q) |
42 | 37, 41 | eqeltrrd 2112 |
. . . . . . . . . . . . . . 15
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((𝐹‘𝑞) +Q (𝑞 +Q
v)) ∈
Q) |
43 | 32, 35 | ffvelrnd 5246 |
. . . . . . . . . . . . . . 15
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (𝐹‘v) ∈
Q) |
44 | | ltsonq 6382 |
. . . . . . . . . . . . . . . 16
⊢
<Q Or Q |
45 | | so2nr 4049 |
. . . . . . . . . . . . . . . 16
⊢ ((
<Q Or Q ∧ (((𝐹‘𝑞) +Q (𝑞 +Q
v)) ∈
Q ∧ (𝐹‘v) ∈
Q)) → ¬ (((𝐹‘𝑞) +Q (𝑞 +Q
v)) <Q (𝐹‘v) ∧ (𝐹‘v) <Q ((𝐹‘𝑞) +Q (𝑞 +Q
v)))) |
46 | 44, 45 | mpan 400 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑞) +Q (𝑞 +Q
v)) ∈
Q ∧ (𝐹‘v) ∈
Q) → ¬ (((𝐹‘𝑞) +Q (𝑞 +Q
v)) <Q (𝐹‘v) ∧ (𝐹‘v) <Q ((𝐹‘𝑞) +Q (𝑞 +Q
v)))) |
47 | 42, 43, 46 | syl2anc 391 |
. . . . . . . . . . . . . 14
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ¬ (((𝐹‘𝑞) +Q (𝑞 +Q
v)) <Q (𝐹‘v) ∧ (𝐹‘v) <Q ((𝐹‘𝑞) +Q (𝑞 +Q
v)))) |
48 | 12 | ad2antrr 457 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → 𝑆 ∈
Q) |
49 | | addcomnqg 6365 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((f ∈ Q ∧ g ∈ Q) → (f +Q g) = (g
+Q f)) |
50 | 49 | adantl 262 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) ∧ (f ∈ Q ∧ g ∈ Q)) → (f +Q g) = (g
+Q f)) |
51 | | addassnqg 6366 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((f ∈ Q ∧ g ∈ Q ∧ ℎ
∈ Q) → ((f +Q g) +Q ℎ) = (f
+Q (g
+Q ℎ))) |
52 | 51 | adantl 262 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) ∧ (f ∈ Q ∧ g ∈ Q ∧ ℎ
∈ Q)) → ((f +Q g) +Q ℎ) = (f
+Q (g
+Q ℎ))) |
53 | 39, 48, 35, 50, 52 | caov32d 5623 |
. . . . . . . . . . . . . . . . . 18
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q
v) = ((((𝐹‘𝑞) +Q 𝑞) +Q v) +Q 𝑆)) |
54 | 53 | breq1d 3765 |
. . . . . . . . . . . . . . . . 17
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q
v) <Q ((𝐹‘v) +Q 𝑆) ↔ ((((𝐹‘𝑞) +Q 𝑞) +Q v) +Q 𝑆) <Q ((𝐹‘v) +Q 𝑆))) |
55 | | ltanqg 6384 |
. . . . . . . . . . . . . . . . . . 19
⊢
((f ∈ Q ∧ g ∈ Q ∧ ℎ
∈ Q) → (f <Q g ↔ (ℎ +Q f) <Q (ℎ +Q g))) |
56 | 55 | adantl 262 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) ∧ (f ∈ Q ∧ g ∈ Q ∧ ℎ
∈ Q)) → (f <Q g ↔ (ℎ +Q f) <Q (ℎ +Q g))) |
57 | 56, 41, 43, 48, 50 | caovord2d 5612 |
. . . . . . . . . . . . . . . . 17
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((((𝐹‘𝑞) +Q 𝑞) +Q v) <Q (𝐹‘v) ↔ ((((𝐹‘𝑞) +Q 𝑞) +Q v) +Q 𝑆) <Q ((𝐹‘v) +Q 𝑆))) |
58 | 37 | breq1d 3765 |
. . . . . . . . . . . . . . . . 17
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((((𝐹‘𝑞) +Q 𝑞) +Q v) <Q (𝐹‘v) ↔ ((𝐹‘𝑞) +Q (𝑞 +Q
v)) <Q (𝐹‘v))) |
59 | 54, 57, 58 | 3bitr2d 205 |
. . . . . . . . . . . . . . . 16
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q
v) <Q ((𝐹‘v) +Q 𝑆) ↔ ((𝐹‘𝑞) +Q (𝑞 +Q
v)) <Q (𝐹‘v))) |
60 | 59 | biimpd 132 |
. . . . . . . . . . . . . . 15
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q
v) <Q ((𝐹‘v) +Q 𝑆) → ((𝐹‘𝑞) +Q (𝑞 +Q
v)) <Q (𝐹‘v))) |
61 | 9 | ad2antrr 457 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ∀𝑝 ∈
Q ∀𝑞 ∈
Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) |
62 | | fveq2 5121 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 = v → (𝐹‘𝑝) = (𝐹‘v)) |
63 | | oveq1 5462 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 = v → (𝑝 +Q 𝑞) = (v
+Q 𝑞)) |
64 | 63 | oveq2d 5471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 = v → ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) = ((𝐹‘𝑞) +Q (v +Q 𝑞))) |
65 | 62, 64 | breq12d 3768 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 = v → ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ↔ (𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)))) |
66 | 62, 63 | oveq12d 5473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 = v → ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)) = ((𝐹‘v) +Q (v +Q 𝑞))) |
67 | 66 | breq2d 3767 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 = v → ((𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)) ↔ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞)))) |
68 | 65, 67 | anbi12d 442 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 = v → (((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))) ↔ ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞))))) |
69 | 68 | ralbidv 2320 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = v → (∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))) ↔ ∀𝑞 ∈
Q ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞))))) |
70 | 69 | rspcv 2646 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (v ∈
Q → (∀𝑝 ∈
Q ∀𝑞 ∈
Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))) → ∀𝑞 ∈
Q ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞))))) |
71 | 70 | adantl 262 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (∀𝑝 ∈
Q ∀𝑞 ∈
Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))) → ∀𝑞 ∈
Q ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞))))) |
72 | 61, 71 | mpd 13 |
. . . . . . . . . . . . . . . . . 18
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ∀𝑞 ∈
Q ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞)))) |
73 | | rsp 2363 |
. . . . . . . . . . . . . . . . . 18
⊢ (∀𝑞 ∈
Q ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞))) → (𝑞 ∈
Q → ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞))))) |
74 | 72, 33, 73 | sylc 56 |
. . . . . . . . . . . . . . . . 17
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞)))) |
75 | 74 | simpld 105 |
. . . . . . . . . . . . . . . 16
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞))) |
76 | | addcomnqg 6365 |
. . . . . . . . . . . . . . . . . 18
⊢
((v ∈ Q ∧ 𝑞
∈ Q) → (v +Q 𝑞) = (𝑞 +Q v)) |
77 | 35, 33, 76 | syl2anc 391 |
. . . . . . . . . . . . . . . . 17
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (v +Q 𝑞) = (𝑞 +Q v)) |
78 | 77 | oveq2d 5471 |
. . . . . . . . . . . . . . . 16
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((𝐹‘𝑞) +Q (v +Q 𝑞)) = ((𝐹‘𝑞) +Q (𝑞 +Q
v))) |
79 | 75, 78 | breqtrd 3779 |
. . . . . . . . . . . . . . 15
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (𝐹‘v) <Q ((𝐹‘𝑞) +Q (𝑞 +Q
v))) |
80 | 60, 79 | jctird 300 |
. . . . . . . . . . . . . 14
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q
v) <Q ((𝐹‘v) +Q 𝑆) → (((𝐹‘𝑞) +Q (𝑞 +Q
v)) <Q (𝐹‘v) ∧ (𝐹‘v) <Q ((𝐹‘𝑞) +Q (𝑞 +Q
v))))) |
81 | 47, 80 | mtod 588 |
. . . . . . . . . . . . 13
⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ¬ ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q
v) <Q ((𝐹‘v) +Q 𝑆)) |
82 | 81 | nrexdv 2406 |
. . . . . . . . . . . 12
⊢ ((φ ∧ 𝑞 ∈ Q) → ¬ ∃v ∈ Q ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q
v) <Q ((𝐹‘v) +Q 𝑆)) |
83 | 8 | ffvelrnda 5245 |
. . . . . . . . . . . . . . 15
⊢ ((φ ∧ 𝑞 ∈ Q) → (𝐹‘𝑞) ∈
Q) |
84 | 83, 38 | sylancom 397 |
. . . . . . . . . . . . . 14
⊢ ((φ ∧ 𝑞 ∈ Q) → ((𝐹‘𝑞) +Q 𝑞) ∈
Q) |
85 | 12 | adantr 261 |
. . . . . . . . . . . . . 14
⊢ ((φ ∧ 𝑞 ∈ Q) → 𝑆 ∈
Q) |
86 | | addclnq 6359 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑞) +Q 𝑞) ∈
Q ∧ 𝑆 ∈
Q) → (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ Q) |
87 | 84, 85, 86 | syl2anc 391 |
. . . . . . . . . . . . 13
⊢ ((φ ∧ 𝑞 ∈ Q) → (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ Q) |
88 | | oveq1 5462 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) → (𝑙 +Q v) = ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q
v)) |
89 | 88 | breq1d 3765 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) → ((𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆) ↔ ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q
v) <Q ((𝐹‘v) +Q 𝑆))) |
90 | 89 | rexbidv 2321 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) → (∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆) ↔ ∃v ∈ Q ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q
v) <Q ((𝐹‘v) +Q 𝑆))) |
91 | 90 | elrab3 2693 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ Q → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ {𝑙 ∈
Q ∣ ∃v ∈
Q (𝑙
+Q v)
<Q ((𝐹‘v) +Q 𝑆)} ↔ ∃v ∈ Q ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q
v) <Q ((𝐹‘v) +Q 𝑆))) |
92 | 87, 91 | syl 14 |
. . . . . . . . . . . 12
⊢ ((φ ∧ 𝑞 ∈ Q) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ {𝑙 ∈
Q ∣ ∃v ∈
Q (𝑙
+Q v)
<Q ((𝐹‘v) +Q 𝑆)} ↔ ∃v ∈ Q ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q
v) <Q ((𝐹‘v) +Q 𝑆))) |
93 | 82, 92 | mtbird 597 |
. . . . . . . . . . 11
⊢ ((φ ∧ 𝑞 ∈ Q) → ¬ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ {𝑙 ∈
Q ∣ ∃v ∈
Q (𝑙
+Q v)
<Q ((𝐹‘v) +Q 𝑆)}) |
94 | 3 | rabex 3892 |
. . . . . . . . . . . . 13
⊢ {𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)} ∈
V |
95 | 3 | rabex 3892 |
. . . . . . . . . . . . 13
⊢ {u ∈
Q ∣ ∃v ∈
Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u} ∈
V |
96 | 94, 95 | op1st 5715 |
. . . . . . . . . . . 12
⊢
(1st ‘〈{𝑙 ∈
Q ∣ ∃v ∈
Q (𝑙
+Q v)
<Q ((𝐹‘v) +Q 𝑆)}, {u
∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}〉) = {𝑙 ∈
Q ∣ ∃v ∈
Q (𝑙
+Q v)
<Q ((𝐹‘v) +Q 𝑆)} |
97 | 96 | eleq2i 2101 |
. . . . . . . . . . 11
⊢ ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘〈{𝑙 ∈
Q ∣ ∃v ∈
Q (𝑙
+Q v)
<Q ((𝐹‘v) +Q 𝑆)}, {u
∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}〉) ↔ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ {𝑙 ∈
Q ∣ ∃v ∈
Q (𝑙
+Q v)
<Q ((𝐹‘v) +Q 𝑆)}) |
98 | 93, 97 | sylnibr 601 |
. . . . . . . . . 10
⊢ ((φ ∧ 𝑞 ∈ Q) → ¬ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘〈{𝑙 ∈
Q ∣ ∃v ∈
Q (𝑙
+Q v)
<Q ((𝐹‘v) +Q 𝑆)}, {u
∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}〉)) |
99 | 31, 98 | ssneldd 2942 |
. . . . . . . . 9
⊢ ((φ ∧ 𝑞 ∈ Q) → ¬ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉))) |
100 | 99 | adantlr 446 |
. . . . . . . 8
⊢ (((φ ∧ 𝑟 ∈ Q) ∧ 𝑞
∈ Q) → ¬ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉))) |
101 | 100 | adantr 261 |
. . . . . . 7
⊢ ((((φ ∧ 𝑟 ∈ Q) ∧ 𝑞
∈ Q) ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟) → ¬ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉))) |
102 | 8, 9, 10, 11 | cauappcvgprlemcl 6625 |
. . . . . . . . . . . . 13
⊢ (φ → 𝐿 ∈
P) |
103 | | nqprlu 6530 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ Q → 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉 ∈
P) |
104 | 12, 103 | syl 14 |
. . . . . . . . . . . . 13
⊢ (φ → 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉 ∈
P) |
105 | | addclpr 6520 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∈ P ∧ 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉 ∈
P) → (𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉) ∈
P) |
106 | 102, 104,
105 | syl2anc 391 |
. . . . . . . . . . . 12
⊢ (φ → (𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉) ∈
P) |
107 | | prop 6458 |
. . . . . . . . . . . 12
⊢ ((𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {u ∣ 𝑆 <Q u}〉) ∈
P → 〈(1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)), (2nd ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {u ∣ 𝑆 <Q u}〉))〉 ∈
P) |
108 | 106, 107 | syl 14 |
. . . . . . . . . . 11
⊢ (φ → 〈(1st ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {u ∣ 𝑆 <Q u}〉)), (2nd ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {u ∣ 𝑆 <Q u}〉))〉 ∈
P) |
109 | | prloc 6474 |
. . . . . . . . . . 11
⊢
((〈(1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)), (2nd ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {u ∣ 𝑆 <Q u}〉))〉 ∈
P ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)) ∨ 𝑟 ∈ (2nd ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)))) |
110 | 108, 109 | sylan 267 |
. . . . . . . . . 10
⊢ ((φ ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)) ∨ 𝑟 ∈ (2nd ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)))) |
111 | 110 | adantlr 446 |
. . . . . . . . 9
⊢ (((φ ∧ 𝑟 ∈ Q) ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)) ∨ 𝑟 ∈ (2nd ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)))) |
112 | 111 | adantlr 446 |
. . . . . . . 8
⊢ ((((φ ∧ 𝑟 ∈ Q) ∧ 𝑞
∈ Q) ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)) ∨ 𝑟 ∈ (2nd ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)))) |
113 | 112 | orcomd 647 |
. . . . . . 7
⊢ ((((φ ∧ 𝑟 ∈ Q) ∧ 𝑞
∈ Q) ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟) → (𝑟 ∈
(2nd ‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)) ∨
(((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)))) |
114 | 101, 113 | ecased 1238 |
. . . . . 6
⊢ ((((φ ∧ 𝑟 ∈ Q) ∧ 𝑞
∈ Q) ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟) → 𝑟 ∈
(2nd ‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉))) |
115 | 114 | ex 108 |
. . . . 5
⊢ (((φ ∧ 𝑟 ∈ Q) ∧ 𝑞
∈ Q) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟 → 𝑟 ∈
(2nd ‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)))) |
116 | 115 | rexlimdva 2427 |
. . . 4
⊢ ((φ ∧ 𝑟 ∈ Q) → (∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟 → 𝑟 ∈
(2nd ‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)))) |
117 | 116 | expimpd 345 |
. . 3
⊢ (φ → ((𝑟 ∈
Q ∧ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
𝑟) → 𝑟 ∈
(2nd ‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)))) |
118 | 7, 117 | syl5bi 141 |
. 2
⊢ (φ → (𝑟 ∈
(2nd ‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈
Q (𝑙
+Q 𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈
Q ∣ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u}〉) → 𝑟 ∈
(2nd ‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉)))) |
119 | 118 | ssrdv 2945 |
1
⊢ (φ → (2nd ‘〈{𝑙 ∈ Q ∣ ∃𝑞 ∈
Q (𝑙
+Q 𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈
Q ∣ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q
u}〉) ⊆ (2nd
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}〉))) |