Step | Hyp | Ref
| Expression |
1 | | 1pr 7552 |
. . . . . 6
⊢
1P ∈ P |
2 | | addclpr 7535 |
. . . . . 6
⊢
((1P ∈ P ∧
1P ∈ P) →
(1P +P
1P) ∈ P) |
3 | 1, 1, 2 | mp2an 426 |
. . . . 5
⊢
(1P +P
1P) ∈ P |
4 | | nnprlu 7551 |
. . . . 5
⊢ (𝑁 ∈ N →
⟨{𝑙 ∣ 𝑙 <Q
[⟨𝑁,
1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ ∈
P) |
5 | | ltaddpr 7595 |
. . . . 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 414 |
. . . 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 7577 |
. . . . . 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 1238 |
. . . . 5
⊢ (𝑁 ∈ N →
((1P +P
1P) +P ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩) = (1P
+P (1P
+P ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩))) |
10 | | addcomprg 7576 |
. . . . . . 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 414 |
. . . . . 6
⊢ (𝑁 ∈ N →
(1P +P ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩) = (⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P)) |
12 | 11 | oveq2d 5890 |
. . . . 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 2210 |
. . . 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 4029 |
. . 3
⊢ (𝑁 ∈ N →
(1P +P
1P)<P
(1P +P (⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P))) |
15 | | addclpr 7535 |
. . . . 5
⊢
((⟨{𝑙 ∣
𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ ∈ P ∧
1P ∈ P) → (⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P) ∈ P) |
16 | 4, 1, 15 | sylancl 413 |
. . . 4
⊢ (𝑁 ∈ N →
(⟨{𝑙 ∣ 𝑙 <Q
[⟨𝑁,
1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P) ∈ P) |
17 | | ltsrprg 7745 |
. . . . 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 436 |
. . . 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 413 |
. . 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 167 |
. 2
⊢ (𝑁 ∈ N →
[⟨1P, 1P⟩]
~R <R [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R ) |
21 | | df-0 7817 |
. . . 4
⊢ 0 =
⟨0R,
0R⟩ |
22 | 21 | breq1i 4010 |
. . 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 7837 |
. . 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 7729 |
. . . 4
⊢
0R = [⟨1P,
1P⟩] ~R |
25 | 24 | breq1i 4010 |
. . 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 206 |
. 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 134 |
1
⊢ (𝑁 ∈ N → 0
<ℝ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R ,
0R⟩) |