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

Theorem modfzo0difsn 12934
 Description: For a number within a half-open range of nonnegative integers with one excluded integer there is a positive integer so that the number is equal to the sum of the positive integer and the excluded integer modulo the upper bound of the range. (Contributed by AV, 19-Mar-2021.)
Assertion
Ref Expression
modfzo0difsn ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁))
Distinct variable groups:   𝑖,𝐽   𝑖,𝐾   𝑖,𝑁

Proof of Theorem modfzo0difsn
StepHypRef Expression
1 eldifi 3873 . . . . . 6 (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → 𝐾 ∈ (0..^𝑁))
2 elfzoelz 12662 . . . . . . 7 (𝐾 ∈ (0..^𝑁) → 𝐾 ∈ ℤ)
32zred 11672 . . . . . 6 (𝐾 ∈ (0..^𝑁) → 𝐾 ∈ ℝ)
41, 3syl 17 . . . . 5 (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → 𝐾 ∈ ℝ)
5 elfzoelz 12662 . . . . . 6 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
65zred 11672 . . . . 5 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℝ)
7 leloe 10314 . . . . 5 ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) → (𝐾𝐽 ↔ (𝐾 < 𝐽𝐾 = 𝐽)))
84, 6, 7syl2anr 496 . . . 4 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → (𝐾𝐽 ↔ (𝐾 < 𝐽𝐾 = 𝐽)))
9 elfzo0 12701 . . . . . . . . . . . 12 (𝐾 ∈ (0..^𝑁) ↔ (𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁))
10 elfzo0 12701 . . . . . . . . . . . . . . 15 (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
11 nn0cn 11492 . . . . . . . . . . . . . . . . . . . . . 22 (𝐾 ∈ ℕ0𝐾 ∈ ℂ)
1211adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ ℕ0𝐾 < 𝑁) → 𝐾 ∈ ℂ)
1312adantl 473 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → 𝐾 ∈ ℂ)
14 nn0cn 11492 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 ∈ ℕ0𝐽 ∈ ℂ)
15143ad2ant1 1128 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝐽 ∈ ℂ)
1615adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → 𝐽 ∈ ℂ)
17 nncn 11218 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
18173ad2ant2 1129 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℂ)
1918adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → 𝑁 ∈ ℂ)
2013, 16, 19subadd23d 10604 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → ((𝐾𝐽) + 𝑁) = (𝐾 + (𝑁𝐽)))
21 simpl 474 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ ℕ0𝐾 < 𝑁) → 𝐾 ∈ ℕ0)
22 nn0z 11590 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 ∈ ℕ0𝐽 ∈ ℤ)
23 nnz 11589 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
24 znnsub 11613 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 < 𝑁 ↔ (𝑁𝐽) ∈ ℕ))
2522, 23, 24syl2an 495 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ) → (𝐽 < 𝑁 ↔ (𝑁𝐽) ∈ ℕ))
2625biimp3a 1579 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝑁𝐽) ∈ ℕ)
27 nn0nnaddcl 11514 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ ℕ0 ∧ (𝑁𝐽) ∈ ℕ) → (𝐾 + (𝑁𝐽)) ∈ ℕ)
2821, 26, 27syl2anr 496 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → (𝐾 + (𝑁𝐽)) ∈ ℕ)
2920, 28eqeltrd 2837 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → ((𝐾𝐽) + 𝑁) ∈ ℕ)
3029adantr 472 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) ∧ 𝐾 < 𝐽) → ((𝐾𝐽) + 𝑁) ∈ ℕ)
31 simp2 1132 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℕ)
3231adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → 𝑁 ∈ ℕ)
3332adantr 472 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) ∧ 𝐾 < 𝐽) → 𝑁 ∈ ℕ)
34 nn0re 11491 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐾 ∈ ℕ0𝐾 ∈ ℝ)
3534adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℕ0𝐾 < 𝑁) → 𝐾 ∈ ℝ)
3635adantl 473 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → 𝐾 ∈ ℝ)
37 nn0re 11491 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ ℕ0𝐽 ∈ ℝ)
38373ad2ant1 1128 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝐽 ∈ ℝ)
3938adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → 𝐽 ∈ ℝ)
4036, 39sublt0d 10843 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → ((𝐾𝐽) < 0 ↔ 𝐾 < 𝐽))
4140bicomd 213 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → (𝐾 < 𝐽 ↔ (𝐾𝐽) < 0))
4241biimpa 502 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) ∧ 𝐾 < 𝐽) → (𝐾𝐽) < 0)
43 resubcl 10535 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) → (𝐾𝐽) ∈ ℝ)
4435, 38, 43syl2anr 496 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → (𝐾𝐽) ∈ ℝ)
45 nnre 11217 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
46453ad2ant2 1129 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℝ)
4746adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → 𝑁 ∈ ℝ)
4844, 47jca 555 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) → ((𝐾𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ))
4948adantr 472 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) ∧ 𝐾 < 𝐽) → ((𝐾𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ))
50 ltaddnegr 10442 . . . . . . . . . . . . . . . . . . 19 (((𝐾𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝐾𝐽) < 0 ↔ ((𝐾𝐽) + 𝑁) < 𝑁))
5149, 50syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) ∧ 𝐾 < 𝐽) → ((𝐾𝐽) < 0 ↔ ((𝐾𝐽) + 𝑁) < 𝑁))
5242, 51mpbid 222 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) ∧ 𝐾 < 𝐽) → ((𝐾𝐽) + 𝑁) < 𝑁)
53 elfzo1 12710 . . . . . . . . . . . . . . . . 17 (((𝐾𝐽) + 𝑁) ∈ (1..^𝑁) ↔ (((𝐾𝐽) + 𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ((𝐾𝐽) + 𝑁) < 𝑁))
5430, 33, 52, 53syl3anbrc 1429 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ0𝐾 < 𝑁)) ∧ 𝐾 < 𝐽) → ((𝐾𝐽) + 𝑁) ∈ (1..^𝑁))
5554exp31 631 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝐾 ∈ ℕ0𝐾 < 𝑁) → (𝐾 < 𝐽 → ((𝐾𝐽) + 𝑁) ∈ (1..^𝑁))))
5610, 55sylbi 207 . . . . . . . . . . . . . 14 (𝐽 ∈ (0..^𝑁) → ((𝐾 ∈ ℕ0𝐾 < 𝑁) → (𝐾 < 𝐽 → ((𝐾𝐽) + 𝑁) ∈ (1..^𝑁))))
5756com12 32 . . . . . . . . . . . . 13 ((𝐾 ∈ ℕ0𝐾 < 𝑁) → (𝐽 ∈ (0..^𝑁) → (𝐾 < 𝐽 → ((𝐾𝐽) + 𝑁) ∈ (1..^𝑁))))
58573adant2 1126 . . . . . . . . . . . 12 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → (𝐽 ∈ (0..^𝑁) → (𝐾 < 𝐽 → ((𝐾𝐽) + 𝑁) ∈ (1..^𝑁))))
599, 58sylbi 207 . . . . . . . . . . 11 (𝐾 ∈ (0..^𝑁) → (𝐽 ∈ (0..^𝑁) → (𝐾 < 𝐽 → ((𝐾𝐽) + 𝑁) ∈ (1..^𝑁))))
601, 59syl 17 . . . . . . . . . 10 (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → (𝐽 ∈ (0..^𝑁) → (𝐾 < 𝐽 → ((𝐾𝐽) + 𝑁) ∈ (1..^𝑁))))
6160impcom 445 . . . . . . . . 9 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → (𝐾 < 𝐽 → ((𝐾𝐽) + 𝑁) ∈ (1..^𝑁)))
6261impcom 445 . . . . . . . 8 ((𝐾 < 𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) → ((𝐾𝐽) + 𝑁) ∈ (1..^𝑁))
63 oveq1 6818 . . . . . . . . . . 11 (𝑖 = ((𝐾𝐽) + 𝑁) → (𝑖 + 𝐽) = (((𝐾𝐽) + 𝑁) + 𝐽))
642zcnd 11673 . . . . . . . . . . . . . . . . . . . . 21 (𝐾 ∈ (0..^𝑁) → 𝐾 ∈ ℂ)
6564adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ (0..^𝑁) ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ)) → 𝐾 ∈ ℂ)
6614adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ) → 𝐽 ∈ ℂ)
6766adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ (0..^𝑁) ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ)) → 𝐽 ∈ ℂ)
6817adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ) → 𝑁 ∈ ℂ)
6968adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ (0..^𝑁) ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ)) → 𝑁 ∈ ℂ)
7065, 67, 693jca 1123 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ (0..^𝑁) ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ)) → (𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ))
7170ex 449 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ (0..^𝑁) → ((𝐽 ∈ ℕ0𝑁 ∈ ℕ) → (𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
721, 71syl 17 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → ((𝐽 ∈ ℕ0𝑁 ∈ ℕ) → (𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
7372com12 32 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ) → (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → (𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
74733adant3 1127 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → (𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
7510, 74sylbi 207 . . . . . . . . . . . . . 14 (𝐽 ∈ (0..^𝑁) → (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → (𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
7675imp 444 . . . . . . . . . . . . 13 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → (𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ))
7776adantl 473 . . . . . . . . . . . 12 ((𝐾 < 𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) → (𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ))
78 nppcan 10493 . . . . . . . . . . . 12 ((𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((𝐾𝐽) + 𝑁) + 𝐽) = (𝐾 + 𝑁))
7977, 78syl 17 . . . . . . . . . . 11 ((𝐾 < 𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) → (((𝐾𝐽) + 𝑁) + 𝐽) = (𝐾 + 𝑁))
8063, 79sylan9eqr 2814 . . . . . . . . . 10 (((𝐾 < 𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) ∧ 𝑖 = ((𝐾𝐽) + 𝑁)) → (𝑖 + 𝐽) = (𝐾 + 𝑁))
8180oveq1d 6826 . . . . . . . . 9 (((𝐾 < 𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) ∧ 𝑖 = ((𝐾𝐽) + 𝑁)) → ((𝑖 + 𝐽) mod 𝑁) = ((𝐾 + 𝑁) mod 𝑁))
8281eqeq2d 2768 . . . . . . . 8 (((𝐾 < 𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) ∧ 𝑖 = ((𝐾𝐽) + 𝑁)) → (𝐾 = ((𝑖 + 𝐽) mod 𝑁) ↔ 𝐾 = ((𝐾 + 𝑁) mod 𝑁)))
839biimpi 206 . . . . . . . . . . . . 13 (𝐾 ∈ (0..^𝑁) → (𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁))
8483a1d 25 . . . . . . . . . . . 12 (𝐾 ∈ (0..^𝑁) → (𝐽 ∈ (0..^𝑁) → (𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)))
851, 84syl 17 . . . . . . . . . . 11 (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → (𝐽 ∈ (0..^𝑁) → (𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)))
8685impcom 445 . . . . . . . . . 10 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → (𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁))
8786adantl 473 . . . . . . . . 9 ((𝐾 < 𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) → (𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁))
88 addmodidr 12911 . . . . . . . . . 10 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → ((𝐾 + 𝑁) mod 𝑁) = 𝐾)
8988eqcomd 2764 . . . . . . . . 9 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝐾 = ((𝐾 + 𝑁) mod 𝑁))
9087, 89syl 17 . . . . . . . 8 ((𝐾 < 𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) → 𝐾 = ((𝐾 + 𝑁) mod 𝑁))
9162, 82, 90rspcedvd 3454 . . . . . . 7 ((𝐾 < 𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁))
9291ex 449 . . . . . 6 (𝐾 < 𝐽 → ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)))
93 eldifsn 4460 . . . . . . . . 9 (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) ↔ (𝐾 ∈ (0..^𝑁) ∧ 𝐾𝐽))
94 eqneqall 2941 . . . . . . . . . . 11 (𝐾 = 𝐽 → (𝐾𝐽 → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)))
9594com12 32 . . . . . . . . . 10 (𝐾𝐽 → (𝐾 = 𝐽 → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)))
9695adantl 473 . . . . . . . . 9 ((𝐾 ∈ (0..^𝑁) ∧ 𝐾𝐽) → (𝐾 = 𝐽 → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)))
9793, 96sylbi 207 . . . . . . . 8 (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → (𝐾 = 𝐽 → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)))
9897adantl 473 . . . . . . 7 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → (𝐾 = 𝐽 → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)))
9998com12 32 . . . . . 6 (𝐾 = 𝐽 → ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)))
10092, 99jaoi 393 . . . . 5 ((𝐾 < 𝐽𝐾 = 𝐽) → ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)))
101100com12 32 . . . 4 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → ((𝐾 < 𝐽𝐾 = 𝐽) → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)))
1028, 101sylbid 230 . . 3 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → (𝐾𝐽 → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)))
103102com12 32 . 2 (𝐾𝐽 → ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)))
104 ltnle 10307 . . . . . . . . 9 ((𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝐽 < 𝐾 ↔ ¬ 𝐾𝐽))
1056, 4, 104syl2an 495 . . . . . . . 8 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → (𝐽 < 𝐾 ↔ ¬ 𝐾𝐽))
106105bicomd 213 . . . . . . 7 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → (¬ 𝐾𝐽𝐽 < 𝐾))
107223ad2ant1 1128 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝐽 ∈ ℤ)
108 nn0z 11590 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ ℕ0𝐾 ∈ ℤ)
109108adantr 472 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ ℕ0𝐾 < 𝑁) → 𝐾 ∈ ℤ)
110 znnsub 11613 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐽 < 𝐾 ↔ (𝐾𝐽) ∈ ℕ))
111107, 109, 110syl2anr 496 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ ℕ0𝐾 < 𝑁) ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → (𝐽 < 𝐾 ↔ (𝐾𝐽) ∈ ℕ))
112111biimpa 502 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ ℕ0𝐾 < 𝑁) ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) ∧ 𝐽 < 𝐾) → (𝐾𝐽) ∈ ℕ)
11331adantl 473 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ ℕ0𝐾 < 𝑁) ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → 𝑁 ∈ ℕ)
114113adantr 472 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ ℕ0𝐾 < 𝑁) ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) ∧ 𝐽 < 𝐾) → 𝑁 ∈ ℕ)
115 nn0ge0 11508 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 ∈ ℕ0 → 0 ≤ 𝐽)
1161153ad2ant1 1128 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 0 ≤ 𝐽)
117116adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ ℕ0 ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → 0 ≤ 𝐽)
118 subge02 10734 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) → (0 ≤ 𝐽 ↔ (𝐾𝐽) ≤ 𝐾))
11934, 38, 118syl2an 495 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ ℕ0 ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → (0 ≤ 𝐽 ↔ (𝐾𝐽) ≤ 𝐾))
120117, 119mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ ℕ0 ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → (𝐾𝐽) ≤ 𝐾)
12138adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℕ0 ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → 𝐽 ∈ ℝ)
12234adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℕ0 ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → 𝐾 ∈ ℝ)
12346adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℕ0 ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → 𝑁 ∈ ℝ)
124121, 122, 1233jca 1123 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ ℕ0 ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → (𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ))
12543ancoms 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝐾𝐽) ∈ ℝ)
1261253adant3 1127 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐾𝐽) ∈ ℝ)
127 simp2 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝐾 ∈ ℝ)
128 simp3 1133 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ∈ ℝ)
129126, 127, 1283jca 1123 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝐾𝐽) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ))
130124, 129syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ ℕ0 ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → ((𝐾𝐽) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ))
131 lelttr 10318 . . . . . . . . . . . . . . . . . . . 20 (((𝐾𝐽) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐾𝐽) ≤ 𝐾𝐾 < 𝑁) → (𝐾𝐽) < 𝑁))
132130, 131syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ ℕ0 ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → (((𝐾𝐽) ≤ 𝐾𝐾 < 𝑁) → (𝐾𝐽) < 𝑁))
133120, 132mpand 713 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ ℕ0 ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → (𝐾 < 𝑁 → (𝐾𝐽) < 𝑁))
134133impancom 455 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ ℕ0𝐾 < 𝑁) → ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐾𝐽) < 𝑁))
135134imp 444 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ ℕ0𝐾 < 𝑁) ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) → (𝐾𝐽) < 𝑁)
136135adantr 472 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ ℕ0𝐾 < 𝑁) ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) ∧ 𝐽 < 𝐾) → (𝐾𝐽) < 𝑁)
137112, 114, 1363jca 1123 . . . . . . . . . . . . . 14 ((((𝐾 ∈ ℕ0𝐾 < 𝑁) ∧ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) ∧ 𝐽 < 𝐾) → ((𝐾𝐽) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾𝐽) < 𝑁))
138137exp31 631 . . . . . . . . . . . . 13 ((𝐾 ∈ ℕ0𝐾 < 𝑁) → ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 < 𝐾 → ((𝐾𝐽) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾𝐽) < 𝑁))))
1391383adant2 1126 . . . . . . . . . . . 12 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 < 𝐾 → ((𝐾𝐽) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾𝐽) < 𝑁))))
1409, 139sylbi 207 . . . . . . . . . . 11 (𝐾 ∈ (0..^𝑁) → ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 < 𝐾 → ((𝐾𝐽) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾𝐽) < 𝑁))))
1411, 140syl 17 . . . . . . . . . 10 (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 < 𝐾 → ((𝐾𝐽) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾𝐽) < 𝑁))))
142141com12 32 . . . . . . . . 9 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → (𝐽 < 𝐾 → ((𝐾𝐽) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾𝐽) < 𝑁))))
14310, 142sylbi 207 . . . . . . . 8 (𝐽 ∈ (0..^𝑁) → (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → (𝐽 < 𝐾 → ((𝐾𝐽) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾𝐽) < 𝑁))))
144143imp 444 . . . . . . 7 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → (𝐽 < 𝐾 → ((𝐾𝐽) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾𝐽) < 𝑁)))
145106, 144sylbid 230 . . . . . 6 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → (¬ 𝐾𝐽 → ((𝐾𝐽) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾𝐽) < 𝑁)))
146145impcom 445 . . . . 5 ((¬ 𝐾𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) → ((𝐾𝐽) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾𝐽) < 𝑁))
147 elfzo1 12710 . . . . 5 ((𝐾𝐽) ∈ (1..^𝑁) ↔ ((𝐾𝐽) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾𝐽) < 𝑁))
148146, 147sylibr 224 . . . 4 ((¬ 𝐾𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) → (𝐾𝐽) ∈ (1..^𝑁))
149 oveq1 6818 . . . . . . 7 (𝑖 = (𝐾𝐽) → (𝑖 + 𝐽) = ((𝐾𝐽) + 𝐽))
1501, 64syl 17 . . . . . . . . 9 (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → 𝐾 ∈ ℂ)
1515zcnd 11673 . . . . . . . . 9 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℂ)
152 npcan 10480 . . . . . . . . 9 ((𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ) → ((𝐾𝐽) + 𝐽) = 𝐾)
153150, 151, 152syl2anr 496 . . . . . . . 8 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → ((𝐾𝐽) + 𝐽) = 𝐾)
154153adantl 473 . . . . . . 7 ((¬ 𝐾𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) → ((𝐾𝐽) + 𝐽) = 𝐾)
155149, 154sylan9eqr 2814 . . . . . 6 (((¬ 𝐾𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) ∧ 𝑖 = (𝐾𝐽)) → (𝑖 + 𝐽) = 𝐾)
156155oveq1d 6826 . . . . 5 (((¬ 𝐾𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) ∧ 𝑖 = (𝐾𝐽)) → ((𝑖 + 𝐽) mod 𝑁) = (𝐾 mod 𝑁))
157156eqeq2d 2768 . . . 4 (((¬ 𝐾𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) ∧ 𝑖 = (𝐾𝐽)) → (𝐾 = ((𝑖 + 𝐽) mod 𝑁) ↔ 𝐾 = (𝐾 mod 𝑁)))
158 zmodidfzoimp 12892 . . . . . . . 8 (𝐾 ∈ (0..^𝑁) → (𝐾 mod 𝑁) = 𝐾)
1591, 158syl 17 . . . . . . 7 (𝐾 ∈ ((0..^𝑁) ∖ {𝐽}) → (𝐾 mod 𝑁) = 𝐾)
160159adantl 473 . . . . . 6 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → (𝐾 mod 𝑁) = 𝐾)
161160adantl 473 . . . . 5 ((¬ 𝐾𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) → (𝐾 mod 𝑁) = 𝐾)
162161eqcomd 2764 . . . 4 ((¬ 𝐾𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) → 𝐾 = (𝐾 mod 𝑁))
163148, 157, 162rspcedvd 3454 . . 3 ((¬ 𝐾𝐽 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽}))) → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁))
164163ex 449 . 2 𝐾𝐽 → ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)))
165103, 164pm2.61i 176 1 ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1072   = wceq 1630   ∈ wcel 2137   ≠ wne 2930  ∃wrex 3049   ∖ cdif 3710  {csn 4319   class class class wbr 4802  (class class class)co 6811  ℂcc 10124  ℝcr 10125  0cc0 10126  1c1 10127   + caddc 10129   < clt 10264   ≤ cle 10265   − cmin 10456  ℕcn 11210  ℕ0cn0 11482  ℤcz 11567  ..^cfzo 12657   mod cmo 12860 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203  ax-pre-sup 10204 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-iun 4672  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-om 7229  df-1st 7331  df-2nd 7332  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-er 7909  df-en 8120  df-dom 8121  df-sdom 8122  df-sup 8511  df-inf 8512  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-div 10875  df-nn 11211  df-n0 11483  df-z 11568  df-uz 11878  df-rp 12024  df-ico 12372  df-fz 12518  df-fzo 12658  df-fl 12785  df-mod 12861 This theorem is referenced by:  cshimadifsn  13773
 Copyright terms: Public domain W3C validator