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

Metamath Proof Explorer

Theorem bezoutlem3

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

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

Proof

Step Hyp Ref Expression
1 bezout.1 ⊢ 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) }
2 bezout.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
3 bezout.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
4 bezout.2 ⊢ 𝐺 = inf ( 𝑀 , ℝ , < )
5 bezout.5 ⊢ ( 𝜑 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
6 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐶 ∈ 𝑀 )
7 eqeq1 ⊢ ( 𝑧 = 𝐶 → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝐶 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
8 7 2rexbidv ⊢ ( 𝑧 = 𝐶 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
9 oveq2 ⊢ ( 𝑥 = 𝑠 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑠 ) )
10 9 oveq1d ⊢ ( 𝑥 = 𝑠 → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑦 ) ) )
11 10 eqeq2d ⊢ ( 𝑥 = 𝑠 → ( 𝐶 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑦 ) ) ) )
12 oveq2 ⊢ ( 𝑦 = 𝑡 → ( 𝐵 · 𝑦 ) = ( 𝐵 · 𝑡 ) )
13 12 oveq2d ⊢ ( 𝑦 = 𝑡 → ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) )
14 13 eqeq2d ⊢ ( 𝑦 = 𝑡 → ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ) )
15 11 14 cbvrex2vw ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) )
16 8 15 bitrdi ⊢ ( 𝑧 = 𝐶 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ) )
17 16 1 elrab2 ⊢ ( 𝐶 ∈ 𝑀 ↔ ( 𝐶 ∈ ℕ ∧ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ) )
18 6 17 sylib ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 ∈ ℕ ∧ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ) )
19 18 simpld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐶 ∈ ℕ )
20 19 nnred ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐶 ∈ ℝ )
21 1 2 3 4 5 bezoutlem2 ⊢ ( 𝜑 → 𝐺 ∈ 𝑀 )
22 oveq2 ⊢ ( 𝑥 = 𝑢 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑢 ) )
23 22 oveq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) )
24 23 eqeq2d ⊢ ( 𝑥 = 𝑢 → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) ) )
25 oveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝐵 · 𝑦 ) = ( 𝐵 · 𝑣 ) )
26 25 oveq2d ⊢ ( 𝑦 = 𝑣 → ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
27 26 eqeq2d ⊢ ( 𝑦 = 𝑣 → ( 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
28 24 27 cbvrex2vw ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
29 eqeq1 ⊢ ( 𝑧 = 𝐺 → ( 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ↔ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
30 29 2rexbidv ⊢ ( 𝑧 = 𝐺 → ( ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
31 28 30 bitrid ⊢ ( 𝑧 = 𝐺 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
32 31 1 elrab2 ⊢ ( 𝐺 ∈ 𝑀 ↔ ( 𝐺 ∈ ℕ ∧ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
33 21 32 sylib ⊢ ( 𝜑 → ( 𝐺 ∈ ℕ ∧ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
34 33 simpld ⊢ ( 𝜑 → 𝐺 ∈ ℕ )
35 34 nnrpd ⊢ ( 𝜑 → 𝐺 ∈ ℝ+ )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐺 ∈ ℝ+ )
37 modlt ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐺 ∈ ℝ+ ) → ( 𝐶 mod 𝐺 ) < 𝐺 )
38 20 36 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 mod 𝐺 ) < 𝐺 )
39 19 nnzd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐶 ∈ ℤ )
40 34 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐺 ∈ ℕ )
41 39 40 zmodcld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 mod 𝐺 ) ∈ ℕ0 )
42 41 nn0red ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 mod 𝐺 ) ∈ ℝ )
43 34 nnred ⊢ ( 𝜑 → 𝐺 ∈ ℝ )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐺 ∈ ℝ )
45 42 44 ltnled ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ( 𝐶 mod 𝐺 ) < 𝐺 ↔ ¬ 𝐺 ≤ ( 𝐶 mod 𝐺 ) ) )
46 38 45 mpbid ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ¬ 𝐺 ≤ ( 𝐶 mod 𝐺 ) )
47 18 simprd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) )
48 33 simprd ⊢ ( 𝜑 → ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) → ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
50 simprll ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑠 ∈ ℤ )
51 simprrl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑢 ∈ ℤ )
52 20 40 nndivred ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 / 𝐺 ) ∈ ℝ )
53 52 flcld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ∈ ℤ )
54 53 adantr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ∈ ℤ )
55 51 54 zmulcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ∈ ℤ )
56 50 55 zsubcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ∈ ℤ )
57 simprlr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑡 ∈ ℤ )
58 simprrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑣 ∈ ℤ )
59 58 54 zmulcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ∈ ℤ )
60 57 59 zsubcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ∈ ℤ )
61 2 zcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
62 61 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝐴 ∈ ℂ )
63 50 zcnd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑠 ∈ ℂ )
64 62 63 mulcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐴 · 𝑠 ) ∈ ℂ )
65 3 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
66 65 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝐵 ∈ ℂ )
67 57 zcnd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑡 ∈ ℂ )
68 66 67 mulcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐵 · 𝑡 ) ∈ ℂ )
69 55 zcnd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ∈ ℂ )
70 62 69 mulcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ∈ ℂ )
71 59 zcnd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ∈ ℂ )
72 66 71 mulcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ∈ ℂ )
73 64 68 70 72 addsub4d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) + ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) = ( ( ( 𝐴 · 𝑠 ) − ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( ( 𝐵 · 𝑡 ) − ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) )
74 51 zcnd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑢 ∈ ℂ )
75 62 74 mulcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐴 · 𝑢 ) ∈ ℂ )
76 53 zcnd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ∈ ℂ )
77 76 adantr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ∈ ℂ )
78 58 zcnd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑣 ∈ ℂ )
79 66 78 mulcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐵 · 𝑣 ) ∈ ℂ )
80 62 74 77 mulassd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( 𝐴 · 𝑢 ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) = ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) )
81 66 78 77 mulassd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( 𝐵 · 𝑣 ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) = ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) )
82 80 81 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( ( 𝐴 · 𝑢 ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) + ( ( 𝐵 · 𝑣 ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) + ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) )
83 75 77 79 82 joinlmuladdmuld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) = ( ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) + ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) )
84 83 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) + ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) )
85 62 63 69 subdid ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) = ( ( 𝐴 · 𝑠 ) − ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) )
86 66 67 71 subdid ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) = ( ( 𝐵 · 𝑡 ) − ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) )
87 85 86 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) = ( ( ( 𝐴 · 𝑠 ) − ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( ( 𝐵 · 𝑡 ) − ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) )
88 73 84 87 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) )
89 oveq2 ⊢ ( 𝑥 = ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( 𝐴 · 𝑥 ) = ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) )
90 89 oveq1d ⊢ ( 𝑥 = ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · 𝑦 ) ) )
91 90 eqeq2d ⊢ ( 𝑥 = ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · 𝑦 ) ) ) )
92 oveq2 ⊢ ( 𝑦 = ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( 𝐵 · 𝑦 ) = ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) )
93 92 oveq2d ⊢ ( 𝑦 = ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) )
94 93 eqeq2d ⊢ ( 𝑦 = ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · 𝑦 ) ) ↔ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) ) )
95 91 94 rspc2ev ⊢ ( ( ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ∈ ℤ ∧ ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ∈ ℤ ∧ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
96 56 60 88 95 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
97 oveq1 ⊢ ( 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) = ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) )
98 oveq12 ⊢ ( ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ∧ ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) = ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) )
99 97 98 sylan2 ⊢ ( ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ∧ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) → ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) )
100 99 eqeq1d ⊢ ( ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ∧ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) → ( ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
101 100 2rexbidv ⊢ ( ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ∧ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
102 96 101 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ∧ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
103 102 expcomd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) ) )
104 103 expr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) → ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) → ( 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) ) ) )
105 104 rexlimdvv ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) → ( ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) ) )
106 49 105 mpd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) → ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
107 106 ex ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) → ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) ) )
108 107 rexlimdvv ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
109 47 108 mpd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
110 modval ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐺 ∈ ℝ+ ) → ( 𝐶 mod 𝐺 ) = ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) )
111 20 36 110 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 mod 𝐺 ) = ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) )
112 111 eqcomd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( 𝐶 mod 𝐺 ) )
113 112 eqeq1d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
114 113 2rexbidv ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
115 109 114 mpbid ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
116 eqeq1 ⊢ ( 𝑧 = ( 𝐶 mod 𝐺 ) → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
117 116 2rexbidv ⊢ ( 𝑧 = ( 𝐶 mod 𝐺 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
118 117 1 elrab2 ⊢ ( ( 𝐶 mod 𝐺 ) ∈ 𝑀 ↔ ( ( 𝐶 mod 𝐺 ) ∈ ℕ ∧ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
119 118 simplbi2com ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) → ( ( 𝐶 mod 𝐺 ) ∈ ℕ → ( 𝐶 mod 𝐺 ) ∈ 𝑀 ) )
120 115 119 syl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ( 𝐶 mod 𝐺 ) ∈ ℕ → ( 𝐶 mod 𝐺 ) ∈ 𝑀 ) )
121 1 ssrab3 ⊢ 𝑀 ⊆ ℕ
122 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
123 121 122 sseqtri ⊢ 𝑀 ⊆ ( ℤ≥ ‘ 1 )
124 infssuzle ⊢ ( ( 𝑀 ⊆ ( ℤ≥ ‘ 1 ) ∧ ( 𝐶 mod 𝐺 ) ∈ 𝑀 ) → inf ( 𝑀 , ℝ , < ) ≤ ( 𝐶 mod 𝐺 ) )
125 123 124 mpan ⊢ ( ( 𝐶 mod 𝐺 ) ∈ 𝑀 → inf ( 𝑀 , ℝ , < ) ≤ ( 𝐶 mod 𝐺 ) )
126 4 125 eqbrtrid ⊢ ( ( 𝐶 mod 𝐺 ) ∈ 𝑀 → 𝐺 ≤ ( 𝐶 mod 𝐺 ) )
127 120 126 syl6 ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ( 𝐶 mod 𝐺 ) ∈ ℕ → 𝐺 ≤ ( 𝐶 mod 𝐺 ) ) )
128 46 127 mtod ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ¬ ( 𝐶 mod 𝐺 ) ∈ ℕ )
129 elnn0 ⊢ ( ( 𝐶 mod 𝐺 ) ∈ ℕ0 ↔ ( ( 𝐶 mod 𝐺 ) ∈ ℕ ∨ ( 𝐶 mod 𝐺 ) = 0 ) )
130 41 129 sylib ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ( 𝐶 mod 𝐺 ) ∈ ℕ ∨ ( 𝐶 mod 𝐺 ) = 0 ) )
131 130 ord ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ¬ ( 𝐶 mod 𝐺 ) ∈ ℕ → ( 𝐶 mod 𝐺 ) = 0 ) )
132 128 131 mpd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 mod 𝐺 ) = 0 )
133 dvdsval3 ⊢ ( ( 𝐺 ∈ ℕ ∧ 𝐶 ∈ ℤ ) → ( 𝐺 ∥ 𝐶 ↔ ( 𝐶 mod 𝐺 ) = 0 ) )
134 40 39 133 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐺 ∥ 𝐶 ↔ ( 𝐶 mod 𝐺 ) = 0 ) )
135 132 134 mpbird ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐺 ∥ 𝐶 )
136 135 ex ⊢ ( 𝜑 → ( 𝐶 ∈ 𝑀 → 𝐺 ∥ 𝐶 ) )