Proof of Theorem caucvgprlemlim
Step | Hyp | Ref
| Expression |
1 | | archrecnq 7618 |
. . . 4
⊢ (𝑥 ∈ Q →
∃𝑗 ∈
N (*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) |
2 | 1 | adantl 275 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ Q) → ∃𝑗 ∈ N
(*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) |
3 | | caucvgpr.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:N⟶Q) |
4 | 3 | ad5antr 493 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ Q) ∧
𝑗 ∈ N)
∧ (*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) ∧ 𝑘 ∈ N) ∧ 𝑗 <N
𝑘) → 𝐹:N⟶Q) |
5 | | caucvgpr.cau |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q
(*Q‘[〈𝑛, 1o〉]
~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q
(*Q‘[〈𝑛, 1o〉]
~Q ))))) |
6 | 5 | ad5antr 493 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ Q) ∧
𝑗 ∈ N)
∧ (*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) ∧ 𝑘 ∈ N) ∧ 𝑗 <N
𝑘) → ∀𝑛 ∈ N
∀𝑘 ∈
N (𝑛
<N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q
(*Q‘[〈𝑛, 1o〉]
~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q
(*Q‘[〈𝑛, 1o〉]
~Q ))))) |
7 | | caucvgpr.bnd |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) |
8 | 7 | ad5antr 493 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ Q) ∧
𝑗 ∈ N)
∧ (*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) ∧ 𝑘 ∈ N) ∧ 𝑗 <N
𝑘) → ∀𝑗 ∈ N 𝐴 <Q
(𝐹‘𝑗)) |
9 | | caucvgpr.lim |
. . . . . . . . 9
⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢}〉 |
10 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ Q) → 𝑥 ∈
Q) |
11 | 10 | ad4antr 491 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ Q) ∧
𝑗 ∈ N)
∧ (*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) ∧ 𝑘 ∈ N) ∧ 𝑗 <N
𝑘) → 𝑥 ∈
Q) |
12 | | simpr 109 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ Q) ∧
𝑗 ∈ N)
∧ (*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) ∧ 𝑘 ∈ N) ∧ 𝑗 <N
𝑘) → 𝑗 <N
𝑘) |
13 | | simpllr 529 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ Q) ∧
𝑗 ∈ N)
∧ (*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) ∧ 𝑘 ∈ N) ∧ 𝑗 <N
𝑘) →
(*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) |
14 | 4, 6, 8, 9, 11, 12, 13 | caucvgprlem1 7634 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ Q) ∧
𝑗 ∈ N)
∧ (*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) ∧ 𝑘 ∈ N) ∧ 𝑗 <N
𝑘) → 〈{𝑙 ∣ 𝑙 <Q (𝐹‘𝑘)}, {𝑢 ∣ (𝐹‘𝑘) <Q 𝑢}〉<P (𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑥}, {𝑢 ∣ 𝑥 <Q 𝑢}〉)) |
15 | 4, 6, 8, 9, 11, 12, 13 | caucvgprlem2 7635 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ Q) ∧
𝑗 ∈ N)
∧ (*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) ∧ 𝑘 ∈ N) ∧ 𝑗 <N
𝑘) → 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹‘𝑘) +Q 𝑥) <Q
𝑢}〉) |
16 | 14, 15 | jca 304 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑥 ∈ Q) ∧
𝑗 ∈ N)
∧ (*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) ∧ 𝑘 ∈ N) ∧ 𝑗 <N
𝑘) → (〈{𝑙 ∣ 𝑙 <Q (𝐹‘𝑘)}, {𝑢 ∣ (𝐹‘𝑘) <Q 𝑢}〉<P (𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑥}, {𝑢 ∣ 𝑥 <Q 𝑢}〉) ∧ 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹‘𝑘) +Q 𝑥) <Q
𝑢}〉)) |
17 | 16 | ex 114 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ Q) ∧
𝑗 ∈ N)
∧ (*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) ∧ 𝑘 ∈ N) → (𝑗 <N
𝑘 → (〈{𝑙 ∣ 𝑙 <Q (𝐹‘𝑘)}, {𝑢 ∣ (𝐹‘𝑘) <Q 𝑢}〉<P (𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑥}, {𝑢 ∣ 𝑥 <Q 𝑢}〉) ∧ 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹‘𝑘) +Q 𝑥) <Q
𝑢}〉))) |
18 | 17 | ralrimiva 2543 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ Q) ∧ 𝑗 ∈ N) ∧
(*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥) → ∀𝑘 ∈ N (𝑗 <N 𝑘 → (〈{𝑙 ∣ 𝑙 <Q (𝐹‘𝑘)}, {𝑢 ∣ (𝐹‘𝑘) <Q 𝑢}〉<P (𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑥}, {𝑢 ∣ 𝑥 <Q 𝑢}〉) ∧ 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹‘𝑘) +Q 𝑥) <Q
𝑢}〉))) |
19 | 18 | ex 114 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ Q) ∧ 𝑗 ∈ N) →
((*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥 → ∀𝑘 ∈ N (𝑗 <N 𝑘 → (〈{𝑙 ∣ 𝑙 <Q (𝐹‘𝑘)}, {𝑢 ∣ (𝐹‘𝑘) <Q 𝑢}〉<P (𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑥}, {𝑢 ∣ 𝑥 <Q 𝑢}〉) ∧ 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹‘𝑘) +Q 𝑥) <Q
𝑢}〉)))) |
20 | 19 | reximdva 2572 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ Q) → (∃𝑗 ∈ N
(*Q‘[〈𝑗, 1o〉]
~Q ) <Q 𝑥 → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N
𝑘 → (〈{𝑙 ∣ 𝑙 <Q (𝐹‘𝑘)}, {𝑢 ∣ (𝐹‘𝑘) <Q 𝑢}〉<P (𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑥}, {𝑢 ∣ 𝑥 <Q 𝑢}〉) ∧ 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹‘𝑘) +Q 𝑥) <Q
𝑢}〉)))) |
21 | 2, 20 | mpd 13 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ Q) → ∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → (〈{𝑙 ∣ 𝑙 <Q (𝐹‘𝑘)}, {𝑢 ∣ (𝐹‘𝑘) <Q 𝑢}〉<P (𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑥}, {𝑢 ∣ 𝑥 <Q 𝑢}〉) ∧ 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹‘𝑘) +Q 𝑥) <Q
𝑢}〉))) |
22 | 21 | ralrimiva 2543 |
1
⊢ (𝜑 → ∀𝑥 ∈ Q ∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → (〈{𝑙 ∣ 𝑙 <Q (𝐹‘𝑘)}, {𝑢 ∣ (𝐹‘𝑘) <Q 𝑢}〉<P (𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑥}, {𝑢 ∣ 𝑥 <Q 𝑢}〉) ∧ 𝐿<P 〈{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹‘𝑘) +Q 𝑥) <Q
𝑢}〉))) |