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	$⊢ C \in 𝑸 \to (A <_{𝑸} B \leftrightarrow (C +_{𝑸} A) <_{𝑸} (C +_{𝑸} B))$

Proof

Step	Hyp	Ref	Expression
1		addnqf	$⊢ +_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
2	1	fdmi	$⊢ dom +_{𝑸} = 𝑸 \times 𝑸$
3		ltrelnq	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸$
4		0nnq	$⊢ \neg \emptyset \in 𝑸$
5		ordpinq	$⊢ (A \in 𝑸 \land B \in 𝑸) \to (A <_{𝑸} B \leftrightarrow (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))$
6	5	3adant3	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (A <_{𝑸} B \leftrightarrow (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))$
7		elpqn	$⊢ C \in 𝑸 \to C \in (𝑵 \times 𝑵)$
8	7	3ad2ant3	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to C \in (𝑵 \times 𝑵)$
9		elpqn	$⊢ A \in 𝑸 \to A \in (𝑵 \times 𝑵)$
10	9	3ad2ant1	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \in (𝑵 \times 𝑵)$
11		addpipq2	$⊢ (C \in (𝑵 \times 𝑵) \land A \in (𝑵 \times 𝑵)) \to C +_{𝑝𝑸} A = ⟨(1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C)), 2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)⟩$
12	8 10 11	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to C +_{𝑝𝑸} A = ⟨(1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C)), 2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)⟩$
13		elpqn	$⊢ B \in 𝑸 \to B \in (𝑵 \times 𝑵)$
14	13	3ad2ant2	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to B \in (𝑵 \times 𝑵)$
15		addpipq2	$⊢ (C \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to C +_{𝑝𝑸} B = ⟨(1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)), 2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)⟩$
16	8 14 15	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to C +_{𝑝𝑸} B = ⟨(1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)), 2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)⟩$
17	12 16	breq12d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ((C +_{𝑝𝑸} A) <_{𝑝𝑸} (C +_{𝑝𝑸} B) \leftrightarrow ⟨(1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C)), 2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)⟩ <_{𝑝𝑸} ⟨(1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)), 2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)⟩)$
18		addpqnq	$⊢ (C \in 𝑸 \land A \in 𝑸) \to C +_{𝑸} A = /_{𝑸} (C +_{𝑝𝑸} A)$
19	18	ancoms	$⊢ (A \in 𝑸 \land C \in 𝑸) \to C +_{𝑸} A = /_{𝑸} (C +_{𝑝𝑸} A)$
20	19	3adant2	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to C +_{𝑸} A = /_{𝑸} (C +_{𝑝𝑸} A)$
21		addpqnq	$⊢ (C \in 𝑸 \land B \in 𝑸) \to C +_{𝑸} B = /_{𝑸} (C +_{𝑝𝑸} B)$
22	21	ancoms	$⊢ (B \in 𝑸 \land C \in 𝑸) \to C +_{𝑸} B = /_{𝑸} (C +_{𝑝𝑸} B)$
23	22	3adant1	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to C +_{𝑸} B = /_{𝑸} (C +_{𝑝𝑸} B)$
24	20 23	breq12d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ((C +_{𝑸} A) <_{𝑸} (C +_{𝑸} B) \leftrightarrow /_{𝑸} (C +_{𝑝𝑸} A) <_{𝑸} /_{𝑸} (C +_{𝑝𝑸} B))$
25		lterpq	$⊢ (C +_{𝑝𝑸} A) <_{𝑝𝑸} (C +_{𝑝𝑸} B) \leftrightarrow /_{𝑸} (C +_{𝑝𝑸} A) <_{𝑸} /_{𝑸} (C +_{𝑝𝑸} B)$
26	24 25	syl6bbr	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ((C +_{𝑸} A) <_{𝑸} (C +_{𝑸} B) \leftrightarrow (C +_{𝑝𝑸} A) <_{𝑝𝑸} (C +_{𝑝𝑸} B))$
27		xp2nd	$⊢ C \in (𝑵 \times 𝑵) \to 2^{nd} (C) \in 𝑵$
28	8 27	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (C) \in 𝑵$
29		mulclpi	$⊢ (2^{nd} (C) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 2^{nd} (C) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
30	28 28 29	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (C) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
31		ltmpi	$⊢ 2^{nd} (C) \cdot_{𝑵} 2^{nd} (C) \in 𝑵 \to ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) <_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))))$
32	30 31	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) <_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))))$
33		xp2nd	$⊢ B \in (𝑵 \times 𝑵) \to 2^{nd} (B) \in 𝑵$
34	14 33	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (B) \in 𝑵$
35		mulclpi	$⊢ (2^{nd} (C) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to 2^{nd} (C) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
36	28 34 35	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (C) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
37		xp1st	$⊢ C \in (𝑵 \times 𝑵) \to 1^{st} (C) \in 𝑵$
38	8 37	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (C) \in 𝑵$
39		xp2nd	$⊢ A \in (𝑵 \times 𝑵) \to 2^{nd} (A) \in 𝑵$
40	10 39	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (A) \in 𝑵$
41		mulclpi	$⊢ (1^{st} (C) \in 𝑵 \land 2^{nd} (A) \in 𝑵) \to 1^{st} (C) \cdot_{𝑵} 2^{nd} (A) \in 𝑵$
42	38 40 41	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (C) \cdot_{𝑵} 2^{nd} (A) \in 𝑵$
43		mulclpi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B) \in 𝑵 \land 1^{st} (C) \cdot_{𝑵} 2^{nd} (A) \in 𝑵) \to (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) \in 𝑵$
44	36 42 43	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) \in 𝑵$
45		ltapi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) \in 𝑵 \to (((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) <_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \leftrightarrow (((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)))) <_{𝑵} (((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))))$
46	44 45	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) <_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \leftrightarrow (((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)))) <_{𝑵} (((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))))$
47	32 46	bitrd	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow (((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)))) <_{𝑵} (((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))))$
48		mulcompi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C))$
49		fvex	$⊢ 1^{st} (A) \in V$
50		fvex	$⊢ 2^{nd} (B) \in V$
51		fvex	$⊢ 2^{nd} (C) \in V$
52		mulcompi	$⊢ x \cdot_{𝑵} y = y \cdot_{𝑵} x$
53		mulasspi	$⊢ (x \cdot_{𝑵} y) \cdot_{𝑵} z = x \cdot_{𝑵} (y \cdot_{𝑵} z)$
54	49 50 51 52 53 51	caov411	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C))$
55	48 54	eqtri	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C))$
56	55	oveq2i	$⊢ ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) = ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C)))$
57		distrpi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} ((1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C))) = ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C)))$
58		mulcompi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} ((1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C))) = ((1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C))) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B))$
59	56 57 58	3eqtr2i	$⊢ ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) = ((1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C))) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B))$
60		mulcompi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) = (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B))$
61		fvex	$⊢ 1^{st} (C) \in V$
62		fvex	$⊢ 2^{nd} (A) \in V$
63	61 62 51 52 53 50	caov411	$⊢ (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) = (2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))$
64	60 63	eqtri	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) = (2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))$
65		mulcompi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) = (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C))$
66		fvex	$⊢ 1^{st} (B) \in V$
67	66 62 51 52 53 51	caov411	$⊢ (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))$
68	65 67	eqtri	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) = (2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))$
69	64 68	oveq12i	$⊢ ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) = ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)))$
70		distrpi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} ((1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))) = ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)))$
71		mulcompi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} ((1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))) = ((1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (A))$
72	69 70 71	3eqtr2i	$⊢ ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) = ((1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (A))$
73	59 72	breq12i	$⊢ (((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)))) <_{𝑵} (((2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))) \leftrightarrow (((1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C))) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B))) <_{𝑵} (((1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)))$
74	47 73	syl6bb	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow (((1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C))) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B))) <_{𝑵} (((1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (A))))$
75		ordpipq	$⊢ ⟨(1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C)), 2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)⟩ <_{𝑝𝑸} ⟨(1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)), 2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)⟩ \leftrightarrow (((1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C))) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B))) <_{𝑵} (((1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)))$
76	74 75	syl6bbr	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow ⟨(1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (C)), 2^{nd} (C) \cdot_{𝑵} 2^{nd} (A)⟩ <_{𝑝𝑸} ⟨(1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)), 2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)⟩)$
77	17 26 76	3bitr4rd	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow (C +_{𝑸} A) <_{𝑸} (C +_{𝑸} B))$
78	6 77	bitrd	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (A <_{𝑸} B \leftrightarrow (C +_{𝑸} A) <_{𝑸} (C +_{𝑸} B))$
79	2 3 4 78	ndmovord	$⊢ C \in 𝑸 \to (A <_{𝑸} B \leftrightarrow (C +_{𝑸} A) <_{𝑸} (C +_{𝑸} B))$

Metamath Proof Explorer

Theorem ltanq

Proof