Theorem ltaddnq

Description: The sum of two fractions is greater than one of them. (Contributed by NM, 14-Mar-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	ltaddnq	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to A{<}_{𝑸}\left(A{+}_{𝑸}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢x=A\to x=A$$
2		oveq1	$$⊢x=A\to x{+}_{𝑸}y=A{+}_{𝑸}y$$
3	1 2	breq12d	$$⊢x=A\to \left(x{<}_{𝑸}\left(x{+}_{𝑸}y\right)\leftrightarrow A{<}_{𝑸}\left(A{+}_{𝑸}y\right)\right)$$
4		oveq2	$$⊢y=B\to A{+}_{𝑸}y=A{+}_{𝑸}B$$
5	4	breq2d	$$⊢y=B\to \left(A{<}_{𝑸}\left(A{+}_{𝑸}y\right)\leftrightarrow A{<}_{𝑸}\left(A{+}_{𝑸}B\right)\right)$$
6		1lt2nq	$$⊢1_{𝑸}{<}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)$$
7		ltmnq	$$⊢y\in 𝑸\to \left(1_{𝑸}{<}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\leftrightarrow \left(y{\cdot }_{𝑸}{1}_{𝑸}\right){<}_{𝑸}\left(y{\cdot }_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)\right)$$
8	6 7	mpbii	$$⊢y\in 𝑸\to \left(y{\cdot }_{𝑸}{1}_{𝑸}\right){<}_{𝑸}\left(y{\cdot }_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)$$
9		mulidnq	$$⊢y\in 𝑸\to y{\cdot }_{𝑸}{1}_{𝑸}=y$$
10		distrnq	$$⊢y{\cdot }_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)=\left(y{\cdot }_{𝑸}{1}_{𝑸}\right){+}_{𝑸}\left(y{\cdot }_{𝑸}{1}_{𝑸}\right)$$
11	9 9	oveq12d	$$⊢y\in 𝑸\to \left(y{\cdot }_{𝑸}{1}_{𝑸}\right){+}_{𝑸}\left(y{\cdot }_{𝑸}{1}_{𝑸}\right)=y{+}_{𝑸}y$$
12	10 11	syl5eq	$$⊢y\in 𝑸\to y{\cdot }_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)=y{+}_{𝑸}y$$
13	8 9 12	3brtr3d	$$⊢y\in 𝑸\to y{<}_{𝑸}\left(y{+}_{𝑸}y\right)$$
14		ltanq	$$⊢x\in 𝑸\to \left(y{<}_{𝑸}\left(y{+}_{𝑸}y\right)\leftrightarrow \left(x{+}_{𝑸}y\right){<}_{𝑸}\left(x{+}_{𝑸}\left(y{+}_{𝑸}y\right)\right)\right)$$
15	13 14	syl5ib	$$⊢x\in 𝑸\to \left(y\in 𝑸\to \left(x{+}_{𝑸}y\right){<}_{𝑸}\left(x{+}_{𝑸}\left(y{+}_{𝑸}y\right)\right)\right)$$
16	15	imp	$$⊢\left(x\in 𝑸\wedge y\in 𝑸\right)\to \left(x{+}_{𝑸}y\right){<}_{𝑸}\left(x{+}_{𝑸}\left(y{+}_{𝑸}y\right)\right)$$
17		addcomnq	$$⊢x{+}_{𝑸}y=y{+}_{𝑸}x$$
18		vex	$$⊢x\in \mathrm{V}$$
19		vex	$$⊢y\in \mathrm{V}$$
20		addcomnq	$$⊢r{+}_{𝑸}s=s{+}_{𝑸}r$$
21		addassnq	$$⊢\left(r{+}_{𝑸}s\right){+}_{𝑸}t=r{+}_{𝑸}\left(s{+}_{𝑸}t\right)$$
22	18 19 19 20 21	caov12	$$⊢x{+}_{𝑸}\left(y{+}_{𝑸}y\right)=y{+}_{𝑸}\left(x{+}_{𝑸}y\right)$$
23	16 17 22	3brtr3g	$$⊢\left(x\in 𝑸\wedge y\in 𝑸\right)\to \left(y{+}_{𝑸}x\right){<}_{𝑸}\left(y{+}_{𝑸}\left(x{+}_{𝑸}y\right)\right)$$
24		ltanq	$$⊢y\in 𝑸\to \left(x{<}_{𝑸}\left(x{+}_{𝑸}y\right)\leftrightarrow \left(y{+}_{𝑸}x\right){<}_{𝑸}\left(y{+}_{𝑸}\left(x{+}_{𝑸}y\right)\right)\right)$$
25	24	adantl	$$⊢\left(x\in 𝑸\wedge y\in 𝑸\right)\to \left(x{<}_{𝑸}\left(x{+}_{𝑸}y\right)\leftrightarrow \left(y{+}_{𝑸}x\right){<}_{𝑸}\left(y{+}_{𝑸}\left(x{+}_{𝑸}y\right)\right)\right)$$
26	23 25	mpbird	$$⊢\left(x\in 𝑸\wedge y\in 𝑸\right)\to x{<}_{𝑸}\left(x{+}_{𝑸}y\right)$$
27	3 5 26	vtocl2ga	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to A{<}_{𝑸}\left(A{+}_{𝑸}B\right)$$