Users' Mathboxes Mathbox for Steve Rodriguez < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  radcnvrat Structured version   Visualization version   GIF version

Theorem radcnvrat 43155
Description: Let 𝐿 be the limit, if one exists, of the ratio (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))) (as in the ratio test cvgdvgrat 43154) as π‘˜ increases. Then the radius of convergence of power series Σ𝑛 ∈ β„•0((π΄β€˜π‘›) Β· (π‘₯↑𝑛)) is (1 / 𝐿) if 𝐿 is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence 43154 β€”a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020.)
Hypotheses
Ref Expression
radcnvrat.g 𝐺 = (π‘₯ ∈ β„‚ ↦ (𝑛 ∈ β„•0 ↦ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛))))
radcnvrat.a (πœ‘ β†’ 𝐴:β„•0βŸΆβ„‚)
radcnvrat.r 𝑅 = sup({π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }, ℝ*, < )
radcnvrat.rat 𝐷 = (π‘˜ ∈ β„•0 ↦ (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))))
radcnvrat.z 𝑍 = (β„€β‰₯β€˜π‘€)
radcnvrat.m (πœ‘ β†’ 𝑀 ∈ β„•0)
radcnvrat.n0 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π΄β€˜π‘˜) β‰  0)
radcnvrat.l (πœ‘ β†’ 𝐷 ⇝ 𝐿)
radcnvrat.ln0 (πœ‘ β†’ 𝐿 β‰  0)
Assertion
Ref Expression
radcnvrat (πœ‘ β†’ 𝑅 = (1 / 𝐿))
Distinct variable groups:   π‘˜,𝑛,π‘₯,πœ‘   𝐴,𝑛,π‘₯   π‘˜,𝐺,𝑛,π‘₯   π‘˜,π‘Ÿ,π‘₯,𝐺   π‘˜,𝐿,π‘₯   π‘˜,𝑍,𝑛   𝐷,π‘˜   π‘˜,𝑀
Allowed substitution hints:   πœ‘(π‘Ÿ)   𝐴(π‘˜,π‘Ÿ)   𝐷(π‘₯,𝑛,π‘Ÿ)   𝑅(π‘₯,π‘˜,𝑛,π‘Ÿ)   𝐿(𝑛,π‘Ÿ)   𝑀(π‘₯,𝑛,π‘Ÿ)   𝑍(π‘₯,π‘Ÿ)

