Metamath Proof Explorer


Theorem pell1qrgaplem

Description: Lemma for pell1qrgap . (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell1qrgaplem ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nnrp ( 𝐷 ∈ ℕ → 𝐷 ∈ ℝ+ )
2 1 ad2antrr ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 𝐷 ∈ ℝ+ )
3 1rp 1 ∈ ℝ+
4 3 a1i ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 1 ∈ ℝ+ )
5 2 4 rpaddcld ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 + 1 ) ∈ ℝ+ )
6 5 rpsqrtcld ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( √ ‘ ( 𝐷 + 1 ) ) ∈ ℝ+ )
7 6 rpred ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( √ ‘ ( 𝐷 + 1 ) ) ∈ ℝ )
8 2 rpsqrtcld ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( √ ‘ 𝐷 ) ∈ ℝ+ )
9 8 rpred ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( √ ‘ 𝐷 ) ∈ ℝ )
10 nn0re ( 𝐴 ∈ ℕ0𝐴 ∈ ℝ )
11 10 adantr ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
12 11 ad2antlr ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 𝐴 ∈ ℝ )
13 nn0re ( 𝐵 ∈ ℕ0𝐵 ∈ ℝ )
14 13 adantl ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) → 𝐵 ∈ ℝ )
15 14 ad2antlr ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 𝐵 ∈ ℝ )
16 9 15 remulcld ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ 𝐷 ) · 𝐵 ) ∈ ℝ )
17 2 rpred ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 𝐷 ∈ ℝ )
18 1re 1 ∈ ℝ
19 18 a1i ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 1 ∈ ℝ )
20 15 resqcld ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
21 19 20 resubcld ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 1 − ( 𝐵 ↑ 2 ) ) ∈ ℝ )
22 17 21 remulcld ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 · ( 1 − ( 𝐵 ↑ 2 ) ) ) ∈ ℝ )
23 0red ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 0 ∈ ℝ )
24 17 23 remulcld ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 · 0 ) ∈ ℝ )
25 12 resqcld ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
26 sq1 ( 1 ↑ 2 ) = 1
27 26 a1i ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 1 ↑ 2 ) = 1 )
28 nnge1 ( 𝐵 ∈ ℕ → 1 ≤ 𝐵 )
29 28 adantl ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 ∈ ℕ ) → 1 ≤ 𝐵 )
30 simplrl ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) )
31 oveq1 ( 𝐵 = 0 → ( 𝐵 ↑ 2 ) = ( 0 ↑ 2 ) )
32 31 adantl ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( 𝐵 ↑ 2 ) = ( 0 ↑ 2 ) )
33 sq0 ( 0 ↑ 2 ) = 0
34 32 33 eqtrdi ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( 𝐵 ↑ 2 ) = 0 )
35 34 oveq2d ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( 𝐷 · ( 𝐵 ↑ 2 ) ) = ( 𝐷 · 0 ) )
36 2 rpcnd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 𝐷 ∈ ℂ )
37 36 adantr ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → 𝐷 ∈ ℂ )
38 37 mul01d ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( 𝐷 · 0 ) = 0 )
39 35 38 eqtrd ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( 𝐷 · ( 𝐵 ↑ 2 ) ) = 0 )
40 39 oveq2d ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = ( ( 𝐴 ↑ 2 ) − 0 ) )
41 simplrr ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 )
42 12 recnd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 𝐴 ∈ ℂ )
43 42 sqcld ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
44 43 adantr ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
45 44 subid1d ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( ( 𝐴 ↑ 2 ) − 0 ) = ( 𝐴 ↑ 2 ) )
46 40 41 45 3eqtr3d ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → 1 = ( 𝐴 ↑ 2 ) )
47 26 46 eqtr2id ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( 𝐴 ↑ 2 ) = ( 1 ↑ 2 ) )
48 nn0ge0 ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
49 48 adantr ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) → 0 ≤ 𝐴 )
50 49 ad2antlr ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 0 ≤ 𝐴 )
51 0le1 0 ≤ 1
52 51 a1i ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 0 ≤ 1 )
53 sq11 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ) → ( ( 𝐴 ↑ 2 ) = ( 1 ↑ 2 ) ↔ 𝐴 = 1 ) )
54 12 50 19 52 53 syl22anc ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝐴 ↑ 2 ) = ( 1 ↑ 2 ) ↔ 𝐴 = 1 ) )
55 54 adantr ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( ( 𝐴 ↑ 2 ) = ( 1 ↑ 2 ) ↔ 𝐴 = 1 ) )
56 47 55 mpbid ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → 𝐴 = 1 )
57 simpr ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → 𝐵 = 0 )
58 57 oveq2d ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( ( √ ‘ 𝐷 ) · 𝐵 ) = ( ( √ ‘ 𝐷 ) · 0 ) )
59 8 rpcnd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( √ ‘ 𝐷 ) ∈ ℂ )
60 59 adantr ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( √ ‘ 𝐷 ) ∈ ℂ )
61 60 mul01d ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( ( √ ‘ 𝐷 ) · 0 ) = 0 )
62 58 61 eqtrd ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( ( √ ‘ 𝐷 ) · 𝐵 ) = 0 )
63 56 62 oveq12d ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = ( 1 + 0 ) )
64 1p0e1 ( 1 + 0 ) = 1
65 63 64 eqtrdi ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) = 1 )
66 30 65 breqtrd ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → 1 < 1 )
67 18 ltnri ¬ 1 < 1
68 pm2.24 ( 1 < 1 → ( ¬ 1 < 1 → 1 ≤ 𝐵 ) )
69 66 67 68 mpisyl ( ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) ∧ 𝐵 = 0 ) → 1 ≤ 𝐵 )
70 simplrr ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 𝐵 ∈ ℕ0 )
71 elnn0 ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) )
72 70 71 sylib ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) )
73 29 69 72 mpjaodan ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 1 ≤ 𝐵 )
74 nn0ge0 ( 𝐵 ∈ ℕ0 → 0 ≤ 𝐵 )
75 74 adantl ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) → 0 ≤ 𝐵 )
76 75 ad2antlr ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 0 ≤ 𝐵 )
77 19 15 52 76 le2sqd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 1 ≤ 𝐵 ↔ ( 1 ↑ 2 ) ≤ ( 𝐵 ↑ 2 ) ) )
78 73 77 mpbid ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 1 ↑ 2 ) ≤ ( 𝐵 ↑ 2 ) )
79 27 78 eqbrtrrd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 1 ≤ ( 𝐵 ↑ 2 ) )
80 19 20 suble0d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( 1 − ( 𝐵 ↑ 2 ) ) ≤ 0 ↔ 1 ≤ ( 𝐵 ↑ 2 ) ) )
81 79 80 mpbird ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 1 − ( 𝐵 ↑ 2 ) ) ≤ 0 )
82 21 23 2 lemul2d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( 1 − ( 𝐵 ↑ 2 ) ) ≤ 0 ↔ ( 𝐷 · ( 1 − ( 𝐵 ↑ 2 ) ) ) ≤ ( 𝐷 · 0 ) ) )
83 81 82 mpbid ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 · ( 1 − ( 𝐵 ↑ 2 ) ) ) ≤ ( 𝐷 · 0 ) )
84 22 24 25 83 leadd2dd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐷 · ( 1 − ( 𝐵 ↑ 2 ) ) ) ) ≤ ( ( 𝐴 ↑ 2 ) + ( 𝐷 · 0 ) ) )
85 5 rpcnd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 + 1 ) ∈ ℂ )
86 85 sqsqrtd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ ( 𝐷 + 1 ) ) ↑ 2 ) = ( 𝐷 + 1 ) )
87 simprr ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 )
88 87 eqcomd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 1 = ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) )
89 88 oveq2d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 + 1 ) = ( 𝐷 + ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) ) )
90 15 recnd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 𝐵 ∈ ℂ )
91 90 sqcld ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
92 36 91 mulcld ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 · ( 𝐵 ↑ 2 ) ) ∈ ℂ )
93 36 43 92 addsub12d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 + ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐷 − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) ) )
94 19 recnd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 1 ∈ ℂ )
95 36 94 91 subdid ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 · ( 1 − ( 𝐵 ↑ 2 ) ) ) = ( ( 𝐷 · 1 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) )
96 36 mulid1d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 · 1 ) = 𝐷 )
97 96 oveq1d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝐷 · 1 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = ( 𝐷 − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) )
98 95 97 eqtr2d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = ( 𝐷 · ( 1 − ( 𝐵 ↑ 2 ) ) ) )
99 98 oveq2d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐷 − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐷 · ( 1 − ( 𝐵 ↑ 2 ) ) ) ) )
100 93 99 eqtrd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 + ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐷 · ( 1 − ( 𝐵 ↑ 2 ) ) ) ) )
101 86 89 100 3eqtrd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ ( 𝐷 + 1 ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐷 · ( 1 − ( 𝐵 ↑ 2 ) ) ) ) )
102 36 mul01d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 · 0 ) = 0 )
103 102 oveq2d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐷 · 0 ) ) = ( ( 𝐴 ↑ 2 ) + 0 ) )
104 43 addid1d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝐴 ↑ 2 ) + 0 ) = ( 𝐴 ↑ 2 ) )
105 103 104 eqtr2d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 𝐴 ↑ 2 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐷 · 0 ) ) )
106 84 101 105 3brtr4d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ ( 𝐷 + 1 ) ) ↑ 2 ) ≤ ( 𝐴 ↑ 2 ) )
107 6 rpge0d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → 0 ≤ ( √ ‘ ( 𝐷 + 1 ) ) )
108 7 12 107 50 le2sqd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ ( 𝐷 + 1 ) ) ≤ 𝐴 ↔ ( ( √ ‘ ( 𝐷 + 1 ) ) ↑ 2 ) ≤ ( 𝐴 ↑ 2 ) ) )
109 106 108 mpbird ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( √ ‘ ( 𝐷 + 1 ) ) ≤ 𝐴 )
110 59 mulid1d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ 𝐷 ) · 1 ) = ( √ ‘ 𝐷 ) )
111 19 15 8 lemul2d ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( 1 ≤ 𝐵 ↔ ( ( √ ‘ 𝐷 ) · 1 ) ≤ ( ( √ ‘ 𝐷 ) · 𝐵 ) ) )
112 73 111 mpbid ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ 𝐷 ) · 1 ) ≤ ( ( √ ‘ 𝐷 ) · 𝐵 ) )
113 110 112 eqbrtrrd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( √ ‘ 𝐷 ) ≤ ( ( √ ‘ 𝐷 ) · 𝐵 ) )
114 7 9 12 16 109 113 le2addd ( ( ( 𝐷 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) ) ∧ ( 1 < ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) ∧ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ ( 𝐴 + ( ( √ ‘ 𝐷 ) · 𝐵 ) ) )