Step | Hyp | Ref
| Expression |
1 | | caucvgprpr.f |
. . 3
⊢ (𝜑 → 𝐹:N⟶P) |
2 | | caucvgprpr.cau |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q
(*Q‘[⟨𝑛, 1o⟩]
~Q )}, {𝑢 ∣
(*Q‘[⟨𝑛, 1o⟩]
~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q
(*Q‘[⟨𝑛, 1o⟩]
~Q )}, {𝑢 ∣
(*Q‘[⟨𝑛, 1o⟩]
~Q ) <Q 𝑢}⟩)))) |
3 | | caucvgprpr.bnd |
. . 3
⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) |
4 | | eqid 2187 |
. . 3
⊢
⟨{𝑙 ∈
Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ = ⟨{𝑙 ∈ Q ∣
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ |
5 | 1, 2, 3, 4 | caucvgprprlemcl 7716 |
. 2
⊢ (𝜑 → ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ ∈
P) |
6 | 1, 2, 3, 4 | caucvgprprlemlim 7723 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ P ∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → ((𝐹‘𝑘)<P (⟨{𝑙 ∈ Q ∣
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩
+P 𝑥) ∧ ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩<P
((𝐹‘𝑘) +P
𝑥)))) |
7 | | oveq1 5895 |
. . . . . . . 8
⊢ (𝑦 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ → (𝑦 +P
𝑥) = (⟨{𝑙 ∈ Q ∣
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩
+P 𝑥)) |
8 | 7 | breq2d 4027 |
. . . . . . 7
⊢ (𝑦 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ → ((𝐹‘𝑘)<P (𝑦 +P
𝑥) ↔ (𝐹‘𝑘)<P (⟨{𝑙 ∈ Q ∣
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩
+P 𝑥))) |
9 | | breq1 4018 |
. . . . . . 7
⊢ (𝑦 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ → (𝑦<P
((𝐹‘𝑘) +P
𝑥) ↔ ⟨{𝑙 ∈ Q ∣
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩<P
((𝐹‘𝑘) +P
𝑥))) |
10 | 8, 9 | anbi12d 473 |
. . . . . 6
⊢ (𝑦 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ → (((𝐹‘𝑘)<P (𝑦 +P
𝑥) ∧ 𝑦<P ((𝐹‘𝑘) +P 𝑥)) ↔ ((𝐹‘𝑘)<P (⟨{𝑙 ∈ Q ∣
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩
+P 𝑥) ∧ ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩<P
((𝐹‘𝑘) +P
𝑥)))) |
11 | 10 | imbi2d 230 |
. . . . 5
⊢ (𝑦 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ → ((𝑗 <N
𝑘 → ((𝐹‘𝑘)<P (𝑦 +P
𝑥) ∧ 𝑦<P ((𝐹‘𝑘) +P 𝑥))) ↔ (𝑗 <N 𝑘 → ((𝐹‘𝑘)<P (⟨{𝑙 ∈ Q ∣
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩
+P 𝑥) ∧ ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩<P
((𝐹‘𝑘) +P
𝑥))))) |
12 | 11 | rexralbidv 2513 |
. . . 4
⊢ (𝑦 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ →
(∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → ((𝐹‘𝑘)<P (𝑦 +P
𝑥) ∧ 𝑦<P ((𝐹‘𝑘) +P 𝑥))) ↔ ∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → ((𝐹‘𝑘)<P (⟨{𝑙 ∈ Q ∣
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩
+P 𝑥) ∧ ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩<P
((𝐹‘𝑘) +P
𝑥))))) |
13 | 12 | ralbidv 2487 |
. . 3
⊢ (𝑦 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ →
(∀𝑥 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘)<P (𝑦 +P
𝑥) ∧ 𝑦<P ((𝐹‘𝑘) +P 𝑥))) ↔ ∀𝑥 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → ((𝐹‘𝑘)<P (⟨{𝑙 ∈ Q ∣
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩
+P 𝑥) ∧ ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩<P
((𝐹‘𝑘) +P
𝑥))))) |
14 | 13 | rspcev 2853 |
. 2
⊢
((⟨{𝑙 ∈
Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ ∈
P ∧ ∀𝑥 ∈ P ∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → ((𝐹‘𝑘)<P (⟨{𝑙 ∈ Q ∣
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩
+P 𝑥) ∧ ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩<P
((𝐹‘𝑘) +P
𝑥)))) → ∃𝑦 ∈ P
∀𝑥 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘)<P (𝑦 +P
𝑥) ∧ 𝑦<P ((𝐹‘𝑘) +P 𝑥)))) |
15 | 5, 6, 14 | syl2anc 411 |
1
⊢ (𝜑 → ∃𝑦 ∈ P ∀𝑥 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → ((𝐹‘𝑘)<P (𝑦 +P
𝑥) ∧ 𝑦<P ((𝐹‘𝑘) +P 𝑥)))) |