Step | Hyp | Ref
| Expression |
1 | | df-nqqs 7310 |
. 2
⊢
Q = ((N × N) /
~Q ) |
2 | | addpipqqs 7332 |
. 2
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈
N ∧ 𝑤
∈ N)) → ([〈𝑥, 𝑦〉] ~Q
+Q [〈𝑧, 𝑤〉] ~Q ) =
[〈((𝑥
·N 𝑤) +N (𝑦
·N 𝑧)), (𝑦 ·N 𝑤)〉]
~Q ) |
3 | | addpipqqs 7332 |
. 2
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑥 ∈
N ∧ 𝑦
∈ N)) → ([〈𝑧, 𝑤〉] ~Q
+Q [〈𝑥, 𝑦〉] ~Q ) =
[〈((𝑧
·N 𝑦) +N (𝑤
·N 𝑥)), (𝑤 ·N 𝑦)〉]
~Q ) |
4 | | mulcompig 7293 |
. . . . 5
⊢ ((𝑥 ∈ N ∧
𝑤 ∈ N)
→ (𝑥
·N 𝑤) = (𝑤 ·N 𝑥)) |
5 | | mulcompig 7293 |
. . . . 5
⊢ ((𝑦 ∈ N ∧
𝑧 ∈ N)
→ (𝑦
·N 𝑧) = (𝑧 ·N 𝑦)) |
6 | 4, 5 | oveqan12d 5872 |
. . . 4
⊢ (((𝑥 ∈ N ∧
𝑤 ∈ N)
∧ (𝑦 ∈
N ∧ 𝑧
∈ N)) → ((𝑥 ·N 𝑤) +N
(𝑦
·N 𝑧)) = ((𝑤 ·N 𝑥) +N
(𝑧
·N 𝑦))) |
7 | 6 | an42s 584 |
. . 3
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈
N ∧ 𝑤
∈ N)) → ((𝑥 ·N 𝑤) +N
(𝑦
·N 𝑧)) = ((𝑤 ·N 𝑥) +N
(𝑧
·N 𝑦))) |
8 | | mulclpi 7290 |
. . . . . 6
⊢ ((𝑤 ∈ N ∧
𝑥 ∈ N)
→ (𝑤
·N 𝑥) ∈ N) |
9 | 8 | ancoms 266 |
. . . . 5
⊢ ((𝑥 ∈ N ∧
𝑤 ∈ N)
→ (𝑤
·N 𝑥) ∈ N) |
10 | 9 | ad2ant2rl 508 |
. . . 4
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈
N ∧ 𝑤
∈ N)) → (𝑤 ·N 𝑥) ∈
N) |
11 | | mulclpi 7290 |
. . . . . 6
⊢ ((𝑧 ∈ N ∧
𝑦 ∈ N)
→ (𝑧
·N 𝑦) ∈ N) |
12 | 11 | ancoms 266 |
. . . . 5
⊢ ((𝑦 ∈ N ∧
𝑧 ∈ N)
→ (𝑧
·N 𝑦) ∈ N) |
13 | 12 | ad2ant2lr 507 |
. . . 4
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈
N ∧ 𝑤
∈ N)) → (𝑧 ·N 𝑦) ∈
N) |
14 | | addcompig 7291 |
. . . 4
⊢ (((𝑤
·N 𝑥) ∈ N ∧ (𝑧
·N 𝑦) ∈ N) → ((𝑤
·N 𝑥) +N (𝑧
·N 𝑦)) = ((𝑧 ·N 𝑦) +N
(𝑤
·N 𝑥))) |
15 | 10, 13, 14 | syl2anc 409 |
. . 3
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈
N ∧ 𝑤
∈ N)) → ((𝑤 ·N 𝑥) +N
(𝑧
·N 𝑦)) = ((𝑧 ·N 𝑦) +N
(𝑤
·N 𝑥))) |
16 | 7, 15 | eqtrd 2203 |
. 2
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈
N ∧ 𝑤
∈ N)) → ((𝑥 ·N 𝑤) +N
(𝑦
·N 𝑧)) = ((𝑧 ·N 𝑦) +N
(𝑤
·N 𝑥))) |
17 | | mulcompig 7293 |
. . 3
⊢ ((𝑦 ∈ N ∧
𝑤 ∈ N)
→ (𝑦
·N 𝑤) = (𝑤 ·N 𝑦)) |
18 | 17 | ad2ant2l 505 |
. 2
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈
N ∧ 𝑤
∈ N)) → (𝑦 ·N 𝑤) = (𝑤 ·N 𝑦)) |
19 | 1, 2, 3, 16, 18 | ecovicom 6621 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
+Q 𝐵) = (𝐵 +Q 𝐴)) |