Proof of Theorem pitonnlem2
Step | Hyp | Ref
| Expression |
1 | | df-1 7782 |
. . . 4
⊢ 1 =
〈1R,
0R〉 |
2 | 1 | oveq2i 5864 |
. . 3
⊢
(〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 + 1) =
(〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 +
〈1R,
0R〉) |
3 | | nnprlu 7515 |
. . . . . . . 8
⊢ (𝐾 ∈ N →
〈{𝑙 ∣ 𝑙 <Q
[〈𝐾,
1o〉] ~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 ∈
P) |
4 | | 1pr 7516 |
. . . . . . . 8
⊢
1P ∈ P |
5 | | addclpr 7499 |
. . . . . . . 8
⊢
((〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 ∈ P ∧
1P ∈ P) → (〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) ∈ P) |
6 | 3, 4, 5 | sylancl 411 |
. . . . . . 7
⊢ (𝐾 ∈ N →
(〈{𝑙 ∣ 𝑙 <Q
[〈𝐾,
1o〉] ~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) ∈ P) |
7 | | opelxpi 4643 |
. . . . . . 7
⊢
(((〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) ∈ P ∧
1P ∈ P) → 〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉 ∈
(P × P)) |
8 | 6, 4, 7 | sylancl 411 |
. . . . . 6
⊢ (𝐾 ∈ N →
〈(〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉 ∈
(P × P)) |
9 | | enrex 7699 |
. . . . . . 7
⊢
~R ∈ V |
10 | 9 | ecelqsi 6567 |
. . . . . 6
⊢
(〈(〈{𝑙
∣ 𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉 ∈
(P × P) → [〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ ((P × P)
/ ~R )) |
11 | 8, 10 | syl 14 |
. . . . 5
⊢ (𝐾 ∈ N →
[〈(〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ ((P × P)
/ ~R )) |
12 | | df-nr 7689 |
. . . . 5
⊢
R = ((P × P) /
~R ) |
13 | 11, 12 | eleqtrrdi 2264 |
. . . 4
⊢ (𝐾 ∈ N →
[〈(〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R) |
14 | | 1sr 7713 |
. . . 4
⊢
1R ∈ R |
15 | | addresr 7799 |
. . . 4
⊢
(([〈(〈{𝑙
∣ 𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R ∧
1R ∈ R) →
(〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 +
〈1R, 0R〉) =
〈([〈(〈{𝑙
∣ 𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R +R
1R),
0R〉) |
16 | 13, 14, 15 | sylancl 411 |
. . 3
⊢ (𝐾 ∈ N →
(〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 +
〈1R, 0R〉) =
〈([〈(〈{𝑙
∣ 𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R +R
1R),
0R〉) |
17 | 2, 16 | eqtrid 2215 |
. 2
⊢ (𝐾 ∈ N →
(〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 + 1) =
〈([〈(〈{𝑙
∣ 𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R +R
1R),
0R〉) |
18 | | pitonnlem1p1 7808 |
. . . . 5
⊢
((〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) ∈ P →
[〈((〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) +P
(1P +P
1P)), (1P
+P 1P)〉]
~R = [〈((〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) +P
1P), 1P〉]
~R ) |
19 | 6, 18 | syl 14 |
. . . 4
⊢ (𝐾 ∈ N →
[〈((〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) +P
(1P +P
1P)), (1P
+P 1P)〉]
~R = [〈((〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) +P
1P), 1P〉]
~R ) |
20 | | df-1r 7694 |
. . . . . 6
⊢
1R = [〈(1P
+P 1P),
1P〉] ~R |
21 | 20 | oveq2i 5864 |
. . . . 5
⊢
([〈(〈{𝑙
∣ 𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R +R
1R) = ([〈(〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R +R
[〈(1P +P
1P), 1P〉]
~R ) |
22 | | addclpr 7499 |
. . . . . . . 8
⊢
((1P ∈ P ∧
1P ∈ P) →
(1P +P
1P) ∈ P) |
23 | 4, 4, 22 | mp2an 424 |
. . . . . . 7
⊢
(1P +P
1P) ∈ P |
24 | | addsrpr 7707 |
. . . . . . . 8
⊢
((((〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) ∈ P ∧
1P ∈ P) ∧
((1P +P
1P) ∈ P ∧
1P ∈ P)) →
([〈(〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R +R
[〈(1P +P
1P), 1P〉]
~R ) = [〈((〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) +P
(1P +P
1P)), (1P
+P 1P)〉]
~R ) |
25 | 4, 24 | mpanl2 433 |
. . . . . . 7
⊢
(((〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) ∈ P ∧
((1P +P
1P) ∈ P ∧
1P ∈ P)) →
([〈(〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R +R
[〈(1P +P
1P), 1P〉]
~R ) = [〈((〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) +P
(1P +P
1P)), (1P
+P 1P)〉]
~R ) |
26 | 23, 4, 25 | mpanr12 437 |
. . . . . 6
⊢
((〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) ∈ P →
([〈(〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R +R
[〈(1P +P
1P), 1P〉]
~R ) = [〈((〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) +P
(1P +P
1P)), (1P
+P 1P)〉]
~R ) |
27 | 6, 26 | syl 14 |
. . . . 5
⊢ (𝐾 ∈ N →
([〈(〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R +R
[〈(1P +P
1P), 1P〉]
~R ) = [〈((〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) +P
(1P +P
1P)), (1P
+P 1P)〉]
~R ) |
28 | 21, 27 | eqtrid 2215 |
. . . 4
⊢ (𝐾 ∈ N →
([〈(〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R +R
1R) = [〈((〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) +P
(1P +P
1P)), (1P
+P 1P)〉]
~R ) |
29 | | addpinq1 7426 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ N →
[〈(𝐾
+N 1o), 1o〉]
~Q = ([〈𝐾, 1o〉]
~Q +Q
1Q)) |
30 | 29 | breq2d 4001 |
. . . . . . . . . 10
⊢ (𝐾 ∈ N →
(𝑙
<Q [〈(𝐾 +N 1o),
1o〉] ~Q ↔ 𝑙 <Q ([〈𝐾, 1o〉]
~Q +Q
1Q))) |
31 | 30 | abbidv 2288 |
. . . . . . . . 9
⊢ (𝐾 ∈ N →
{𝑙 ∣ 𝑙 <Q
[〈(𝐾
+N 1o), 1o〉]
~Q } = {𝑙 ∣ 𝑙 <Q ([〈𝐾, 1o〉]
~Q +Q
1Q)}) |
32 | 29 | breq1d 3999 |
. . . . . . . . . 10
⊢ (𝐾 ∈ N →
([〈(𝐾
+N 1o), 1o〉]
~Q <Q 𝑢 ↔ ([〈𝐾, 1o〉]
~Q +Q
1Q) <Q 𝑢)) |
33 | 32 | abbidv 2288 |
. . . . . . . . 9
⊢ (𝐾 ∈ N →
{𝑢 ∣ [〈(𝐾 +N
1o), 1o〉] ~Q
<Q 𝑢} = {𝑢 ∣ ([〈𝐾, 1o〉]
~Q +Q
1Q) <Q 𝑢}) |
34 | 31, 33 | opeq12d 3773 |
. . . . . . . 8
⊢ (𝐾 ∈ N →
〈{𝑙 ∣ 𝑙 <Q
[〈(𝐾
+N 1o), 1o〉]
~Q }, {𝑢 ∣ [〈(𝐾 +N 1o),
1o〉] ~Q <Q
𝑢}〉 = 〈{𝑙 ∣ 𝑙 <Q ([〈𝐾, 1o〉]
~Q +Q
1Q)}, {𝑢 ∣ ([〈𝐾, 1o〉]
~Q +Q
1Q) <Q 𝑢}〉) |
35 | | nnnq 7384 |
. . . . . . . . 9
⊢ (𝐾 ∈ N →
[〈𝐾,
1o〉] ~Q ∈
Q) |
36 | | addnqpr1 7524 |
. . . . . . . . 9
⊢
([〈𝐾,
1o〉] ~Q ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
([〈𝐾,
1o〉] ~Q +Q
1Q)}, {𝑢 ∣ ([〈𝐾, 1o〉]
~Q +Q
1Q) <Q 𝑢}〉 = (〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P)) |
37 | 35, 36 | syl 14 |
. . . . . . . 8
⊢ (𝐾 ∈ N →
〈{𝑙 ∣ 𝑙 <Q
([〈𝐾,
1o〉] ~Q +Q
1Q)}, {𝑢 ∣ ([〈𝐾, 1o〉]
~Q +Q
1Q) <Q 𝑢}〉 = (〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P)) |
38 | 34, 37 | eqtrd 2203 |
. . . . . . 7
⊢ (𝐾 ∈ N →
〈{𝑙 ∣ 𝑙 <Q
[〈(𝐾
+N 1o), 1o〉]
~Q }, {𝑢 ∣ [〈(𝐾 +N 1o),
1o〉] ~Q <Q
𝑢}〉 = (〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P)) |
39 | 38 | oveq1d 5868 |
. . . . . 6
⊢ (𝐾 ∈ N →
(〈{𝑙 ∣ 𝑙 <Q
[〈(𝐾
+N 1o), 1o〉]
~Q }, {𝑢 ∣ [〈(𝐾 +N 1o),
1o〉] ~Q <Q
𝑢}〉
+P 1P) = ((〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) +P
1P)) |
40 | 39 | opeq1d 3771 |
. . . . 5
⊢ (𝐾 ∈ N →
〈(〈{𝑙 ∣
𝑙
<Q [〈(𝐾 +N 1o),
1o〉] ~Q }, {𝑢 ∣ [〈(𝐾 +N 1o),
1o〉] ~Q <Q
𝑢}〉
+P 1P),
1P〉 = 〈((〈{𝑙 ∣ 𝑙 <Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) +P
1P),
1P〉) |
41 | 40 | eceq1d 6549 |
. . . 4
⊢ (𝐾 ∈ N →
[〈(〈{𝑙 ∣
𝑙
<Q [〈(𝐾 +N 1o),
1o〉] ~Q }, {𝑢 ∣ [〈(𝐾 +N 1o),
1o〉] ~Q <Q
𝑢}〉
+P 1P),
1P〉] ~R =
[〈((〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P) +P
1P), 1P〉]
~R ) |
42 | 19, 28, 41 | 3eqtr4d 2213 |
. . 3
⊢ (𝐾 ∈ N →
([〈(〈{𝑙 ∣
𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R +R
1R) = [〈(〈{𝑙 ∣ 𝑙 <Q [〈(𝐾 +N
1o), 1o〉] ~Q }, {𝑢 ∣ [〈(𝐾 +N
1o), 1o〉] ~Q
<Q 𝑢}〉 +P
1P), 1P〉]
~R ) |
43 | 42 | opeq1d 3771 |
. 2
⊢ (𝐾 ∈ N →
〈([〈(〈{𝑙
∣ 𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R +R
1R), 0R〉 =
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈(𝐾 +N 1o),
1o〉] ~Q }, {𝑢 ∣ [〈(𝐾 +N 1o),
1o〉] ~Q <Q
𝑢}〉
+P 1P),
1P〉] ~R ,
0R〉) |
44 | 17, 43 | eqtrd 2203 |
1
⊢ (𝐾 ∈ N →
(〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝐾, 1o〉]
~Q }, {𝑢 ∣ [〈𝐾, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 + 1) =
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈(𝐾 +N 1o),
1o〉] ~Q }, {𝑢 ∣ [〈(𝐾 +N 1o),
1o〉] ~Q <Q
𝑢}〉
+P 1P),
1P〉] ~R ,
0R〉) |