Proof of Theorem jm2.19lem4
Step | Hyp | Ref
| Expression |
1 | | elznn0 12264 |
. . 3
⊢ (𝐼 ∈ ℤ ↔ (𝐼 ∈ ℝ ∧ (𝐼 ∈ ℕ0 ∨
-𝐼 ∈
ℕ0))) |
2 | | jm2.19lem3 40729 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℕ0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀))))) |
3 | 2 | 3expia 1119 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐼 ∈ ℕ0 → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀)))))) |
4 | 3 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) → (𝐼 ∈ ℕ0 → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀)))))) |
5 | | simplll 771 |
. . . . . . . 8
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → 𝐴 ∈
(ℤ≥‘2)) |
6 | | simprl 767 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑀 ∈ ℤ) |
7 | 6 | ad2antrr 722 |
. . . . . . . 8
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → 𝑀 ∈
ℤ) |
8 | | simprr 769 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℤ) |
9 | 8 | ad2antrr 722 |
. . . . . . . . 9
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → 𝑁 ∈
ℤ) |
10 | | nn0z 12273 |
. . . . . . . . . . . 12
⊢ (-𝐼 ∈ ℕ0
→ -𝐼 ∈
ℤ) |
11 | 10 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → -𝐼 ∈
ℤ) |
12 | | simplr 765 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → 𝐼 ∈
ℝ) |
13 | 12 | recnd 10934 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → 𝐼 ∈
ℂ) |
14 | | znegclb 12287 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ ℂ → (𝐼 ∈ ℤ ↔ -𝐼 ∈
ℤ)) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → (𝐼 ∈ ℤ ↔ -𝐼 ∈
ℤ)) |
16 | 11, 15 | mpbird 256 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → 𝐼 ∈
ℤ) |
17 | 16, 7 | zmulcld 12361 |
. . . . . . . . 9
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → (𝐼 · 𝑀) ∈ ℤ) |
18 | 9, 17 | zaddcld 12359 |
. . . . . . . 8
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → (𝑁 + (𝐼 · 𝑀)) ∈ ℤ) |
19 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → -𝐼 ∈
ℕ0) |
20 | | jm2.19lem3 40729 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ (𝑁 + (𝐼 · 𝑀)) ∈ ℤ) ∧ -𝐼 ∈ ℕ0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀))) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm ((𝑁 + (𝐼 · 𝑀)) + (-𝐼 · 𝑀))))) |
21 | 5, 7, 18, 19, 20 | syl121anc 1373 |
. . . . . . 7
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀))) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm ((𝑁 + (𝐼 · 𝑀)) + (-𝐼 · 𝑀))))) |
22 | | zcn 12254 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
23 | 22 | ad2antrl 724 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑀 ∈ ℂ) |
24 | 23 | ad2antrr 722 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → 𝑀 ∈
ℂ) |
25 | 13, 24 | mulneg1d 11358 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → (-𝐼 · 𝑀) = -(𝐼 · 𝑀)) |
26 | 25 | oveq2d 7271 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → ((𝑁 + (𝐼 · 𝑀)) + (-𝐼 · 𝑀)) = ((𝑁 + (𝐼 · 𝑀)) + -(𝐼 · 𝑀))) |
27 | | zcn 12254 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
28 | 27 | ad2antll 725 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℂ) |
29 | 28 | ad2antrr 722 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → 𝑁 ∈
ℂ) |
30 | 13, 24 | mulcld 10926 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → (𝐼 · 𝑀) ∈ ℂ) |
31 | 29, 30 | addcld 10925 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → (𝑁 + (𝐼 · 𝑀)) ∈ ℂ) |
32 | 31, 30 | negsubd 11268 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → ((𝑁 + (𝐼 · 𝑀)) + -(𝐼 · 𝑀)) = ((𝑁 + (𝐼 · 𝑀)) − (𝐼 · 𝑀))) |
33 | 29, 30 | pncand 11263 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → ((𝑁 + (𝐼 · 𝑀)) − (𝐼 · 𝑀)) = 𝑁) |
34 | 26, 32, 33 | 3eqtrd 2782 |
. . . . . . . . 9
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → ((𝑁 + (𝐼 · 𝑀)) + (-𝐼 · 𝑀)) = 𝑁) |
35 | 34 | oveq2d 7271 |
. . . . . . . 8
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → (𝐴 Yrm ((𝑁 + (𝐼 · 𝑀)) + (-𝐼 · 𝑀))) = (𝐴 Yrm 𝑁)) |
36 | 35 | breq2d 5082 |
. . . . . . 7
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm ((𝑁 + (𝐼 · 𝑀)) + (-𝐼 · 𝑀))) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁))) |
37 | 21, 36 | bitr2d 279 |
. . . . . 6
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) ∧ -𝐼 ∈ ℕ0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀))))) |
38 | 37 | ex 412 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) → (-𝐼 ∈ ℕ0 → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀)))))) |
39 | 4, 38 | jaod 855 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℝ) → ((𝐼 ∈ ℕ0 ∨ -𝐼 ∈ ℕ0)
→ ((𝐴 Yrm
𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀)))))) |
40 | 39 | expimpd 453 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐼 ∈ ℝ ∧ (𝐼 ∈ ℕ0 ∨ -𝐼 ∈ ℕ0))
→ ((𝐴 Yrm
𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀)))))) |
41 | 1, 40 | syl5bi 241 |
. 2
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐼 ∈ ℤ → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀)))))) |
42 | 41 | 3impia 1115 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℤ) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀))))) |