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

Theorem plyeq0lem 25587
Description: Lemma for plyeq0 25588. If 𝐴 is the coefficient function for a nonzero polynomial such that 𝑃(𝑧) = Ξ£π‘˜ ∈ β„•0𝐴(π‘˜) Β· π‘§β†‘π‘˜ = 0 for every 𝑧 ∈ β„‚ and 𝐴(𝑀) is the nonzero leading coefficient, then the function 𝐹(𝑧) = 𝑃(𝑧) / 𝑧↑𝑀 is a sum of powers of 1 / 𝑧, and so the limit of this function as 𝑧 ⇝ +∞ is the constant term, 𝐴(𝑀). But 𝐹(𝑧) = 0 everywhere, so this limit is also equal to zero so that 𝐴(𝑀) = 0, a contradiction. (Contributed by Mario Carneiro, 22-Jul-2014.)
Hypotheses
Ref Expression
plyeq0.1 (πœ‘ β†’ 𝑆 βŠ† β„‚)
plyeq0.2 (πœ‘ β†’ 𝑁 ∈ β„•0)
plyeq0.3 (πœ‘ β†’ 𝐴 ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))
plyeq0.4 (πœ‘ β†’ (𝐴 β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
plyeq0.5 (πœ‘ β†’ 0𝑝 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
plyeq0.6 𝑀 = sup((◑𝐴 β€œ (𝑆 βˆ– {0})), ℝ, < )
plyeq0.7 (πœ‘ β†’ (◑𝐴 β€œ (𝑆 βˆ– {0})) β‰  βˆ…)
Assertion
Ref Expression
plyeq0lem Β¬ πœ‘
Distinct variable groups:   𝑧,π‘˜,𝐴   π‘˜,𝑀   π‘˜,𝑁,𝑧   πœ‘,π‘˜,𝑧   𝑆,π‘˜,𝑧
Allowed substitution hint:   𝑀(𝑧)

Proof of Theorem plyeq0lem
Dummy variables π‘š 𝑛 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 12813 . . . . . 6 β„• = (β„€β‰₯β€˜1)
2 1zzd 12541 . . . . . 6 (πœ‘ β†’ 1 ∈ β„€)
3 fzfid 13885 . . . . . 6 (πœ‘ β†’ (0...𝑁) ∈ Fin)
4 1zzd 12541 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ 1 ∈ β„€)
5 plyeq0.3 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐴 ∈ ((𝑆 βˆͺ {0}) ↑m β„•0))
6 plyeq0.1 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑆 βŠ† β„‚)
7 0cn 11154 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ β„‚
87a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 0 ∈ β„‚)
98snssd 4774 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ {0} βŠ† β„‚)
106, 9unssd 4151 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑆 βˆͺ {0}) βŠ† β„‚)
11 cnex 11139 . . . . . . . . . . . . . . . . . . 19 β„‚ ∈ V
12 ssexg 5285 . . . . . . . . . . . . . . . . . . 19 (((𝑆 βˆͺ {0}) βŠ† β„‚ ∧ β„‚ ∈ V) β†’ (𝑆 βˆͺ {0}) ∈ V)
1310, 11, 12sylancl 587 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑆 βˆͺ {0}) ∈ V)
14 nn0ex 12426 . . . . . . . . . . . . . . . . . 18 β„•0 ∈ V
15 elmapg 8785 . . . . . . . . . . . . . . . . . 18 (((𝑆 βˆͺ {0}) ∈ V ∧ β„•0 ∈ V) β†’ (𝐴 ∈ ((𝑆 βˆͺ {0}) ↑m β„•0) ↔ 𝐴:β„•0⟢(𝑆 βˆͺ {0})))
1613, 14, 15sylancl 587 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐴 ∈ ((𝑆 βˆͺ {0}) ↑m β„•0) ↔ 𝐴:β„•0⟢(𝑆 βˆͺ {0})))
175, 16mpbid 231 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐴:β„•0⟢(𝑆 βˆͺ {0}))
1817, 10fssd 6691 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐴:β„•0βŸΆβ„‚)
19 elfznn0 13541 . . . . . . . . . . . . . . 15 (π‘˜ ∈ (0...𝑁) β†’ π‘˜ ∈ β„•0)
20 ffvelcdm 7037 . . . . . . . . . . . . . . 15 ((𝐴:β„•0βŸΆβ„‚ ∧ π‘˜ ∈ β„•0) β†’ (π΄β€˜π‘˜) ∈ β„‚)
2118, 19, 20syl2an 597 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (π΄β€˜π‘˜) ∈ β„‚)
2221adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ (π΄β€˜π‘˜) ∈ β„‚)
2322abscld 15328 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ (absβ€˜(π΄β€˜π‘˜)) ∈ ℝ)
2423recnd 11190 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ (absβ€˜(π΄β€˜π‘˜)) ∈ β„‚)
25 divcnv 15745 . . . . . . . . . . 11 ((absβ€˜(π΄β€˜π‘˜)) ∈ β„‚ β†’ (𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) / 𝑛)) ⇝ 0)
2624, 25syl 17 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ (𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) / 𝑛)) ⇝ 0)
27 nnex 12166 . . . . . . . . . . . 12 β„• ∈ V
2827mptex 7178 . . . . . . . . . . 11 (𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) ∈ V
2928a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ (𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) ∈ V)
30 oveq2 7370 . . . . . . . . . . . . 13 (𝑛 = π‘š β†’ ((absβ€˜(π΄β€˜π‘˜)) / 𝑛) = ((absβ€˜(π΄β€˜π‘˜)) / π‘š))
31 eqid 2737 . . . . . . . . . . . . 13 (𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) / 𝑛)) = (𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) / 𝑛))
32 ovex 7395 . . . . . . . . . . . . 13 ((absβ€˜(π΄β€˜π‘˜)) / π‘š) ∈ V
3330, 31, 32fvmpt 6953 . . . . . . . . . . . 12 (π‘š ∈ β„• β†’ ((𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) / 𝑛))β€˜π‘š) = ((absβ€˜(π΄β€˜π‘˜)) / π‘š))
3433adantl 483 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) / 𝑛))β€˜π‘š) = ((absβ€˜(π΄β€˜π‘˜)) / π‘š))
35 nndivre 12201 . . . . . . . . . . . 12 (((absβ€˜(π΄β€˜π‘˜)) ∈ ℝ ∧ π‘š ∈ β„•) β†’ ((absβ€˜(π΄β€˜π‘˜)) / π‘š) ∈ ℝ)
3623, 35sylan 581 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((absβ€˜(π΄β€˜π‘˜)) / π‘š) ∈ ℝ)
3734, 36eqeltrd 2838 . . . . . . . . . 10 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) / 𝑛))β€˜π‘š) ∈ ℝ)
38 oveq1 7369 . . . . . . . . . . . . . 14 (𝑛 = π‘š β†’ (𝑛↑(π‘˜ βˆ’ 𝑀)) = (π‘šβ†‘(π‘˜ βˆ’ 𝑀)))
3938oveq2d 7378 . . . . . . . . . . . . 13 (𝑛 = π‘š β†’ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))) = ((absβ€˜(π΄β€˜π‘˜)) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))))
40 eqid 2737 . . . . . . . . . . . . 13 (𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) = (𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))
41 ovex 7395 . . . . . . . . . . . . 13 ((absβ€˜(π΄β€˜π‘˜)) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))) ∈ V
4239, 40, 41fvmpt 6953 . . . . . . . . . . . 12 (π‘š ∈ β„• β†’ ((𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) = ((absβ€˜(π΄β€˜π‘˜)) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))))
4342adantl 483 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) = ((absβ€˜(π΄β€˜π‘˜)) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))))
4421ad2antrr 725 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (π΄β€˜π‘˜) ∈ β„‚)
4544abscld 15328 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (absβ€˜(π΄β€˜π‘˜)) ∈ ℝ)
46 nnrp 12933 . . . . . . . . . . . . . . 15 (π‘š ∈ β„• β†’ π‘š ∈ ℝ+)
4746adantl 483 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ π‘š ∈ ℝ+)
48 elfzelz 13448 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ (0...𝑁) β†’ π‘˜ ∈ β„€)
49 cnvimass 6038 . . . . . . . . . . . . . . . . . . 19 (◑𝐴 β€œ (𝑆 βˆ– {0})) βŠ† dom 𝐴
5049, 17fssdm 6693 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (◑𝐴 β€œ (𝑆 βˆ– {0})) βŠ† β„•0)
51 plyeq0.6 . . . . . . . . . . . . . . . . . . 19 𝑀 = sup((◑𝐴 β€œ (𝑆 βˆ– {0})), ℝ, < )
52 nn0ssz 12529 . . . . . . . . . . . . . . . . . . . . 21 β„•0 βŠ† β„€
5350, 52sstrdi 3961 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (◑𝐴 β€œ (𝑆 βˆ– {0})) βŠ† β„€)
54 plyeq0.7 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (◑𝐴 β€œ (𝑆 βˆ– {0})) β‰  βˆ…)
55 plyeq0.2 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝑁 ∈ β„•0)
5655nn0red 12481 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑁 ∈ ℝ)
5717ffnd 6674 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝐴 Fn β„•0)
58 elpreima 7013 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 Fn β„•0 β†’ (𝑧 ∈ (◑𝐴 β€œ (𝑆 βˆ– {0})) ↔ (𝑧 ∈ β„•0 ∧ (π΄β€˜π‘§) ∈ (𝑆 βˆ– {0}))))
5957, 58syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝑧 ∈ (◑𝐴 β€œ (𝑆 βˆ– {0})) ↔ (𝑧 ∈ β„•0 ∧ (π΄β€˜π‘§) ∈ (𝑆 βˆ– {0}))))
6059simplbda 501 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑧 ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))) β†’ (π΄β€˜π‘§) ∈ (𝑆 βˆ– {0}))
61 eldifsni 4755 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π΄β€˜π‘§) ∈ (𝑆 βˆ– {0}) β†’ (π΄β€˜π‘§) β‰  0)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑧 ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))) β†’ (π΄β€˜π‘§) β‰  0)
63 fveq2 6847 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ = 𝑧 β†’ (π΄β€˜π‘˜) = (π΄β€˜π‘§))
6463neeq1d 3004 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ = 𝑧 β†’ ((π΄β€˜π‘˜) β‰  0 ↔ (π΄β€˜π‘§) β‰  0))
65 breq1 5113 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ = 𝑧 β†’ (π‘˜ ≀ 𝑁 ↔ 𝑧 ≀ 𝑁))
6664, 65imbi12d 345 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = 𝑧 β†’ (((π΄β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ 𝑁) ↔ ((π΄β€˜π‘§) β‰  0 β†’ 𝑧 ≀ 𝑁)))
67 plyeq0.4 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝐴 β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0})
68 plyco0 25569 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ β„•0 ∧ 𝐴:β„•0βŸΆβ„‚) β†’ ((𝐴 β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0} ↔ βˆ€π‘˜ ∈ β„•0 ((π΄β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ 𝑁)))
6955, 18, 68syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ ((𝐴 β€œ (β„€β‰₯β€˜(𝑁 + 1))) = {0} ↔ βˆ€π‘˜ ∈ β„•0 ((π΄β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ 𝑁)))
7067, 69mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ βˆ€π‘˜ ∈ β„•0 ((π΄β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ 𝑁))
7170adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑧 ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))) β†’ βˆ€π‘˜ ∈ β„•0 ((π΄β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ 𝑁))
7250sselda 3949 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑧 ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))) β†’ 𝑧 ∈ β„•0)
7366, 71, 72rspcdva 3585 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑧 ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))) β†’ ((π΄β€˜π‘§) β‰  0 β†’ 𝑧 ≀ 𝑁))
7462, 73mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑧 ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))) β†’ 𝑧 ≀ 𝑁)
7574ralrimiva 3144 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ βˆ€π‘§ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))𝑧 ≀ 𝑁)
76 brralrspcev 5170 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℝ ∧ βˆ€π‘§ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))𝑧 ≀ 𝑁) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))𝑧 ≀ π‘₯)
7756, 75, 76syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))𝑧 ≀ π‘₯)
78 suprzcl 12590 . . . . . . . . . . . . . . . . . . . 20 (((◑𝐴 β€œ (𝑆 βˆ– {0})) βŠ† β„€ ∧ (◑𝐴 β€œ (𝑆 βˆ– {0})) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))𝑧 ≀ π‘₯) β†’ sup((◑𝐴 β€œ (𝑆 βˆ– {0})), ℝ, < ) ∈ (◑𝐴 β€œ (𝑆 βˆ– {0})))
7953, 54, 77, 78syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ sup((◑𝐴 β€œ (𝑆 βˆ– {0})), ℝ, < ) ∈ (◑𝐴 β€œ (𝑆 βˆ– {0})))
8051, 79eqeltrid 2842 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑀 ∈ (◑𝐴 β€œ (𝑆 βˆ– {0})))
8150, 80sseldd 3950 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑀 ∈ β„•0)
8281nn0zd 12532 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑀 ∈ β„€)
83 zsubcl 12552 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ β„€ ∧ 𝑀 ∈ β„€) β†’ (π‘˜ βˆ’ 𝑀) ∈ β„€)
8448, 82, 83syl2anr 598 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘˜ βˆ’ 𝑀) ∈ β„€)
8584ad2antrr 725 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (π‘˜ βˆ’ 𝑀) ∈ β„€)
8647, 85rpexpcld 14157 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (π‘šβ†‘(π‘˜ βˆ’ 𝑀)) ∈ ℝ+)
8786rpred 12964 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (π‘šβ†‘(π‘˜ βˆ’ 𝑀)) ∈ ℝ)
8845, 87remulcld 11192 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((absβ€˜(π΄β€˜π‘˜)) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))) ∈ ℝ)
8943, 88eqeltrd 2838 . . . . . . . . . 10 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) ∈ ℝ)
90 nnrecre 12202 . . . . . . . . . . . . 13 (π‘š ∈ β„• β†’ (1 / π‘š) ∈ ℝ)
9190adantl 483 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (1 / π‘š) ∈ ℝ)
9222absge0d 15336 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ 0 ≀ (absβ€˜(π΄β€˜π‘˜)))
9392adantr 482 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ 0 ≀ (absβ€˜(π΄β€˜π‘˜)))
94 nnre 12167 . . . . . . . . . . . . . . 15 (π‘š ∈ β„• β†’ π‘š ∈ ℝ)
9594adantl 483 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ π‘š ∈ ℝ)
96 nnge1 12188 . . . . . . . . . . . . . . 15 (π‘š ∈ β„• β†’ 1 ≀ π‘š)
9796adantl 483 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ 1 ≀ π‘š)
98 1red 11163 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ 1 ∈ ℝ)
9985zred 12614 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (π‘˜ βˆ’ 𝑀) ∈ ℝ)
100 simplr 768 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ π‘˜ < 𝑀)
10148adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ π‘˜ ∈ β„€)
102101ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ π‘˜ ∈ β„€)
10382ad3antrrr 729 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ 𝑀 ∈ β„€)
104 zltp1le 12560 . . . . . . . . . . . . . . . . . . . 20 ((π‘˜ ∈ β„€ ∧ 𝑀 ∈ β„€) β†’ (π‘˜ < 𝑀 ↔ (π‘˜ + 1) ≀ 𝑀))
105102, 103, 104syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (π‘˜ < 𝑀 ↔ (π‘˜ + 1) ≀ 𝑀))
106100, 105mpbid 231 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (π‘˜ + 1) ≀ 𝑀)
10719adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ π‘˜ ∈ β„•0)
108107nn0red 12481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ π‘˜ ∈ ℝ)
109108ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ π‘˜ ∈ ℝ)
11081adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝑀 ∈ β„•0)
111110nn0red 12481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝑀 ∈ ℝ)
112111ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ 𝑀 ∈ ℝ)
113109, 98, 112leaddsub2d 11764 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((π‘˜ + 1) ≀ 𝑀 ↔ 1 ≀ (𝑀 βˆ’ π‘˜)))
114106, 113mpbid 231 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ 1 ≀ (𝑀 βˆ’ π‘˜))
115108recnd 11190 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ π‘˜ ∈ β„‚)
116115ad2antrr 725 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ π‘˜ ∈ β„‚)
117111recnd 11190 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝑀 ∈ β„‚)
118117ad2antrr 725 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ 𝑀 ∈ β„‚)
119116, 118negsubdi2d 11535 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ -(π‘˜ βˆ’ 𝑀) = (𝑀 βˆ’ π‘˜))
120114, 119breqtrrd 5138 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ 1 ≀ -(π‘˜ βˆ’ 𝑀))
12198, 99, 120lenegcon2d 11745 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (π‘˜ βˆ’ 𝑀) ≀ -1)
122 neg1z 12546 . . . . . . . . . . . . . . . 16 -1 ∈ β„€
123 eluz 12784 . . . . . . . . . . . . . . . 16 (((π‘˜ βˆ’ 𝑀) ∈ β„€ ∧ -1 ∈ β„€) β†’ (-1 ∈ (β„€β‰₯β€˜(π‘˜ βˆ’ 𝑀)) ↔ (π‘˜ βˆ’ 𝑀) ≀ -1))
12485, 122, 123sylancl 587 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (-1 ∈ (β„€β‰₯β€˜(π‘˜ βˆ’ 𝑀)) ↔ (π‘˜ βˆ’ 𝑀) ≀ -1))
125121, 124mpbird 257 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ -1 ∈ (β„€β‰₯β€˜(π‘˜ βˆ’ 𝑀)))
12695, 97, 125leexp2ad 14164 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (π‘šβ†‘(π‘˜ βˆ’ 𝑀)) ≀ (π‘šβ†‘-1))
127 nncn 12168 . . . . . . . . . . . . . . 15 (π‘š ∈ β„• β†’ π‘š ∈ β„‚)
128127adantl 483 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ π‘š ∈ β„‚)
129 expn1 13984 . . . . . . . . . . . . . 14 (π‘š ∈ β„‚ β†’ (π‘šβ†‘-1) = (1 / π‘š))
130128, 129syl 17 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (π‘šβ†‘-1) = (1 / π‘š))
131126, 130breqtrd 5136 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (π‘šβ†‘(π‘˜ βˆ’ 𝑀)) ≀ (1 / π‘š))
13287, 91, 45, 93, 131lemul2ad 12102 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((absβ€˜(π΄β€˜π‘˜)) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))) ≀ ((absβ€˜(π΄β€˜π‘˜)) Β· (1 / π‘š)))
13324adantr 482 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (absβ€˜(π΄β€˜π‘˜)) ∈ β„‚)
134 nnne0 12194 . . . . . . . . . . . . . 14 (π‘š ∈ β„• β†’ π‘š β‰  0)
135134adantl 483 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ π‘š β‰  0)
136133, 128, 135divrecd 11941 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((absβ€˜(π΄β€˜π‘˜)) / π‘š) = ((absβ€˜(π΄β€˜π‘˜)) Β· (1 / π‘š)))
13734, 136eqtrd 2777 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) / 𝑛))β€˜π‘š) = ((absβ€˜(π΄β€˜π‘˜)) Β· (1 / π‘š)))
138132, 43, 1373brtr4d 5142 . . . . . . . . . 10 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) ≀ ((𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) / 𝑛))β€˜π‘š))
13986rpge0d 12968 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ 0 ≀ (π‘šβ†‘(π‘˜ βˆ’ 𝑀)))
14045, 87, 93, 139mulge0d 11739 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ 0 ≀ ((absβ€˜(π΄β€˜π‘˜)) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))))
141140, 43breqtrrd 5138 . . . . . . . . . 10 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ 0 ≀ ((𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š))
1421, 4, 26, 29, 37, 89, 138, 141climsqz2 15531 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ (𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) ⇝ 0)
14327mptex 7178 . . . . . . . . . . 11 (𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) ∈ V
144143a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ (𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) ∈ V)
14538oveq2d 7378 . . . . . . . . . . . . . . 15 (𝑛 = π‘š β†’ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))) = ((π΄β€˜π‘˜) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))))
146 eqid 2737 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) = (𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))
147 ovex 7395 . . . . . . . . . . . . . . 15 ((π΄β€˜π‘˜) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))) ∈ V
148145, 146, 147fvmpt 6953 . . . . . . . . . . . . . 14 (π‘š ∈ β„• β†’ ((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) = ((π΄β€˜π‘˜) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))))
149148ad2antlr 726 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) = ((π΄β€˜π‘˜) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))))
15018adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 𝐴:β„•0βŸΆβ„‚)
151150, 19, 20syl2an 597 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π΄β€˜π‘˜) ∈ β„‚)
152127ad2antlr 726 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ π‘š ∈ β„‚)
153134ad2antlr 726 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ π‘š β‰  0)
15482adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 𝑀 ∈ β„€)
15548, 154, 83syl2anr 598 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘˜ βˆ’ 𝑀) ∈ β„€)
156152, 153, 155expclzd 14063 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘šβ†‘(π‘˜ βˆ’ 𝑀)) ∈ β„‚)
157151, 156mulcld 11182 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π΄β€˜π‘˜) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))) ∈ β„‚)
158149, 157eqeltrd 2838 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) ∈ β„‚)
159158an32s 651 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘š ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) ∈ β„‚)
160159adantlr 714 . . . . . . . . . 10 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) ∈ β„‚)
16187recnd 11190 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (π‘šβ†‘(π‘˜ βˆ’ 𝑀)) ∈ β„‚)
16244, 161absmuld 15346 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (absβ€˜((π΄β€˜π‘˜) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀)))) = ((absβ€˜(π΄β€˜π‘˜)) Β· (absβ€˜(π‘šβ†‘(π‘˜ βˆ’ 𝑀)))))
16387, 139absidd 15314 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (absβ€˜(π‘šβ†‘(π‘˜ βˆ’ 𝑀))) = (π‘šβ†‘(π‘˜ βˆ’ 𝑀)))
164163oveq2d 7378 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((absβ€˜(π΄β€˜π‘˜)) Β· (absβ€˜(π‘šβ†‘(π‘˜ βˆ’ 𝑀)))) = ((absβ€˜(π΄β€˜π‘˜)) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))))
165162, 164eqtrd 2777 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (absβ€˜((π΄β€˜π‘˜) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀)))) = ((absβ€˜(π΄β€˜π‘˜)) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))))
166148adantl 483 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) = ((π΄β€˜π‘˜) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))))
167166fveq2d 6851 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ (absβ€˜((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š)) = (absβ€˜((π΄β€˜π‘˜) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀)))))
168165, 167, 433eqtr4rd 2788 . . . . . . . . . 10 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) ∧ π‘š ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) = (absβ€˜((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š)))
1691, 4, 144, 29, 160, 168climabs0 15474 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ ((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) ⇝ 0 ↔ (𝑛 ∈ β„• ↦ ((absβ€˜(π΄β€˜π‘˜)) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) ⇝ 0))
170142, 169mpbird 257 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ (𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) ⇝ 0)
171108adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ π‘˜ ∈ ℝ)
172 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ π‘˜ < 𝑀)
173171, 172ltned 11298 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ π‘˜ β‰  𝑀)
174 velsn 4607 . . . . . . . . . . 11 (π‘˜ ∈ {𝑀} ↔ π‘˜ = 𝑀)
175174necon3bbii 2992 . . . . . . . . . 10 (Β¬ π‘˜ ∈ {𝑀} ↔ π‘˜ β‰  𝑀)
176173, 175sylibr 233 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ Β¬ π‘˜ ∈ {𝑀})
177176iffalsed 4502 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0) = 0)
178170, 177breqtrrd 5138 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ π‘˜ < 𝑀) β†’ (𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) ⇝ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0))
179 nncn 12168 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„• β†’ 𝑛 ∈ β„‚)
180179ad2antlr 726 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) = 0) β†’ 𝑛 ∈ β„‚)
181 nnne0 12194 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„• β†’ 𝑛 β‰  0)
182181ad2antlr 726 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) = 0) β†’ 𝑛 β‰  0)
18384ad3antrrr 729 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) = 0) β†’ (π‘˜ βˆ’ 𝑀) ∈ β„€)
184180, 182, 183expclzd 14063 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) = 0) β†’ (𝑛↑(π‘˜ βˆ’ 𝑀)) ∈ β„‚)
185184mul02d 11360 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) = 0) β†’ (0 Β· (𝑛↑(π‘˜ βˆ’ 𝑀))) = 0)
186 simpr 486 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) = 0) β†’ (π΄β€˜π‘˜) = 0)
187186oveq1d 7377 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) = 0) β†’ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))) = (0 Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))
188186ifeq1d 4510 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) = 0) β†’ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0) = if(π‘˜ ∈ {𝑀}, 0, 0))
189 ifid 4531 . . . . . . . . . . . . 13 if(π‘˜ ∈ {𝑀}, 0, 0) = 0
190188, 189eqtrdi 2793 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) = 0) β†’ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0) = 0)
191185, 187, 1903eqtr4d 2787 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) = 0) β†’ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))) = if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0))
19221adantr 482 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) β†’ (π΄β€˜π‘˜) ∈ β„‚)
193192ad2antrr 725 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (π΄β€˜π‘˜) ∈ β„‚)
194193mulid1d 11179 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ ((π΄β€˜π‘˜) Β· 1) = (π΄β€˜π‘˜))
195 nn0ssre 12424 . . . . . . . . . . . . . . . . . . . . . . 23 β„•0 βŠ† ℝ
19650, 195sstrdi 3961 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (◑𝐴 β€œ (𝑆 βˆ– {0})) βŠ† ℝ)
197196ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (◑𝐴 β€œ (𝑆 βˆ– {0})) βŠ† ℝ)
19854ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (◑𝐴 β€œ (𝑆 βˆ– {0})) β‰  βˆ…)
19977ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ (π΄β€˜π‘˜) β‰  0) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))𝑧 ≀ π‘₯)
20019ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ (π΄β€˜π‘˜) β‰  0) β†’ π‘˜ ∈ β„•0)
201 ffvelcdm 7037 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴:β„•0⟢(𝑆 βˆͺ {0}) ∧ π‘˜ ∈ β„•0) β†’ (π΄β€˜π‘˜) ∈ (𝑆 βˆͺ {0}))
20217, 19, 201syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (π΄β€˜π‘˜) ∈ (𝑆 βˆͺ {0}))
203202anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ (π΄β€˜π‘˜) β‰  0) β†’ ((π΄β€˜π‘˜) ∈ (𝑆 βˆͺ {0}) ∧ (π΄β€˜π‘˜) β‰  0))
204 eldifsn 4752 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π΄β€˜π‘˜) ∈ ((𝑆 βˆͺ {0}) βˆ– {0}) ↔ ((π΄β€˜π‘˜) ∈ (𝑆 βˆͺ {0}) ∧ (π΄β€˜π‘˜) β‰  0))
205203, 204sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (π΄β€˜π‘˜) ∈ ((𝑆 βˆͺ {0}) βˆ– {0}))
206 difun2 4445 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 βˆͺ {0}) βˆ– {0}) = (𝑆 βˆ– {0})
207205, 206eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (π΄β€˜π‘˜) ∈ (𝑆 βˆ– {0}))
208 elpreima 7013 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 Fn β„•0 β†’ (π‘˜ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0})) ↔ (π‘˜ ∈ β„•0 ∧ (π΄β€˜π‘˜) ∈ (𝑆 βˆ– {0}))))
20957, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (π‘˜ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0})) ↔ (π‘˜ ∈ β„•0 ∧ (π΄β€˜π‘˜) ∈ (𝑆 βˆ– {0}))))
210209ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (π‘˜ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0})) ↔ (π‘˜ ∈ β„•0 ∧ (π΄β€˜π‘˜) ∈ (𝑆 βˆ– {0}))))
211200, 207, 210mpbir2and 712 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ (π΄β€˜π‘˜) β‰  0) β†’ π‘˜ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0})))
212197, 198, 199, 211suprubd 12124 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ (π΄β€˜π‘˜) β‰  0) β†’ π‘˜ ≀ sup((◑𝐴 β€œ (𝑆 βˆ– {0})), ℝ, < ))
213212, 51breqtrrdi 5152 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ (π΄β€˜π‘˜) β‰  0) β†’ π‘˜ ≀ 𝑀)
214213ad4ant14 751 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ π‘˜ ≀ 𝑀)
215 simpllr 775 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ 𝑀 ≀ π‘˜)
216108ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ π‘˜ ∈ ℝ)
217111ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ 𝑀 ∈ ℝ)
218216, 217letri3d 11304 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (π‘˜ = 𝑀 ↔ (π‘˜ ≀ 𝑀 ∧ 𝑀 ≀ π‘˜)))
219214, 215, 218mpbir2and 712 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ π‘˜ = 𝑀)
220219oveq1d 7377 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (π‘˜ βˆ’ 𝑀) = (𝑀 βˆ’ 𝑀))
221117ad3antrrr 729 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ 𝑀 ∈ β„‚)
222221subidd 11507 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (𝑀 βˆ’ 𝑀) = 0)
223220, 222eqtrd 2777 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (π‘˜ βˆ’ 𝑀) = 0)
224223oveq2d 7378 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (𝑛↑(π‘˜ βˆ’ 𝑀)) = (𝑛↑0))
225179ad2antlr 726 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ 𝑛 ∈ β„‚)
226225exp0d 14052 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (𝑛↑0) = 1)
227224, 226eqtrd 2777 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ (𝑛↑(π‘˜ βˆ’ 𝑀)) = 1)
228227oveq2d 7378 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))) = ((π΄β€˜π‘˜) Β· 1))
229219, 174sylibr 233 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ π‘˜ ∈ {𝑀})
230229iftrued 4499 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0) = (π΄β€˜π‘˜))
231194, 228, 2303eqtr4d 2787 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) ∧ (π΄β€˜π‘˜) β‰  0) β†’ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))) = if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0))
232191, 231pm2.61dane 3033 . . . . . . . . . 10 ((((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) ∧ 𝑛 ∈ β„•) β†’ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))) = if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0))
233232mpteq2dva 5210 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) β†’ (𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) = (𝑛 ∈ β„• ↦ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0)))
234 fconstmpt 5699 . . . . . . . . 9 (β„• Γ— {if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0)}) = (𝑛 ∈ β„• ↦ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0))
235233, 234eqtr4di 2795 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) β†’ (𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) = (β„• Γ— {if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0)}))
236 ifcl 4536 . . . . . . . . . 10 (((π΄β€˜π‘˜) ∈ β„‚ ∧ 0 ∈ β„‚) β†’ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0) ∈ β„‚)
237192, 7, 236sylancl 587 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) β†’ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0) ∈ β„‚)
238 1z 12540 . . . . . . . . 9 1 ∈ β„€
2391eqimss2i 4008 . . . . . . . . . 10 (β„€β‰₯β€˜1) βŠ† β„•
240239, 27climconst2 15437 . . . . . . . . 9 ((if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0) ∈ β„‚ ∧ 1 ∈ β„€) β†’ (β„• Γ— {if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0)}) ⇝ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0))
241237, 238, 240sylancl 587 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) β†’ (β„• Γ— {if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0)}) ⇝ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0))
242235, 241eqbrtrd 5132 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) ∧ 𝑀 ≀ π‘˜) β†’ (𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) ⇝ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0))
243178, 242, 108, 111ltlecasei 11270 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (0...𝑁)) β†’ (𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀)))) ⇝ if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0))
244 snex 5393 . . . . . . . 8 {0} ∈ V
24527, 244xpex 7692 . . . . . . 7 (β„• Γ— {0}) ∈ V
246245a1i 11 . . . . . 6 (πœ‘ β†’ (β„• Γ— {0}) ∈ V)
247159anasss 468 . . . . . 6 ((πœ‘ ∧ (π‘˜ ∈ (0...𝑁) ∧ π‘š ∈ β„•)) β†’ ((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) ∈ β„‚)
248 plyeq0.5 . . . . . . . . . . . 12 (πœ‘ β†’ 0𝑝 = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘§β†‘π‘˜))))
249248fveq1d 6849 . . . . . . . . . . 11 (πœ‘ β†’ (0π‘β€˜π‘š) = ((𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘§β†‘π‘˜)))β€˜π‘š))
250249adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (0π‘β€˜π‘š) = ((𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘§β†‘π‘˜)))β€˜π‘š))
251127adantl 483 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•) β†’ π‘š ∈ β„‚)
252 0pval 25051 . . . . . . . . . . 11 (π‘š ∈ β„‚ β†’ (0π‘β€˜π‘š) = 0)
253251, 252syl 17 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (0π‘β€˜π‘š) = 0)
254 oveq1 7369 . . . . . . . . . . . . . 14 (𝑧 = π‘š β†’ (π‘§β†‘π‘˜) = (π‘šβ†‘π‘˜))
255254oveq2d 7378 . . . . . . . . . . . . 13 (𝑧 = π‘š β†’ ((π΄β€˜π‘˜) Β· (π‘§β†‘π‘˜)) = ((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)))
256255sumeq2sdv 15596 . . . . . . . . . . . 12 (𝑧 = π‘š β†’ Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘§β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)))
257 eqid 2737 . . . . . . . . . . . 12 (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘§β†‘π‘˜))) = (𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘§β†‘π‘˜)))
258 sumex 15579 . . . . . . . . . . . 12 Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)) ∈ V
259256, 257, 258fvmpt 6953 . . . . . . . . . . 11 (π‘š ∈ β„‚ β†’ ((𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘§β†‘π‘˜)))β€˜π‘š) = Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)))
260251, 259syl 17 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((𝑧 ∈ β„‚ ↦ Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘§β†‘π‘˜)))β€˜π‘š) = Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)))
261250, 253, 2603eqtr3d 2785 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 0 = Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)))
262261oveq1d 7377 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (0 / (π‘šβ†‘π‘€)) = (Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)) / (π‘šβ†‘π‘€)))
263 expcl 13992 . . . . . . . . . 10 ((π‘š ∈ β„‚ ∧ 𝑀 ∈ β„•0) β†’ (π‘šβ†‘π‘€) ∈ β„‚)
264127, 81, 263syl2anr 598 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (π‘šβ†‘π‘€) ∈ β„‚)
265134adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•) β†’ π‘š β‰  0)
266251, 265, 154expne0d 14064 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (π‘šβ†‘π‘€) β‰  0)
267264, 266div0d 11937 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (0 / (π‘šβ†‘π‘€)) = 0)
268 fzfid 13885 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (0...𝑁) ∈ Fin)
269 expcl 13992 . . . . . . . . . . 11 ((π‘š ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (π‘šβ†‘π‘˜) ∈ β„‚)
270251, 19, 269syl2an 597 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘šβ†‘π‘˜) ∈ β„‚)
271151, 270mulcld 11182 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)) ∈ β„‚)
272268, 264, 271, 266fsumdivc 15678 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (Ξ£π‘˜ ∈ (0...𝑁)((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)) / (π‘šβ†‘π‘€)) = Ξ£π‘˜ ∈ (0...𝑁)(((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)) / (π‘šβ†‘π‘€)))
273262, 267, 2723eqtr3d 2785 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 0 = Ξ£π‘˜ ∈ (0...𝑁)(((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)) / (π‘šβ†‘π‘€)))
274 fvconst2g 7156 . . . . . . . 8 ((0 ∈ β„‚ ∧ π‘š ∈ β„•) β†’ ((β„• Γ— {0})β€˜π‘š) = 0)
2758, 274sylan 581 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((β„• Γ— {0})β€˜π‘š) = 0)
276154adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ 𝑀 ∈ β„€)
27748adantl 483 . . . . . . . . . . 11 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ π‘˜ ∈ β„€)
278152, 153, 276, 277expsubd 14069 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘šβ†‘(π‘˜ βˆ’ 𝑀)) = ((π‘šβ†‘π‘˜) / (π‘šβ†‘π‘€)))
279278oveq2d 7378 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((π΄β€˜π‘˜) Β· (π‘šβ†‘(π‘˜ βˆ’ 𝑀))) = ((π΄β€˜π‘˜) Β· ((π‘šβ†‘π‘˜) / (π‘šβ†‘π‘€))))
280264adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘šβ†‘π‘€) ∈ β„‚)
281266adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ (π‘šβ†‘π‘€) β‰  0)
282151, 270, 280, 281divassd 11973 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ (((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)) / (π‘šβ†‘π‘€)) = ((π΄β€˜π‘˜) Β· ((π‘šβ†‘π‘˜) / (π‘šβ†‘π‘€))))
283279, 149, 2823eqtr4d 2787 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...𝑁)) β†’ ((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) = (((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)) / (π‘šβ†‘π‘€)))
284283sumeq2dv 15595 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ β„•) β†’ Ξ£π‘˜ ∈ (0...𝑁)((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š) = Ξ£π‘˜ ∈ (0...𝑁)(((π΄β€˜π‘˜) Β· (π‘šβ†‘π‘˜)) / (π‘šβ†‘π‘€)))
285273, 275, 2843eqtr4d 2787 . . . . . 6 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((β„• Γ— {0})β€˜π‘š) = Ξ£π‘˜ ∈ (0...𝑁)((𝑛 ∈ β„• ↦ ((π΄β€˜π‘˜) Β· (𝑛↑(π‘˜ βˆ’ 𝑀))))β€˜π‘š))
2861, 2, 3, 243, 246, 247, 285climfsum 15712 . . . . 5 (πœ‘ β†’ (β„• Γ— {0}) ⇝ Ξ£π‘˜ ∈ (0...𝑁)if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0))
287 suprleub 12128 . . . . . . . . . . . 12 ((((◑𝐴 β€œ (𝑆 βˆ– {0})) βŠ† ℝ ∧ (◑𝐴 β€œ (𝑆 βˆ– {0})) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))𝑧 ≀ π‘₯) ∧ 𝑁 ∈ ℝ) β†’ (sup((◑𝐴 β€œ (𝑆 βˆ– {0})), ℝ, < ) ≀ 𝑁 ↔ βˆ€π‘§ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))𝑧 ≀ 𝑁))
288196, 54, 77, 56, 287syl31anc 1374 . . . . . . . . . . 11 (πœ‘ β†’ (sup((◑𝐴 β€œ (𝑆 βˆ– {0})), ℝ, < ) ≀ 𝑁 ↔ βˆ€π‘§ ∈ (◑𝐴 β€œ (𝑆 βˆ– {0}))𝑧 ≀ 𝑁))
28975, 288mpbird 257 . . . . . . . . . 10 (πœ‘ β†’ sup((◑𝐴 β€œ (𝑆 βˆ– {0})), ℝ, < ) ≀ 𝑁)
29051, 289eqbrtrid 5145 . . . . . . . . 9 (πœ‘ β†’ 𝑀 ≀ 𝑁)
291 nn0uz 12812 . . . . . . . . . . 11 β„•0 = (β„€β‰₯β€˜0)
29281, 291eleqtrdi 2848 . . . . . . . . . 10 (πœ‘ β†’ 𝑀 ∈ (β„€β‰₯β€˜0))
29355nn0zd 12532 . . . . . . . . . 10 (πœ‘ β†’ 𝑁 ∈ β„€)
294 elfz5 13440 . . . . . . . . . 10 ((𝑀 ∈ (β„€β‰₯β€˜0) ∧ 𝑁 ∈ β„€) β†’ (𝑀 ∈ (0...𝑁) ↔ 𝑀 ≀ 𝑁))
295292, 293, 294syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ (𝑀 ∈ (0...𝑁) ↔ 𝑀 ≀ 𝑁))
296290, 295mpbird 257 . . . . . . . 8 (πœ‘ β†’ 𝑀 ∈ (0...𝑁))
297296snssd 4774 . . . . . . 7 (πœ‘ β†’ {𝑀} βŠ† (0...𝑁))
29818, 81ffvelcdmd 7041 . . . . . . . . 9 (πœ‘ β†’ (π΄β€˜π‘€) ∈ β„‚)
299 elsni 4608 . . . . . . . . . . 11 (π‘˜ ∈ {𝑀} β†’ π‘˜ = 𝑀)
300299fveq2d 6851 . . . . . . . . . 10 (π‘˜ ∈ {𝑀} β†’ (π΄β€˜π‘˜) = (π΄β€˜π‘€))
301300eleq1d 2823 . . . . . . . . 9 (π‘˜ ∈ {𝑀} β†’ ((π΄β€˜π‘˜) ∈ β„‚ ↔ (π΄β€˜π‘€) ∈ β„‚))
302298, 301syl5ibrcom 247 . . . . . . . 8 (πœ‘ β†’ (π‘˜ ∈ {𝑀} β†’ (π΄β€˜π‘˜) ∈ β„‚))
303302ralrimiv 3143 . . . . . . 7 (πœ‘ β†’ βˆ€π‘˜ ∈ {𝑀} (π΄β€˜π‘˜) ∈ β„‚)
3043olcd 873 . . . . . . 7 (πœ‘ β†’ ((0...𝑁) βŠ† (β„€β‰₯β€˜0) ∨ (0...𝑁) ∈ Fin))
305 sumss2 15618 . . . . . . 7 ((({𝑀} βŠ† (0...𝑁) ∧ βˆ€π‘˜ ∈ {𝑀} (π΄β€˜π‘˜) ∈ β„‚) ∧ ((0...𝑁) βŠ† (β„€β‰₯β€˜0) ∨ (0...𝑁) ∈ Fin)) β†’ Ξ£π‘˜ ∈ {𝑀} (π΄β€˜π‘˜) = Ξ£π‘˜ ∈ (0...𝑁)if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0))
306297, 303, 304, 305syl21anc 837 . . . . . 6 (πœ‘ β†’ Ξ£π‘˜ ∈ {𝑀} (π΄β€˜π‘˜) = Ξ£π‘˜ ∈ (0...𝑁)if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0))
307 ltso 11242 . . . . . . . . 9 < Or ℝ
308307supex 9406 . . . . . . . 8 sup((◑𝐴 β€œ (𝑆 βˆ– {0})), ℝ, < ) ∈ V
30951, 308eqeltri 2834 . . . . . . 7 𝑀 ∈ V
310 fveq2 6847 . . . . . . . 8 (π‘˜ = 𝑀 β†’ (π΄β€˜π‘˜) = (π΄β€˜π‘€))
311310sumsn 15638 . . . . . . 7 ((𝑀 ∈ V ∧ (π΄β€˜π‘€) ∈ β„‚) β†’ Ξ£π‘˜ ∈ {𝑀} (π΄β€˜π‘˜) = (π΄β€˜π‘€))
312309, 298, 311sylancr 588 . . . . . 6 (πœ‘ β†’ Ξ£π‘˜ ∈ {𝑀} (π΄β€˜π‘˜) = (π΄β€˜π‘€))
313306, 312eqtr3d 2779 . . . . 5 (πœ‘ β†’ Ξ£π‘˜ ∈ (0...𝑁)if(π‘˜ ∈ {𝑀}, (π΄β€˜π‘˜), 0) = (π΄β€˜π‘€))
314286, 313breqtrd 5136 . . . 4 (πœ‘ β†’ (β„• Γ— {0}) ⇝ (π΄β€˜π‘€))
315239, 27climconst2 15437 . . . . 5 ((0 ∈ β„‚ ∧ 1 ∈ β„€) β†’ (β„• Γ— {0}) ⇝ 0)
3167, 238, 315mp2an 691 . . . 4 (β„• Γ— {0}) ⇝ 0
317 climuni 15441 . . . 4 (((β„• Γ— {0}) ⇝ (π΄β€˜π‘€) ∧ (β„• Γ— {0}) ⇝ 0) β†’ (π΄β€˜π‘€) = 0)
318314, 316, 317sylancl 587 . . 3 (πœ‘ β†’ (π΄β€˜π‘€) = 0)
319 fvex 6860 . . . 4 (π΄β€˜π‘€) ∈ V
320319elsn 4606 . . 3 ((π΄β€˜π‘€) ∈ {0} ↔ (π΄β€˜π‘€) = 0)
321318, 320sylibr 233 . 2 (πœ‘ β†’ (π΄β€˜π‘€) ∈ {0})
322 elpreima 7013 . . . . . 6 (𝐴 Fn β„•0 β†’ (𝑀 ∈ (◑𝐴 β€œ (𝑆 βˆ– {0})) ↔ (𝑀 ∈ β„•0 ∧ (π΄β€˜π‘€) ∈ (𝑆 βˆ– {0}))))
32357, 322syl 17 . . . . 5 (πœ‘ β†’ (𝑀 ∈ (◑𝐴 β€œ (𝑆 βˆ– {0})) ↔ (𝑀 ∈ β„•0 ∧ (π΄β€˜π‘€) ∈ (𝑆 βˆ– {0}))))
32480, 323mpbid 231 . . . 4 (πœ‘ β†’ (𝑀 ∈ β„•0 ∧ (π΄β€˜π‘€) ∈ (𝑆 βˆ– {0})))
325324simprd 497 . . 3 (πœ‘ β†’ (π΄β€˜π‘€) ∈ (𝑆 βˆ– {0}))
326325eldifbd 3928 . 2 (πœ‘ β†’ Β¬ (π΄β€˜π‘€) ∈ {0})
327321, 326pm2.65i 193 1 Β¬ πœ‘
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3448   βˆ– cdif 3912   βˆͺ cun 3913   βŠ† wss 3915  βˆ…c0 4287  ifcif 4491  {csn 4591   class class class wbr 5110   ↦ cmpt 5193   Γ— cxp 5636  β—‘ccnv 5637   β€œ cima 5641   Fn wfn 6496  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   ↑m cmap 8772  Fincfn 8890  supcsup 9383  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  -cneg 11393   / cdiv 11819  β„•cn 12160  β„•0cn0 12420  β„€cz 12506  β„€β‰₯cuz 12770  β„+crp 12922  ...cfz 13431  β†‘cexp 13974  abscabs 15126   ⇝ cli 15373  Ξ£csu 15577  0𝑝c0p 25049
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-fz 13432  df-fzo 13575  df-fl 13704  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-rlim 15378  df-sum 15578  df-0p 25050
This theorem is referenced by:  plyeq0  25588
  Copyright terms: Public domain W3C validator