Theorem archnq

Description: For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	archnq	$$⊢A\in 𝑸\to \exists x\in 𝑵A{<}_{𝑸}⟨x,1_{𝑜}⟩$$

Proof

Step	Hyp	Ref	Expression
1		elpqn	$$⊢A\in 𝑸\to A\in \left(𝑵\times 𝑵\right)$$
2		xp1st	$$⊢A\in \left(𝑵\times 𝑵\right)\to 1^{st}\left(A\right)\in 𝑵$$
3	1 2	syl	$$⊢A\in 𝑸\to 1^{st}\left(A\right)\in 𝑵$$
4		1pi	$$⊢1_{𝑜}\in 𝑵$$
5		addclpi	$$⊢\left(1^{st}\left(A\right)\in 𝑵\wedge 1_{𝑜}\in 𝑵\right)\to 1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\in 𝑵$$
6	3 4 5	sylancl	$$⊢A\in 𝑸\to 1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\in 𝑵$$
7		xp2nd	$$⊢A\in \left(𝑵\times 𝑵\right)\to 2^{nd}\left(A\right)\in 𝑵$$
8	1 7	syl	$$⊢A\in 𝑸\to 2^{nd}\left(A\right)\in 𝑵$$
9		mulclpi	$$⊢\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\in 𝑵\wedge 2^{nd}\left(A\right)\in 𝑵\right)\to \left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\in 𝑵$$
10	6 8 9	syl2anc	$$⊢A\in 𝑸\to \left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\in 𝑵$$
11		eqid	$$⊢1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}$$
12		oveq2	$$⊢x=1_{𝑜}\to 1^{st}\left(A\right){+}_{𝑵}x=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}$$
13	12	eqeq1d	$$⊢x=1_{𝑜}\to \left(1^{st}\left(A\right){+}_{𝑵}x=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\leftrightarrow 1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right)$$
14	13	rspcev	$$⊢\left(1_{𝑜}\in 𝑵\wedge 1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right)\to \exists x\in 𝑵1^{st}\left(A\right){+}_{𝑵}x=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}$$
15	4 11 14	mp2an	$$⊢\exists x\in 𝑵1^{st}\left(A\right){+}_{𝑵}x=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}$$
16		ltexpi	$$⊢\left(1^{st}\left(A\right)\in 𝑵\wedge 1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\in 𝑵\right)\to \left(1^{st}\left(A\right){<}_{𝑵}\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right)\leftrightarrow \exists x\in 𝑵1^{st}\left(A\right){+}_{𝑵}x=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right)$$
17	15 16	mpbiri	$$⊢\left(1^{st}\left(A\right)\in 𝑵\wedge 1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\in 𝑵\right)\to 1^{st}\left(A\right){<}_{𝑵}\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right)$$
18	3 6 17	syl2anc	$$⊢A\in 𝑸\to 1^{st}\left(A\right){<}_{𝑵}\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right)$$
19		nlt1pi	$$⊢\neg 2^{nd}\left(A\right){<}_{𝑵}{1}_{𝑜}$$
20		ltmpi	$$⊢1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\in 𝑵\to \left(2^{nd}\left(A\right){<}_{𝑵}{1}_{𝑜}\leftrightarrow \left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right){<}_{𝑵}\left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{1}_{𝑜}\right)\right)$$
21	6 20	syl	$$⊢A\in 𝑸\to \left(2^{nd}\left(A\right){<}_{𝑵}{1}_{𝑜}\leftrightarrow \left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right){<}_{𝑵}\left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{1}_{𝑜}\right)\right)$$
22		mulidpi	$$⊢1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\in 𝑵\to \left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{1}_{𝑜}=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}$$
23	6 22	syl	$$⊢A\in 𝑸\to \left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{1}_{𝑜}=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}$$
24	23	breq2d	$$⊢A\in 𝑸\to \left(\left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right){<}_{𝑵}\left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{1}_{𝑜}\right)\leftrightarrow \left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right){<}_{𝑵}\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right)\right)$$
25	21 24	bitrd	$$⊢A\in 𝑸\to \left(2^{nd}\left(A\right){<}_{𝑵}{1}_{𝑜}\leftrightarrow \left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right){<}_{𝑵}\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right)\right)$$
26	19 25	mtbii	$$⊢A\in 𝑸\to \neg \left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right){<}_{𝑵}\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right)$$
27		ltsopi	$$⊢{<}_{𝑵}\mathrm{Or}𝑵$$
28		ltrelpi	$$⊢{<}_{𝑵}\subseteq 𝑵\times 𝑵$$
29	27 28	sotri3	$$⊢\left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\in 𝑵\wedge 1^{st}\left(A\right){<}_{𝑵}\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right)\wedge \neg \left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right){<}_{𝑵}\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right)\right)\to 1^{st}\left(A\right){<}_{𝑵}\left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)$$
30	10 18 26 29	syl3anc	$$⊢A\in 𝑸\to 1^{st}\left(A\right){<}_{𝑵}\left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)$$
31		pinq	$$⊢1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\in 𝑵\to ⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\in 𝑸$$
32	6 31	syl	$$⊢A\in 𝑸\to ⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\in 𝑸$$
33		ordpinq	$$⊢\left(A\in 𝑸\wedge ⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\in 𝑸\right)\to \left(A{<}_{𝑸}⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\leftrightarrow \left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right)\right){<}_{𝑵}\left(1^{st}\left(⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)\right)$$
34	32 33	mpdan	$$⊢A\in 𝑸\to \left(A{<}_{𝑸}⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\leftrightarrow \left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right)\right){<}_{𝑵}\left(1^{st}\left(⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)\right)$$
35		ovex	$$⊢1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\in \mathrm{V}$$
36		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
37	35 36	op2nd	$$⊢2^{nd}\left(⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right)=1_{𝑜}$$
38	37	oveq2i	$$⊢1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right)=1^{st}\left(A\right){\cdot }_{𝑵}{1}_{𝑜}$$
39		mulidpi	$$⊢1^{st}\left(A\right)\in 𝑵\to 1^{st}\left(A\right){\cdot }_{𝑵}{1}_{𝑜}=1^{st}\left(A\right)$$
40	3 39	syl	$$⊢A\in 𝑸\to 1^{st}\left(A\right){\cdot }_{𝑵}{1}_{𝑜}=1^{st}\left(A\right)$$
41	38 40	syl5eq	$$⊢A\in 𝑸\to 1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right)=1^{st}\left(A\right)$$
42	35 36	op1st	$$⊢1^{st}\left(⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right)=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}$$
43	42	oveq1i	$$⊢1^{st}\left(⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)=\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)$$
44	43	a1i	$$⊢A\in 𝑸\to 1^{st}\left(⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)=\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)$$
45	41 44	breq12d	$$⊢A\in 𝑸\to \left(\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right)\right){<}_{𝑵}\left(1^{st}\left(⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)\leftrightarrow 1^{st}\left(A\right){<}_{𝑵}\left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)\right)$$
46	34 45	bitrd	$$⊢A\in 𝑸\to \left(A{<}_{𝑸}⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\leftrightarrow 1^{st}\left(A\right){<}_{𝑵}\left(\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)\right)$$
47	30 46	mpbird	$$⊢A\in 𝑸\to A{<}_{𝑸}⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩$$
48		opeq1	$$⊢x=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\to ⟨x,1_{𝑜}⟩=⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩$$
49	48	breq2d	$$⊢x=1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\to \left(A{<}_{𝑸}⟨x,1_{𝑜}⟩\leftrightarrow A{<}_{𝑸}⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right)$$
50	49	rspcev	$$⊢\left(1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜}\in 𝑵\wedge A{<}_{𝑸}⟨1^{st}\left(A\right){+}_{𝑵}{1}_{𝑜},1_{𝑜}⟩\right)\to \exists x\in 𝑵A{<}_{𝑸}⟨x,1_{𝑜}⟩$$
51	6 47 50	syl2anc	$$⊢A\in 𝑸\to \exists x\in 𝑵A{<}_{𝑸}⟨x,1_{𝑜}⟩$$