Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pell1qrgaplem Structured version   Visualization version   GIF version

Theorem pell1qrgaplem 42565
Description: Lemma for pell1qrgap 42566. (Contributed by Stefan O'Rear, 18-Sep-2014.)
Assertion
Ref Expression
pell1qrgaplem (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (𝐴 + ((√‘𝐷) · 𝐵)))

Proof of Theorem pell1qrgaplem
StepHypRef Expression
1 nnrp 13031 . . . . . 6 (𝐷 ∈ ℕ → 𝐷 ∈ ℝ+)
21ad2antrr 724 . . . . 5 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 𝐷 ∈ ℝ+)
3 1rp 13024 . . . . . 6 1 ∈ ℝ+
43a1i 11 . . . . 5 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 1 ∈ ℝ+)
52, 4rpaddcld 13077 . . . 4 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 + 1) ∈ ℝ+)
65rpsqrtcld 15409 . . 3 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (√‘(𝐷 + 1)) ∈ ℝ+)
76rpred 13062 . 2 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (√‘(𝐷 + 1)) ∈ ℝ)
82rpsqrtcld 15409 . . 3 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (√‘𝐷) ∈ ℝ+)
98rpred 13062 . 2 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (√‘𝐷) ∈ ℝ)
10 nn0re 12525 . . . 4 (𝐴 ∈ ℕ0𝐴 ∈ ℝ)
1110adantr 479 . . 3 ((𝐴 ∈ ℕ0𝐵 ∈ ℕ0) → 𝐴 ∈ ℝ)
1211ad2antlr 725 . 2 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 𝐴 ∈ ℝ)
13 nn0re 12525 . . . . 5 (𝐵 ∈ ℕ0𝐵 ∈ ℝ)
1413adantl 480 . . . 4 ((𝐴 ∈ ℕ0𝐵 ∈ ℕ0) → 𝐵 ∈ ℝ)
1514ad2antlr 725 . . 3 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 𝐵 ∈ ℝ)
169, 15remulcld 11283 . 2 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘𝐷) · 𝐵) ∈ ℝ)
172rpred 13062 . . . . . 6 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 𝐷 ∈ ℝ)
18 1re 11253 . . . . . . . 8 1 ∈ ℝ
1918a1i 11 . . . . . . 7 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 1 ∈ ℝ)
2015resqcld 14136 . . . . . . 7 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐵↑2) ∈ ℝ)
2119, 20resubcld 11681 . . . . . 6 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (1 − (𝐵↑2)) ∈ ℝ)
2217, 21remulcld 11283 . . . . 5 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 · (1 − (𝐵↑2))) ∈ ℝ)
23 0red 11256 . . . . . 6 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 0 ∈ ℝ)
2417, 23remulcld 11283 . . . . 5 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 · 0) ∈ ℝ)
2512resqcld 14136 . . . . 5 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐴↑2) ∈ ℝ)
26 sq1 14205 . . . . . . . . 9 (1↑2) = 1
2726a1i 11 . . . . . . . 8 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (1↑2) = 1)
28 nnge1 12284 . . . . . . . . . . 11 (𝐵 ∈ ℕ → 1 ≤ 𝐵)
2928adantl 480 . . . . . . . . . 10 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 ∈ ℕ) → 1 ≤ 𝐵)
30 simplrl 775 . . . . . . . . . . . 12 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → 1 < (𝐴 + ((√‘𝐷) · 𝐵)))
31 oveq1 7421 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 = 0 → (𝐵↑2) = (0↑2))
3231adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → (𝐵↑2) = (0↑2))
33 sq0 14202 . . . . . . . . . . . . . . . . . . . . 21 (0↑2) = 0
3432, 33eqtrdi 2782 . . . . . . . . . . . . . . . . . . . 20 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → (𝐵↑2) = 0)
3534oveq2d 7430 . . . . . . . . . . . . . . . . . . 19 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → (𝐷 · (𝐵↑2)) = (𝐷 · 0))
362rpcnd 13064 . . . . . . . . . . . . . . . . . . . . 21 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 𝐷 ∈ ℂ)
3736adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → 𝐷 ∈ ℂ)
3837mul01d 11452 . . . . . . . . . . . . . . . . . . 19 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → (𝐷 · 0) = 0)
3935, 38eqtrd 2766 . . . . . . . . . . . . . . . . . 18 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → (𝐷 · (𝐵↑2)) = 0)
4039oveq2d 7430 . . . . . . . . . . . . . . . . 17 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = ((𝐴↑2) − 0))
41 simplrr 776 . . . . . . . . . . . . . . . . 17 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)
4212recnd 11281 . . . . . . . . . . . . . . . . . . . 20 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 𝐴 ∈ ℂ)
4342sqcld 14155 . . . . . . . . . . . . . . . . . . 19 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐴↑2) ∈ ℂ)
4443adantr 479 . . . . . . . . . . . . . . . . . 18 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → (𝐴↑2) ∈ ℂ)
4544subid1d 11599 . . . . . . . . . . . . . . . . 17 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → ((𝐴↑2) − 0) = (𝐴↑2))
4640, 41, 453eqtr3d 2774 . . . . . . . . . . . . . . . 16 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → 1 = (𝐴↑2))
4726, 46eqtr2id 2779 . . . . . . . . . . . . . . 15 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → (𝐴↑2) = (1↑2))
48 nn0ge0 12541 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℕ0 → 0 ≤ 𝐴)
4948adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℕ0𝐵 ∈ ℕ0) → 0 ≤ 𝐴)
5049ad2antlr 725 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 0 ≤ 𝐴)
51 0le1 11776 . . . . . . . . . . . . . . . . . 18 0 ≤ 1
5251a1i 11 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 0 ≤ 1)
53 sq11 14142 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → ((𝐴↑2) = (1↑2) ↔ 𝐴 = 1))
5412, 50, 19, 52, 53syl22anc 837 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((𝐴↑2) = (1↑2) ↔ 𝐴 = 1))
5554adantr 479 . . . . . . . . . . . . . . 15 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → ((𝐴↑2) = (1↑2) ↔ 𝐴 = 1))
5647, 55mpbid 231 . . . . . . . . . . . . . 14 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → 𝐴 = 1)
57 simpr 483 . . . . . . . . . . . . . . . 16 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → 𝐵 = 0)
5857oveq2d 7430 . . . . . . . . . . . . . . 15 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → ((√‘𝐷) · 𝐵) = ((√‘𝐷) · 0))
598rpcnd 13064 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (√‘𝐷) ∈ ℂ)
6059adantr 479 . . . . . . . . . . . . . . . 16 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → (√‘𝐷) ∈ ℂ)
6160mul01d 11452 . . . . . . . . . . . . . . 15 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → ((√‘𝐷) · 0) = 0)
6258, 61eqtrd 2766 . . . . . . . . . . . . . 14 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → ((√‘𝐷) · 𝐵) = 0)
6356, 62oveq12d 7432 . . . . . . . . . . . . 13 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → (𝐴 + ((√‘𝐷) · 𝐵)) = (1 + 0))
64 1p0e1 12380 . . . . . . . . . . . . 13 (1 + 0) = 1
6563, 64eqtrdi 2782 . . . . . . . . . . . 12 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → (𝐴 + ((√‘𝐷) · 𝐵)) = 1)
6630, 65breqtrd 5170 . . . . . . . . . . 11 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → 1 < 1)
6718ltnri 11362 . . . . . . . . . . 11 ¬ 1 < 1
68 pm2.24 124 . . . . . . . . . . 11 (1 < 1 → (¬ 1 < 1 → 1 ≤ 𝐵))
6966, 67, 68mpisyl 21 . . . . . . . . . 10 ((((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) ∧ 𝐵 = 0) → 1 ≤ 𝐵)
70 simplrr 776 . . . . . . . . . . 11 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 𝐵 ∈ ℕ0)
71 elnn0 12518 . . . . . . . . . . 11 (𝐵 ∈ ℕ0 ↔ (𝐵 ∈ ℕ ∨ 𝐵 = 0))
7270, 71sylib 217 . . . . . . . . . 10 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐵 ∈ ℕ ∨ 𝐵 = 0))
7329, 69, 72mpjaodan 956 . . . . . . . . 9 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 1 ≤ 𝐵)
74 nn0ge0 12541 . . . . . . . . . . . 12 (𝐵 ∈ ℕ0 → 0 ≤ 𝐵)
7574adantl 480 . . . . . . . . . . 11 ((𝐴 ∈ ℕ0𝐵 ∈ ℕ0) → 0 ≤ 𝐵)
7675ad2antlr 725 . . . . . . . . . 10 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 0 ≤ 𝐵)
7719, 15, 52, 76le2sqd 14267 . . . . . . . . 9 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (1 ≤ 𝐵 ↔ (1↑2) ≤ (𝐵↑2)))
7873, 77mpbid 231 . . . . . . . 8 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (1↑2) ≤ (𝐵↑2))
7927, 78eqbrtrrd 5168 . . . . . . 7 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 1 ≤ (𝐵↑2))
8019, 20suble0d 11844 . . . . . . 7 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((1 − (𝐵↑2)) ≤ 0 ↔ 1 ≤ (𝐵↑2)))
8179, 80mpbird 256 . . . . . 6 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (1 − (𝐵↑2)) ≤ 0)
8221, 23, 2lemul2d 13106 . . . . . 6 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((1 − (𝐵↑2)) ≤ 0 ↔ (𝐷 · (1 − (𝐵↑2))) ≤ (𝐷 · 0)))
8381, 82mpbid 231 . . . . 5 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 · (1 − (𝐵↑2))) ≤ (𝐷 · 0))
8422, 24, 25, 83leadd2dd 11868 . . . 4 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((𝐴↑2) + (𝐷 · (1 − (𝐵↑2)))) ≤ ((𝐴↑2) + (𝐷 · 0)))
855rpcnd 13064 . . . . . 6 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 + 1) ∈ ℂ)
8685sqsqrtd 15437 . . . . 5 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘(𝐷 + 1))↑2) = (𝐷 + 1))
87 simprr 771 . . . . . . 7 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)
8887eqcomd 2732 . . . . . 6 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 1 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
8988oveq2d 7430 . . . . 5 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 + 1) = (𝐷 + ((𝐴↑2) − (𝐷 · (𝐵↑2)))))
9015recnd 11281 . . . . . . . . 9 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 𝐵 ∈ ℂ)
9190sqcld 14155 . . . . . . . 8 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐵↑2) ∈ ℂ)
9236, 91mulcld 11273 . . . . . . 7 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 · (𝐵↑2)) ∈ ℂ)
9336, 43, 92addsub12d 11633 . . . . . 6 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 + ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = ((𝐴↑2) + (𝐷 − (𝐷 · (𝐵↑2)))))
9419recnd 11281 . . . . . . . . 9 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 1 ∈ ℂ)
9536, 94, 91subdid 11709 . . . . . . . 8 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 · (1 − (𝐵↑2))) = ((𝐷 · 1) − (𝐷 · (𝐵↑2))))
9636mulridd 11270 . . . . . . . . 9 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 · 1) = 𝐷)
9796oveq1d 7429 . . . . . . . 8 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((𝐷 · 1) − (𝐷 · (𝐵↑2))) = (𝐷 − (𝐷 · (𝐵↑2))))
9895, 97eqtr2d 2767 . . . . . . 7 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 − (𝐷 · (𝐵↑2))) = (𝐷 · (1 − (𝐵↑2))))
9998oveq2d 7430 . . . . . 6 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((𝐴↑2) + (𝐷 − (𝐷 · (𝐵↑2)))) = ((𝐴↑2) + (𝐷 · (1 − (𝐵↑2)))))
10093, 99eqtrd 2766 . . . . 5 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 + ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = ((𝐴↑2) + (𝐷 · (1 − (𝐵↑2)))))
10186, 89, 1003eqtrd 2770 . . . 4 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘(𝐷 + 1))↑2) = ((𝐴↑2) + (𝐷 · (1 − (𝐵↑2)))))
10236mul01d 11452 . . . . . 6 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐷 · 0) = 0)
103102oveq2d 7430 . . . . 5 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((𝐴↑2) + (𝐷 · 0)) = ((𝐴↑2) + 0))
10443addridd 11453 . . . . 5 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((𝐴↑2) + 0) = (𝐴↑2))
105103, 104eqtr2d 2767 . . . 4 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (𝐴↑2) = ((𝐴↑2) + (𝐷 · 0)))
10684, 101, 1053brtr4d 5176 . . 3 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘(𝐷 + 1))↑2) ≤ (𝐴↑2))
1076rpge0d 13066 . . . 4 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → 0 ≤ (√‘(𝐷 + 1)))
1087, 12, 107, 50le2sqd 14267 . . 3 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘(𝐷 + 1)) ≤ 𝐴 ↔ ((√‘(𝐷 + 1))↑2) ≤ (𝐴↑2)))
109106, 108mpbird 256 . 2 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (√‘(𝐷 + 1)) ≤ 𝐴)
11059mulridd 11270 . . 3 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘𝐷) · 1) = (√‘𝐷))
11119, 15, 8lemul2d 13106 . . . 4 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (1 ≤ 𝐵 ↔ ((√‘𝐷) · 1) ≤ ((√‘𝐷) · 𝐵)))
11273, 111mpbid 231 . . 3 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘𝐷) · 1) ≤ ((√‘𝐷) · 𝐵))
113110, 112eqbrtrrd 5168 . 2 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → (√‘𝐷) ≤ ((√‘𝐷) · 𝐵))
1147, 9, 12, 16, 109, 113le2addd 11872 1 (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (𝐴 + ((√‘𝐷) · 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845   = wceq 1534  wcel 2099   class class class wbr 5144  cfv 6544  (class class class)co 7414  cc 11145  cr 11146  0cc0 11147  1c1 11148   + caddc 11150   · cmul 11152   < clt 11287  cle 11288  cmin 11483  cn 12256  2c2 12311  0cn0 12516  +crp 13020  cexp 14073  csqrt 15231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7736  ax-cnex 11203  ax-resscn 11204  ax-1cn 11205  ax-icn 11206  ax-addcl 11207  ax-addrcl 11208  ax-mulcl 11209  ax-mulrcl 11210  ax-mulcom 11211  ax-addass 11212  ax-mulass 11213  ax-distr 11214  ax-i2m1 11215  ax-1ne0 11216  ax-1rid 11217  ax-rnegex 11218  ax-rrecex 11219  ax-cnre 11220  ax-pre-lttri 11221  ax-pre-lttrn 11222  ax-pre-ltadd 11223  ax-pre-mulgt0 11224  ax-pre-sup 11225
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3365  df-reu 3366  df-rab 3421  df-v 3465  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4324  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4907  df-iun 4996  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6303  df-ord 6369  df-on 6370  df-lim 6371  df-suc 6372  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7867  df-2nd 7994  df-frecs 8286  df-wrecs 8317  df-recs 8391  df-rdg 8430  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-sup 9476  df-pnf 11289  df-mnf 11290  df-xr 11291  df-ltxr 11292  df-le 11293  df-sub 11485  df-neg 11486  df-div 11911  df-nn 12257  df-2 12319  df-3 12320  df-n0 12517  df-z 12603  df-uz 12867  df-rp 13021  df-seq 14014  df-exp 14074  df-cj 15097  df-re 15098  df-im 15099  df-sqrt 15233  df-abs 15234
This theorem is referenced by:  pell1qrgap  42566
  Copyright terms: Public domain W3C validator