Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  climinfmpt Structured version   Visualization version   GIF version

Theorem climinfmpt 44882
Description: A bounded below, monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypotheses
Ref Expression
climinfmpt.p 𝑘𝜑
climinfmpt.j 𝑗𝜑
climinfmpt.m (𝜑𝑀 ∈ ℤ)
climinfmpt.z 𝑍 = (ℤ𝑀)
climinfmpt.b ((𝜑𝑘𝑍) → 𝐵 ∈ ℝ)
climinfmpt.c (𝑘 = 𝑗𝐵 = 𝐶)
climinfmpt.l ((𝜑𝑘𝑍𝑗 = (𝑘 + 1)) → 𝐶𝐵)
climinfmpt.e (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘𝑍 𝑥𝐵)
Assertion
Ref Expression
climinfmpt (𝜑 → (𝑘𝑍𝐵) ⇝ inf(ran (𝑘𝑍𝐵), ℝ*, < ))
Distinct variable groups:   𝐵,𝑗   𝑥,𝐵   𝐶,𝑘   𝑗,𝑍,𝑘   𝑥,𝑍,𝑘
Allowed substitution hints:   𝜑(𝑥,𝑗,𝑘)   𝐵(𝑘)   𝐶(𝑥,𝑗)   𝑀(𝑥,𝑗,𝑘)

