ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  lgsval GIF version

Theorem lgsval 14072
Description: Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
Hypothesis
Ref Expression
lgsval.1 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))
Assertion
Ref Expression
lgsval ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))
Distinct variable groups:   𝐴,𝑛   𝑛,𝑁
Allowed substitution hint:   𝐹(𝑛)

Proof of Theorem lgsval
Dummy variables 𝑎 𝑚 𝑘 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1zzd 9269 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 1 ∈ ℤ)
2 0zd 9254 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 0 ∈ ℤ)
3 zsqcl 10576 . . . . . 6 (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
43ad2antrr 488 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℤ)
5 zdceq 9317 . . . . 5 (((𝐴↑2) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴↑2) = 1)
64, 1, 5syl2anc 411 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → DECID (𝐴↑2) = 1)
71, 2, 6ifcldcd 3569 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → if((𝐴↑2) = 1, 1, 0) ∈ ℤ)
8 neg1z 9274 . . . . . 6 -1 ∈ ℤ
98a1i 9 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → -1 ∈ ℤ)
10 1zzd 9269 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 1 ∈ ℤ)
11 simpr 110 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
12 0zd 9254 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 0 ∈ ℤ)
13 zdclt 9319 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 < 0)
1411, 12, 13syl2an2r 595 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID 𝑁 < 0)
15 simpl 109 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐴 ∈ ℤ)
16 zdclt 9319 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝐴 < 0)
1715, 12, 16syl2an2r 595 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID 𝐴 < 0)
18 dcan2 934 . . . . . 6 (DECID 𝑁 < 0 → (DECID 𝐴 < 0 → DECID (𝑁 < 0 ∧ 𝐴 < 0)))
1914, 17, 18sylc 62 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID (𝑁 < 0 ∧ 𝐴 < 0))
209, 10, 19ifcldcd 3569 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℤ)
21 nnuz 9552 . . . . . 6 ℕ = (ℤ‘1)
22 lgsval.1 . . . . . . . 8 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))
23 eleq1w 2238 . . . . . . . . 9 (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
24 eqeq1 2184 . . . . . . . . . . 11 (𝑛 = 𝑘 → (𝑛 = 2 ↔ 𝑘 = 2))
25 oveq1 5876 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → (𝑛 − 1) = (𝑘 − 1))
2625oveq1d 5884 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → ((𝑛 − 1) / 2) = ((𝑘 − 1) / 2))
2726oveq2d 5885 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝐴↑((𝑛 − 1) / 2)) = (𝐴↑((𝑘 − 1) / 2)))
2827oveq1d 5884 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ((𝐴↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑘 − 1) / 2)) + 1))
29 id 19 . . . . . . . . . . . . 13 (𝑛 = 𝑘𝑛 = 𝑘)
3028, 29oveq12d 5887 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘))
3130oveq1d 5884 . . . . . . . . . . 11 (𝑛 = 𝑘 → ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))
3224, 31ifbieq2d 3558 . . . . . . . . . 10 (𝑛 = 𝑘 → if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) = if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1)))
33 oveq1 5876 . . . . . . . . . 10 (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
3432, 33oveq12d 5887 . . . . . . . . 9 (𝑛 = 𝑘 → (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)) = (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)))
3523, 34ifbieq1d 3556 . . . . . . . 8 (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)), 1))
36 simpr 110 . . . . . . . 8 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
37 0zd 9254 . . . . . . . . . . . 12 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 0 ∈ ℤ)
38 1zzd 9269 . . . . . . . . . . . . 13 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 1 ∈ ℤ)
3938znegcld 9366 . . . . . . . . . . . . 13 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → -1 ∈ ℤ)
40 id 19 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℤ → 𝐴 ∈ ℤ)
41 8nn 9075 . . . . . . . . . . . . . . . . . . . 20 8 ∈ ℕ
4241a1i 9 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℤ → 8 ∈ ℕ)
4340, 42zmodcld 10331 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℕ0)
4443nn0zd 9362 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℤ)
45 1zzd 9269 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℤ → 1 ∈ ℤ)
46 zdceq 9317 . . . . . . . . . . . . . . . . 17 (((𝐴 mod 8) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 mod 8) = 1)
4744, 45, 46syl2anc 411 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 1)
48 7nn 9074 . . . . . . . . . . . . . . . . . 18 7 ∈ ℕ
4948nnzi 9263 . . . . . . . . . . . . . . . . 17 7 ∈ ℤ
50 zdceq 9317 . . . . . . . . . . . . . . . . 17 (((𝐴 mod 8) ∈ ℤ ∧ 7 ∈ ℤ) → DECID (𝐴 mod 8) = 7)
5144, 49, 50sylancl 413 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 7)
52 dcor 935 . . . . . . . . . . . . . . . 16 (DECID (𝐴 mod 8) = 1 → (DECID (𝐴 mod 8) = 7 → DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
5347, 51, 52sylc 62 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℤ → DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7))
54 elprg 3611 . . . . . . . . . . . . . . . . 17 ((𝐴 mod 8) ∈ ℕ0 → ((𝐴 mod 8) ∈ {1, 7} ↔ ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
5543, 54syl 14 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℤ → ((𝐴 mod 8) ∈ {1, 7} ↔ ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
5655dcbid 838 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℤ → (DECID (𝐴 mod 8) ∈ {1, 7} ↔ DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
5753, 56mpbird 167 . . . . . . . . . . . . . 14 (𝐴 ∈ ℤ → DECID (𝐴 mod 8) ∈ {1, 7})
5857ad5antr 496 . . . . . . . . . . . . 13 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → DECID (𝐴 mod 8) ∈ {1, 7})
5938, 39, 58ifcldcd 3569 . . . . . . . . . . . 12 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ∈ ℤ)
60 2nn 9069 . . . . . . . . . . . . . 14 2 ∈ ℕ
6160a1i 9 . . . . . . . . . . . . 13 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 2 ∈ ℕ)
62 simp-5l 543 . . . . . . . . . . . . 13 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 𝐴 ∈ ℤ)
63 dvdsdc 11789 . . . . . . . . . . . . 13 ((2 ∈ ℕ ∧ 𝐴 ∈ ℤ) → DECID 2 ∥ 𝐴)
6461, 62, 63syl2anc 411 . . . . . . . . . . . 12 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → DECID 2 ∥ 𝐴)
6537, 59, 64ifcldcd 3569 . . . . . . . . . . 11 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) ∈ ℤ)
66 simp-5l 543 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 𝐴 ∈ ℤ)
67 simpr 110 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ¬ 𝑘 = 2)
68 prm2orodd 12109 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℙ → (𝑘 = 2 ∨ ¬ 2 ∥ 𝑘))
6968orcomd 729 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℙ → (¬ 2 ∥ 𝑘𝑘 = 2))
7069ad2antlr 489 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (¬ 2 ∥ 𝑘𝑘 = 2))
7167, 70ecased 1349 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ¬ 2 ∥ 𝑘)
72 prmnn 12093 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℙ → 𝑘 ∈ ℕ)
7372nnnn0d 9218 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℙ → 𝑘 ∈ ℕ0)
74 nn0oddm1d2 11897 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ0 → (¬ 2 ∥ 𝑘 ↔ ((𝑘 − 1) / 2) ∈ ℕ0))
7573, 74syl 14 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℙ → (¬ 2 ∥ 𝑘 ↔ ((𝑘 − 1) / 2) ∈ ℕ0))
7675ad2antlr 489 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (¬ 2 ∥ 𝑘 ↔ ((𝑘 − 1) / 2) ∈ ℕ0))
7771, 76mpbid 147 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((𝑘 − 1) / 2) ∈ ℕ0)
78 zexpcl 10521 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ ((𝑘 − 1) / 2) ∈ ℕ0) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
7966, 77, 78syl2anc 411 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
8079peano2zd 9367 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((𝐴↑((𝑘 − 1) / 2)) + 1) ∈ ℤ)
8136ad2antrr 488 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 𝑘 ∈ ℕ)
8280, 81zmodcld 10331 . . . . . . . . . . . . 13 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) ∈ ℕ0)
8382nn0zd 9362 . . . . . . . . . . . 12 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) ∈ ℤ)
84 1zzd 9269 . . . . . . . . . . . 12 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 1 ∈ ℤ)
8583, 84zsubcld 9369 . . . . . . . . . . 11 ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1) ∈ ℤ)
86 nnz 9261 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
8786ad2antlr 489 . . . . . . . . . . . 12 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
88 2z 9270 . . . . . . . . . . . 12 2 ∈ ℤ
89 zdceq 9317 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ 2 ∈ ℤ) → DECID 𝑘 = 2)
9087, 88, 89sylancl 413 . . . . . . . . . . 11 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → DECID 𝑘 = 2)
9165, 85, 90ifcldadc 3563 . . . . . . . . . 10 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1)) ∈ ℤ)
92 simpr 110 . . . . . . . . . . 11 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ)
93 simp-4r 542 . . . . . . . . . . 11 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
94 neqne 2355 . . . . . . . . . . . 12 𝑁 = 0 → 𝑁 ≠ 0)
9594ad3antlr 493 . . . . . . . . . . 11 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
96 pczcl 12281 . . . . . . . . . . 11 ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ0)
9792, 93, 95, 96syl12anc 1236 . . . . . . . . . 10 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ0)
98 zexpcl 10521 . . . . . . . . . 10 ((if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1)) ∈ ℤ ∧ (𝑘 pCnt 𝑁) ∈ ℕ0) → (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)) ∈ ℤ)
9991, 97, 98syl2anc 411 . . . . . . . . 9 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)) ∈ ℤ)
100 1zzd 9269 . . . . . . . . 9 (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ ℤ)
101 prmdc 12113 . . . . . . . . . 10 (𝑘 ∈ ℕ → DECID 𝑘 ∈ ℙ)
102101adantl 277 . . . . . . . . 9 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → DECID 𝑘 ∈ ℙ)
10399, 100, 102ifcldadc 3563 . . . . . . . 8 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → if(𝑘 ∈ ℙ, (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)), 1) ∈ ℤ)
10422, 35, 36, 103fvmptd3 5605 . . . . . . 7 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = if(𝑘 ∈ ℙ, (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)), 1))
105104, 103eqeltrd 2254 . . . . . 6 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℤ)
106 zmulcl 9295 . . . . . . 7 ((𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ) → (𝑘 · 𝑣) ∈ ℤ)
107106adantl 277 . . . . . 6 ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ (𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (𝑘 · 𝑣) ∈ ℤ)
10821, 10, 105, 107seqf 10447 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → seq1( · , 𝐹):ℕ⟶ℤ)
109 simplr 528 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 𝑁 ∈ ℤ)
11094adantl 277 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 𝑁 ≠ 0)
111 nnabscl 11093 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
112109, 110, 111syl2anc 411 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (abs‘𝑁) ∈ ℕ)
113108, 112ffvelcdmd 5648 . . . 4 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (seq1( · , 𝐹)‘(abs‘𝑁)) ∈ ℤ)
11420, 113zmulcld 9370 . . 3 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))) ∈ ℤ)
115 0zd 9254 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ∈ ℤ)
116 zdceq 9317 . . . 4 ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
11711, 115, 116syl2anc 411 . . 3 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑁 = 0)
1187, 114, 117ifcldadc 3563 . 2 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))) ∈ ℤ)
119 simpr 110 . . . . 5 ((𝑎 = 𝐴𝑚 = 𝑁) → 𝑚 = 𝑁)
120119eqeq1d 2186 . . . 4 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑚 = 0 ↔ 𝑁 = 0))
121 simpl 109 . . . . . . 7 ((𝑎 = 𝐴𝑚 = 𝑁) → 𝑎 = 𝐴)
122121oveq1d 5884 . . . . . 6 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑎↑2) = (𝐴↑2))
123122eqeq1d 2186 . . . . 5 ((𝑎 = 𝐴𝑚 = 𝑁) → ((𝑎↑2) = 1 ↔ (𝐴↑2) = 1))
124123ifbid 3555 . . . 4 ((𝑎 = 𝐴𝑚 = 𝑁) → if((𝑎↑2) = 1, 1, 0) = if((𝐴↑2) = 1, 1, 0))
125119breq1d 4010 . . . . . . 7 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑚 < 0 ↔ 𝑁 < 0))
126121breq1d 4010 . . . . . . 7 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑎 < 0 ↔ 𝐴 < 0))
127125, 126anbi12d 473 . . . . . 6 ((𝑎 = 𝐴𝑚 = 𝑁) → ((𝑚 < 0 ∧ 𝑎 < 0) ↔ (𝑁 < 0 ∧ 𝐴 < 0)))
128127ifbid 3555 . . . . 5 ((𝑎 = 𝐴𝑚 = 𝑁) → if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1))
129121breq2d 4012 . . . . . . . . . . . . 13 ((𝑎 = 𝐴𝑚 = 𝑁) → (2 ∥ 𝑎 ↔ 2 ∥ 𝐴))
130121oveq1d 5884 . . . . . . . . . . . . . . 15 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑎 mod 8) = (𝐴 mod 8))
131130eleq1d 2246 . . . . . . . . . . . . . 14 ((𝑎 = 𝐴𝑚 = 𝑁) → ((𝑎 mod 8) ∈ {1, 7} ↔ (𝐴 mod 8) ∈ {1, 7}))
132131ifbid 3555 . . . . . . . . . . . . 13 ((𝑎 = 𝐴𝑚 = 𝑁) → if((𝑎 mod 8) ∈ {1, 7}, 1, -1) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
133129, 132ifbieq2d 3558 . . . . . . . . . . . 12 ((𝑎 = 𝐴𝑚 = 𝑁) → if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
134121oveq1d 5884 . . . . . . . . . . . . . . 15 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑎↑((𝑛 − 1) / 2)) = (𝐴↑((𝑛 − 1) / 2)))
135134oveq1d 5884 . . . . . . . . . . . . . 14 ((𝑎 = 𝐴𝑚 = 𝑁) → ((𝑎↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑛 − 1) / 2)) + 1))
136135oveq1d 5884 . . . . . . . . . . . . 13 ((𝑎 = 𝐴𝑚 = 𝑁) → (((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛))
137136oveq1d 5884 . . . . . . . . . . . 12 ((𝑎 = 𝐴𝑚 = 𝑁) → ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))
138133, 137ifeq12d 3553 . . . . . . . . . . 11 ((𝑎 = 𝐴𝑚 = 𝑁) → if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) = if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)))
139119oveq2d 5885 . . . . . . . . . . 11 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑛 pCnt 𝑚) = (𝑛 pCnt 𝑁))
140138, 139oveq12d 5887 . . . . . . . . . 10 ((𝑎 = 𝐴𝑚 = 𝑁) → (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)) = (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)))
141140ifeq1d 3551 . . . . . . . . 9 ((𝑎 = 𝐴𝑚 = 𝑁) → if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1) = if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))
142141mpteq2dv 4091 . . . . . . . 8 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)))
143142, 22eqtr4di 2228 . . . . . . 7 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)) = 𝐹)
144143seqeq3d 10439 . . . . . 6 ((𝑎 = 𝐴𝑚 = 𝑁) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1))) = seq1( · , 𝐹))
145119fveq2d 5515 . . . . . 6 ((𝑎 = 𝐴𝑚 = 𝑁) → (abs‘𝑚) = (abs‘𝑁))
146144, 145fveq12d 5518 . . . . 5 ((𝑎 = 𝐴𝑚 = 𝑁) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚)) = (seq1( · , 𝐹)‘(abs‘𝑁)))
147128, 146oveq12d 5887 . . . 4 ((𝑎 = 𝐴𝑚 = 𝑁) → (if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚))) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))))
148120, 124, 147ifbieq12d 3560 . . 3 ((𝑎 = 𝐴𝑚 = 𝑁) → if(𝑚 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚)))) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))
149 df-lgs 14066 . . 3 /L = (𝑎 ∈ ℤ, 𝑚 ∈ ℤ ↦ if(𝑚 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚)))))
150148, 149ovmpoga 5998 . 2 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))) ∈ ℤ) → (𝐴 /L 𝑁) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))
151118, 150mpd3an3 1338 1 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834   = wceq 1353  wcel 2148  wne 2347  ifcif 3534  {cpr 3592   class class class wbr 4000  cmpt 4061  cfv 5212  (class class class)co 5869  0cc0 7802  1c1 7803   + caddc 7805   · cmul 7807   < clt 7982  cmin 8118  -cneg 8119   / cdiv 8618  cn 8908  2c2 8959  7c7 8964  8c8 8965  0cn0 9165  cz 9242   mod cmo 10308  seqcseq 10431  cexp 10505  abscabs 10990  cdvds 11778  cprime 12090   pCnt cpc 12267   /L clgs 14065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584  ax-cnex 7893  ax-resscn 7894  ax-1cn 7895  ax-1re 7896  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-mulrcl 7901  ax-addcom 7902  ax-mulcom 7903  ax-addass 7904  ax-mulass 7905  ax-distr 7906  ax-i2m1 7907  ax-0lt1 7908  ax-1rid 7909  ax-0id 7910  ax-rnegex 7911  ax-precex 7912  ax-cnre 7913  ax-pre-ltirr 7914  ax-pre-ltwlin 7915  ax-pre-lttrn 7916  ax-pre-apti 7917  ax-pre-ltadd 7918  ax-pre-mulgt0 7919  ax-pre-mulext 7920  ax-arch 7921  ax-caucvg 7922
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-xor 1376  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-po 4293  df-iso 4294  df-iord 4363  df-on 4365  df-ilim 4366  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-isom 5221  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-frec 6386  df-1o 6411  df-2o 6412  df-er 6529  df-en 6735  df-fin 6737  df-sup 6977  df-inf 6978  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988  df-sub 8120  df-neg 8121  df-reap 8522  df-ap 8529  df-div 8619  df-inn 8909  df-2 8967  df-3 8968  df-4 8969  df-5 8970  df-6 8971  df-7 8972  df-8 8973  df-n0 9166  df-z 9243  df-uz 9518  df-q 9609  df-rp 9641  df-fz 9996  df-fzo 10129  df-fl 10256  df-mod 10309  df-seqfrec 10432  df-exp 10506  df-cj 10835  df-re 10836  df-im 10837  df-rsqrt 10991  df-abs 10992  df-dvds 11779  df-gcd 11927  df-prm 12091  df-pc 12268  df-lgs 14066
This theorem is referenced by:  lgscllem  14075  lgsval2lem  14078  lgs0  14081  lgsval4  14088
  Copyright terms: Public domain W3C validator