pinq

Description: The representatives of positive integers as positive fractions. (Contributed by NM, 29-Oct-1995) (Revised by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	pinq	⊢ ( 𝐴 ∈ N → ⟨ 𝐴 , 1_o ⟩ ∈ Q )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑥 = ⟨ 𝐴 , 1_o ⟩ → ( 𝑥 ~_Q 𝑦 ↔ ⟨ 𝐴 , 1_o ⟩ ~_Q 𝑦 ) )
2		fveq2	⊢ ( 𝑥 = ⟨ 𝐴 , 1_o ⟩ → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ ⟨ 𝐴 , 1_o ⟩ ) )
3	2	breq2d	⊢ ( 𝑥 = ⟨ 𝐴 , 1_o ⟩ → ( ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ 𝑥 ) ↔ ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ ⟨ 𝐴 , 1_o ⟩ ) ) )
4	3	notbid	⊢ ( 𝑥 = ⟨ 𝐴 , 1_o ⟩ → ( ¬ ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ 𝑥 ) ↔ ¬ ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ ⟨ 𝐴 , 1_o ⟩ ) ) )
5	1 4	imbi12d	⊢ ( 𝑥 = ⟨ 𝐴 , 1_o ⟩ → ( ( 𝑥 ~_Q 𝑦 → ¬ ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ 𝑥 ) ) ↔ ( ⟨ 𝐴 , 1_o ⟩ ~_Q 𝑦 → ¬ ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ ⟨ 𝐴 , 1_o ⟩ ) ) ) )
6	5	ralbidv	⊢ ( 𝑥 = ⟨ 𝐴 , 1_o ⟩ → ( ∀ 𝑦 ∈ ( N × N ) ( 𝑥 ~_Q 𝑦 → ¬ ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ 𝑥 ) ) ↔ ∀ 𝑦 ∈ ( N × N ) ( ⟨ 𝐴 , 1_o ⟩ ~_Q 𝑦 → ¬ ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ ⟨ 𝐴 , 1_o ⟩ ) ) ) )
7		1pi	⊢ 1_o ∈ N
8		opelxpi	⊢ ( ( 𝐴 ∈ N ∧ 1_o ∈ N ) → ⟨ 𝐴 , 1_o ⟩ ∈ ( N × N ) )
9	7 8	mpan2	⊢ ( 𝐴 ∈ N → ⟨ 𝐴 , 1_o ⟩ ∈ ( N × N ) )
10		nlt1pi	⊢ ¬ ( 2^nd ‘ 𝑦 ) <_N 1_o
11		1oex	⊢ 1_o ∈ V
12		op2ndg	⊢ ( ( 𝐴 ∈ N ∧ 1_o ∈ V ) → ( 2^nd ‘ ⟨ 𝐴 , 1_o ⟩ ) = 1_o )
13	11 12	mpan2	⊢ ( 𝐴 ∈ N → ( 2^nd ‘ ⟨ 𝐴 , 1_o ⟩ ) = 1_o )
14	13	breq2d	⊢ ( 𝐴 ∈ N → ( ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ ⟨ 𝐴 , 1_o ⟩ ) ↔ ( 2^nd ‘ 𝑦 ) <_N 1_o ) )
15	10 14	mtbiri	⊢ ( 𝐴 ∈ N → ¬ ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ ⟨ 𝐴 , 1_o ⟩ ) )
16	15	a1d	⊢ ( 𝐴 ∈ N → ( ⟨ 𝐴 , 1_o ⟩ ~_Q 𝑦 → ¬ ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ ⟨ 𝐴 , 1_o ⟩ ) ) )
17	16	ralrimivw	⊢ ( 𝐴 ∈ N → ∀ 𝑦 ∈ ( N × N ) ( ⟨ 𝐴 , 1_o ⟩ ~_Q 𝑦 → ¬ ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ ⟨ 𝐴 , 1_o ⟩ ) ) )
18	6 9 17	elrabd	⊢ ( 𝐴 ∈ N → ⟨ 𝐴 , 1_o ⟩ ∈ { 𝑥 ∈ ( N × N ) ∣ ∀ 𝑦 ∈ ( N × N ) ( 𝑥 ~_Q 𝑦 → ¬ ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ 𝑥 ) ) } )
19		df-nq	⊢ Q = { 𝑥 ∈ ( N × N ) ∣ ∀ 𝑦 ∈ ( N × N ) ( 𝑥 ~_Q 𝑦 → ¬ ( 2^nd ‘ 𝑦 ) <_N ( 2^nd ‘ 𝑥 ) ) }
20	18 19	eleqtrrdi	⊢ ( 𝐴 ∈ N → ⟨ 𝐴 , 1_o ⟩ ∈ Q )

Metamath Proof Explorer

Theorem pinq

Proof