Proof of Theorem climinfmpt
Dummy variables 𝑖 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1909 . 2 𝑖𝜑
2 nfcv 2895 . 2 𝑖(𝑘𝑍𝐵)
3 climinfmpt.z . 2 𝑍 = (ℤ𝑀)
4 climinfmpt.m . 2 (𝜑𝑀 ∈ ℤ)
5 climinfmpt.p . . 3 𝑘𝜑
6 climinfmpt.b . . 3 ((𝜑𝑘𝑍) → 𝐵 ∈ ℝ)
75, 6fmptd2f 44388 . 2 (𝜑 → (𝑘𝑍𝐵):𝑍⟶ℝ)
8 nfv 1909 . . . . . . 7 𝑘 𝑖𝑍
95, 8nfan 1894 . . . . . 6 𝑘(𝜑𝑖𝑍)
10 nfv 1909 . . . . . 6 𝑘(𝑖 + 1) / 𝑗𝐶𝑖 / 𝑗𝐶
119, 10nfim 1891 . . . . 5 𝑘((𝜑𝑖𝑍) → (𝑖 + 1) / 𝑗𝐶𝑖 / 𝑗𝐶)
12 eleq1 2813 . . . . . . 7 (𝑘 = 𝑖 → (𝑘𝑍𝑖𝑍))
1312anbi2d 628 . . . . . 6 (𝑘 = 𝑖 → ((𝜑𝑘𝑍) ↔ (𝜑𝑖𝑍)))
14 oveq1 7408 . . . . . . . 8 (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1))
1514csbeq1d 3889 . . . . . . 7 (𝑘 = 𝑖(𝑘 + 1) / 𝑗𝐶 = (𝑖 + 1) / 𝑗𝐶)
16 eqidd 2725 . . . . . . . 8 (𝑘 = 𝑖𝐵 = 𝐵)
17 csbcow 3900 . . . . . . . . . . 11 𝑘 / 𝑗𝑗 / 𝑘𝐵 = 𝑘 / 𝑘𝐵
18 csbid 3898 . . . . . . . . . . 11 𝑘 / 𝑘𝐵 = 𝐵
1917, 18eqtr2i 2753 . . . . . . . . . 10 𝐵 = 𝑘 / 𝑗𝑗 / 𝑘𝐵
20 nfcv 2895 . . . . . . . . . . . . 13 𝑗𝐵
21 nfcv 2895 . . . . . . . . . . . . 13 𝑘𝐶
22 climinfmpt.c . . . . . . . . . . . . 13 (𝑘 = 𝑗𝐵 = 𝐶)
2320, 21, 22cbvcsbw 3895 . . . . . . . . . . . 12 𝑗 / 𝑘𝐵 = 𝑗 / 𝑗𝐶
24 csbid 3898 . . . . . . . . . . . 12 𝑗 / 𝑗𝐶 = 𝐶
2523, 24eqtri 2752 . . . . . . . . . . 11 𝑗 / 𝑘𝐵 = 𝐶
2625csbeq2i 3893 . . . . . . . . . 10 𝑘 / 𝑗𝑗 / 𝑘𝐵 = 𝑘 / 𝑗𝐶
2719, 26eqtri 2752 . . . . . . . . 9 𝐵 = 𝑘 / 𝑗𝐶
2827a1i 11 . . . . . . . 8 (𝑘 = 𝑖𝐵 = 𝑘 / 𝑗𝐶)
29 csbeq1 3888 . . . . . . . 8 (𝑘 = 𝑖𝑘 / 𝑗𝐶 = 𝑖 / 𝑗𝐶)
3016, 28, 293eqtrd 2768 . . . . . . 7 (𝑘 = 𝑖𝐵 = 𝑖 / 𝑗𝐶)
3115, 30breq12d 5151 . . . . . 6 (𝑘 = 𝑖 → ((𝑘 + 1) / 𝑗𝐶𝐵(𝑖 + 1) / 𝑗𝐶𝑖 / 𝑗𝐶))
3213, 31imbi12d 344 . . . . 5 (𝑘 = 𝑖 → (((𝜑𝑘𝑍) → (𝑘 + 1) / 𝑗𝐶𝐵) ↔ ((𝜑𝑖𝑍) → (𝑖 + 1) / 𝑗𝐶𝑖 / 𝑗𝐶)))
33 simpl 482 . . . . . 6 ((𝜑𝑘𝑍) → 𝜑)
34 simpr 484 . . . . . 6 ((𝜑𝑘𝑍) → 𝑘𝑍)
35 eqidd 2725 . . . . . 6 ((𝜑𝑘𝑍) → (𝑘 + 1) = (𝑘 + 1))
36 climinfmpt.j . . . . . . . . 9 𝑗𝜑
37 nfv 1909 . . . . . . . . 9 𝑗 𝑘𝑍
38 nfv 1909 . . . . . . . . 9 𝑗(𝑘 + 1) = (𝑘 + 1)
3936, 37, 38nf3an 1896 . . . . . . . 8 𝑗(𝜑𝑘𝑍 ∧ (𝑘 + 1) = (𝑘 + 1))
40 nfcsb1v 3910 . . . . . . . . 9 𝑗(𝑘 + 1) / 𝑗𝐶
41 nfcv 2895 . . . . . . . . 9 𝑗
4240, 41, 20nfbr 5185 . . . . . . . 8 𝑗(𝑘 + 1) / 𝑗𝐶𝐵
4339, 42nfim 1891 . . . . . . 7 𝑗((𝜑𝑘𝑍 ∧ (𝑘 + 1) = (𝑘 + 1)) → (𝑘 + 1) / 𝑗𝐶𝐵)
44 ovex 7434 . . . . . . 7 (𝑘 + 1) ∈ V
45 eqeq1 2728 . . . . . . . . 9 (𝑗 = (𝑘 + 1) → (𝑗 = (𝑘 + 1) ↔ (𝑘 + 1) = (𝑘 + 1)))
46453anbi3d 1438 . . . . . . . 8 (𝑗 = (𝑘 + 1) → ((𝜑𝑘𝑍𝑗 = (𝑘 + 1)) ↔ (𝜑𝑘𝑍 ∧ (𝑘 + 1) = (𝑘 + 1))))
47 csbeq1a 3899 . . . . . . . . 9 (𝑗 = (𝑘 + 1) → 𝐶 = (𝑘 + 1) / 𝑗𝐶)
4847breq1d 5148 . . . . . . . 8 (𝑗 = (𝑘 + 1) → (𝐶𝐵(𝑘 + 1) / 𝑗𝐶𝐵))
4946, 48imbi12d 344 . . . . . . 7 (𝑗 = (𝑘 + 1) → (((𝜑𝑘𝑍𝑗 = (𝑘 + 1)) → 𝐶𝐵) ↔ ((𝜑𝑘𝑍 ∧ (𝑘 + 1) = (𝑘 + 1)) → (𝑘 + 1) / 𝑗𝐶𝐵)))
50 climinfmpt.l . . . . . . 7 ((𝜑𝑘𝑍𝑗 = (𝑘 + 1)) → 𝐶𝐵)
5143, 44, 49, 50vtoclf 3544 . . . . . 6 ((𝜑𝑘𝑍 ∧ (𝑘 + 1) = (𝑘 + 1)) → (𝑘 + 1) / 𝑗𝐶𝐵)
5233, 34, 35, 51syl3anc 1368 . . . . 5 ((𝜑𝑘𝑍) → (𝑘 + 1) / 𝑗𝐶𝐵)
5311, 32, 52chvarfv 2225 . . . 4 ((𝜑𝑖𝑍) → (𝑖 + 1) / 𝑗𝐶𝑖 / 𝑗𝐶)
5420, 21, 22cbvcsbw 3895 . . . . . 6 (𝑖 + 1) / 𝑘𝐵 = (𝑖 + 1) / 𝑗𝐶
5554a1i 11 . . . . 5 ((𝜑𝑖𝑍) → (𝑖 + 1) / 𝑘𝐵 = (𝑖 + 1) / 𝑗𝐶)
56 eqidd 2725 . . . . 5 ((𝜑𝑖𝑍) → 𝑖 / 𝑗𝐶 = 𝑖 / 𝑗𝐶)
5755, 56breq12d 5151 . . . 4 ((𝜑𝑖𝑍) → ((𝑖 + 1) / 𝑘𝐵𝑖 / 𝑗𝐶(𝑖 + 1) / 𝑗𝐶𝑖 / 𝑗𝐶))
5853, 57mpbird 257 . . 3 ((𝜑𝑖𝑍) → (𝑖 + 1) / 𝑘𝐵𝑖 / 𝑗𝐶)
593peano2uzs 12882 . . . . . 6 (𝑖𝑍 → (𝑖 + 1) ∈ 𝑍)
6059adantl 481 . . . . 5 ((𝜑𝑖𝑍) → (𝑖 + 1) ∈ 𝑍)
61 nfv 1909 . . . . . . . . 9 𝑘(𝑖 + 1) ∈ 𝑍
625, 61nfan 1894 . . . . . . . 8 𝑘(𝜑 ∧ (𝑖 + 1) ∈ 𝑍)
63 nfcv 2895 . . . . . . . . . 10 𝑘(𝑖 + 1)
6463nfcsb1 3909 . . . . . . . . 9 𝑘(𝑖 + 1) / 𝑘𝐵
6564nfel1 2911 . . . . . . . 8 𝑘(𝑖 + 1) / 𝑘𝐵 ∈ ℝ
6662, 65nfim 1891 . . . . . . 7 𝑘((𝜑 ∧ (𝑖 + 1) ∈ 𝑍) → (𝑖 + 1) / 𝑘𝐵 ∈ ℝ)
67 ovex 7434 . . . . . . 7 (𝑖 + 1) ∈ V
68 eleq1 2813 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → (𝑘𝑍 ↔ (𝑖 + 1) ∈ 𝑍))
6968anbi2d 628 . . . . . . . 8 (𝑘 = (𝑖 + 1) → ((𝜑𝑘𝑍) ↔ (𝜑 ∧ (𝑖 + 1) ∈ 𝑍)))
70 csbeq1a 3899 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → 𝐵 = (𝑖 + 1) / 𝑘𝐵)
7170eleq1d 2810 . . . . . . . 8 (𝑘 = (𝑖 + 1) → (𝐵 ∈ ℝ ↔ (𝑖 + 1) / 𝑘𝐵 ∈ ℝ))
7269, 71imbi12d 344 . . . . . . 7 (𝑘 = (𝑖 + 1) → (((𝜑𝑘𝑍) → 𝐵 ∈ ℝ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ 𝑍) → (𝑖 + 1) / 𝑘𝐵 ∈ ℝ)))
7366, 67, 72, 6vtoclf 3544 . . . . . 6 ((𝜑 ∧ (𝑖 + 1) ∈ 𝑍) → (𝑖 + 1) / 𝑘𝐵 ∈ ℝ)
7459, 73sylan2 592 . . . . 5 ((𝜑𝑖𝑍) → (𝑖 + 1) / 𝑘𝐵 ∈ ℝ)
75 eqid 2724 . . . . . 6 (𝑘𝑍𝐵) = (𝑘𝑍𝐵)
7663, 64, 70, 75fvmptf 7009 . . . . 5 (((𝑖 + 1) ∈ 𝑍(𝑖 + 1) / 𝑘𝐵 ∈ ℝ) → ((𝑘𝑍𝐵)‘(𝑖 + 1)) = (𝑖 + 1) / 𝑘𝐵)
7760, 74, 76syl2anc 583 . . . 4 ((𝜑𝑖𝑍) → ((𝑘𝑍𝐵)‘(𝑖 + 1)) = (𝑖 + 1) / 𝑘𝐵)
78 simpr 484 . . . . 5 ((𝜑𝑖𝑍) → 𝑖𝑍)
79 nfv 1909 . . . . . . . 8 𝑗 𝑖𝑍
8036, 79nfan 1894 . . . . . . 7 𝑗(𝜑𝑖𝑍)
81 nfcsb1v 3910 . . . . . . . 8 𝑗𝑖 / 𝑗𝐶
82 nfcv 2895 . . . . . . . 8 𝑗
8381, 82nfel 2909 . . . . . . 7 𝑗𝑖 / 𝑗𝐶 ∈ ℝ
8480, 83nfim 1891 . . . . . 6 𝑗((𝜑𝑖𝑍) → 𝑖 / 𝑗𝐶 ∈ ℝ)
85 eleq1 2813 . . . . . . . 8 (𝑗 = 𝑖 → (𝑗𝑍𝑖𝑍))
8685anbi2d 628 . . . . . . 7 (𝑗 = 𝑖 → ((𝜑𝑗𝑍) ↔ (𝜑𝑖𝑍)))
87 csbeq1a 3899 . . . . . . . 8 (𝑗 = 𝑖𝐶 = 𝑖 / 𝑗𝐶)
8887eleq1d 2810 . . . . . . 7 (𝑗 = 𝑖 → (𝐶 ∈ ℝ ↔ 𝑖 / 𝑗𝐶 ∈ ℝ))
8986, 88imbi12d 344 . . . . . 6 (𝑗 = 𝑖 → (((𝜑𝑗𝑍) → 𝐶 ∈ ℝ) ↔ ((𝜑𝑖𝑍) → 𝑖 / 𝑗𝐶 ∈ ℝ)))
90 nfv 1909 . . . . . . . . 9 𝑘 𝑗𝑍
915, 90nfan 1894 . . . . . . . 8 𝑘(𝜑𝑗𝑍)
92 nfv 1909 . . . . . . . 8 𝑘 𝐶 ∈ ℝ
9391, 92nfim 1891 . . . . . . 7 𝑘((𝜑𝑗𝑍) → 𝐶 ∈ ℝ)
94 eleq1 2813 . . . . . . . . 9 (𝑘 = 𝑗 → (𝑘𝑍𝑗𝑍))
9594anbi2d 628 . . . . . . . 8 (𝑘 = 𝑗 → ((𝜑𝑘𝑍) ↔ (𝜑𝑗𝑍)))
9622eleq1d 2810 . . . . . . . 8 (𝑘 = 𝑗 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ))
9795, 96imbi12d 344 . . . . . . 7 (𝑘 = 𝑗 → (((𝜑𝑘𝑍) → 𝐵 ∈ ℝ) ↔ ((𝜑𝑗𝑍) → 𝐶 ∈ ℝ)))
9893, 97, 6chvarfv 2225 . . . . . 6 ((𝜑𝑗𝑍) → 𝐶 ∈ ℝ)
9984, 89, 98chvarfv 2225 . . . . 5 ((𝜑𝑖𝑍) → 𝑖 / 𝑗𝐶 ∈ ℝ)
100 nfcv 2895 . . . . . 6 𝑘𝑖
101 nfcv 2895 . . . . . 6 𝑘𝑖 / 𝑗𝐶
102100, 101, 30, 75fvmptf 7009 . . . . 5 ((𝑖𝑍𝑖 / 𝑗𝐶 ∈ ℝ) → ((𝑘𝑍𝐵)‘𝑖) = 𝑖 / 𝑗𝐶)
10378, 99, 102syl2anc 583 . . . 4 ((𝜑𝑖𝑍) → ((𝑘𝑍𝐵)‘𝑖) = 𝑖 / 𝑗𝐶)
10477, 103breq12d 5151 . . 3 ((𝜑𝑖𝑍) → (((𝑘𝑍𝐵)‘(𝑖 + 1)) ≤ ((𝑘𝑍𝐵)‘𝑖) ↔ (𝑖 + 1) / 𝑘𝐵𝑖 / 𝑗𝐶))
10558, 104mpbird 257 . 2 ((𝜑𝑖𝑍) → ((𝑘𝑍𝐵)‘(𝑖 + 1)) ≤ ((𝑘𝑍𝐵)‘𝑖))
106 climinfmpt.e . . . 4 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘𝑍 𝑥𝐵)
107 breq1 5141 . . . . . 6 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
108107ralbidv 3169 . . . . 5 (𝑥 = 𝑦 → (∀𝑘𝑍 𝑥𝐵 ↔ ∀𝑘𝑍 𝑦𝐵))
109108cbvrexvw 3227 . . . 4 (∃𝑥 ∈ ℝ ∀𝑘𝑍 𝑥𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑘𝑍 𝑦𝐵)
110106, 109sylib 217 . . 3 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑘𝑍 𝑦𝐵)
111 nfcv 2895 . . . . . . . 8 𝑘𝑦
112 nfcv 2895 . . . . . . . 8 𝑘
113 nfmpt1 5246 . . . . . . . . 9 𝑘(𝑘𝑍𝐵)
114113, 100nffv 6891 . . . . . . . 8 𝑘((𝑘𝑍𝐵)‘𝑖)
115111, 112, 114nfbr 5185 . . . . . . 7 𝑘 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖)
116 nfv 1909 . . . . . . 7 𝑖 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑘)
117 fveq2 6881 . . . . . . . 8 (𝑖 = 𝑘 → ((𝑘𝑍𝐵)‘𝑖) = ((𝑘𝑍𝐵)‘𝑘))
118117breq2d 5150 . . . . . . 7 (𝑖 = 𝑘 → (𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖) ↔ 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑘)))
119115, 116, 118cbvralw 3295 . . . . . 6 (∀𝑖𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖) ↔ ∀𝑘𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑘))
120119a1i 11 . . . . 5 (𝜑 → (∀𝑖𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖) ↔ ∀𝑘𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑘)))
12175a1i 11 . . . . . . . 8 (𝜑 → (𝑘𝑍𝐵) = (𝑘𝑍𝐵))
122121, 6fvmpt2d 7001 . . . . . . 7 ((𝜑𝑘𝑍) → ((𝑘𝑍𝐵)‘𝑘) = 𝐵)
123122breq2d 5150 . . . . . 6 ((𝜑𝑘𝑍) → (𝑦 ≤ ((𝑘𝑍𝐵)‘𝑘) ↔ 𝑦𝐵))
1245, 123ralbida 3259 . . . . 5 (𝜑 → (∀𝑘𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑘) ↔ ∀𝑘𝑍 𝑦𝐵))
125120, 124bitrd 279 . . . 4 (𝜑 → (∀𝑖𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖) ↔ ∀𝑘𝑍 𝑦𝐵))
126125rexbidv 3170 . . 3 (𝜑 → (∃𝑦 ∈ ℝ ∀𝑖𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖) ↔ ∃𝑦 ∈ ℝ ∀𝑘𝑍 𝑦𝐵))
127110, 126mpbird 257 . 2 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑖𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖))
1281, 2, 3, 4, 7, 105, 127climinf2 44874 1 (𝜑 → (𝑘𝑍𝐵) ⇝ inf(ran (𝑘𝑍𝐵), ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wnf 1777  wcel 2098  wral 3053  wrex 3062  csb 3885   class class class wbr 5138  cmpt 5221  ran crn 5667  cfv 6533  (class class class)co 7401  infcinf 9431  cr 11104  1c1 11106   + caddc 11108  *cxr 11243   < clt 11244  cle 11245  cz 12554  cuz 12818  cli 15424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182  ax-pre-sup 11183
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-er 8698  df-en 8935  df-dom 8936  df-sdom 8937  df-sup 9432  df-inf 9433  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-fz 13481  df-seq 13963  df-exp 14024  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator