Step | Hyp | Ref
| Expression |
1 | | caucvgprprlemaddq.ex |
. 2
⊢ (𝜑 → ∃𝑟 ∈ N (𝑋 +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄)) |
2 | | nfv 1521 |
. . 3
⊢
Ⅎ𝑟𝜑 |
3 | | nfcv 2312 |
. . . 4
⊢
Ⅎ𝑟𝑋 |
4 | | nfcv 2312 |
. . . 4
⊢
Ⅎ𝑟<P |
5 | | caucvgprpr.lim |
. . . . . 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 𝑞}〉}〉 |
6 | | nfre1 2513 |
. . . . . . . 8
⊢
Ⅎ𝑟∃𝑟 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟) |
7 | | nfcv 2312 |
. . . . . . . 8
⊢
Ⅎ𝑟Q |
8 | 6, 7 | nfrabxy 2650 |
. . . . . . 7
⊢
Ⅎ𝑟{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)} |
9 | | nfre1 2513 |
. . . . . . . 8
⊢
Ⅎ𝑟∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉 |
10 | 9, 7 | nfrabxy 2650 |
. . . . . . 7
⊢
Ⅎ𝑟{𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} |
11 | 8, 10 | nfop 3779 |
. . . . . 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 𝑞}〉}〉 |
12 | 5, 11 | nfcxfr 2309 |
. . . . 5
⊢
Ⅎ𝑟𝐿 |
13 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑟
+P |
14 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑟𝑄 |
15 | 12, 13, 14 | nfov 5881 |
. . . 4
⊢
Ⅎ𝑟(𝐿 +P 𝑄) |
16 | 3, 4, 15 | nfbr 4033 |
. . 3
⊢
Ⅎ𝑟 𝑋<P
(𝐿
+P 𝑄) |
17 | | caucvgprpr.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:N⟶P) |
18 | 17 | ad2antrr 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
𝐹:N⟶P) |
19 | | caucvgprpr.cau |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉)))) |
20 | 19 | ad2antrr 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
∀𝑛 ∈
N ∀𝑘
∈ N (𝑛
<N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉)))) |
21 | | simpr 109 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
𝑏 ∈
N) |
22 | | simplrl 530 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
𝑟 ∈
N) |
23 | 18, 20, 21, 22 | caucvgprprlemnbj 7648 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
¬ (((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉)<P (𝐹‘𝑟)) |
24 | 18, 21 | ffvelrnd 5630 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
(𝐹‘𝑏) ∈ P) |
25 | | recnnpr 7503 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ N →
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉 ∈
P) |
26 | 25 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉 ∈
P) |
27 | | addclpr 7492 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑏) ∈ P ∧ 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉 ∈ P) →
((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) ∈
P) |
28 | 24, 26, 27 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) ∈
P) |
29 | | recnnpr 7503 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ N →
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 ∈
P) |
30 | 22, 29 | syl 14 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 ∈
P) |
31 | | caucvgprprlemaddq.q |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑄 ∈ P) |
32 | 31 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
𝑄 ∈
P) |
33 | | addassprg 7534 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) ∈ P ∧
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 ∈ P ∧ 𝑄 ∈ P) →
((((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉) +P 𝑄) = (((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 +P 𝑄))) |
34 | 28, 30, 32, 33 | syl3anc 1233 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
((((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉) +P 𝑄) = (((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 +P 𝑄))) |
35 | 34 | breq1d 3997 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
(((((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉) +P 𝑄)<P
((𝐹‘𝑟) +P
𝑄) ↔ (((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 +P 𝑄))<P
((𝐹‘𝑟) +P
𝑄))) |
36 | | ltaprg 7574 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P
∧ ℎ ∈
P) → (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P
(ℎ
+P 𝑔))) |
37 | 36 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) ∧
(𝑓 ∈ P
∧ 𝑔 ∈
P ∧ ℎ
∈ P)) → (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P
(ℎ
+P 𝑔))) |
38 | | addclpr 7492 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) ∈ P ∧
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 ∈ P) →
(((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉) ∈
P) |
39 | 28, 30, 38 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
(((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉) ∈
P) |
40 | 18, 22 | ffvelrnd 5630 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
(𝐹‘𝑟) ∈ P) |
41 | | addcomprg 7533 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
42 | 41 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) ∧
(𝑓 ∈ P
∧ 𝑔 ∈
P)) → (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
43 | 37, 39, 40, 32, 42 | caovord2d 6020 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
((((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉)<P (𝐹‘𝑟) ↔ ((((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉) +P 𝑄)<P
((𝐹‘𝑟) +P
𝑄))) |
44 | | addcomprg 7533 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ P ∧
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 ∈ P) → (𝑄 +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉) = (〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 +P 𝑄)) |
45 | 32, 30, 44 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
(𝑄
+P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉) = (〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 +P 𝑄)) |
46 | 45 | oveq2d 5867 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
(((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P (𝑄 +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉)) = (((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 +P 𝑄))) |
47 | 46 | breq1d 3997 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
((((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P (𝑄 +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉))<P
((𝐹‘𝑟) +P
𝑄) ↔ (((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 +P 𝑄))<P
((𝐹‘𝑟) +P
𝑄))) |
48 | 35, 43, 47 | 3bitr4rd 220 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
((((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P (𝑄 +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉))<P
((𝐹‘𝑟) +P
𝑄) ↔ (((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉)<P (𝐹‘𝑟))) |
49 | 23, 48 | mtbird 668 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ 𝑏 ∈ N) →
¬ (((𝐹‘𝑏) +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P (𝑄 +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉))<P
((𝐹‘𝑟) +P
𝑄)) |
50 | 49 | nrexdv 2563 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → ¬
∃𝑏 ∈
N (((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P (𝑄 +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉))<P
((𝐹‘𝑟) +P
𝑄)) |
51 | | breq1 3990 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑙 → (𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q ) ↔ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q ))) |
52 | 51 | cbvabv 2295 |
. . . . . . . . . . . . 13
⊢ {𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )} = {𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )} |
53 | | breq2 3991 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑢 →
((*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞 ↔
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢)) |
54 | 53 | cbvabv 2295 |
. . . . . . . . . . . . 13
⊢ {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞} = {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢} |
55 | 52, 54 | opeq12i 3768 |
. . . . . . . . . . . 12
⊢
〈{𝑝 ∣
𝑝
<Q (*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉 = 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉 |
56 | 55 | oveq2i 5862 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) = ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) |
57 | | breq1 3990 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑙 → (𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q ) ↔ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q ))) |
58 | 57 | cbvabv 2295 |
. . . . . . . . . . . . 13
⊢ {𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )} = {𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )} |
59 | | breq2 3991 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑢 →
((*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞 ↔
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢)) |
60 | 59 | cbvabv 2295 |
. . . . . . . . . . . . 13
⊢ {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞} = {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢} |
61 | 58, 60 | opeq12i 3768 |
. . . . . . . . . . . 12
⊢
〈{𝑝 ∣
𝑝
<Q (*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉 = 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉 |
62 | 61 | oveq2i 5862 |
. . . . . . . . . . 11
⊢ (𝑄 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) = (𝑄 +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉) |
63 | 56, 62 | oveq12i 5863 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P (𝑄 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)) = (((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P (𝑄 +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉)) |
64 | 63 | breq1i 3994 |
. . . . . . . . 9
⊢ ((((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P (𝑄 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉))<P
((𝐹‘𝑟) +P
𝑄) ↔ (((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P (𝑄 +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉))<P
((𝐹‘𝑟) +P
𝑄)) |
65 | 64 | rexbii 2477 |
. . . . . . . 8
⊢
(∃𝑏 ∈
N (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P (𝑄 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉))<P
((𝐹‘𝑟) +P
𝑄) ↔ ∃𝑏 ∈ N (((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑢}〉) +P (𝑄 +P
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑢}〉))<P
((𝐹‘𝑟) +P
𝑄)) |
66 | 50, 65 | sylnibr 672 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → ¬
∃𝑏 ∈
N (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P (𝑄 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉))<P
((𝐹‘𝑟) +P
𝑄)) |
67 | 17 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → 𝐹:N⟶P) |
68 | 19 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → ∀𝑛 ∈ N
∀𝑘 ∈
N (𝑛
<N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉)))) |
69 | | caucvgprpr.bnd |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) |
70 | 69 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → ∀𝑚 ∈ N 𝐴<P
(𝐹‘𝑚)) |
71 | 31 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → 𝑄 ∈
P) |
72 | | simprl 526 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → 𝑟 ∈
N) |
73 | 67, 68, 70, 5, 71, 72 | caucvgprprlemexb 7662 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → (((𝐿 +P
𝑄)
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄) → ∃𝑏 ∈ N (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P (𝑄 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉))<P
((𝐹‘𝑟) +P
𝑄))) |
74 | 66, 73 | mtod 658 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → ¬ ((𝐿 +P
𝑄)
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄)) |
75 | | simprr 527 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄)) |
76 | | caucvgprprlemaddq.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ P) |
77 | 76 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → 𝑋 ∈
P) |
78 | | recnnpr 7503 |
. . . . . . . . . 10
⊢ (𝑟 ∈ N →
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉 ∈
P) |
79 | 72, 78 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉 ∈
P) |
80 | | addclpr 7492 |
. . . . . . . . 9
⊢ ((𝑋 ∈ P ∧
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉 ∈ P) → (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
81 | 77, 79, 80 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
82 | 67, 72 | ffvelrnd 5630 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → (𝐹‘𝑟) ∈ P) |
83 | | addclpr 7492 |
. . . . . . . . 9
⊢ (((𝐹‘𝑟) ∈ P ∧ 𝑄 ∈ P) →
((𝐹‘𝑟) +P
𝑄) ∈
P) |
84 | 82, 71, 83 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → ((𝐹‘𝑟) +P 𝑄) ∈
P) |
85 | 17, 19, 69, 5 | caucvgprprlemcl 7659 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈ P) |
86 | 85 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → 𝐿 ∈
P) |
87 | | addclpr 7492 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ P ∧
𝑄 ∈ P)
→ (𝐿
+P 𝑄) ∈ P) |
88 | 86, 71, 87 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → (𝐿 +P
𝑄) ∈
P) |
89 | | addclpr 7492 |
. . . . . . . . 9
⊢ (((𝐿 +P
𝑄) ∈ P
∧ 〈{𝑝 ∣
𝑝
<Q (*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉 ∈ P) →
((𝐿
+P 𝑄) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
90 | 88, 79, 89 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → ((𝐿 +P
𝑄)
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
91 | | ltsopr 7551 |
. . . . . . . . 9
⊢
<P Or P |
92 | | sowlin 4303 |
. . . . . . . . 9
⊢
((<P Or P ∧ ((𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) ∈ P ∧ ((𝐹‘𝑟) +P 𝑄) ∈ P ∧
((𝐿
+P 𝑄) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) ∈ P)) →
((𝑋
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄) → ((𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐿
+P 𝑄) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) ∨ ((𝐿 +P 𝑄) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄)))) |
93 | 91, 92 | mpan 422 |
. . . . . . . 8
⊢ (((𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) ∈ P ∧ ((𝐹‘𝑟) +P 𝑄) ∈ P ∧
((𝐿
+P 𝑄) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) ∈ P) →
((𝑋
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄) → ((𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐿
+P 𝑄) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) ∨ ((𝐿 +P 𝑄) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄)))) |
94 | 81, 84, 90, 93 | syl3anc 1233 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → ((𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄) → ((𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐿
+P 𝑄) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) ∨ ((𝐿 +P 𝑄) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄)))) |
95 | 75, 94 | mpd 13 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → ((𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐿
+P 𝑄) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) ∨ ((𝐿 +P 𝑄) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) |
96 | 74, 95 | ecased 1344 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐿
+P 𝑄) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)) |
97 | 36 | adantl 275 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ (𝑓 ∈ P ∧
𝑔 ∈ P
∧ ℎ ∈
P)) → (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P
(ℎ
+P 𝑔))) |
98 | 41 | adantl 275 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) ∧ (𝑓 ∈ P ∧
𝑔 ∈ P))
→ (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
99 | 97, 77, 88, 79, 98 | caovord2d 6020 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → (𝑋<P
(𝐿
+P 𝑄) ↔ (𝑋 +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐿
+P 𝑄) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉))) |
100 | 96, 99 | mpbird 166 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄))) → 𝑋<P
(𝐿
+P 𝑄)) |
101 | 100 | exp32 363 |
. . 3
⊢ (𝜑 → (𝑟 ∈ N → ((𝑋 +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄) → 𝑋<P (𝐿 +P
𝑄)))) |
102 | 2, 16, 101 | rexlimd 2584 |
. 2
⊢ (𝜑 → (∃𝑟 ∈ N (𝑋 +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑟) +P
𝑄) → 𝑋<P (𝐿 +P
𝑄))) |
103 | 1, 102 | mpd 13 |
1
⊢ (𝜑 → 𝑋<P (𝐿 +P
𝑄)) |