Proof of Theorem pellexlem1
Step | Hyp | Ref
| Expression |
1 | | nncn 11634 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) |
2 | 1 | 3ad2ant2 1126 |
. . . . . 6
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℂ) |
3 | 2 | sqcld 13496 |
. . . . 5
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴↑2) ∈
ℂ) |
4 | | nncn 11634 |
. . . . . . 7
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℂ) |
5 | 4 | 3ad2ant1 1125 |
. . . . . 6
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐷 ∈
ℂ) |
6 | | nncn 11634 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
7 | 6 | 3ad2ant3 1127 |
. . . . . . 7
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℂ) |
8 | 7 | sqcld 13496 |
. . . . . 6
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵↑2) ∈
ℂ) |
9 | 5, 8 | mulcld 10649 |
. . . . 5
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐷 · (𝐵↑2)) ∈ ℂ) |
10 | 3, 9 | subeq0ad 10995 |
. . . 4
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) = 0 ↔ (𝐴↑2) = (𝐷 · (𝐵↑2)))) |
11 | | nnne0 11659 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0) |
12 | 11 | 3ad2ant3 1127 |
. . . . . . 7
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ≠ 0) |
13 | | sqne0 13477 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ → ((𝐵↑2) ≠ 0 ↔ 𝐵 ≠ 0)) |
14 | 7, 13 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐵↑2) ≠ 0 ↔ 𝐵 ≠ 0)) |
15 | 12, 14 | mpbird 258 |
. . . . . 6
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵↑2) ≠
0) |
16 | 3, 5, 8, 15 | divmul3d 11438 |
. . . . 5
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴↑2) / (𝐵↑2)) = 𝐷 ↔ (𝐴↑2) = (𝐷 · (𝐵↑2)))) |
17 | | sqdiv 13475 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) |
18 | 17 | fveq2d 6667 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) →
(√‘((𝐴 / 𝐵)↑2)) =
(√‘((𝐴↑2)
/ (𝐵↑2)))) |
19 | 2, 7, 12, 18 | syl3anc 1363 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(√‘((𝐴 / 𝐵)↑2)) =
(√‘((𝐴↑2)
/ (𝐵↑2)))) |
20 | | nnre 11633 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
21 | 20 | 3ad2ant2 1126 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℝ) |
22 | | nnre 11633 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
23 | 22 | 3ad2ant3 1127 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℝ) |
24 | 21, 23, 12 | redivcld 11456 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℝ) |
25 | | nnnn0 11892 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
26 | 25 | nn0ge0d 11946 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ → 0 ≤
𝐴) |
27 | 26 | 3ad2ant2 1126 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 0 ≤
𝐴) |
28 | | nngt0 11656 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℕ → 0 <
𝐵) |
29 | 28 | 3ad2ant3 1127 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 0 <
𝐵) |
30 | | divge0 11497 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵)) |
31 | 21, 27, 23, 29, 30 | syl22anc 834 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 0 ≤
(𝐴 / 𝐵)) |
32 | 24, 31 | sqrtsqd 14767 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(√‘((𝐴 / 𝐵)↑2)) = (𝐴 / 𝐵)) |
33 | 19, 32 | eqtr3d 2855 |
. . . . . . 7
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(√‘((𝐴↑2)
/ (𝐵↑2))) = (𝐴 / 𝐵)) |
34 | | nnq 12349 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℚ) |
35 | 34 | 3ad2ant2 1126 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℚ) |
36 | | nnq 12349 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℚ) |
37 | 36 | 3ad2ant3 1127 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℚ) |
38 | | qdivcl 12357 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ) |
39 | 35, 37, 12, 38 | syl3anc 1363 |
. . . . . . 7
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) |
40 | 33, 39 | eqeltrd 2910 |
. . . . . 6
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(√‘((𝐴↑2)
/ (𝐵↑2))) ∈
ℚ) |
41 | | fveq2 6663 |
. . . . . . 7
⊢ (((𝐴↑2) / (𝐵↑2)) = 𝐷 → (√‘((𝐴↑2) / (𝐵↑2))) = (√‘𝐷)) |
42 | 41 | eleq1d 2894 |
. . . . . 6
⊢ (((𝐴↑2) / (𝐵↑2)) = 𝐷 → ((√‘((𝐴↑2) / (𝐵↑2))) ∈ ℚ ↔
(√‘𝐷) ∈
ℚ)) |
43 | 40, 42 | syl5ibcom 246 |
. . . . 5
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴↑2) / (𝐵↑2)) = 𝐷 → (√‘𝐷) ∈ ℚ)) |
44 | 16, 43 | sylbird 261 |
. . . 4
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴↑2) = (𝐷 · (𝐵↑2)) → (√‘𝐷) ∈
ℚ)) |
45 | 10, 44 | sylbid 241 |
. . 3
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) = 0 → (√‘𝐷) ∈
ℚ)) |
46 | 45 | necon3bd 3027 |
. 2
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (¬
(√‘𝐷) ∈
ℚ → ((𝐴↑2)
− (𝐷 · (𝐵↑2))) ≠
0)) |
47 | 46 | imp 407 |
1
⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ ¬
(√‘𝐷) ∈
ℚ) → ((𝐴↑2)
− (𝐷 · (𝐵↑2))) ≠
0) |