Step | Hyp | Ref
| Expression |
1 | | ltrelsr 6666 |
. . . 4
⊢
<R ⊆ (R ×
R) |
2 | 1 | brel 4335 |
. . 3
⊢
(0R <R A → (0R ∈ R ∧ A ∈ R)) |
3 | 2 | simprd 107 |
. 2
⊢
(0R <R A → A ∈ R) |
4 | | df-nr 6655 |
. . 3
⊢
R = ((P × P) /
~R ) |
5 | | breq2 3759 |
. . . 4
⊢
([〈y, z〉] ~R = A → (0R
<R [〈y,
z〉] ~R ↔
0R <R A)) |
6 | | oveq1 5462 |
. . . . . . 7
⊢
([〈y, z〉] ~R = A → ([〈y, z〉]
~R ·R x) = (A
·R x)) |
7 | 6 | eqeq1d 2045 |
. . . . . 6
⊢
([〈y, z〉] ~R = A → (([〈y, z〉]
~R ·R x) = 1R ↔ (A ·R x) = 1R)) |
8 | 7 | anbi2d 437 |
. . . . 5
⊢
([〈y, z〉] ~R = A → ((0R
<R x ∧ ([〈y,
z〉] ~R
·R x) =
1R) ↔ (0R
<R x ∧ (A
·R x) =
1R))) |
9 | 8 | rexbidv 2321 |
. . . 4
⊢
([〈y, z〉] ~R = A → (∃x ∈ R (0R
<R x ∧ ([〈y,
z〉] ~R
·R x) =
1R) ↔ ∃x ∈ R (0R
<R x ∧ (A
·R x) =
1R))) |
10 | 5, 9 | imbi12d 223 |
. . 3
⊢
([〈y, z〉] ~R = A → ((0R
<R [〈y,
z〉] ~R →
∃x ∈ R (0R
<R x ∧ ([〈y,
z〉] ~R
·R x) =
1R)) ↔ (0R
<R A →
∃x ∈ R (0R
<R x ∧ (A
·R x) =
1R)))) |
11 | | gt0srpr 6676 |
. . . . 5
⊢
(0R <R
[〈y, z〉] ~R ↔ z<P y) |
12 | | ltexpri 6587 |
. . . . 5
⊢ (z<P y → ∃w ∈ P (z +P w) = y) |
13 | 11, 12 | sylbi 114 |
. . . 4
⊢
(0R <R
[〈y, z〉] ~R → ∃w ∈ P (z +P w) = y) |
14 | | recexpr 6610 |
. . . . . . 7
⊢ (w ∈
P → ∃v ∈
P (w
·P v) =
1P) |
15 | 14 | adantl 262 |
. . . . . 6
⊢
(((y ∈ P ∧ z ∈ P) ∧ w ∈ P) → ∃v ∈ P (w ·P v) = 1P) |
16 | | 1pr 6535 |
. . . . . . . . . . . . . 14
⊢
1P ∈
P |
17 | | addclpr 6520 |
. . . . . . . . . . . . . 14
⊢
((v ∈ P ∧ 1P ∈ P) → (v +P
1P) ∈
P) |
18 | 16, 17 | mpan2 401 |
. . . . . . . . . . . . 13
⊢ (v ∈
P → (v
+P 1P) ∈ P) |
19 | | enrex 6665 |
. . . . . . . . . . . . . 14
⊢
~R ∈
V |
20 | 19, 4 | ecopqsi 6097 |
. . . . . . . . . . . . 13
⊢
(((v +P
1P) ∈
P ∧ 1P
∈ P) → [〈(v +P
1P), 1P〉]
~R ∈
R) |
21 | 18, 16, 20 | sylancl 392 |
. . . . . . . . . . . 12
⊢ (v ∈
P → [〈(v
+P 1P),
1P〉] ~R ∈ R) |
22 | 21 | adantl 262 |
. . . . . . . . . . 11
⊢
((w ∈ P ∧ v ∈ P) → [〈(v +P
1P), 1P〉]
~R ∈
R) |
23 | 22 | ad2antlr 458 |
. . . . . . . . . 10
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
[〈(v +P
1P), 1P〉]
~R ∈
R) |
24 | | simprr 484 |
. . . . . . . . . . . 12
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → v ∈
P) |
25 | 24 | adantr 261 |
. . . . . . . . . . 11
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
v ∈
P) |
26 | | ltaddpr 6571 |
. . . . . . . . . . . . . 14
⊢
((1P ∈
P ∧ v ∈
P) →
1P<P
(1P +P v)) |
27 | 16, 26 | mpan 400 |
. . . . . . . . . . . . 13
⊢ (v ∈
P →
1P<P
(1P +P v)) |
28 | | addcomprg 6554 |
. . . . . . . . . . . . . 14
⊢
((1P ∈
P ∧ v ∈
P) → (1P
+P v) = (v +P
1P)) |
29 | 16, 28 | mpan 400 |
. . . . . . . . . . . . 13
⊢ (v ∈
P → (1P +P
v) = (v
+P 1P)) |
30 | 27, 29 | breqtrd 3779 |
. . . . . . . . . . . 12
⊢ (v ∈
P →
1P<P (v +P
1P)) |
31 | | gt0srpr 6676 |
. . . . . . . . . . . 12
⊢
(0R <R
[〈(v +P
1P), 1P〉]
~R ↔
1P<P (v +P
1P)) |
32 | 30, 31 | sylibr 137 |
. . . . . . . . . . 11
⊢ (v ∈
P → 0R
<R [〈(v
+P 1P),
1P〉] ~R
) |
33 | 25, 32 | syl 14 |
. . . . . . . . . 10
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
0R <R [〈(v +P
1P), 1P〉]
~R ) |
34 | 18, 16 | jctir 296 |
. . . . . . . . . . . . . . . 16
⊢ (v ∈
P → ((v
+P 1P) ∈ P ∧ 1P ∈ P)) |
35 | 34 | anim2i 324 |
. . . . . . . . . . . . . . 15
⊢
(((y ∈ P ∧ z ∈ P) ∧ v ∈ P) → ((y ∈
P ∧ z ∈
P) ∧ ((v +P
1P) ∈
P ∧ 1P
∈ P))) |
36 | 35 | adantr 261 |
. . . . . . . . . . . . . 14
⊢
((((y ∈ P ∧ z ∈ P) ∧ v ∈ P) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
((y ∈
P ∧ z ∈
P) ∧ ((v +P
1P) ∈
P ∧ 1P
∈ P))) |
37 | | mulsrpr 6674 |
. . . . . . . . . . . . . 14
⊢
(((y ∈ P ∧ z ∈ P) ∧ ((v
+P 1P) ∈ P ∧ 1P ∈ P)) → ([〈y, z〉]
~R ·R [〈(v +P
1P), 1P〉]
~R ) = [〈((y
·P (v
+P 1P))
+P (z
·P 1P)), ((y ·P
1P) +P (z ·P (v +P
1P)))〉] ~R
) |
38 | 36, 37 | syl 14 |
. . . . . . . . . . . . 13
⊢
((((y ∈ P ∧ z ∈ P) ∧ v ∈ P) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
([〈y, z〉] ~R
·R [〈(v +P
1P), 1P〉]
~R ) = [〈((y
·P (v
+P 1P))
+P (z
·P 1P)), ((y ·P
1P) +P (z ·P (v +P
1P)))〉] ~R
) |
39 | 38 | adantlrl 451 |
. . . . . . . . . . . 12
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
([〈y, z〉] ~R
·R [〈(v +P
1P), 1P〉]
~R ) = [〈((y
·P (v
+P 1P))
+P (z
·P 1P)), ((y ·P
1P) +P (z ·P (v +P
1P)))〉] ~R
) |
40 | | oveq1 5462 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((z +P
w) = y
→ ((z +P
w) ·P
v) = (y
·P v)) |
41 | 40 | eqcomd 2042 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((z +P
w) = y
→ (y
·P v) =
((z +P w) ·P v)) |
42 | 41 | ad2antll 460 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
(y ·P
v) = ((z +P w) ·P v)) |
43 | | mulcomprg 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((f ∈ P ∧ ℎ
∈ P) → (f ·P ℎ) = (ℎ ·P f)) |
44 | 43 | 3adant2 922 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((f ∈ P ∧ g ∈ P ∧ ℎ
∈ P) → (f ·P ℎ) = (ℎ ·P f)) |
45 | | mulcomprg 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((g ∈ P ∧ ℎ
∈ P) → (g ·P ℎ) = (ℎ ·P g)) |
46 | 45 | 3adant1 921 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((f ∈ P ∧ g ∈ P ∧ ℎ
∈ P) → (g ·P ℎ) = (ℎ ·P g)) |
47 | 44, 46 | oveq12d 5473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((f ∈ P ∧ g ∈ P ∧ ℎ
∈ P) → ((f ·P ℎ) +P (g ·P ℎ)) = ((ℎ ·P f) +P (ℎ ·P g))) |
48 | | distrprg 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ ∈
P ∧ f ∈
P ∧ g ∈
P) → (ℎ
·P (f
+P g)) = ((ℎ ·P
f) +P (ℎ ·P
g))) |
49 | 48 | 3coml 1110 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((f ∈ P ∧ g ∈ P ∧ ℎ
∈ P) → (ℎ ·P (f +P g)) = ((ℎ ·P f) +P (ℎ ·P g))) |
50 | | simp3 905 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((f ∈ P ∧ g ∈ P ∧ ℎ
∈ P) → ℎ ∈
P) |
51 | | addclpr 6520 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((f ∈ P ∧ g ∈ P) → (f +P g) ∈
P) |
52 | 51 | 3adant3 923 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((f ∈ P ∧ g ∈ P ∧ ℎ
∈ P) → (f +P g) ∈
P) |
53 | | mulcomprg 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ ∈
P ∧ (f +P g) ∈
P) → (ℎ
·P (f
+P g)) =
((f +P g) ·P ℎ)) |
54 | 50, 52, 53 | syl2anc 391 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((f ∈ P ∧ g ∈ P ∧ ℎ
∈ P) → (ℎ ·P (f +P g)) = ((f
+P g)
·P ℎ)) |
55 | 47, 49, 54 | 3eqtr2rd 2076 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((f ∈ P ∧ g ∈ P ∧ ℎ
∈ P) → ((f +P g) ·P ℎ) = ((f ·P ℎ) +P (g ·P ℎ))) |
56 | 55 | adantl 262 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ (f ∈ P ∧ g ∈ P ∧ ℎ
∈ P)) → ((f +P g) ·P ℎ) = ((f ·P ℎ) +P (g ·P ℎ))) |
57 | | simplr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → z ∈
P) |
58 | | simprl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → w ∈
P) |
59 | 56, 57, 58, 24 | caovdird 5621 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((z +P w) ·P v) = ((z
·P v)
+P (w
·P v))) |
60 | | oveq2 5463 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((w
·P v) =
1P → ((z
·P v)
+P (w
·P v)) =
((z ·P
v) +P
1P)) |
61 | 59, 60 | sylan9eq 2089 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ (w
·P v) =
1P) → ((z
+P w)
·P v) =
((z ·P
v) +P
1P)) |
62 | 61 | adantrr 448 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
((z +P w) ·P v) = ((z
·P v)
+P 1P)) |
63 | 42, 62 | eqtrd 2069 |
. . . . . . . . . . . . . . . . . 18
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
(y ·P
v) = ((z ·P v) +P
1P)) |
64 | 63 | oveq1d 5470 |
. . . . . . . . . . . . . . . . 17
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
((y ·P
v) +P ((y ·P
1P) +P (z ·P
1P))) = (((z
·P v)
+P 1P)
+P ((y
·P 1P)
+P (z
·P
1P)))) |
65 | | mulclpr 6553 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((z ∈ P ∧ v ∈ P) → (z ·P v) ∈
P) |
66 | 57, 24, 65 | syl2anc 391 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (z ·P v) ∈
P) |
67 | 16 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) →
1P ∈
P) |
68 | | simpll 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → y ∈
P) |
69 | | mulclpr 6553 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((y ∈ P ∧ 1P ∈ P) → (y ·P
1P) ∈
P) |
70 | 68, 16, 69 | sylancl 392 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (y ·P
1P) ∈
P) |
71 | | mulclpr 6553 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((z ∈ P ∧ 1P ∈ P) → (z ·P
1P) ∈
P) |
72 | 57, 16, 71 | sylancl 392 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (z ·P
1P) ∈
P) |
73 | | addclpr 6520 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((y
·P 1P) ∈ P ∧ (z
·P 1P) ∈ P) → ((y ·P
1P) +P (z ·P
1P)) ∈
P) |
74 | 70, 72, 73 | syl2anc 391 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·P
1P) +P (z ·P
1P)) ∈
P) |
75 | | addcomprg 6554 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((f ∈ P ∧ g ∈ P) → (f +P g) = (g
+P f)) |
76 | 75 | adantl 262 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ (f ∈ P ∧ g ∈ P)) → (f +P g) = (g
+P f)) |
77 | | addassprg 6555 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((f ∈ P ∧ g ∈ P ∧ ℎ
∈ P) → ((f +P g) +P ℎ) = (f
+P (g
+P ℎ))) |
78 | 77 | adantl 262 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ (f ∈ P ∧ g ∈ P ∧ ℎ
∈ P)) → ((f +P g) +P ℎ) = (f
+P (g
+P ℎ))) |
79 | 66, 67, 74, 76, 78 | caov32d 5623 |
. . . . . . . . . . . . . . . . . 18
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (((z ·P v) +P
1P) +P ((y ·P
1P) +P (z ·P
1P))) = (((z
·P v)
+P ((y
·P 1P)
+P (z
·P 1P)))
+P 1P)) |
80 | 79 | adantr 261 |
. . . . . . . . . . . . . . . . 17
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
(((z ·P
v) +P
1P) +P ((y ·P
1P) +P (z ·P
1P))) = (((z
·P v)
+P ((y
·P 1P)
+P (z
·P 1P)))
+P 1P)) |
81 | 64, 80 | eqtrd 2069 |
. . . . . . . . . . . . . . . 16
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
((y ·P
v) +P ((y ·P
1P) +P (z ·P
1P))) = (((z
·P v)
+P ((y
·P 1P)
+P (z
·P 1P)))
+P 1P)) |
82 | 81 | oveq1d 5470 |
. . . . . . . . . . . . . . 15
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
(((y ·P
v) +P ((y ·P
1P) +P (z ·P
1P))) +P
1P) = ((((z
·P v)
+P ((y
·P 1P)
+P (z
·P 1P)))
+P 1P)
+P 1P)) |
83 | | addclpr 6520 |
. . . . . . . . . . . . . . . . . 18
⊢
(((z
·P v) ∈ P ∧ ((y
·P 1P)
+P (z
·P 1P)) ∈ P) → ((z ·P v) +P ((y ·P
1P) +P (z ·P
1P))) ∈
P) |
84 | 66, 74, 83 | syl2anc 391 |
. . . . . . . . . . . . . . . . 17
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((z ·P v) +P ((y ·P
1P) +P (z ·P
1P))) ∈
P) |
85 | 84 | adantr 261 |
. . . . . . . . . . . . . . . 16
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
((z ·P
v) +P ((y ·P
1P) +P (z ·P
1P))) ∈
P) |
86 | 16 | a1i 9 |
. . . . . . . . . . . . . . . 16
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
1P ∈
P) |
87 | | addassprg 6555 |
. . . . . . . . . . . . . . . 16
⊢
((((z
·P v)
+P ((y
·P 1P)
+P (z
·P 1P))) ∈ P ∧ 1P ∈ P ∧ 1P ∈ P) → ((((z ·P v) +P ((y ·P
1P) +P (z ·P
1P))) +P
1P) +P
1P) = (((z
·P v)
+P ((y
·P 1P)
+P (z
·P 1P)))
+P (1P
+P 1P))) |
88 | 85, 86, 86, 87 | syl3anc 1134 |
. . . . . . . . . . . . . . 15
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
((((z ·P
v) +P ((y ·P
1P) +P (z ·P
1P))) +P
1P) +P
1P) = (((z
·P v)
+P ((y
·P 1P)
+P (z
·P 1P)))
+P (1P
+P 1P))) |
89 | 82, 88 | eqtrd 2069 |
. . . . . . . . . . . . . 14
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
(((y ·P
v) +P ((y ·P
1P) +P (z ·P
1P))) +P
1P) = (((z
·P v)
+P ((y
·P 1P)
+P (z
·P 1P)))
+P (1P
+P 1P))) |
90 | | distrprg 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢
((y ∈ P ∧ v ∈ P ∧ 1P ∈ P) → (y ·P (v +P
1P)) = ((y
·P v)
+P (y
·P
1P))) |
91 | 68, 24, 67, 90 | syl3anc 1134 |
. . . . . . . . . . . . . . . . . 18
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (y ·P (v +P
1P)) = ((y
·P v)
+P (y
·P
1P))) |
92 | 91 | oveq1d 5470 |
. . . . . . . . . . . . . . . . 17
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·P (v +P
1P)) +P (z ·P
1P)) = (((y
·P v)
+P (y
·P 1P))
+P (z
·P
1P))) |
93 | | mulclpr 6553 |
. . . . . . . . . . . . . . . . . . 19
⊢
((y ∈ P ∧ v ∈ P) → (y ·P v) ∈
P) |
94 | 68, 24, 93 | syl2anc 391 |
. . . . . . . . . . . . . . . . . 18
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (y ·P v) ∈
P) |
95 | | addassprg 6555 |
. . . . . . . . . . . . . . . . . 18
⊢
(((y
·P v) ∈ P ∧ (y
·P 1P) ∈ P ∧ (z
·P 1P) ∈ P) → (((y ·P v) +P (y ·P
1P)) +P (z ·P
1P)) = ((y
·P v)
+P ((y
·P 1P)
+P (z
·P
1P)))) |
96 | 94, 70, 72, 95 | syl3anc 1134 |
. . . . . . . . . . . . . . . . 17
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (((y ·P v) +P (y ·P
1P)) +P (z ·P
1P)) = ((y
·P v)
+P ((y
·P 1P)
+P (z
·P
1P)))) |
97 | 92, 96 | eqtrd 2069 |
. . . . . . . . . . . . . . . 16
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·P (v +P
1P)) +P (z ·P
1P)) = ((y
·P v)
+P ((y
·P 1P)
+P (z
·P
1P)))) |
98 | 97 | oveq1d 5470 |
. . . . . . . . . . . . . . 15
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (((y ·P (v +P
1P)) +P (z ·P
1P)) +P
1P) = (((y
·P v)
+P ((y
·P 1P)
+P (z
·P 1P)))
+P 1P)) |
99 | 98 | adantr 261 |
. . . . . . . . . . . . . 14
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
(((y ·P
(v +P
1P)) +P (z ·P
1P)) +P
1P) = (((y
·P v)
+P ((y
·P 1P)
+P (z
·P 1P)))
+P 1P)) |
100 | | distrprg 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢
((z ∈ P ∧ v ∈ P ∧ 1P ∈ P) → (z ·P (v +P
1P)) = ((z
·P v)
+P (z
·P
1P))) |
101 | 57, 24, 67, 100 | syl3anc 1134 |
. . . . . . . . . . . . . . . . . 18
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (z ·P (v +P
1P)) = ((z
·P v)
+P (z
·P
1P))) |
102 | 101 | oveq2d 5471 |
. . . . . . . . . . . . . . . . 17
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·P
1P) +P (z ·P (v +P
1P))) = ((y
·P 1P)
+P ((z
·P v)
+P (z
·P
1P)))) |
103 | 70, 66, 72, 76, 78 | caov12d 5624 |
. . . . . . . . . . . . . . . . 17
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·P
1P) +P ((z ·P v) +P (z ·P
1P))) = ((z
·P v)
+P ((y
·P 1P)
+P (z
·P
1P)))) |
104 | 102, 103 | eqtrd 2069 |
. . . . . . . . . . . . . . . 16
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·P
1P) +P (z ·P (v +P
1P))) = ((z
·P v)
+P ((y
·P 1P)
+P (z
·P
1P)))) |
105 | 104 | oveq1d 5470 |
. . . . . . . . . . . . . . 15
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (((y ·P
1P) +P (z ·P (v +P
1P))) +P
(1P +P
1P)) = (((z
·P v)
+P ((y
·P 1P)
+P (z
·P 1P)))
+P (1P
+P 1P))) |
106 | 105 | adantr 261 |
. . . . . . . . . . . . . 14
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
(((y ·P
1P) +P (z ·P (v +P
1P))) +P
(1P +P
1P)) = (((z
·P v)
+P ((y
·P 1P)
+P (z
·P 1P)))
+P (1P
+P 1P))) |
107 | 89, 99, 106 | 3eqtr4d 2079 |
. . . . . . . . . . . . 13
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
(((y ·P
(v +P
1P)) +P (z ·P
1P)) +P
1P) = (((y
·P 1P)
+P (z
·P (v
+P 1P)))
+P (1P
+P 1P))) |
108 | 24, 16, 17 | sylancl 392 |
. . . . . . . . . . . . . . . . 17
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (v +P
1P) ∈
P) |
109 | | mulclpr 6553 |
. . . . . . . . . . . . . . . . 17
⊢
((y ∈ P ∧ (v
+P 1P) ∈ P) → (y ·P (v +P
1P)) ∈
P) |
110 | 68, 108, 109 | syl2anc 391 |
. . . . . . . . . . . . . . . 16
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → (y ·P (v +P
1P)) ∈
P) |
111 | | addclpr 6520 |
. . . . . . . . . . . . . . . 16
⊢
(((y
·P (v
+P 1P)) ∈ P ∧ (z
·P 1P) ∈ P) → ((y ·P (v +P
1P)) +P (z ·P
1P)) ∈
P) |
112 | 110, 72, 111 | syl2anc 391 |
. . . . . . . . . . . . . . 15
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·P (v +P
1P)) +P (z ·P
1P)) ∈
P) |
113 | 104, 84 | eqeltrd 2111 |
. . . . . . . . . . . . . . 15
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((y ·P
1P) +P (z ·P (v +P
1P))) ∈
P) |
114 | | addclpr 6520 |
. . . . . . . . . . . . . . . . 17
⊢
((1P ∈
P ∧ 1P
∈ P) →
(1P +P
1P) ∈
P) |
115 | 16, 16, 114 | mp2an 402 |
. . . . . . . . . . . . . . . 16
⊢
(1P +P
1P) ∈
P |
116 | 115 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) →
(1P +P
1P) ∈
P) |
117 | | enreceq 6664 |
. . . . . . . . . . . . . . 15
⊢
(((((y
·P (v
+P 1P))
+P (z
·P 1P)) ∈ P ∧ ((y
·P 1P)
+P (z
·P (v
+P 1P))) ∈ P) ∧ ((1P
+P 1P) ∈ P ∧ 1P ∈ P)) → ([〈((y ·P (v +P
1P)) +P (z ·P
1P)), ((y
·P 1P)
+P (z
·P (v
+P 1P)))〉]
~R = [〈(1P
+P 1P),
1P〉] ~R ↔
(((y ·P
(v +P
1P)) +P (z ·P
1P)) +P
1P) = (((y
·P 1P)
+P (z
·P (v
+P 1P)))
+P (1P
+P 1P)))) |
118 | 112, 113,
116, 67, 117 | syl22anc 1135 |
. . . . . . . . . . . . . 14
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ([〈((y ·P (v +P
1P)) +P (z ·P
1P)), ((y
·P 1P)
+P (z
·P (v
+P 1P)))〉]
~R = [〈(1P
+P 1P),
1P〉] ~R ↔
(((y ·P
(v +P
1P)) +P (z ·P
1P)) +P
1P) = (((y
·P 1P)
+P (z
·P (v
+P 1P)))
+P (1P
+P 1P)))) |
119 | 118 | adantr 261 |
. . . . . . . . . . . . 13
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
([〈((y
·P (v
+P 1P))
+P (z
·P 1P)), ((y ·P
1P) +P (z ·P (v +P
1P)))〉] ~R =
[〈(1P +P
1P), 1P〉]
~R ↔ (((y
·P (v
+P 1P))
+P (z
·P 1P))
+P 1P) = (((y ·P
1P) +P (z ·P (v +P
1P))) +P
(1P +P
1P)))) |
120 | 107, 119 | mpbird 156 |
. . . . . . . . . . . 12
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
[〈((y
·P (v
+P 1P))
+P (z
·P 1P)), ((y ·P
1P) +P (z ·P (v +P
1P)))〉] ~R =
[〈(1P +P
1P), 1P〉]
~R ) |
121 | 39, 120 | eqtrd 2069 |
. . . . . . . . . . 11
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
([〈y, z〉] ~R
·R [〈(v +P
1P), 1P〉]
~R ) = [〈(1P
+P 1P),
1P〉] ~R
) |
122 | | df-1r 6660 |
. . . . . . . . . . 11
⊢
1R = [〈(1P
+P 1P),
1P〉] ~R |
123 | 121, 122 | syl6eqr 2087 |
. . . . . . . . . 10
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
([〈y, z〉] ~R
·R [〈(v +P
1P), 1P〉]
~R ) = 1R) |
124 | | breq2 3759 |
. . . . . . . . . . . 12
⊢ (x = [〈(v
+P 1P),
1P〉] ~R →
(0R <R x ↔ 0R
<R [〈(v
+P 1P),
1P〉] ~R
)) |
125 | | oveq2 5463 |
. . . . . . . . . . . . 13
⊢ (x = [〈(v
+P 1P),
1P〉] ~R →
([〈y, z〉] ~R
·R x) =
([〈y, z〉] ~R
·R [〈(v +P
1P), 1P〉]
~R )) |
126 | 125 | eqeq1d 2045 |
. . . . . . . . . . . 12
⊢ (x = [〈(v
+P 1P),
1P〉] ~R →
(([〈y, z〉] ~R
·R x) =
1R ↔ ([〈y, z〉]
~R ·R [〈(v +P
1P), 1P〉]
~R ) = 1R)) |
127 | 124, 126 | anbi12d 442 |
. . . . . . . . . . 11
⊢ (x = [〈(v
+P 1P),
1P〉] ~R →
((0R <R x ∧
([〈y, z〉] ~R
·R x) =
1R) ↔ (0R
<R [〈(v
+P 1P),
1P〉] ~R ∧ ([〈y,
z〉] ~R
·R [〈(v +P
1P), 1P〉]
~R ) = 1R))) |
128 | 127 | rspcev 2650 |
. . . . . . . . . 10
⊢
(([〈(v
+P 1P),
1P〉] ~R ∈ R ∧ (0R
<R [〈(v
+P 1P),
1P〉] ~R ∧ ([〈y,
z〉] ~R
·R [〈(v +P
1P), 1P〉]
~R ) = 1R)) → ∃x ∈ R (0R
<R x ∧ ([〈y,
z〉] ~R
·R x) =
1R)) |
129 | 23, 33, 123, 128 | syl12anc 1132 |
. . . . . . . . 9
⊢
((((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) ∧ ((w
·P v) =
1P ∧ (z +P w) = y)) →
∃x ∈ R (0R
<R x ∧ ([〈y,
z〉] ~R
·R x) =
1R)) |
130 | 129 | exp32 347 |
. . . . . . . 8
⊢
(((y ∈ P ∧ z ∈ P) ∧ (w ∈ P ∧ v ∈ P)) → ((w ·P v) = 1P → ((z +P w) = y →
∃x ∈ R (0R
<R x ∧ ([〈y,
z〉] ~R
·R x) =
1R)))) |
131 | 130 | anassrs 380 |
. . . . . . 7
⊢
((((y ∈ P ∧ z ∈ P) ∧ w ∈ P) ∧ v ∈ P) → ((w ·P v) = 1P → ((z +P w) = y →
∃x ∈ R (0R
<R x ∧ ([〈y,
z〉] ~R
·R x) =
1R)))) |
132 | 131 | rexlimdva 2427 |
. . . . . 6
⊢
(((y ∈ P ∧ z ∈ P) ∧ w ∈ P) → (∃v ∈ P (w ·P v) = 1P → ((z +P w) = y →
∃x ∈ R (0R
<R x ∧ ([〈y,
z〉] ~R
·R x) =
1R)))) |
133 | 15, 132 | mpd 13 |
. . . . 5
⊢
(((y ∈ P ∧ z ∈ P) ∧ w ∈ P) → ((z +P w) = y →
∃x ∈ R (0R
<R x ∧ ([〈y,
z〉] ~R
·R x) =
1R))) |
134 | 133 | rexlimdva 2427 |
. . . 4
⊢
((y ∈ P ∧ z ∈ P) → (∃w ∈ P (z +P w) = y →
∃x ∈ R (0R
<R x ∧ ([〈y,
z〉] ~R
·R x) =
1R))) |
135 | 13, 134 | syl5 28 |
. . 3
⊢
((y ∈ P ∧ z ∈ P) →
(0R <R [〈y, z〉]
~R → ∃x ∈
R (0R <R
x ∧
([〈y, z〉] ~R
·R x) =
1R))) |
136 | 4, 10, 135 | ecoptocl 6129 |
. 2
⊢ (A ∈
R → (0R
<R A →
∃x ∈ R (0R
<R x ∧ (A
·R x) =
1R))) |
137 | 3, 136 | mpcom 32 |
1
⊢
(0R <R A → ∃x ∈ R (0R
<R x ∧ (A
·R x) =
1R)) |