Metamath Proof Explorer

Theorem pellexlem1

Description: Lemma for pellex . Arithmetical core of pellexlem3, norm lower bound. This begins Dirichlet's proof of the Pell equation solution existence; the proof here follows theorem 62 of vandenDries p. 43. (Contributed by Stefan O'Rear, 14-Sep-2014)

Ref Expression
Assertion pellexlem1 ( ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 nncn ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
2 1 3ad2ant2 ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℂ )
3 2 sqcld ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
4 nncn ⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℂ )
5 4 3ad2ant1 ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐷 ∈ ℂ )
6 nncn ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
7 6 3ad2ant3 ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℂ )
8 7 sqcld ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
9 5 8 mulcld ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐷 · ( 𝐵 ↑ 2 ) ) ∈ ℂ )
10 3 9 subeq0ad ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 0 ↔ ( 𝐴 ↑ 2 ) = ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) )
11 nnne0 ⊢ ( 𝐵 ∈ ℕ → 𝐵 ≠ 0 )
12 11 3ad2ant3 ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐵 ≠ 0 )
13 sqne0 ⊢ ( 𝐵 ∈ ℂ → ( ( 𝐵 ↑ 2 ) ≠ 0 ↔ 𝐵 ≠ 0 ) )
14 7 13 syl ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐵 ↑ 2 ) ≠ 0 ↔ 𝐵 ≠ 0 ) )
15 12 14 mpbird ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 ↑ 2 ) ≠ 0 )
16 3 5 8 15 divmul3d ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) = 𝐷 ↔ ( 𝐴 ↑ 2 ) = ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) )
17 sqdiv ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) )
18 17 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( √ ‘ ( ( 𝐴 / 𝐵 ) ↑ 2 ) ) = ( √ ‘ ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) ) )
19 2 7 12 18 syl3anc ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( √ ‘ ( ( 𝐴 / 𝐵 ) ↑ 2 ) ) = ( √ ‘ ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) ) )
20 nnre ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
21 20 3ad2ant2 ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℝ )
22 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
23 22 3ad2ant3 ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℝ )
24 21 23 12 redivcld ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
25 nnnn0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
26 25 nn0ge0d ⊢ ( 𝐴 ∈ ℕ → 0 ≤ 𝐴 )
27 26 3ad2ant2 ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 0 ≤ 𝐴 )
28 nngt0 ⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
29 28 3ad2ant3 ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 0 < 𝐵 )
30 divge0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 ≤ ( 𝐴 / 𝐵 ) )
31 21 27 23 29 30 syl22anc ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 0 ≤ ( 𝐴 / 𝐵 ) )
32 24 31 sqrtsqd ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( √ ‘ ( ( 𝐴 / 𝐵 ) ↑ 2 ) ) = ( 𝐴 / 𝐵 ) )
33 19 32 eqtr3d ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) ) = ( 𝐴 / 𝐵 ) )
34 nnq ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℚ )
35 34 3ad2ant2 ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℚ )
36 nnq ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℚ )
37 36 3ad2ant3 ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℚ )
38 qdivcl ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℚ )
39 35 37 12 38 syl3anc ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / 𝐵 ) ∈ ℚ )
40 33 39 eqeltrd ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) ) ∈ ℚ )
41 fveq2 ⊢ ( ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) = 𝐷 → ( √ ‘ ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) ) = ( √ ‘ 𝐷 ) )
42 41 eleq1d ⊢ ( ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) = 𝐷 → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) ) ∈ ℚ ↔ ( √ ‘ 𝐷 ) ∈ ℚ ) )
43 40 42 syl5ibcom ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) = 𝐷 → ( √ ‘ 𝐷 ) ∈ ℚ ) )
44 16 43 sylbird ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 ↑ 2 ) = ( 𝐷 · ( 𝐵 ↑ 2 ) ) → ( √ ‘ 𝐷 ) ∈ ℚ ) )
45 10 44 sylbid ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 0 → ( √ ‘ 𝐷 ) ∈ ℚ ) )
46 45 necon3bd ⊢ ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ¬ ( √ ‘ 𝐷 ) ∈ ℚ → ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) ≠ 0 ) )
47 46 imp ⊢ ( ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) ≠ 0 )