Step | Hyp | Ref
| Expression |
1 | | addnqf 10023 |
. . 3
⊢
+_{Q} :(Q ×
Q)⟶Q |
2 | 1 | fdmi 6233 |
. 2
⊢ dom
+_{Q} = (Q ×
Q) |
3 | | ltrelnq 10001 |
. 2
⊢
<_{Q} ⊆ (Q ×
Q) |
4 | | 0nnq 9999 |
. 2
⊢ ¬
∅ ∈ Q |
5 | | ordpinq 10018 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<_{Q} 𝐵 ↔ ((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) <_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴)))) |
6 | 5 | 3adant3 1162 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
<_{Q} 𝐵 ↔ ((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) <_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴)))) |
7 | | elpqn 10000 |
. . . . . . 7
⊢ (𝐶 ∈ Q →
𝐶 ∈ (N
× N)) |
8 | 7 | 3ad2ant3 1165 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐶
∈ (N × N)) |
9 | | elpqn 10000 |
. . . . . . 7
⊢ (𝐴 ∈ Q →
𝐴 ∈ (N
× N)) |
10 | 9 | 3ad2ant1 1163 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴
∈ (N × N)) |
11 | | addpipq2 10011 |
. . . . . 6
⊢ ((𝐶 ∈ (N ×
N) ∧ 𝐴
∈ (N × N)) → (𝐶 +_{pQ} 𝐴) = ⟨(((1^{st}
‘𝐶)
·_{N} (2^{nd} ‘𝐴)) +_{N}
((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))), ((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐴))⟩) |
12 | 8, 10, 11 | syl2anc 579 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
+_{pQ} 𝐴) = ⟨(((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐴)) +_{N}
((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))), ((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐴))⟩) |
13 | | elpqn 10000 |
. . . . . . 7
⊢ (𝐵 ∈ Q →
𝐵 ∈ (N
× N)) |
14 | 13 | 3ad2ant2 1164 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐵
∈ (N × N)) |
15 | | addpipq2 10011 |
. . . . . 6
⊢ ((𝐶 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐶 +_{pQ} 𝐵) = ⟨(((1^{st}
‘𝐶)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))), ((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))⟩) |
16 | 8, 14, 15 | syl2anc 579 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
+_{pQ} 𝐵) = ⟨(((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))), ((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))⟩) |
17 | 12, 16 | breq12d 4822 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐶
+_{pQ} 𝐴) <_{pQ} (𝐶 +_{pQ}
𝐵) ↔
⟨(((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
+_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶))), ((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐴))⟩ <_{pQ}
⟨(((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))), ((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))⟩)) |
18 | | addpqnq 10013 |
. . . . . . . 8
⊢ ((𝐶 ∈ Q ∧
𝐴 ∈ Q)
→ (𝐶
+_{Q} 𝐴) = ([Q]‘(𝐶 +_{pQ}
𝐴))) |
19 | 18 | ancoms 450 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐶
+_{Q} 𝐴) = ([Q]‘(𝐶 +_{pQ}
𝐴))) |
20 | 19 | 3adant2 1161 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
+_{Q} 𝐴) = ([Q]‘(𝐶 +_{pQ}
𝐴))) |
21 | | addpqnq 10013 |
. . . . . . . 8
⊢ ((𝐶 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐶
+_{Q} 𝐵) = ([Q]‘(𝐶 +_{pQ}
𝐵))) |
22 | 21 | ancoms 450 |
. . . . . . 7
⊢ ((𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐶
+_{Q} 𝐵) = ([Q]‘(𝐶 +_{pQ}
𝐵))) |
23 | 22 | 3adant1 1160 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
+_{Q} 𝐵) = ([Q]‘(𝐶 +_{pQ}
𝐵))) |
24 | 20, 23 | breq12d 4822 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐶
+_{Q} 𝐴) <_{Q} (𝐶 +_{Q}
𝐵) ↔
([Q]‘(𝐶
+_{pQ} 𝐴)) <_{Q}
([Q]‘(𝐶
+_{pQ} 𝐵)))) |
25 | | lterpq 10045 |
. . . . 5
⊢ ((𝐶 +_{pQ}
𝐴)
<_{pQ} (𝐶 +_{pQ} 𝐵) ↔
([Q]‘(𝐶
+_{pQ} 𝐴)) <_{Q}
([Q]‘(𝐶
+_{pQ} 𝐵))) |
26 | 24, 25 | syl6bbr 280 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐶
+_{Q} 𝐴) <_{Q} (𝐶 +_{Q}
𝐵) ↔ (𝐶 +_{pQ}
𝐴)
<_{pQ} (𝐶 +_{pQ} 𝐵))) |
27 | | xp2nd 7399 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (N ×
N) → (2^{nd} ‘𝐶) ∈ N) |
28 | 8, 27 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2^{nd} ‘𝐶) ∈ N) |
29 | | mulclpi 9968 |
. . . . . . . . 9
⊢
(((2^{nd} ‘𝐶) ∈ N ∧
(2^{nd} ‘𝐶)
∈ N) → ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
∈ N) |
30 | 28, 28, 29 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
∈ N) |
31 | | ltmpi 9979 |
. . . . . . . 8
⊢
(((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
∈ N → (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
<_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
↔ (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
<_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))))) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
<_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
↔ (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
<_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))))) |
33 | | xp2nd 7399 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (N ×
N) → (2^{nd} ‘𝐵) ∈ N) |
34 | 14, 33 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2^{nd} ‘𝐵) ∈ N) |
35 | | mulclpi 9968 |
. . . . . . . . . 10
⊢
(((2^{nd} ‘𝐶) ∈ N ∧
(2^{nd} ‘𝐵)
∈ N) → ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
36 | 28, 34, 35 | syl2anc 579 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
37 | | xp1st 7398 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (N ×
N) → (1^{st} ‘𝐶) ∈ N) |
38 | 8, 37 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1^{st} ‘𝐶) ∈ N) |
39 | | xp2nd 7399 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (N ×
N) → (2^{nd} ‘𝐴) ∈ N) |
40 | 10, 39 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2^{nd} ‘𝐴) ∈ N) |
41 | | mulclpi 9968 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝐶) ∈ N ∧
(2^{nd} ‘𝐴)
∈ N) → ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
∈ N) |
42 | 38, 40, 41 | syl2anc 579 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
∈ N) |
43 | | mulclpi 9968 |
. . . . . . . . 9
⊢
((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
∈ N ∧ ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
∈ N) → (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
∈ N) |
44 | 36, 42, 43 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
∈ N) |
45 | | ltapi 9978 |
. . . . . . . 8
⊢
((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
∈ N → ((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
<_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))
↔ ((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
+_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))) <_{N}
((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
+_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))))) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
<_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))
↔ ((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
+_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))) <_{N}
((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
+_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))))) |
47 | 32, 46 | bitrd 270 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
<_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
↔ ((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
+_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))) <_{N}
((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
+_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))))) |
48 | | mulcompi 9971 |
. . . . . . . . . 10
⊢
(((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
= (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))) |
49 | | fvex 6388 |
. . . . . . . . . . 11
⊢
(1^{st} ‘𝐴) ∈ V |
50 | | fvex 6388 |
. . . . . . . . . . 11
⊢
(2^{nd} ‘𝐵) ∈ V |
51 | | fvex 6388 |
. . . . . . . . . . 11
⊢
(2^{nd} ‘𝐶) ∈ V |
52 | | mulcompi 9971 |
. . . . . . . . . . 11
⊢ (𝑥
·_{N} 𝑦) = (𝑦 ·_{N} 𝑥) |
53 | | mulasspi 9972 |
. . . . . . . . . . 11
⊢ ((𝑥
·_{N} 𝑦) ·_{N} 𝑧) = (𝑥 ·_{N} (𝑦
·_{N} 𝑧)) |
54 | 49, 50, 51, 52, 53, 51 | caov411 7064 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶)))
= (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶))) |
55 | 48, 54 | eqtri 2787 |
. . . . . . . . 9
⊢
(((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
= (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶))) |
56 | 55 | oveq2i 6853 |
. . . . . . . 8
⊢
((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
+_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))) = ((((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐴))) +_{N}
(((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐶)))) |
57 | | distrpi 9973 |
. . . . . . . 8
⊢
(((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} (((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
+_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))) = ((((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐴))) +_{N}
(((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐶)))) |
58 | | mulcompi 9971 |
. . . . . . . 8
⊢
(((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} (((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
+_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))) = ((((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐴)) +_{N}
((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))) ·_{N}
((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))) |
59 | 56, 57, 58 | 3eqtr2i 2793 |
. . . . . . 7
⊢
((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
+_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))) = ((((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐴)) +_{N}
((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))) ·_{N}
((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))) |
60 | | mulcompi 9971 |
. . . . . . . . . 10
⊢
(((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
= (((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
·_{N} ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))) |
61 | | fvex 6388 |
. . . . . . . . . . 11
⊢
(1^{st} ‘𝐶) ∈ V |
62 | | fvex 6388 |
. . . . . . . . . . 11
⊢
(2^{nd} ‘𝐴) ∈ V |
63 | 61, 62, 51, 52, 53, 50 | caov411 7064 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
·_{N} ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
= (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))) |
64 | 60, 63 | eqtri 2787 |
. . . . . . . . 9
⊢
(((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
= (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))) |
65 | | mulcompi 9971 |
. . . . . . . . . 10
⊢
(((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))
= (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
·_{N} ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))) |
66 | | fvex 6388 |
. . . . . . . . . . 11
⊢
(1^{st} ‘𝐵) ∈ V |
67 | 66, 62, 51, 52, 53, 51 | caov411 7064 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
·_{N} ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶)))
= (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))) |
68 | 65, 67 | eqtri 2787 |
. . . . . . . . 9
⊢
(((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))
= (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))) |
69 | 64, 68 | oveq12i 6854 |
. . . . . . . 8
⊢
((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
+_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))) = ((((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))) +_{N}
(((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)))) |
70 | | distrpi 9973 |
. . . . . . . 8
⊢
(((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))) = ((((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))) +_{N}
(((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)))) |
71 | | mulcompi 9971 |
. . . . . . . 8
⊢
(((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))) = ((((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))) ·_{N}
((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐴))) |
72 | 69, 70, 71 | 3eqtr2i 2793 |
. . . . . . 7
⊢
((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
+_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))) = ((((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))) ·_{N}
((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐴))) |
73 | 59, 72 | breq12i 4818 |
. . . . . 6
⊢
(((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
+_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))) <_{N}
((((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))
+_{N} (((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐶))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))) ↔ ((((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐴)) +_{N}
((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))) ·_{N}
((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))) <_{N}
((((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
·_{N} ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))) |
74 | 47, 73 | syl6bb 278 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
<_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
↔ ((((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
+_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))
·_{N} ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
<_{N} ((((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
·_{N} ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))))) |
75 | | ordpipq 10017 |
. . . . 5
⊢
(⟨(((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
+_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶))), ((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐴))⟩ <_{pQ}
⟨(((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))), ((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))⟩ ↔ ((((1^{st}
‘𝐶)
·_{N} (2^{nd} ‘𝐴)) +_{N}
((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))) ·_{N}
((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))) <_{N}
((((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
·_{N} ((2^{nd} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴)))) |
76 | 74, 75 | syl6bbr 280 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
<_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
↔ ⟨(((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐴))
+_{N} ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶))), ((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐴))⟩ <_{pQ}
⟨(((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))), ((2^{nd} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))⟩)) |
77 | 17, 26, 76 | 3bitr4rd 303 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
<_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
↔ (𝐶
+_{Q} 𝐴) <_{Q} (𝐶 +_{Q}
𝐵))) |
78 | 6, 77 | bitrd 270 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
<_{Q} 𝐵 ↔ (𝐶 +_{Q} 𝐴) <_{Q}
(𝐶
+_{Q} 𝐵))) |
79 | 2, 3, 4, 78 | ndmovord 7022 |
1
⊢ (𝐶 ∈ Q →
(𝐴
<_{Q} 𝐵 ↔ (𝐶 +_{Q} 𝐴) <_{Q}
(𝐶
+_{Q} 𝐵))) |