Step | Hyp | Ref
| Expression |
1 | | caucvgprlemlim.jk |
. . . . 5
⊢ (𝜑 → 𝐽 <N 𝐾) |
2 | | caucvgprlemlim.jkq |
. . . . 5
⊢ (𝜑 →
(*Q‘[〈𝐽, 1o〉]
~Q ) <Q 𝑄) |
3 | 1, 2 | caucvgprlemk 7627 |
. . . 4
⊢ (𝜑 →
(*Q‘[〈𝐾, 1o〉]
~Q ) <Q 𝑄) |
4 | | caucvgpr.f |
. . . . 5
⊢ (𝜑 → 𝐹:N⟶Q) |
5 | | ltrelpi 7286 |
. . . . . . . 8
⊢
<N ⊆ (N ×
N) |
6 | 5 | brel 4663 |
. . . . . . 7
⊢ (𝐽 <N
𝐾 → (𝐽 ∈ N ∧ 𝐾 ∈
N)) |
7 | 1, 6 | syl 14 |
. . . . . 6
⊢ (𝜑 → (𝐽 ∈ N ∧ 𝐾 ∈
N)) |
8 | 7 | simprd 113 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ N) |
9 | 4, 8 | ffvelrnd 5632 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐾) ∈ Q) |
10 | | ltanqi 7364 |
. . . 4
⊢
(((*Q‘[〈𝐾, 1o〉]
~Q ) <Q 𝑄 ∧ (𝐹‘𝐾) ∈ Q) → ((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q ((𝐹‘𝐾) +Q 𝑄)) |
11 | 3, 9, 10 | syl2anc 409 |
. . 3
⊢ (𝜑 → ((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q ((𝐹‘𝐾) +Q 𝑄)) |
12 | | ltbtwnnqq 7377 |
. . 3
⊢ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q ((𝐹‘𝐾) +Q 𝑄) ↔ ∃𝑥 ∈ Q (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄))) |
13 | 11, 12 | sylib 121 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ Q (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄))) |
14 | | simprl 526 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → 𝑥 ∈ Q) |
15 | 8 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → 𝐾 ∈ N) |
16 | | simprrl 534 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → ((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥) |
17 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑗 = 𝐾 → (𝐹‘𝑗) = (𝐹‘𝐾)) |
18 | | opeq1 3765 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝐾 → 〈𝑗, 1o〉 = 〈𝐾,
1o〉) |
19 | 18 | eceq1d 6549 |
. . . . . . . . . 10
⊢ (𝑗 = 𝐾 → [〈𝑗, 1o〉]
~Q = [〈𝐾, 1o〉]
~Q ) |
20 | 19 | fveq2d 5500 |
. . . . . . . . 9
⊢ (𝑗 = 𝐾 →
(*Q‘[〈𝑗, 1o〉]
~Q ) = (*Q‘[〈𝐾, 1o〉]
~Q )) |
21 | 17, 20 | oveq12d 5871 |
. . . . . . . 8
⊢ (𝑗 = 𝐾 → ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) = ((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q ))) |
22 | 21 | breq1d 3999 |
. . . . . . 7
⊢ (𝑗 = 𝐾 → (((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑥 ↔ ((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥)) |
23 | 22 | rspcev 2834 |
. . . . . 6
⊢ ((𝐾 ∈ N ∧
((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥) → ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑥) |
24 | 15, 16, 23 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑥) |
25 | | breq2 3993 |
. . . . . . 7
⊢ (𝑢 = 𝑥 → (((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢 ↔ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑥)) |
26 | 25 | rexbidv 2471 |
. . . . . 6
⊢ (𝑢 = 𝑥 → (∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢 ↔ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑥)) |
27 | | caucvgpr.lim |
. . . . . . . 8
⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢}〉 |
28 | 27 | fveq2i 5499 |
. . . . . . 7
⊢
(2nd ‘𝐿) = (2nd ‘〈{𝑙 ∈ Q ∣
∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢}〉) |
29 | | nqex 7325 |
. . . . . . . . 9
⊢
Q ∈ V |
30 | 29 | rabex 4133 |
. . . . . . . 8
⊢ {𝑙 ∈ Q ∣
∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)} ∈ V |
31 | 29 | rabex 4133 |
. . . . . . . 8
⊢ {𝑢 ∈ Q ∣
∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢} ∈ V |
32 | 30, 31 | op2nd 6126 |
. . . . . . 7
⊢
(2nd ‘〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢}〉) = {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢} |
33 | 28, 32 | eqtri 2191 |
. . . . . 6
⊢
(2nd ‘𝐿) = {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢} |
34 | 26, 33 | elrab2 2889 |
. . . . 5
⊢ (𝑥 ∈ (2nd
‘𝐿) ↔ (𝑥 ∈ Q ∧
∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑥)) |
35 | 14, 24, 34 | sylanbrc 415 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → 𝑥 ∈ (2nd ‘𝐿)) |
36 | | simprrr 535 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)) |
37 | | vex 2733 |
. . . . . . 7
⊢ 𝑥 ∈ V |
38 | | breq1 3992 |
. . . . . . 7
⊢ (𝑙 = 𝑥 → (𝑙 <Q ((𝐹‘𝐾) +Q 𝑄) ↔ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄))) |
39 | 37, 38 | elab 2874 |
. . . . . 6
⊢ (𝑥 ∈ {𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)} ↔ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)) |
40 | 36, 39 | sylibr 133 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → 𝑥 ∈ {𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}) |
41 | | ltnqex 7511 |
. . . . . 6
⊢ {𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)} ∈ V |
42 | | gtnqex 7512 |
. . . . . 6
⊢ {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢} ∈
V |
43 | 41, 42 | op1st 6125 |
. . . . 5
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉) = {𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)} |
44 | 40, 43 | eleqtrrdi 2264 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → 𝑥 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉)) |
45 | | rspe 2519 |
. . . 4
⊢ ((𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘𝐿) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉))) →
∃𝑥 ∈
Q (𝑥 ∈
(2nd ‘𝐿)
∧ 𝑥 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉))) |
46 | 14, 35, 44, 45 | syl12anc 1231 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘𝐿) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉))) |
47 | | caucvgpr.cau |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q
(*Q‘[〈𝑛, 1o〉]
~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q
(*Q‘[〈𝑛, 1o〉]
~Q ))))) |
48 | | caucvgpr.bnd |
. . . . . 6
⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) |
49 | 4, 47, 48, 27 | caucvgprlemcl 7638 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ P) |
50 | 49 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → 𝐿 ∈ P) |
51 | | caucvgprlemlim.q |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ Q) |
52 | | addclnq 7337 |
. . . . . . 7
⊢ (((𝐹‘𝐾) ∈ Q ∧ 𝑄 ∈ Q) →
((𝐹‘𝐾) +Q 𝑄) ∈
Q) |
53 | 9, 51, 52 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝐾) +Q 𝑄) ∈
Q) |
54 | | nqprlu 7509 |
. . . . . 6
⊢ (((𝐹‘𝐾) +Q 𝑄) ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉 ∈
P) |
55 | 53, 54 | syl 14 |
. . . . 5
⊢ (𝜑 → 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉 ∈
P) |
56 | 55 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉 ∈
P) |
57 | | ltdfpr 7468 |
. . . 4
⊢ ((𝐿 ∈ P ∧
〈{𝑙 ∣ 𝑙 <Q
((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉 ∈
P) → (𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉 ↔
∃𝑥 ∈
Q (𝑥 ∈
(2nd ‘𝐿)
∧ 𝑥 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉)))) |
58 | 50, 56, 57 | syl2anc 409 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → (𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉 ↔
∃𝑥 ∈
Q (𝑥 ∈
(2nd ‘𝐿)
∧ 𝑥 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉)))) |
59 | 46, 58 | mpbird 166 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (((𝐹‘𝐾) +Q
(*Q‘[〈𝐾, 1o〉]
~Q )) <Q 𝑥 ∧ 𝑥 <Q ((𝐹‘𝐾) +Q 𝑄)))) → 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉) |
60 | 13, 59 | rexlimddv 2592 |
1
⊢ (𝜑 → 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q
𝑢}〉) |