Step | Hyp | Ref
| Expression |
1 | | df-nr 7689 |
. . 3
⊢
R = ((P × P) /
~R ) |
2 | | breq2 3993 |
. . . 4
⊢
([〈𝑎, 𝑏〉]
~R = 𝐴 → (0R
<R [〈𝑎, 𝑏〉] ~R ↔
0R <R 𝐴)) |
3 | | eqeq2 2180 |
. . . . 5
⊢
([〈𝑎, 𝑏〉]
~R = 𝐴 → ([〈(𝑥 +P
1P), 1P〉]
~R = [〈𝑎, 𝑏〉] ~R ↔
[〈(𝑥
+P 1P),
1P〉] ~R = 𝐴)) |
4 | 3 | reubidv 2653 |
. . . 4
⊢
([〈𝑎, 𝑏〉]
~R = 𝐴 → (∃!𝑥 ∈ P [〈(𝑥 +P
1P), 1P〉]
~R = [〈𝑎, 𝑏〉] ~R ↔
∃!𝑥 ∈
P [〈(𝑥
+P 1P),
1P〉] ~R = 𝐴)) |
5 | 2, 4 | imbi12d 233 |
. . 3
⊢
([〈𝑎, 𝑏〉]
~R = 𝐴 → ((0R
<R [〈𝑎, 𝑏〉] ~R →
∃!𝑥 ∈
P [〈(𝑥
+P 1P),
1P〉] ~R = [〈𝑎, 𝑏〉] ~R ) ↔
(0R <R 𝐴 → ∃!𝑥 ∈ P [〈(𝑥 +P
1P), 1P〉]
~R = 𝐴))) |
6 | | gt0srpr 7710 |
. . . . . . . 8
⊢
(0R <R [〈𝑎, 𝑏〉] ~R ↔
𝑏<P 𝑎) |
7 | 6 | biimpi 119 |
. . . . . . 7
⊢
(0R <R [〈𝑎, 𝑏〉] ~R →
𝑏<P 𝑎) |
8 | 7 | adantl 275 |
. . . . . 6
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) →
𝑏<P 𝑎) |
9 | | lteupri 7579 |
. . . . . 6
⊢ (𝑏<P
𝑎 → ∃!𝑥 ∈ P (𝑏 +P
𝑥) = 𝑎) |
10 | 8, 9 | syl 14 |
. . . . 5
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) →
∃!𝑥 ∈
P (𝑏
+P 𝑥) = 𝑎) |
11 | | simpr 109 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ 𝑥 ∈
P) |
12 | | 1pr 7516 |
. . . . . . . . . 10
⊢
1P ∈ P |
13 | 12 | a1i 9 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ 1P ∈ P) |
14 | | addclpr 7499 |
. . . . . . . . 9
⊢ ((𝑥 ∈ P ∧
1P ∈ P) → (𝑥 +P
1P) ∈ P) |
15 | 11, 13, 14 | syl2anc 409 |
. . . . . . . 8
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ (𝑥
+P 1P) ∈
P) |
16 | | simplll 528 |
. . . . . . . 8
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ 𝑎 ∈
P) |
17 | | simpllr 529 |
. . . . . . . 8
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ 𝑏 ∈
P) |
18 | | enreceq 7698 |
. . . . . . . 8
⊢ ((((𝑥 +P
1P) ∈ P ∧
1P ∈ P) ∧ (𝑎 ∈ P ∧ 𝑏 ∈ P)) →
([〈(𝑥
+P 1P),
1P〉] ~R = [〈𝑎, 𝑏〉] ~R ↔
((𝑥
+P 1P)
+P 𝑏) = (1P
+P 𝑎))) |
19 | 15, 13, 16, 17, 18 | syl22anc 1234 |
. . . . . . 7
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ ([〈(𝑥
+P 1P),
1P〉] ~R = [〈𝑎, 𝑏〉] ~R ↔
((𝑥
+P 1P)
+P 𝑏) = (1P
+P 𝑎))) |
20 | | addcomprg 7540 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ P ∧
1P ∈ P) → (𝑥 +P
1P) = (1P
+P 𝑥)) |
21 | 11, 13, 20 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ (𝑥
+P 1P) =
(1P +P 𝑥)) |
22 | 21 | oveq1d 5868 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ ((𝑥
+P 1P)
+P 𝑏) = ((1P
+P 𝑥) +P 𝑏)) |
23 | | addassprg 7541 |
. . . . . . . . . . 11
⊢
((1P ∈ P ∧ 𝑥 ∈ P ∧
𝑏 ∈ P)
→ ((1P +P 𝑥) +P
𝑏) =
(1P +P (𝑥 +P 𝑏))) |
24 | 13, 11, 17, 23 | syl3anc 1233 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ ((1P +P 𝑥) +P
𝑏) =
(1P +P (𝑥 +P 𝑏))) |
25 | 22, 24 | eqtrd 2203 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ ((𝑥
+P 1P)
+P 𝑏) = (1P
+P (𝑥 +P 𝑏))) |
26 | 25 | eqeq1d 2179 |
. . . . . . . 8
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ (((𝑥
+P 1P)
+P 𝑏) = (1P
+P 𝑎) ↔ (1P
+P (𝑥 +P 𝑏)) =
(1P +P 𝑎))) |
27 | | addclpr 7499 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ P ∧
𝑏 ∈ P)
→ (𝑥
+P 𝑏) ∈ P) |
28 | 11, 17, 27 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ (𝑥
+P 𝑏) ∈ P) |
29 | | addcanprg 7578 |
. . . . . . . . . 10
⊢
((1P ∈ P ∧ (𝑥 +P
𝑏) ∈ P
∧ 𝑎 ∈
P) → ((1P
+P (𝑥 +P 𝑏)) =
(1P +P 𝑎) → (𝑥 +P 𝑏) = 𝑎)) |
30 | 13, 28, 16, 29 | syl3anc 1233 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ ((1P +P (𝑥 +P
𝑏)) =
(1P +P 𝑎) → (𝑥 +P 𝑏) = 𝑎)) |
31 | | oveq2 5861 |
. . . . . . . . 9
⊢ ((𝑥 +P
𝑏) = 𝑎 → (1P
+P (𝑥 +P 𝑏)) =
(1P +P 𝑎)) |
32 | 30, 31 | impbid1 141 |
. . . . . . . 8
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ ((1P +P (𝑥 +P
𝑏)) =
(1P +P 𝑎) ↔ (𝑥 +P 𝑏) = 𝑎)) |
33 | 26, 32 | bitrd 187 |
. . . . . . 7
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ (((𝑥
+P 1P)
+P 𝑏) = (1P
+P 𝑎) ↔ (𝑥 +P 𝑏) = 𝑎)) |
34 | | addcomprg 7540 |
. . . . . . . . 9
⊢ ((𝑥 ∈ P ∧
𝑏 ∈ P)
→ (𝑥
+P 𝑏) = (𝑏 +P 𝑥)) |
35 | 11, 17, 34 | syl2anc 409 |
. . . . . . . 8
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ (𝑥
+P 𝑏) = (𝑏 +P 𝑥)) |
36 | 35 | eqeq1d 2179 |
. . . . . . 7
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ ((𝑥
+P 𝑏) = 𝑎 ↔ (𝑏 +P 𝑥) = 𝑎)) |
37 | 19, 33, 36 | 3bitrrd 214 |
. . . . . 6
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) ∧
𝑥 ∈ P)
→ ((𝑏
+P 𝑥) = 𝑎 ↔ [〈(𝑥 +P
1P), 1P〉]
~R = [〈𝑎, 𝑏〉] ~R
)) |
38 | 37 | reubidva 2652 |
. . . . 5
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) →
(∃!𝑥 ∈
P (𝑏
+P 𝑥) = 𝑎 ↔ ∃!𝑥 ∈ P [〈(𝑥 +P
1P), 1P〉]
~R = [〈𝑎, 𝑏〉] ~R
)) |
39 | 10, 38 | mpbid 146 |
. . . 4
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ 0R <R [〈𝑎, 𝑏〉] ~R ) →
∃!𝑥 ∈
P [〈(𝑥
+P 1P),
1P〉] ~R = [〈𝑎, 𝑏〉] ~R
) |
40 | 39 | ex 114 |
. . 3
⊢ ((𝑎 ∈ P ∧
𝑏 ∈ P)
→ (0R <R [〈𝑎, 𝑏〉] ~R →
∃!𝑥 ∈
P [〈(𝑥
+P 1P),
1P〉] ~R = [〈𝑎, 𝑏〉] ~R
)) |
41 | 1, 5, 40 | ecoptocl 6600 |
. 2
⊢ (𝐴 ∈ R →
(0R <R 𝐴 → ∃!𝑥 ∈ P [〈(𝑥 +P
1P), 1P〉]
~R = 𝐴)) |
42 | 41 | imp 123 |
1
⊢ ((𝐴 ∈ R ∧
0R <R 𝐴) → ∃!𝑥 ∈ P [〈(𝑥 +P
1P), 1P〉]
~R = 𝐴) |