Step | Hyp | Ref
| Expression |
1 | | caucvgprlemlim.jk |
. . . . . 6
⊢ (𝜑 → 𝐽 <N 𝐾) |
2 | | ltrelpi 7322 |
. . . . . . 7
⊢
<N ⊆ (N ×
N) |
3 | 2 | brel 4678 |
. . . . . 6
⊢ (𝐽 <N
𝐾 → (𝐽 ∈ N ∧ 𝐾 ∈
N)) |
4 | 1, 3 | syl 14 |
. . . . 5
⊢ (𝜑 → (𝐽 ∈ N ∧ 𝐾 ∈
N)) |
5 | 4 | simprd 114 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ N) |
6 | | caucvgprlemlim.jkq |
. . . . . 6
⊢ (𝜑 →
(*Q‘[⟨𝐽, 1o⟩]
~Q ) <Q 𝑄) |
7 | 1, 6 | caucvgprlemk 7663 |
. . . . 5
⊢ (𝜑 →
(*Q‘[⟨𝐾, 1o⟩]
~Q ) <Q 𝑄) |
8 | | caucvgpr.f |
. . . . . 6
⊢ (𝜑 → 𝐹:N⟶Q) |
9 | 8, 5 | ffvelcdmd 5652 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐾) ∈ Q) |
10 | | ltanqi 7400 |
. . . . 5
⊢
(((*Q‘[⟨𝐾, 1o⟩]
~Q ) <Q 𝑄 ∧ (𝐹‘𝐾) ∈ Q) → ((𝐹‘𝐾) +Q
(*Q‘[⟨𝐾, 1o⟩]
~Q )) <Q ((𝐹‘𝐾) +Q 𝑄)) |
11 | 7, 9, 10 | syl2anc 411 |
. . . 4
⊢ (𝜑 → ((𝐹‘𝐾) +Q
(*Q‘[⟨𝐾, 1o⟩]
~Q )) <Q ((𝐹‘𝐾) +Q 𝑄)) |
12 | | opeq1 3778 |
. . . . . . . . 9
⊢ (𝑗 = 𝐾 → ⟨𝑗, 1o⟩ = ⟨𝐾,
1o⟩) |
13 | 12 | eceq1d 6570 |
. . . . . . . 8
⊢ (𝑗 = 𝐾 → [⟨𝑗, 1o⟩]
~Q = [⟨𝐾, 1o⟩]
~Q ) |
14 | 13 | fveq2d 5519 |
. . . . . . 7
⊢ (𝑗 = 𝐾 →
(*Q‘[⟨𝑗, 1o⟩]
~Q ) = (*Q‘[⟨𝐾, 1o⟩]
~Q )) |
15 | 14 | oveq2d 5890 |
. . . . . 6
⊢ (𝑗 = 𝐾 → ((𝐹‘𝐾) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) = ((𝐹‘𝐾) +Q
(*Q‘[⟨𝐾, 1o⟩]
~Q ))) |
16 | | fveq2 5515 |
. . . . . . 7
⊢ (𝑗 = 𝐾 → (𝐹‘𝑗) = (𝐹‘𝐾)) |
17 | 16 | oveq1d 5889 |
. . . . . 6
⊢ (𝑗 = 𝐾 → ((𝐹‘𝑗) +Q 𝑄) = ((𝐹‘𝐾) +Q 𝑄)) |
18 | 15, 17 | breq12d 4016 |
. . . . 5
⊢ (𝑗 = 𝐾 → (((𝐹‘𝐾) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄) ↔ ((𝐹‘𝐾) +Q
(*Q‘[⟨𝐾, 1o⟩]
~Q )) <Q ((𝐹‘𝐾) +Q 𝑄))) |
19 | 18 | rspcev 2841 |
. . . 4
⊢ ((𝐾 ∈ N ∧
((𝐹‘𝐾) +Q
(*Q‘[⟨𝐾, 1o⟩]
~Q )) <Q ((𝐹‘𝐾) +Q 𝑄)) → ∃𝑗 ∈ N ((𝐹‘𝐾) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄)) |
20 | 5, 11, 19 | syl2anc 411 |
. . 3
⊢ (𝜑 → ∃𝑗 ∈ N ((𝐹‘𝐾) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄)) |
21 | | oveq1 5881 |
. . . . . . . 8
⊢ (𝑙 = (𝐹‘𝐾) → (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) = ((𝐹‘𝐾) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q ))) |
22 | 21 | breq1d 4013 |
. . . . . . 7
⊢ (𝑙 = (𝐹‘𝐾) → ((𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄) ↔ ((𝐹‘𝐾) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄))) |
23 | 22 | rexbidv 2478 |
. . . . . 6
⊢ (𝑙 = (𝐹‘𝐾) → (∃𝑗 ∈ N (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄) ↔ ∃𝑗 ∈ N ((𝐹‘𝐾) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄))) |
24 | 23 | elrab3 2894 |
. . . . 5
⊢ ((𝐹‘𝐾) ∈ Q → ((𝐹‘𝐾) ∈ {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄)} ↔ ∃𝑗 ∈ N ((𝐹‘𝐾) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄))) |
25 | 9, 24 | syl 14 |
. . . 4
⊢ (𝜑 → ((𝐹‘𝐾) ∈ {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄)} ↔ ∃𝑗 ∈ N ((𝐹‘𝐾) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄))) |
26 | | caucvgpr.cau |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q
(*Q‘[⟨𝑛, 1o⟩]
~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q
(*Q‘[⟨𝑛, 1o⟩]
~Q ))))) |
27 | | caucvgpr.bnd |
. . . . . 6
⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) |
28 | | caucvgpr.lim |
. . . . . 6
⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝑢}⟩ |
29 | | caucvgprlemlim.q |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ Q) |
30 | 8, 26, 27, 28, 29 | caucvgprlemladdrl 7676 |
. . . . 5
⊢ (𝜑 → {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄)} ⊆ (1st
‘(𝐿
+P ⟨{𝑙 ∣ 𝑙 <Q 𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩))) |
31 | 30 | sseld 3154 |
. . . 4
⊢ (𝜑 → ((𝐹‘𝐾) ∈ {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄)} → (𝐹‘𝐾) ∈ (1st ‘(𝐿 +P
⟨{𝑙 ∣ 𝑙 <Q
𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩)))) |
32 | 25, 31 | sylbird 170 |
. . 3
⊢ (𝜑 → (∃𝑗 ∈ N ((𝐹‘𝐾) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q ((𝐹‘𝑗) +Q 𝑄) → (𝐹‘𝐾) ∈ (1st ‘(𝐿 +P
⟨{𝑙 ∣ 𝑙 <Q
𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩)))) |
33 | 20, 32 | mpd 13 |
. 2
⊢ (𝜑 → (𝐹‘𝐾) ∈ (1st ‘(𝐿 +P
⟨{𝑙 ∣ 𝑙 <Q
𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩))) |
34 | 8, 26, 27, 28 | caucvgprlemcl 7674 |
. . . 4
⊢ (𝜑 → 𝐿 ∈ P) |
35 | | nqprlu 7545 |
. . . . 5
⊢ (𝑄 ∈ Q →
⟨{𝑙 ∣ 𝑙 <Q
𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩ ∈
P) |
36 | 29, 35 | syl 14 |
. . . 4
⊢ (𝜑 → ⟨{𝑙 ∣ 𝑙 <Q 𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩ ∈
P) |
37 | | addclpr 7535 |
. . . 4
⊢ ((𝐿 ∈ P ∧
⟨{𝑙 ∣ 𝑙 <Q
𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩ ∈ P)
→ (𝐿
+P ⟨{𝑙 ∣ 𝑙 <Q 𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩) ∈
P) |
38 | 34, 36, 37 | syl2anc 411 |
. . 3
⊢ (𝜑 → (𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩) ∈
P) |
39 | | nqprl 7549 |
. . 3
⊢ (((𝐹‘𝐾) ∈ Q ∧ (𝐿 +P
⟨{𝑙 ∣ 𝑙 <Q
𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩) ∈ P)
→ ((𝐹‘𝐾) ∈ (1st
‘(𝐿
+P ⟨{𝑙 ∣ 𝑙 <Q 𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩)) ↔ ⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝐾)}, {𝑢 ∣ (𝐹‘𝐾) <Q 𝑢}⟩<P (𝐿 +P
⟨{𝑙 ∣ 𝑙 <Q
𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩))) |
40 | 9, 38, 39 | syl2anc 411 |
. 2
⊢ (𝜑 → ((𝐹‘𝐾) ∈ (1st ‘(𝐿 +P
⟨{𝑙 ∣ 𝑙 <Q
𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩)) ↔ ⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝐾)}, {𝑢 ∣ (𝐹‘𝐾) <Q 𝑢}⟩<P (𝐿 +P
⟨{𝑙 ∣ 𝑙 <Q
𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩))) |
41 | 33, 40 | mpbid 147 |
1
⊢ (𝜑 → ⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝐾)}, {𝑢 ∣ (𝐹‘𝐾) <Q 𝑢}⟩<P (𝐿 +P
⟨{𝑙 ∣ 𝑙 <Q
𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩)) |