Proof of Theorem rmspecsqrtnqOLD
Step | Hyp | Ref
| Expression |
1 | | eluzelcn 11699 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℂ) |
2 | 1 | sqcld 13006 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴↑2) ∈ ℂ) |
3 | | ax-1cn 9994 |
. . . 4
⊢ 1 ∈
ℂ |
4 | | subcl 10280 |
. . . 4
⊢ (((𝐴↑2) ∈ ℂ ∧ 1
∈ ℂ) → ((𝐴↑2) − 1) ∈
ℂ) |
5 | 2, 3, 4 | sylancl 694 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℂ) |
6 | 5 | sqrtcld 14176 |
. 2
⊢ (𝐴 ∈
(ℤ≥‘2) → (√‘((𝐴↑2) − 1)) ∈
ℂ) |
7 | | eluz2nn 11726 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℕ) |
8 | 7 | nnsqcld 13029 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴↑2) ∈ ℕ) |
9 | | nnm1nn0 11334 |
. . . 4
⊢ ((𝐴↑2) ∈ ℕ →
((𝐴↑2) − 1)
∈ ℕ0) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℕ0) |
11 | | nnm1nn0 11334 |
. . . 4
⊢ (𝐴 ∈ ℕ → (𝐴 − 1) ∈
ℕ0) |
12 | 7, 11 | syl 17 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∈
ℕ0) |
13 | | binom2sub 12981 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 −
1)↑2) = (((𝐴↑2)
− (2 · (𝐴
· 1))) + (1↑2))) |
14 | 1, 3, 13 | sylancl 694 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴 − 1)↑2) = (((𝐴↑2) − (2 · (𝐴 · 1))) +
(1↑2))) |
15 | | 2re 11090 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
16 | | eluzelre 11698 |
. . . . . . . . 9
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℝ) |
17 | | 1re 10039 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
18 | | remulcl 10021 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐴 ·
1) ∈ ℝ) |
19 | 16, 17, 18 | sylancl 694 |
. . . . . . . 8
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 · 1) ∈
ℝ) |
20 | | remulcl 10021 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ (𝐴
· 1) ∈ ℝ) → (2 · (𝐴 · 1)) ∈
ℝ) |
21 | 15, 19, 20 | sylancr 695 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) → (2 · (𝐴 · 1)) ∈
ℝ) |
22 | 21 | recnd 10068 |
. . . . . 6
⊢ (𝐴 ∈
(ℤ≥‘2) → (2 · (𝐴 · 1)) ∈
ℂ) |
23 | 17 | resqcli 12949 |
. . . . . . . 8
⊢
(1↑2) ∈ ℝ |
24 | 23 | recni 10052 |
. . . . . . 7
⊢
(1↑2) ∈ ℂ |
25 | 24 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈
(ℤ≥‘2) → (1↑2) ∈
ℂ) |
26 | 2, 22, 25 | subsubd 10420 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − ((2 · (𝐴 · 1)) −
(1↑2))) = (((𝐴↑2)
− (2 · (𝐴
· 1))) + (1↑2))) |
27 | 14, 26 | eqtr4d 2659 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴 − 1)↑2) = ((𝐴↑2) − ((2 · (𝐴 · 1)) −
(1↑2)))) |
28 | 17 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → 1 ∈ ℝ) |
29 | | resubcl 10345 |
. . . . . 6
⊢ (((2
· (𝐴 · 1))
∈ ℝ ∧ (1↑2) ∈ ℝ) → ((2 · (𝐴 · 1)) −
(1↑2)) ∈ ℝ) |
30 | 21, 23, 29 | sylancl 694 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → ((2 · (𝐴 · 1)) − (1↑2)) ∈
ℝ) |
31 | 8 | nnred 11035 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴↑2) ∈ ℝ) |
32 | 3 | 2timesi 11147 |
. . . . . . . 8
⊢ (2
· 1) = (1 + 1) |
33 | | eluz2b2 11761 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) ↔ (𝐴 ∈ ℕ ∧ 1 < 𝐴)) |
34 | 33 | simprbi 480 |
. . . . . . . . 9
⊢ (𝐴 ∈
(ℤ≥‘2) → 1 < 𝐴) |
35 | 15 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → 2 ∈ ℝ) |
36 | | 2pos 11112 |
. . . . . . . . . . 11
⊢ 0 <
2 |
37 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → 0 < 2) |
38 | | ltmul2 10874 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 𝐴
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (1 < 𝐴 ↔ (2 · 1) < (2
· 𝐴))) |
39 | 28, 16, 35, 37, 38 | syl112anc 1330 |
. . . . . . . . 9
⊢ (𝐴 ∈
(ℤ≥‘2) → (1 < 𝐴 ↔ (2 · 1) < (2 ·
𝐴))) |
40 | 34, 39 | mpbid 222 |
. . . . . . . 8
⊢ (𝐴 ∈
(ℤ≥‘2) → (2 · 1) < (2 · 𝐴)) |
41 | 32, 40 | syl5eqbrr 4689 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) → (1 + 1) < (2 · 𝐴)) |
42 | | remulcl 10021 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ 𝐴
∈ ℝ) → (2 · 𝐴) ∈ ℝ) |
43 | 15, 16, 42 | sylancr 695 |
. . . . . . . 8
⊢ (𝐴 ∈
(ℤ≥‘2) → (2 · 𝐴) ∈ ℝ) |
44 | 28, 28, 43 | ltaddsubd 10627 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) → ((1 + 1) < (2 · 𝐴) ↔ 1 < ((2 ·
𝐴) −
1))) |
45 | 41, 44 | mpbid 222 |
. . . . . 6
⊢ (𝐴 ∈
(ℤ≥‘2) → 1 < ((2 · 𝐴) − 1)) |
46 | 1 | mulid1d 10057 |
. . . . . . . 8
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 · 1) = 𝐴) |
47 | 46 | oveq2d 6666 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) → (2 · (𝐴 · 1)) = (2 · 𝐴)) |
48 | | sq1 12958 |
. . . . . . . 8
⊢
(1↑2) = 1 |
49 | 48 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) → (1↑2) = 1) |
50 | 47, 49 | oveq12d 6668 |
. . . . . 6
⊢ (𝐴 ∈
(ℤ≥‘2) → ((2 · (𝐴 · 1)) − (1↑2)) = ((2
· 𝐴) −
1)) |
51 | 45, 50 | breqtrrd 4681 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → 1 < ((2 · (𝐴 · 1)) −
(1↑2))) |
52 | 28, 30, 31, 51 | ltsub2dd 10640 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − ((2 · (𝐴 · 1)) −
(1↑2))) < ((𝐴↑2) − 1)) |
53 | 27, 52 | eqbrtrd 4675 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴 − 1)↑2) < ((𝐴↑2) − 1)) |
54 | 31 | ltm1d 10956 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) < (𝐴↑2)) |
55 | | npcan 10290 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 −
1) + 1) = 𝐴) |
56 | 1, 3, 55 | sylancl 694 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴 − 1) + 1) = 𝐴) |
57 | 56 | oveq1d 6665 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → (((𝐴 − 1) + 1)↑2) = (𝐴↑2)) |
58 | 54, 57 | breqtrrd 4681 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) < (((𝐴 − 1) +
1)↑2)) |
59 | | nonsq 15467 |
. . 3
⊢
(((((𝐴↑2)
− 1) ∈ ℕ0 ∧ (𝐴 − 1) ∈ ℕ0)
∧ (((𝐴 −
1)↑2) < ((𝐴↑2)
− 1) ∧ ((𝐴↑2) − 1) < (((𝐴 − 1) + 1)↑2)))
→ ¬ (√‘((𝐴↑2) − 1)) ∈
ℚ) |
60 | 10, 12, 53, 58, 59 | syl22anc 1327 |
. 2
⊢ (𝐴 ∈
(ℤ≥‘2) → ¬ (√‘((𝐴↑2) − 1)) ∈
ℚ) |
61 | 6, 60 | eldifd 3585 |
1
⊢ (𝐴 ∈
(ℤ≥‘2) → (√‘((𝐴↑2) − 1)) ∈ (ℂ ∖
ℚ)) |