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

Theorem climinfmpt 41433
 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 1873 . 2 𝑖𝜑
2 nfcv 2932 . 2 𝑖(𝑘𝑍𝐵)
3 climinfmpt.z . 2 𝑍 = (ℤ𝑀)
4 climinfmpt.m . 2 (𝜑𝑀 ∈ ℤ)
5 climinfmpt.p . . 3 𝑘𝜑
6 climinfmpt.b . . 3 ((𝜑𝑘𝑍) → 𝐵 ∈ ℝ)
75, 6fmptd2f 40938 . 2 (𝜑 → (𝑘𝑍𝐵):𝑍⟶ℝ)
8 nfv 1873 . . . . . . 7 𝑘 𝑖𝑍
95, 8nfan 1862 . . . . . 6 𝑘(𝜑𝑖𝑍)
10 nfv 1873 . . . . . 6 𝑘(𝑖 + 1) / 𝑗𝐶𝑖 / 𝑗𝐶
119, 10nfim 1859 . . . . 5 𝑘((𝜑𝑖𝑍) → (𝑖 + 1) / 𝑗𝐶𝑖 / 𝑗𝐶)
12 eleq1 2853 . . . . . . 7 (𝑘 = 𝑖 → (𝑘𝑍𝑖𝑍))
1312anbi2d 619 . . . . . 6 (𝑘 = 𝑖 → ((𝜑𝑘𝑍) ↔ (𝜑𝑖𝑍)))
14 oveq1 6983 . . . . . . . 8 (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1))
1514csbeq1d 3793 . . . . . . 7 (𝑘 = 𝑖(𝑘 + 1) / 𝑗𝐶 = (𝑖 + 1) / 𝑗𝐶)
16 eqidd 2779 . . . . . . . 8 (𝑘 = 𝑖𝐵 = 𝐵)
17 csbco 3796 . . . . . . . . . . 11 𝑘 / 𝑗𝑗 / 𝑘𝐵 = 𝑘 / 𝑘𝐵
18 csbid 3794 . . . . . . . . . . 11 𝑘 / 𝑘𝐵 = 𝐵
1917, 18eqtr2i 2803 . . . . . . . . . 10 𝐵 = 𝑘 / 𝑗𝑗 / 𝑘𝐵
20 nfcv 2932 . . . . . . . . . . . . 13 𝑗𝐵
21 nfcv 2932 . . . . . . . . . . . . 13 𝑘𝐶
22 climinfmpt.c . . . . . . . . . . . . 13 (𝑘 = 𝑗𝐵 = 𝐶)
2320, 21, 22cbvcsb 3791 . . . . . . . . . . . 12 𝑗 / 𝑘𝐵 = 𝑗 / 𝑗𝐶
24 csbid 3794 . . . . . . . . . . . 12 𝑗 / 𝑗𝐶 = 𝐶
2523, 24eqtri 2802 . . . . . . . . . . 11 𝑗 / 𝑘𝐵 = 𝐶
2625csbeq2i 4257 . . . . . . . . . 10 𝑘 / 𝑗𝑗 / 𝑘𝐵 = 𝑘 / 𝑗𝐶
2719, 26eqtri 2802 . . . . . . . . 9 𝐵 = 𝑘 / 𝑗𝐶
2827a1i 11 . . . . . . . 8 (𝑘 = 𝑖𝐵 = 𝑘 / 𝑗𝐶)
29 csbeq1 3789 . . . . . . . 8 (𝑘 = 𝑖𝑘 / 𝑗𝐶 = 𝑖 / 𝑗𝐶)
3016, 28, 293eqtrd 2818 . . . . . . 7 (𝑘 = 𝑖𝐵 = 𝑖 / 𝑗𝐶)
3115, 30breq12d 4942 . . . . . 6 (𝑘 = 𝑖 → ((𝑘 + 1) / 𝑗𝐶𝐵(𝑖 + 1) / 𝑗𝐶𝑖 / 𝑗𝐶))
3213, 31imbi12d 337 . . . . 5 (𝑘 = 𝑖 → (((𝜑𝑘𝑍) → (𝑘 + 1) / 𝑗𝐶𝐵) ↔ ((𝜑𝑖𝑍) → (𝑖 + 1) / 𝑗𝐶𝑖 / 𝑗𝐶)))
33 simpl 475 . . . . . 6 ((𝜑𝑘𝑍) → 𝜑)
34 simpr 477 . . . . . 6 ((𝜑𝑘𝑍) → 𝑘𝑍)
35 eqidd 2779 . . . . . 6 ((𝜑𝑘𝑍) → (𝑘 + 1) = (𝑘 + 1))
36 climinfmpt.j . . . . . . . . 9 𝑗𝜑
37 nfv 1873 . . . . . . . . 9 𝑗 𝑘𝑍
38 nfv 1873 . . . . . . . . 9 𝑗(𝑘 + 1) = (𝑘 + 1)
3936, 37, 38nf3an 1864 . . . . . . . 8 𝑗(𝜑𝑘𝑍 ∧ (𝑘 + 1) = (𝑘 + 1))
40 nfcsb1v 3804 . . . . . . . . 9 𝑗(𝑘 + 1) / 𝑗𝐶
41 nfcv 2932 . . . . . . . . 9 𝑗
4240, 41, 20nfbr 4976 . . . . . . . 8 𝑗(𝑘 + 1) / 𝑗𝐶𝐵
4339, 42nfim 1859 . . . . . . 7 𝑗((𝜑𝑘𝑍 ∧ (𝑘 + 1) = (𝑘 + 1)) → (𝑘 + 1) / 𝑗𝐶𝐵)
44 ovex 7008 . . . . . . 7 (𝑘 + 1) ∈ V
45 eqeq1 2782 . . . . . . . . 9 (𝑗 = (𝑘 + 1) → (𝑗 = (𝑘 + 1) ↔ (𝑘 + 1) = (𝑘 + 1)))
46453anbi3d 1421 . . . . . . . 8 (𝑗 = (𝑘 + 1) → ((𝜑𝑘𝑍𝑗 = (𝑘 + 1)) ↔ (𝜑𝑘𝑍 ∧ (𝑘 + 1) = (𝑘 + 1))))
47 csbeq1a 3795 . . . . . . . . 9 (𝑗 = (𝑘 + 1) → 𝐶 = (𝑘 + 1) / 𝑗𝐶)
4847breq1d 4939 . . . . . . . 8 (𝑗 = (𝑘 + 1) → (𝐶𝐵(𝑘 + 1) / 𝑗𝐶𝐵))
4946, 48imbi12d 337 . . . . . . 7 (𝑗 = (𝑘 + 1) → (((𝜑𝑘𝑍𝑗 = (𝑘 + 1)) → 𝐶𝐵) ↔ ((𝜑𝑘𝑍 ∧ (𝑘 + 1) = (𝑘 + 1)) → (𝑘 + 1) / 𝑗𝐶𝐵)))
50 climinfmpt.l . . . . . . 7 ((𝜑𝑘𝑍𝑗 = (𝑘 + 1)) → 𝐶𝐵)
5143, 44, 49, 50vtoclf 3477 . . . . . 6 ((𝜑𝑘𝑍 ∧ (𝑘 + 1) = (𝑘 + 1)) → (𝑘 + 1) / 𝑗𝐶𝐵)
5233, 34, 35, 51syl3anc 1351 . . . . 5 ((𝜑𝑘𝑍) → (𝑘 + 1) / 𝑗𝐶𝐵)
5311, 32, 52chvar 2326 . . . 4 ((𝜑𝑖𝑍) → (𝑖 + 1) / 𝑗𝐶𝑖 / 𝑗𝐶)
54 csbco 3796 . . . . . . . 8 (𝑖 + 1) / 𝑗𝑗 / 𝑘𝐵 = (𝑖 + 1) / 𝑘𝐵
5554eqcomi 2787 . . . . . . 7 (𝑖 + 1) / 𝑘𝐵 = (𝑖 + 1) / 𝑗𝑗 / 𝑘𝐵
5625csbeq2i 4257 . . . . . . 7 (𝑖 + 1) / 𝑗𝑗 / 𝑘𝐵 = (𝑖 + 1) / 𝑗𝐶
5755, 56eqtri 2802 . . . . . 6 (𝑖 + 1) / 𝑘𝐵 = (𝑖 + 1) / 𝑗𝐶
5857a1i 11 . . . . 5 ((𝜑𝑖𝑍) → (𝑖 + 1) / 𝑘𝐵 = (𝑖 + 1) / 𝑗𝐶)
59 eqidd 2779 . . . . 5 ((𝜑𝑖𝑍) → 𝑖 / 𝑗𝐶 = 𝑖 / 𝑗𝐶)
6058, 59breq12d 4942 . . . 4 ((𝜑𝑖𝑍) → ((𝑖 + 1) / 𝑘𝐵𝑖 / 𝑗𝐶(𝑖 + 1) / 𝑗𝐶𝑖 / 𝑗𝐶))
6153, 60mpbird 249 . . 3 ((𝜑𝑖𝑍) → (𝑖 + 1) / 𝑘𝐵𝑖 / 𝑗𝐶)
623peano2uzs 12116 . . . . . 6 (𝑖𝑍 → (𝑖 + 1) ∈ 𝑍)
6362adantl 474 . . . . 5 ((𝜑𝑖𝑍) → (𝑖 + 1) ∈ 𝑍)
64 nfv 1873 . . . . . . . . 9 𝑘(𝑖 + 1) ∈ 𝑍
655, 64nfan 1862 . . . . . . . 8 𝑘(𝜑 ∧ (𝑖 + 1) ∈ 𝑍)
66 nfcv 2932 . . . . . . . . . 10 𝑘(𝑖 + 1)
6766nfcsb1 3803 . . . . . . . . 9 𝑘(𝑖 + 1) / 𝑘𝐵
6867nfel1 2946 . . . . . . . 8 𝑘(𝑖 + 1) / 𝑘𝐵 ∈ ℝ
6965, 68nfim 1859 . . . . . . 7 𝑘((𝜑 ∧ (𝑖 + 1) ∈ 𝑍) → (𝑖 + 1) / 𝑘𝐵 ∈ ℝ)
70 ovex 7008 . . . . . . 7 (𝑖 + 1) ∈ V
71 eleq1 2853 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → (𝑘𝑍 ↔ (𝑖 + 1) ∈ 𝑍))
7271anbi2d 619 . . . . . . . 8 (𝑘 = (𝑖 + 1) → ((𝜑𝑘𝑍) ↔ (𝜑 ∧ (𝑖 + 1) ∈ 𝑍)))
73 csbeq1a 3795 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → 𝐵 = (𝑖 + 1) / 𝑘𝐵)
7473eleq1d 2850 . . . . . . . 8 (𝑘 = (𝑖 + 1) → (𝐵 ∈ ℝ ↔ (𝑖 + 1) / 𝑘𝐵 ∈ ℝ))
7572, 74imbi12d 337 . . . . . . 7 (𝑘 = (𝑖 + 1) → (((𝜑𝑘𝑍) → 𝐵 ∈ ℝ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ 𝑍) → (𝑖 + 1) / 𝑘𝐵 ∈ ℝ)))
7669, 70, 75, 6vtoclf 3477 . . . . . 6 ((𝜑 ∧ (𝑖 + 1) ∈ 𝑍) → (𝑖 + 1) / 𝑘𝐵 ∈ ℝ)
7762, 76sylan2 583 . . . . 5 ((𝜑𝑖𝑍) → (𝑖 + 1) / 𝑘𝐵 ∈ ℝ)
78 eqid 2778 . . . . . 6 (𝑘𝑍𝐵) = (𝑘𝑍𝐵)
7966, 67, 73, 78fvmptf 6615 . . . . 5 (((𝑖 + 1) ∈ 𝑍(𝑖 + 1) / 𝑘𝐵 ∈ ℝ) → ((𝑘𝑍𝐵)‘(𝑖 + 1)) = (𝑖 + 1) / 𝑘𝐵)
8063, 77, 79syl2anc 576 . . . 4 ((𝜑𝑖𝑍) → ((𝑘𝑍𝐵)‘(𝑖 + 1)) = (𝑖 + 1) / 𝑘𝐵)
81 simpr 477 . . . . 5 ((𝜑𝑖𝑍) → 𝑖𝑍)
82 nfv 1873 . . . . . . . 8 𝑗 𝑖𝑍
8336, 82nfan 1862 . . . . . . 7 𝑗(𝜑𝑖𝑍)
84 nfcsb1v 3804 . . . . . . . 8 𝑗𝑖 / 𝑗𝐶
85 nfcv 2932 . . . . . . . 8 𝑗
8684, 85nfel 2944 . . . . . . 7 𝑗𝑖 / 𝑗𝐶 ∈ ℝ
8783, 86nfim 1859 . . . . . 6 𝑗((𝜑𝑖𝑍) → 𝑖 / 𝑗𝐶 ∈ ℝ)
88 eleq1 2853 . . . . . . . 8 (𝑗 = 𝑖 → (𝑗𝑍𝑖𝑍))
8988anbi2d 619 . . . . . . 7 (𝑗 = 𝑖 → ((𝜑𝑗𝑍) ↔ (𝜑𝑖𝑍)))
90 csbeq1a 3795 . . . . . . . 8 (𝑗 = 𝑖𝐶 = 𝑖 / 𝑗𝐶)
9190eleq1d 2850 . . . . . . 7 (𝑗 = 𝑖 → (𝐶 ∈ ℝ ↔ 𝑖 / 𝑗𝐶 ∈ ℝ))
9289, 91imbi12d 337 . . . . . 6 (𝑗 = 𝑖 → (((𝜑𝑗𝑍) → 𝐶 ∈ ℝ) ↔ ((𝜑𝑖𝑍) → 𝑖 / 𝑗𝐶 ∈ ℝ)))
93 nfv 1873 . . . . . . . . 9 𝑘 𝑗𝑍
945, 93nfan 1862 . . . . . . . 8 𝑘(𝜑𝑗𝑍)
95 nfv 1873 . . . . . . . 8 𝑘 𝐶 ∈ ℝ
9694, 95nfim 1859 . . . . . . 7 𝑘((𝜑𝑗𝑍) → 𝐶 ∈ ℝ)
97 eleq1 2853 . . . . . . . . 9 (𝑘 = 𝑗 → (𝑘𝑍𝑗𝑍))
9897anbi2d 619 . . . . . . . 8 (𝑘 = 𝑗 → ((𝜑𝑘𝑍) ↔ (𝜑𝑗𝑍)))
9922eleq1d 2850 . . . . . . . 8 (𝑘 = 𝑗 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ))
10098, 99imbi12d 337 . . . . . . 7 (𝑘 = 𝑗 → (((𝜑𝑘𝑍) → 𝐵 ∈ ℝ) ↔ ((𝜑𝑗𝑍) → 𝐶 ∈ ℝ)))
10196, 100, 6chvar 2326 . . . . . 6 ((𝜑𝑗𝑍) → 𝐶 ∈ ℝ)
10287, 92, 101chvar 2326 . . . . 5 ((𝜑𝑖𝑍) → 𝑖 / 𝑗𝐶 ∈ ℝ)
103 nfcv 2932 . . . . . 6 𝑘𝑖
104 nfcv 2932 . . . . . 6 𝑘𝑖 / 𝑗𝐶
105103, 104, 30, 78fvmptf 6615 . . . . 5 ((𝑖𝑍𝑖 / 𝑗𝐶 ∈ ℝ) → ((𝑘𝑍𝐵)‘𝑖) = 𝑖 / 𝑗𝐶)
10681, 102, 105syl2anc 576 . . . 4 ((𝜑𝑖𝑍) → ((𝑘𝑍𝐵)‘𝑖) = 𝑖 / 𝑗𝐶)
10780, 106breq12d 4942 . . 3 ((𝜑𝑖𝑍) → (((𝑘𝑍𝐵)‘(𝑖 + 1)) ≤ ((𝑘𝑍𝐵)‘𝑖) ↔ (𝑖 + 1) / 𝑘𝐵𝑖 / 𝑗𝐶))
10861, 107mpbird 249 . 2 ((𝜑𝑖𝑍) → ((𝑘𝑍𝐵)‘(𝑖 + 1)) ≤ ((𝑘𝑍𝐵)‘𝑖))
109 climinfmpt.e . . . 4 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘𝑍 𝑥𝐵)
110 breq1 4932 . . . . . 6 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
111110ralbidv 3147 . . . . 5 (𝑥 = 𝑦 → (∀𝑘𝑍 𝑥𝐵 ↔ ∀𝑘𝑍 𝑦𝐵))
112111cbvrexv 3384 . . . 4 (∃𝑥 ∈ ℝ ∀𝑘𝑍 𝑥𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑘𝑍 𝑦𝐵)
113109, 112sylib 210 . . 3 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑘𝑍 𝑦𝐵)
114 nfcv 2932 . . . . . . . 8 𝑘𝑦
115 nfcv 2932 . . . . . . . 8 𝑘
116 nfmpt1 5025 . . . . . . . . 9 𝑘(𝑘𝑍𝐵)
117116, 103nffv 6509 . . . . . . . 8 𝑘((𝑘𝑍𝐵)‘𝑖)
118114, 115, 117nfbr 4976 . . . . . . 7 𝑘 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖)
119 nfv 1873 . . . . . . 7 𝑖 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑘)
120 fveq2 6499 . . . . . . . 8 (𝑖 = 𝑘 → ((𝑘𝑍𝐵)‘𝑖) = ((𝑘𝑍𝐵)‘𝑘))
121120breq2d 4941 . . . . . . 7 (𝑖 = 𝑘 → (𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖) ↔ 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑘)))
122118, 119, 121cbvral 3379 . . . . . 6 (∀𝑖𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖) ↔ ∀𝑘𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑘))
123122a1i 11 . . . . 5 (𝜑 → (∀𝑖𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖) ↔ ∀𝑘𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑘)))
12478a1i 11 . . . . . . . 8 (𝜑 → (𝑘𝑍𝐵) = (𝑘𝑍𝐵))
125124, 6fvmpt2d 6607 . . . . . . 7 ((𝜑𝑘𝑍) → ((𝑘𝑍𝐵)‘𝑘) = 𝐵)
126125breq2d 4941 . . . . . 6 ((𝜑𝑘𝑍) → (𝑦 ≤ ((𝑘𝑍𝐵)‘𝑘) ↔ 𝑦𝐵))
1275, 126ralbida 3177 . . . . 5 (𝜑 → (∀𝑘𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑘) ↔ ∀𝑘𝑍 𝑦𝐵))
128123, 127bitrd 271 . . . 4 (𝜑 → (∀𝑖𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖) ↔ ∀𝑘𝑍 𝑦𝐵))
129128rexbidv 3242 . . 3 (𝜑 → (∃𝑦 ∈ ℝ ∀𝑖𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖) ↔ ∃𝑦 ∈ ℝ ∀𝑘𝑍 𝑦𝐵))
130113, 129mpbird 249 . 2 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑖𝑍 𝑦 ≤ ((𝑘𝑍𝐵)‘𝑖))
1311, 2, 3, 4, 7, 108, 130climinf2 41425 1 (𝜑 → (𝑘𝑍𝐵) ⇝ inf(ran (𝑘𝑍𝐵), ℝ*, < ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1068   = wceq 1507  Ⅎwnf 1746   ∈ wcel 2050  ∀wral 3088  ∃wrex 3089  ⦋csb 3786   class class class wbr 4929   ↦ cmpt 5008  ran crn 5408  ‘cfv 6188  (class class class)co 6976  infcinf 8700  ℝcr 10334  1c1 10336   + caddc 10338  ℝ*cxr 10473   < clt 10474   ≤ cle 10475  ℤcz 11793  ℤ≥cuz 12058   ⇝ cli 14702 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412  ax-pre-sup 10413 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-om 7397  df-1st 7501  df-2nd 7502  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-er 8089  df-en 8307  df-dom 8308  df-sdom 8309  df-sup 8701  df-inf 8702  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-div 11099  df-nn 11440  df-2 11503  df-3 11504  df-n0 11708  df-z 11794  df-uz 12059  df-rp 12205  df-fz 12709  df-seq 13185  df-exp 13245  df-cj 14319  df-re 14320  df-im 14321  df-sqrt 14455  df-abs 14456  df-clim 14706 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator