Description: The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | 12gcd5e1 | ⊢ ( ; 1 2 gcd 5 ) = 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2lt5 | ⊢ 2 < 5 | |
2 | 1 | olci | ⊢ ( 5 < 2 ∨ 2 < 5 ) |
3 | 5re | ⊢ 5 ∈ ℝ | |
4 | 2re | ⊢ 2 ∈ ℝ | |
5 | lttri2 | ⊢ ( ( 5 ∈ ℝ ∧ 2 ∈ ℝ ) → ( 5 ≠ 2 ↔ ( 5 < 2 ∨ 2 < 5 ) ) ) | |
6 | 3 4 5 | mp2an | ⊢ ( 5 ≠ 2 ↔ ( 5 < 2 ∨ 2 < 5 ) ) |
7 | 2 6 | mpbir | ⊢ 5 ≠ 2 |
8 | 5prm | ⊢ 5 ∈ ℙ | |
9 | 2prm | ⊢ 2 ∈ ℙ | |
10 | prmrp | ⊢ ( ( 5 ∈ ℙ ∧ 2 ∈ ℙ ) → ( ( 5 gcd 2 ) = 1 ↔ 5 ≠ 2 ) ) | |
11 | 8 9 10 | mp2an | ⊢ ( ( 5 gcd 2 ) = 1 ↔ 5 ≠ 2 ) |
12 | 7 11 | mpbir | ⊢ ( 5 gcd 2 ) = 1 |
13 | 5nn | ⊢ 5 ∈ ℕ | |
14 | 2nn | ⊢ 2 ∈ ℕ | |
15 | 14 | nnzi | ⊢ 2 ∈ ℤ |
16 | 13 14 15 | gcdaddmzz2nncomi | ⊢ ( 5 gcd 2 ) = ( 5 gcd ( ( 2 · 5 ) + 2 ) ) |
17 | 13 14 | mulcomnni | ⊢ ( 5 · 2 ) = ( 2 · 5 ) |
18 | 5t2e10 | ⊢ ( 5 · 2 ) = ; 1 0 | |
19 | 17 18 | eqtr3i | ⊢ ( 2 · 5 ) = ; 1 0 |
20 | 19 | oveq1i | ⊢ ( ( 2 · 5 ) + 2 ) = ( ; 1 0 + 2 ) |
21 | 1nn0 | ⊢ 1 ∈ ℕ0 | |
22 | 0nn0 | ⊢ 0 ∈ ℕ0 | |
23 | 14 | nnnn0i | ⊢ 2 ∈ ℕ0 |
24 | eqid | ⊢ ; 1 0 = ; 1 0 | |
25 | 23 | dec0h | ⊢ 2 = ; 0 2 |
26 | 1p0e1 | ⊢ ( 1 + 0 ) = 1 | |
27 | 2cn | ⊢ 2 ∈ ℂ | |
28 | 27 | addid2i | ⊢ ( 0 + 2 ) = 2 |
29 | 21 22 22 23 24 25 26 28 | decadd | ⊢ ( ; 1 0 + 2 ) = ; 1 2 |
30 | 20 29 | eqtri | ⊢ ( ( 2 · 5 ) + 2 ) = ; 1 2 |
31 | 30 | oveq2i | ⊢ ( 5 gcd ( ( 2 · 5 ) + 2 ) ) = ( 5 gcd ; 1 2 ) |
32 | 16 31 | eqtri | ⊢ ( 5 gcd 2 ) = ( 5 gcd ; 1 2 ) |
33 | 12 32 | eqtr3i | ⊢ 1 = ( 5 gcd ; 1 2 ) |
34 | 21 14 | decnncl | ⊢ ; 1 2 ∈ ℕ |
35 | 13 34 | gcdcomnni | ⊢ ( 5 gcd ; 1 2 ) = ( ; 1 2 gcd 5 ) |
36 | 33 35 | eqtr2i | ⊢ ( ; 1 2 gcd 5 ) = 1 |