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