Step | Hyp | Ref
| Expression |
1 | | df-nqqs 6332 |
. . 3
⊢
Q = ((N × N) /
~Q ) |
2 | | breq1 3758 |
. . . 4
⊢
([〈y, z〉] ~Q = A → ([〈y, z〉]
~Q <Q [〈w, v〉]
~Q ↔ A
<Q [〈w,
v〉] ~Q
)) |
3 | | oveq1 5462 |
. . . . . 6
⊢
([〈y, z〉] ~Q = A → ([〈y, z〉]
~Q +Q x) = (A
+Q x)) |
4 | 3 | eqeq1d 2045 |
. . . . 5
⊢
([〈y, z〉] ~Q = A → (([〈y, z〉]
~Q +Q x) = [〈w,
v〉] ~Q ↔
(A +Q x) = [〈w,
v〉] ~Q
)) |
5 | 4 | rexbidv 2321 |
. . . 4
⊢
([〈y, z〉] ~Q = A → (∃x ∈ Q ([〈y, z〉]
~Q +Q x) = [〈w,
v〉] ~Q ↔
∃x ∈ Q (A +Q x) = [〈w,
v〉] ~Q
)) |
6 | 2, 5 | imbi12d 223 |
. . 3
⊢
([〈y, z〉] ~Q = A → (([〈y, z〉]
~Q <Q [〈w, v〉]
~Q → ∃x ∈
Q ([〈y, z〉] ~Q
+Q x) =
[〈w, v〉] ~Q ) ↔
(A <Q
[〈w, v〉] ~Q → ∃x ∈ Q (A +Q x) = [〈w,
v〉] ~Q
))) |
7 | | breq2 3759 |
. . . 4
⊢
([〈w, v〉] ~Q = B → (A
<Q [〈w,
v〉] ~Q ↔
A <Q B)) |
8 | | eqeq2 2046 |
. . . . 5
⊢
([〈w, v〉] ~Q = B → ((A
+Q x) =
[〈w, v〉] ~Q ↔
(A +Q x) = B)) |
9 | 8 | rexbidv 2321 |
. . . 4
⊢
([〈w, v〉] ~Q = B → (∃x ∈ Q (A +Q x) = [〈w,
v〉] ~Q ↔
∃x ∈ Q (A +Q x) = B)) |
10 | 7, 9 | imbi12d 223 |
. . 3
⊢
([〈w, v〉] ~Q = B → ((A
<Q [〈w,
v〉] ~Q →
∃x ∈ Q (A +Q x) = [〈w,
v〉] ~Q )
↔ (A <Q
B → ∃x ∈ Q (A +Q x) = B))) |
11 | | ordpipqqs 6358 |
. . . 4
⊢
(((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) → ([〈y, z〉]
~Q <Q [〈w, v〉]
~Q ↔ (y
·N v)
<N (z
·N w))) |
12 | | mulclpi 6312 |
. . . . . . . . 9
⊢
((y ∈ N ∧ v ∈ N) → (y ·N v) ∈
N) |
13 | | mulclpi 6312 |
. . . . . . . . 9
⊢
((z ∈ N ∧ w ∈ N) → (z ·N w) ∈
N) |
14 | 12, 13 | anim12i 321 |
. . . . . . . 8
⊢
(((y ∈ N ∧ v ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ((y ·N v) ∈
N ∧ (z ·N w) ∈
N)) |
15 | 14 | an42s 523 |
. . . . . . 7
⊢
(((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) → ((y ·N v) ∈
N ∧ (z ·N w) ∈
N)) |
16 | | ltexpi 6321 |
. . . . . . 7
⊢
(((y
·N v) ∈ N ∧ (z
·N w) ∈ N) → ((y ·N v) <N (z ·N w) ↔ ∃u ∈ N ((y ·N v) +N u) = (z
·N w))) |
17 | 15, 16 | syl 14 |
. . . . . 6
⊢
(((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) → ((y ·N v) <N (z ·N w) ↔ ∃u ∈ N ((y ·N v) +N u) = (z
·N w))) |
18 | | df-rex 2306 |
. . . . . 6
⊢ (∃u ∈ N ((y ·N v) +N u) = (z
·N w)
↔ ∃u(u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) |
19 | 17, 18 | syl6bb 185 |
. . . . 5
⊢
(((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) → ((y ·N v) <N (z ·N w) ↔ ∃u(u ∈
N ∧ ((y ·N v) +N u) = (z
·N w)))) |
20 | | simpll 481 |
. . . . . . . . . . . 12
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ u ∈ N) → (y ∈
N ∧ z ∈
N)) |
21 | | simpr 103 |
. . . . . . . . . . . 12
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ u ∈ N) → u ∈
N) |
22 | | simpr 103 |
. . . . . . . . . . . . . . 15
⊢
((y ∈ N ∧ z ∈ N) → z ∈
N) |
23 | | simpr 103 |
. . . . . . . . . . . . . . 15
⊢
((w ∈ N ∧ v ∈ N) → v ∈
N) |
24 | 22, 23 | anim12i 321 |
. . . . . . . . . . . . . 14
⊢
(((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) → (z ∈
N ∧ v ∈
N)) |
25 | 24 | adantr 261 |
. . . . . . . . . . . . 13
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ u ∈ N) → (z ∈
N ∧ v ∈
N)) |
26 | | mulclpi 6312 |
. . . . . . . . . . . . 13
⊢
((z ∈ N ∧ v ∈ N) → (z ·N v) ∈
N) |
27 | 25, 26 | syl 14 |
. . . . . . . . . . . 12
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ u ∈ N) → (z ·N v) ∈
N) |
28 | 20, 21, 27 | jca32 293 |
. . . . . . . . . . 11
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ u ∈ N) → ((y ∈
N ∧ z ∈
N) ∧ (u ∈
N ∧ (z ·N v) ∈
N))) |
29 | 28 | adantrr 448 |
. . . . . . . . . 10
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → ((y
∈ N ∧ z ∈ N) ∧ (u ∈ N ∧ (z
·N v) ∈ N))) |
30 | | addpipqqs 6354 |
. . . . . . . . . 10
⊢
(((y ∈ N ∧ z ∈ N) ∧ (u ∈ N ∧ (z
·N v) ∈ N)) → ([〈y, z〉]
~Q +Q [〈u, (z
·N v)〉] ~Q ) =
[〈((y
·N (z
·N v))
+N (z
·N u)),
(z ·N
(z ·N
v))〉] ~Q
) |
31 | 29, 30 | syl 14 |
. . . . . . . . 9
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → ([〈y, z〉]
~Q +Q [〈u, (z
·N v)〉] ~Q ) =
[〈((y
·N (z
·N v))
+N (z
·N u)),
(z ·N
(z ·N
v))〉] ~Q
) |
32 | | simplll 485 |
. . . . . . . . . . . . . . 15
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → y
∈ N) |
33 | | simpllr 486 |
. . . . . . . . . . . . . . 15
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → z
∈ N) |
34 | | simplrr 488 |
. . . . . . . . . . . . . . 15
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → v
∈ N) |
35 | | mulcompig 6315 |
. . . . . . . . . . . . . . . 16
⊢
((f ∈ N ∧ g ∈ N) → (f ·N g) = (g
·N f)) |
36 | 35 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
(((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) ∧ (f ∈
N ∧ g ∈
N)) → (f
·N g) =
(g ·N
f)) |
37 | | mulasspig 6316 |
. . . . . . . . . . . . . . . 16
⊢
((f ∈ N ∧ g ∈ N ∧ ℎ
∈ N) → ((f ·N g) ·N ℎ) = (f ·N (g ·N ℎ))) |
38 | 37 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
(((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) ∧ (f ∈
N ∧ g ∈
N ∧ ℎ ∈
N)) → ((f
·N g)
·N ℎ) = (f
·N (g
·N ℎ))) |
39 | 32, 33, 34, 36, 38 | caov12d 5624 |
. . . . . . . . . . . . . 14
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → (y
·N (z
·N v)) =
(z ·N
(y ·N
v))) |
40 | 39 | oveq1d 5470 |
. . . . . . . . . . . . 13
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → ((y
·N (z
·N v))
+N (z
·N u)) =
((z ·N
(y ·N
v)) +N (z ·N u))) |
41 | 32, 34, 12 | syl2anc 391 |
. . . . . . . . . . . . . 14
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → (y
·N v) ∈ N) |
42 | | simprl 483 |
. . . . . . . . . . . . . 14
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → u
∈ N) |
43 | | distrpig 6317 |
. . . . . . . . . . . . . 14
⊢
((z ∈ N ∧ (y
·N v) ∈ N ∧ u ∈ N) → (z ·N ((y ·N v) +N u)) = ((z
·N (y
·N v))
+N (z
·N u))) |
44 | 33, 41, 42, 43 | syl3anc 1134 |
. . . . . . . . . . . . 13
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → (z
·N ((y
·N v)
+N u)) =
((z ·N
(y ·N
v)) +N (z ·N u))) |
45 | 40, 44 | eqtr4d 2072 |
. . . . . . . . . . . 12
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → ((y
·N (z
·N v))
+N (z
·N u)) =
(z ·N
((y ·N
v) +N u))) |
46 | 45 | opeq1d 3546 |
. . . . . . . . . . 11
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → 〈((y ·N (z ·N v)) +N (z ·N u)), (z
·N (z
·N v))〉 = 〈(z ·N ((y ·N v) +N u)), (z
·N (z
·N v))〉) |
47 | 46 | eceq1d 6078 |
. . . . . . . . . 10
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → [〈((y ·N (z ·N v)) +N (z ·N u)), (z
·N (z
·N v))〉] ~Q =
[〈(z
·N ((y
·N v)
+N u)), (z ·N (z ·N v))〉] ~Q
) |
48 | | simpllr 486 |
. . . . . . . . . . . . 13
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ u ∈ N) → z ∈
N) |
49 | 12 | ad2ant2rl 480 |
. . . . . . . . . . . . . 14
⊢
(((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) → (y ·N v) ∈
N) |
50 | | addclpi 6311 |
. . . . . . . . . . . . . 14
⊢
(((y
·N v) ∈ N ∧ u ∈ N) → ((y ·N v) +N u) ∈
N) |
51 | 49, 50 | sylan 267 |
. . . . . . . . . . . . 13
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ u ∈ N) → ((y ·N v) +N u) ∈
N) |
52 | 48, 51, 27 | 3jca 1083 |
. . . . . . . . . . . 12
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ u ∈ N) → (z ∈
N ∧ ((y ·N v) +N u) ∈
N ∧ (z ·N v) ∈
N)) |
53 | 52 | adantrr 448 |
. . . . . . . . . . 11
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → (z
∈ N ∧ ((y
·N v)
+N u) ∈ N ∧ (z
·N v) ∈ N)) |
54 | | mulcanenqec 6370 |
. . . . . . . . . . 11
⊢
((z ∈ N ∧ ((y
·N v)
+N u) ∈ N ∧ (z
·N v) ∈ N) → [〈(z ·N ((y ·N v) +N u)), (z
·N (z
·N v))〉] ~Q =
[〈((y
·N v)
+N u), (z ·N v)〉] ~Q
) |
55 | 53, 54 | syl 14 |
. . . . . . . . . 10
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → [〈(z ·N ((y ·N v) +N u)), (z
·N (z
·N v))〉] ~Q =
[〈((y
·N v)
+N u), (z ·N v)〉] ~Q
) |
56 | 47, 55 | eqtrd 2069 |
. . . . . . . . 9
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → [〈((y ·N (z ·N v)) +N (z ·N u)), (z
·N (z
·N v))〉] ~Q =
[〈((y
·N v)
+N u), (z ·N v)〉] ~Q
) |
57 | | 3anass 888 |
. . . . . . . . . . . . . 14
⊢
((z ∈ N ∧ w ∈ N ∧ v ∈ N) ↔ (z ∈
N ∧ (w ∈
N ∧ v ∈
N))) |
58 | 57 | biimpri 124 |
. . . . . . . . . . . . 13
⊢
((z ∈ N ∧ (w ∈ N ∧ v ∈ N)) → (z ∈
N ∧ w ∈
N ∧ v ∈
N)) |
59 | 58 | adantll 445 |
. . . . . . . . . . . 12
⊢
(((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) → (z ∈
N ∧ w ∈
N ∧ v ∈
N)) |
60 | 59 | anim1i 323 |
. . . . . . . . . . 11
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ ((y
·N v)
+N u) = (z ·N w)) → ((z
∈ N ∧ w ∈ N ∧ v ∈ N) ∧ ((y
·N v)
+N u) = (z ·N w))) |
61 | 60 | adantrl 447 |
. . . . . . . . . 10
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → ((z
∈ N ∧ w ∈ N ∧ v ∈ N) ∧ ((y
·N v)
+N u) = (z ·N w))) |
62 | | opeq1 3540 |
. . . . . . . . . . . 12
⊢
(((y
·N v)
+N u) = (z ·N w) → 〈((y ·N v) +N u), (z
·N v)〉
= 〈(z
·N w),
(z ·N
v)〉) |
63 | 62 | eceq1d 6078 |
. . . . . . . . . . 11
⊢
(((y
·N v)
+N u) = (z ·N w) → [〈((y ·N v) +N u), (z
·N v)〉] ~Q =
[〈(z
·N w),
(z ·N
v)〉] ~Q
) |
64 | | mulcanenqec 6370 |
. . . . . . . . . . 11
⊢
((z ∈ N ∧ w ∈ N ∧ v ∈ N) → [〈(z ·N w), (z
·N v)〉] ~Q =
[〈w, v〉] ~Q
) |
65 | 63, 64 | sylan9eqr 2091 |
. . . . . . . . . 10
⊢
(((z ∈ N ∧ w ∈ N ∧ v ∈ N) ∧ ((y
·N v)
+N u) = (z ·N w)) → [〈((y ·N v) +N u), (z
·N v)〉] ~Q =
[〈w, v〉] ~Q
) |
66 | 61, 65 | syl 14 |
. . . . . . . . 9
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → [〈((y ·N v) +N u), (z
·N v)〉] ~Q =
[〈w, v〉] ~Q
) |
67 | 31, 56, 66 | 3eqtrd 2073 |
. . . . . . . 8
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → ([〈y, z〉]
~Q +Q [〈u, (z
·N v)〉] ~Q ) =
[〈w, v〉] ~Q
) |
68 | 33, 34, 26 | syl2anc 391 |
. . . . . . . . . . 11
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → (z
·N v) ∈ N) |
69 | | opelxpi 4319 |
. . . . . . . . . . . 12
⊢
((u ∈ N ∧ (z
·N v) ∈ N) → 〈u, (z
·N v)〉
∈ (N ×
N)) |
70 | | enqex 6344 |
. . . . . . . . . . . . 13
⊢
~Q ∈
V |
71 | 70 | ecelqsi 6096 |
. . . . . . . . . . . 12
⊢
(〈u, (z ·N v)〉 ∈
(N × N) → [〈u, (z
·N v)〉] ~Q ∈ ((N × N)
/ ~Q )) |
72 | 69, 71 | syl 14 |
. . . . . . . . . . 11
⊢
((u ∈ N ∧ (z
·N v) ∈ N) → [〈u, (z
·N v)〉] ~Q ∈ ((N × N)
/ ~Q )) |
73 | 42, 68, 72 | syl2anc 391 |
. . . . . . . . . 10
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → [〈u, (z
·N v)〉] ~Q ∈ ((N × N)
/ ~Q )) |
74 | 73, 1 | syl6eleqr 2128 |
. . . . . . . . 9
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → [〈u, (z
·N v)〉] ~Q ∈ Q) |
75 | | oveq2 5463 |
. . . . . . . . . . 11
⊢ (x = [〈u,
(z ·N
v)〉] ~Q
→ ([〈y, z〉] ~Q
+Q x) =
([〈y, z〉] ~Q
+Q [〈u,
(z ·N
v)〉] ~Q
)) |
76 | 75 | eqeq1d 2045 |
. . . . . . . . . 10
⊢ (x = [〈u,
(z ·N
v)〉] ~Q
→ (([〈y, z〉] ~Q
+Q x) =
[〈w, v〉] ~Q ↔
([〈y, z〉] ~Q
+Q [〈u,
(z ·N
v)〉] ~Q ) =
[〈w, v〉] ~Q
)) |
77 | 76 | adantl 262 |
. . . . . . . . 9
⊢
(((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) ∧ x = [〈u,
(z ·N
v)〉] ~Q )
→ (([〈y, z〉] ~Q
+Q x) =
[〈w, v〉] ~Q ↔
([〈y, z〉] ~Q
+Q [〈u,
(z ·N
v)〉] ~Q ) =
[〈w, v〉] ~Q
)) |
78 | 74, 77 | rspcedv 2654 |
. . . . . . . 8
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → (([〈y, z〉]
~Q +Q [〈u, (z
·N v)〉] ~Q ) =
[〈w, v〉] ~Q → ∃x ∈ Q ([〈y, z〉]
~Q +Q x) = [〈w,
v〉] ~Q
)) |
79 | 67, 78 | mpd 13 |
. . . . . . 7
⊢
((((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) ∧ (u ∈ N ∧ ((y
·N v)
+N u) = (z ·N w))) → ∃x ∈ Q ([〈y, z〉]
~Q +Q x) = [〈w,
v〉] ~Q
) |
80 | 79 | ex 108 |
. . . . . 6
⊢
(((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) → ((u ∈
N ∧ ((y ·N v) +N u) = (z
·N w))
→ ∃x ∈
Q ([〈y, z〉] ~Q
+Q x) =
[〈w, v〉] ~Q
)) |
81 | 80 | exlimdv 1697 |
. . . . 5
⊢
(((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) → (∃u(u ∈
N ∧ ((y ·N v) +N u) = (z
·N w))
→ ∃x ∈
Q ([〈y, z〉] ~Q
+Q x) =
[〈w, v〉] ~Q
)) |
82 | 19, 81 | sylbid 139 |
. . . 4
⊢
(((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) → ((y ·N v) <N (z ·N w) → ∃x ∈ Q ([〈y, z〉]
~Q +Q x) = [〈w,
v〉] ~Q
)) |
83 | 11, 82 | sylbid 139 |
. . 3
⊢
(((y ∈ N ∧ z ∈ N) ∧ (w ∈ N ∧ v ∈ N)) → ([〈y, z〉]
~Q <Q [〈w, v〉]
~Q → ∃x ∈
Q ([〈y, z〉] ~Q
+Q x) =
[〈w, v〉] ~Q
)) |
84 | 1, 6, 10, 83 | 2ecoptocl 6130 |
. 2
⊢
((A ∈ Q ∧ B ∈ Q) → (A <Q B → ∃x ∈ Q (A +Q x) = B)) |
85 | | ltaddnq 6390 |
. . . . 5
⊢
((A ∈ Q ∧ x ∈ Q) → A <Q (A +Q x)) |
86 | | breq2 3759 |
. . . . 5
⊢
((A +Q
x) = B
→ (A <Q
(A +Q x) ↔ A
<Q B)) |
87 | 85, 86 | syl5ibcom 144 |
. . . 4
⊢
((A ∈ Q ∧ x ∈ Q) → ((A +Q x) = B →
A <Q B)) |
88 | 87 | rexlimdva 2427 |
. . 3
⊢ (A ∈
Q → (∃x ∈
Q (A
+Q x) = B → A
<Q B)) |
89 | 88 | adantr 261 |
. 2
⊢
((A ∈ Q ∧ B ∈ Q) → (∃x ∈ Q (A +Q x) = B →
A <Q B)) |
90 | 84, 89 | impbid 120 |
1
⊢
((A ∈ Q ∧ B ∈ Q) → (A <Q B ↔ ∃x ∈ Q (A +Q x) = B)) |