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

Theorem lgsdirprm 25253
Description: The Legendre symbol is completely multiplicative at the primes. See theorem 9.3 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 18-Mar-2022.)
Assertion
Ref Expression
lgsdirprm ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))

Proof of Theorem lgsdirprm
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simpl1 1228 . . . 4 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → 𝐴 ∈ ℤ)
2 simpl2 1230 . . . 4 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → 𝐵 ∈ ℤ)
3 lgsdir2 25252 . . . 4 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /L 2) = ((𝐴 /L 2) · (𝐵 /L 2)))
41, 2, 3syl2anc 696 . . 3 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → ((𝐴 · 𝐵) /L 2) = ((𝐴 /L 2) · (𝐵 /L 2)))
5 simpr 479 . . . 4 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → 𝑃 = 2)
65oveq2d 6827 . . 3 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 · 𝐵) /L 2))
75oveq2d 6827 . . . 4 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → (𝐴 /L 𝑃) = (𝐴 /L 2))
85oveq2d 6827 . . . 4 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → (𝐵 /L 𝑃) = (𝐵 /L 2))
97, 8oveq12d 6829 . . 3 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) = ((𝐴 /L 2) · (𝐵 /L 2)))
104, 6, 93eqtr4d 2802 . 2 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 = 2) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))
11 simpl1 1228 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝐴 ∈ ℤ)
12 simpl2 1230 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝐵 ∈ ℤ)
1311, 12zmulcld 11678 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴 · 𝐵) ∈ ℤ)
14 simpl3 1232 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∈ ℙ)
15 prmz 15589 . . . . . 6 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
1614, 15syl 17 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∈ ℤ)
17 lgscl 25233 . . . . 5 (((𝐴 · 𝐵) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐴 · 𝐵) /L 𝑃) ∈ ℤ)
1813, 16, 17syl2anc 696 . . . 4 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 · 𝐵) /L 𝑃) ∈ ℤ)
1918zcnd 11673 . . 3 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 · 𝐵) /L 𝑃) ∈ ℂ)
20 lgscl 25233 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐴 /L 𝑃) ∈ ℤ)
2111, 16, 20syl2anc 696 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴 /L 𝑃) ∈ ℤ)
22 lgscl 25233 . . . . . 6 ((𝐵 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐵 /L 𝑃) ∈ ℤ)
2312, 16, 22syl2anc 696 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵 /L 𝑃) ∈ ℤ)
2421, 23zmulcld 11678 . . . 4 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ ℤ)
2524zcnd 11673 . . 3 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ ℂ)
2619, 25subcld 10582 . . . 4 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ∈ ℂ)
2726abscld 14372 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ∈ ℝ)
28 prmnn 15588 . . . . . . . 8 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2914, 28syl 17 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∈ ℕ)
3029nnrpd 12061 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∈ ℝ+)
3126absge0d 14380 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 0 ≤ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))))
32 2re 11280 . . . . . . . 8 2 ∈ ℝ
3332a1i 11 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 2 ∈ ℝ)
3429nnred 11225 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∈ ℝ)
3519abscld 14372 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (abs‘((𝐴 · 𝐵) /L 𝑃)) ∈ ℝ)
3625abscld 14372 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ∈ ℝ)
3735, 36readdcld 10259 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((abs‘((𝐴 · 𝐵) /L 𝑃)) + (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ∈ ℝ)
3819, 25abs2dif2d 14394 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ≤ ((abs‘((𝐴 · 𝐵) /L 𝑃)) + (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))))
39 1red 10245 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 1 ∈ ℝ)
40 lgsle1 25234 . . . . . . . . . . 11 (((𝐴 · 𝐵) ∈ ℤ ∧ 𝑃 ∈ ℤ) → (abs‘((𝐴 · 𝐵) /L 𝑃)) ≤ 1)
4113, 16, 40syl2anc 696 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (abs‘((𝐴 · 𝐵) /L 𝑃)) ≤ 1)
42 eqid 2758 . . . . . . . . . . . . . 14 {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}
4342lgscl2 25231 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐴 /L 𝑃) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1})
4411, 16, 43syl2anc 696 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴 /L 𝑃) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1})
4542lgscl2 25231 . . . . . . . . . . . . 13 ((𝐵 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐵 /L 𝑃) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1})
4612, 16, 45syl2anc 696 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵 /L 𝑃) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1})
4742lgslem3 25221 . . . . . . . . . . . 12 (((𝐴 /L 𝑃) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} ∧ (𝐵 /L 𝑃) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}) → ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1})
4844, 46, 47syl2anc 696 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1})
49 fveq2 6350 . . . . . . . . . . . . . 14 (𝑥 = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) → (abs‘𝑥) = (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃))))
5049breq1d 4812 . . . . . . . . . . . . 13 (𝑥 = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) → ((abs‘𝑥) ≤ 1 ↔ (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ≤ 1))
5150elrab 3502 . . . . . . . . . . . 12 (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} ↔ (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ ℤ ∧ (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ≤ 1))
5251simprbi 483 . . . . . . . . . . 11 (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1} → (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ≤ 1)
5348, 52syl 17 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ≤ 1)
5435, 36, 39, 39, 41, 53le2addd 10836 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((abs‘((𝐴 · 𝐵) /L 𝑃)) + (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ≤ (1 + 1))
55 df-2 11269 . . . . . . . . 9 2 = (1 + 1)
5654, 55syl6breqr 4844 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((abs‘((𝐴 · 𝐵) /L 𝑃)) + (abs‘((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ≤ 2)
5727, 37, 33, 38, 56letrd 10384 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ≤ 2)
58 prmuz2 15608 . . . . . . . . 9 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
59 eluzle 11890 . . . . . . . . 9 (𝑃 ∈ (ℤ‘2) → 2 ≤ 𝑃)
6014, 58, 593syl 18 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 2 ≤ 𝑃)
61 simpr 479 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ≠ 2)
62 ltlen 10328 . . . . . . . . 9 ((2 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (2 < 𝑃 ↔ (2 ≤ 𝑃𝑃 ≠ 2)))
6332, 34, 62sylancr 698 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (2 < 𝑃 ↔ (2 ≤ 𝑃𝑃 ≠ 2)))
6460, 61, 63mpbir2and 995 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 2 < 𝑃)
6527, 33, 34, 57, 64lelttrd 10385 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) < 𝑃)
66 modid 12887 . . . . . 6 ((((abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ∈ ℝ ∧ 𝑃 ∈ ℝ+) ∧ (0 ≤ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) ∧ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) < 𝑃)) → ((abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) mod 𝑃) = (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))))
6727, 30, 31, 65, 66syl22anc 1478 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) mod 𝑃) = (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))))
6811zcnd 11673 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝐴 ∈ ℂ)
6912zcnd 11673 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝐵 ∈ ℂ)
70 eldifsn 4460 . . . . . . . . . . . . . . 15 (𝑃 ∈ (ℙ ∖ {2}) ↔ (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
7114, 61, 70sylanbrc 701 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∈ (ℙ ∖ {2}))
72 oddprm 15715 . . . . . . . . . . . . . 14 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
7371, 72syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝑃 − 1) / 2) ∈ ℕ)
7473nnnn0d 11541 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝑃 − 1) / 2) ∈ ℕ0)
7568, 69, 74mulexpd 13215 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 · 𝐵)↑((𝑃 − 1) / 2)) = ((𝐴↑((𝑃 − 1) / 2)) · (𝐵↑((𝑃 − 1) / 2))))
76 zexpcl 13067 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ0) → (𝐴↑((𝑃 − 1) / 2)) ∈ ℤ)
7711, 74, 76syl2anc 696 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴↑((𝑃 − 1) / 2)) ∈ ℤ)
7877zcnd 11673 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴↑((𝑃 − 1) / 2)) ∈ ℂ)
79 zexpcl 13067 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ0) → (𝐵↑((𝑃 − 1) / 2)) ∈ ℤ)
8012, 74, 79syl2anc 696 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵↑((𝑃 − 1) / 2)) ∈ ℤ)
8180zcnd 11673 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵↑((𝑃 − 1) / 2)) ∈ ℂ)
8278, 81mulcomd 10251 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴↑((𝑃 − 1) / 2)) · (𝐵↑((𝑃 − 1) / 2))) = ((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2))))
8375, 82eqtrd 2792 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 · 𝐵)↑((𝑃 − 1) / 2)) = ((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2))))
8483oveq1d 6826 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 · 𝐵)↑((𝑃 − 1) / 2)) mod 𝑃) = (((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃))
85 lgsvalmod 25238 . . . . . . . . . 10 (((𝐴 · 𝐵) ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((𝐴 · 𝐵) /L 𝑃) mod 𝑃) = (((𝐴 · 𝐵)↑((𝑃 − 1) / 2)) mod 𝑃))
8613, 71, 85syl2anc 696 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 · 𝐵) /L 𝑃) mod 𝑃) = (((𝐴 · 𝐵)↑((𝑃 − 1) / 2)) mod 𝑃))
8721zred 11672 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴 /L 𝑃) ∈ ℝ)
8877zred 11672 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐴↑((𝑃 − 1) / 2)) ∈ ℝ)
89 lgsvalmod 25238 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) mod 𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃))
9011, 71, 89syl2anc 696 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 /L 𝑃) mod 𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃))
91 modmul1 12915 . . . . . . . . . . 11 ((((𝐴 /L 𝑃) ∈ ℝ ∧ (𝐴↑((𝑃 − 1) / 2)) ∈ ℝ) ∧ ((𝐵 /L 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℝ+) ∧ ((𝐴 /L 𝑃) mod 𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃)) → (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) mod 𝑃) = (((𝐴↑((𝑃 − 1) / 2)) · (𝐵 /L 𝑃)) mod 𝑃))
9287, 88, 23, 30, 90, 91syl221anc 1488 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) mod 𝑃) = (((𝐴↑((𝑃 − 1) / 2)) · (𝐵 /L 𝑃)) mod 𝑃))
9323zcnd 11673 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵 /L 𝑃) ∈ ℂ)
9478, 93mulcomd 10251 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴↑((𝑃 − 1) / 2)) · (𝐵 /L 𝑃)) = ((𝐵 /L 𝑃) · (𝐴↑((𝑃 − 1) / 2))))
9594oveq1d 6826 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴↑((𝑃 − 1) / 2)) · (𝐵 /L 𝑃)) mod 𝑃) = (((𝐵 /L 𝑃) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃))
9623zred 11672 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵 /L 𝑃) ∈ ℝ)
9780zred 11672 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝐵↑((𝑃 − 1) / 2)) ∈ ℝ)
98 lgsvalmod 25238 . . . . . . . . . . . 12 ((𝐵 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐵 /L 𝑃) mod 𝑃) = ((𝐵↑((𝑃 − 1) / 2)) mod 𝑃))
9912, 71, 98syl2anc 696 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐵 /L 𝑃) mod 𝑃) = ((𝐵↑((𝑃 − 1) / 2)) mod 𝑃))
100 modmul1 12915 . . . . . . . . . . 11 ((((𝐵 /L 𝑃) ∈ ℝ ∧ (𝐵↑((𝑃 − 1) / 2)) ∈ ℝ) ∧ ((𝐴↑((𝑃 − 1) / 2)) ∈ ℤ ∧ 𝑃 ∈ ℝ+) ∧ ((𝐵 /L 𝑃) mod 𝑃) = ((𝐵↑((𝑃 − 1) / 2)) mod 𝑃)) → (((𝐵 /L 𝑃) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃) = (((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃))
10196, 97, 77, 30, 99, 100syl221anc 1488 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐵 /L 𝑃) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃) = (((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃))
10292, 95, 1013eqtrd 2796 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) mod 𝑃) = (((𝐵↑((𝑃 − 1) / 2)) · (𝐴↑((𝑃 − 1) / 2))) mod 𝑃))
10384, 86, 1023eqtr4d 2802 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 · 𝐵) /L 𝑃) mod 𝑃) = (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) mod 𝑃))
104 moddvds 15191 . . . . . . . . 9 ((𝑃 ∈ ℕ ∧ ((𝐴 · 𝐵) /L 𝑃) ∈ ℤ ∧ ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) ∈ ℤ) → ((((𝐴 · 𝐵) /L 𝑃) mod 𝑃) = (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) mod 𝑃) ↔ 𝑃 ∥ (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))))
10529, 18, 24, 104syl3anc 1477 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((((𝐴 · 𝐵) /L 𝑃) mod 𝑃) = (((𝐴 /L 𝑃) · (𝐵 /L 𝑃)) mod 𝑃) ↔ 𝑃 ∥ (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))))
106103, 105mpbid 222 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∥ (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))))
10718, 24zsubcld 11677 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ∈ ℤ)
108 dvdsabsb 15201 . . . . . . . 8 ((𝑃 ∈ ℤ ∧ (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ∈ ℤ) → (𝑃 ∥ (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ↔ 𝑃 ∥ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))))))
10916, 107, 108syl2anc 696 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (𝑃 ∥ (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) ↔ 𝑃 ∥ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))))))
110106, 109mpbid 222 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → 𝑃 ∥ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))))
111 dvdsmod0 15186 . . . . . 6 ((𝑃 ∈ ℕ ∧ 𝑃 ∥ (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))))) → ((abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) mod 𝑃) = 0)
11229, 110, 111syl2anc 696 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) mod 𝑃) = 0)
11367, 112eqtr3d 2794 . . . 4 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (abs‘(((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))) = 0)
11426, 113abs00d 14382 . . 3 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → (((𝐴 · 𝐵) /L 𝑃) − ((𝐴 /L 𝑃) · (𝐵 /L 𝑃))) = 0)
11519, 25, 114subeq0d 10590 . 2 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ≠ 2) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))
11610, 115pm2.61dane 3017 1 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1630  wcel 2137  wne 2930  {crab 3052  cdif 3710  {csn 4319   class class class wbr 4802  cfv 6047  (class class class)co 6811  cr 10125  0cc0 10126  1c1 10127   + caddc 10129   · cmul 10131   < clt 10264  cle 10265  cmin 10456   / cdiv 10874  cn 11210  2c2 11260  0cn0 11482  cz 11567  cuz 11877  +crp 12023   mod cmo 12860  cexp 13052  abscabs 14171  cdvds 15180  cprime 15585   /L clgs 25216
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-rep 4921  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-int 4626  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-1o 7727  df-2o 7728  df-oadd 7731  df-er 7909  df-map 8023  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-sup 8511  df-inf 8512  df-card 8953  df-cda 9180  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-2 11269  df-3 11270  df-4 11271  df-5 11272  df-6 11273  df-7 11274  df-8 11275  df-9 11276  df-n0 11483  df-xnn0 11554  df-z 11568  df-uz 11878  df-q 11980  df-rp 12024  df-fz 12518  df-fzo 12658  df-fl 12785  df-mod 12861  df-seq 12994  df-exp 13053  df-hash 13310  df-cj 14036  df-re 14037  df-im 14038  df-sqrt 14172  df-abs 14173  df-dvds 15181  df-gcd 15417  df-prm 15586  df-phi 15671  df-pc 15742  df-lgs 25217
This theorem is referenced by:  lgsdir  25254
  Copyright terms: Public domain W3C validator