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	syl6bbr	⊢ ( ( 𝐴 ∈ 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	syl6bb	⊢ ( ( 𝐴 ∈ 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	syl6bbr	⊢ ( ( 𝐴 ∈ 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 𝐵 ) ) )