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