Step | Hyp | Ref
| Expression |
1 | | caucvgprprlemexbt.lt |
. . . . 5
⊢ (𝜑 → (𝐿 +P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P 𝑇) |
2 | | caucvgprpr.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:N⟶P) |
3 | | caucvgprpr.cau |
. . . . . . . 8
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉)))) |
4 | | caucvgprpr.bnd |
. . . . . . . 8
⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) |
5 | | caucvgprpr.lim |
. . . . . . . 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 𝑞}〉}〉 |
6 | 2, 3, 4, 5 | caucvgprprlemclphr 7667 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ P) |
7 | | caucvgprprlemexbt.q |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ Q) |
8 | | nqprlu 7509 |
. . . . . . . 8
⊢ (𝑄 ∈ Q →
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉 ∈
P) |
9 | 7, 8 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉 ∈
P) |
10 | | addclpr 7499 |
. . . . . . 7
⊢ ((𝐿 ∈ P ∧
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉 ∈ P)
→ (𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉) ∈
P) |
11 | 6, 9, 10 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → (𝐿 +P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉) ∈
P) |
12 | | caucvgprprlemexbt.t |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ P) |
13 | | ltdfpr 7468 |
. . . . . 6
⊢ (((𝐿 +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉) ∈ P
∧ 𝑇 ∈
P) → ((𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P 𝑇 ↔ ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) |
14 | 11, 12, 13 | syl2anc 409 |
. . . . 5
⊢ (𝜑 → ((𝐿 +P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P 𝑇 ↔ ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) |
15 | 1, 14 | mpbid 146 |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ Q (𝑥 ∈ (2nd ‘(𝐿 +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇))) |
16 | 6 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) → 𝐿 ∈
P) |
17 | 7 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) → 𝑄 ∈
Q) |
18 | | simprrl 534 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) → 𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉))) |
19 | 16, 17, 18 | prplnqu 7582 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) →
∃𝑦 ∈
(2nd ‘𝐿)(𝑦 +Q 𝑄) = 𝑥) |
20 | | simprl 526 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) → 𝑦 ∈ (2nd ‘𝐿)) |
21 | | breq2 3993 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑦 → (𝑝 <Q 𝑢 ↔ 𝑝 <Q 𝑦)) |
22 | 21 | abbidv 2288 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑦 → {𝑝 ∣ 𝑝 <Q 𝑢} = {𝑝 ∣ 𝑝 <Q 𝑦}) |
23 | | breq1 3992 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑦 → (𝑢 <Q 𝑞 ↔ 𝑦 <Q 𝑞)) |
24 | 23 | abbidv 2288 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑦 → {𝑞 ∣ 𝑢 <Q 𝑞} = {𝑞 ∣ 𝑦 <Q 𝑞}) |
25 | 22, 24 | opeq12d 3773 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑦 → 〈{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q 𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) |
26 | 25 | breq2d 4001 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑦 → (((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉 ↔ ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉)) |
27 | 26 | rexbidv 2471 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑦 → (∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉 ↔ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉)) |
28 | 5 | fveq2i 5499 |
. . . . . . . . . . . . . 14
⊢
(2nd ‘𝐿) = (2nd ‘〈{𝑙 ∈ 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 𝑞}〉}〉) |
29 | | nqex 7325 |
. . . . . . . . . . . . . . . 16
⊢
Q ∈ V |
30 | 29 | rabex 4133 |
. . . . . . . . . . . . . . 15
⊢ {𝑙 ∈ Q ∣
∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)} ∈ V |
31 | 29 | rabex 4133 |
. . . . . . . . . . . . . . 15
⊢ {𝑢 ∈ Q ∣
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} ∈
V |
32 | 30, 31 | op2nd 6126 |
. . . . . . . . . . . . . 14
⊢
(2nd ‘〈{𝑙 ∈ 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 ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} |
33 | 28, 32 | eqtri 2191 |
. . . . . . . . . . . . 13
⊢
(2nd ‘𝐿) = {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} |
34 | 27, 33 | elrab2 2889 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (2nd
‘𝐿) ↔ (𝑦 ∈ Q ∧
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉)) |
35 | 34 | biimpi 119 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (2nd
‘𝐿) → (𝑦 ∈ Q ∧
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉)) |
36 | 35 | simprd 113 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (2nd
‘𝐿) →
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) |
37 | 20, 36 | syl 14 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) → ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) |
38 | | fveq2 5496 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑏 → (𝐹‘𝑟) = (𝐹‘𝑏)) |
39 | | opeq1 3765 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑏 → 〈𝑟, 1o〉 = 〈𝑏,
1o〉) |
40 | 39 | eceq1d 6549 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑏 → [〈𝑟, 1o〉]
~Q = [〈𝑏, 1o〉]
~Q ) |
41 | 40 | fveq2d 5500 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝑏 →
(*Q‘[〈𝑟, 1o〉]
~Q ) = (*Q‘[〈𝑏, 1o〉]
~Q )) |
42 | 41 | breq2d 4001 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑏 → (𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q ) ↔ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q ))) |
43 | 42 | abbidv 2288 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑏 → {𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )} = {𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}) |
44 | 41 | breq1d 3999 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑏 →
((*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞 ↔
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞)) |
45 | 44 | abbidv 2288 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑏 → {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞} = {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}) |
46 | 43, 45 | opeq12d 3773 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑏 → 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) |
47 | 38, 46 | oveq12d 5871 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑏 → ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) = ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)) |
48 | 47 | breq1d 3999 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑏 → (((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉 ↔ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉)) |
49 | 48 | cbvrexv 2697 |
. . . . . . . . 9
⊢
(∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉 ↔ ∃𝑏 ∈ N ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) |
50 | 37, 49 | sylib 121 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) → ∃𝑏 ∈ N ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) |
51 | | simpr 109 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) |
52 | | ltaprg 7581 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P
∧ ℎ ∈
P) → (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P
(ℎ
+P 𝑔))) |
53 | 52 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) ∧ (𝑓 ∈ P ∧
𝑔 ∈ P
∧ ℎ ∈
P)) → (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P
(ℎ
+P 𝑔))) |
54 | 2 | ad4antr 491 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → 𝐹:N⟶P) |
55 | | simplr 525 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → 𝑏 ∈
N) |
56 | 54, 55 | ffvelrnd 5632 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → (𝐹‘𝑏) ∈ P) |
57 | | recnnpr 7510 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ N →
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉 ∈
P) |
58 | 55, 57 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉 ∈
P) |
59 | | addclpr 7499 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑏) ∈ P ∧ 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉 ∈ P) →
((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
60 | 56, 58, 59 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
61 | 20 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → 𝑦 ∈ (2nd
‘𝐿)) |
62 | 35 | simpld 111 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (2nd
‘𝐿) → 𝑦 ∈
Q) |
63 | 61, 62 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → 𝑦 ∈
Q) |
64 | | nqprlu 7509 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ Q →
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉 ∈
P) |
65 | 63, 64 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → 〈{𝑝 ∣ 𝑝 <Q 𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉 ∈
P) |
66 | 9 | ad4antr 491 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉 ∈
P) |
67 | | addcomprg 7540 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
68 | 67 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) ∧ (𝑓 ∈ P ∧
𝑔 ∈ P))
→ (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
69 | 53, 60, 65, 66, 68 | caovord2d 6022 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉 ↔ (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P
(〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉))) |
70 | 51, 69 | mpbid 146 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P
(〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) |
71 | 7 | ad4antr 491 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → 𝑄 ∈
Q) |
72 | | addnqpr 7523 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ Q ∧
𝑄 ∈ Q)
→ 〈{𝑝 ∣
𝑝
<Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q
𝑞}〉 = (〈{𝑝 ∣ 𝑝 <Q 𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) |
73 | 63, 71, 72 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → 〈{𝑝 ∣ 𝑝 <Q (𝑦 +Q
𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q
𝑞}〉 = (〈{𝑝 ∣ 𝑝 <Q 𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) |
74 | 70, 73 | breqtrrd 4017 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
(𝑦
+Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q
𝑞}〉) |
75 | | simplrr 531 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) → (𝑦 +Q
𝑄) = 𝑥) |
76 | 75 | adantr 274 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → (𝑦 +Q
𝑄) = 𝑥) |
77 | | breq2 3993 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 +Q
𝑄) = 𝑥 → (𝑝 <Q (𝑦 +Q
𝑄) ↔ 𝑝 <Q
𝑥)) |
78 | 77 | abbidv 2288 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 +Q
𝑄) = 𝑥 → {𝑝 ∣ 𝑝 <Q (𝑦 +Q
𝑄)} = {𝑝 ∣ 𝑝 <Q 𝑥}) |
79 | | breq1 3992 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 +Q
𝑄) = 𝑥 → ((𝑦 +Q 𝑄) <Q
𝑞 ↔ 𝑥 <Q 𝑞)) |
80 | 79 | abbidv 2288 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 +Q
𝑄) = 𝑥 → {𝑞 ∣ (𝑦 +Q 𝑄) <Q
𝑞} = {𝑞 ∣ 𝑥 <Q 𝑞}) |
81 | 78, 80 | opeq12d 3773 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 +Q
𝑄) = 𝑥 → 〈{𝑝 ∣ 𝑝 <Q (𝑦 +Q
𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q
𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q 𝑥}, {𝑞 ∣ 𝑥 <Q 𝑞}〉) |
82 | 81 | breq2d 4001 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 +Q
𝑄) = 𝑥 → ((((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
(𝑦
+Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q
𝑞}〉 ↔ (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑥}, {𝑞 ∣ 𝑥 <Q 𝑞}〉)) |
83 | 76, 82 | syl 14 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → ((((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
(𝑦
+Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q
𝑞}〉 ↔ (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑥}, {𝑞 ∣ 𝑥 <Q 𝑞}〉)) |
84 | 74, 83 | mpbid 146 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑥}, {𝑞 ∣ 𝑥 <Q 𝑞}〉) |
85 | | simplrl 530 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) → 𝑥 ∈ Q) |
86 | 85 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → 𝑥 ∈
Q) |
87 | | addclpr 7499 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) ∈ P ∧
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉 ∈ P)
→ (((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉) ∈
P) |
88 | 60, 66, 87 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉) ∈
P) |
89 | | nqpru 7514 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ Q ∧
(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉) ∈ P)
→ (𝑥 ∈
(2nd ‘(((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ↔ (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑥}, {𝑞 ∣ 𝑥 <Q 𝑞}〉)) |
90 | 86, 88, 89 | syl2anc 409 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → (𝑥 ∈ (2nd
‘(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ↔ (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑥}, {𝑞 ∣ 𝑥 <Q 𝑞}〉)) |
91 | 84, 90 | mpbird 166 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → 𝑥 ∈ (2nd
‘(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉))) |
92 | | simprrr 535 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) → 𝑥 ∈ (1st
‘𝑇)) |
93 | 92 | ad3antrrr 489 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → 𝑥 ∈ (1st
‘𝑇)) |
94 | 91, 93 | jca 304 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉) → (𝑥 ∈ (2nd
‘(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇))) |
95 | 94 | ex 114 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) ∧ 𝑏 ∈ N) → (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉 → (𝑥 ∈ (2nd
‘(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) |
96 | 95 | reximdva 2572 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) → (∃𝑏 ∈ N ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑦}, {𝑞 ∣ 𝑦 <Q 𝑞}〉 → ∃𝑏 ∈ N (𝑥 ∈ (2nd
‘(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) |
97 | 50, 96 | mpd 13 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) ∧ (𝑦 ∈ (2nd
‘𝐿) ∧ (𝑦 +Q
𝑄) = 𝑥)) → ∃𝑏 ∈ N (𝑥 ∈ (2nd ‘(((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇))) |
98 | 19, 97 | rexlimddv 2592 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) →
∃𝑏 ∈
N (𝑥 ∈
(2nd ‘(((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇))) |
99 | 98 | expr 373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ Q) → ((𝑥 ∈ (2nd
‘(𝐿
+P 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)) →
∃𝑏 ∈
N (𝑥 ∈
(2nd ‘(((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) |
100 | 99 | reximdva 2572 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ Q (𝑥 ∈ (2nd ‘(𝐿 +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)) →
∃𝑥 ∈
Q ∃𝑏
∈ N (𝑥
∈ (2nd ‘(((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) |
101 | 15, 100 | mpd 13 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ Q ∃𝑏 ∈ N (𝑥 ∈ (2nd
‘(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇))) |
102 | | rexcom 2634 |
. . 3
⊢
(∃𝑥 ∈
Q ∃𝑏
∈ N (𝑥
∈ (2nd ‘(((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)) ↔
∃𝑏 ∈
N ∃𝑥
∈ Q (𝑥
∈ (2nd ‘(((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇))) |
103 | 101, 102 | sylib 121 |
. 2
⊢ (𝜑 → ∃𝑏 ∈ N ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇))) |
104 | 2 | ffvelrnda 5631 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ N) → (𝐹‘𝑏) ∈ P) |
105 | 57 | adantl 275 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ N) → 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉 ∈
P) |
106 | 104, 105,
59 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ N) → ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
107 | 9 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ N) → 〈{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉 ∈
P) |
108 | 106, 107,
87 | syl2anc 409 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ N) → (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉) ∈
P) |
109 | 12 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ N) → 𝑇 ∈
P) |
110 | | ltdfpr 7468 |
. . . 4
⊢
(((((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉) ∈ P
∧ 𝑇 ∈
P) → ((((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P 𝑇 ↔ ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) |
111 | 108, 109,
110 | syl2anc 409 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ N) → ((((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P 𝑇 ↔ ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) |
112 | 111 | rexbidva 2467 |
. 2
⊢ (𝜑 → (∃𝑏 ∈ N (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P 𝑇 ↔ ∃𝑏 ∈ N
∃𝑥 ∈
Q (𝑥 ∈
(2nd ‘(((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)) ∧ 𝑥 ∈ (1st
‘𝑇)))) |
113 | 103, 112 | mpbird 166 |
1
⊢ (𝜑 → ∃𝑏 ∈ N (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) +P
〈{𝑝 ∣ 𝑝 <Q
𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}〉)<P 𝑇) |