Metamath Proof Explorer


Theorem pell14qrmulcl

Description: Positive Pell solutions are closed under multiplication. (Contributed by Stefan O'Rear, 17-Sep-2014)

Ref Expression
Assertion pell14qrmulcl ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 · 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) ) → 𝐷 ∈ ( ℕ ∖ ◻NN ) )
2 simprll ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) ) → 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) )
3 simprrl ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) ) → 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) )
4 pell1234qrmulcl ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ) → ( 𝐴 · 𝐵 ) ∈ ( Pell1234QR ‘ 𝐷 ) )
5 1 2 3 4 syl3anc ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) ) → ( 𝐴 · 𝐵 ) ∈ ( Pell1234QR ‘ 𝐷 ) )
6 pell1234qrre ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ) → 𝐴 ∈ ℝ )
7 2 6 syldan ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) ) → 𝐴 ∈ ℝ )
8 pell1234qrre ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ) → 𝐵 ∈ ℝ )
9 3 8 syldan ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) ) → 𝐵 ∈ ℝ )
10 simprlr ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) ) → 0 < 𝐴 )
11 simprrr ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) ) → 0 < 𝐵 )
12 7 9 10 11 mulgt0d ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) ) → 0 < ( 𝐴 · 𝐵 ) )
13 5 12 jca ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) ) → ( ( 𝐴 · 𝐵 ) ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < ( 𝐴 · 𝐵 ) ) )
14 13 ex ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) → ( ( 𝐴 · 𝐵 ) ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < ( 𝐴 · 𝐵 ) ) ) )
15 elpell14qr2 ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ) )
16 elpell14qr2 ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) )
17 15 16 anbi12d ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) ↔ ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < 𝐵 ) ) ) )
18 elpell14qr2 ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝐴 · 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( ( 𝐴 · 𝐵 ) ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 0 < ( 𝐴 · 𝐵 ) ) ) )
19 14 17 18 3imtr4d ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 · 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) ) )
20 19 3impib ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 · 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )