Metamath Proof Explorer

Theorem pell1234qrne0

Description: No solution to a Pell equation is zero. (Contributed by Stefan O'Rear, 17-Sep-2014)

Ref Expression
Assertion pell1234qrne0 ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ) → 𝐴 ≠ 0 )

Proof

Step Hyp Ref Expression
1 elpell1234qr ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
2 simprl ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
3 ax-1ne0 ⊢ 1 ≠ 0
4 eldifi ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℕ )
5 4 adantr ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) → 𝐷 ∈ ℕ )
6 5 nncnd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) → 𝐷 ∈ ℂ )
7 6 ad3antrrr ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → 𝐷 ∈ ℂ )
8 7 sqrtcld ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( √ ‘ 𝐷 ) ∈ ℂ )
9 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
10 9 ad2antll ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
11 10 ad2antrr ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → 𝑏 ∈ ℂ )
12 8 11 sqmuld ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) = ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑏 ↑ 2 ) ) )
13 7 sqsqrtd ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( ( √ ‘ 𝐷 ) ↑ 2 ) = 𝐷 )
14 13 oveq1d ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑏 ↑ 2 ) ) = ( 𝐷 · ( 𝑏 ↑ 2 ) ) )
15 12 14 eqtr2d ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( 𝐷 · ( 𝑏 ↑ 2 ) ) = ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) )
16 15 oveq2d ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) ) )
17 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
18 17 ad2antrl ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
19 18 ad2antrr ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → 𝑎 ∈ ℂ )
20 8 11 mulcld ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( ( √ ‘ 𝐷 ) · 𝑏 ) ∈ ℂ )
21 subsq ⊢ ( ( 𝑎 ∈ ℂ ∧ ( ( √ ‘ 𝐷 ) · 𝑏 ) ∈ ℂ ) → ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) ) = ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) )
22 19 20 21 syl2anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) ) = ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) )
23 16 22 eqtrd ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) )
24 simplr ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 )
25 simpr ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 )
26 25 oveq1d ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) = ( 0 · ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) )
27 19 20 subcld ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∈ ℂ )
28 27 mul02d ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( 0 · ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) = 0 )
29 26 28 eqtrd ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) = 0 )
30 23 24 29 3eqtr3d ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 ) → 1 = 0 )
31 30 ex ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = 0 → 1 = 0 ) )
32 31 necon3d ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 1 ≠ 0 → ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ≠ 0 ) )
33 3 32 mpi ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ≠ 0 )
34 33 adantrl ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ≠ 0 )
35 2 34 eqnetrd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝐴 ≠ 0 )
36 35 ex ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 𝐴 ≠ 0 ) )
37 36 rexlimdvva ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 𝐴 ≠ 0 ) )
38 37 expimpd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝐴 ∈ ℝ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝐴 ≠ 0 ) )
39 1 38 sylbid ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) → 𝐴 ≠ 0 ) )
40 39 imp ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ) → 𝐴 ≠ 0 )