| Step | Hyp | Ref
| Expression |
| 1 | | anass 468 |
. . 3
⊢ (((𝑁 = 0 ∧ 𝑀 = 0) ∧ 𝑃 = 0) ↔ (𝑁 = 0 ∧ (𝑀 = 0 ∧ 𝑃 = 0))) |
| 2 | | anass 468 |
. . . . 5
⊢ (((𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀) ∧ 𝑥 ∥ 𝑃) ↔ (𝑥 ∥ 𝑁 ∧ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃))) |
| 3 | 2 | rabbii 3442 |
. . . 4
⊢ {𝑥 ∈ ℤ ∣ ((𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀) ∧ 𝑥 ∥ 𝑃)} = {𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑁 ∧ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃))} |
| 4 | 3 | supeq1i 9487 |
. . 3
⊢
sup({𝑥 ∈
ℤ ∣ ((𝑥 ∥
𝑁 ∧ 𝑥 ∥ 𝑀) ∧ 𝑥 ∥ 𝑃)}, ℝ, < ) = sup({𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑁 ∧ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃))}, ℝ, < ) |
| 5 | 1, 4 | ifbieq2i 4551 |
. 2
⊢
if(((𝑁 = 0 ∧
𝑀 = 0) ∧ 𝑃 = 0), 0, sup({𝑥 ∈ ℤ ∣ ((𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀) ∧ 𝑥 ∥ 𝑃)}, ℝ, < )) = if((𝑁 = 0 ∧ (𝑀 = 0 ∧ 𝑃 = 0)), 0, sup({𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑁 ∧ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃))}, ℝ, < )) |
| 6 | | gcdcl 16543 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 gcd 𝑀) ∈
ℕ0) |
| 7 | 6 | 3adant3 1133 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑁 gcd 𝑀) ∈
ℕ0) |
| 8 | 7 | nn0zd 12639 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑁 gcd 𝑀) ∈ ℤ) |
| 9 | | simp3 1139 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∈
ℤ) |
| 10 | | gcdval 16533 |
. . . 4
⊢ (((𝑁 gcd 𝑀) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑁 gcd 𝑀) gcd 𝑃) = if(((𝑁 gcd 𝑀) = 0 ∧ 𝑃 = 0), 0, sup({𝑥 ∈ ℤ ∣ (𝑥 ∥ (𝑁 gcd 𝑀) ∧ 𝑥 ∥ 𝑃)}, ℝ, < ))) |
| 11 | 8, 9, 10 | syl2anc 584 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑁 gcd 𝑀) gcd 𝑃) = if(((𝑁 gcd 𝑀) = 0 ∧ 𝑃 = 0), 0, sup({𝑥 ∈ ℤ ∣ (𝑥 ∥ (𝑁 gcd 𝑀) ∧ 𝑥 ∥ 𝑃)}, ℝ, < ))) |
| 12 | | gcdeq0 16554 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 gcd 𝑀) = 0 ↔ (𝑁 = 0 ∧ 𝑀 = 0))) |
| 13 | 12 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑁 gcd 𝑀) = 0 ↔ (𝑁 = 0 ∧ 𝑀 = 0))) |
| 14 | 13 | anbi1d 631 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (((𝑁 gcd 𝑀) = 0 ∧ 𝑃 = 0) ↔ ((𝑁 = 0 ∧ 𝑀 = 0) ∧ 𝑃 = 0))) |
| 15 | 14 | bicomd 223 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (((𝑁 = 0 ∧ 𝑀 = 0) ∧ 𝑃 = 0) ↔ ((𝑁 gcd 𝑀) = 0 ∧ 𝑃 = 0))) |
| 16 | | simpr 484 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℤ) |
| 17 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ 𝑥 ∈ ℤ) → 𝑁 ∈
ℤ) |
| 18 | | simpl2 1193 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ 𝑥 ∈ ℤ) → 𝑀 ∈
ℤ) |
| 19 | | dvdsgcdb 16582 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀) ↔ 𝑥 ∥ (𝑁 gcd 𝑀))) |
| 20 | 16, 17, 18, 19 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ 𝑥 ∈ ℤ) → ((𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀) ↔ 𝑥 ∥ (𝑁 gcd 𝑀))) |
| 21 | 20 | anbi1d 631 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ 𝑥 ∈ ℤ) → (((𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀) ∧ 𝑥 ∥ 𝑃) ↔ (𝑥 ∥ (𝑁 gcd 𝑀) ∧ 𝑥 ∥ 𝑃))) |
| 22 | 21 | rabbidva 3443 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → {𝑥 ∈ ℤ ∣ ((𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀) ∧ 𝑥 ∥ 𝑃)} = {𝑥 ∈ ℤ ∣ (𝑥 ∥ (𝑁 gcd 𝑀) ∧ 𝑥 ∥ 𝑃)}) |
| 23 | 22 | supeq1d 9486 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) →
sup({𝑥 ∈ ℤ
∣ ((𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀) ∧ 𝑥 ∥ 𝑃)}, ℝ, < ) = sup({𝑥 ∈ ℤ ∣ (𝑥 ∥ (𝑁 gcd 𝑀) ∧ 𝑥 ∥ 𝑃)}, ℝ, < )) |
| 24 | 15, 23 | ifbieq2d 4552 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) →
if(((𝑁 = 0 ∧ 𝑀 = 0) ∧ 𝑃 = 0), 0, sup({𝑥 ∈ ℤ ∣ ((𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀) ∧ 𝑥 ∥ 𝑃)}, ℝ, < )) = if(((𝑁 gcd 𝑀) = 0 ∧ 𝑃 = 0), 0, sup({𝑥 ∈ ℤ ∣ (𝑥 ∥ (𝑁 gcd 𝑀) ∧ 𝑥 ∥ 𝑃)}, ℝ, < ))) |
| 25 | 11, 24 | eqtr4d 2780 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑁 gcd 𝑀) gcd 𝑃) = if(((𝑁 = 0 ∧ 𝑀 = 0) ∧ 𝑃 = 0), 0, sup({𝑥 ∈ ℤ ∣ ((𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀) ∧ 𝑥 ∥ 𝑃)}, ℝ, < ))) |
| 26 | | simp1 1137 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑁 ∈
ℤ) |
| 27 | | gcdcl 16543 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑀 gcd 𝑃) ∈
ℕ0) |
| 28 | 27 | 3adant1 1131 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑀 gcd 𝑃) ∈
ℕ0) |
| 29 | 28 | nn0zd 12639 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑀 gcd 𝑃) ∈ ℤ) |
| 30 | | gcdval 16533 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 gcd 𝑃) ∈ ℤ) → (𝑁 gcd (𝑀 gcd 𝑃)) = if((𝑁 = 0 ∧ (𝑀 gcd 𝑃) = 0), 0, sup({𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑁 ∧ 𝑥 ∥ (𝑀 gcd 𝑃))}, ℝ, < ))) |
| 31 | 26, 29, 30 | syl2anc 584 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑁 gcd (𝑀 gcd 𝑃)) = if((𝑁 = 0 ∧ (𝑀 gcd 𝑃) = 0), 0, sup({𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑁 ∧ 𝑥 ∥ (𝑀 gcd 𝑃))}, ℝ, < ))) |
| 32 | | gcdeq0 16554 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑀 gcd 𝑃) = 0 ↔ (𝑀 = 0 ∧ 𝑃 = 0))) |
| 33 | 32 | 3adant1 1131 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑀 gcd 𝑃) = 0 ↔ (𝑀 = 0 ∧ 𝑃 = 0))) |
| 34 | 33 | anbi2d 630 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑁 = 0 ∧ (𝑀 gcd 𝑃) = 0) ↔ (𝑁 = 0 ∧ (𝑀 = 0 ∧ 𝑃 = 0)))) |
| 35 | 34 | bicomd 223 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑁 = 0 ∧ (𝑀 = 0 ∧ 𝑃 = 0)) ↔ (𝑁 = 0 ∧ (𝑀 gcd 𝑃) = 0))) |
| 36 | | simpl3 1194 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ 𝑥 ∈ ℤ) → 𝑃 ∈
ℤ) |
| 37 | | dvdsgcdb 16582 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃) ↔ 𝑥 ∥ (𝑀 gcd 𝑃))) |
| 38 | 16, 18, 36, 37 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ 𝑥 ∈ ℤ) → ((𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃) ↔ 𝑥 ∥ (𝑀 gcd 𝑃))) |
| 39 | 38 | anbi2d 630 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ 𝑥 ∈ ℤ) → ((𝑥 ∥ 𝑁 ∧ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃)) ↔ (𝑥 ∥ 𝑁 ∧ 𝑥 ∥ (𝑀 gcd 𝑃)))) |
| 40 | 39 | rabbidva 3443 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → {𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑁 ∧ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃))} = {𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑁 ∧ 𝑥 ∥ (𝑀 gcd 𝑃))}) |
| 41 | 40 | supeq1d 9486 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) →
sup({𝑥 ∈ ℤ
∣ (𝑥 ∥ 𝑁 ∧ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃))}, ℝ, < ) = sup({𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑁 ∧ 𝑥 ∥ (𝑀 gcd 𝑃))}, ℝ, < )) |
| 42 | 35, 41 | ifbieq2d 4552 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) →
if((𝑁 = 0 ∧ (𝑀 = 0 ∧ 𝑃 = 0)), 0, sup({𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑁 ∧ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃))}, ℝ, < )) = if((𝑁 = 0 ∧ (𝑀 gcd 𝑃) = 0), 0, sup({𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑁 ∧ 𝑥 ∥ (𝑀 gcd 𝑃))}, ℝ, < ))) |
| 43 | 31, 42 | eqtr4d 2780 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑁 gcd (𝑀 gcd 𝑃)) = if((𝑁 = 0 ∧ (𝑀 = 0 ∧ 𝑃 = 0)), 0, sup({𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑁 ∧ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃))}, ℝ, < ))) |
| 44 | 5, 25, 43 | 3eqtr4a 2803 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑁 gcd 𝑀) gcd 𝑃) = (𝑁 gcd (𝑀 gcd 𝑃))) |