Proof of Theorem radcnvrat
StepHypRef Expression
1 radcnvrat.r . 2 𝑅 = sup({π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }, ℝ*, < )
2 xrltso 13122 . . . 4 < Or ℝ*
32a1i 11 . . 3 (πœ‘ β†’ < Or ℝ*)
4 radcnvrat.z . . . . . 6 𝑍 = (β„€β‰₯β€˜π‘€)
5 radcnvrat.m . . . . . . 7 (πœ‘ β†’ 𝑀 ∈ β„•0)
65nn0zd 12586 . . . . . 6 (πœ‘ β†’ 𝑀 ∈ β„€)
74reseq2i 5978 . . . . . . 7 (𝐷 β†Ύ 𝑍) = (𝐷 β†Ύ (β„€β‰₯β€˜π‘€))
8 radcnvrat.l . . . . . . . 8 (πœ‘ β†’ 𝐷 ⇝ 𝐿)
9 radcnvrat.rat . . . . . . . . . 10 𝐷 = (π‘˜ ∈ β„•0 ↦ (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))))
10 nn0ex 12480 . . . . . . . . . . 11 β„•0 ∈ V
1110mptex 7227 . . . . . . . . . 10 (π‘˜ ∈ β„•0 ↦ (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)))) ∈ V
129, 11eqeltri 2829 . . . . . . . . 9 𝐷 ∈ V
13 climres 15521 . . . . . . . . 9 ((𝑀 ∈ β„€ ∧ 𝐷 ∈ V) β†’ ((𝐷 β†Ύ (β„€β‰₯β€˜π‘€)) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿))
146, 12, 13sylancl 586 . . . . . . . 8 (πœ‘ β†’ ((𝐷 β†Ύ (β„€β‰₯β€˜π‘€)) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿))
158, 14mpbird 256 . . . . . . 7 (πœ‘ β†’ (𝐷 β†Ύ (β„€β‰₯β€˜π‘€)) ⇝ 𝐿)
167, 15eqbrtrid 5183 . . . . . 6 (πœ‘ β†’ (𝐷 β†Ύ 𝑍) ⇝ 𝐿)
179reseq1i 5977 . . . . . . . . 9 (𝐷 β†Ύ 𝑍) = ((π‘˜ ∈ β„•0 ↦ (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)))) β†Ύ 𝑍)
18 eluznn0 12903 . . . . . . . . . . . . . 14 ((𝑀 ∈ β„•0 ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘€)) β†’ π‘˜ ∈ β„•0)
195, 18sylan 580 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘€)) β†’ π‘˜ ∈ β„•0)
2019ex 413 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘˜ ∈ (β„€β‰₯β€˜π‘€) β†’ π‘˜ ∈ β„•0))
2120ssrdv 3988 . . . . . . . . . . 11 (πœ‘ β†’ (β„€β‰₯β€˜π‘€) βŠ† β„•0)
224, 21eqsstrid 4030 . . . . . . . . . 10 (πœ‘ β†’ 𝑍 βŠ† β„•0)
2322resmptd 6040 . . . . . . . . 9 (πœ‘ β†’ ((π‘˜ ∈ β„•0 ↦ (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)))) β†Ύ 𝑍) = (π‘˜ ∈ 𝑍 ↦ (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)))))
2417, 23eqtrid 2784 . . . . . . . 8 (πœ‘ β†’ (𝐷 β†Ύ 𝑍) = (π‘˜ ∈ 𝑍 ↦ (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)))))
25 fvexd 6906 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))) ∈ V)
2624, 25fvmpt2d 7011 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ ((𝐷 β†Ύ 𝑍)β€˜π‘˜) = (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))))
274peano2uzs 12888 . . . . . . . . . 10 (π‘˜ ∈ 𝑍 β†’ (π‘˜ + 1) ∈ 𝑍)
2822sselda 3982 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ + 1) ∈ 𝑍) β†’ (π‘˜ + 1) ∈ β„•0)
29 radcnvrat.a . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴:β„•0βŸΆβ„‚)
3029ffvelcdmda 7086 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ + 1) ∈ β„•0) β†’ (π΄β€˜(π‘˜ + 1)) ∈ β„‚)
3128, 30syldan 591 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ + 1) ∈ 𝑍) β†’ (π΄β€˜(π‘˜ + 1)) ∈ β„‚)
3227, 31sylan2 593 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π΄β€˜(π‘˜ + 1)) ∈ β„‚)
3322sselda 3982 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ π‘˜ ∈ β„•0)
3429ffvelcdmda 7086 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π΄β€˜π‘˜) ∈ β„‚)
3533, 34syldan 591 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π΄β€˜π‘˜) ∈ β„‚)
36 radcnvrat.n0 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π΄β€˜π‘˜) β‰  0)
3732, 35, 36divcld 11992 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ ((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)) ∈ β„‚)
3837abscld 15385 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))) ∈ ℝ)
3926, 38eqeltrd 2833 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ ((𝐷 β†Ύ 𝑍)β€˜π‘˜) ∈ ℝ)
404, 6, 16, 39climrecl 15529 . . . . 5 (πœ‘ β†’ 𝐿 ∈ ℝ)
41 radcnvrat.ln0 . . . . 5 (πœ‘ β†’ 𝐿 β‰  0)
4240, 41rereccld 12043 . . . 4 (πœ‘ β†’ (1 / 𝐿) ∈ ℝ)
4342rexrd 11266 . . 3 (πœ‘ β†’ (1 / 𝐿) ∈ ℝ*)
44 simpr 485 . . . 4 ((πœ‘ ∧ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }) β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ })
45 elrabi 3677 . . . . 5 (π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ } β†’ π‘₯ ∈ ℝ)
4642adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (1 / 𝐿) ∈ ℝ)
47 recn 11202 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ π‘₯ ∈ β„‚)
4847abscld 15385 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ (absβ€˜π‘₯) ∈ ℝ)
4948adantl 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (absβ€˜π‘₯) ∈ ℝ)
5046, 49ltlend 11361 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((1 / 𝐿) < (absβ€˜π‘₯) ↔ ((1 / 𝐿) ≀ (absβ€˜π‘₯) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿))))
5150simplbda 500 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (1 / 𝐿) < (absβ€˜π‘₯)) β†’ (absβ€˜π‘₯) β‰  (1 / 𝐿))
5250adantr 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿)) β†’ ((1 / 𝐿) < (absβ€˜π‘₯) ↔ ((1 / 𝐿) ≀ (absβ€˜π‘₯) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿))))
53 simpr 485 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿)) β†’ (absβ€˜π‘₯) β‰  (1 / 𝐿))
5453biantrud 532 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿)) β†’ ((1 / 𝐿) ≀ (absβ€˜π‘₯) ↔ ((1 / 𝐿) ≀ (absβ€˜π‘₯) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿))))
5546, 49lenltd 11362 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((1 / 𝐿) ≀ (absβ€˜π‘₯) ↔ Β¬ (absβ€˜π‘₯) < (1 / 𝐿)))
5655adantr 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿)) β†’ ((1 / 𝐿) ≀ (absβ€˜π‘₯) ↔ Β¬ (absβ€˜π‘₯) < (1 / 𝐿)))
5752, 54, 563bitr2d 306 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿)) β†’ ((1 / 𝐿) < (absβ€˜π‘₯) ↔ Β¬ (absβ€˜π‘₯) < (1 / 𝐿)))
58 1cnd 11211 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ 1 ∈ β„‚)
5949recnd 11244 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (absβ€˜π‘₯) ∈ β„‚)
6040recnd 11244 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐿 ∈ β„‚)
6160adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ 𝐿 ∈ β„‚)
6241adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ 𝐿 β‰  0)
6358, 59, 61, 62divmul3d 12026 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((1 / 𝐿) = (absβ€˜π‘₯) ↔ 1 = ((absβ€˜π‘₯) Β· 𝐿)))
64 eqcom 2739 . . . . . . . . . . . . . . . . 17 ((1 / 𝐿) = (absβ€˜π‘₯) ↔ (absβ€˜π‘₯) = (1 / 𝐿))
65 eqcom 2739 . . . . . . . . . . . . . . . . 17 (1 = ((absβ€˜π‘₯) Β· 𝐿) ↔ ((absβ€˜π‘₯) Β· 𝐿) = 1)
6663, 64, 653bitr3g 312 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((absβ€˜π‘₯) = (1 / 𝐿) ↔ ((absβ€˜π‘₯) Β· 𝐿) = 1))
6766necon3bid 2985 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((absβ€˜π‘₯) β‰  (1 / 𝐿) ↔ ((absβ€˜π‘₯) Β· 𝐿) β‰  1))
6867biimpa 477 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿)) β†’ ((absβ€˜π‘₯) Β· 𝐿) β‰  1)
69 1red 11217 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ 1 ∈ ℝ)
70 fvres 6910 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ ∈ 𝑍 β†’ ((𝐷 β†Ύ 𝑍)β€˜π‘˜) = (π·β€˜π‘˜))
7170adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ ((𝐷 β†Ύ 𝑍)β€˜π‘˜) = (π·β€˜π‘˜))
7271, 39eqeltrrd 2834 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π·β€˜π‘˜) ∈ ℝ)
7337absge0d 15393 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ 0 ≀ (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))))
7473, 26breqtrrd 5176 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ 0 ≀ ((𝐷 β†Ύ 𝑍)β€˜π‘˜))
7574, 71breqtrd 5174 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ 0 ≀ (π·β€˜π‘˜))
764, 6, 8, 72, 75climge0 15530 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 0 ≀ 𝐿)
7740, 76, 41ne0gt0d 11353 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 0 < 𝐿)
7840, 77elrpd 13015 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐿 ∈ ℝ+)
7978adantr 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ 𝐿 ∈ ℝ+)
8049, 69, 79ltmuldivd 13065 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (((absβ€˜π‘₯) Β· 𝐿) < 1 ↔ (absβ€˜π‘₯) < (1 / 𝐿)))
8180adantr 481 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) β†’ (((absβ€˜π‘₯) Β· 𝐿) < 1 ↔ (absβ€˜π‘₯) < (1 / 𝐿)))
82 elun 4148 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ ((ℝ ∩ {0}) βˆͺ (ℝ βˆ– {0})) ↔ (π‘₯ ∈ (ℝ ∩ {0}) ∨ π‘₯ ∈ (ℝ βˆ– {0})))
83 inundif 4478 . . . . . . . . . . . . . . . . . . 19 ((ℝ ∩ {0}) βˆͺ (ℝ βˆ– {0})) = ℝ
8483eleq2i 2825 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ ((ℝ ∩ {0}) βˆͺ (ℝ βˆ– {0})) ↔ π‘₯ ∈ ℝ)
8582, 84bitr3i 276 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ (ℝ ∩ {0}) ∨ π‘₯ ∈ (ℝ βˆ– {0})) ↔ π‘₯ ∈ ℝ)
86 elin 3964 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ (ℝ ∩ {0}) ↔ (π‘₯ ∈ ℝ ∧ π‘₯ ∈ {0}))
8786simprbi 497 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (ℝ ∩ {0}) β†’ π‘₯ ∈ {0})
88 elsni 4645 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ {0} β†’ π‘₯ = 0)
8987, 88syl 17 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (ℝ ∩ {0}) β†’ π‘₯ = 0)
90 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = 0 β†’ (absβ€˜π‘₯) = (absβ€˜0))
91 abs0 15234 . . . . . . . . . . . . . . . . . . . . . . . . 25 (absβ€˜0) = 0
9290, 91eqtrdi 2788 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = 0 β†’ (absβ€˜π‘₯) = 0)
9392oveq1d 7426 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = 0 β†’ ((absβ€˜π‘₯) Β· 𝐿) = (0 Β· 𝐿))
9460mul02d 11414 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (0 Β· 𝐿) = 0)
9593, 94sylan9eqr 2794 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ = 0) β†’ ((absβ€˜π‘₯) Β· 𝐿) = 0)
96 0lt1 11738 . . . . . . . . . . . . . . . . . . . . . 22 0 < 1
9795, 96eqbrtrdi 5187 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ = 0) β†’ ((absβ€˜π‘₯) Β· 𝐿) < 1)
98 radcnvrat.g . . . . . . . . . . . . . . . . . . . . . . . 24 𝐺 = (π‘₯ ∈ β„‚ ↦ (𝑛 ∈ β„•0 ↦ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛))))
9998, 29radcnv0 25935 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 0 ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ })
100 eleq1 2821 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = 0 β†’ (π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ } ↔ 0 ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
10199, 100syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (π‘₯ = 0 β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
102101imp 407 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ = 0) β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ })
10397, 1022thd 264 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ = 0) β†’ (((absβ€˜π‘₯) Β· 𝐿) < 1 ↔ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
10489, 103sylan2 593 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ (ℝ ∩ {0})) β†’ (((absβ€˜π‘₯) Β· 𝐿) < 1 ↔ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
105104adantlr 713 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) ∧ π‘₯ ∈ (ℝ ∩ {0})) β†’ (((absβ€˜π‘₯) Β· 𝐿) < 1 ↔ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
106 ax-resscn 11169 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ βŠ† β„‚
107 ssdif 4139 . . . . . . . . . . . . . . . . . . . . . . 23 (ℝ βŠ† β„‚ β†’ (ℝ βˆ– {0}) βŠ† (β„‚ βˆ– {0}))
108106, 107ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (ℝ βˆ– {0}) βŠ† (β„‚ βˆ– {0})
109108sseli 3978 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (ℝ βˆ– {0}) β†’ π‘₯ ∈ (β„‚ βˆ– {0}))
110 nn0uz 12866 . . . . . . . . . . . . . . . . . . . . . 22 β„•0 = (β„€β‰₯β€˜0)
1115ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) β†’ 𝑀 ∈ β„•0)
112 fvexd 6906 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) β†’ (πΊβ€˜π‘₯) ∈ V)
113 eldifi 4126 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ (β„‚ βˆ– {0}) β†’ π‘₯ ∈ β„‚)
11498a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ 𝐺 = (π‘₯ ∈ β„‚ ↦ (𝑛 ∈ β„•0 ↦ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛)))))
11510mptex 7227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ β„•0 ↦ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛))) ∈ V
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ π‘₯ ∈ β„‚) β†’ (𝑛 ∈ β„•0 ↦ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛))) ∈ V)
117114, 116fvmpt2d 7011 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ π‘₯ ∈ β„‚) β†’ (πΊβ€˜π‘₯) = (𝑛 ∈ β„•0 ↦ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛))))
118117adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ (πΊβ€˜π‘₯) = (𝑛 ∈ β„•0 ↦ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛))))
119 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = π‘˜ β†’ (π΄β€˜π‘›) = (π΄β€˜π‘˜))
120 oveq2 7419 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = π‘˜ β†’ (π‘₯↑𝑛) = (π‘₯β†‘π‘˜))
121119, 120oveq12d 7429 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = π‘˜ β†’ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛)) = ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜)))
122121adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 = π‘˜) β†’ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛)) = ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜)))
123 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„•0)
124 ovexd 7446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜)) ∈ V)
125118, 122, 123, 124fvmptd 7005 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ ((πΊβ€˜π‘₯)β€˜π‘˜) = ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜)))
12634adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ (π΄β€˜π‘˜) ∈ β„‚)
127 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ π‘₯ ∈ β„‚)
128127, 123expcld 14113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ (π‘₯β†‘π‘˜) ∈ β„‚)
129126, 128mulcld 11236 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜)) ∈ β„‚)
130125, 129eqeltrd 2833 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ β„•0) β†’ ((πΊβ€˜π‘₯)β€˜π‘˜) ∈ β„‚)
131113, 130sylanl2 679 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ β„•0) β†’ ((πΊβ€˜π‘₯)β€˜π‘˜) ∈ β„‚)
132131adantlr 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) ∧ π‘˜ ∈ β„•0) β†’ ((πΊβ€˜π‘₯)β€˜π‘˜) ∈ β„‚)
13333adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) β†’ π‘˜ ∈ β„•0)
134133, 125syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) β†’ ((πΊβ€˜π‘₯)β€˜π‘˜) = ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜)))
135113, 134sylanl2 679 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ ((πΊβ€˜π‘₯)β€˜π‘˜) = ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜)))
13635adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π΄β€˜π‘˜) ∈ β„‚)
137113adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ π‘₯ ∈ β„‚)
138137adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ π‘₯ ∈ β„‚)
13933adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ π‘˜ ∈ β„•0)
140138, 139expcld 14113 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π‘₯β†‘π‘˜) ∈ β„‚)
14136adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π΄β€˜π‘˜) β‰  0)
142 eldifsni 4793 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘₯ ∈ (β„‚ βˆ– {0}) β†’ π‘₯ β‰  0)
143142ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ π‘₯ β‰  0)
144139nn0zd 12586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ π‘˜ ∈ β„€)
145138, 143, 144expne0d 14119 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π‘₯β†‘π‘˜) β‰  0)
146136, 140, 141, 145mulne0d 11868 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜)) β‰  0)
147135, 146eqnetrd 3008 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ ((πΊβ€˜π‘₯)β€˜π‘˜) β‰  0)
148147adantlr 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) ∧ π‘˜ ∈ 𝑍) β†’ ((πΊβ€˜π‘₯)β€˜π‘˜) β‰  0)
149 fvoveq1 7434 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = π‘˜ β†’ ((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) = ((πΊβ€˜π‘₯)β€˜(π‘˜ + 1)))
150 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = π‘˜ β†’ ((πΊβ€˜π‘₯)β€˜π‘›) = ((πΊβ€˜π‘₯)β€˜π‘˜))
151149, 150oveq12d 7429 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = π‘˜ β†’ (((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)) = (((πΊβ€˜π‘₯)β€˜(π‘˜ + 1)) / ((πΊβ€˜π‘₯)β€˜π‘˜)))
152151fveq2d 6895 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = π‘˜ β†’ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›))) = (absβ€˜(((πΊβ€˜π‘₯)β€˜(π‘˜ + 1)) / ((πΊβ€˜π‘₯)β€˜π‘˜))))
153152cbvmptv 5261 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ 𝑍 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) = (π‘˜ ∈ 𝑍 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(π‘˜ + 1)) / ((πΊβ€˜π‘₯)β€˜π‘˜))))
1544reseq2i 5978 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) β†Ύ 𝑍) = ((𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) β†Ύ (β„€β‰₯β€˜π‘€))
15522adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ 𝑍 βŠ† β„•0)
156155resmptd 6040 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ ((𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) β†Ύ 𝑍) = (𝑛 ∈ 𝑍 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))))
157154, 156eqtr3id 2786 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ ((𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) β†Ύ (β„€β‰₯β€˜π‘€)) = (𝑛 ∈ 𝑍 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))))
1586adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ 𝑀 ∈ β„€)
1598adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ 𝐷 ⇝ 𝐿)
160137abscld 15385 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ (absβ€˜π‘₯) ∈ ℝ)
161160recnd 11244 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ (absβ€˜π‘₯) ∈ β„‚)
16210mptex 7227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) ∈ V
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ (𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) ∈ V)
16472recnd 11244 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π·β€˜π‘˜) ∈ β„‚)
165164adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π·β€˜π‘˜) ∈ β„‚)
166 eqidd 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) = (𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))))
167152adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) ∧ 𝑛 = π‘˜) β†’ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›))) = (absβ€˜(((πΊβ€˜π‘₯)β€˜(π‘˜ + 1)) / ((πΊβ€˜π‘₯)β€˜π‘˜))))
168 fvexd 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (absβ€˜(((πΊβ€˜π‘₯)β€˜(π‘˜ + 1)) / ((πΊβ€˜π‘₯)β€˜π‘˜))) ∈ V)
169166, 167, 139, 168fvmptd 7005 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ ((𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›))))β€˜π‘˜) = (absβ€˜(((πΊβ€˜π‘₯)β€˜(π‘˜ + 1)) / ((πΊβ€˜π‘₯)β€˜π‘˜))))
170117adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) β†’ (πΊβ€˜π‘₯) = (𝑛 ∈ β„•0 ↦ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛))))
171 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) ∧ 𝑛 = (π‘˜ + 1)) β†’ 𝑛 = (π‘˜ + 1))
172171fveq2d 6895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) ∧ 𝑛 = (π‘˜ + 1)) β†’ (π΄β€˜π‘›) = (π΄β€˜(π‘˜ + 1)))
173171oveq2d 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) ∧ 𝑛 = (π‘˜ + 1)) β†’ (π‘₯↑𝑛) = (π‘₯↑(π‘˜ + 1)))
174172, 173oveq12d 7429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) ∧ 𝑛 = (π‘˜ + 1)) β†’ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛)) = ((π΄β€˜(π‘˜ + 1)) Β· (π‘₯↑(π‘˜ + 1))))
175 1nn0 12490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1 ∈ β„•0
176175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) β†’ 1 ∈ β„•0)
177133, 176nn0addcld 12538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) β†’ (π‘˜ + 1) ∈ β„•0)
178 ovexd 7446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) β†’ ((π΄β€˜(π‘˜ + 1)) Β· (π‘₯↑(π‘˜ + 1))) ∈ V)
179170, 174, 177, 178fvmptd 7005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) β†’ ((πΊβ€˜π‘₯)β€˜(π‘˜ + 1)) = ((π΄β€˜(π‘˜ + 1)) Β· (π‘₯↑(π‘˜ + 1))))
180121adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) ∧ 𝑛 = π‘˜) β†’ ((π΄β€˜π‘›) Β· (π‘₯↑𝑛)) = ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜)))
181 ovexd 7446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) β†’ ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜)) ∈ V)
182170, 180, 133, 181fvmptd 7005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) β†’ ((πΊβ€˜π‘₯)β€˜π‘˜) = ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜)))
183179, 182oveq12d 7429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ π‘˜ ∈ 𝑍) β†’ (((πΊβ€˜π‘₯)β€˜(π‘˜ + 1)) / ((πΊβ€˜π‘₯)β€˜π‘˜)) = (((π΄β€˜(π‘˜ + 1)) Β· (π‘₯↑(π‘˜ + 1))) / ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜))))
184113, 183sylanl2 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (((πΊβ€˜π‘₯)β€˜(π‘˜ + 1)) / ((πΊβ€˜π‘₯)β€˜π‘˜)) = (((π΄β€˜(π‘˜ + 1)) Β· (π‘₯↑(π‘˜ + 1))) / ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜))))
18532adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π΄β€˜(π‘˜ + 1)) ∈ β„‚)
186113, 177sylanl2 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π‘˜ + 1) ∈ β„•0)
187138, 186expcld 14113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π‘₯↑(π‘˜ + 1)) ∈ β„‚)
188185, 136, 187, 140, 141, 145divmuldivd 12033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)) Β· ((π‘₯↑(π‘˜ + 1)) / (π‘₯β†‘π‘˜))) = (((π΄β€˜(π‘˜ + 1)) Β· (π‘₯↑(π‘˜ + 1))) / ((π΄β€˜π‘˜) Β· (π‘₯β†‘π‘˜))))
189139nn0cnd 12536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ π‘˜ ∈ β„‚)
190 1cnd 11211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ 1 ∈ β„‚)
191189, 190pncan2d 11575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ ((π‘˜ + 1) βˆ’ π‘˜) = 1)
192191oveq2d 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π‘₯↑((π‘˜ + 1) βˆ’ π‘˜)) = (π‘₯↑1))
193186nn0zd 12586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π‘˜ + 1) ∈ β„€)
194138, 143, 144, 193expsubd 14124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π‘₯↑((π‘˜ + 1) βˆ’ π‘˜)) = ((π‘₯↑(π‘˜ + 1)) / (π‘₯β†‘π‘˜)))
195138exp1d 14108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π‘₯↑1) = π‘₯)
196192, 194, 1953eqtr3d 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ ((π‘₯↑(π‘˜ + 1)) / (π‘₯β†‘π‘˜)) = π‘₯)
197196oveq2d 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)) Β· ((π‘₯↑(π‘˜ + 1)) / (π‘₯β†‘π‘˜))) = (((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)) Β· π‘₯))
198184, 188, 1973eqtr2d 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (((πΊβ€˜π‘₯)β€˜(π‘˜ + 1)) / ((πΊβ€˜π‘₯)β€˜π‘˜)) = (((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)) Β· π‘₯))
199198fveq2d 6895 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (absβ€˜(((πΊβ€˜π‘₯)β€˜(π‘˜ + 1)) / ((πΊβ€˜π‘₯)β€˜π‘˜))) = (absβ€˜(((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)) Β· π‘₯)))
20037adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ ((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)) ∈ β„‚)
201200, 138absmuld 15403 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (absβ€˜(((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜)) Β· π‘₯)) = ((absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))) Β· (absβ€˜π‘₯)))
202169, 199, 2013eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ ((𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›))))β€˜π‘˜) = ((absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))) Β· (absβ€˜π‘₯)))
20371, 26eqtr3d 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π·β€˜π‘˜) = (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))))
204203adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (π·β€˜π‘˜) = (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))))
205204eqcomd 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))) = (π·β€˜π‘˜))
206205oveq1d 7426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ ((absβ€˜((π΄β€˜(π‘˜ + 1)) / (π΄β€˜π‘˜))) Β· (absβ€˜π‘₯)) = ((π·β€˜π‘˜) Β· (absβ€˜π‘₯)))
207161adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ (absβ€˜π‘₯) ∈ β„‚)
208165, 207mulcomd 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ ((π·β€˜π‘˜) Β· (absβ€˜π‘₯)) = ((absβ€˜π‘₯) Β· (π·β€˜π‘˜)))
209202, 206, 2083eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ π‘˜ ∈ 𝑍) β†’ ((𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›))))β€˜π‘˜) = ((absβ€˜π‘₯) Β· (π·β€˜π‘˜)))
2104, 158, 159, 161, 163, 165, 209climmulc2 15583 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ (𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) ⇝ ((absβ€˜π‘₯) Β· 𝐿))
211 climres 15521 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ β„€ ∧ (𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) ∈ V) β†’ (((𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) β†Ύ (β„€β‰₯β€˜π‘€)) ⇝ ((absβ€˜π‘₯) Β· 𝐿) ↔ (𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) ⇝ ((absβ€˜π‘₯) Β· 𝐿)))
212158, 162, 211sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ (((𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) β†Ύ (β„€β‰₯β€˜π‘€)) ⇝ ((absβ€˜π‘₯) Β· 𝐿) ↔ (𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) ⇝ ((absβ€˜π‘₯) Β· 𝐿)))
213210, 212mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ ((𝑛 ∈ β„•0 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) β†Ύ (β„€β‰₯β€˜π‘€)) ⇝ ((absβ€˜π‘₯) Β· 𝐿))
214157, 213eqbrtrrd 5172 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) β†’ (𝑛 ∈ 𝑍 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) ⇝ ((absβ€˜π‘₯) Β· 𝐿))
215214adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) β†’ (𝑛 ∈ 𝑍 ↦ (absβ€˜(((πΊβ€˜π‘₯)β€˜(𝑛 + 1)) / ((πΊβ€˜π‘₯)β€˜π‘›)))) ⇝ ((absβ€˜π‘₯) Β· 𝐿))
216 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) β†’ ((absβ€˜π‘₯) Β· 𝐿) β‰  1)
217110, 4, 111, 112, 132, 148, 153, 215, 216cvgdvgrat 43154 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘₯ ∈ (β„‚ βˆ– {0})) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) β†’ (((absβ€˜π‘₯) Β· 𝐿) < 1 ↔ seq0( + , (πΊβ€˜π‘₯)) ∈ dom ⇝ ))
218109, 217sylanl2 679 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘₯ ∈ (ℝ βˆ– {0})) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) β†’ (((absβ€˜π‘₯) Β· 𝐿) < 1 ↔ seq0( + , (πΊβ€˜π‘₯)) ∈ dom ⇝ ))
219 eldifi 4126 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ (ℝ βˆ– {0}) β†’ π‘₯ ∈ ℝ)
220 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ÿ = π‘₯ β†’ (πΊβ€˜π‘Ÿ) = (πΊβ€˜π‘₯))
221220seqeq3d 13976 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ÿ = π‘₯ β†’ seq0( + , (πΊβ€˜π‘Ÿ)) = seq0( + , (πΊβ€˜π‘₯)))
222221eleq1d 2818 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Ÿ = π‘₯ β†’ (seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ ↔ seq0( + , (πΊβ€˜π‘₯)) ∈ dom ⇝ ))
223222elrab3 3684 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ ℝ β†’ (π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ } ↔ seq0( + , (πΊβ€˜π‘₯)) ∈ dom ⇝ ))
224219, 223syl 17 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (ℝ βˆ– {0}) β†’ (π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ } ↔ seq0( + , (πΊβ€˜π‘₯)) ∈ dom ⇝ ))
225224ad2antlr 725 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘₯ ∈ (ℝ βˆ– {0})) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) β†’ (π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ } ↔ seq0( + , (πΊβ€˜π‘₯)) ∈ dom ⇝ ))
226218, 225bitr4d 281 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘₯ ∈ (ℝ βˆ– {0})) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) β†’ (((absβ€˜π‘₯) Β· 𝐿) < 1 ↔ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
227226an32s 650 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) ∧ π‘₯ ∈ (ℝ βˆ– {0})) β†’ (((absβ€˜π‘₯) Β· 𝐿) < 1 ↔ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
228105, 227jaodan 956 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) ∧ (π‘₯ ∈ (ℝ ∩ {0}) ∨ π‘₯ ∈ (ℝ βˆ– {0}))) β†’ (((absβ€˜π‘₯) Β· 𝐿) < 1 ↔ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
22985, 228sylan2br 595 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) ∧ π‘₯ ∈ ℝ) β†’ (((absβ€˜π‘₯) Β· 𝐿) < 1 ↔ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
230229an32s 650 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) β†’ (((absβ€˜π‘₯) Β· 𝐿) < 1 ↔ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
23181, 230bitr3d 280 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ ((absβ€˜π‘₯) Β· 𝐿) β‰  1) β†’ ((absβ€˜π‘₯) < (1 / 𝐿) ↔ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
23268, 231syldan 591 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿)) β†’ ((absβ€˜π‘₯) < (1 / 𝐿) ↔ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
233232notbid 317 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿)) β†’ (Β¬ (absβ€˜π‘₯) < (1 / 𝐿) ↔ Β¬ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
23457, 233bitrd 278 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿)) β†’ ((1 / 𝐿) < (absβ€˜π‘₯) ↔ Β¬ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
235234biimpd 228 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿)) β†’ ((1 / 𝐿) < (absβ€˜π‘₯) β†’ Β¬ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
236235impancom 452 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (1 / 𝐿) < (absβ€˜π‘₯)) β†’ ((absβ€˜π‘₯) β‰  (1 / 𝐿) β†’ Β¬ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
23751, 236mpd 15 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (1 / 𝐿) < (absβ€˜π‘₯)) β†’ Β¬ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ })
238237ex 413 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((1 / 𝐿) < (absβ€˜π‘₯) β†’ Β¬ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
239238con2d 134 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ } β†’ Β¬ (1 / 𝐿) < (absβ€˜π‘₯)))
24046adantr 481 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (1 / 𝐿) < π‘₯) β†’ (1 / 𝐿) ∈ ℝ)
241 simplr 767 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (1 / 𝐿) < π‘₯) β†’ π‘₯ ∈ ℝ)
24249adantr 481 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (1 / 𝐿) < π‘₯) β†’ (absβ€˜π‘₯) ∈ ℝ)
243 simpr 485 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (1 / 𝐿) < π‘₯) β†’ (1 / 𝐿) < π‘₯)
244241leabsd 15363 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (1 / 𝐿) < π‘₯) β†’ π‘₯ ≀ (absβ€˜π‘₯))
245240, 241, 242, 243, 244ltletrd 11376 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (1 / 𝐿) < π‘₯) β†’ (1 / 𝐿) < (absβ€˜π‘₯))
246245ex 413 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((1 / 𝐿) < π‘₯ β†’ (1 / 𝐿) < (absβ€˜π‘₯)))
247239, 246nsyld 156 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ } β†’ Β¬ (1 / 𝐿) < π‘₯))
24845, 247sylan2 593 . . . 4 ((πœ‘ ∧ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }) β†’ (π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ } β†’ Β¬ (1 / 𝐿) < π‘₯))
24944, 248mpd 15 . . 3 ((πœ‘ ∧ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }) β†’ Β¬ (1 / 𝐿) < π‘₯)
25042renegcld 11643 . . . . . . . . 9 (πœ‘ β†’ -(1 / 𝐿) ∈ ℝ)
251250rexrd 11266 . . . . . . . 8 (πœ‘ β†’ -(1 / 𝐿) ∈ ℝ*)
252 iooss1 13361 . . . . . . . 8 ((-(1 / 𝐿) ∈ ℝ* ∧ -(1 / 𝐿) ≀ π‘₯) β†’ (π‘₯(,)(1 / 𝐿)) βŠ† (-(1 / 𝐿)(,)(1 / 𝐿)))
253251, 252sylan 580 . . . . . . 7 ((πœ‘ ∧ -(1 / 𝐿) ≀ π‘₯) β†’ (π‘₯(,)(1 / 𝐿)) βŠ† (-(1 / 𝐿)(,)(1 / 𝐿)))
254253adantlr 713 . . . . . 6 (((πœ‘ ∧ (π‘₯ ∈ ℝ* ∧ π‘₯ < (1 / 𝐿))) ∧ -(1 / 𝐿) ≀ π‘₯) β†’ (π‘₯(,)(1 / 𝐿)) βŠ† (-(1 / 𝐿)(,)(1 / 𝐿)))
255 eliooord 13385 . . . . . . . . . . 11 (π‘˜ ∈ (π‘₯(,)(1 / 𝐿)) β†’ (π‘₯ < π‘˜ ∧ π‘˜ < (1 / 𝐿)))
256255simpld 495 . . . . . . . . . 10 (π‘˜ ∈ (π‘₯(,)(1 / 𝐿)) β†’ π‘₯ < π‘˜)
257256rgen 3063 . . . . . . . . 9 βˆ€π‘˜ ∈ (π‘₯(,)(1 / 𝐿))π‘₯ < π‘˜
258 ioon0 13352 . . . . . . . . . . . . 13 ((π‘₯ ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) β†’ ((π‘₯(,)(1 / 𝐿)) β‰  βˆ… ↔ π‘₯ < (1 / 𝐿)))
25943, 258sylan2 593 . . . . . . . . . . . 12 ((π‘₯ ∈ ℝ* ∧ πœ‘) β†’ ((π‘₯(,)(1 / 𝐿)) β‰  βˆ… ↔ π‘₯ < (1 / 𝐿)))
260259ancoms 459 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ℝ*) β†’ ((π‘₯(,)(1 / 𝐿)) β‰  βˆ… ↔ π‘₯ < (1 / 𝐿)))
261260biimpar 478 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ*) ∧ π‘₯ < (1 / 𝐿)) β†’ (π‘₯(,)(1 / 𝐿)) β‰  βˆ…)
262 r19.2zb 4495 . . . . . . . . . 10 ((π‘₯(,)(1 / 𝐿)) β‰  βˆ… ↔ (βˆ€π‘˜ ∈ (π‘₯(,)(1 / 𝐿))π‘₯ < π‘˜ β†’ βˆƒπ‘˜ ∈ (π‘₯(,)(1 / 𝐿))π‘₯ < π‘˜))
263261, 262sylib 217 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ ℝ*) ∧ π‘₯ < (1 / 𝐿)) β†’ (βˆ€π‘˜ ∈ (π‘₯(,)(1 / 𝐿))π‘₯ < π‘˜ β†’ βˆƒπ‘˜ ∈ (π‘₯(,)(1 / 𝐿))π‘₯ < π‘˜))
264257, 263mpi 20 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ℝ*) ∧ π‘₯ < (1 / 𝐿)) β†’ βˆƒπ‘˜ ∈ (π‘₯(,)(1 / 𝐿))π‘₯ < π‘˜)
265264anasss 467 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ ℝ* ∧ π‘₯ < (1 / 𝐿))) β†’ βˆƒπ‘˜ ∈ (π‘₯(,)(1 / 𝐿))π‘₯ < π‘˜)
266265adantr 481 . . . . . 6 (((πœ‘ ∧ (π‘₯ ∈ ℝ* ∧ π‘₯ < (1 / 𝐿))) ∧ -(1 / 𝐿) ≀ π‘₯) β†’ βˆƒπ‘˜ ∈ (π‘₯(,)(1 / 𝐿))π‘₯ < π‘˜)
267 ssrexv 4051 . . . . . 6 ((π‘₯(,)(1 / 𝐿)) βŠ† (-(1 / 𝐿)(,)(1 / 𝐿)) β†’ (βˆƒπ‘˜ ∈ (π‘₯(,)(1 / 𝐿))π‘₯ < π‘˜ β†’ βˆƒπ‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜))
268254, 266, 267sylc 65 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ ℝ* ∧ π‘₯ < (1 / 𝐿))) ∧ -(1 / 𝐿) ≀ π‘₯) β†’ βˆƒπ‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜)
269 simplr 767 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ*) ∧ Β¬ -(1 / 𝐿) ≀ π‘₯) β†’ π‘₯ ∈ ℝ*)
270 xrltnle 11283 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) β†’ (π‘₯ < -(1 / 𝐿) ↔ Β¬ -(1 / 𝐿) ≀ π‘₯))
271 xrltle 13130 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) β†’ (π‘₯ < -(1 / 𝐿) β†’ π‘₯ ≀ -(1 / 𝐿)))
272270, 271sylbird 259 . . . . . . . . . . . . . 14 ((π‘₯ ∈ ℝ* ∧ -(1 / 𝐿) ∈ ℝ*) β†’ (Β¬ -(1 / 𝐿) ≀ π‘₯ β†’ π‘₯ ≀ -(1 / 𝐿)))
273251, 272sylan2 593 . . . . . . . . . . . . 13 ((π‘₯ ∈ ℝ* ∧ πœ‘) β†’ (Β¬ -(1 / 𝐿) ≀ π‘₯ β†’ π‘₯ ≀ -(1 / 𝐿)))
274273ancoms 459 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ ℝ*) β†’ (Β¬ -(1 / 𝐿) ≀ π‘₯ β†’ π‘₯ ≀ -(1 / 𝐿)))
275274imp 407 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ*) ∧ Β¬ -(1 / 𝐿) ≀ π‘₯) β†’ π‘₯ ≀ -(1 / 𝐿))
276 iooss1 13361 . . . . . . . . . . 11 ((π‘₯ ∈ ℝ* ∧ π‘₯ ≀ -(1 / 𝐿)) β†’ (-(1 / 𝐿)(,)(1 / 𝐿)) βŠ† (π‘₯(,)(1 / 𝐿)))
277269, 275, 276syl2anc 584 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ*) ∧ Β¬ -(1 / 𝐿) ≀ π‘₯) β†’ (-(1 / 𝐿)(,)(1 / 𝐿)) βŠ† (π‘₯(,)(1 / 𝐿)))
278277sselda 3982 . . . . . . . . 9 ((((πœ‘ ∧ π‘₯ ∈ ℝ*) ∧ Β¬ -(1 / 𝐿) ≀ π‘₯) ∧ π‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) β†’ π‘˜ ∈ (π‘₯(,)(1 / 𝐿)))
279278, 256syl 17 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ ℝ*) ∧ Β¬ -(1 / 𝐿) ≀ π‘₯) ∧ π‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) β†’ π‘₯ < π‘˜)
280279ralrimiva 3146 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ ℝ*) ∧ Β¬ -(1 / 𝐿) ≀ π‘₯) β†’ βˆ€π‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜)
28140, 77recgt0d 12150 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < (1 / 𝐿))
28242, 42, 281, 281addgt0d 11791 . . . . . . . . . . . 12 (πœ‘ β†’ 0 < ((1 / 𝐿) + (1 / 𝐿)))
28342recnd 11244 . . . . . . . . . . . . 13 (πœ‘ β†’ (1 / 𝐿) ∈ β„‚)
284283, 283subnegd 11580 . . . . . . . . . . . 12 (πœ‘ β†’ ((1 / 𝐿) βˆ’ -(1 / 𝐿)) = ((1 / 𝐿) + (1 / 𝐿)))
285282, 284breqtrrd 5176 . . . . . . . . . . 11 (πœ‘ β†’ 0 < ((1 / 𝐿) βˆ’ -(1 / 𝐿)))
286250, 42posdifd 11803 . . . . . . . . . . 11 (πœ‘ β†’ (-(1 / 𝐿) < (1 / 𝐿) ↔ 0 < ((1 / 𝐿) βˆ’ -(1 / 𝐿))))
287285, 286mpbird 256 . . . . . . . . . 10 (πœ‘ β†’ -(1 / 𝐿) < (1 / 𝐿))
288 ioon0 13352 . . . . . . . . . . 11 ((-(1 / 𝐿) ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) β†’ ((-(1 / 𝐿)(,)(1 / 𝐿)) β‰  βˆ… ↔ -(1 / 𝐿) < (1 / 𝐿)))
289251, 43, 288syl2anc 584 . . . . . . . . . 10 (πœ‘ β†’ ((-(1 / 𝐿)(,)(1 / 𝐿)) β‰  βˆ… ↔ -(1 / 𝐿) < (1 / 𝐿)))
290287, 289mpbird 256 . . . . . . . . 9 (πœ‘ β†’ (-(1 / 𝐿)(,)(1 / 𝐿)) β‰  βˆ…)
291 r19.2zb 4495 . . . . . . . . 9 ((-(1 / 𝐿)(,)(1 / 𝐿)) β‰  βˆ… ↔ (βˆ€π‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜ β†’ βˆƒπ‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜))
292290, 291sylib 217 . . . . . . . 8 (πœ‘ β†’ (βˆ€π‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜ β†’ βˆƒπ‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜))
293292ad2antrr 724 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ ℝ*) ∧ Β¬ -(1 / 𝐿) ≀ π‘₯) β†’ (βˆ€π‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜ β†’ βˆƒπ‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜))
294280, 293mpd 15 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ ℝ*) ∧ Β¬ -(1 / 𝐿) ≀ π‘₯) β†’ βˆƒπ‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜)
295294adantlrr 719 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ ℝ* ∧ π‘₯ < (1 / 𝐿))) ∧ Β¬ -(1 / 𝐿) ≀ π‘₯) β†’ βˆƒπ‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜)
296268, 295pm2.61dan 811 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ ℝ* ∧ π‘₯ < (1 / 𝐿))) β†’ βˆƒπ‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜)
297 elioo2 13367 . . . . . . . . . . 11 ((-(1 / 𝐿) ∈ ℝ* ∧ (1 / 𝐿) ∈ ℝ*) β†’ (π‘₯ ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) ↔ (π‘₯ ∈ ℝ ∧ -(1 / 𝐿) < π‘₯ ∧ π‘₯ < (1 / 𝐿))))
298251, 43, 297syl2anc 584 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) ↔ (π‘₯ ∈ ℝ ∧ -(1 / 𝐿) < π‘₯ ∧ π‘₯ < (1 / 𝐿))))
299298biimpa 477 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) β†’ (π‘₯ ∈ ℝ ∧ -(1 / 𝐿) < π‘₯ ∧ π‘₯ < (1 / 𝐿)))
300 simpr 485 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ π‘₯ ∈ ℝ)
301300, 46absltd 15378 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((absβ€˜π‘₯) < (1 / 𝐿) ↔ (-(1 / 𝐿) < π‘₯ ∧ π‘₯ < (1 / 𝐿))))
30249adantr 481 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) < (1 / 𝐿)) β†’ (absβ€˜π‘₯) ∈ ℝ)
303 simpr 485 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) < (1 / 𝐿)) β†’ (absβ€˜π‘₯) < (1 / 𝐿))
304302, 303ltned 11352 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) < (1 / 𝐿)) β†’ (absβ€˜π‘₯) β‰  (1 / 𝐿))
305232biimpd 228 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) β‰  (1 / 𝐿)) β†’ ((absβ€˜π‘₯) < (1 / 𝐿) β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
306305impancom 452 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) < (1 / 𝐿)) β†’ ((absβ€˜π‘₯) β‰  (1 / 𝐿) β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
307304, 306mpd 15 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ (absβ€˜π‘₯) < (1 / 𝐿)) β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ })
308307ex 413 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((absβ€˜π‘₯) < (1 / 𝐿) β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
309301, 308sylbird 259 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((-(1 / 𝐿) < π‘₯ ∧ π‘₯ < (1 / 𝐿)) β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
310309impr 455 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ ℝ ∧ (-(1 / 𝐿) < π‘₯ ∧ π‘₯ < (1 / 𝐿)))) β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ })
311310expcom 414 . . . . . . . . . . 11 ((π‘₯ ∈ ℝ ∧ (-(1 / 𝐿) < π‘₯ ∧ π‘₯ < (1 / 𝐿))) β†’ (πœ‘ β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
3123113impb 1115 . . . . . . . . . 10 ((π‘₯ ∈ ℝ ∧ -(1 / 𝐿) < π‘₯ ∧ π‘₯ < (1 / 𝐿)) β†’ (πœ‘ β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
313312impcom 408 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ ℝ ∧ -(1 / 𝐿) < π‘₯ ∧ π‘₯ < (1 / 𝐿))) β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ })
314299, 313syldan 591 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ })
315314ex 413 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) β†’ π‘₯ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }))
316315ssrdv 3988 . . . . . 6 (πœ‘ β†’ (-(1 / 𝐿)(,)(1 / 𝐿)) βŠ† {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ })
317 ssrexv 4051 . . . . . 6 ((-(1 / 𝐿)(,)(1 / 𝐿)) βŠ† {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ } β†’ (βˆƒπ‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜ β†’ βˆƒπ‘˜ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }π‘₯ < π‘˜))
318316, 317syl 17 . . . . 5 (πœ‘ β†’ (βˆƒπ‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜ β†’ βˆƒπ‘˜ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }π‘₯ < π‘˜))
319318adantr 481 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ ℝ* ∧ π‘₯ < (1 / 𝐿))) β†’ (βˆƒπ‘˜ ∈ (-(1 / 𝐿)(,)(1 / 𝐿))π‘₯ < π‘˜ β†’ βˆƒπ‘˜ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }π‘₯ < π‘˜))
320296, 319mpd 15 . . 3 ((πœ‘ ∧ (π‘₯ ∈ ℝ* ∧ π‘₯ < (1 / 𝐿))) β†’ βˆƒπ‘˜ ∈ {π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }π‘₯ < π‘˜)
3213, 43, 249, 320eqsupd 9454 . 2 (πœ‘ β†’ sup({π‘Ÿ ∈ ℝ ∣ seq0( + , (πΊβ€˜π‘Ÿ)) ∈ dom ⇝ }, ℝ*, < ) = (1 / 𝐿))
3221, 321eqtrid 2784 1 (πœ‘ β†’ 𝑅 = (1 / 𝐿))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432  Vcvv 3474   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  {csn 4628   class class class wbr 5148   ↦ cmpt 5231   Or wor 5587  dom cdm 5676   β†Ύ cres 5678  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411  supcsup 9437  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117  β„*cxr 11249   < clt 11250   ≀ cle 11251   βˆ’ cmin 11446  -cneg 11447   / cdiv 11873  β„•0cn0 12474  β„€cz 12560  β„€β‰₯cuz 12824  β„+crp 12976  (,)cioo 13326  seqcseq 13968  β†‘cexp 14029  abscabs 15183   ⇝ cli 15430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-z 12561  df-uz 12825  df-q 12935  df-rp 12977  df-ioo 13330  df-ico 13332  df-fz 13487  df-fzo 13630  df-fl 13759  df-seq 13969  df-exp 14030  df-hash 14293  df-shft 15016  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-limsup 15417  df-clim 15434  df-rlim 15435  df-sum 15635
This theorem is referenced by:  binomcxplemradcnv  43193
  Copyright terms: Public domain W3C validator