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