Proof of Theorem pitoregt0
Step | Hyp | Ref
| Expression |
1 | | 1pr 7516 |
. . . . . 6
⊢
1P ∈ P |
2 | | addclpr 7499 |
. . . . . 6
⊢
((1P ∈ P ∧
1P ∈ P) →
(1P +P
1P) ∈ P) |
3 | 1, 1, 2 | mp2an 424 |
. . . . 5
⊢
(1P +P
1P) ∈ P |
4 | | nnprlu 7515 |
. . . . 5
⊢ (𝑁 ∈ N →
〈{𝑙 ∣ 𝑙 <Q
[〈𝑁,
1o〉] ~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 ∈
P) |
5 | | ltaddpr 7559 |
. . . . 5
⊢
(((1P +P
1P) ∈ P ∧ 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 ∈ P) →
(1P +P
1P)<P
((1P +P
1P) +P 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉)) |
6 | 3, 4, 5 | sylancr 412 |
. . . 4
⊢ (𝑁 ∈ N →
(1P +P
1P)<P
((1P +P
1P) +P 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉)) |
7 | 1 | a1i 9 |
. . . . . 6
⊢ (𝑁 ∈ N →
1P ∈ P) |
8 | | addassprg 7541 |
. . . . . 6
⊢
((1P ∈ P ∧
1P ∈ P ∧ 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 ∈ P) →
((1P +P
1P) +P 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉) = (1P
+P (1P
+P 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉))) |
9 | 7, 7, 4, 8 | syl3anc 1233 |
. . . . 5
⊢ (𝑁 ∈ N →
((1P +P
1P) +P 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉) = (1P
+P (1P
+P 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉))) |
10 | | addcomprg 7540 |
. . . . . . 7
⊢
((1P ∈ P ∧ 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 ∈ P) →
(1P +P 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉) = (〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P)) |
11 | 1, 4, 10 | sylancr 412 |
. . . . . 6
⊢ (𝑁 ∈ N →
(1P +P 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉) = (〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P)) |
12 | 11 | oveq2d 5869 |
. . . . 5
⊢ (𝑁 ∈ N →
(1P +P
(1P +P 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉)) = (1P
+P (〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P))) |
13 | 9, 12 | eqtrd 2203 |
. . . 4
⊢ (𝑁 ∈ N →
((1P +P
1P) +P 〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉) = (1P
+P (〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P))) |
14 | 6, 13 | breqtrd 4015 |
. . 3
⊢ (𝑁 ∈ N →
(1P +P
1P)<P
(1P +P (〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P))) |
15 | | addclpr 7499 |
. . . . 5
⊢
((〈{𝑙 ∣
𝑙
<Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 ∈ P ∧
1P ∈ P) → (〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P) ∈ P) |
16 | 4, 1, 15 | sylancl 411 |
. . . 4
⊢ (𝑁 ∈ N →
(〈{𝑙 ∣ 𝑙 <Q
[〈𝑁,
1o〉] ~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P) ∈ P) |
17 | | ltsrprg 7709 |
. . . . 5
⊢
(((1P ∈ P ∧
1P ∈ P) ∧ ((〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P) ∈ P ∧
1P ∈ P)) →
([〈1P, 1P〉]
~R <R [〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ↔ (1P
+P
1P)<P
(1P +P (〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P)))) |
18 | 1, 1, 17 | mpanl12 434 |
. . . 4
⊢
(((〈{𝑙 ∣
𝑙
<Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P) ∈ P ∧
1P ∈ P) →
([〈1P, 1P〉]
~R <R [〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ↔ (1P
+P
1P)<P
(1P +P (〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P)))) |
19 | 16, 1, 18 | sylancl 411 |
. . 3
⊢ (𝑁 ∈ N →
([〈1P, 1P〉]
~R <R [〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ↔ (1P
+P
1P)<P
(1P +P (〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P)))) |
20 | 14, 19 | mpbird 166 |
. 2
⊢ (𝑁 ∈ N →
[〈1P, 1P〉]
~R <R [〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ) |
21 | | df-0 7781 |
. . . 4
⊢ 0 =
〈0R,
0R〉 |
22 | 21 | breq1i 3996 |
. . 3
⊢ (0
<ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ↔
〈0R, 0R〉
<ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ,
0R〉) |
23 | | ltresr 7801 |
. . 3
⊢
(〈0R, 0R〉
<ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ↔
0R <R [〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ) |
24 | | df-0r 7693 |
. . . 4
⊢
0R = [〈1P,
1P〉] ~R |
25 | 24 | breq1i 3996 |
. . 3
⊢
(0R <R
[〈(〈{𝑙 ∣
𝑙
<Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ↔ [〈1P,
1P〉] ~R
<R [〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ) |
26 | 22, 23, 25 | 3bitri 205 |
. 2
⊢ (0
<ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ↔
[〈1P, 1P〉]
~R <R [〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ) |
27 | 20, 26 | sylibr 133 |
1
⊢ (𝑁 ∈ N → 0
<ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑁, 1o〉]
~Q }, {𝑢 ∣ [〈𝑁, 1o〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ,
0R〉) |