Metamath Proof Explorer

Theorem pellqrexplicit

Description: Condition for a calculated real to be a Pell solution. (Contributed by Stefan O'Rear, 19-Sep-2014)

Ref Expression
Assertion pellqrexplicit ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) → ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∈ ( Pell1QR ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 nn0re ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
2 1 3ad2ant2 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
3 eldifi ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℕ )
4 3 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → 𝐷 ∈ ℕ )
5 4 nnrpd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → 𝐷 ∈ ℝ+ )
6 5 rpsqrtcld ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( √ ‘ 𝐷 ) ∈ ℝ+ )
7 6 rpred ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( √ ‘ 𝐷 ) ∈ ℝ )
8 nn0re ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℝ )
9 8 3ad2ant3 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → 𝐵 ∈ ℝ )
10 7 9 remulcld ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( √ ‘ 𝐷 ) · 𝐵 ) ∈ ℝ )
11 2 10 readdcld ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∈ ℝ )
12 11 adantr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) → ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∈ ℝ )
13 simpl2 ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) → 𝐴 ∈ ℕ0 )
14 simpl3 ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) → 𝐵 ∈ ℕ0 )
15 eqidd ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) → ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) )
16 simpr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) → ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 )
17 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
18 17 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ↔ ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) )
19 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
20 19 oveq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) )
21 20 eqeq1d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ↔ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) )
22 18 21 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ↔ ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) )
23 oveq2 ⊢ ( 𝑏 = 𝐵 → ( ( √ ‘ 𝐷 ) · 𝑏 ) = ( ( √ ‘ 𝐷 ) · 𝐵 ) )
24 23 oveq2d ⊢ ( 𝑏 = 𝐵 → ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) )
25 24 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ↔ ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ) )
26 oveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ↑ 2 ) = ( 𝐵 ↑ 2 ) )
27 26 oveq2d ⊢ ( 𝑏 = 𝐵 → ( 𝐷 · ( 𝑏 ↑ 2 ) ) = ( 𝐷 · ( 𝐵 ↑ 2 ) ) )
28 27 oveq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) )
29 28 eqeq1d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ↔ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) )
30 25 29 anbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ↔ ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) )
31 22 30 rspc2ev ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) )
32 13 14 15 16 31 syl112anc ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) → ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) )
33 elpell1qr ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∈ ℝ ∧ ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
34 33 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∈ ℝ ∧ ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
35 34 adantr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) → ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∈ ℝ ∧ ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
36 12 32 35 mpbir2and ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) → ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∈ ( Pell1QR ‘ 𝐷 ) )