rlimno1 - Metamath Proof Explorer

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

Theorem rlimno1 14672

Description: A function whose inverse converges to zero is unbounded. (Contributed by Mario Carneiro, 30-May-2016.)

**Hypotheses**
Ref	Expression
rlimno1.1	⊢ (𝜑 → sup(𝐴, ℝ^*, < ) = +∞)
rlimno1.2	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) ⇝_𝑟 0)
rlimno1.3	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
rlimno1.4	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0)

**Assertion**
Ref	Expression
rlimno1	⊢ (𝜑 → ¬ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))

Distinct variable groups: 𝑥,𝐴 𝜑,𝑥 Allowed substitution hint: 𝐵(𝑥)

Proof of Theorem rlimno1 Dummy variables 𝑐 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fal 1667	. . . 4 ⊢ ¬ ⊥
2		rlimno1.3	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
3		rlimno1.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0)
4	2, 3	reccld 11050	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 / 𝐵) ∈ ℂ)
5	4	ralrimiva 3113	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (1 / 𝐵) ∈ ℂ)
6	5	adantr 472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∀𝑥 ∈ 𝐴 (1 / 𝐵) ∈ ℂ)
7		simpr 477	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
8		1re 10295	. . . . . . . . 9 ⊢ 1 ∈ ℝ
9		ifcl 4289	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ ∧ 1 ∈ ℝ) → if(1 ≤ 𝑦, 𝑦, 1) ∈ ℝ)
10	7, 8, 9	sylancl 580	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(1 ≤ 𝑦, 𝑦, 1) ∈ ℝ)
11		1rp 12035	. . . . . . . . 9 ⊢ 1 ∈ ℝ⁺
12	11	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈ ℝ⁺)
13		max1 12221	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 1 ≤ if(1 ≤ 𝑦, 𝑦, 1))
14	8, 7, 13	sylancr 581	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ≤ if(1 ≤ 𝑦, 𝑦, 1))
15	10, 12, 14	rpgecld 12112	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(1 ≤ 𝑦, 𝑦, 1) ∈ ℝ⁺)
16	15	rpreccld 12083	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∈ ℝ⁺)
17		rlimno1.2	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) ⇝_𝑟 0)
18	17	adantr 472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) ⇝_𝑟 0)
19	6, 16, 18	rlimi 14532	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1))))
20		dmmptg 5820	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 (1 / 𝐵) ∈ ℂ → dom (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) = 𝐴)
21	5, 20	syl 17	. . . . . . . . 9 ⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) = 𝐴)
22		rlimss 14521	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) ⇝_𝑟 0 → dom (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) ⊆ ℝ)
23	17, 22	syl 17	. . . . . . . . 9 ⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) ⊆ ℝ)
24	21, 23	eqsstr3d 3802	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
25	24	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐴 ⊆ ℝ)
26		rexanre 14374	. . . . . . 7 ⊢ (𝐴 ⊆ ℝ → (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦)) ↔ (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1))) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦))))
27	25, 26	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦)) ↔ (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1))) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦))))
28		rlimno1.1	. . . . . . . . 9 ⊢ (𝜑 → sup(𝐴, ℝ^*, < ) = +∞)
29		ressxr 10339	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℝ^*
30	24, 29	syl6ss 3775	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
31		supxrunb1 12354	. . . . . . . . . 10 ⊢ (𝐴 ⊆ ℝ^* → (∀𝑐 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ↔ sup(𝐴, ℝ^*, < ) = +∞))
32	30, 31	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑐 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ↔ sup(𝐴, ℝ^*, < ) = +∞))
33	28, 32	mpbird 248	. . . . . . . 8 ⊢ (𝜑 → ∀𝑐 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥)
34	33	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∀𝑐 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥)
35		r19.29 3219	. . . . . . . 8 ⊢ ((∀𝑐 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ∃𝑐 ∈ ℝ (∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))))
36		r19.29r 3220	. . . . . . . . . 10 ⊢ ((∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ∃𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 ∧ (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))))
37	2	adantlr 706	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
38	3	adantlr 706	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0)
39	37, 38	absrpcld 14475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ⁺)
40	39	adantr 472	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘𝐵) ∈ ℝ⁺)
41	15	ad2antrr 717	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → if(1 ≤ 𝑦, 𝑦, 1) ∈ ℝ⁺)
42	8	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 1 ∈ ℝ)
43		0le1 10807	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ 1
44	43	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 0 ≤ 1)
45	40	rpred 12073	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘𝐵) ∈ ℝ)
46	7	ad2antrr 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 𝑦 ∈ ℝ)
47	10	ad2antrr 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → if(1 ≤ 𝑦, 𝑦, 1) ∈ ℝ)
48		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘𝐵) ≤ 𝑦)
49		max2 12223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ≤ if(1 ≤ 𝑦, 𝑦, 1))
50	8, 46, 49	sylancr 581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 𝑦 ≤ if(1 ≤ 𝑦, 𝑦, 1))
51	45, 46, 47, 48, 50	letrd 10450	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘𝐵) ≤ if(1 ≤ 𝑦, 𝑦, 1))
52	40, 41, 42, 44, 51	lediv2ad 12095	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (1 / if(1 ≤ 𝑦, 𝑦, 1)) ≤ (1 / (abs‘𝐵)))
53	41	rprecred 12084	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∈ ℝ)
54	40	rprecred 12084	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (1 / (abs‘𝐵)) ∈ ℝ)
55	53, 54	lenltd 10439	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ((1 / if(1 ≤ 𝑦, 𝑦, 1)) ≤ (1 / (abs‘𝐵)) ↔ ¬ (1 / (abs‘𝐵)) < (1 / if(1 ≤ 𝑦, 𝑦, 1))))
56	52, 55	mpbid 223	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ¬ (1 / (abs‘𝐵)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)))
57	37	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 𝐵 ∈ ℂ)
58	38	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 𝐵 ≠ 0)
59	57, 58	reccld 11050	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (1 / 𝐵) ∈ ℂ)
60	59	subid1d 10637	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ((1 / 𝐵) − 0) = (1 / 𝐵))
61	60	fveq2d 6381	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘((1 / 𝐵) − 0)) = (abs‘(1 / 𝐵)))
62		1cnd 10290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 1 ∈ ℂ)
63	62, 57, 58	absdivd 14482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘(1 / 𝐵)) = ((abs‘1) / (abs‘𝐵)))
64	42, 44	absidd 14449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘1) = 1)
65	64	oveq1d 6859	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ((abs‘1) / (abs‘𝐵)) = (1 / (abs‘𝐵)))
66	61, 63, 65	3eqtrd 2803	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘((1 / 𝐵) − 0)) = (1 / (abs‘𝐵)))
67	66	breq1d 4821	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ↔ (1 / (abs‘𝐵)) < (1 / if(1 ≤ 𝑦, 𝑦, 1))))
68	56, 67	mtbird 316	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ¬ (abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)))
69	68	pm2.21d 119	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) → ⊥))
70	69	expimpd 445	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (((abs‘𝐵) ≤ 𝑦 ∧ (abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1))) → ⊥))
71	70	ancomsd 457	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦) → ⊥))
72	71	imim2d 57	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦)) → (𝑐 ≤ 𝑥 → ⊥)))
73	72	com23 86	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑐 ≤ 𝑥 → ((𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦)) → ⊥)))
74	73	impd 398	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝑐 ≤ 𝑥 ∧ (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ⊥))
75	74	rexlimdva 3178	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 ∧ (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ⊥))
76	36, 75	syl5 34	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ⊥))
77	76	rexlimdvw 3181	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑐 ∈ ℝ (∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ⊥))
78	35, 77	syl5 34	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((∀𝑐 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ⊥))
79	34, 78	mpand 686	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦)) → ⊥))
80	27, 79	sylbird 251	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1))) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦)) → ⊥))
81	19, 80	mpand 686	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦) → ⊥))
82	1, 81	mtoi 190	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ¬ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦))
83	82	nrexdv 3147	. 2 ⊢ (𝜑 → ¬ ∃𝑦 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦))
84	24, 2	elo1mpt 14553	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1) ↔ ∃𝑐 ∈ ℝ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦)))
85		rexcom 3246	. . 3 ⊢ (∃𝑐 ∈ ℝ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦) ↔ ∃𝑦 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦))
86	84, 85	syl6bb 278	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1) ↔ ∃𝑦 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦)))
87	83, 86	mtbird 316	1 ⊢ (𝜑 → ¬ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 197 ∧ wa 384 = wceq 1652 ⊥wfal 1665 ∈ wcel 2155 ≠ wne 2937 ∀wral 3055 ∃wrex 3056 ⊆ wss 3734 ifcif 4245 class class class wbr 4811 ↦ cmpt 4890 dom cdm 5279 ‘cfv 6070 (class class class)co 6844 supcsup 8555 ℂcc 10189 ℝcr 10190 0cc0 10191 1c1 10192 +∞cpnf 10327 ℝ^*cxr 10329 < clt 10330 ≤ cle 10331 − cmin 10522 / cdiv 10940 ℝ⁺crp 12031 abscabs 14262 ⇝_𝑟 crli 14504 𝑂(1)co1 14505

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-sep 4943 ax-nul 4951 ax-pow 5003 ax-pr 5064 ax-un 7149 ax-cnex 10247 ax-resscn 10248 ax-1cn 10249 ax-icn 10250 ax-addcl 10251 ax-addrcl 10252 ax-mulcl 10253 ax-mulrcl 10254 ax-mulcom 10255 ax-addass 10256 ax-mulass 10257 ax-distr 10258 ax-i2m1 10259 ax-1ne0 10260 ax-1rid 10261 ax-rnegex 10262 ax-rrecex 10263 ax-cnre 10264 ax-pre-lttri 10265 ax-pre-lttrn 10266 ax-pre-ltadd 10267 ax-pre-mulgt0 10268 ax-pre-sup 10269

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3or 1108 df-3an 1109 df-tru 1656 df-fal 1666 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-nel 3041 df-ral 3060 df-rex 3061 df-reu 3062 df-rmo 3063 df-rab 3064 df-v 3352 df-sbc 3599 df-csb 3694 df-dif 3737 df-un 3739 df-in 3741 df-ss 3748 df-pss 3750 df-nul 4082 df-if 4246 df-pw 4319 df-sn 4337 df-pr 4339 df-tp 4341 df-op 4343 df-uni 4597 df-iun 4680 df-br 4812 df-opab 4874 df-mpt 4891 df-tr 4914 df-id 5187 df-eprel 5192 df-po 5200 df-so 5201 df-fr 5238 df-we 5240 df-xp 5285 df-rel 5286 df-cnv 5287 df-co 5288 df-dm 5289 df-rn 5290 df-res 5291 df-ima 5292 df-pred 5867 df-ord 5913 df-on 5914 df-lim 5915 df-suc 5916 df-iota 6033 df-fun 6072 df-fn 6073 df-f 6074 df-f1 6075 df-fo 6076 df-f1o 6077 df-fv 6078 df-riota 6805 df-ov 6847 df-oprab 6848 df-mpt2 6849 df-om 7266 df-2nd 7369 df-wrecs 7612 df-recs 7674 df-rdg 7712 df-er 7949 df-pm 8065 df-en 8163 df-dom 8164 df-sdom 8165 df-sup 8557 df-pnf 10332 df-mnf 10333 df-xr 10334 df-ltxr 10335 df-le 10336 df-sub 10524 df-neg 10525 df-div 10941 df-nn 11277 df-2 11337 df-3 11338 df-n0 11541 df-z 11627 df-uz 11890 df-rp 12032 df-ico 12386 df-seq 13012 df-exp 13071 df-cj 14127 df-re 14128 df-im 14129 df-sqrt 14263 df-abs 14264 df-rlim 14508 df-o1 14509 df-lo1 14510

This theorem is referenced by: logno1 24676

W3C validator