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

Theorem eulerthlema 12105
Description: Lemma for eulerth 12108. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
Hypotheses
Ref Expression
eulerth.1 (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))
eulerth.2 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
eulerth.4 (𝜑𝐹:(1...(ϕ‘𝑁))–1-1-onto𝑆)
Assertion
Ref Expression
eulerthlema (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝑁   𝑦,𝑁   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑦)   𝑆(𝑥,𝑦)   𝐹(𝑦)

Proof of Theorem eulerthlema
Dummy variables 𝑘 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eulerth.1 . . . . . 6 (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))
21simp1d 994 . . . . 5 (𝜑𝑁 ∈ ℕ)
32phicld 12093 . . . 4 (𝜑 → (ϕ‘𝑁) ∈ ℕ)
4 elnnuz 9475 . . . 4 ((ϕ‘𝑁) ∈ ℕ ↔ (ϕ‘𝑁) ∈ (ℤ‘1))
53, 4sylib 121 . . 3 (𝜑 → (ϕ‘𝑁) ∈ (ℤ‘1))
6 eluzfz2 9934 . . 3 ((ϕ‘𝑁) ∈ (ℤ‘1) → (ϕ‘𝑁) ∈ (1...(ϕ‘𝑁)))
75, 6syl 14 . 2 (𝜑 → (ϕ‘𝑁) ∈ (1...(ϕ‘𝑁)))
8 oveq2 5832 . . . . . . 7 (𝑤 = 1 → (𝐴𝑤) = (𝐴↑1))
9 oveq2 5832 . . . . . . . 8 (𝑤 = 1 → (1...𝑤) = (1...1))
109prodeq1d 11461 . . . . . . 7 (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)(𝐹𝑥) = ∏𝑥 ∈ (1...1)(𝐹𝑥))
118, 10oveq12d 5842 . . . . . 6 (𝑤 = 1 → ((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) = ((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹𝑥)))
1211oveq1d 5839 . . . . 5 (𝑤 = 1 → (((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) mod 𝑁) = (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹𝑥)) mod 𝑁))
139prodeq1d 11461 . . . . . 6 (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...1)((𝐴 · (𝐹𝑥)) mod 𝑁))
1413oveq1d 5839 . . . . 5 (𝑤 = 1 → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))
1512, 14eqeq12d 2172 . . . 4 (𝑤 = 1 → ((((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)))
1615imbi2d 229 . . 3 (𝑤 = 1 → ((𝜑 → (((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))))
17 oveq2 5832 . . . . . . 7 (𝑤 = 𝑘 → (𝐴𝑤) = (𝐴𝑘))
18 oveq2 5832 . . . . . . . 8 (𝑤 = 𝑘 → (1...𝑤) = (1...𝑘))
1918prodeq1d 11461 . . . . . . 7 (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)(𝐹𝑥) = ∏𝑥 ∈ (1...𝑘)(𝐹𝑥))
2017, 19oveq12d 5842 . . . . . 6 (𝑤 = 𝑘 → ((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) = ((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)))
2120oveq1d 5839 . . . . 5 (𝑤 = 𝑘 → (((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) mod 𝑁) = (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁))
2218prodeq1d 11461 . . . . . 6 (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁))
2322oveq1d 5839 . . . . 5 (𝑤 = 𝑘 → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))
2421, 23eqeq12d 2172 . . . 4 (𝑤 = 𝑘 → ((((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)))
2524imbi2d 229 . . 3 (𝑤 = 𝑘 → ((𝜑 → (((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))))
26 oveq2 5832 . . . . . . 7 (𝑤 = (𝑘 + 1) → (𝐴𝑤) = (𝐴↑(𝑘 + 1)))
27 oveq2 5832 . . . . . . . 8 (𝑤 = (𝑘 + 1) → (1...𝑤) = (1...(𝑘 + 1)))
2827prodeq1d 11461 . . . . . . 7 (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)(𝐹𝑥) = ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥))
2926, 28oveq12d 5842 . . . . . 6 (𝑤 = (𝑘 + 1) → ((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) = ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥)))
3029oveq1d 5839 . . . . 5 (𝑤 = (𝑘 + 1) → (((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) mod 𝑁) = (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥)) mod 𝑁))
3127prodeq1d 11461 . . . . . 6 (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹𝑥)) mod 𝑁))
3231oveq1d 5839 . . . . 5 (𝑤 = (𝑘 + 1) → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))
3330, 32eqeq12d 2172 . . . 4 (𝑤 = (𝑘 + 1) → ((((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)))
3433imbi2d 229 . . 3 (𝑤 = (𝑘 + 1) → ((𝜑 → (((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))))
35 oveq2 5832 . . . . . . 7 (𝑤 = (ϕ‘𝑁) → (𝐴𝑤) = (𝐴↑(ϕ‘𝑁)))
36 oveq2 5832 . . . . . . . 8 (𝑤 = (ϕ‘𝑁) → (1...𝑤) = (1...(ϕ‘𝑁)))
3736prodeq1d 11461 . . . . . . 7 (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)(𝐹𝑥) = ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹𝑥))
3835, 37oveq12d 5842 . . . . . 6 (𝑤 = (ϕ‘𝑁) → ((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) = ((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹𝑥)))
3938oveq1d 5839 . . . . 5 (𝑤 = (ϕ‘𝑁) → (((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) mod 𝑁) = (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹𝑥)) mod 𝑁))
4036prodeq1d 11461 . . . . . 6 (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹𝑥)) mod 𝑁))
4140oveq1d 5839 . . . . 5 (𝑤 = (ϕ‘𝑁) → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))
4239, 41eqeq12d 2172 . . . 4 (𝑤 = (ϕ‘𝑁) → ((((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)))
4342imbi2d 229 . . 3 (𝑤 = (ϕ‘𝑁) → ((𝜑 → (((𝐴𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))))
441simp2d 995 . . . . . . . 8 (𝜑𝐴 ∈ ℤ)
45 eulerth.2 . . . . . . . . . . . 12 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
46 ssrab2 3213 . . . . . . . . . . . 12 {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
4745, 46eqsstri 3160 . . . . . . . . . . 11 𝑆 ⊆ (0..^𝑁)
48 fzo0ssnn0 10114 . . . . . . . . . . 11 (0..^𝑁) ⊆ ℕ0
4947, 48sstri 3137 . . . . . . . . . 10 𝑆 ⊆ ℕ0
50 nn0ssz 9185 . . . . . . . . . 10 0 ⊆ ℤ
5149, 50sstri 3137 . . . . . . . . 9 𝑆 ⊆ ℤ
52 eulerth.4 . . . . . . . . . . 11 (𝜑𝐹:(1...(ϕ‘𝑁))–1-1-onto𝑆)
53 f1of 5414 . . . . . . . . . . 11 (𝐹:(1...(ϕ‘𝑁))–1-1-onto𝑆𝐹:(1...(ϕ‘𝑁))⟶𝑆)
5452, 53syl 14 . . . . . . . . . 10 (𝜑𝐹:(1...(ϕ‘𝑁))⟶𝑆)
55 1nn 8844 . . . . . . . . . . . 12 1 ∈ ℕ
5655a1i 9 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℕ)
573nnge1d 8876 . . . . . . . . . . 11 (𝜑 → 1 ≤ (ϕ‘𝑁))
58 elfz1b 9992 . . . . . . . . . . 11 (1 ∈ (1...(ϕ‘𝑁)) ↔ (1 ∈ ℕ ∧ (ϕ‘𝑁) ∈ ℕ ∧ 1 ≤ (ϕ‘𝑁)))
5956, 3, 57, 58syl3anbrc 1166 . . . . . . . . . 10 (𝜑 → 1 ∈ (1...(ϕ‘𝑁)))
6054, 59ffvelrnd 5603 . . . . . . . . 9 (𝜑 → (𝐹‘1) ∈ 𝑆)
6151, 60sseldi 3126 . . . . . . . 8 (𝜑 → (𝐹‘1) ∈ ℤ)
6244, 61zmulcld 9292 . . . . . . 7 (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℤ)
63 zq 9535 . . . . . . 7 ((𝐴 · (𝐹‘1)) ∈ ℤ → (𝐴 · (𝐹‘1)) ∈ ℚ)
6462, 63syl 14 . . . . . 6 (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℚ)
65 nnq 9542 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
662, 65syl 14 . . . . . 6 (𝜑𝑁 ∈ ℚ)
672nngt0d 8877 . . . . . 6 (𝜑 → 0 < 𝑁)
68 modqabs2 10257 . . . . . 6 (((𝐴 · (𝐹‘1)) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
6964, 66, 67, 68syl3anc 1220 . . . . 5 (𝜑 → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
70 1z 9193 . . . . . . 7 1 ∈ ℤ
7162, 2zmodcld 10244 . . . . . . . 8 (𝜑 → ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℕ0)
7271nn0cnd 9145 . . . . . . 7 (𝜑 → ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℂ)
73 fveq2 5468 . . . . . . . . . 10 (𝑥 = 1 → (𝐹𝑥) = (𝐹‘1))
7473oveq2d 5840 . . . . . . . . 9 (𝑥 = 1 → (𝐴 · (𝐹𝑥)) = (𝐴 · (𝐹‘1)))
7574oveq1d 5839 . . . . . . . 8 (𝑥 = 1 → ((𝐴 · (𝐹𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
7675fprod1 11491 . . . . . . 7 ((1 ∈ ℤ ∧ ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℂ) → ∏𝑥 ∈ (1...1)((𝐴 · (𝐹𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
7770, 72, 76sylancr 411 . . . . . 6 (𝜑 → ∏𝑥 ∈ (1...1)((𝐴 · (𝐹𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
7877oveq1d 5839 . . . . 5 (𝜑 → (∏𝑥 ∈ (1...1)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) = (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁))
7944zcnd 9287 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
8079exp1d 10546 . . . . . . 7 (𝜑 → (𝐴↑1) = 𝐴)
81 nn0sscn 9095 . . . . . . . . . 10 0 ⊆ ℂ
8249, 81sstri 3137 . . . . . . . . 9 𝑆 ⊆ ℂ
8382, 60sseldi 3126 . . . . . . . 8 (𝜑 → (𝐹‘1) ∈ ℂ)
8473fprod1 11491 . . . . . . . 8 ((1 ∈ ℤ ∧ (𝐹‘1) ∈ ℂ) → ∏𝑥 ∈ (1...1)(𝐹𝑥) = (𝐹‘1))
8570, 83, 84sylancr 411 . . . . . . 7 (𝜑 → ∏𝑥 ∈ (1...1)(𝐹𝑥) = (𝐹‘1))
8680, 85oveq12d 5842 . . . . . 6 (𝜑 → ((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹𝑥)) = (𝐴 · (𝐹‘1)))
8786oveq1d 5839 . . . . 5 (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁))
8869, 78, 873eqtr4rd 2201 . . . 4 (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))
8988a1i 9 . . 3 ((ϕ‘𝑁) ∈ (ℤ‘1) → (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)))
9044adantr 274 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐴 ∈ ℤ)
91 elfzo1 10089 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1..^(ϕ‘𝑁)) ↔ (𝑘 ∈ ℕ ∧ (ϕ‘𝑁) ∈ ℕ ∧ 𝑘 < (ϕ‘𝑁)))
9291simp1bi 997 . . . . . . . . . . . . . 14 (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈ ℕ)
9392adantl 275 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℕ)
9493nnnn0d 9143 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℕ0)
95 zexpcl 10434 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℤ)
9690, 94, 95syl2anc 409 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴𝑘) ∈ ℤ)
9770a1i 9 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → 1 ∈ ℤ)
9893nnzd 9285 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℤ)
9997, 98fzfigd 10330 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (1...𝑘) ∈ Fin)
10054ad2antrr 480 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
101 elfzelz 9928 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℤ)
102101zred 9286 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℝ)
103102adantl 275 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ ℝ)
1043nnzd 9285 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ϕ‘𝑁) ∈ ℤ)
105104ad2antrr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℤ)
106105zred 9286 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℝ)
10793nnred 8846 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℝ)
108107adantr 274 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
109 elfzle2 9930 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑘) → 𝑥𝑘)
110109adantl 275 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥𝑘)
111 elfzolt2 10055 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 < (ϕ‘𝑁))
112111ad2antlr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 < (ϕ‘𝑁))
113103, 108, 106, 110, 112lelttrd 8000 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 < (ϕ‘𝑁))
114103, 106, 113ltled 7994 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ (ϕ‘𝑁))
115 elfzuz 9924 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...𝑘) → 𝑥 ∈ (ℤ‘1))
116 elfz5 9920 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (ℤ‘1) ∧ (ϕ‘𝑁) ∈ ℤ) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
117115, 105, 116syl2an2 584 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
118114, 117mpbird 166 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ (1...(ϕ‘𝑁)))
119100, 118ffvelrnd 5603 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹𝑥) ∈ 𝑆)
12051, 119sseldi 3126 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹𝑥) ∈ ℤ)
12199, 120fprodzcl 11506 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)(𝐹𝑥) ∈ ℤ)
12296, 121zmulcld 9292 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) ∈ ℤ)
123 zq 9535 . . . . . . . . . 10 (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) ∈ ℤ → ((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) ∈ ℚ)
124122, 123syl 14 . . . . . . . . 9 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) ∈ ℚ)
125124adantr 274 . . . . . . . 8 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → ((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) ∈ ℚ)
12690adantr 274 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝐴 ∈ ℤ)
127126, 120zmulcld 9292 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐴 · (𝐹𝑥)) ∈ ℤ)
1282ad2antrr 480 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑁 ∈ ℕ)
129127, 128zmodcld 10244 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → ((𝐴 · (𝐹𝑥)) mod 𝑁) ∈ ℕ0)
130129nn0zd 9284 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → ((𝐴 · (𝐹𝑥)) mod 𝑁) ∈ ℤ)
13199, 130fprodzcl 11506 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) ∈ ℤ)
132 zq 9535 . . . . . . . . . 10 (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) ∈ ℤ → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) ∈ ℚ)
133131, 132syl 14 . . . . . . . . 9 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) ∈ ℚ)
134133adantr 274 . . . . . . . 8 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) ∈ ℚ)
13544ad2antrr 480 . . . . . . . . 9 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → 𝐴 ∈ ℤ)
13654ad2antrr 480 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
137 fzofzp1 10126 . . . . . . . . . . . 12 (𝑘 ∈ (1..^(ϕ‘𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
138137ad2antlr 481 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
139136, 138ffvelrnd 5603 . . . . . . . . . 10 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → (𝐹‘(𝑘 + 1)) ∈ 𝑆)
14051, 139sseldi 3126 . . . . . . . . 9 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℤ)
141135, 140zmulcld 9292 . . . . . . . 8 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ)
14266ad2antrr 480 . . . . . . . 8 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → 𝑁 ∈ ℚ)
14367ad2antrr 480 . . . . . . . 8 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → 0 < 𝑁)
144 simpr 109 . . . . . . . 8 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))
145125, 134, 141, 142, 143, 144modqmul1 10276 . . . . . . 7 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → ((((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁))
146145ex 114 . . . . . 6 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) → ((((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁)))
14796zcnd 9287 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴𝑘) ∈ ℂ)
148121zcnd 9287 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)(𝐹𝑥) ∈ ℂ)
14979adantr 274 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐴 ∈ ℂ)
15054adantr 274 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
151137adantl 275 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
152150, 151ffvelrnd 5603 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ 𝑆)
15382, 152sseldi 3126 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
154147, 148, 149, 153mul4d 8030 . . . . . . . . 9 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) = (((𝐴𝑘) · 𝐴) · (∏𝑥 ∈ (1...𝑘)(𝐹𝑥) · (𝐹‘(𝑘 + 1)))))
155149, 94expp1d 10552 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑(𝑘 + 1)) = ((𝐴𝑘) · 𝐴))
156 elfzouz 10050 . . . . . . . . . . . 12 (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈ (ℤ‘1))
157156adantl 275 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ (ℤ‘1))
158150adantr 274 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆)
159 elfzelz 9928 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℤ)
160159zred 9286 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℝ)
161160adantl 275 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ ℝ)
162 peano2re 8011 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
163107, 162syl 14 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝑘 + 1) ∈ ℝ)
164163adantr 274 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ∈ ℝ)
165104ad2antrr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈ ℤ)
166165zred 9286 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈ ℝ)
167 elfzle2 9930 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ≤ (𝑘 + 1))
168167adantl 275 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (𝑘 + 1))
169137ad2antlr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁)))
170 elfzle2 9930 . . . . . . . . . . . . . . . 16 ((𝑘 + 1) ∈ (1...(ϕ‘𝑁)) → (𝑘 + 1) ≤ (ϕ‘𝑁))
171169, 170syl 14 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ≤ (ϕ‘𝑁))
172161, 164, 166, 168, 171letrd 7999 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (ϕ‘𝑁))
173 elfzuz 9924 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ (ℤ‘1))
174173, 165, 116syl2an2 584 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁)))
175172, 174mpbird 166 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ (1...(ϕ‘𝑁)))
176158, 175ffvelrnd 5603 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹𝑥) ∈ 𝑆)
17782, 176sseldi 3126 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹𝑥) ∈ ℂ)
178 fveq2 5468 . . . . . . . . . . 11 (𝑥 = (𝑘 + 1) → (𝐹𝑥) = (𝐹‘(𝑘 + 1)))
179157, 177, 178fprodp1 11497 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥) = (∏𝑥 ∈ (1...𝑘)(𝐹𝑥) · (𝐹‘(𝑘 + 1))))
180155, 179oveq12d 5842 . . . . . . . . 9 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥)) = (((𝐴𝑘) · 𝐴) · (∏𝑥 ∈ (1...𝑘)(𝐹𝑥) · (𝐹‘(𝑘 + 1)))))
181154, 180eqtr4d 2193 . . . . . . . 8 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) = ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥)))
182181oveq1d 5839 . . . . . . 7 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥)) mod 𝑁))
18351, 152sseldi 3126 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℤ)
18490, 183zmulcld 9292 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ)
1852adantr 274 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑁 ∈ ℕ)
186184, 185zmodcld 10244 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℕ0)
187186nn0zd 9284 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℤ)
188 zq 9535 . . . . . . . . . 10 (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℤ → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℚ)
189187, 188syl 14 . . . . . . . . 9 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℚ)
190 zq 9535 . . . . . . . . . 10 ((𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ)
191184, 190syl 14 . . . . . . . . 9 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ)
19266adantr 274 . . . . . . . . 9 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑁 ∈ ℚ)
19367adantr 274 . . . . . . . . 9 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → 0 < 𝑁)
194 modqabs2 10257 . . . . . . . . . 10 (((𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
195191, 192, 193, 194syl3anc 1220 . . . . . . . . 9 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
196189, 191, 131, 192, 193, 195modqmul1 10276 . . . . . . . 8 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁)) mod 𝑁))
19790adantr 274 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐴 ∈ ℤ)
19851, 176sseldi 3126 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹𝑥) ∈ ℤ)
199197, 198zmulcld 9292 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐴 · (𝐹𝑥)) ∈ ℤ)
200185adantr 274 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑁 ∈ ℕ)
201199, 200zmodcld 10244 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → ((𝐴 · (𝐹𝑥)) mod 𝑁) ∈ ℕ0)
202201nn0cnd 9145 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → ((𝐴 · (𝐹𝑥)) mod 𝑁) ∈ ℂ)
203178oveq2d 5840 . . . . . . . . . . . 12 (𝑥 = (𝑘 + 1) → (𝐴 · (𝐹𝑥)) = (𝐴 · (𝐹‘(𝑘 + 1))))
204203oveq1d 5839 . . . . . . . . . . 11 (𝑥 = (𝑘 + 1) → ((𝐴 · (𝐹𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))
205157, 202, 204fprodp1 11497 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) · ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)))
206186nn0cnd 9145 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℂ)
207131zcnd 9287 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) ∈ ℂ)
208206, 207mulcomd 7899 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁)) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) · ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)))
209205, 208eqtr4d 2193 . . . . . . . . 9 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹𝑥)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁)))
210209oveq1d 5839 . . . . . . . 8 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) = ((((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁)) mod 𝑁))
211149, 153mulcld 7898 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℂ)
212207, 211mulcomd 7899 . . . . . . . . 9 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) = ((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁)))
213212oveq1d 5839 . . . . . . . 8 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁)) mod 𝑁))
214196, 210, 2133eqtr4rd 2201 . . . . . . 7 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))
215182, 214eqeq12d 2172 . . . . . 6 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → (((((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) ↔ (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)))
216146, 215sylibd 148 . . . . 5 ((𝜑𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)))
217216expcom 115 . . . 4 (𝑘 ∈ (1..^(ϕ‘𝑁)) → (𝜑 → ((((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁) → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))))
218217a2d 26 . . 3 (𝑘 ∈ (1..^(ϕ‘𝑁)) → ((𝜑 → (((𝐴𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)) → (𝜑 → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))))
21916, 25, 34, 43, 89, 218fzind2 10138 . 2 ((ϕ‘𝑁) ∈ (1...(ϕ‘𝑁)) → (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁)))
2207, 219mpcom 36 1 (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹𝑥)) mod 𝑁) mod 𝑁))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 963   = wceq 1335  wcel 2128  {crab 2439   class class class wbr 3965  wf 5166  1-1-ontowf1o 5169  cfv 5170  (class class class)co 5824  cc 7730  cr 7731  0cc0 7732  1c1 7733   + caddc 7735   · cmul 7737   < clt 7912  cle 7913  cn 8833  0cn0 9090  cz 9167  cuz 9439  cq 9528  ...cfz 9912  ..^cfzo 10041   mod cmo 10221  cexp 10418  cprod 11447   gcd cgcd 11829  ϕcphi 12084
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4496  ax-iinf 4547  ax-cnex 7823  ax-resscn 7824  ax-1cn 7825  ax-1re 7826  ax-icn 7827  ax-addcl 7828  ax-addrcl 7829  ax-mulcl 7830  ax-mulrcl 7831  ax-addcom 7832  ax-mulcom 7833  ax-addass 7834  ax-mulass 7835  ax-distr 7836  ax-i2m1 7837  ax-0lt1 7838  ax-1rid 7839  ax-0id 7840  ax-rnegex 7841  ax-precex 7842  ax-cnre 7843  ax-pre-ltirr 7844  ax-pre-ltwlin 7845  ax-pre-lttrn 7846  ax-pre-apti 7847  ax-pre-ltadd 7848  ax-pre-mulgt0 7849  ax-pre-mulext 7850  ax-arch 7851  ax-caucvg 7852
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rmo 2443  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4253  df-po 4256  df-iso 4257  df-iord 4326  df-on 4328  df-ilim 4329  df-suc 4331  df-iom 4550  df-xp 4592  df-rel 4593  df-cnv 4594  df-co 4595  df-dm 4596  df-rn 4597  df-res 4598  df-ima 4599  df-iota 5135  df-fun 5172  df-fn 5173  df-f 5174  df-f1 5175  df-fo 5176  df-f1o 5177  df-fv 5178  df-isom 5179  df-riota 5780  df-ov 5827  df-oprab 5828  df-mpo 5829  df-1st 6088  df-2nd 6089  df-recs 6252  df-irdg 6317  df-frec 6338  df-1o 6363  df-oadd 6367  df-er 6480  df-en 6686  df-dom 6687  df-fin 6688  df-sup 6928  df-pnf 7914  df-mnf 7915  df-xr 7916  df-ltxr 7917  df-le 7918  df-sub 8048  df-neg 8049  df-reap 8450  df-ap 8457  df-div 8546  df-inn 8834  df-2 8892  df-3 8893  df-4 8894  df-n0 9091  df-z 9168  df-uz 9440  df-q 9529  df-rp 9561  df-fz 9913  df-fzo 10042  df-fl 10169  df-mod 10222  df-seqfrec 10345  df-exp 10419  df-ihash 10650  df-cj 10742  df-re 10743  df-im 10744  df-rsqrt 10898  df-abs 10899  df-clim 11176  df-proddc 11448  df-dvds 11684  df-gcd 11830  df-phi 12086
This theorem is referenced by:  eulerthlemth  12107
  Copyright terms: Public domain W3C validator