Metamath Proof Explorer

Theorem pell1qr1

Description: 1 is a Pell solution and in the first quadrant as one. (Contributed by Stefan O'Rear, 17-Sep-2014)

Ref Expression
Assertion pell1qr1 ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 ∈ ( Pell1QR ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 1red ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 ∈ ℝ )
2 1nn0 ⊢ 1 ∈ ℕ0
3 2 a1i ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 ∈ ℕ0 )
4 0nn0 ⊢ 0 ∈ ℕ0
5 4 a1i ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 0 ∈ ℕ0 )
6 eldifi ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℕ )
7 6 nncnd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℂ )
8 7 sqrtcld ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( √ ‘ 𝐷 ) ∈ ℂ )
9 8 mul01d ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( √ ‘ 𝐷 ) · 0 ) = 0 )
10 9 oveq2d ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 1 + ( ( √ ‘ 𝐷 ) · 0 ) ) = ( 1 + 0 ) )
11 1p0e1 ⊢ ( 1 + 0 ) = 1
12 10 11 eqtr2di ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 = ( 1 + ( ( √ ‘ 𝐷 ) · 0 ) ) )
13 sq1 ⊢ ( 1 ↑ 2 ) = 1
14 13 a1i ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 1 ↑ 2 ) = 1 )
15 sq0 ⊢ ( 0 ↑ 2 ) = 0
16 15 oveq2i ⊢ ( 𝐷 · ( 0 ↑ 2 ) ) = ( 𝐷 · 0 )
17 7 mul01d ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐷 · 0 ) = 0 )
18 16 17 syl5eq ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐷 · ( 0 ↑ 2 ) ) = 0 )
19 14 18 oveq12d ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 1 ↑ 2 ) − ( 𝐷 · ( 0 ↑ 2 ) ) ) = ( 1 − 0 ) )
20 1m0e1 ⊢ ( 1 − 0 ) = 1
21 19 20 eqtrdi ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 1 ↑ 2 ) − ( 𝐷 · ( 0 ↑ 2 ) ) ) = 1 )
22 oveq1 ⊢ ( 𝑎 = 1 → ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = ( 1 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
23 22 eqeq2d ⊢ ( 𝑎 = 1 → ( 1 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ↔ 1 = ( 1 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) )
24 oveq1 ⊢ ( 𝑎 = 1 → ( 𝑎 ↑ 2 ) = ( 1 ↑ 2 ) )
25 24 oveq1d ⊢ ( 𝑎 = 1 → ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = ( ( 1 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) )
26 25 eqeq1d ⊢ ( 𝑎 = 1 → ( ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ↔ ( ( 1 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) )
27 23 26 anbi12d ⊢ ( 𝑎 = 1 → ( ( 1 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ↔ ( 1 = ( 1 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 1 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) )
28 oveq2 ⊢ ( 𝑏 = 0 → ( ( √ ‘ 𝐷 ) · 𝑏 ) = ( ( √ ‘ 𝐷 ) · 0 ) )
29 28 oveq2d ⊢ ( 𝑏 = 0 → ( 1 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = ( 1 + ( ( √ ‘ 𝐷 ) · 0 ) ) )
30 29 eqeq2d ⊢ ( 𝑏 = 0 → ( 1 = ( 1 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ↔ 1 = ( 1 + ( ( √ ‘ 𝐷 ) · 0 ) ) ) )
31 oveq1 ⊢ ( 𝑏 = 0 → ( 𝑏 ↑ 2 ) = ( 0 ↑ 2 ) )
32 31 oveq2d ⊢ ( 𝑏 = 0 → ( 𝐷 · ( 𝑏 ↑ 2 ) ) = ( 𝐷 · ( 0 ↑ 2 ) ) )
33 32 oveq2d ⊢ ( 𝑏 = 0 → ( ( 1 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = ( ( 1 ↑ 2 ) − ( 𝐷 · ( 0 ↑ 2 ) ) ) )
34 33 eqeq1d ⊢ ( 𝑏 = 0 → ( ( ( 1 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ↔ ( ( 1 ↑ 2 ) − ( 𝐷 · ( 0 ↑ 2 ) ) ) = 1 ) )
35 30 34 anbi12d ⊢ ( 𝑏 = 0 → ( ( 1 = ( 1 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 1 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ↔ ( 1 = ( 1 + ( ( √ ‘ 𝐷 ) · 0 ) ) ∧ ( ( 1 ↑ 2 ) − ( 𝐷 · ( 0 ↑ 2 ) ) ) = 1 ) ) )
36 27 35 rspc2ev ⊢ ( ( 1 ∈ ℕ0 ∧ 0 ∈ ℕ0 ∧ ( 1 = ( 1 + ( ( √ ‘ 𝐷 ) · 0 ) ) ∧ ( ( 1 ↑ 2 ) − ( 𝐷 · ( 0 ↑ 2 ) ) ) = 1 ) ) → ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 1 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) )
37 3 5 12 21 36 syl112anc ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 1 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) )
38 elpell1qr ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 1 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 1 ∈ ℝ ∧ ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 1 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
39 1 37 38 mpbir2and ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 ∈ ( Pell1QR ‘ 𝐷 ) )