Step |
Hyp |
Ref |
Expression |
1 |
|
gcdcllem2.1 |
⊢ 𝑆 = { 𝑧 ∈ ℤ ∣ ∀ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑧 ∥ 𝑛 } |
2 |
|
gcdcllem2.2 |
⊢ 𝑅 = { 𝑧 ∈ ℤ ∣ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) } |
3 |
2
|
ssrab3 |
⊢ 𝑅 ⊆ ℤ |
4 |
|
prssi |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → { 𝑀 , 𝑁 } ⊆ ℤ ) |
5 |
|
neorian |
⊢ ( ( 𝑀 ≠ 0 ∨ 𝑁 ≠ 0 ) ↔ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) |
6 |
|
prid1g |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ { 𝑀 , 𝑁 } ) |
7 |
|
neeq1 |
⊢ ( 𝑛 = 𝑀 → ( 𝑛 ≠ 0 ↔ 𝑀 ≠ 0 ) ) |
8 |
7
|
rspcev |
⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 0 ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 ) |
9 |
6 8
|
sylan |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 ) |
10 |
9
|
adantlr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 ) |
11 |
|
prid2g |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ { 𝑀 , 𝑁 } ) |
12 |
|
neeq1 |
⊢ ( 𝑛 = 𝑁 → ( 𝑛 ≠ 0 ↔ 𝑁 ≠ 0 ) ) |
13 |
12
|
rspcev |
⊢ ( ( 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ≠ 0 ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 ) |
14 |
11 13
|
sylan |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 ) |
15 |
14
|
adantll |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 ) |
16 |
10 15
|
jaodan |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∨ 𝑁 ≠ 0 ) ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 ) |
17 |
5 16
|
sylan2br |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 ) |
18 |
1
|
gcdcllem1 |
⊢ ( ( { 𝑀 , 𝑁 } ⊆ ℤ ∧ ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 ) → ( 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) ) |
19 |
4 17 18
|
syl2an2r |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) ) |
20 |
1 2
|
gcdcllem2 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑅 = 𝑆 ) |
21 |
|
neeq1 |
⊢ ( 𝑅 = 𝑆 → ( 𝑅 ≠ ∅ ↔ 𝑆 ≠ ∅ ) ) |
22 |
|
raleq |
⊢ ( 𝑅 = 𝑆 → ( ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) ) |
23 |
22
|
rexbidv |
⊢ ( 𝑅 = 𝑆 → ( ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) ) |
24 |
21 23
|
anbi12d |
⊢ ( 𝑅 = 𝑆 → ( ( 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) ↔ ( 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) ) ) |
25 |
20 24
|
syl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) ↔ ( 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) ) ) |
26 |
25
|
adantr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) ↔ ( 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) ) ) |
27 |
19 26
|
mpbird |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) ) |
28 |
|
suprzcl2 |
⊢ ( ( 𝑅 ⊆ ℤ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) → sup ( 𝑅 , ℝ , < ) ∈ 𝑅 ) |
29 |
3 28
|
mp3an1 |
⊢ ( ( 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) → sup ( 𝑅 , ℝ , < ) ∈ 𝑅 ) |
30 |
27 29
|
syl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → sup ( 𝑅 , ℝ , < ) ∈ 𝑅 ) |
31 |
3 30
|
sselid |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → sup ( 𝑅 , ℝ , < ) ∈ ℤ ) |
32 |
27
|
simprd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) |
33 |
|
1dvds |
⊢ ( 𝑀 ∈ ℤ → 1 ∥ 𝑀 ) |
34 |
|
1dvds |
⊢ ( 𝑁 ∈ ℤ → 1 ∥ 𝑁 ) |
35 |
33 34
|
anim12i |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 1 ∥ 𝑀 ∧ 1 ∥ 𝑁 ) ) |
36 |
|
1z |
⊢ 1 ∈ ℤ |
37 |
|
breq1 |
⊢ ( 𝑧 = 1 → ( 𝑧 ∥ 𝑀 ↔ 1 ∥ 𝑀 ) ) |
38 |
|
breq1 |
⊢ ( 𝑧 = 1 → ( 𝑧 ∥ 𝑁 ↔ 1 ∥ 𝑁 ) ) |
39 |
37 38
|
anbi12d |
⊢ ( 𝑧 = 1 → ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ↔ ( 1 ∥ 𝑀 ∧ 1 ∥ 𝑁 ) ) ) |
40 |
39 2
|
elrab2 |
⊢ ( 1 ∈ 𝑅 ↔ ( 1 ∈ ℤ ∧ ( 1 ∥ 𝑀 ∧ 1 ∥ 𝑁 ) ) ) |
41 |
36 40
|
mpbiran |
⊢ ( 1 ∈ 𝑅 ↔ ( 1 ∥ 𝑀 ∧ 1 ∥ 𝑁 ) ) |
42 |
35 41
|
sylibr |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 1 ∈ 𝑅 ) |
43 |
42
|
adantr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → 1 ∈ 𝑅 ) |
44 |
|
suprzub |
⊢ ( ( 𝑅 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ∧ 1 ∈ 𝑅 ) → 1 ≤ sup ( 𝑅 , ℝ , < ) ) |
45 |
3 32 43 44
|
mp3an2i |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → 1 ≤ sup ( 𝑅 , ℝ , < ) ) |
46 |
|
elnnz1 |
⊢ ( sup ( 𝑅 , ℝ , < ) ∈ ℕ ↔ ( sup ( 𝑅 , ℝ , < ) ∈ ℤ ∧ 1 ≤ sup ( 𝑅 , ℝ , < ) ) ) |
47 |
31 45 46
|
sylanbrc |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → sup ( 𝑅 , ℝ , < ) ∈ ℕ ) |
48 |
|
breq1 |
⊢ ( 𝑥 = sup ( 𝑅 , ℝ , < ) → ( 𝑥 ∥ 𝑀 ↔ sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ) ) |
49 |
|
breq1 |
⊢ ( 𝑥 = sup ( 𝑅 , ℝ , < ) → ( 𝑥 ∥ 𝑁 ↔ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) ) |
50 |
48 49
|
anbi12d |
⊢ ( 𝑥 = sup ( 𝑅 , ℝ , < ) → ( ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) ↔ ( sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ∧ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) ) ) |
51 |
|
breq1 |
⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∥ 𝑀 ↔ 𝑥 ∥ 𝑀 ) ) |
52 |
|
breq1 |
⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∥ 𝑁 ↔ 𝑥 ∥ 𝑁 ) ) |
53 |
51 52
|
anbi12d |
⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ↔ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) ) ) |
54 |
53
|
cbvrabv |
⊢ { 𝑧 ∈ ℤ ∣ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) } = { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) } |
55 |
2 54
|
eqtri |
⊢ 𝑅 = { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) } |
56 |
50 55
|
elrab2 |
⊢ ( sup ( 𝑅 , ℝ , < ) ∈ 𝑅 ↔ ( sup ( 𝑅 , ℝ , < ) ∈ ℤ ∧ ( sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ∧ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) ) ) |
57 |
30 56
|
sylib |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( sup ( 𝑅 , ℝ , < ) ∈ ℤ ∧ ( sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ∧ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) ) ) |
58 |
57
|
simprd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ∧ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) ) |
59 |
|
breq1 |
⊢ ( 𝑧 = 𝐾 → ( 𝑧 ∥ 𝑀 ↔ 𝐾 ∥ 𝑀 ) ) |
60 |
|
breq1 |
⊢ ( 𝑧 = 𝐾 → ( 𝑧 ∥ 𝑁 ↔ 𝐾 ∥ 𝑁 ) ) |
61 |
59 60
|
anbi12d |
⊢ ( 𝑧 = 𝐾 → ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ↔ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) ) |
62 |
61 2
|
elrab2 |
⊢ ( 𝐾 ∈ 𝑅 ↔ ( 𝐾 ∈ ℤ ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) ) |
63 |
62
|
biimpri |
⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) → 𝐾 ∈ 𝑅 ) |
64 |
63
|
3impb |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∈ 𝑅 ) |
65 |
|
suprzub |
⊢ ( ( 𝑅 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ∧ 𝐾 ∈ 𝑅 ) → 𝐾 ≤ sup ( 𝑅 , ℝ , < ) ) |
66 |
65
|
3expia |
⊢ ( ( 𝑅 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) → ( 𝐾 ∈ 𝑅 → 𝐾 ≤ sup ( 𝑅 , ℝ , < ) ) ) |
67 |
3 66
|
mpan |
⊢ ( ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 → ( 𝐾 ∈ 𝑅 → 𝐾 ≤ sup ( 𝑅 , ℝ , < ) ) ) |
68 |
32 64 67
|
syl2im |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ sup ( 𝑅 , ℝ , < ) ) ) |
69 |
47 58 68
|
3jca |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( sup ( 𝑅 , ℝ , < ) ∈ ℕ ∧ ( sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ∧ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ sup ( 𝑅 , ℝ , < ) ) ) ) |