Theorem addpipq

Description: Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	addpipq	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ +pQ ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( ( 𝐴 ·N 𝐷 ) +N ( 𝐶 ·N 𝐵 ) ) , ( 𝐵 ·N 𝐷 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		opelxpi	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) )
2		opelxpi	⊢ ( ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) )
3		addpipq2	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ +pQ ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) +N ( ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) , ( ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ⟩ )
4	1 2 3	syl2an	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ +pQ ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) +N ( ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) , ( ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ⟩ )
5		op1stg	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
6		op2ndg	⊢ ( ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) → ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
7	5 6	oveqan12d	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) = ( 𝐴 ·N 𝐷 ) )
8		op1stg	⊢ ( ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) → ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
9		op2ndg	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
10	8 9	oveqan12rd	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ( ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝐶 ·N 𝐵 ) )
11	7 10	oveq12d	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) +N ( ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) = ( ( 𝐴 ·N 𝐷 ) +N ( 𝐶 ·N 𝐵 ) ) )
12	9 6	oveqan12d	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ( ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) = ( 𝐵 ·N 𝐷 ) )
13	11 12	opeq12d	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ⟨ ( ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) +N ( ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) , ( ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ⟩ = ⟨ ( ( 𝐴 ·N 𝐷 ) +N ( 𝐶 ·N 𝐵 ) ) , ( 𝐵 ·N 𝐷 ) ⟩ )
14	4 13	eqtrd	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ +pQ ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( ( 𝐴 ·N 𝐷 ) +N ( 𝐶 ·N 𝐵 ) ) , ( 𝐵 ·N 𝐷 ) ⟩ )