Step | Hyp | Ref
| Expression |
1 | | nqpi 7340 |
. . . 4
⊢ (𝐴 ∈ Q →
∃𝑧∃𝑤((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q
)) |
2 | | nqpi 7340 |
. . . 4
⊢ (𝐵 ∈ Q →
∃𝑣∃𝑢((𝑣 ∈ N ∧ 𝑢 ∈ N) ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q
)) |
3 | 1, 2 | anim12i 336 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (∃𝑧∃𝑤((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
∃𝑣∃𝑢((𝑣 ∈ N ∧ 𝑢 ∈ N) ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q
))) |
4 | | ee4anv 1927 |
. . 3
⊢
(∃𝑧∃𝑤∃𝑣∃𝑢(((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
((𝑣 ∈ N
∧ 𝑢 ∈
N) ∧ 𝐵 =
[〈𝑣, 𝑢〉]
~Q )) ↔ (∃𝑧∃𝑤((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
∃𝑣∃𝑢((𝑣 ∈ N ∧ 𝑢 ∈ N) ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q
))) |
5 | 3, 4 | sylibr 133 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ∃𝑧∃𝑤∃𝑣∃𝑢(((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
((𝑣 ∈ N
∧ 𝑢 ∈
N) ∧ 𝐵 =
[〈𝑣, 𝑢〉]
~Q ))) |
6 | | oveq12 5862 |
. . . . . . 7
⊢ ((𝐴 = [〈𝑧, 𝑤〉] ~Q ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q ) →
(𝐴
·Q 𝐵) = ([〈𝑧, 𝑤〉] ~Q
·Q [〈𝑣, 𝑢〉] ~Q
)) |
7 | | mulpiord 7279 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ N ∧
𝑣 ∈ N)
→ (𝑧
·N 𝑣) = (𝑧 ·o 𝑣)) |
8 | 7 | ad2ant2r 506 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝑧 ·N 𝑣) = (𝑧 ·o 𝑣)) |
9 | | mulpiord 7279 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ N ∧
𝑢 ∈ N)
→ (𝑤
·N 𝑢) = (𝑤 ·o 𝑢)) |
10 | 9 | ad2ant2l 505 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝑤 ·N 𝑢) = (𝑤 ·o 𝑢)) |
11 | 8, 10 | opeq12d 3773 |
. . . . . . . . 9
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → 〈(𝑧 ·N 𝑣), (𝑤 ·N 𝑢)〉 = 〈(𝑧 ·o 𝑣), (𝑤 ·o 𝑢)〉) |
12 | 11 | eceq1d 6549 |
. . . . . . . 8
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → [〈(𝑧 ·N 𝑣), (𝑤 ·N 𝑢)〉]
~Q0 = [〈(𝑧 ·o 𝑣), (𝑤 ·o 𝑢)〉] ~Q0
) |
13 | | mulpipqqs 7335 |
. . . . . . . . 9
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ([〈𝑧, 𝑤〉] ~Q
·Q [〈𝑣, 𝑢〉] ~Q ) =
[〈(𝑧
·N 𝑣), (𝑤 ·N 𝑢)〉]
~Q ) |
14 | | mulclpi 7290 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ N ∧
𝑣 ∈ N)
→ (𝑧
·N 𝑣) ∈ N) |
15 | 14 | ad2ant2r 506 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝑧 ·N 𝑣) ∈
N) |
16 | | mulclpi 7290 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ N ∧
𝑢 ∈ N)
→ (𝑤
·N 𝑢) ∈ N) |
17 | 16 | ad2ant2l 505 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝑤 ·N 𝑢) ∈
N) |
18 | | nqnq0pi 7400 |
. . . . . . . . . 10
⊢ (((𝑧
·N 𝑣) ∈ N ∧ (𝑤
·N 𝑢) ∈ N) →
[〈(𝑧
·N 𝑣), (𝑤 ·N 𝑢)〉]
~Q0 = [〈(𝑧 ·N 𝑣), (𝑤 ·N 𝑢)〉]
~Q ) |
19 | 15, 17, 18 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → [〈(𝑧 ·N 𝑣), (𝑤 ·N 𝑢)〉]
~Q0 = [〈(𝑧 ·N 𝑣), (𝑤 ·N 𝑢)〉]
~Q ) |
20 | 13, 19 | eqtr4d 2206 |
. . . . . . . 8
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ([〈𝑧, 𝑤〉] ~Q
·Q [〈𝑣, 𝑢〉] ~Q ) =
[〈(𝑧
·N 𝑣), (𝑤 ·N 𝑢)〉]
~Q0 ) |
21 | | pinn 7271 |
. . . . . . . . . 10
⊢ (𝑧 ∈ N →
𝑧 ∈
ω) |
22 | 21 | anim1i 338 |
. . . . . . . . 9
⊢ ((𝑧 ∈ N ∧
𝑤 ∈ N)
→ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) |
23 | | pinn 7271 |
. . . . . . . . . 10
⊢ (𝑣 ∈ N →
𝑣 ∈
ω) |
24 | 23 | anim1i 338 |
. . . . . . . . 9
⊢ ((𝑣 ∈ N ∧
𝑢 ∈ N)
→ (𝑣 ∈ ω
∧ 𝑢 ∈
N)) |
25 | | mulnnnq0 7412 |
. . . . . . . . 9
⊢ (((𝑧 ∈ ω ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ ω ∧
𝑢 ∈ N))
→ ([〈𝑧, 𝑤〉]
~Q0 ·Q0 [〈𝑣, 𝑢〉] ~Q0 ) =
[〈(𝑧
·o 𝑣),
(𝑤 ·o
𝑢)〉]
~Q0 ) |
26 | 22, 24, 25 | syl2an 287 |
. . . . . . . 8
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ([〈𝑧, 𝑤〉] ~Q0
·Q0 [〈𝑣, 𝑢〉] ~Q0 ) =
[〈(𝑧
·o 𝑣),
(𝑤 ·o
𝑢)〉]
~Q0 ) |
27 | 12, 20, 26 | 3eqtr4d 2213 |
. . . . . . 7
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ([〈𝑧, 𝑤〉] ~Q
·Q [〈𝑣, 𝑢〉] ~Q ) =
([〈𝑧, 𝑤〉]
~Q0 ·Q0 [〈𝑣, 𝑢〉] ~Q0
)) |
28 | 6, 27 | sylan9eqr 2225 |
. . . . . 6
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) ∧ (𝐴 = [〈𝑧, 𝑤〉] ~Q ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q )) →
(𝐴
·Q 𝐵) = ([〈𝑧, 𝑤〉] ~Q0
·Q0 [〈𝑣, 𝑢〉] ~Q0
)) |
29 | | nqnq0pi 7400 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ N ∧
𝑤 ∈ N)
→ [〈𝑧, 𝑤〉]
~Q0 = [〈𝑧, 𝑤〉] ~Q
) |
30 | 29 | adantr 274 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → [〈𝑧, 𝑤〉] ~Q0 =
[〈𝑧, 𝑤〉]
~Q ) |
31 | 30 | eqeq2d 2182 |
. . . . . . . . 9
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝐴 = [〈𝑧, 𝑤〉] ~Q0 ↔
𝐴 = [〈𝑧, 𝑤〉] ~Q
)) |
32 | | nqnq0pi 7400 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ N ∧
𝑢 ∈ N)
→ [〈𝑣, 𝑢〉]
~Q0 = [〈𝑣, 𝑢〉] ~Q
) |
33 | 32 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → [〈𝑣, 𝑢〉] ~Q0 =
[〈𝑣, 𝑢〉]
~Q ) |
34 | 33 | eqeq2d 2182 |
. . . . . . . . 9
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝐵 = [〈𝑣, 𝑢〉] ~Q0 ↔
𝐵 = [〈𝑣, 𝑢〉] ~Q
)) |
35 | 31, 34 | anbi12d 470 |
. . . . . . . 8
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ((𝐴 = [〈𝑧, 𝑤〉] ~Q0 ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q0 ) ↔
(𝐴 = [〈𝑧, 𝑤〉] ~Q ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q
))) |
36 | 35 | pm5.32i 451 |
. . . . . . 7
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) ∧ (𝐴 = [〈𝑧, 𝑤〉] ~Q0 ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q0 ))
↔ (((𝑧 ∈
N ∧ 𝑤
∈ N) ∧ (𝑣 ∈ N ∧ 𝑢 ∈ N)) ∧
(𝐴 = [〈𝑧, 𝑤〉] ~Q ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q
))) |
37 | | oveq12 5862 |
. . . . . . . 8
⊢ ((𝐴 = [〈𝑧, 𝑤〉] ~Q0 ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q0 ) →
(𝐴
·Q0 𝐵) = ([〈𝑧, 𝑤〉] ~Q0
·Q0 [〈𝑣, 𝑢〉] ~Q0
)) |
38 | 37 | adantl 275 |
. . . . . . 7
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) ∧ (𝐴 = [〈𝑧, 𝑤〉] ~Q0 ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q0 ))
→ (𝐴
·Q0 𝐵) = ([〈𝑧, 𝑤〉] ~Q0
·Q0 [〈𝑣, 𝑢〉] ~Q0
)) |
39 | 36, 38 | sylbir 134 |
. . . . . 6
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) ∧ (𝐴 = [〈𝑧, 𝑤〉] ~Q ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q )) →
(𝐴
·Q0 𝐵) = ([〈𝑧, 𝑤〉] ~Q0
·Q0 [〈𝑣, 𝑢〉] ~Q0
)) |
40 | 28, 39 | eqtr4d 2206 |
. . . . 5
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) ∧ (𝐴 = [〈𝑧, 𝑤〉] ~Q ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q )) →
(𝐴
·Q 𝐵) = (𝐴 ·Q0 𝐵)) |
41 | 40 | an4s 583 |
. . . 4
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ 𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
((𝑣 ∈ N
∧ 𝑢 ∈
N) ∧ 𝐵 =
[〈𝑣, 𝑢〉]
~Q )) → (𝐴 ·Q 𝐵) = (𝐴 ·Q0 𝐵)) |
42 | 41 | exlimivv 1889 |
. . 3
⊢
(∃𝑣∃𝑢(((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
((𝑣 ∈ N
∧ 𝑢 ∈
N) ∧ 𝐵 =
[〈𝑣, 𝑢〉]
~Q )) → (𝐴 ·Q 𝐵) = (𝐴 ·Q0 𝐵)) |
43 | 42 | exlimivv 1889 |
. 2
⊢
(∃𝑧∃𝑤∃𝑣∃𝑢(((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
((𝑣 ∈ N
∧ 𝑢 ∈
N) ∧ 𝐵 =
[〈𝑣, 𝑢〉]
~Q )) → (𝐴 ·Q 𝐵) = (𝐴 ·Q0 𝐵)) |
44 | 5, 43 | syl 14 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
·Q 𝐵) = (𝐴 ·Q0 𝐵)) |