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	⊢ ( 𝐴 ∈ Q → ∃ 𝑥 ∈ N 𝐴 <_Q ⟨ 𝑥 , 1_o ⟩ )

Proof

Step	Hyp	Ref	Expression
1		elpqn	⊢ ( 𝐴 ∈ Q → 𝐴 ∈ ( N × N ) )
2		xp1st	⊢ ( 𝐴 ∈ ( N × N ) → ( 1^st ‘ 𝐴 ) ∈ N )
3	1 2	syl	⊢ ( 𝐴 ∈ Q → ( 1^st ‘ 𝐴 ) ∈ N )
4		1pi	⊢ 1_o ∈ N
5		addclpi	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ N ∧ 1_o ∈ N ) → ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ∈ N )
6	3 4 5	sylancl	⊢ ( 𝐴 ∈ Q → ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ∈ N )
7		xp2nd	⊢ ( 𝐴 ∈ ( N × N ) → ( 2^nd ‘ 𝐴 ) ∈ N )
8	1 7	syl	⊢ ( 𝐴 ∈ Q → ( 2^nd ‘ 𝐴 ) ∈ N )
9		mulclpi	⊢ ( ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ∈ N ∧ ( 2^nd ‘ 𝐴 ) ∈ N ) → ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) ∈ N )
10	6 8 9	syl2anc	⊢ ( 𝐴 ∈ Q → ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) ∈ N )
11		eqid	⊢ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) = ( ( 1^st ‘ 𝐴 ) +_N 1_o )
12		oveq2	⊢ ( 𝑥 = 1_o → ( ( 1^st ‘ 𝐴 ) +_N 𝑥 ) = ( ( 1^st ‘ 𝐴 ) +_N 1_o ) )
13	12	eqeq1d	⊢ ( 𝑥 = 1_o → ( ( ( 1^st ‘ 𝐴 ) +_N 𝑥 ) = ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ↔ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) = ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ) )
14	13	rspcev	⊢ ( ( 1_o ∈ N ∧ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) = ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ) → ∃ 𝑥 ∈ N ( ( 1^st ‘ 𝐴 ) +_N 𝑥 ) = ( ( 1^st ‘ 𝐴 ) +_N 1_o ) )
15	4 11 14	mp2an	⊢ ∃ 𝑥 ∈ N ( ( 1^st ‘ 𝐴 ) +_N 𝑥 ) = ( ( 1^st ‘ 𝐴 ) +_N 1_o )
16		ltexpi	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ N ∧ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ∈ N ) → ( ( 1^st ‘ 𝐴 ) <_N ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ↔ ∃ 𝑥 ∈ N ( ( 1^st ‘ 𝐴 ) +_N 𝑥 ) = ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ) )
17	15 16	mpbiri	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ N ∧ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ∈ N ) → ( 1^st ‘ 𝐴 ) <_N ( ( 1^st ‘ 𝐴 ) +_N 1_o ) )
18	3 6 17	syl2anc	⊢ ( 𝐴 ∈ Q → ( 1^st ‘ 𝐴 ) <_N ( ( 1^st ‘ 𝐴 ) +_N 1_o ) )
19		nlt1pi	⊢ ¬ ( 2^nd ‘ 𝐴 ) <_N 1_o
20		ltmpi	⊢ ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ∈ N → ( ( 2^nd ‘ 𝐴 ) <_N 1_o ↔ ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) <_N ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N 1_o ) ) )
21	6 20	syl	⊢ ( 𝐴 ∈ Q → ( ( 2^nd ‘ 𝐴 ) <_N 1_o ↔ ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) <_N ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N 1_o ) ) )
22		mulidpi	⊢ ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ∈ N → ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N 1_o ) = ( ( 1^st ‘ 𝐴 ) +_N 1_o ) )
23	6 22	syl	⊢ ( 𝐴 ∈ Q → ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N 1_o ) = ( ( 1^st ‘ 𝐴 ) +_N 1_o ) )
24	23	breq2d	⊢ ( 𝐴 ∈ Q → ( ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) <_N ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N 1_o ) ↔ ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) <_N ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ) )
25	21 24	bitrd	⊢ ( 𝐴 ∈ Q → ( ( 2^nd ‘ 𝐴 ) <_N 1_o ↔ ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) <_N ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ) )
26	19 25	mtbii	⊢ ( 𝐴 ∈ Q → ¬ ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) <_N ( ( 1^st ‘ 𝐴 ) +_N 1_o ) )
27		ltsopi	⊢ <_N Or N
28		ltrelpi	⊢ <_N ⊆ ( N × N )
29	27 28	sotri3	⊢ ( ( ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) ∈ N ∧ ( 1^st ‘ 𝐴 ) <_N ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ∧ ¬ ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) <_N ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ) → ( 1^st ‘ 𝐴 ) <_N ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) )
30	10 18 26 29	syl3anc	⊢ ( 𝐴 ∈ Q → ( 1^st ‘ 𝐴 ) <_N ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) )
31		pinq	⊢ ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ∈ N → ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ∈ Q )
32	6 31	syl	⊢ ( 𝐴 ∈ Q → ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ∈ Q )
33		ordpinq	⊢ ( ( 𝐴 ∈ Q ∧ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ∈ Q ) → ( 𝐴 <_Q ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) ) <_N ( ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
34	32 33	mpdan	⊢ ( 𝐴 ∈ Q → ( 𝐴 <_Q ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) ) <_N ( ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
35		ovex	⊢ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ∈ V
36		1oex	⊢ 1_o ∈ V
37	35 36	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) = 1_o
38	37	oveq2i	⊢ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) ) = ( ( 1^st ‘ 𝐴 ) ·_N 1_o )
39		mulidpi	⊢ ( ( 1^st ‘ 𝐴 ) ∈ N → ( ( 1^st ‘ 𝐴 ) ·_N 1_o ) = ( 1^st ‘ 𝐴 ) )
40	3 39	syl	⊢ ( 𝐴 ∈ Q → ( ( 1^st ‘ 𝐴 ) ·_N 1_o ) = ( 1^st ‘ 𝐴 ) )
41	38 40	syl5eq	⊢ ( 𝐴 ∈ Q → ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) ) = ( 1^st ‘ 𝐴 ) )
42	35 36	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) = ( ( 1^st ‘ 𝐴 ) +_N 1_o )
43	42	oveq1i	⊢ ( ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) ·_N ( 2^nd ‘ 𝐴 ) ) = ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) )
44	43	a1i	⊢ ( 𝐴 ∈ Q → ( ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) ·_N ( 2^nd ‘ 𝐴 ) ) = ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) )
45	41 44	breq12d	⊢ ( 𝐴 ∈ Q → ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) ) <_N ( ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) ·_N ( 2^nd ‘ 𝐴 ) ) ↔ ( 1^st ‘ 𝐴 ) <_N ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
46	34 45	bitrd	⊢ ( 𝐴 ∈ Q → ( 𝐴 <_Q ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ↔ ( 1^st ‘ 𝐴 ) <_N ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
47	30 46	mpbird	⊢ ( 𝐴 ∈ Q → 𝐴 <_Q ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ )
48		opeq1	⊢ ( 𝑥 = ( ( 1^st ‘ 𝐴 ) +_N 1_o ) → ⟨ 𝑥 , 1_o ⟩ = ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ )
49	48	breq2d	⊢ ( 𝑥 = ( ( 1^st ‘ 𝐴 ) +_N 1_o ) → ( 𝐴 <_Q ⟨ 𝑥 , 1_o ⟩ ↔ 𝐴 <_Q ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) )
50	49	rspcev	⊢ ( ( ( ( 1^st ‘ 𝐴 ) +_N 1_o ) ∈ N ∧ 𝐴 <_Q ⟨ ( ( 1^st ‘ 𝐴 ) +_N 1_o ) , 1_o ⟩ ) → ∃ 𝑥 ∈ N 𝐴 <_Q ⟨ 𝑥 , 1_o ⟩ )
51	6 47 50	syl2anc	⊢ ( 𝐴 ∈ Q → ∃ 𝑥 ∈ N 𝐴 <_Q ⟨ 𝑥 , 1_o ⟩ )

Metamath Proof Explorer

Theorem archnq

Proof