Theorem 1lt2nq

Description: One is less than two (one plus one). (Contributed by NM, 13-Mar-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	1lt2nq	$$⊢1_{𝑸}{<}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)$$

Proof

Step	Hyp	Ref	Expression
1		1lt2pi	$$⊢1_{𝑜}{<}_{𝑵}\left(1_{𝑜}{+}_{𝑵}{1}_{𝑜}\right)$$
2		1pi	$$⊢1_{𝑜}\in 𝑵$$
3		mulidpi	$$⊢1_{𝑜}\in 𝑵\to 1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}=1_{𝑜}$$
4	2 3	ax-mp	$$⊢1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}=1_{𝑜}$$
5		addclpi	$$⊢\left(1_{𝑜}\in 𝑵\wedge 1_{𝑜}\in 𝑵\right)\to 1_{𝑜}{+}_{𝑵}{1}_{𝑜}\in 𝑵$$
6	2 2 5	mp2an	$$⊢1_{𝑜}{+}_{𝑵}{1}_{𝑜}\in 𝑵$$
7		mulidpi	$$⊢1_{𝑜}{+}_{𝑵}{1}_{𝑜}\in 𝑵\to \left(1_{𝑜}{+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{1}_{𝑜}=1_{𝑜}{+}_{𝑵}{1}_{𝑜}$$
8	6 7	ax-mp	$$⊢\left(1_{𝑜}{+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{1}_{𝑜}=1_{𝑜}{+}_{𝑵}{1}_{𝑜}$$
9	1 4 8	3brtr4i	$$⊢\left(1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}\right){<}_{𝑵}\left(\left(1_{𝑜}{+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{1}_{𝑜}\right)$$
10		ordpipq	$$⊢⟨1_{𝑜},1_{𝑜}⟩{<}_{\mathrm{𝑝𝑸}}⟨1_{𝑜}{+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\leftrightarrow \left(1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}\right){<}_{𝑵}\left(\left(1_{𝑜}{+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{1}_{𝑜}\right)$$
11	9 10	mpbir	$$⊢⟨1_{𝑜},1_{𝑜}⟩{<}_{\mathrm{𝑝𝑸}}⟨1_{𝑜}{+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩$$
12		df-1nq	$$⊢1_{𝑸}=⟨1_{𝑜},1_{𝑜}⟩$$
13	12 12	oveq12i	$$⊢1_{𝑸}{+}_{\mathrm{𝑝𝑸}}{1}_{𝑸}=⟨1_{𝑜},1_{𝑜}⟩{+}_{\mathrm{𝑝𝑸}}⟨1_{𝑜},1_{𝑜}⟩$$
14		addpipq	$$⊢\left(\left(1_{𝑜}\in 𝑵\wedge 1_{𝑜}\in 𝑵\right)\wedge \left(1_{𝑜}\in 𝑵\wedge 1_{𝑜}\in 𝑵\right)\right)\to ⟨1_{𝑜},1_{𝑜}⟩{+}_{\mathrm{𝑝𝑸}}⟨1_{𝑜},1_{𝑜}⟩=⟨\left(1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}\right){+}_{𝑵}\left(1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}\right),1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}⟩$$
15	2 2 2 2 14	mp4an	$$⊢⟨1_{𝑜},1_{𝑜}⟩{+}_{\mathrm{𝑝𝑸}}⟨1_{𝑜},1_{𝑜}⟩=⟨\left(1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}\right){+}_{𝑵}\left(1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}\right),1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}⟩$$
16	4 4	oveq12i	$$⊢\left(1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}\right){+}_{𝑵}\left(1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}\right)=1_{𝑜}{+}_{𝑵}{1}_{𝑜}$$
17	16 4	opeq12i	$$⊢⟨\left(1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}\right){+}_{𝑵}\left(1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}\right),1_{𝑜}{\cdot }_{𝑵}{1}_{𝑜}⟩=⟨1_{𝑜}{+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩$$
18	13 15 17	3eqtri	$$⊢1_{𝑸}{+}_{\mathrm{𝑝𝑸}}{1}_{𝑸}=⟨1_{𝑜}{+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩$$
19	11 12 18	3brtr4i	$$⊢1_{𝑸}{<}_{\mathrm{𝑝𝑸}}\left(1_{𝑸}{+}_{\mathrm{𝑝𝑸}}{1}_{𝑸}\right)$$
20		lterpq	$$⊢1_{𝑸}{<}_{\mathrm{𝑝𝑸}}\left(1_{𝑸}{+}_{\mathrm{𝑝𝑸}}{1}_{𝑸}\right)\leftrightarrow {/}_{𝑸}\left(1_{𝑸}\right){<}_{𝑸}{/}_{𝑸}\left(1_{𝑸}{+}_{\mathrm{𝑝𝑸}}{1}_{𝑸}\right)$$
21	19 20	mpbi	$$⊢{/}_{𝑸}\left(1_{𝑸}\right){<}_{𝑸}{/}_{𝑸}\left(1_{𝑸}{+}_{\mathrm{𝑝𝑸}}{1}_{𝑸}\right)$$
22		1nq	$$⊢1_{𝑸}\in 𝑸$$
23		nqerid	$$⊢1_{𝑸}\in 𝑸\to {/}_{𝑸}\left(1_{𝑸}\right)=1_{𝑸}$$
24	22 23	ax-mp	$$⊢{/}_{𝑸}\left(1_{𝑸}\right)=1_{𝑸}$$
25	24	eqcomi	$$⊢1_{𝑸}={/}_{𝑸}\left(1_{𝑸}\right)$$
26		addpqnq	$$⊢\left(1_{𝑸}\in 𝑸\wedge 1_{𝑸}\in 𝑸\right)\to 1_{𝑸}{+}_{𝑸}{1}_{𝑸}={/}_{𝑸}\left(1_{𝑸}{+}_{\mathrm{𝑝𝑸}}{1}_{𝑸}\right)$$
27	22 22 26	mp2an	$$⊢1_{𝑸}{+}_{𝑸}{1}_{𝑸}={/}_{𝑸}\left(1_{𝑸}{+}_{\mathrm{𝑝𝑸}}{1}_{𝑸}\right)$$
28	21 25 27	3brtr4i	$$⊢1_{𝑸}{<}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)$$