Step | Hyp | Ref
| Expression |
1 | | df-nqqs 7310 |
. . 3
⊢
Q = ((N × N) /
~Q ) |
2 | | breq1 3992 |
. . . 4
⊢
([〈𝑦, 𝑧〉]
~Q = 𝐴 → ([〈𝑦, 𝑧〉] ~Q
<Q [〈𝑤, 𝑣〉] ~Q ↔
𝐴
<Q [〈𝑤, 𝑣〉] ~Q
)) |
3 | | oveq1 5860 |
. . . . . 6
⊢
([〈𝑦, 𝑧〉]
~Q = 𝐴 → ([〈𝑦, 𝑧〉] ~Q
+Q 𝑥) = (𝐴 +Q 𝑥)) |
4 | 3 | eqeq1d 2179 |
. . . . 5
⊢
([〈𝑦, 𝑧〉]
~Q = 𝐴 → (([〈𝑦, 𝑧〉] ~Q
+Q 𝑥) = [〈𝑤, 𝑣〉] ~Q ↔
(𝐴
+Q 𝑥) = [〈𝑤, 𝑣〉] ~Q
)) |
5 | 4 | rexbidv 2471 |
. . . 4
⊢
([〈𝑦, 𝑧〉]
~Q = 𝐴 → (∃𝑥 ∈ Q ([〈𝑦, 𝑧〉] ~Q
+Q 𝑥) = [〈𝑤, 𝑣〉] ~Q ↔
∃𝑥 ∈
Q (𝐴
+Q 𝑥) = [〈𝑤, 𝑣〉] ~Q
)) |
6 | 2, 5 | imbi12d 233 |
. . 3
⊢
([〈𝑦, 𝑧〉]
~Q = 𝐴 → (([〈𝑦, 𝑧〉] ~Q
<Q [〈𝑤, 𝑣〉] ~Q →
∃𝑥 ∈
Q ([〈𝑦,
𝑧〉]
~Q +Q 𝑥) = [〈𝑤, 𝑣〉] ~Q ) ↔
(𝐴
<Q [〈𝑤, 𝑣〉] ~Q →
∃𝑥 ∈
Q (𝐴
+Q 𝑥) = [〈𝑤, 𝑣〉] ~Q
))) |
7 | | breq2 3993 |
. . . 4
⊢
([〈𝑤, 𝑣〉]
~Q = 𝐵 → (𝐴 <Q [〈𝑤, 𝑣〉] ~Q ↔
𝐴
<Q 𝐵)) |
8 | | eqeq2 2180 |
. . . . 5
⊢
([〈𝑤, 𝑣〉]
~Q = 𝐵 → ((𝐴 +Q 𝑥) = [〈𝑤, 𝑣〉] ~Q ↔
(𝐴
+Q 𝑥) = 𝐵)) |
9 | 8 | rexbidv 2471 |
. . . 4
⊢
([〈𝑤, 𝑣〉]
~Q = 𝐵 → (∃𝑥 ∈ Q (𝐴 +Q 𝑥) = [〈𝑤, 𝑣〉] ~Q ↔
∃𝑥 ∈
Q (𝐴
+Q 𝑥) = 𝐵)) |
10 | 7, 9 | imbi12d 233 |
. . 3
⊢
([〈𝑤, 𝑣〉]
~Q = 𝐵 → ((𝐴 <Q [〈𝑤, 𝑣〉] ~Q →
∃𝑥 ∈
Q (𝐴
+Q 𝑥) = [〈𝑤, 𝑣〉] ~Q ) ↔
(𝐴
<Q 𝐵 → ∃𝑥 ∈ Q (𝐴 +Q 𝑥) = 𝐵))) |
11 | | ordpipqqs 7336 |
. . . 4
⊢ (((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) → ([〈𝑦, 𝑧〉] ~Q
<Q [〈𝑤, 𝑣〉] ~Q ↔
(𝑦
·N 𝑣) <N (𝑧
·N 𝑤))) |
12 | | mulclpi 7290 |
. . . . . . . . 9
⊢ ((𝑦 ∈ N ∧
𝑣 ∈ N)
→ (𝑦
·N 𝑣) ∈ N) |
13 | | mulclpi 7290 |
. . . . . . . . 9
⊢ ((𝑧 ∈ N ∧
𝑤 ∈ N)
→ (𝑧
·N 𝑤) ∈ N) |
14 | 12, 13 | anim12i 336 |
. . . . . . . 8
⊢ (((𝑦 ∈ N ∧
𝑣 ∈ N)
∧ (𝑧 ∈
N ∧ 𝑤
∈ N)) → ((𝑦 ·N 𝑣) ∈ N ∧
(𝑧
·N 𝑤) ∈ N)) |
15 | 14 | an42s 584 |
. . . . . . 7
⊢ (((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) → ((𝑦 ·N 𝑣) ∈ N ∧
(𝑧
·N 𝑤) ∈ N)) |
16 | | ltexpi 7299 |
. . . . . . 7
⊢ (((𝑦
·N 𝑣) ∈ N ∧ (𝑧
·N 𝑤) ∈ N) → ((𝑦
·N 𝑣) <N (𝑧
·N 𝑤) ↔ ∃𝑢 ∈ N ((𝑦 ·N 𝑣) +N
𝑢) = (𝑧 ·N 𝑤))) |
17 | 15, 16 | syl 14 |
. . . . . 6
⊢ (((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) → ((𝑦 ·N 𝑣) <N
(𝑧
·N 𝑤) ↔ ∃𝑢 ∈ N ((𝑦 ·N 𝑣) +N
𝑢) = (𝑧 ·N 𝑤))) |
18 | | df-rex 2454 |
. . . . . 6
⊢
(∃𝑢 ∈
N ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤) ↔ ∃𝑢(𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) |
19 | 17, 18 | bitrdi 195 |
. . . . 5
⊢ (((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) → ((𝑦 ·N 𝑣) <N
(𝑧
·N 𝑤) ↔ ∃𝑢(𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤)))) |
20 | | simpll 524 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ 𝑢 ∈ N) → (𝑦 ∈ N ∧
𝑧 ∈
N)) |
21 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ 𝑢 ∈ N) → 𝑢 ∈
N) |
22 | | simpr 109 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ N ∧
𝑧 ∈ N)
→ 𝑧 ∈
N) |
23 | | simpr 109 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ N ∧
𝑣 ∈ N)
→ 𝑣 ∈
N) |
24 | 22, 23 | anim12i 336 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) → (𝑧 ∈ N ∧ 𝑣 ∈
N)) |
25 | 24 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ 𝑢 ∈ N) → (𝑧 ∈ N ∧
𝑣 ∈
N)) |
26 | | mulclpi 7290 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ N ∧
𝑣 ∈ N)
→ (𝑧
·N 𝑣) ∈ N) |
27 | 25, 26 | syl 14 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ 𝑢 ∈ N) → (𝑧
·N 𝑣) ∈ N) |
28 | 20, 21, 27 | jca32 308 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ 𝑢 ∈ N) → ((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑢 ∈
N ∧ (𝑧
·N 𝑣) ∈ N))) |
29 | 28 | adantrr 476 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → ((𝑦 ∈ N ∧ 𝑧 ∈ N) ∧
(𝑢 ∈ N
∧ (𝑧
·N 𝑣) ∈ N))) |
30 | | addpipqqs 7332 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑢 ∈
N ∧ (𝑧
·N 𝑣) ∈ N)) →
([〈𝑦, 𝑧〉]
~Q +Q [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q ) = [〈((𝑦 ·N (𝑧
·N 𝑣)) +N (𝑧
·N 𝑢)), (𝑧 ·N (𝑧
·N 𝑣))〉] ~Q
) |
31 | 29, 30 | syl 14 |
. . . . . . . . 9
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → ([〈𝑦, 𝑧〉] ~Q
+Q [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q ) = [〈((𝑦 ·N (𝑧
·N 𝑣)) +N (𝑧
·N 𝑢)), (𝑧 ·N (𝑧
·N 𝑣))〉] ~Q
) |
32 | | simplll 528 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → 𝑦 ∈ N) |
33 | | simpllr 529 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → 𝑧 ∈ N) |
34 | | simplrr 531 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → 𝑣 ∈ N) |
35 | | mulcompig 7293 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ N ∧
𝑔 ∈ N)
→ (𝑓
·N 𝑔) = (𝑔 ·N 𝑓)) |
36 | 35 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
N ∧ 𝑧
∈ N) ∧ (𝑤 ∈ N ∧ 𝑣 ∈ N)) ∧
(𝑢 ∈ N
∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) ∧ (𝑓 ∈ N ∧ 𝑔 ∈ N)) →
(𝑓
·N 𝑔) = (𝑔 ·N 𝑓)) |
37 | | mulasspig 7294 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ N ∧
𝑔 ∈ N
∧ ℎ ∈
N) → ((𝑓
·N 𝑔) ·N ℎ) = (𝑓 ·N (𝑔
·N ℎ))) |
38 | 37 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
N ∧ 𝑧
∈ N) ∧ (𝑤 ∈ N ∧ 𝑣 ∈ N)) ∧
(𝑢 ∈ N
∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) ∧ (𝑓 ∈ N ∧ 𝑔 ∈ N ∧
ℎ ∈ N))
→ ((𝑓
·N 𝑔) ·N ℎ) = (𝑓 ·N (𝑔
·N ℎ))) |
39 | 32, 33, 34, 36, 38 | caov12d 6034 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → (𝑦 ·N (𝑧
·N 𝑣)) = (𝑧 ·N (𝑦
·N 𝑣))) |
40 | 39 | oveq1d 5868 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → ((𝑦 ·N (𝑧
·N 𝑣)) +N (𝑧
·N 𝑢)) = ((𝑧 ·N (𝑦
·N 𝑣)) +N (𝑧
·N 𝑢))) |
41 | 32, 34, 12 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → (𝑦 ·N 𝑣) ∈
N) |
42 | | simprl 526 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → 𝑢 ∈ N) |
43 | | distrpig 7295 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ N ∧
(𝑦
·N 𝑣) ∈ N ∧ 𝑢 ∈ N) →
(𝑧
·N ((𝑦 ·N 𝑣) +N
𝑢)) = ((𝑧 ·N (𝑦
·N 𝑣)) +N (𝑧
·N 𝑢))) |
44 | 33, 41, 42, 43 | syl3anc 1233 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → (𝑧 ·N ((𝑦
·N 𝑣) +N 𝑢)) = ((𝑧 ·N (𝑦
·N 𝑣)) +N (𝑧
·N 𝑢))) |
45 | 40, 44 | eqtr4d 2206 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → ((𝑦 ·N (𝑧
·N 𝑣)) +N (𝑧
·N 𝑢)) = (𝑧 ·N ((𝑦
·N 𝑣) +N 𝑢))) |
46 | 45 | opeq1d 3771 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → 〈((𝑦
·N (𝑧 ·N 𝑣)) +N
(𝑧
·N 𝑢)), (𝑧 ·N (𝑧
·N 𝑣))〉 = 〈(𝑧 ·N ((𝑦
·N 𝑣) +N 𝑢)), (𝑧 ·N (𝑧
·N 𝑣))〉) |
47 | 46 | eceq1d 6549 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → [〈((𝑦
·N (𝑧 ·N 𝑣)) +N
(𝑧
·N 𝑢)), (𝑧 ·N (𝑧
·N 𝑣))〉] ~Q =
[〈(𝑧
·N ((𝑦 ·N 𝑣) +N
𝑢)), (𝑧 ·N (𝑧
·N 𝑣))〉] ~Q
) |
48 | | simpllr 529 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ 𝑢 ∈ N) → 𝑧 ∈
N) |
49 | 12 | ad2ant2rl 508 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) → (𝑦 ·N 𝑣) ∈
N) |
50 | | addclpi 7289 |
. . . . . . . . . . . . . 14
⊢ (((𝑦
·N 𝑣) ∈ N ∧ 𝑢 ∈ N) →
((𝑦
·N 𝑣) +N 𝑢) ∈
N) |
51 | 49, 50 | sylan 281 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ 𝑢 ∈ N) → ((𝑦
·N 𝑣) +N 𝑢) ∈
N) |
52 | 48, 51, 27 | 3jca 1172 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ 𝑢 ∈ N) → (𝑧 ∈ N ∧
((𝑦
·N 𝑣) +N 𝑢) ∈ N ∧
(𝑧
·N 𝑣) ∈ N)) |
53 | 52 | adantrr 476 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → (𝑧 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) ∈ N ∧
(𝑧
·N 𝑣) ∈ N)) |
54 | | mulcanenqec 7348 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ N ∧
((𝑦
·N 𝑣) +N 𝑢) ∈ N ∧
(𝑧
·N 𝑣) ∈ N) →
[〈(𝑧
·N ((𝑦 ·N 𝑣) +N
𝑢)), (𝑧 ·N (𝑧
·N 𝑣))〉] ~Q =
[〈((𝑦
·N 𝑣) +N 𝑢), (𝑧 ·N 𝑣)〉]
~Q ) |
55 | 53, 54 | syl 14 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → [〈(𝑧
·N ((𝑦 ·N 𝑣) +N
𝑢)), (𝑧 ·N (𝑧
·N 𝑣))〉] ~Q =
[〈((𝑦
·N 𝑣) +N 𝑢), (𝑧 ·N 𝑣)〉]
~Q ) |
56 | 47, 55 | eqtrd 2203 |
. . . . . . . . 9
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → [〈((𝑦
·N (𝑧 ·N 𝑣)) +N
(𝑧
·N 𝑢)), (𝑧 ·N (𝑧
·N 𝑣))〉] ~Q =
[〈((𝑦
·N 𝑣) +N 𝑢), (𝑧 ·N 𝑣)〉]
~Q ) |
57 | | 3anass 977 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ N ∧
𝑤 ∈ N
∧ 𝑣 ∈
N) ↔ (𝑧
∈ N ∧ (𝑤 ∈ N ∧ 𝑣 ∈
N))) |
58 | 57 | biimpri 132 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ N ∧
(𝑤 ∈ N
∧ 𝑣 ∈
N)) → (𝑧
∈ N ∧ 𝑤 ∈ N ∧ 𝑣 ∈
N)) |
59 | 58 | adantll 473 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) → (𝑧 ∈ N ∧ 𝑤 ∈ N ∧
𝑣 ∈
N)) |
60 | 59 | anim1i 338 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ ((𝑦 ·N 𝑣) +N
𝑢) = (𝑧 ·N 𝑤)) → ((𝑧 ∈ N ∧ 𝑤 ∈ N ∧
𝑣 ∈ N)
∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) |
61 | 60 | adantrl 475 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → ((𝑧 ∈ N ∧ 𝑤 ∈ N ∧
𝑣 ∈ N)
∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) |
62 | | opeq1 3765 |
. . . . . . . . . . . 12
⊢ (((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤) → 〈((𝑦
·N 𝑣) +N 𝑢), (𝑧 ·N 𝑣)〉 = 〈(𝑧
·N 𝑤), (𝑧 ·N 𝑣)〉) |
63 | 62 | eceq1d 6549 |
. . . . . . . . . . 11
⊢ (((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤) → [〈((𝑦
·N 𝑣) +N 𝑢), (𝑧 ·N 𝑣)〉]
~Q = [〈(𝑧 ·N 𝑤), (𝑧 ·N 𝑣)〉]
~Q ) |
64 | | mulcanenqec 7348 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ N ∧
𝑤 ∈ N
∧ 𝑣 ∈
N) → [〈(𝑧 ·N 𝑤), (𝑧 ·N 𝑣)〉]
~Q = [〈𝑤, 𝑣〉] ~Q
) |
65 | 63, 64 | sylan9eqr 2225 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N
∧ 𝑣 ∈
N) ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤)) → [〈((𝑦
·N 𝑣) +N 𝑢), (𝑧 ·N 𝑣)〉]
~Q = [〈𝑤, 𝑣〉] ~Q
) |
66 | 61, 65 | syl 14 |
. . . . . . . . 9
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → [〈((𝑦
·N 𝑣) +N 𝑢), (𝑧 ·N 𝑣)〉]
~Q = [〈𝑤, 𝑣〉] ~Q
) |
67 | 31, 56, 66 | 3eqtrd 2207 |
. . . . . . . 8
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → ([〈𝑦, 𝑧〉] ~Q
+Q [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q ) = [〈𝑤, 𝑣〉] ~Q
) |
68 | 33, 34, 26 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → (𝑧 ·N 𝑣) ∈
N) |
69 | | opelxpi 4643 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ N ∧
(𝑧
·N 𝑣) ∈ N) → 〈𝑢, (𝑧 ·N 𝑣)〉 ∈ (N
× N)) |
70 | | enqex 7322 |
. . . . . . . . . . . . 13
⊢
~Q ∈ V |
71 | 70 | ecelqsi 6567 |
. . . . . . . . . . . 12
⊢
(〈𝑢, (𝑧
·N 𝑣)〉 ∈ (N ×
N) → [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q ∈ ((N × N)
/ ~Q )) |
72 | 69, 71 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ N ∧
(𝑧
·N 𝑣) ∈ N) → [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q ∈ ((N × N)
/ ~Q )) |
73 | 42, 68, 72 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q ∈ ((N × N)
/ ~Q )) |
74 | 73, 1 | eleqtrrdi 2264 |
. . . . . . . . 9
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q ∈ Q) |
75 | | oveq2 5861 |
. . . . . . . . . . 11
⊢ (𝑥 = [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q → ([〈𝑦, 𝑧〉] ~Q
+Q 𝑥) = ([〈𝑦, 𝑧〉] ~Q
+Q [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q )) |
76 | 75 | eqeq1d 2179 |
. . . . . . . . . 10
⊢ (𝑥 = [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q → (([〈𝑦, 𝑧〉] ~Q
+Q 𝑥) = [〈𝑤, 𝑣〉] ~Q ↔
([〈𝑦, 𝑧〉]
~Q +Q [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q ) = [〈𝑤, 𝑣〉] ~Q
)) |
77 | 76 | adantl 275 |
. . . . . . . . 9
⊢
(((((𝑦 ∈
N ∧ 𝑧
∈ N) ∧ (𝑤 ∈ N ∧ 𝑣 ∈ N)) ∧
(𝑢 ∈ N
∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) ∧ 𝑥 = [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q ) → (([〈𝑦, 𝑧〉] ~Q
+Q 𝑥) = [〈𝑤, 𝑣〉] ~Q ↔
([〈𝑦, 𝑧〉]
~Q +Q [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q ) = [〈𝑤, 𝑣〉] ~Q
)) |
78 | 74, 77 | rspcedv 2838 |
. . . . . . . 8
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → (([〈𝑦, 𝑧〉] ~Q
+Q [〈𝑢, (𝑧 ·N 𝑣)〉]
~Q ) = [〈𝑤, 𝑣〉] ~Q →
∃𝑥 ∈
Q ([〈𝑦,
𝑧〉]
~Q +Q 𝑥) = [〈𝑤, 𝑣〉] ~Q
)) |
79 | 67, 78 | mpd 13 |
. . . . . . 7
⊢ ((((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) ∧ (𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤))) → ∃𝑥 ∈ Q
([〈𝑦, 𝑧〉]
~Q +Q 𝑥) = [〈𝑤, 𝑣〉] ~Q
) |
80 | 79 | ex 114 |
. . . . . 6
⊢ (((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) → ((𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤)) → ∃𝑥 ∈ Q
([〈𝑦, 𝑧〉]
~Q +Q 𝑥) = [〈𝑤, 𝑣〉] ~Q
)) |
81 | 80 | exlimdv 1812 |
. . . . 5
⊢ (((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) → (∃𝑢(𝑢 ∈ N ∧ ((𝑦
·N 𝑣) +N 𝑢) = (𝑧 ·N 𝑤)) → ∃𝑥 ∈ Q
([〈𝑦, 𝑧〉]
~Q +Q 𝑥) = [〈𝑤, 𝑣〉] ~Q
)) |
82 | 19, 81 | sylbid 149 |
. . . 4
⊢ (((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) → ((𝑦 ·N 𝑣) <N
(𝑧
·N 𝑤) → ∃𝑥 ∈ Q ([〈𝑦, 𝑧〉] ~Q
+Q 𝑥) = [〈𝑤, 𝑣〉] ~Q
)) |
83 | 11, 82 | sylbid 149 |
. . 3
⊢ (((𝑦 ∈ N ∧
𝑧 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) → ([〈𝑦, 𝑧〉] ~Q
<Q [〈𝑤, 𝑣〉] ~Q →
∃𝑥 ∈
Q ([〈𝑦,
𝑧〉]
~Q +Q 𝑥) = [〈𝑤, 𝑣〉] ~Q
)) |
84 | 1, 6, 10, 83 | 2ecoptocl 6601 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<Q 𝐵 → ∃𝑥 ∈ Q (𝐴 +Q 𝑥) = 𝐵)) |
85 | | ltaddnq 7369 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝑥 ∈ Q)
→ 𝐴
<Q (𝐴 +Q 𝑥)) |
86 | | breq2 3993 |
. . . . 5
⊢ ((𝐴 +Q
𝑥) = 𝐵 → (𝐴 <Q (𝐴 +Q
𝑥) ↔ 𝐴 <Q 𝐵)) |
87 | 85, 86 | syl5ibcom 154 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝑥 ∈ Q)
→ ((𝐴
+Q 𝑥) = 𝐵 → 𝐴 <Q 𝐵)) |
88 | 87 | rexlimdva 2587 |
. . 3
⊢ (𝐴 ∈ Q →
(∃𝑥 ∈
Q (𝐴
+Q 𝑥) = 𝐵 → 𝐴 <Q 𝐵)) |
89 | 88 | adantr 274 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (∃𝑥 ∈
Q (𝐴
+Q 𝑥) = 𝐵 → 𝐴 <Q 𝐵)) |
90 | 84, 89 | impbid 128 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<Q 𝐵 ↔ ∃𝑥 ∈ Q (𝐴 +Q 𝑥) = 𝐵)) |