This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bezoutlem2

Description: Lemma for bezout . (Contributed by Mario Carneiro, 15-Mar-2014) ( Revised by AV, 30-Sep-2020.)

Ref Expression
Hypotheses bezout.1 ⊢ 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) }
bezout.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
bezout.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
bezout.2 ⊢ 𝐺 = inf ( 𝑀 , ℝ , < )
bezout.5 ⊢ ( 𝜑 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
Assertion bezoutlem2 ( 𝜑 → 𝐺 ∈ 𝑀 )

Proof

Step Hyp Ref Expression
1 bezout.1 ⊢ 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) }
2 bezout.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
3 bezout.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
4 bezout.2 ⊢ 𝐺 = inf ( 𝑀 , ℝ , < )
5 bezout.5 ⊢ ( 𝜑 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
6 1 ssrab3 ⊢ 𝑀 ⊆ ℕ
7 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
8 6 7 sseqtri ⊢ 𝑀 ⊆ ( ℤ≥ ‘ 1 )
9 1 2 3 bezoutlem1 ⊢ ( 𝜑 → ( 𝐴 ≠ 0 → ( abs ‘ 𝐴 ) ∈ 𝑀 ) )
10 ne0i ⊢ ( ( abs ‘ 𝐴 ) ∈ 𝑀 → 𝑀 ≠ ∅ )
11 9 10 syl6 ⊢ ( 𝜑 → ( 𝐴 ≠ 0 → 𝑀 ≠ ∅ ) )
12 eqid ⊢ { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } = { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) }
13 12 3 2 bezoutlem1 ⊢ ( 𝜑 → ( 𝐵 ≠ 0 → ( abs ‘ 𝐵 ) ∈ { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } ) )
14 rexcom ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
15 2 zcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → 𝐴 ∈ ℂ )
17 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
18 17 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → 𝑥 ∈ ℂ )
19 16 18 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
20 3 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → 𝐵 ∈ ℂ )
22 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
23 22 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → 𝑦 ∈ ℂ )
24 21 23 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( 𝐵 · 𝑦 ) ∈ ℂ )
25 19 24 addcomd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) )
26 25 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) ) )
27 26 2rexbidva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) ) )
28 14 27 bitrid ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) ) )
29 28 rabbidv ⊢ ( 𝜑 → { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) } = { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } )
30 1 29 eqtrid ⊢ ( 𝜑 → 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } )
31 30 eleq2d ⊢ ( 𝜑 → ( ( abs ‘ 𝐵 ) ∈ 𝑀 ↔ ( abs ‘ 𝐵 ) ∈ { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } ) )
32 13 31 sylibrd ⊢ ( 𝜑 → ( 𝐵 ≠ 0 → ( abs ‘ 𝐵 ) ∈ 𝑀 ) )
33 ne0i ⊢ ( ( abs ‘ 𝐵 ) ∈ 𝑀 → 𝑀 ≠ ∅ )
34 32 33 syl6 ⊢ ( 𝜑 → ( 𝐵 ≠ 0 → 𝑀 ≠ ∅ ) )
35 neorian ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
36 5 35 sylibr ⊢ ( 𝜑 → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
37 11 34 36 mpjaod ⊢ ( 𝜑 → 𝑀 ≠ ∅ )
38 infssuzcl ⊢ ( ( 𝑀 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ≠ ∅ ) → inf ( 𝑀 , ℝ , < ) ∈ 𝑀 )
39 8 37 38 sylancr ⊢ ( 𝜑 → inf ( 𝑀 , ℝ , < ) ∈ 𝑀 )
40 4 39 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ 𝑀 )