Step | Hyp | Ref
| Expression |
1 | | df-nqqs 6332 |
. 2
⊢
Q = ((N × N) /
~Q ) |
2 | | addpipqqs 6354 |
. 2
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ([〈x, y〉]
~Q +Q [〈z, w〉]
~Q ) = [〈((x
·N w)
+N (y
·N z)),
(y ·N
w)〉] ~Q
) |
3 | | addpipqqs 6354 |
. 2
⊢
(((z ∈ N ∧ w ∈ N) ∧ (x ∈ N ∧ y ∈ N)) → ([〈z, w〉]
~Q +Q [〈x, y〉]
~Q ) = [〈((z
·N y)
+N (w
·N x)),
(w ·N
y)〉] ~Q
) |
4 | | mulcompig 6315 |
. . . . 5
⊢
((x ∈ N ∧ w ∈ N) → (x ·N w) = (w
·N x)) |
5 | | mulcompig 6315 |
. . . . 5
⊢
((y ∈ N ∧ z ∈ N) → (y ·N z) = (z
·N y)) |
6 | 4, 5 | oveqan12d 5474 |
. . . 4
⊢
(((x ∈ N ∧ w ∈ N) ∧ (y ∈ N ∧ z ∈ N)) → ((x ·N w) +N (y ·N z)) = ((w
·N x)
+N (z
·N y))) |
7 | 6 | an42s 523 |
. . 3
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ((x ·N w) +N (y ·N z)) = ((w
·N x)
+N (z
·N y))) |
8 | | mulclpi 6312 |
. . . . . 6
⊢
((w ∈ N ∧ x ∈ N) → (w ·N x) ∈
N) |
9 | 8 | ancoms 255 |
. . . . 5
⊢
((x ∈ N ∧ w ∈ N) → (w ·N x) ∈
N) |
10 | 9 | ad2ant2rl 480 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → (w ·N x) ∈
N) |
11 | | mulclpi 6312 |
. . . . . 6
⊢
((z ∈ N ∧ y ∈ N) → (z ·N y) ∈
N) |
12 | 11 | ancoms 255 |
. . . . 5
⊢
((y ∈ N ∧ z ∈ N) → (z ·N y) ∈
N) |
13 | 12 | ad2ant2lr 479 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → (z ·N y) ∈
N) |
14 | | addcompig 6313 |
. . . 4
⊢
(((w
·N x) ∈ N ∧ (z
·N y) ∈ N) → ((w ·N x) +N (z ·N y)) = ((z
·N y)
+N (w
·N x))) |
15 | 10, 13, 14 | syl2anc 391 |
. . 3
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ((w ·N x) +N (z ·N y)) = ((z
·N y)
+N (w
·N x))) |
16 | 7, 15 | eqtrd 2069 |
. 2
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ((x ·N w) +N (y ·N z)) = ((z
·N y)
+N (w
·N x))) |
17 | | mulcompig 6315 |
. . 3
⊢
((y ∈ N ∧ w ∈ N) → (y ·N w) = (w
·N y)) |
18 | 17 | ad2ant2l 477 |
. 2
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → (y ·N w) = (w
·N y)) |
19 | 1, 2, 3, 16, 18 | ecovicom 6150 |
1
⊢
((A ∈ Q ∧ B ∈ Q) → (A +Q B) = (B
+Q A)) |