Proof of Theorem pellexlem1
| Step | Hyp | Ref
| Expression |
| 1 | | nncn 12274 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) |
| 2 | 1 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℂ) |
| 3 | 2 | sqcld 14184 |
. . . . 5
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴↑2) ∈
ℂ) |
| 4 | | nncn 12274 |
. . . . . . 7
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℂ) |
| 5 | 4 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐷 ∈
ℂ) |
| 6 | | nncn 12274 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
| 7 | 6 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℂ) |
| 8 | 7 | sqcld 14184 |
. . . . . 6
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵↑2) ∈
ℂ) |
| 9 | 5, 8 | mulcld 11281 |
. . . . 5
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐷 · (𝐵↑2)) ∈ ℂ) |
| 10 | 3, 9 | subeq0ad 11630 |
. . . 4
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) = 0 ↔ (𝐴↑2) = (𝐷 · (𝐵↑2)))) |
| 11 | | nnne0 12300 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0) |
| 12 | 11 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ≠ 0) |
| 13 | | sqne0 14163 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ → ((𝐵↑2) ≠ 0 ↔ 𝐵 ≠ 0)) |
| 14 | 7, 13 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐵↑2) ≠ 0 ↔ 𝐵 ≠ 0)) |
| 15 | 12, 14 | mpbird 257 |
. . . . . 6
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵↑2) ≠
0) |
| 16 | 3, 5, 8, 15 | divmul3d 12077 |
. . . . 5
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴↑2) / (𝐵↑2)) = 𝐷 ↔ (𝐴↑2) = (𝐷 · (𝐵↑2)))) |
| 17 | | sqdiv 14161 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) |
| 18 | 17 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) →
(√‘((𝐴 / 𝐵)↑2)) =
(√‘((𝐴↑2)
/ (𝐵↑2)))) |
| 19 | 2, 7, 12, 18 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(√‘((𝐴 / 𝐵)↑2)) =
(√‘((𝐴↑2)
/ (𝐵↑2)))) |
| 20 | | nnre 12273 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
| 21 | 20 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℝ) |
| 22 | | nnre 12273 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
| 23 | 22 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℝ) |
| 24 | 21, 23, 12 | redivcld 12095 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℝ) |
| 25 | | nnnn0 12533 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
| 26 | 25 | nn0ge0d 12590 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ → 0 ≤
𝐴) |
| 27 | 26 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 0 ≤
𝐴) |
| 28 | | nngt0 12297 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℕ → 0 <
𝐵) |
| 29 | 28 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 0 <
𝐵) |
| 30 | | divge0 12137 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵)) |
| 31 | 21, 27, 23, 29, 30 | syl22anc 839 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 0 ≤
(𝐴 / 𝐵)) |
| 32 | 24, 31 | sqrtsqd 15458 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(√‘((𝐴 / 𝐵)↑2)) = (𝐴 / 𝐵)) |
| 33 | 19, 32 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(√‘((𝐴↑2)
/ (𝐵↑2))) = (𝐴 / 𝐵)) |
| 34 | | nnq 13004 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℚ) |
| 35 | 34 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℚ) |
| 36 | | nnq 13004 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℚ) |
| 37 | 36 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℚ) |
| 38 | | qdivcl 13012 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ) |
| 39 | 35, 37, 12, 38 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) |
| 40 | 33, 39 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(√‘((𝐴↑2)
/ (𝐵↑2))) ∈
ℚ) |
| 41 | | fveq2 6906 |
. . . . . . 7
⊢ (((𝐴↑2) / (𝐵↑2)) = 𝐷 → (√‘((𝐴↑2) / (𝐵↑2))) = (√‘𝐷)) |
| 42 | 41 | eleq1d 2826 |
. . . . . 6
⊢ (((𝐴↑2) / (𝐵↑2)) = 𝐷 → ((√‘((𝐴↑2) / (𝐵↑2))) ∈ ℚ ↔
(√‘𝐷) ∈
ℚ)) |
| 43 | 40, 42 | syl5ibcom 245 |
. . . . 5
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴↑2) / (𝐵↑2)) = 𝐷 → (√‘𝐷) ∈ ℚ)) |
| 44 | 16, 43 | sylbird 260 |
. . . 4
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴↑2) = (𝐷 · (𝐵↑2)) → (√‘𝐷) ∈
ℚ)) |
| 45 | 10, 44 | sylbid 240 |
. . 3
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) = 0 → (√‘𝐷) ∈
ℚ)) |
| 46 | 45 | necon3bd 2954 |
. 2
⊢ ((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (¬
(√‘𝐷) ∈
ℚ → ((𝐴↑2)
− (𝐷 · (𝐵↑2))) ≠
0)) |
| 47 | 46 | imp 406 |
1
⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ ¬
(√‘𝐷) ∈
ℚ) → ((𝐴↑2)
− (𝐷 · (𝐵↑2))) ≠
0) |