MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  divalglem8 Structured version   Visualization version   GIF version

Theorem divalglem8 14904
Description: Lemma for divalg 14907. (Contributed by Paul Chapman, 21-Mar-2011.)
Hypotheses
Ref Expression
divalglem8.1 𝑁 ∈ ℤ
divalglem8.2 𝐷 ∈ ℤ
divalglem8.3 𝐷 ≠ 0
divalglem8.4 𝑆 = {𝑟 ∈ ℕ0𝐷 ∥ (𝑁𝑟)}
Assertion
Ref Expression
divalglem8 (((𝑋𝑆𝑌𝑆) ∧ (𝑋 < (abs‘𝐷) ∧ 𝑌 < (abs‘𝐷))) → (𝐾 ∈ ℤ → ((𝐾 · (abs‘𝐷)) = (𝑌𝑋) → 𝑋 = 𝑌)))
Distinct variable groups:   𝐷,𝑟   𝑁,𝑟
Allowed substitution hints:   𝑆(𝑟)   𝐾(𝑟)   𝑋(𝑟)   𝑌(𝑟)

Proof of Theorem divalglem8
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 divalglem8.4 . . . . . . . . . . . . 13 𝑆 = {𝑟 ∈ ℕ0𝐷 ∥ (𝑁𝑟)}
2 ssrab2 3646 . . . . . . . . . . . . 13 {𝑟 ∈ ℕ0𝐷 ∥ (𝑁𝑟)} ⊆ ℕ0
31, 2eqsstri 3594 . . . . . . . . . . . 12 𝑆 ⊆ ℕ0
4 nn0sscn 11141 . . . . . . . . . . . 12 0 ⊆ ℂ
53, 4sstri 3573 . . . . . . . . . . 11 𝑆 ⊆ ℂ
65sseli 3560 . . . . . . . . . 10 (𝑌𝑆𝑌 ∈ ℂ)
75sseli 3560 . . . . . . . . . 10 (𝑋𝑆𝑋 ∈ ℂ)
8 divalglem8.2 . . . . . . . . . . . . . 14 𝐷 ∈ ℤ
9 divalglem8.3 . . . . . . . . . . . . . 14 𝐷 ≠ 0
10 nnabscl 13856 . . . . . . . . . . . . . 14 ((𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (abs‘𝐷) ∈ ℕ)
118, 9, 10mp2an 703 . . . . . . . . . . . . 13 (abs‘𝐷) ∈ ℕ
1211nnzi 11231 . . . . . . . . . . . 12 (abs‘𝐷) ∈ ℤ
13 zmulcl 11256 . . . . . . . . . . . 12 ((𝐾 ∈ ℤ ∧ (abs‘𝐷) ∈ ℤ) → (𝐾 · (abs‘𝐷)) ∈ ℤ)
1412, 13mpan2 702 . . . . . . . . . . 11 (𝐾 ∈ ℤ → (𝐾 · (abs‘𝐷)) ∈ ℤ)
1514zcnd 11312 . . . . . . . . . 10 (𝐾 ∈ ℤ → (𝐾 · (abs‘𝐷)) ∈ ℂ)
16 subadd 10132 . . . . . . . . . 10 ((𝑌 ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ (𝐾 · (abs‘𝐷)) ∈ ℂ) → ((𝑌𝑋) = (𝐾 · (abs‘𝐷)) ↔ (𝑋 + (𝐾 · (abs‘𝐷))) = 𝑌))
176, 7, 15, 16syl3an 1359 . . . . . . . . 9 ((𝑌𝑆𝑋𝑆𝐾 ∈ ℤ) → ((𝑌𝑋) = (𝐾 · (abs‘𝐷)) ↔ (𝑋 + (𝐾 · (abs‘𝐷))) = 𝑌))
18173com12 1260 . . . . . . . 8 ((𝑋𝑆𝑌𝑆𝐾 ∈ ℤ) → ((𝑌𝑋) = (𝐾 · (abs‘𝐷)) ↔ (𝑋 + (𝐾 · (abs‘𝐷))) = 𝑌))
19 eqcom 2613 . . . . . . . 8 ((𝑌𝑋) = (𝐾 · (abs‘𝐷)) ↔ (𝐾 · (abs‘𝐷)) = (𝑌𝑋))
20 eqcom 2613 . . . . . . . 8 ((𝑋 + (𝐾 · (abs‘𝐷))) = 𝑌𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))))
2118, 19, 203bitr3g 300 . . . . . . 7 ((𝑋𝑆𝑌𝑆𝐾 ∈ ℤ) → ((𝐾 · (abs‘𝐷)) = (𝑌𝑋) ↔ 𝑌 = (𝑋 + (𝐾 · (abs‘𝐷)))))
22213adant1r 1310 . . . . . 6 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ 𝑌𝑆𝐾 ∈ ℤ) → ((𝐾 · (abs‘𝐷)) = (𝑌𝑋) ↔ 𝑌 = (𝑋 + (𝐾 · (abs‘𝐷)))))
23223adant2r 1312 . . . . 5 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ (𝑌𝑆𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → ((𝐾 · (abs‘𝐷)) = (𝑌𝑋) ↔ 𝑌 = (𝑋 + (𝐾 · (abs‘𝐷)))))
24 breq1 4577 . . . . . . . . . . . 12 (𝑧 = 𝑌 → (𝑧 < (abs‘𝐷) ↔ 𝑌 < (abs‘𝐷)))
25 eleq1 2672 . . . . . . . . . . . 12 (𝑧 = 𝑌 → (𝑧 ∈ (0...((abs‘𝐷) − 1)) ↔ 𝑌 ∈ (0...((abs‘𝐷) − 1))))
2624, 25imbi12d 332 . . . . . . . . . . 11 (𝑧 = 𝑌 → ((𝑧 < (abs‘𝐷) → 𝑧 ∈ (0...((abs‘𝐷) − 1))) ↔ (𝑌 < (abs‘𝐷) → 𝑌 ∈ (0...((abs‘𝐷) − 1)))))
273sseli 3560 . . . . . . . . . . . . . . . 16 (𝑧𝑆𝑧 ∈ ℕ0)
28 elnn0z 11220 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℕ0 ↔ (𝑧 ∈ ℤ ∧ 0 ≤ 𝑧))
2927, 28sylib 206 . . . . . . . . . . . . . . 15 (𝑧𝑆 → (𝑧 ∈ ℤ ∧ 0 ≤ 𝑧))
3029anim1i 589 . . . . . . . . . . . . . 14 ((𝑧𝑆𝑧 < (abs‘𝐷)) → ((𝑧 ∈ ℤ ∧ 0 ≤ 𝑧) ∧ 𝑧 < (abs‘𝐷)))
31 df-3an 1032 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℤ ∧ 0 ≤ 𝑧𝑧 < (abs‘𝐷)) ↔ ((𝑧 ∈ ℤ ∧ 0 ≤ 𝑧) ∧ 𝑧 < (abs‘𝐷)))
3230, 31sylibr 222 . . . . . . . . . . . . 13 ((𝑧𝑆𝑧 < (abs‘𝐷)) → (𝑧 ∈ ℤ ∧ 0 ≤ 𝑧𝑧 < (abs‘𝐷)))
33 0z 11218 . . . . . . . . . . . . . 14 0 ∈ ℤ
34 elfzm11 12232 . . . . . . . . . . . . . 14 ((0 ∈ ℤ ∧ (abs‘𝐷) ∈ ℤ) → (𝑧 ∈ (0...((abs‘𝐷) − 1)) ↔ (𝑧 ∈ ℤ ∧ 0 ≤ 𝑧𝑧 < (abs‘𝐷))))
3533, 12, 34mp2an 703 . . . . . . . . . . . . 13 (𝑧 ∈ (0...((abs‘𝐷) − 1)) ↔ (𝑧 ∈ ℤ ∧ 0 ≤ 𝑧𝑧 < (abs‘𝐷)))
3632, 35sylibr 222 . . . . . . . . . . . 12 ((𝑧𝑆𝑧 < (abs‘𝐷)) → 𝑧 ∈ (0...((abs‘𝐷) − 1)))
3736ex 448 . . . . . . . . . . 11 (𝑧𝑆 → (𝑧 < (abs‘𝐷) → 𝑧 ∈ (0...((abs‘𝐷) − 1))))
3826, 37vtoclga 3241 . . . . . . . . . 10 (𝑌𝑆 → (𝑌 < (abs‘𝐷) → 𝑌 ∈ (0...((abs‘𝐷) − 1))))
39 eleq1 2672 . . . . . . . . . . 11 (𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))) → (𝑌 ∈ (0...((abs‘𝐷) − 1)) ↔ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1))))
4039biimpd 217 . . . . . . . . . 10 (𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))) → (𝑌 ∈ (0...((abs‘𝐷) − 1)) → (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1))))
4138, 40sylan9 686 . . . . . . . . 9 ((𝑌𝑆𝑌 = (𝑋 + (𝐾 · (abs‘𝐷)))) → (𝑌 < (abs‘𝐷) → (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1))))
4241impancom 454 . . . . . . . 8 ((𝑌𝑆𝑌 < (abs‘𝐷)) → (𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))) → (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1))))
43423ad2ant2 1075 . . . . . . 7 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ (𝑌𝑆𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → (𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))) → (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1))))
44 breq1 4577 . . . . . . . . . . . . 13 (𝑧 = 𝑋 → (𝑧 < (abs‘𝐷) ↔ 𝑋 < (abs‘𝐷)))
45 eleq1 2672 . . . . . . . . . . . . 13 (𝑧 = 𝑋 → (𝑧 ∈ (0...((abs‘𝐷) − 1)) ↔ 𝑋 ∈ (0...((abs‘𝐷) − 1))))
4644, 45imbi12d 332 . . . . . . . . . . . 12 (𝑧 = 𝑋 → ((𝑧 < (abs‘𝐷) → 𝑧 ∈ (0...((abs‘𝐷) − 1))) ↔ (𝑋 < (abs‘𝐷) → 𝑋 ∈ (0...((abs‘𝐷) − 1)))))
4746, 37vtoclga 3241 . . . . . . . . . . 11 (𝑋𝑆 → (𝑋 < (abs‘𝐷) → 𝑋 ∈ (0...((abs‘𝐷) − 1))))
4847imp 443 . . . . . . . . . 10 ((𝑋𝑆𝑋 < (abs‘𝐷)) → 𝑋 ∈ (0...((abs‘𝐷) − 1)))
498, 9divalglem7 14903 . . . . . . . . . 10 ((𝑋 ∈ (0...((abs‘𝐷) − 1)) ∧ 𝐾 ∈ ℤ) → (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1))))
5048, 49sylan 486 . . . . . . . . 9 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1))))
51503adant2 1072 . . . . . . . 8 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ (𝑌𝑆𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1))))
5251con2d 127 . . . . . . 7 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ (𝑌𝑆𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → ((𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)) → ¬ 𝐾 ≠ 0))
5343, 52syld 45 . . . . . 6 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ (𝑌𝑆𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → (𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))) → ¬ 𝐾 ≠ 0))
54 df-ne 2778 . . . . . . 7 (𝐾 ≠ 0 ↔ ¬ 𝐾 = 0)
5554con2bii 345 . . . . . 6 (𝐾 = 0 ↔ ¬ 𝐾 ≠ 0)
5653, 55syl6ibr 240 . . . . 5 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ (𝑌𝑆𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → (𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))) → 𝐾 = 0))
5723, 56sylbid 228 . . . 4 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ (𝑌𝑆𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → ((𝐾 · (abs‘𝐷)) = (𝑌𝑋) → 𝐾 = 0))
58 oveq1 6531 . . . . . . . . . . 11 (𝐾 = 0 → (𝐾 · (abs‘𝐷)) = (0 · (abs‘𝐷)))
5911nncni 10874 . . . . . . . . . . . 12 (abs‘𝐷) ∈ ℂ
6059mul02i 10073 . . . . . . . . . . 11 (0 · (abs‘𝐷)) = 0
6158, 60syl6eq 2656 . . . . . . . . . 10 (𝐾 = 0 → (𝐾 · (abs‘𝐷)) = 0)
6261eqeq1d 2608 . . . . . . . . 9 (𝐾 = 0 → ((𝐾 · (abs‘𝐷)) = (𝑌𝑋) ↔ 0 = (𝑌𝑋)))
6362biimpac 501 . . . . . . . 8 (((𝐾 · (abs‘𝐷)) = (𝑌𝑋) ∧ 𝐾 = 0) → 0 = (𝑌𝑋))
64 subeq0 10155 . . . . . . . . . 10 ((𝑌 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((𝑌𝑋) = 0 ↔ 𝑌 = 𝑋))
656, 7, 64syl2anr 493 . . . . . . . . 9 ((𝑋𝑆𝑌𝑆) → ((𝑌𝑋) = 0 ↔ 𝑌 = 𝑋))
66 eqcom 2613 . . . . . . . . 9 ((𝑌𝑋) = 0 ↔ 0 = (𝑌𝑋))
67 eqcom 2613 . . . . . . . . 9 (𝑌 = 𝑋𝑋 = 𝑌)
6865, 66, 673bitr3g 300 . . . . . . . 8 ((𝑋𝑆𝑌𝑆) → (0 = (𝑌𝑋) ↔ 𝑋 = 𝑌))
6963, 68syl5ib 232 . . . . . . 7 ((𝑋𝑆𝑌𝑆) → (((𝐾 · (abs‘𝐷)) = (𝑌𝑋) ∧ 𝐾 = 0) → 𝑋 = 𝑌))
7069ad2ant2r 778 . . . . . 6 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ (𝑌𝑆𝑌 < (abs‘𝐷))) → (((𝐾 · (abs‘𝐷)) = (𝑌𝑋) ∧ 𝐾 = 0) → 𝑋 = 𝑌))
71703adant3 1073 . . . . 5 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ (𝑌𝑆𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → (((𝐾 · (abs‘𝐷)) = (𝑌𝑋) ∧ 𝐾 = 0) → 𝑋 = 𝑌))
7271expd 450 . . . 4 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ (𝑌𝑆𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → ((𝐾 · (abs‘𝐷)) = (𝑌𝑋) → (𝐾 = 0 → 𝑋 = 𝑌)))
7357, 72mpdd 41 . . 3 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ (𝑌𝑆𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → ((𝐾 · (abs‘𝐷)) = (𝑌𝑋) → 𝑋 = 𝑌))
74733expia 1258 . 2 (((𝑋𝑆𝑋 < (abs‘𝐷)) ∧ (𝑌𝑆𝑌 < (abs‘𝐷))) → (𝐾 ∈ ℤ → ((𝐾 · (abs‘𝐷)) = (𝑌𝑋) → 𝑋 = 𝑌)))
7574an4s 864 1 (((𝑋𝑆𝑌𝑆) ∧ (𝑋 < (abs‘𝐷) ∧ 𝑌 < (abs‘𝐷))) → (𝐾 ∈ ℤ → ((𝐾 · (abs‘𝐷)) = (𝑌𝑋) → 𝑋 = 𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2776  {crab 2896   class class class wbr 4574  cfv 5787  (class class class)co 6524  cc 9787  0cc0 9789  1c1 9790   + caddc 9792   · cmul 9794   < clt 9927  cle 9928  cmin 10114  cn 10864  0cn0 11136  cz 11207  ...cfz 12149  abscabs 13765  cdvds 14764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-er 7603  df-en 7816  df-dom 7817  df-sdom 7818  df-sup 8205  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-n0 11137  df-z 11208  df-uz 11517  df-rp 11662  df-fz 12150  df-seq 12616  df-exp 12675  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767
This theorem is referenced by:  divalglem9  14905
  Copyright terms: Public domain W3C validator