Metamath Proof Explorer


Theorem ltanq

Description: Ordering property of addition for positive fractions. Proposition 9-2.6(ii) of Gleason p. 120. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

Ref Expression
Assertion ltanq ( 𝐶Q → ( 𝐴 <Q 𝐵 ↔ ( 𝐶 +Q 𝐴 ) <Q ( 𝐶 +Q 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 addnqf +Q : ( Q × Q ) ⟶ Q
2 1 fdmi dom +Q = ( Q × Q )
3 ltrelnq <Q ⊆ ( Q × Q )
4 0nnq ¬ ∅ ∈ Q
5 ordpinq ( ( 𝐴Q𝐵Q ) → ( 𝐴 <Q 𝐵 ↔ ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) <N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) )
6 5 3adant3 ( ( 𝐴Q𝐵Q𝐶Q ) → ( 𝐴 <Q 𝐵 ↔ ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) <N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) )
7 elpqn ( 𝐶Q𝐶 ∈ ( N × N ) )
8 7 3ad2ant3 ( ( 𝐴Q𝐵Q𝐶Q ) → 𝐶 ∈ ( N × N ) )
9 elpqn ( 𝐴Q𝐴 ∈ ( N × N ) )
10 9 3ad2ant1 ( ( 𝐴Q𝐵Q𝐶Q ) → 𝐴 ∈ ( N × N ) )
11 addpipq2 ( ( 𝐶 ∈ ( N × N ) ∧ 𝐴 ∈ ( N × N ) ) → ( 𝐶 +pQ 𝐴 ) = ⟨ ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) +N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) , ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ⟩ )
12 8 10 11 syl2anc ( ( 𝐴Q𝐵Q𝐶Q ) → ( 𝐶 +pQ 𝐴 ) = ⟨ ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) +N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) , ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ⟩ )
13 elpqn ( 𝐵Q𝐵 ∈ ( N × N ) )
14 13 3ad2ant2 ( ( 𝐴Q𝐵Q𝐶Q ) → 𝐵 ∈ ( N × N ) )
15 addpipq2 ( ( 𝐶 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐶 +pQ 𝐵 ) = ⟨ ( ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) +N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) , ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ⟩ )
16 8 14 15 syl2anc ( ( 𝐴Q𝐵Q𝐶Q ) → ( 𝐶 +pQ 𝐵 ) = ⟨ ( ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) +N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) , ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ⟩ )
17 12 16 breq12d ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( 𝐶 +pQ 𝐴 ) <pQ ( 𝐶 +pQ 𝐵 ) ↔ ⟨ ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) +N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) , ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ⟩ <pQ ⟨ ( ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) +N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) , ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ⟩ ) )
18 addpqnq ( ( 𝐶Q𝐴Q ) → ( 𝐶 +Q 𝐴 ) = ( [Q] ‘ ( 𝐶 +pQ 𝐴 ) ) )
19 18 ancoms ( ( 𝐴Q𝐶Q ) → ( 𝐶 +Q 𝐴 ) = ( [Q] ‘ ( 𝐶 +pQ 𝐴 ) ) )
20 19 3adant2 ( ( 𝐴Q𝐵Q𝐶Q ) → ( 𝐶 +Q 𝐴 ) = ( [Q] ‘ ( 𝐶 +pQ 𝐴 ) ) )
21 addpqnq ( ( 𝐶Q𝐵Q ) → ( 𝐶 +Q 𝐵 ) = ( [Q] ‘ ( 𝐶 +pQ 𝐵 ) ) )
22 21 ancoms ( ( 𝐵Q𝐶Q ) → ( 𝐶 +Q 𝐵 ) = ( [Q] ‘ ( 𝐶 +pQ 𝐵 ) ) )
23 22 3adant1 ( ( 𝐴Q𝐵Q𝐶Q ) → ( 𝐶 +Q 𝐵 ) = ( [Q] ‘ ( 𝐶 +pQ 𝐵 ) ) )
24 20 23 breq12d ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( 𝐶 +Q 𝐴 ) <Q ( 𝐶 +Q 𝐵 ) ↔ ( [Q] ‘ ( 𝐶 +pQ 𝐴 ) ) <Q ( [Q] ‘ ( 𝐶 +pQ 𝐵 ) ) ) )
25 lterpq ( ( 𝐶 +pQ 𝐴 ) <pQ ( 𝐶 +pQ 𝐵 ) ↔ ( [Q] ‘ ( 𝐶 +pQ 𝐴 ) ) <Q ( [Q] ‘ ( 𝐶 +pQ 𝐵 ) ) )
26 24 25 bitr4di ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( 𝐶 +Q 𝐴 ) <Q ( 𝐶 +Q 𝐵 ) ↔ ( 𝐶 +pQ 𝐴 ) <pQ ( 𝐶 +pQ 𝐵 ) ) )
27 xp2nd ( 𝐶 ∈ ( N × N ) → ( 2nd𝐶 ) ∈ N )
28 8 27 syl ( ( 𝐴Q𝐵Q𝐶Q ) → ( 2nd𝐶 ) ∈ N )
29 mulclpi ( ( ( 2nd𝐶 ) ∈ N ∧ ( 2nd𝐶 ) ∈ N ) → ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ∈ N )
30 28 28 29 syl2anc ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ∈ N )
31 ltmpi ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ∈ N → ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) <N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ↔ ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) <N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ) )
32 30 31 syl ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) <N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ↔ ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) <N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ) )
33 xp2nd ( 𝐵 ∈ ( N × N ) → ( 2nd𝐵 ) ∈ N )
34 14 33 syl ( ( 𝐴Q𝐵Q𝐶Q ) → ( 2nd𝐵 ) ∈ N )
35 mulclpi ( ( ( 2nd𝐶 ) ∈ N ∧ ( 2nd𝐵 ) ∈ N ) → ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ∈ N )
36 28 34 35 syl2anc ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ∈ N )
37 xp1st ( 𝐶 ∈ ( N × N ) → ( 1st𝐶 ) ∈ N )
38 8 37 syl ( ( 𝐴Q𝐵Q𝐶Q ) → ( 1st𝐶 ) ∈ N )
39 xp2nd ( 𝐴 ∈ ( N × N ) → ( 2nd𝐴 ) ∈ N )
40 10 39 syl ( ( 𝐴Q𝐵Q𝐶Q ) → ( 2nd𝐴 ) ∈ N )
41 mulclpi ( ( ( 1st𝐶 ) ∈ N ∧ ( 2nd𝐴 ) ∈ N ) → ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ∈ N )
42 38 40 41 syl2anc ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ∈ N )
43 mulclpi ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ∈ N ∧ ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ∈ N ) → ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) ∈ N )
44 36 42 43 syl2anc ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) ∈ N )
45 ltapi ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) ∈ N → ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) <N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ↔ ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) ) <N ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ) ) )
46 44 45 syl ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) <N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ↔ ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) ) <N ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ) ) )
47 32 46 bitrd ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) <N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ↔ ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) ) <N ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ) ) )
48 mulcompi ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) = ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) )
49 fvex ( 1st𝐴 ) ∈ V
50 fvex ( 2nd𝐵 ) ∈ V
51 fvex ( 2nd𝐶 ) ∈ V
52 mulcompi ( 𝑥 ·N 𝑦 ) = ( 𝑦 ·N 𝑥 )
53 mulasspi ( ( 𝑥 ·N 𝑦 ) ·N 𝑧 ) = ( 𝑥 ·N ( 𝑦 ·N 𝑧 ) )
54 49 50 51 52 53 51 caov411 ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ) = ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) )
55 48 54 eqtri ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) = ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) )
56 55 oveq2i ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) ) = ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) )
57 distrpi ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) +N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) ) = ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) )
58 mulcompi ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) +N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) ) = ( ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) +N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) )
59 56 57 58 3eqtr2i ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) ) = ( ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) +N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) )
60 mulcompi ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) = ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) )
61 fvex ( 1st𝐶 ) ∈ V
62 fvex ( 2nd𝐴 ) ∈ V
63 61 62 51 52 53 50 caov411 ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ) = ( ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) )
64 60 63 eqtri ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) = ( ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) )
65 mulcompi ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) = ( ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) )
66 fvex ( 1st𝐵 ) ∈ V
67 66 62 51 52 53 51 caov411 ( ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ) = ( ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) )
68 65 67 eqtri ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) = ( ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) )
69 64 68 oveq12i ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ) = ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) )
70 distrpi ( ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ·N ( ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) +N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) ) = ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) )
71 mulcompi ( ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ·N ( ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) +N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) ) = ( ( ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) +N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) )
72 69 70 71 3eqtr2i ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ) = ( ( ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) +N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) )
73 59 72 breq12i ( ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) ) <N ( ( ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) ) +N ( ( ( 2nd𝐶 ) ·N ( 2nd𝐶 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ) ↔ ( ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) +N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ) <N ( ( ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) +N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ) )
74 47 73 bitrdi ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) <N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ↔ ( ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) +N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ) <N ( ( ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) +N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ) ) )
75 ordpipq ( ⟨ ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) +N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) , ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ⟩ <pQ ⟨ ( ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) +N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) , ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ⟩ ↔ ( ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) +N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ) <N ( ( ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) +N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) ·N ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ) )
76 74 75 bitr4di ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) <N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ↔ ⟨ ( ( ( 1st𝐶 ) ·N ( 2nd𝐴 ) ) +N ( ( 1st𝐴 ) ·N ( 2nd𝐶 ) ) ) , ( ( 2nd𝐶 ) ·N ( 2nd𝐴 ) ) ⟩ <pQ ⟨ ( ( ( 1st𝐶 ) ·N ( 2nd𝐵 ) ) +N ( ( 1st𝐵 ) ·N ( 2nd𝐶 ) ) ) , ( ( 2nd𝐶 ) ·N ( 2nd𝐵 ) ) ⟩ ) )
77 17 26 76 3bitr4rd ( ( 𝐴Q𝐵Q𝐶Q ) → ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) <N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ↔ ( 𝐶 +Q 𝐴 ) <Q ( 𝐶 +Q 𝐵 ) ) )
78 6 77 bitrd ( ( 𝐴Q𝐵Q𝐶Q ) → ( 𝐴 <Q 𝐵 ↔ ( 𝐶 +Q 𝐴 ) <Q ( 𝐶 +Q 𝐵 ) ) )
79 2 3 4 78 ndmovord ( 𝐶Q → ( 𝐴 <Q 𝐵 ↔ ( 𝐶 +Q 𝐴 ) <Q ( 𝐶 +Q 𝐵 ) ) )