Proof of Theorem rmxyadd
| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐴 ∈
(ℤ≥‘2)) |
| 2 | | zaddcl 12657 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
| 3 | 2 | 3adant1 1131 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
| 4 | | rmxyval 42927 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝐴 Xrm (𝑀 + 𝑁)) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm (𝑀 + 𝑁)))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑(𝑀 + 𝑁))) |
| 5 | 1, 3, 4 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm (𝑀 + 𝑁)) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm (𝑀 + 𝑁)))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑(𝑀 + 𝑁))) |
| 6 | | eluzelz 12888 |
. . . . . . . 8
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℤ) |
| 7 | 6 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐴 ∈ ℤ) |
| 8 | 7 | zcnd 12723 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐴 ∈ ℂ) |
| 9 | | zq 12996 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℚ) |
| 10 | | qsqcl 14170 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℚ → (𝐴↑2) ∈
ℚ) |
| 11 | 7, 9, 10 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴↑2) ∈ ℚ) |
| 12 | | zssq 12998 |
. . . . . . . . . . 11
⊢ ℤ
⊆ ℚ |
| 13 | | 1z 12647 |
. . . . . . . . . . 11
⊢ 1 ∈
ℤ |
| 14 | 12, 13 | sselii 3980 |
. . . . . . . . . 10
⊢ 1 ∈
ℚ |
| 15 | 14 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 1 ∈
ℚ) |
| 16 | | qsubcl 13010 |
. . . . . . . . 9
⊢ (((𝐴↑2) ∈ ℚ ∧ 1
∈ ℚ) → ((𝐴↑2) − 1) ∈
ℚ) |
| 17 | 11, 15, 16 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴↑2) − 1) ∈
ℚ) |
| 18 | | qcn 13005 |
. . . . . . . 8
⊢ (((𝐴↑2) − 1) ∈
ℚ → ((𝐴↑2)
− 1) ∈ ℂ) |
| 19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴↑2) − 1) ∈
ℂ) |
| 20 | 19 | sqrtcld 15476 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(√‘((𝐴↑2)
− 1)) ∈ ℂ) |
| 21 | 8, 20 | addcld 11280 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 + (√‘((𝐴↑2) − 1))) ∈
ℂ) |
| 22 | | rmbaserp 42931 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 + (√‘((𝐴↑2) − 1))) ∈
ℝ+) |
| 23 | 22 | rpne0d 13082 |
. . . . . 6
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 + (√‘((𝐴↑2) − 1))) ≠
0) |
| 24 | 23 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 + (√‘((𝐴↑2) − 1))) ≠
0) |
| 25 | | simp2 1138 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ) |
| 26 | | simp3 1139 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ) |
| 27 | | expaddz 14147 |
. . . . 5
⊢ ((((𝐴 + (√‘((𝐴↑2) − 1))) ∈
ℂ ∧ (𝐴 +
(√‘((𝐴↑2)
− 1))) ≠ 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 + (√‘((𝐴↑2) − 1)))↑(𝑀 + 𝑁)) = (((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑀) · ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁))) |
| 28 | 21, 24, 25, 26, 27 | syl22anc 839 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 + (√‘((𝐴↑2) − 1)))↑(𝑀 + 𝑁)) = (((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑀) · ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁))) |
| 29 | | frmx 42925 |
. . . . . . . . 9
⊢
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 |
| 30 | 29 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → Xrm
:((ℤ≥‘2) ×
ℤ)⟶ℕ0) |
| 31 | 30, 1, 25 | fovcdmd 7605 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑀) ∈
ℕ0) |
| 32 | 31 | nn0cnd 12589 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑀) ∈ ℂ) |
| 33 | | frmy 42926 |
. . . . . . . . . 10
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
| 34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → Yrm
:((ℤ≥‘2) ×
ℤ)⟶ℤ) |
| 35 | 34, 1, 25 | fovcdmd 7605 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ) |
| 36 | 35 | zcnd 12723 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℂ) |
| 37 | 20, 36 | mulcld 11281 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑀)) ∈
ℂ) |
| 38 | 30, 1, 26 | fovcdmd 7605 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
| 39 | 38 | nn0cnd 12589 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℂ) |
| 40 | 34, 1, 26 | fovcdmd 7605 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ) |
| 41 | 40 | zcnd 12723 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℂ) |
| 42 | 20, 41 | mulcld 11281 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑁)) ∈
ℂ) |
| 43 | 32, 37, 39, 42 | muladdd 11721 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑀) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑀))) · ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)))) = ((((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)) ·
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑀)))) +
(((𝐴 Xrm 𝑀) ·
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑁))) +
((𝐴 Xrm 𝑁) ·
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑀)))))) |
| 44 | | rmxyval 42927 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → ((𝐴 Xrm 𝑀) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑀))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑀)) |
| 45 | 1, 25, 44 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑀) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑀))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑀)) |
| 46 | | rmxyval 42927 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)) |
| 47 | 1, 26, 46 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)) |
| 48 | 45, 47 | oveq12d 7449 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑀) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑀))) · ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)))) = (((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑀) · ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁))) |
| 49 | 43, 48 | eqtr3d 2779 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)) ·
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑀)))) +
(((𝐴 Xrm 𝑀) ·
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑁))) +
((𝐴 Xrm 𝑁) ·
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑀))))) =
(((𝐴 +
(√‘((𝐴↑2)
− 1)))↑𝑀)
· ((𝐴 +
(√‘((𝐴↑2)
− 1)))↑𝑁))) |
| 50 | 20, 41, 20, 36 | mul4d 11473 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)) ·
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑀))) =
(((√‘((𝐴↑2) − 1)) ·
(√‘((𝐴↑2)
− 1))) · ((𝐴
Yrm 𝑁) ·
(𝐴 Yrm 𝑀)))) |
| 51 | 19 | msqsqrtd 15479 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((√‘((𝐴↑2)
− 1)) · (√‘((𝐴↑2) − 1))) = ((𝐴↑2) − 1)) |
| 52 | 41, 36 | mulcomd 11282 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑀)) = ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁))) |
| 53 | 51, 52 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(((√‘((𝐴↑2) − 1)) ·
(√‘((𝐴↑2)
− 1))) · ((𝐴
Yrm 𝑁) ·
(𝐴 Yrm 𝑀))) = (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) |
| 54 | 50, 53 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)) ·
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑀))) =
(((𝐴↑2) − 1)
· ((𝐴 Yrm
𝑀) · (𝐴 Yrm 𝑁)))) |
| 55 | 54 | oveq2d 7447 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)) ·
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑀)))) =
(((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁))))) |
| 56 | 32, 20, 41 | mul12d 11470 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑀) · ((√‘((𝐴↑2) − 1)) ·
(𝐴 Yrm 𝑁))) = ((√‘((𝐴↑2) − 1)) ·
((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)))) |
| 57 | 39, 20, 36 | mul12d 11470 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) · ((√‘((𝐴↑2) − 1)) ·
(𝐴 Yrm 𝑀))) = ((√‘((𝐴↑2) − 1)) ·
((𝐴 Xrm 𝑁) · (𝐴 Yrm 𝑀)))) |
| 58 | 56, 57 | oveq12d 7449 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑀) · ((√‘((𝐴↑2) − 1)) ·
(𝐴 Yrm 𝑁))) + ((𝐴 Xrm 𝑁) · ((√‘((𝐴↑2) − 1)) ·
(𝐴 Yrm 𝑀)))) = (((√‘((𝐴↑2) − 1)) ·
((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))) + ((√‘((𝐴↑2) − 1)) · ((𝐴 Xrm 𝑁) · (𝐴 Yrm 𝑀))))) |
| 59 | 32, 41 | mulcld 11281 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)) ∈ ℂ) |
| 60 | 39, 36 | mulcld 11281 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) · (𝐴 Yrm 𝑀)) ∈ ℂ) |
| 61 | 20, 59, 60 | adddid 11285 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((√‘((𝐴↑2)
− 1)) · (((𝐴
Xrm 𝑀) ·
(𝐴 Yrm 𝑁)) + ((𝐴 Xrm 𝑁) · (𝐴 Yrm 𝑀)))) = (((√‘((𝐴↑2) − 1)) · ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))) + ((√‘((𝐴↑2) − 1)) · ((𝐴 Xrm 𝑁) · (𝐴 Yrm 𝑀))))) |
| 62 | 59, 60 | addcomd 11463 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)) + ((𝐴 Xrm 𝑁) · (𝐴 Yrm 𝑀))) = (((𝐴 Xrm 𝑁) · (𝐴 Yrm 𝑀)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)))) |
| 63 | 39, 36 | mulcomd 11282 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) · (𝐴 Yrm 𝑀)) = ((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁))) |
| 64 | 63 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑁) · (𝐴 Yrm 𝑀)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))) = (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)))) |
| 65 | 62, 64 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)) + ((𝐴 Xrm 𝑁) · (𝐴 Yrm 𝑀))) = (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)))) |
| 66 | 65 | oveq2d 7447 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((√‘((𝐴↑2)
− 1)) · (((𝐴
Xrm 𝑀) ·
(𝐴 Yrm 𝑁)) + ((𝐴 Xrm 𝑁) · (𝐴 Yrm 𝑀)))) = ((√‘((𝐴↑2) − 1)) · (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))))) |
| 67 | 58, 61, 66 | 3eqtr2d 2783 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑀) · ((√‘((𝐴↑2) − 1)) ·
(𝐴 Yrm 𝑁))) + ((𝐴 Xrm 𝑁) · ((√‘((𝐴↑2) − 1)) ·
(𝐴 Yrm 𝑀)))) = ((√‘((𝐴↑2) − 1)) ·
(((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))))) |
| 68 | 55, 67 | oveq12d 7449 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)) ·
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑀)))) +
(((𝐴 Xrm 𝑀) ·
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑁))) +
((𝐴 Xrm 𝑁) ·
((√‘((𝐴↑2)
− 1)) · (𝐴
Yrm 𝑀))))) =
((((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) + ((√‘((𝐴↑2) − 1)) · (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)))))) |
| 69 | 28, 49, 68 | 3eqtr2d 2783 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 + (√‘((𝐴↑2) − 1)))↑(𝑀 + 𝑁)) = ((((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) + ((√‘((𝐴↑2) − 1)) · (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)))))) |
| 70 | 5, 69 | eqtrd 2777 |
. 2
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm (𝑀 + 𝑁)) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm (𝑀 + 𝑁)))) = ((((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) + ((√‘((𝐴↑2) − 1)) · (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)))))) |
| 71 | | rmspecsqrtnq 42917 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → (√‘((𝐴↑2) − 1)) ∈ (ℂ ∖
ℚ)) |
| 72 | 71 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(√‘((𝐴↑2)
− 1)) ∈ (ℂ ∖ ℚ)) |
| 73 | | nn0ssq 12999 |
. . . 4
⊢
ℕ0 ⊆ ℚ |
| 74 | 30, 1, 3 | fovcdmd 7605 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm (𝑀 + 𝑁)) ∈
ℕ0) |
| 75 | 73, 74 | sselid 3981 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm (𝑀 + 𝑁)) ∈ ℚ) |
| 76 | 34, 1, 3 | fovcdmd 7605 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm (𝑀 + 𝑁)) ∈ ℤ) |
| 77 | 12, 76 | sselid 3981 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm (𝑀 + 𝑁)) ∈ ℚ) |
| 78 | 73, 31 | sselid 3981 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑀) ∈ ℚ) |
| 79 | 73, 38 | sselid 3981 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℚ) |
| 80 | | qmulcl 13009 |
. . . . 5
⊢ (((𝐴 Xrm 𝑀) ∈ ℚ ∧ (𝐴 Xrm 𝑁) ∈ ℚ) → ((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) ∈ ℚ) |
| 81 | 78, 79, 80 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) ∈ ℚ) |
| 82 | 12, 35 | sselid 3981 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℚ) |
| 83 | 12, 40 | sselid 3981 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℚ) |
| 84 | | qmulcl 13009 |
. . . . . 6
⊢ (((𝐴 Yrm 𝑀) ∈ ℚ ∧ (𝐴 Yrm 𝑁) ∈ ℚ) → ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)) ∈ ℚ) |
| 85 | 82, 83, 84 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)) ∈ ℚ) |
| 86 | | qmulcl 13009 |
. . . . 5
⊢ ((((𝐴↑2) − 1) ∈
ℚ ∧ ((𝐴
Yrm 𝑀) ·
(𝐴 Yrm 𝑁)) ∈ ℚ) →
(((𝐴↑2) − 1)
· ((𝐴 Yrm
𝑀) · (𝐴 Yrm 𝑁))) ∈
ℚ) |
| 87 | 17, 85, 86 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁))) ∈ ℚ) |
| 88 | | qaddcl 13007 |
. . . 4
⊢ ((((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) ∈ ℚ ∧ (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁))) ∈ ℚ) → (((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) ∈ ℚ) |
| 89 | 81, 87, 88 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) ∈ ℚ) |
| 90 | | qmulcl 13009 |
. . . . 5
⊢ (((𝐴 Yrm 𝑀) ∈ ℚ ∧ (𝐴 Xrm 𝑁) ∈ ℚ) → ((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) ∈ ℚ) |
| 91 | 82, 79, 90 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) ∈ ℚ) |
| 92 | | qmulcl 13009 |
. . . . 5
⊢ (((𝐴 Xrm 𝑀) ∈ ℚ ∧ (𝐴 Yrm 𝑁) ∈ ℚ) → ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)) ∈ ℚ) |
| 93 | 78, 83, 92 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)) ∈ ℚ) |
| 94 | | qaddcl 13007 |
. . . 4
⊢ ((((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) ∈ ℚ ∧ ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)) ∈ ℚ) → (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))) ∈ ℚ) |
| 95 | 91, 93, 94 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))) ∈ ℚ) |
| 96 | | qirropth 42919 |
. . 3
⊢
(((√‘((𝐴↑2) − 1)) ∈ (ℂ ∖
ℚ) ∧ ((𝐴
Xrm (𝑀 + 𝑁)) ∈ ℚ ∧ (𝐴 Yrm (𝑀 + 𝑁)) ∈ ℚ) ∧ ((((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) ∈ ℚ ∧ (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))) ∈ ℚ)) → (((𝐴 Xrm (𝑀 + 𝑁)) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm (𝑀 + 𝑁)))) = ((((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) + ((√‘((𝐴↑2) − 1)) · (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))))) ↔ ((𝐴 Xrm (𝑀 + 𝑁)) = (((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) ∧ (𝐴 Yrm (𝑀 + 𝑁)) = (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)))))) |
| 97 | 72, 75, 77, 89, 95, 96 | syl122anc 1381 |
. 2
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm (𝑀 + 𝑁)) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm (𝑀 + 𝑁)))) = ((((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) + ((√‘((𝐴↑2) − 1)) · (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))))) ↔ ((𝐴 Xrm (𝑀 + 𝑁)) = (((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) ∧ (𝐴 Yrm (𝑀 + 𝑁)) = (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)))))) |
| 98 | 70, 97 | mpbid 232 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm (𝑀 + 𝑁)) = (((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) ∧ (𝐴 Yrm (𝑀 + 𝑁)) = (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))))) |