Step | Hyp | Ref
| Expression |
1 | | simprl 789 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝐴 ∈
(ℤ≥‘2)) |
2 | | simprrr 802 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑁 ∈ ℤ) |
3 | | frmx 38321 |
. . . . . . . . . . 11
⊢
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 |
4 | 3 | fovcl 7025 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
5 | 4 | nn0zd 11808 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℤ) |
6 | 1, 2, 5 | syl2anc 581 |
. . . . . . . 8
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∈ ℤ) |
7 | | simprrl 801 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑀 ∈ ℤ) |
8 | | frmy 38322 |
. . . . . . . . . 10
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
9 | 8 | fovcl 7025 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ) |
10 | 1, 7, 9 | syl2anc 581 |
. . . . . . . 8
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm 𝑀) ∈ ℤ) |
11 | | congid 38381 |
. . . . . . . 8
⊢ (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑀))) |
12 | 6, 10, 11 | syl2anc 581 |
. . . . . . 7
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑀))) |
13 | | 2cnd 11429 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → 2 ∈
ℂ) |
14 | | zcn 11709 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
15 | 13, 14 | mulcld 10377 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → (2
· 𝑁) ∈
ℂ) |
16 | 15 | mul02d 10553 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → (0
· (2 · 𝑁)) =
0) |
17 | 16 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0
· (2 · 𝑁)) =
0) |
18 | 17 | oveq2d 6921 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + (0 · (2 · 𝑁))) = (𝑀 + 0)) |
19 | | zcn 11709 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
20 | 19 | addid1d 10555 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (𝑀 + 0) = 𝑀) |
21 | 20 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 0) = 𝑀) |
22 | 18, 21 | eqtrd 2861 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + (0 · (2 · 𝑁))) = 𝑀) |
23 | 22 | ad2antll 722 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + (0 · (2 · 𝑁))) = 𝑀) |
24 | 23 | oveq2d 6921 |
. . . . . . . 8
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) = (𝐴 Yrm 𝑀)) |
25 | 24 | oveq1d 6920 |
. . . . . . 7
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑀))) |
26 | 12, 25 | breqtrrd 4901 |
. . . . . 6
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))) |
27 | 26 | orcd 906 |
. . . . 5
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) |
28 | 27 | ex 403 |
. . . 4
⊢ (𝐼 ∈ ℤ → ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) |
29 | | simprl 789 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝐴 ∈
(ℤ≥‘2)) |
30 | | simprrr 802 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑁 ∈ ℤ) |
31 | 29, 30, 5 | syl2anc 581 |
. . . . . . 7
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∈ ℤ) |
32 | | simprrl 801 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑀 ∈ ℤ) |
33 | 29, 32, 9 | syl2anc 581 |
. . . . . . 7
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm 𝑀) ∈ ℤ) |
34 | | simpl 476 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑏 ∈ ℤ) |
35 | 34 | peano2zd 11813 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑏 + 1) ∈
ℤ) |
36 | | eluzel2 11973 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈
(ℤ≥‘2) → 2 ∈ ℤ) |
37 | 36 | ad2antrl 721 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 2 ∈
ℤ) |
38 | 37, 30 | zmulcld 11816 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · 𝑁) ∈
ℤ) |
39 | 35, 38 | zmulcld 11816 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝑏 + 1) · (2 · 𝑁)) ∈
ℤ) |
40 | 32, 39 | zaddcld 11814 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + ((𝑏 + 1) · (2 · 𝑁))) ∈ ℤ) |
41 | 8 | fovcl 7025 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 + ((𝑏 + 1) · (2 · 𝑁))) ∈ ℤ) → (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) ∈ ℤ) |
42 | 29, 40, 41 | syl2anc 581 |
. . . . . . 7
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) ∈ ℤ) |
43 | 34, 38 | zmulcld 11816 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑏 · (2 · 𝑁)) ∈
ℤ) |
44 | 32, 43 | zaddcld 11814 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ) |
45 | 8 | fovcl 7025 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ) → (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ) |
46 | 29, 44, 45 | syl2anc 581 |
. . . . . . 7
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ) |
47 | 3 | fovcl 7025 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (2 · 𝑁) ∈ ℤ) → (𝐴 Xrm (2 · 𝑁)) ∈
ℕ0) |
48 | 47 | nn0zd 11808 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (2 · 𝑁) ∈ ℤ) → (𝐴 Xrm (2 · 𝑁)) ∈
ℤ) |
49 | 29, 38, 48 | syl2anc 581 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm (2 · 𝑁)) ∈
ℤ) |
50 | 46, 49 | zmulcld 11816 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) ∈
ℤ) |
51 | 46 | znegcld 11812 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ) |
52 | 50, 51 | zsubcld 11815 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∈ ℤ) |
53 | 3 | fovcl 7025 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ) → (𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈
ℕ0) |
54 | 53 | nn0zd 11808 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ) → (𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ) |
55 | 29, 44, 54 | syl2anc 581 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ) |
56 | 8 | fovcl 7025 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (2 · 𝑁) ∈ ℤ) → (𝐴 Yrm (2 · 𝑁)) ∈
ℤ) |
57 | 29, 38, 56 | syl2anc 581 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (2 · 𝑁)) ∈
ℤ) |
58 | 55, 57 | zmulcld 11816 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))) ∈
ℤ) |
59 | 37, 31 | zmulcld 11816 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · (𝐴 Xrm 𝑁)) ∈
ℤ) |
60 | | dvdsmul2 15381 |
. . . . . . . . . . . . . 14
⊢ (((2
· (𝐴 Xrm
𝑁)) ∈ ℤ ∧
(𝐴 Xrm 𝑁) ∈ ℤ) → (𝐴 Xrm 𝑁) ∥ ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁))) |
61 | 59, 31, 60 | syl2anc 581 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁))) |
62 | | rmxdbl 38347 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm (2 · 𝑁)) = ((2 · ((𝐴 Xrm 𝑁)↑2)) −
1)) |
63 | 29, 30, 62 | syl2anc 581 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm (2 · 𝑁)) = ((2 · ((𝐴 Xrm 𝑁)↑2)) −
1)) |
64 | 63 | oveq1d 6920 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (2 ·
𝑁)) + 1) = (((2 ·
((𝐴 Xrm 𝑁)↑2)) − 1) +
1)) |
65 | | 2cnd 11429 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 2 ∈
ℂ) |
66 | 29, 30, 4 | syl2anc 581 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
67 | 66 | nn0cnd 11680 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∈ ℂ) |
68 | 67 | sqcld 13300 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁)↑2) ∈
ℂ) |
69 | 65, 68 | mulcld 10377 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 ·
((𝐴 Xrm 𝑁)↑2)) ∈
ℂ) |
70 | | 1cnd 10351 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 1 ∈
ℂ) |
71 | 69, 70 | npcand 10717 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((2 ·
((𝐴 Xrm 𝑁)↑2)) − 1) + 1) = (2
· ((𝐴 Xrm
𝑁)↑2))) |
72 | 67 | sqvald 13299 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁)↑2) = ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁))) |
73 | 72 | oveq2d 6921 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 ·
((𝐴 Xrm 𝑁)↑2)) = (2 · ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁)))) |
74 | | mulass 10340 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ (𝐴
Xrm 𝑁) ∈
ℂ ∧ (𝐴
Xrm 𝑁) ∈
ℂ) → ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁)) = (2 · ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁)))) |
75 | 74 | eqcomd 2831 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℂ ∧ (𝐴
Xrm 𝑁) ∈
ℂ ∧ (𝐴
Xrm 𝑁) ∈
ℂ) → (2 · ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁))) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁))) |
76 | 65, 67, 67, 75 | syl3anc 1496 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 ·
((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁))) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁))) |
77 | 73, 76 | eqtrd 2861 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 ·
((𝐴 Xrm 𝑁)↑2)) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁))) |
78 | 64, 71, 77 | 3eqtrd 2865 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (2 ·
𝑁)) + 1) = ((2 ·
(𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁))) |
79 | 61, 78 | breqtrrd 4901 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (2 · 𝑁)) + 1)) |
80 | 49 | peano2zd 11813 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (2 ·
𝑁)) + 1) ∈
ℤ) |
81 | | dvdsmultr2 15398 |
. . . . . . . . . . . . 13
⊢ (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ ∧ ((𝐴 Xrm (2 ·
𝑁)) + 1) ∈ ℤ)
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Xrm (2 ·
𝑁)) + 1) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1)))) |
82 | 31, 46, 80, 81 | syl3anc 1496 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (2 · 𝑁)) + 1) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1)))) |
83 | 79, 82 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1))) |
84 | 46 | zcnd 11811 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℂ) |
85 | 84 | mulid1d 10374 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · 1) = (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) |
86 | 85 | oveq2d 6921 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · 1)) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))) |
87 | 49 | zcnd 11811 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm (2 · 𝑁)) ∈
ℂ) |
88 | 84, 87, 70 | adddid 10381 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1)) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · 1))) |
89 | 50 | zcnd 11811 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) ∈
ℂ) |
90 | 89, 84 | subnegd 10720 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))) |
91 | 86, 88, 90 | 3eqtr4d 2871 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1)) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))) |
92 | 83, 91 | breqtrd 4899 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))) |
93 | 8 | fovcl 7025 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ) |
94 | 29, 30, 93 | syl2anc 581 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm 𝑁) ∈ ℤ) |
95 | 37, 94 | zmulcld 11816 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · (𝐴 Yrm 𝑁)) ∈
ℤ) |
96 | | dvdsmul2 15381 |
. . . . . . . . . . . . 13
⊢ (((2
· (𝐴 Yrm
𝑁)) ∈ ℤ ∧
(𝐴 Xrm 𝑁) ∈ ℤ) → (𝐴 Xrm 𝑁) ∥ ((2 · (𝐴 Yrm 𝑁)) · (𝐴 Xrm 𝑁))) |
97 | 95, 31, 96 | syl2anc 581 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((2 · (𝐴 Yrm 𝑁)) · (𝐴 Xrm 𝑁))) |
98 | | rmydbl 38348 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm (2 · 𝑁)) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Yrm 𝑁))) |
99 | 29, 30, 98 | syl2anc 581 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (2 · 𝑁)) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Yrm 𝑁))) |
100 | 94 | zcnd 11811 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm 𝑁) ∈ ℂ) |
101 | 65, 67, 100 | mul32d 10565 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((2 ·
(𝐴 Xrm 𝑁)) · (𝐴 Yrm 𝑁)) = ((2 · (𝐴 Yrm 𝑁)) · (𝐴 Xrm 𝑁))) |
102 | 99, 101 | eqtrd 2861 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (2 · 𝑁)) = ((2 · (𝐴 Yrm 𝑁)) · (𝐴 Xrm 𝑁))) |
103 | 97, 102 | breqtrrd 4901 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ (𝐴 Yrm (2 · 𝑁))) |
104 | | dvdsmultr2 15398 |
. . . . . . . . . . . 12
⊢ (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ ∧ (𝐴 Yrm (2 · 𝑁)) ∈ ℤ) →
((𝐴 Xrm 𝑁) ∥ (𝐴 Yrm (2 · 𝑁)) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) |
105 | 31, 55, 57, 104 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁) ∥ (𝐴 Yrm (2 · 𝑁)) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) |
106 | 103, 105 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))) |
107 | | dvds2add 15392 |
. . . . . . . . . . 11
⊢ (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∈ ℤ ∧ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))) ∈ ℤ) →
(((𝐴 Xrm 𝑁) ∥ (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∧ (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))) → (𝐴 Xrm 𝑁) ∥ ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))))) |
108 | 107 | imp 397 |
. . . . . . . . . 10
⊢ ((((𝐴 Xrm 𝑁) ∈ ℤ ∧ (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∈ ℤ ∧ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))) ∈ ℤ) ∧
((𝐴 Xrm 𝑁) ∥ (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∧ (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) → (𝐴 Xrm 𝑁) ∥ ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) |
109 | 31, 52, 58, 92, 106, 108 | syl32anc 1503 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) |
110 | 34 | zcnd 11811 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑏 ∈ ℂ) |
111 | 38 | zcnd 11811 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · 𝑁) ∈
ℂ) |
112 | 110, 70, 111 | adddird 10382 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝑏 + 1) · (2 · 𝑁)) = ((𝑏 · (2 · 𝑁)) + (1 · (2 · 𝑁)))) |
113 | 112 | oveq2d 6921 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + ((𝑏 + 1) · (2 · 𝑁))) = (𝑀 + ((𝑏 · (2 · 𝑁)) + (1 · (2 · 𝑁))))) |
114 | 32 | zcnd 11811 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑀 ∈ ℂ) |
115 | 43 | zcnd 11811 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑏 · (2 · 𝑁)) ∈
ℂ) |
116 | | 1zzd 11736 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 1 ∈
ℤ) |
117 | 116, 38 | zmulcld 11816 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (1 · (2
· 𝑁)) ∈
ℤ) |
118 | 117 | zcnd 11811 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (1 · (2
· 𝑁)) ∈
ℂ) |
119 | 114, 115,
118 | addassd 10379 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝑀 + (𝑏 · (2 · 𝑁))) + (1 · (2 · 𝑁))) = (𝑀 + ((𝑏 · (2 · 𝑁)) + (1 · (2 · 𝑁))))) |
120 | 111 | mulid2d 10375 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (1 · (2
· 𝑁)) = (2 ·
𝑁)) |
121 | 120 | oveq2d 6921 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝑀 + (𝑏 · (2 · 𝑁))) + (1 · (2 · 𝑁))) = ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁))) |
122 | 113, 119,
121 | 3eqtr2d 2867 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + ((𝑏 + 1) · (2 · 𝑁))) = ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁))) |
123 | 122 | oveq2d 6921 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) = (𝐴 Yrm ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁)))) |
124 | | rmyadd 38339 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ) → (𝐴 Yrm ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁))) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) |
125 | 29, 44, 38, 124 | syl3anc 1496 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁))) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) |
126 | 123, 125 | eqtrd 2861 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) |
127 | 126 | oveq1d 6920 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) = ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))) |
128 | 58 | zcnd 11811 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))) ∈
ℂ) |
129 | 51 | zcnd 11811 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℂ) |
130 | 89, 128, 129 | addsubd 10734 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) = ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) |
131 | 127, 130 | eqtrd 2861 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) = ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) |
132 | 109, 131 | breqtrrd 4901 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))) |
133 | 132 | olcd 907 |
. . . . . . 7
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))))) |
134 | | jm2.25lem1 38408 |
. . . . . . 7
⊢ ((((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ) ∧ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) ∈ ℤ ∧ (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))))) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) |
135 | 31, 33, 42, 46, 133, 134 | syl221anc 1506 |
. . . . . 6
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) |
136 | 135 | pm5.74da 840 |
. . . . 5
⊢ (𝑏 ∈ ℤ → (((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))) |
137 | | oveq1 6912 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → (𝑎 · (2 · 𝑁)) = (𝑏 · (2 · 𝑁))) |
138 | 137 | oveq2d 6921 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + (𝑏 · (2 · 𝑁)))) |
139 | 138 | oveq2d 6921 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) |
140 | 139 | oveq1d 6920 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))) |
141 | 140 | breq2d 4885 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))) |
142 | 139 | oveq1d 6920 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) |
143 | 142 | breq2d 4885 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) |
144 | 141, 143 | orbi12d 949 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) |
145 | 144 | imbi2d 332 |
. . . . 5
⊢ (𝑎 = 𝑏 → (((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))) |
146 | | oveq1 6912 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑏 + 1) → (𝑎 · (2 · 𝑁)) = ((𝑏 + 1) · (2 · 𝑁))) |
147 | 146 | oveq2d 6921 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑏 + 1) → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) |
148 | 147 | oveq2d 6921 |
. . . . . . . . 9
⊢ (𝑎 = (𝑏 + 1) → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁))))) |
149 | 148 | oveq1d 6920 |
. . . . . . . 8
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))) |
150 | 149 | breq2d 4885 |
. . . . . . 7
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))) |
151 | 148 | oveq1d 6920 |
. . . . . . . 8
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) |
152 | 151 | breq2d 4885 |
. . . . . . 7
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) |
153 | 150, 152 | orbi12d 949 |
. . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) |
154 | 153 | imbi2d 332 |
. . . . 5
⊢ (𝑎 = (𝑏 + 1) → (((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))) |
155 | | oveq1 6912 |
. . . . . . . . . . 11
⊢ (𝑎 = 0 → (𝑎 · (2 · 𝑁)) = (0 · (2 · 𝑁))) |
156 | 155 | oveq2d 6921 |
. . . . . . . . . 10
⊢ (𝑎 = 0 → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + (0 · (2 · 𝑁)))) |
157 | 156 | oveq2d 6921 |
. . . . . . . . 9
⊢ (𝑎 = 0 → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + (0 · (2 · 𝑁))))) |
158 | 157 | oveq1d 6920 |
. . . . . . . 8
⊢ (𝑎 = 0 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))) |
159 | 158 | breq2d 4885 |
. . . . . . 7
⊢ (𝑎 = 0 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))) |
160 | 157 | oveq1d 6920 |
. . . . . . . 8
⊢ (𝑎 = 0 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) |
161 | 160 | breq2d 4885 |
. . . . . . 7
⊢ (𝑎 = 0 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) |
162 | 159, 161 | orbi12d 949 |
. . . . . 6
⊢ (𝑎 = 0 → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) |
163 | 162 | imbi2d 332 |
. . . . 5
⊢ (𝑎 = 0 → (((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))) |
164 | | oveq1 6912 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐼 → (𝑎 · (2 · 𝑁)) = (𝐼 · (2 · 𝑁))) |
165 | 164 | oveq2d 6921 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐼 → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + (𝐼 · (2 · 𝑁)))) |
166 | 165 | oveq2d 6921 |
. . . . . . . . 9
⊢ (𝑎 = 𝐼 → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁))))) |
167 | 166 | oveq1d 6920 |
. . . . . . . 8
⊢ (𝑎 = 𝐼 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))) |
168 | 167 | breq2d 4885 |
. . . . . . 7
⊢ (𝑎 = 𝐼 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))) |
169 | 166 | oveq1d 6920 |
. . . . . . . 8
⊢ (𝑎 = 𝐼 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) |
170 | 169 | breq2d 4885 |
. . . . . . 7
⊢ (𝑎 = 𝐼 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) |
171 | 168, 170 | orbi12d 949 |
. . . . . 6
⊢ (𝑎 = 𝐼 → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) |
172 | 171 | imbi2d 332 |
. . . . 5
⊢ (𝑎 = 𝐼 → (((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))) |
173 | 136, 145,
154, 163, 172 | zindbi 38354 |
. . . 4
⊢ (𝐼 ∈ ℤ → (((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))) |
174 | 28, 173 | mpbid 224 |
. . 3
⊢ (𝐼 ∈ ℤ → ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) |
175 | 174 | impcom 398 |
. 2
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) |
176 | 175 | 3impa 1142 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) |