Step | Hyp | Ref
| Expression |
1 | | ltrelnq 9708 |
. . . 4
⊢
<_{Q} ⊆ (Q ×
Q) |
2 | 1 | brel 5138 |
. . 3
⊢ (𝐴 <_{Q}
𝐵 → (𝐴 ∈ Q ∧ 𝐵 ∈
Q)) |
3 | | ordpinq 9725 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<_{Q} 𝐵 ↔ ((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) <_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴)))) |
4 | | elpqn 9707 |
. . . . . . . . 9
⊢ (𝐴 ∈ Q →
𝐴 ∈ (N
× N)) |
5 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ 𝐴 ∈
(N × N)) |
6 | | xp1st 7158 |
. . . . . . . 8
⊢ (𝐴 ∈ (N ×
N) → (1^{st} ‘𝐴) ∈ N) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1^{st} ‘𝐴) ∈ N) |
8 | | elpqn 9707 |
. . . . . . . . 9
⊢ (𝐵 ∈ Q →
𝐵 ∈ (N
× N)) |
9 | 8 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ 𝐵 ∈
(N × N)) |
10 | | xp2nd 7159 |
. . . . . . . 8
⊢ (𝐵 ∈ (N ×
N) → (2^{nd} ‘𝐵) ∈ N) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2^{nd} ‘𝐵) ∈ N) |
12 | | mulclpi 9675 |
. . . . . . 7
⊢
(((1^{st} ‘𝐴) ∈ N ∧
(2^{nd} ‘𝐵)
∈ N) → ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
13 | 7, 11, 12 | syl2anc 692 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
14 | | xp1st 7158 |
. . . . . . . 8
⊢ (𝐵 ∈ (N ×
N) → (1^{st} ‘𝐵) ∈ N) |
15 | 9, 14 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1^{st} ‘𝐵) ∈ N) |
16 | | xp2nd 7159 |
. . . . . . . 8
⊢ (𝐴 ∈ (N ×
N) → (2^{nd} ‘𝐴) ∈ N) |
17 | 5, 16 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2^{nd} ‘𝐴) ∈ N) |
18 | | mulclpi 9675 |
. . . . . . 7
⊢
(((1^{st} ‘𝐵) ∈ N ∧
(2^{nd} ‘𝐴)
∈ N) → ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
∈ N) |
19 | 15, 17, 18 | syl2anc 692 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
∈ N) |
20 | | ltexpi 9684 |
. . . . . 6
⊢
((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N ∧ ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
∈ N) → (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
<_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
↔ ∃𝑦 ∈
N (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} 𝑦) = ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))) |
21 | 13, 19, 20 | syl2anc 692 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
<_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
↔ ∃𝑦 ∈
N (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} 𝑦) = ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))) |
22 | | relxp 5198 |
. . . . . . . . . . . 12
⊢ Rel
(N × N) |
23 | 4 | ad2antrr 761 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 𝐴
∈ (N × N)) |
24 | | 1st2nd 7174 |
. . . . . . . . . . . 12
⊢ ((Rel
(N × N) ∧ 𝐴 ∈ (N ×
N)) → 𝐴
= ⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩) |
25 | 22, 23, 24 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 𝐴 =
⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩) |
26 | 25 | oveq1d 6630 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (𝐴
+_{pQ} ⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩) = (⟨(1^{st}
‘𝐴), (2^{nd}
‘𝐴)⟩
+_{pQ} ⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩)) |
27 | 7 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (1^{st} ‘𝐴) ∈ N) |
28 | 17 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (2^{nd} ‘𝐴) ∈ N) |
29 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 𝑦
∈ N) |
30 | | mulclpi 9675 |
. . . . . . . . . . . . 13
⊢
(((2^{nd} ‘𝐴) ∈ N ∧
(2^{nd} ‘𝐵)
∈ N) → ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
31 | 17, 11, 30 | syl2anc 692 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
32 | 31 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
33 | | addpipq 9719 |
. . . . . . . . . . 11
⊢
((((1^{st} ‘𝐴) ∈ N ∧
(2^{nd} ‘𝐴)
∈ N) ∧ (𝑦 ∈ N ∧
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) ∈ N)) →
(⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩ +_{pQ}
⟨𝑦, ((2^{nd}
‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩) = ⟨(((1^{st}
‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
+_{N} (𝑦 ·_{N}
(2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))⟩) |
34 | 27, 28, 29, 32, 33 | syl22anc 1324 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩ +_{pQ}
⟨𝑦, ((2^{nd}
‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩) = ⟨(((1^{st}
‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
+_{N} (𝑦 ·_{N}
(2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))⟩) |
35 | 26, 34 | eqtrd 2655 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (𝐴
+_{pQ} ⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩) = ⟨(((1^{st}
‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
+_{N} (𝑦 ·_{N}
(2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))⟩) |
36 | | oveq2 6623 |
. . . . . . . . . . . 12
⊢
((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} 𝑦) = ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
→ ((2^{nd} ‘𝐴) ·_{N}
(((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) +_{N} 𝑦)) = ((2^{nd}
‘𝐴)
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))) |
37 | | distrpi 9680 |
. . . . . . . . . . . . 13
⊢
((2^{nd} ‘𝐴) ·_{N}
(((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) +_{N} 𝑦)) = (((2^{nd}
‘𝐴)
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
+_{N} ((2^{nd} ‘𝐴) ·_{N} 𝑦)) |
38 | | fvex 6168 |
. . . . . . . . . . . . . . 15
⊢
(2^{nd} ‘𝐴) ∈ V |
39 | | fvex 6168 |
. . . . . . . . . . . . . . 15
⊢
(1^{st} ‘𝐴) ∈ V |
40 | | fvex 6168 |
. . . . . . . . . . . . . . 15
⊢
(2^{nd} ‘𝐵) ∈ V |
41 | | mulcompi 9678 |
. . . . . . . . . . . . . . 15
⊢ (𝑥
·_{N} 𝑦) = (𝑦 ·_{N} 𝑥) |
42 | | mulasspi 9679 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥
·_{N} 𝑦) ·_{N} 𝑧) = (𝑥 ·_{N} (𝑦
·_{N} 𝑧)) |
43 | 38, 39, 40, 41, 42 | caov12 6827 |
. . . . . . . . . . . . . 14
⊢
((2^{nd} ‘𝐴) ·_{N}
((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))) = ((1^{st} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))) |
44 | | mulcompi 9678 |
. . . . . . . . . . . . . 14
⊢
((2^{nd} ‘𝐴) ·_{N} 𝑦) = (𝑦 ·_{N}
(2^{nd} ‘𝐴)) |
45 | 43, 44 | oveq12i 6627 |
. . . . . . . . . . . . 13
⊢
(((2^{nd} ‘𝐴) ·_{N}
((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))) +_{N}
((2^{nd} ‘𝐴)
·_{N} 𝑦)) = (((1^{st} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
+_{N} (𝑦 ·_{N}
(2^{nd} ‘𝐴))) |
46 | 37, 45 | eqtr2i 2644 |
. . . . . . . . . . . 12
⊢
(((1^{st} ‘𝐴) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))) +_{N} (𝑦
·_{N} (2^{nd} ‘𝐴))) = ((2^{nd} ‘𝐴)
·_{N} (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} 𝑦)) |
47 | | mulasspi 9679 |
. . . . . . . . . . . . 13
⊢
(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)) = ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(1^{st} ‘𝐵))) |
48 | | mulcompi 9678 |
. . . . . . . . . . . . . 14
⊢
((2^{nd} ‘𝐴) ·_{N}
(1^{st} ‘𝐵))
= ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)) |
49 | 48 | oveq2i 6626 |
. . . . . . . . . . . . 13
⊢
((2^{nd} ‘𝐴) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (1^{st} ‘𝐵))) = ((2^{nd} ‘𝐴)
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))) |
50 | 47, 49 | eqtri 2643 |
. . . . . . . . . . . 12
⊢
(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)) = ((2^{nd} ‘𝐴)
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))) |
51 | 36, 46, 50 | 3eqtr4g 2680 |
. . . . . . . . . . 11
⊢
((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} 𝑦) = ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
→ (((1^{st} ‘𝐴) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))) +_{N} (𝑦
·_{N} (2^{nd} ‘𝐴))) = (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(1^{st} ‘𝐵))) |
52 | | mulasspi 9679 |
. . . . . . . . . . . . 13
⊢
(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (2^{nd} ‘𝐵)) = ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))) |
53 | 52 | eqcomi 2630 |
. . . . . . . . . . . 12
⊢
((2^{nd} ‘𝐴) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))) = (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵)) |
54 | 53 | a1i 11 |
. . . . . . . . . . 11
⊢
((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} 𝑦) = ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
→ ((2^{nd} ‘𝐴) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))) = (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))) |
55 | 51, 54 | opeq12d 4385 |
. . . . . . . . . 10
⊢
((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} 𝑦) = ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
→ ⟨(((1^{st} ‘𝐴) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))) +_{N} (𝑦
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))⟩ = ⟨(((2^{nd}
‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(1^{st} ‘𝐵)),
(((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩) |
56 | 55 | eqeq2d 2631 |
. . . . . . . . 9
⊢
((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} 𝑦) = ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
→ ((𝐴
+_{pQ} ⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩) = ⟨(((1^{st}
‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
+_{N} (𝑦 ·_{N}
(2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))⟩ ↔ (𝐴 +_{pQ} ⟨𝑦, ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩) = ⟨(((2^{nd}
‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(1^{st} ‘𝐵)),
(((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩)) |
57 | 35, 56 | syl5ibcom 235 |
. . . . . . . 8
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} 𝑦) = ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
→ (𝐴
+_{pQ} ⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩) = ⟨(((2^{nd}
‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(1^{st} ‘𝐵)),
(((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩)) |
58 | | fveq2 6158 |
. . . . . . . . 9
⊢ ((𝐴 +_{pQ}
⟨𝑦, ((2^{nd}
‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩) = ⟨(((2^{nd}
‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(1^{st} ‘𝐵)),
(((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩ →
([Q]‘(𝐴
+_{pQ} ⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩)) =
([Q]‘⟨(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩)) |
59 | | adderpq 9738 |
. . . . . . . . . . 11
⊢
(([Q]‘𝐴) +_{Q}
([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩)) = ([Q]‘(𝐴 +_{pQ}
⟨𝑦, ((2^{nd}
‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩)) |
60 | | nqerid 9715 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Q →
([Q]‘𝐴)
= 𝐴) |
61 | 60 | ad2antrr 761 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ([Q]‘𝐴) = 𝐴) |
62 | 61 | oveq1d 6630 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (([Q]‘𝐴) +_{Q}
([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩)) = (𝐴 +_{Q}
([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩))) |
63 | 59, 62 | syl5eqr 2669 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ([Q]‘(𝐴 +_{pQ} ⟨𝑦, ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩)) = (𝐴 +_{Q}
([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩))) |
64 | | mulclpi 9675 |
. . . . . . . . . . . . . . . 16
⊢
(((2^{nd} ‘𝐴) ∈ N ∧
(2^{nd} ‘𝐴)
∈ N) → ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
∈ N) |
65 | 17, 17, 64 | syl2anc 692 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
∈ N) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
∈ N) |
67 | 15 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (1^{st} ‘𝐵) ∈ N) |
68 | 11 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (2^{nd} ‘𝐵) ∈ N) |
69 | | mulcanenq 9742 |
. . . . . . . . . . . . . 14
⊢
((((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
∈ N ∧ (1^{st} ‘𝐵) ∈ N ∧
(2^{nd} ‘𝐵)
∈ N) → ⟨(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩ ~_{Q}
⟨(1^{st} ‘𝐵), (2^{nd} ‘𝐵)⟩) |
70 | 66, 67, 68, 69 | syl3anc 1323 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ⟨(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩ ~_{Q}
⟨(1^{st} ‘𝐵), (2^{nd} ‘𝐵)⟩) |
71 | 8 | ad2antlr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 𝐵
∈ (N × N)) |
72 | | 1st2nd 7174 |
. . . . . . . . . . . . . 14
⊢ ((Rel
(N × N) ∧ 𝐵 ∈ (N ×
N)) → 𝐵
= ⟨(1^{st} ‘𝐵), (2^{nd} ‘𝐵)⟩) |
73 | 22, 71, 72 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 𝐵 =
⟨(1^{st} ‘𝐵), (2^{nd} ‘𝐵)⟩) |
74 | 70, 73 | breqtrrd 4651 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ⟨(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩ ~_{Q} 𝐵) |
75 | | mulclpi 9675 |
. . . . . . . . . . . . . . 15
⊢
((((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
∈ N ∧ (1^{st} ‘𝐵) ∈ N) →
(((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(1^{st} ‘𝐵))
∈ N) |
76 | 66, 67, 75 | syl2anc 692 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)) ∈ N) |
77 | | mulclpi 9675 |
. . . . . . . . . . . . . . 15
⊢
((((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
∈ N ∧ (2^{nd} ‘𝐵) ∈ N) →
(((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
78 | 66, 68, 77 | syl2anc 692 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (2^{nd} ‘𝐵)) ∈ N) |
79 | | opelxpi 5118 |
. . . . . . . . . . . . . 14
⊢
(((((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)) ∈ N ∧
(((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))
∈ N) → ⟨(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩ ∈ (N ×
N)) |
80 | 76, 78, 79 | syl2anc 692 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ⟨(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩ ∈ (N ×
N)) |
81 | | nqereq 9717 |
. . . . . . . . . . . . 13
⊢
((⟨(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩ ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
(⟨(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩ ~_{Q} 𝐵 ↔
([Q]‘⟨(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩) = ([Q]‘𝐵))) |
82 | 80, 71, 81 | syl2anc 692 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (⟨(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩ ~_{Q} 𝐵 ↔
([Q]‘⟨(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩) = ([Q]‘𝐵))) |
83 | 74, 82 | mpbid 222 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ([Q]‘⟨(((2^{nd}
‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(1^{st} ‘𝐵)),
(((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩) = ([Q]‘𝐵)) |
84 | | nqerid 9715 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ Q →
([Q]‘𝐵)
= 𝐵) |
85 | 84 | ad2antlr 762 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ([Q]‘𝐵) = 𝐵) |
86 | 83, 85 | eqtrd 2655 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ([Q]‘⟨(((2^{nd}
‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(1^{st} ‘𝐵)),
(((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩) = 𝐵) |
87 | 63, 86 | eqeq12d 2636 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (([Q]‘(𝐴 +_{pQ} ⟨𝑦, ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩)) =
([Q]‘⟨(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (1^{st} ‘𝐵)), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩) ↔ (𝐴 +_{Q}
([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩)) = 𝐵)) |
88 | 58, 87 | syl5ib 234 |
. . . . . . . 8
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ((𝐴
+_{pQ} ⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩) = ⟨(((2^{nd}
‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(1^{st} ‘𝐵)),
(((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐵))⟩ → (𝐴 +_{Q}
([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩)) = 𝐵)) |
89 | 57, 88 | syld 47 |
. . . . . . 7
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} 𝑦) = ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
→ (𝐴
+_{Q} ([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩)) = 𝐵)) |
90 | | fvex 6168 |
. . . . . . . 8
⊢
([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩) ∈ V |
91 | | oveq2 6623 |
. . . . . . . . 9
⊢ (𝑥 =
([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩) → (𝐴 +_{Q} 𝑥) = (𝐴 +_{Q}
([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩))) |
92 | 91 | eqeq1d 2623 |
. . . . . . . 8
⊢ (𝑥 =
([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩) → ((𝐴 +_{Q} 𝑥) = 𝐵 ↔ (𝐴 +_{Q}
([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩)) = 𝐵)) |
93 | 90, 92 | spcev 3290 |
. . . . . . 7
⊢ ((𝐴 +_{Q}
([Q]‘⟨𝑦, ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))⟩)) = 𝐵 → ∃𝑥(𝐴 +_{Q} 𝑥) = 𝐵) |
94 | 89, 93 | syl6 35 |
. . . . . 6
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} 𝑦) = ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
→ ∃𝑥(𝐴 +_{Q}
𝑥) = 𝐵)) |
95 | 94 | rexlimdva 3026 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (∃𝑦 ∈
N (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} 𝑦) = ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
→ ∃𝑥(𝐴 +_{Q}
𝑥) = 𝐵)) |
96 | 21, 95 | sylbid 230 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
<_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
→ ∃𝑥(𝐴 +_{Q}
𝑥) = 𝐵)) |
97 | 3, 96 | sylbid 230 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<_{Q} 𝐵 → ∃𝑥(𝐴 +_{Q} 𝑥) = 𝐵)) |
98 | 2, 97 | mpcom 38 |
. 2
⊢ (𝐴 <_{Q}
𝐵 → ∃𝑥(𝐴 +_{Q} 𝑥) = 𝐵) |
99 | | eleq1 2686 |
. . . . . . 7
⊢ ((𝐴 +_{Q}
𝑥) = 𝐵 → ((𝐴 +_{Q} 𝑥) ∈ Q ↔
𝐵 ∈
Q)) |
100 | 99 | biimparc 504 |
. . . . . 6
⊢ ((𝐵 ∈ Q ∧
(𝐴
+_{Q} 𝑥) = 𝐵) → (𝐴 +_{Q} 𝑥) ∈
Q) |
101 | | addnqf 9730 |
. . . . . . . 8
⊢
+_{Q} :(Q ×
Q)⟶Q |
102 | 101 | fdmi 6019 |
. . . . . . 7
⊢ dom
+_{Q} = (Q ×
Q) |
103 | | 0nnq 9706 |
. . . . . . 7
⊢ ¬
∅ ∈ Q |
104 | 102, 103 | ndmovrcl 6785 |
. . . . . 6
⊢ ((𝐴 +_{Q}
𝑥) ∈ Q
→ (𝐴 ∈
Q ∧ 𝑥
∈ Q)) |
105 | | ltaddnq 9756 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝑥 ∈ Q)
→ 𝐴
<_{Q} (𝐴 +_{Q} 𝑥)) |
106 | 100, 104,
105 | 3syl 18 |
. . . . 5
⊢ ((𝐵 ∈ Q ∧
(𝐴
+_{Q} 𝑥) = 𝐵) → 𝐴 <_{Q} (𝐴 +_{Q}
𝑥)) |
107 | | simpr 477 |
. . . . 5
⊢ ((𝐵 ∈ Q ∧
(𝐴
+_{Q} 𝑥) = 𝐵) → (𝐴 +_{Q} 𝑥) = 𝐵) |
108 | 106, 107 | breqtrd 4649 |
. . . 4
⊢ ((𝐵 ∈ Q ∧
(𝐴
+_{Q} 𝑥) = 𝐵) → 𝐴 <_{Q} 𝐵) |
109 | 108 | ex 450 |
. . 3
⊢ (𝐵 ∈ Q →
((𝐴
+_{Q} 𝑥) = 𝐵 → 𝐴 <_{Q} 𝐵)) |
110 | 109 | exlimdv 1858 |
. 2
⊢ (𝐵 ∈ Q →
(∃𝑥(𝐴 +_{Q} 𝑥) = 𝐵 → 𝐴 <_{Q} 𝐵)) |
111 | 98, 110 | impbid2 216 |
1
⊢ (𝐵 ∈ Q →
(𝐴
<_{Q} 𝐵 ↔ ∃𝑥(𝐴 +_{Q} 𝑥) = 𝐵)) |