Metamath Proof Explorer

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 𝐷 ) ⟩ )