Step | Hyp | Ref
| Expression |
1 | | ltrelnq 10540 |
. . . 4
⊢
<Q ⊆ (Q ×
Q) |
2 | 1 | brel 5614 |
. . 3
⊢ (𝐴 <Q
𝐵 → (𝐴 ∈ Q ∧ 𝐵 ∈
Q)) |
3 | | ordpinq 10557 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<Q 𝐵 ↔ ((1st ‘𝐴)
·N (2nd ‘𝐵)) <N
((1st ‘𝐵)
·N (2nd ‘𝐴)))) |
4 | | elpqn 10539 |
. . . . . . . . 9
⊢ (𝐴 ∈ Q →
𝐴 ∈ (N
× N)) |
5 | 4 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ 𝐴 ∈
(N × N)) |
6 | | xp1st 7793 |
. . . . . . . 8
⊢ (𝐴 ∈ (N ×
N) → (1st ‘𝐴) ∈ N) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1st ‘𝐴) ∈ N) |
8 | | elpqn 10539 |
. . . . . . . . 9
⊢ (𝐵 ∈ Q →
𝐵 ∈ (N
× N)) |
9 | 8 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ 𝐵 ∈
(N × N)) |
10 | | xp2nd 7794 |
. . . . . . . 8
⊢ (𝐵 ∈ (N ×
N) → (2nd ‘𝐵) ∈ N) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2nd ‘𝐵) ∈ N) |
12 | | mulclpi 10507 |
. . . . . . 7
⊢
(((1st ‘𝐴) ∈ N ∧
(2nd ‘𝐵)
∈ N) → ((1st ‘𝐴) ·N
(2nd ‘𝐵))
∈ N) |
13 | 7, 11, 12 | syl2anc 587 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((1st ‘𝐴) ·N
(2nd ‘𝐵))
∈ N) |
14 | | xp1st 7793 |
. . . . . . . 8
⊢ (𝐵 ∈ (N ×
N) → (1st ‘𝐵) ∈ N) |
15 | 9, 14 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1st ‘𝐵) ∈ N) |
16 | | xp2nd 7794 |
. . . . . . . 8
⊢ (𝐴 ∈ (N ×
N) → (2nd ‘𝐴) ∈ N) |
17 | 5, 16 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2nd ‘𝐴) ∈ N) |
18 | | mulclpi 10507 |
. . . . . . 7
⊢
(((1st ‘𝐵) ∈ N ∧
(2nd ‘𝐴)
∈ N) → ((1st ‘𝐵) ·N
(2nd ‘𝐴))
∈ N) |
19 | 15, 17, 18 | syl2anc 587 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((1st ‘𝐵) ·N
(2nd ‘𝐴))
∈ N) |
20 | | ltexpi 10516 |
. . . . . 6
⊢
((((1st ‘𝐴) ·N
(2nd ‘𝐵))
∈ N ∧ ((1st ‘𝐵) ·N
(2nd ‘𝐴))
∈ N) → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ ∃𝑦 ∈
N (((1st ‘𝐴) ·N
(2nd ‘𝐵))
+N 𝑦) = ((1st ‘𝐵) ·N
(2nd ‘𝐴)))) |
21 | 13, 19, 20 | syl2anc 587 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ ∃𝑦 ∈
N (((1st ‘𝐴) ·N
(2nd ‘𝐵))
+N 𝑦) = ((1st ‘𝐵) ·N
(2nd ‘𝐴)))) |
22 | | relxp 5569 |
. . . . . . . . . . . 12
⊢ Rel
(N × N) |
23 | 4 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 𝐴
∈ (N × N)) |
24 | | 1st2nd 7810 |
. . . . . . . . . . . 12
⊢ ((Rel
(N × N) ∧ 𝐴 ∈ (N ×
N)) → 𝐴
= 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
25 | 22, 23, 24 | sylancr 590 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 𝐴 =
〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
26 | 25 | oveq1d 7228 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (𝐴
+pQ 〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉) = (〈(1st
‘𝐴), (2nd
‘𝐴)〉
+pQ 〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉)) |
27 | 7 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (1st ‘𝐴) ∈ N) |
28 | 17 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (2nd ‘𝐴) ∈ N) |
29 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 𝑦
∈ N) |
30 | | mulclpi 10507 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘𝐴) ∈ N ∧
(2nd ‘𝐵)
∈ N) → ((2nd ‘𝐴) ·N
(2nd ‘𝐵))
∈ N) |
31 | 17, 11, 30 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((2nd ‘𝐴) ·N
(2nd ‘𝐵))
∈ N) |
32 | 31 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ((2nd ‘𝐴) ·N
(2nd ‘𝐵))
∈ N) |
33 | | addpipq 10551 |
. . . . . . . . . . 11
⊢
((((1st ‘𝐴) ∈ N ∧
(2nd ‘𝐴)
∈ N) ∧ (𝑦 ∈ N ∧
((2nd ‘𝐴)
·N (2nd ‘𝐵)) ∈ N)) →
(〈(1st ‘𝐴), (2nd ‘𝐴)〉 +pQ
〈𝑦, ((2nd
‘𝐴)
·N (2nd ‘𝐵))〉) = 〈(((1st
‘𝐴)
·N ((2nd ‘𝐴) ·N
(2nd ‘𝐵)))
+N (𝑦 ·N
(2nd ‘𝐴))), ((2nd ‘𝐴)
·N ((2nd ‘𝐴) ·N
(2nd ‘𝐵)))〉) |
34 | 27, 28, 29, 32, 33 | syl22anc 839 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (〈(1st ‘𝐴), (2nd ‘𝐴)〉 +pQ
〈𝑦, ((2nd
‘𝐴)
·N (2nd ‘𝐵))〉) = 〈(((1st
‘𝐴)
·N ((2nd ‘𝐴) ·N
(2nd ‘𝐵)))
+N (𝑦 ·N
(2nd ‘𝐴))), ((2nd ‘𝐴)
·N ((2nd ‘𝐴) ·N
(2nd ‘𝐵)))〉) |
35 | 26, 34 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (𝐴
+pQ 〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉) = 〈(((1st
‘𝐴)
·N ((2nd ‘𝐴) ·N
(2nd ‘𝐵)))
+N (𝑦 ·N
(2nd ‘𝐴))), ((2nd ‘𝐴)
·N ((2nd ‘𝐴) ·N
(2nd ‘𝐵)))〉) |
36 | | oveq2 7221 |
. . . . . . . . . . . 12
⊢
((((1st ‘𝐴) ·N
(2nd ‘𝐵))
+N 𝑦) = ((1st ‘𝐵) ·N
(2nd ‘𝐴))
→ ((2nd ‘𝐴) ·N
(((1st ‘𝐴)
·N (2nd ‘𝐵)) +N 𝑦)) = ((2nd
‘𝐴)
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))) |
37 | | distrpi 10512 |
. . . . . . . . . . . . 13
⊢
((2nd ‘𝐴) ·N
(((1st ‘𝐴)
·N (2nd ‘𝐵)) +N 𝑦)) = (((2nd
‘𝐴)
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))
+N ((2nd ‘𝐴) ·N 𝑦)) |
38 | | fvex 6730 |
. . . . . . . . . . . . . . 15
⊢
(2nd ‘𝐴) ∈ V |
39 | | fvex 6730 |
. . . . . . . . . . . . . . 15
⊢
(1st ‘𝐴) ∈ V |
40 | | fvex 6730 |
. . . . . . . . . . . . . . 15
⊢
(2nd ‘𝐵) ∈ V |
41 | | mulcompi 10510 |
. . . . . . . . . . . . . . 15
⊢ (𝑥
·N 𝑦) = (𝑦 ·N 𝑥) |
42 | | mulasspi 10511 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥
·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦
·N 𝑧)) |
43 | 38, 39, 40, 41, 42 | caov12 7436 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝐴) ·N
((1st ‘𝐴)
·N (2nd ‘𝐵))) = ((1st ‘𝐴)
·N ((2nd ‘𝐴) ·N
(2nd ‘𝐵))) |
44 | | mulcompi 10510 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝐴) ·N 𝑦) = (𝑦 ·N
(2nd ‘𝐴)) |
45 | 43, 44 | oveq12i 7225 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘𝐴) ·N
((1st ‘𝐴)
·N (2nd ‘𝐵))) +N
((2nd ‘𝐴)
·N 𝑦)) = (((1st ‘𝐴)
·N ((2nd ‘𝐴) ·N
(2nd ‘𝐵)))
+N (𝑦 ·N
(2nd ‘𝐴))) |
46 | 37, 45 | eqtr2i 2766 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝐴) ·N
((2nd ‘𝐴)
·N (2nd ‘𝐵))) +N (𝑦
·N (2nd ‘𝐴))) = ((2nd ‘𝐴)
·N (((1st ‘𝐴) ·N
(2nd ‘𝐵))
+N 𝑦)) |
47 | | mulasspi 10511 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)) = ((2nd ‘𝐴)
·N ((2nd ‘𝐴) ·N
(1st ‘𝐵))) |
48 | | mulcompi 10510 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝐴) ·N
(1st ‘𝐵))
= ((1st ‘𝐵) ·N
(2nd ‘𝐴)) |
49 | 48 | oveq2i 7224 |
. . . . . . . . . . . . 13
⊢
((2nd ‘𝐴) ·N
((2nd ‘𝐴)
·N (1st ‘𝐵))) = ((2nd ‘𝐴)
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴))) |
50 | 47, 49 | eqtri 2765 |
. . . . . . . . . . . 12
⊢
(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)) = ((2nd ‘𝐴)
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴))) |
51 | 36, 46, 50 | 3eqtr4g 2803 |
. . . . . . . . . . 11
⊢
((((1st ‘𝐴) ·N
(2nd ‘𝐵))
+N 𝑦) = ((1st ‘𝐵) ·N
(2nd ‘𝐴))
→ (((1st ‘𝐴) ·N
((2nd ‘𝐴)
·N (2nd ‘𝐵))) +N (𝑦
·N (2nd ‘𝐴))) = (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(1st ‘𝐵))) |
52 | | mulasspi 10511 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (2nd ‘𝐵)) = ((2nd ‘𝐴)
·N ((2nd ‘𝐴) ·N
(2nd ‘𝐵))) |
53 | 52 | eqcomi 2746 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝐴) ·N
((2nd ‘𝐴)
·N (2nd ‘𝐵))) = (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵)) |
54 | 53 | a1i 11 |
. . . . . . . . . . 11
⊢
((((1st ‘𝐴) ·N
(2nd ‘𝐵))
+N 𝑦) = ((1st ‘𝐵) ·N
(2nd ‘𝐴))
→ ((2nd ‘𝐴) ·N
((2nd ‘𝐴)
·N (2nd ‘𝐵))) = (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))) |
55 | 51, 54 | opeq12d 4792 |
. . . . . . . . . 10
⊢
((((1st ‘𝐴) ·N
(2nd ‘𝐵))
+N 𝑦) = ((1st ‘𝐵) ·N
(2nd ‘𝐴))
→ 〈(((1st ‘𝐴) ·N
((2nd ‘𝐴)
·N (2nd ‘𝐵))) +N (𝑦
·N (2nd ‘𝐴))), ((2nd ‘𝐴)
·N ((2nd ‘𝐴) ·N
(2nd ‘𝐵)))〉 = 〈(((2nd
‘𝐴)
·N (2nd ‘𝐴)) ·N
(1st ‘𝐵)),
(((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉) |
56 | 55 | eqeq2d 2748 |
. . . . . . . . 9
⊢
((((1st ‘𝐴) ·N
(2nd ‘𝐵))
+N 𝑦) = ((1st ‘𝐵) ·N
(2nd ‘𝐴))
→ ((𝐴
+pQ 〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉) = 〈(((1st
‘𝐴)
·N ((2nd ‘𝐴) ·N
(2nd ‘𝐵)))
+N (𝑦 ·N
(2nd ‘𝐴))), ((2nd ‘𝐴)
·N ((2nd ‘𝐴) ·N
(2nd ‘𝐵)))〉 ↔ (𝐴 +pQ 〈𝑦, ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉) = 〈(((2nd
‘𝐴)
·N (2nd ‘𝐴)) ·N
(1st ‘𝐵)),
(((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉)) |
57 | 35, 56 | syl5ibcom 248 |
. . . . . . . 8
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ((((1st ‘𝐴) ·N
(2nd ‘𝐵))
+N 𝑦) = ((1st ‘𝐵) ·N
(2nd ‘𝐴))
→ (𝐴
+pQ 〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉) = 〈(((2nd
‘𝐴)
·N (2nd ‘𝐴)) ·N
(1st ‘𝐵)),
(((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉)) |
58 | | fveq2 6717 |
. . . . . . . . 9
⊢ ((𝐴 +pQ
〈𝑦, ((2nd
‘𝐴)
·N (2nd ‘𝐵))〉) = 〈(((2nd
‘𝐴)
·N (2nd ‘𝐴)) ·N
(1st ‘𝐵)),
(((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉 →
([Q]‘(𝐴
+pQ 〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉)) =
([Q]‘〈(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)), (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉)) |
59 | | adderpq 10570 |
. . . . . . . . . . 11
⊢
(([Q]‘𝐴) +Q
([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉)) = ([Q]‘(𝐴 +pQ
〈𝑦, ((2nd
‘𝐴)
·N (2nd ‘𝐵))〉)) |
60 | | nqerid 10547 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Q →
([Q]‘𝐴)
= 𝐴) |
61 | 60 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ([Q]‘𝐴) = 𝐴) |
62 | 61 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (([Q]‘𝐴) +Q
([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉)) = (𝐴 +Q
([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉))) |
63 | 59, 62 | eqtr3id 2792 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ([Q]‘(𝐴 +pQ 〈𝑦, ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉)) = (𝐴 +Q
([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉))) |
64 | | mulclpi 10507 |
. . . . . . . . . . . . . . . 16
⊢
(((2nd ‘𝐴) ∈ N ∧
(2nd ‘𝐴)
∈ N) → ((2nd ‘𝐴) ·N
(2nd ‘𝐴))
∈ N) |
65 | 17, 17, 64 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((2nd ‘𝐴) ·N
(2nd ‘𝐴))
∈ N) |
66 | 65 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ((2nd ‘𝐴) ·N
(2nd ‘𝐴))
∈ N) |
67 | 15 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (1st ‘𝐵) ∈ N) |
68 | 11 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (2nd ‘𝐵) ∈ N) |
69 | | mulcanenq 10574 |
. . . . . . . . . . . . . 14
⊢
((((2nd ‘𝐴) ·N
(2nd ‘𝐴))
∈ N ∧ (1st ‘𝐵) ∈ N ∧
(2nd ‘𝐵)
∈ N) → 〈(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)), (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉 ~Q
〈(1st ‘𝐵), (2nd ‘𝐵)〉) |
70 | 66, 67, 68, 69 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 〈(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)), (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉 ~Q
〈(1st ‘𝐵), (2nd ‘𝐵)〉) |
71 | 8 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 𝐵
∈ (N × N)) |
72 | | 1st2nd 7810 |
. . . . . . . . . . . . . 14
⊢ ((Rel
(N × N) ∧ 𝐵 ∈ (N ×
N)) → 𝐵
= 〈(1st ‘𝐵), (2nd ‘𝐵)〉) |
73 | 22, 71, 72 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 𝐵 =
〈(1st ‘𝐵), (2nd ‘𝐵)〉) |
74 | 70, 73 | breqtrrd 5081 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 〈(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)), (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉 ~Q 𝐵) |
75 | | mulclpi 10507 |
. . . . . . . . . . . . . . 15
⊢
((((2nd ‘𝐴) ·N
(2nd ‘𝐴))
∈ N ∧ (1st ‘𝐵) ∈ N) →
(((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(1st ‘𝐵))
∈ N) |
76 | 66, 67, 75 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)) ∈ N) |
77 | | mulclpi 10507 |
. . . . . . . . . . . . . . 15
⊢
((((2nd ‘𝐴) ·N
(2nd ‘𝐴))
∈ N ∧ (2nd ‘𝐵) ∈ N) →
(((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))
∈ N) |
78 | 66, 68, 77 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (2nd ‘𝐵)) ∈ N) |
79 | 76, 78 | opelxpd 5589 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → 〈(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)), (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉 ∈ (N ×
N)) |
80 | | nqereq 10549 |
. . . . . . . . . . . . 13
⊢
((〈(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)), (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
(〈(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)), (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉 ~Q 𝐵 ↔
([Q]‘〈(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)), (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉) = ([Q]‘𝐵))) |
81 | 79, 71, 80 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (〈(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)), (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉 ~Q 𝐵 ↔
([Q]‘〈(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)), (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉) = ([Q]‘𝐵))) |
82 | 74, 81 | mpbid 235 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ([Q]‘〈(((2nd
‘𝐴)
·N (2nd ‘𝐴)) ·N
(1st ‘𝐵)),
(((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉) = ([Q]‘𝐵)) |
83 | | nqerid 10547 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ Q →
([Q]‘𝐵)
= 𝐵) |
84 | 83 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ([Q]‘𝐵) = 𝐵) |
85 | 82, 84 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ([Q]‘〈(((2nd
‘𝐴)
·N (2nd ‘𝐴)) ·N
(1st ‘𝐵)),
(((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉) = 𝐵) |
86 | 63, 85 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → (([Q]‘(𝐴 +pQ 〈𝑦, ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉)) =
([Q]‘〈(((2nd ‘𝐴) ·N
(2nd ‘𝐴))
·N (1st ‘𝐵)), (((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉) ↔ (𝐴 +Q
([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉)) = 𝐵)) |
87 | 58, 86 | syl5ib 247 |
. . . . . . . 8
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ((𝐴
+pQ 〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉) = 〈(((2nd
‘𝐴)
·N (2nd ‘𝐴)) ·N
(1st ‘𝐵)),
(((2nd ‘𝐴)
·N (2nd ‘𝐴)) ·N
(2nd ‘𝐵))〉 → (𝐴 +Q
([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉)) = 𝐵)) |
88 | 57, 87 | syld 47 |
. . . . . . 7
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ((((1st ‘𝐴) ·N
(2nd ‘𝐵))
+N 𝑦) = ((1st ‘𝐵) ·N
(2nd ‘𝐴))
→ (𝐴
+Q ([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉)) = 𝐵)) |
89 | | fvex 6730 |
. . . . . . . 8
⊢
([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉) ∈ V |
90 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑥 =
([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉) → (𝐴 +Q 𝑥) = (𝐴 +Q
([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉))) |
91 | 90 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑥 =
([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉) → ((𝐴 +Q 𝑥) = 𝐵 ↔ (𝐴 +Q
([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉)) = 𝐵)) |
92 | 89, 91 | spcev 3521 |
. . . . . . 7
⊢ ((𝐴 +Q
([Q]‘〈𝑦, ((2nd ‘𝐴) ·N
(2nd ‘𝐵))〉)) = 𝐵 → ∃𝑥(𝐴 +Q 𝑥) = 𝐵) |
93 | 88, 92 | syl6 35 |
. . . . . 6
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑦 ∈
N) → ((((1st ‘𝐴) ·N
(2nd ‘𝐵))
+N 𝑦) = ((1st ‘𝐵) ·N
(2nd ‘𝐴))
→ ∃𝑥(𝐴 +Q
𝑥) = 𝐵)) |
94 | 93 | rexlimdva 3203 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (∃𝑦 ∈
N (((1st ‘𝐴) ·N
(2nd ‘𝐵))
+N 𝑦) = ((1st ‘𝐵) ·N
(2nd ‘𝐴))
→ ∃𝑥(𝐴 +Q
𝑥) = 𝐵)) |
95 | 21, 94 | sylbid 243 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
→ ∃𝑥(𝐴 +Q
𝑥) = 𝐵)) |
96 | 3, 95 | sylbid 243 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<Q 𝐵 → ∃𝑥(𝐴 +Q 𝑥) = 𝐵)) |
97 | 2, 96 | mpcom 38 |
. 2
⊢ (𝐴 <Q
𝐵 → ∃𝑥(𝐴 +Q 𝑥) = 𝐵) |
98 | | eleq1 2825 |
. . . . . . 7
⊢ ((𝐴 +Q
𝑥) = 𝐵 → ((𝐴 +Q 𝑥) ∈ Q ↔
𝐵 ∈
Q)) |
99 | 98 | biimparc 483 |
. . . . . 6
⊢ ((𝐵 ∈ Q ∧
(𝐴
+Q 𝑥) = 𝐵) → (𝐴 +Q 𝑥) ∈
Q) |
100 | | addnqf 10562 |
. . . . . . . 8
⊢
+Q :(Q ×
Q)⟶Q |
101 | 100 | fdmi 6557 |
. . . . . . 7
⊢ dom
+Q = (Q ×
Q) |
102 | | 0nnq 10538 |
. . . . . . 7
⊢ ¬
∅ ∈ Q |
103 | 101, 102 | ndmovrcl 7394 |
. . . . . 6
⊢ ((𝐴 +Q
𝑥) ∈ Q
→ (𝐴 ∈
Q ∧ 𝑥
∈ Q)) |
104 | | ltaddnq 10588 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝑥 ∈ Q)
→ 𝐴
<Q (𝐴 +Q 𝑥)) |
105 | 99, 103, 104 | 3syl 18 |
. . . . 5
⊢ ((𝐵 ∈ Q ∧
(𝐴
+Q 𝑥) = 𝐵) → 𝐴 <Q (𝐴 +Q
𝑥)) |
106 | | simpr 488 |
. . . . 5
⊢ ((𝐵 ∈ Q ∧
(𝐴
+Q 𝑥) = 𝐵) → (𝐴 +Q 𝑥) = 𝐵) |
107 | 105, 106 | breqtrd 5079 |
. . . 4
⊢ ((𝐵 ∈ Q ∧
(𝐴
+Q 𝑥) = 𝐵) → 𝐴 <Q 𝐵) |
108 | 107 | ex 416 |
. . 3
⊢ (𝐵 ∈ Q →
((𝐴
+Q 𝑥) = 𝐵 → 𝐴 <Q 𝐵)) |
109 | 108 | exlimdv 1941 |
. 2
⊢ (𝐵 ∈ Q →
(∃𝑥(𝐴 +Q 𝑥) = 𝐵 → 𝐴 <Q 𝐵)) |
110 | 97, 109 | impbid2 229 |
1
⊢ (𝐵 ∈ Q →
(𝐴
<Q 𝐵 ↔ ∃𝑥(𝐴 +Q 𝑥) = 𝐵)) |