| Step | Hyp | Ref
| Expression |
| 1 | | ltrelsr 11108 |
. . . . 5
⊢
<R ⊆ (R ×
R) |
| 2 | 1 | brel 5750 |
. . . 4
⊢ ((𝐶 +R
-1R) <R 𝐴 → ((𝐶 +R
-1R) ∈ R ∧ 𝐴 ∈ R)) |
| 3 | 2 | simprd 495 |
. . 3
⊢ ((𝐶 +R
-1R) <R 𝐴 → 𝐴 ∈ R) |
| 4 | | map2psrpr.2 |
. . . . . 6
⊢ 𝐶 ∈
R |
| 5 | | ltasr 11140 |
. . . . . 6
⊢ (𝐶 ∈ R →
(-1R <R ((𝐶
·R -1R)
+R 𝐴) ↔ (𝐶 +R
-1R) <R (𝐶 +R ((𝐶
·R -1R)
+R 𝐴)))) |
| 6 | 4, 5 | ax-mp 5 |
. . . . 5
⊢
(-1R <R ((𝐶
·R -1R)
+R 𝐴) ↔ (𝐶 +R
-1R) <R (𝐶 +R ((𝐶
·R -1R)
+R 𝐴))) |
| 7 | | pn0sr 11141 |
. . . . . . . . . 10
⊢ (𝐶 ∈ R →
(𝐶
+R (𝐶 ·R
-1R)) = 0R) |
| 8 | 4, 7 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝐶 +R
(𝐶
·R -1R)) =
0R |
| 9 | 8 | oveq1i 7441 |
. . . . . . . 8
⊢ ((𝐶 +R
(𝐶
·R -1R))
+R 𝐴) = (0R
+R 𝐴) |
| 10 | | addasssr 11128 |
. . . . . . . 8
⊢ ((𝐶 +R
(𝐶
·R -1R))
+R 𝐴) = (𝐶 +R ((𝐶
·R -1R)
+R 𝐴)) |
| 11 | | addcomsr 11127 |
. . . . . . . 8
⊢
(0R +R 𝐴) = (𝐴 +R
0R) |
| 12 | 9, 10, 11 | 3eqtr3i 2773 |
. . . . . . 7
⊢ (𝐶 +R
((𝐶
·R -1R)
+R 𝐴)) = (𝐴 +R
0R) |
| 13 | | 0idsr 11137 |
. . . . . . 7
⊢ (𝐴 ∈ R →
(𝐴
+R 0R) = 𝐴) |
| 14 | 12, 13 | eqtrid 2789 |
. . . . . 6
⊢ (𝐴 ∈ R →
(𝐶
+R ((𝐶 ·R
-1R) +R 𝐴)) = 𝐴) |
| 15 | 14 | breq2d 5155 |
. . . . 5
⊢ (𝐴 ∈ R →
((𝐶
+R -1R)
<R (𝐶 +R ((𝐶
·R -1R)
+R 𝐴)) ↔ (𝐶 +R
-1R) <R 𝐴)) |
| 16 | 6, 15 | bitrid 283 |
. . . 4
⊢ (𝐴 ∈ R →
(-1R <R ((𝐶
·R -1R)
+R 𝐴) ↔ (𝐶 +R
-1R) <R 𝐴)) |
| 17 | | m1r 11122 |
. . . . . . . 8
⊢
-1R ∈ R |
| 18 | | mulclsr 11124 |
. . . . . . . 8
⊢ ((𝐶 ∈ R ∧
-1R ∈ R) → (𝐶 ·R
-1R) ∈ R) |
| 19 | 4, 17, 18 | mp2an 692 |
. . . . . . 7
⊢ (𝐶
·R -1R) ∈
R |
| 20 | | addclsr 11123 |
. . . . . . 7
⊢ (((𝐶
·R -1R) ∈
R ∧ 𝐴
∈ R) → ((𝐶 ·R
-1R) +R 𝐴) ∈ R) |
| 21 | 19, 20 | mpan 690 |
. . . . . 6
⊢ (𝐴 ∈ R →
((𝐶
·R -1R)
+R 𝐴) ∈ R) |
| 22 | | df-nr 11096 |
. . . . . . 7
⊢
R = ((P × P) /
~R ) |
| 23 | | breq2 5147 |
. . . . . . . 8
⊢
([〈𝑦, 𝑧〉]
~R = ((𝐶 ·R
-1R) +R 𝐴) → (-1R
<R [〈𝑦, 𝑧〉] ~R ↔
-1R <R ((𝐶 ·R
-1R) +R 𝐴))) |
| 24 | | eqeq2 2749 |
. . . . . . . . 9
⊢
([〈𝑦, 𝑧〉]
~R = ((𝐶 ·R
-1R) +R 𝐴) → ([〈𝑥, 1P〉]
~R = [〈𝑦, 𝑧〉] ~R ↔
[〈𝑥,
1P〉] ~R = ((𝐶
·R -1R)
+R 𝐴))) |
| 25 | 24 | rexbidv 3179 |
. . . . . . . 8
⊢
([〈𝑦, 𝑧〉]
~R = ((𝐶 ·R
-1R) +R 𝐴) → (∃𝑥 ∈ P [〈𝑥,
1P〉] ~R = [〈𝑦, 𝑧〉] ~R ↔
∃𝑥 ∈
P [〈𝑥,
1P〉] ~R = ((𝐶
·R -1R)
+R 𝐴))) |
| 26 | 23, 25 | imbi12d 344 |
. . . . . . 7
⊢
([〈𝑦, 𝑧〉]
~R = ((𝐶 ·R
-1R) +R 𝐴) → ((-1R
<R [〈𝑦, 𝑧〉] ~R →
∃𝑥 ∈
P [〈𝑥,
1P〉] ~R = [〈𝑦, 𝑧〉] ~R ) ↔
(-1R <R ((𝐶
·R -1R)
+R 𝐴) → ∃𝑥 ∈ P [〈𝑥,
1P〉] ~R = ((𝐶
·R -1R)
+R 𝐴)))) |
| 27 | | df-m1r 11102 |
. . . . . . . . . . 11
⊢
-1R = [〈1P,
(1P +P
1P)〉]
~R |
| 28 | 27 | breq1i 5150 |
. . . . . . . . . 10
⊢
(-1R <R
[〈𝑦, 𝑧〉]
~R ↔ [〈1P,
(1P +P
1P)〉] ~R
<R [〈𝑦, 𝑧〉] ~R
) |
| 29 | | addasspr 11062 |
. . . . . . . . . . . 12
⊢
((1P +P
1P) +P 𝑦) = (1P
+P (1P
+P 𝑦)) |
| 30 | 29 | breq2i 5151 |
. . . . . . . . . . 11
⊢
((1P +P 𝑧)<P
((1P +P
1P) +P 𝑦) ↔ (1P
+P 𝑧)<P
(1P +P
(1P +P 𝑦))) |
| 31 | | ltsrpr 11117 |
. . . . . . . . . . 11
⊢
([〈1P, (1P
+P 1P)〉]
~R <R [〈𝑦, 𝑧〉] ~R ↔
(1P +P 𝑧)<P
((1P +P
1P) +P 𝑦)) |
| 32 | | 1pr 11055 |
. . . . . . . . . . . 12
⊢
1P ∈ P |
| 33 | | ltapr 11085 |
. . . . . . . . . . . 12
⊢
(1P ∈ P → (𝑧<P
(1P +P 𝑦) ↔ (1P
+P 𝑧)<P
(1P +P
(1P +P 𝑦)))) |
| 34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑧<P
(1P +P 𝑦) ↔ (1P
+P 𝑧)<P
(1P +P
(1P +P 𝑦))) |
| 35 | 30, 31, 34 | 3bitr4i 303 |
. . . . . . . . . 10
⊢
([〈1P, (1P
+P 1P)〉]
~R <R [〈𝑦, 𝑧〉] ~R ↔
𝑧<P
(1P +P 𝑦)) |
| 36 | 28, 35 | bitri 275 |
. . . . . . . . 9
⊢
(-1R <R
[〈𝑦, 𝑧〉]
~R ↔ 𝑧<P
(1P +P 𝑦)) |
| 37 | | ltexpri 11083 |
. . . . . . . . 9
⊢ (𝑧<P
(1P +P 𝑦) → ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P
+P 𝑦)) |
| 38 | 36, 37 | sylbi 217 |
. . . . . . . 8
⊢
(-1R <R
[〈𝑦, 𝑧〉]
~R → ∃𝑥 ∈ P (𝑧 +P 𝑥) = (1P
+P 𝑦)) |
| 39 | | enreceq 11106 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ P ∧
1P ∈ P) ∧ (𝑦 ∈ P ∧ 𝑧 ∈ P)) →
([〈𝑥,
1P〉] ~R = [〈𝑦, 𝑧〉] ~R ↔
(𝑥
+P 𝑧) = (1P
+P 𝑦))) |
| 40 | 32, 39 | mpanl2 701 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ P ∧
(𝑦 ∈ P
∧ 𝑧 ∈
P)) → ([〈𝑥, 1P〉]
~R = [〈𝑦, 𝑧〉] ~R ↔
(𝑥
+P 𝑧) = (1P
+P 𝑦))) |
| 41 | | addcompr 11061 |
. . . . . . . . . . . 12
⊢ (𝑧 +P
𝑥) = (𝑥 +P 𝑧) |
| 42 | 41 | eqeq1i 2742 |
. . . . . . . . . . 11
⊢ ((𝑧 +P
𝑥) =
(1P +P 𝑦) ↔ (𝑥 +P 𝑧) = (1P
+P 𝑦)) |
| 43 | 40, 42 | bitr4di 289 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ P ∧
(𝑦 ∈ P
∧ 𝑧 ∈
P)) → ([〈𝑥, 1P〉]
~R = [〈𝑦, 𝑧〉] ~R ↔
(𝑧
+P 𝑥) = (1P
+P 𝑦))) |
| 44 | 43 | ancoms 458 |
. . . . . . . . 9
⊢ (((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑥 ∈
P) → ([〈𝑥, 1P〉]
~R = [〈𝑦, 𝑧〉] ~R ↔
(𝑧
+P 𝑥) = (1P
+P 𝑦))) |
| 45 | 44 | rexbidva 3177 |
. . . . . . . 8
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (∃𝑥 ∈
P [〈𝑥,
1P〉] ~R = [〈𝑦, 𝑧〉] ~R ↔
∃𝑥 ∈
P (𝑧
+P 𝑥) = (1P
+P 𝑦))) |
| 46 | 38, 45 | imbitrrid 246 |
. . . . . . 7
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (-1R <R
[〈𝑦, 𝑧〉]
~R → ∃𝑥 ∈ P [〈𝑥,
1P〉] ~R = [〈𝑦, 𝑧〉] ~R
)) |
| 47 | 22, 26, 46 | ecoptocl 8847 |
. . . . . 6
⊢ (((𝐶
·R -1R)
+R 𝐴) ∈ R →
(-1R <R ((𝐶
·R -1R)
+R 𝐴) → ∃𝑥 ∈ P [〈𝑥,
1P〉] ~R = ((𝐶
·R -1R)
+R 𝐴))) |
| 48 | 21, 47 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ R →
(-1R <R ((𝐶
·R -1R)
+R 𝐴) → ∃𝑥 ∈ P [〈𝑥,
1P〉] ~R = ((𝐶
·R -1R)
+R 𝐴))) |
| 49 | | oveq2 7439 |
. . . . . . . 8
⊢
([〈𝑥,
1P〉] ~R = ((𝐶
·R -1R)
+R 𝐴) → (𝐶 +R [〈𝑥,
1P〉] ~R ) = (𝐶 +R
((𝐶
·R -1R)
+R 𝐴))) |
| 50 | 49, 14 | sylan9eqr 2799 |
. . . . . . 7
⊢ ((𝐴 ∈ R ∧
[〈𝑥,
1P〉] ~R = ((𝐶
·R -1R)
+R 𝐴)) → (𝐶 +R [〈𝑥,
1P〉] ~R ) = 𝐴) |
| 51 | 50 | ex 412 |
. . . . . 6
⊢ (𝐴 ∈ R →
([〈𝑥,
1P〉] ~R = ((𝐶
·R -1R)
+R 𝐴) → (𝐶 +R [〈𝑥,
1P〉] ~R ) = 𝐴)) |
| 52 | 51 | reximdv 3170 |
. . . . 5
⊢ (𝐴 ∈ R →
(∃𝑥 ∈
P [〈𝑥,
1P〉] ~R = ((𝐶
·R -1R)
+R 𝐴) → ∃𝑥 ∈ P (𝐶 +R [〈𝑥,
1P〉] ~R ) = 𝐴)) |
| 53 | 48, 52 | syld 47 |
. . . 4
⊢ (𝐴 ∈ R →
(-1R <R ((𝐶
·R -1R)
+R 𝐴) → ∃𝑥 ∈ P (𝐶 +R [〈𝑥,
1P〉] ~R ) = 𝐴)) |
| 54 | 16, 53 | sylbird 260 |
. . 3
⊢ (𝐴 ∈ R →
((𝐶
+R -1R)
<R 𝐴 → ∃𝑥 ∈ P (𝐶 +R [〈𝑥,
1P〉] ~R ) = 𝐴)) |
| 55 | 3, 54 | mpcom 38 |
. 2
⊢ ((𝐶 +R
-1R) <R 𝐴 → ∃𝑥 ∈ P (𝐶 +R [〈𝑥,
1P〉] ~R ) = 𝐴) |
| 56 | 4 | mappsrpr 11148 |
. . . . 5
⊢ ((𝐶 +R
-1R) <R (𝐶 +R [〈𝑥,
1P〉] ~R ) ↔ 𝑥 ∈
P) |
| 57 | | breq2 5147 |
. . . . 5
⊢ ((𝐶 +R
[〈𝑥,
1P〉] ~R ) = 𝐴 → ((𝐶 +R
-1R) <R (𝐶 +R [〈𝑥,
1P〉] ~R ) ↔ (𝐶 +R
-1R) <R 𝐴)) |
| 58 | 56, 57 | bitr3id 285 |
. . . 4
⊢ ((𝐶 +R
[〈𝑥,
1P〉] ~R ) = 𝐴 → (𝑥 ∈ P ↔ (𝐶 +R
-1R) <R 𝐴)) |
| 59 | 58 | biimpac 478 |
. . 3
⊢ ((𝑥 ∈ P ∧
(𝐶
+R [〈𝑥, 1P〉]
~R ) = 𝐴) → (𝐶 +R
-1R) <R 𝐴) |
| 60 | 59 | rexlimiva 3147 |
. 2
⊢
(∃𝑥 ∈
P (𝐶
+R [〈𝑥, 1P〉]
~R ) = 𝐴 → (𝐶 +R
-1R) <R 𝐴) |
| 61 | 55, 60 | impbii 209 |
1
⊢ ((𝐶 +R
-1R) <R 𝐴 ↔ ∃𝑥 ∈ P (𝐶 +R [〈𝑥,
1P〉] ~R ) = 𝐴) |