This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐵 ) ) )