lgsval4a - Metamath Proof Explorer

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

Theorem lgsval4a 26789

Description: Same as lgsval4 26787 for positive 𝑁. (Contributed by Mario Carneiro, 4-Feb-2015.)

**Hypothesis**
Ref	Expression
lgsval4.1	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))

**Assertion**
Ref	Expression
lgsval4a	⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /_L 𝑁) = (seq1( · , 𝐹)‘𝑁))

Distinct variable groups: 𝐴,𝑛 𝑛,𝑁 Allowed substitution hint: 𝐹(𝑛)

Proof of Theorem lgsval4a Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 484	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐴 ∈ ℤ)
2		nnz 12566	. . . 4 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
3	2	adantl 483	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℤ)
4		nnne0 12233	. . . 4 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
5	4	adantl 483	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0)
6		lgsval4.1	. . . 4 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
7	6	lgsval4 26787	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))))
8	1, 3, 5, 7	syl3anc 1372	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))))
9		nngt0 12230	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
10	9	adantl 483	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 < 𝑁)
11		0re 11203	. . . . . . 7 ⊢ 0 ∈ ℝ
12		nnre 12206	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
13	12	adantl 483	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ)
14		ltnsym 11299	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 < 𝑁 → ¬ 𝑁 < 0))
15	11, 13, 14	sylancr 588	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (0 < 𝑁 → ¬ 𝑁 < 0))
16	10, 15	mpd 15	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ¬ 𝑁 < 0)
17	16	intnanrd 491	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ¬ (𝑁 < 0 ∧ 𝐴 < 0))
18	17	iffalsed 4535	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = 1)
19		nnnn0 12466	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
20	19	adantl 483	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ₀)
21	20	nn0ge0d 12522	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 ≤ 𝑁)
22	13, 21	absidd 15356	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (abs‘𝑁) = 𝑁)
23	22	fveq2d 6885	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (seq1( · , 𝐹)‘(abs‘𝑁)) = (seq1( · , 𝐹)‘𝑁))
24	18, 23	oveq12d 7414	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))) = (1 · (seq1( · , 𝐹)‘𝑁)))
25		simpr 486	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ)
26		nnuz 12852	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
27	25, 26	eleqtrdi 2844	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (ℤ_≥‘1))
28	6	lgsfcl3 26788	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹:ℕ⟶ℤ)
29	1, 3, 5, 28	syl3anc 1372	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐹:ℕ⟶ℤ)
30		elfznn 13517	. . . . . 6 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
31		ffvelcdm 7071	. . . . . 6 ⊢ ((𝐹:ℕ⟶ℤ ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ ℤ)
32	29, 30, 31	syl2an 597	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (1...𝑁)) → (𝐹‘𝑥) ∈ ℤ)
33		zmulcl 12598	. . . . . 6 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ)
34	33	adantl 483	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ)
35	27, 32, 34	seqcl 13975	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (seq1( · , 𝐹)‘𝑁) ∈ ℤ)
36	35	zcnd 12654	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (seq1( · , 𝐹)‘𝑁) ∈ ℂ)
37	36	mullidd 11219	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (1 · (seq1( · , 𝐹)‘𝑁)) = (seq1( · , 𝐹)‘𝑁))
38	8, 24, 37	3eqtrd 2777	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /_L 𝑁) = (seq1( · , 𝐹)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 ifcif 4524 class class class wbr 5144 ↦ cmpt 5227 ⟶wf 6531 ‘cfv 6535 (class class class)co 7396 ℝcr 11096 0cc0 11097 1c1 11098 · cmul 11102 < clt 11235 -cneg 11432 ℕcn 12199 ℕ₀cn0 12459 ℤcz 12545 ℤ_≥cuz 12809 ...cfz 13471 seqcseq 13953 ↑cexp 14014 abscabs 15168 ℙcprime 16595 pCnt cpc 16756 /_L clgs 26764

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5281 ax-sep 5295 ax-nul 5302 ax-pow 5359 ax-pr 5423 ax-un 7712 ax-cnex 11153 ax-resscn 11154 ax-1cn 11155 ax-icn 11156 ax-addcl 11157 ax-addrcl 11158 ax-mulcl 11159 ax-mulrcl 11160 ax-mulcom 11161 ax-addass 11162 ax-mulass 11163 ax-distr 11164 ax-i2m1 11165 ax-1ne0 11166 ax-1rid 11167 ax-rnegex 11168 ax-rrecex 11169 ax-cnre 11170 ax-pre-lttri 11171 ax-pre-lttrn 11172 ax-pre-ltadd 11173 ax-pre-mulgt0 11174 ax-pre-sup 11175

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-pss 3965 df-nul 4321 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4905 df-int 4947 df-iun 4995 df-br 5145 df-opab 5207 df-mpt 5228 df-tr 5262 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6292 df-ord 6359 df-on 6360 df-lim 6361 df-suc 6362 df-iota 6487 df-fun 6537 df-fn 6538 df-f 6539 df-f1 6540 df-fo 6541 df-f1o 6542 df-fv 6543 df-riota 7352 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7843 df-1st 7962 df-2nd 7963 df-frecs 8253 df-wrecs 8284 df-recs 8358 df-rdg 8397 df-1o 8453 df-2o 8454 df-oadd 8457 df-er 8691 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-sup 9424 df-inf 9425 df-dju 9883 df-card 9921 df-pnf 11237 df-mnf 11238 df-xr 11239 df-ltxr 11240 df-le 11241 df-sub 11433 df-neg 11434 df-div 11859 df-nn 12200 df-2 12262 df-3 12263 df-n0 12460 df-xnn0 12532 df-z 12546 df-uz 12810 df-q 12920 df-rp 12962 df-fz 13472 df-fzo 13615 df-fl 13744 df-mod 13822 df-seq 13954 df-exp 14015 df-hash 14278 df-cj 15033 df-re 15034 df-im 15035 df-sqrt 15169 df-abs 15170 df-dvds 16185 df-gcd 16423 df-prm 16596 df-phi 16686 df-pc 16757 df-lgs 26765

This theorem is referenced by: lgsmod 26793

W3C validator