Proof of Theorem dvdsaddre2b
Step | Hyp | Ref
| Expression |
1 | | dvdsadd2b 15895 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵))) |
2 | 1 | a1d 25 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐵 ∈ ℝ → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))) |
3 | 2 | 3exp 1121 |
. . . . 5
⊢ (𝐴 ∈ ℤ → (𝐵 ∈ ℤ → ((𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶) → (𝐵 ∈ ℝ → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))))) |
4 | 3 | com24 95 |
. . . 4
⊢ (𝐴 ∈ ℤ → (𝐵 ∈ ℝ → ((𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶) → (𝐵 ∈ ℤ → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))))) |
5 | 4 | 3imp 1113 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐵 ∈ ℤ → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))) |
6 | 5 | com12 32 |
. 2
⊢ (𝐵 ∈ ℤ → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))) |
7 | | dvdszrcl 15848 |
. . . . . . 7
⊢ (𝐴 ∥ 𝐵 → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) |
8 | | pm2.24 124 |
. . . . . . 7
⊢ (𝐵 ∈ ℤ → (¬
𝐵 ∈ ℤ →
𝐴 ∥ (𝐶 + 𝐵))) |
9 | 7, 8 | simpl2im 507 |
. . . . . 6
⊢ (𝐴 ∥ 𝐵 → (¬ 𝐵 ∈ ℤ → 𝐴 ∥ (𝐶 + 𝐵))) |
10 | 9 | com12 32 |
. . . . 5
⊢ (¬
𝐵 ∈ ℤ →
(𝐴 ∥ 𝐵 → 𝐴 ∥ (𝐶 + 𝐵))) |
11 | 10 | adantr 484 |
. . . 4
⊢ ((¬
𝐵 ∈ ℤ ∧
(𝐴 ∈ ℤ ∧
𝐵 ∈ ℝ ∧
(𝐶 ∈ ℤ ∧
𝐴 ∥ 𝐶))) → (𝐴 ∥ 𝐵 → 𝐴 ∥ (𝐶 + 𝐵))) |
12 | | dvdszrcl 15848 |
. . . . . 6
⊢ (𝐴 ∥ (𝐶 + 𝐵) → (𝐴 ∈ ℤ ∧ (𝐶 + 𝐵) ∈ ℤ)) |
13 | | zcn 12206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
ℂ) |
14 | 13 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ ℤ ∧ (𝐵 ∈ ℝ ∧ ¬
𝐵 ∈ ℤ)) →
𝐶 ∈
ℂ) |
15 | | recn 10844 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
16 | 15 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ ℤ ∧ (𝐵 ∈ ℝ ∧ ¬
𝐵 ∈ ℤ)) →
𝐵 ∈
ℂ) |
17 | 14, 16 | addcomd 11059 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ ℤ ∧ (𝐵 ∈ ℝ ∧ ¬
𝐵 ∈ ℤ)) →
(𝐶 + 𝐵) = (𝐵 + 𝐶)) |
18 | | eldif 3891 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ (ℝ ∖
ℤ) ↔ (𝐵 ∈
ℝ ∧ ¬ 𝐵
∈ ℤ)) |
19 | | nzadd 12250 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ (ℝ ∖
ℤ) ∧ 𝐶 ∈
ℤ) → (𝐵 + 𝐶) ∈ (ℝ ∖
ℤ)) |
20 | 19 | eldifbd 3894 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ (ℝ ∖
ℤ) ∧ 𝐶 ∈
ℤ) → ¬ (𝐵 +
𝐶) ∈
ℤ) |
21 | 20 | expcom 417 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∈ ℤ → (𝐵 ∈ (ℝ ∖
ℤ) → ¬ (𝐵 +
𝐶) ∈
ℤ)) |
22 | 18, 21 | syl5bir 246 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ ℤ → ((𝐵 ∈ ℝ ∧ ¬
𝐵 ∈ ℤ) →
¬ (𝐵 + 𝐶) ∈
ℤ)) |
23 | 22 | imp 410 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ ℤ ∧ (𝐵 ∈ ℝ ∧ ¬
𝐵 ∈ ℤ)) →
¬ (𝐵 + 𝐶) ∈
ℤ) |
24 | 17, 23 | eqneltrd 2858 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ ℤ ∧ (𝐵 ∈ ℝ ∧ ¬
𝐵 ∈ ℤ)) →
¬ (𝐶 + 𝐵) ∈
ℤ) |
25 | 24 | exp32 424 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ ℤ → (𝐵 ∈ ℝ → (¬
𝐵 ∈ ℤ →
¬ (𝐶 + 𝐵) ∈
ℤ))) |
26 | | pm2.21 123 |
. . . . . . . . . . . . 13
⊢ (¬
(𝐶 + 𝐵) ∈ ℤ → ((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵)) |
27 | 25, 26 | syl8 76 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ ℤ → (𝐵 ∈ ℝ → (¬
𝐵 ∈ ℤ →
((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵)))) |
28 | 27 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶) → (𝐵 ∈ ℝ → (¬ 𝐵 ∈ ℤ → ((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵)))) |
29 | 28 | com12 32 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → ((𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶) → (¬ 𝐵 ∈ ℤ → ((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵)))) |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → (𝐵 ∈ ℝ → ((𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶) → (¬ 𝐵 ∈ ℤ → ((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵))))) |
31 | 30 | 3imp 1113 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (¬ 𝐵 ∈ ℤ → ((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵))) |
32 | 31 | impcom 411 |
. . . . . . 7
⊢ ((¬
𝐵 ∈ ℤ ∧
(𝐴 ∈ ℤ ∧
𝐵 ∈ ℝ ∧
(𝐶 ∈ ℤ ∧
𝐴 ∥ 𝐶))) → ((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵)) |
33 | 32 | com12 32 |
. . . . . 6
⊢ ((𝐶 + 𝐵) ∈ ℤ → ((¬ 𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶))) → 𝐴 ∥ 𝐵)) |
34 | 12, 33 | simpl2im 507 |
. . . . 5
⊢ (𝐴 ∥ (𝐶 + 𝐵) → ((¬ 𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶))) → 𝐴 ∥ 𝐵)) |
35 | 34 | com12 32 |
. . . 4
⊢ ((¬
𝐵 ∈ ℤ ∧
(𝐴 ∈ ℤ ∧
𝐵 ∈ ℝ ∧
(𝐶 ∈ ℤ ∧
𝐴 ∥ 𝐶))) → (𝐴 ∥ (𝐶 + 𝐵) → 𝐴 ∥ 𝐵)) |
36 | 11, 35 | impbid 215 |
. . 3
⊢ ((¬
𝐵 ∈ ℤ ∧
(𝐴 ∈ ℤ ∧
𝐵 ∈ ℝ ∧
(𝐶 ∈ ℤ ∧
𝐴 ∥ 𝐶))) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵))) |
37 | 36 | ex 416 |
. 2
⊢ (¬
𝐵 ∈ ℤ →
((𝐴 ∈ ℤ ∧
𝐵 ∈ ℝ ∧
(𝐶 ∈ ℤ ∧
𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))) |
38 | 6, 37 | pm2.61i 185 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵))) |