This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimno1

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

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

Proof

Step Hyp Ref Expression
1 rlimno1.1 ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
2 rlimno1.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐵 ) ) ⇝𝑟 0 )
3 rlimno1.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4 rlimno1.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≠ 0 )
5 fal ⊢ ¬ ⊥
6 3 4 reccld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1 / 𝐵 ) ∈ ℂ )
7 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 1 / 𝐵 ) ∈ ℂ )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∀ 𝑥 ∈ 𝐴 ( 1 / 𝐵 ) ∈ ℂ )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
10 1re ⊢ 1 ∈ ℝ
11 ifcl ⊢ ( ( 𝑦 ∈ ℝ ∧ 1 ∈ ℝ ) → if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ∈ ℝ )
12 9 10 11 sylancl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ∈ ℝ )
13 1rp ⊢ 1 ∈ ℝ+
14 13 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℝ+ )
15 max1 ⊢ ( ( 1 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 1 ≤ if ( 1 ≤ 𝑦 , 𝑦 , 1 ) )
16 10 9 15 sylancr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 1 ≤ if ( 1 ≤ 𝑦 , 𝑦 , 1 ) )
17 12 14 16 rpgecld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ∈ ℝ+ )
18 17 rpreccld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∈ ℝ+ )
19 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐵 ) ) ⇝𝑟 0 )
20 8 18 19 rlimi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ) )
21 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 1 / 𝐵 ) ∈ ℂ → dom ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐵 ) ) = 𝐴 )
22 7 21 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐵 ) ) = 𝐴 )
23 rlimss ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐵 ) ) ⇝𝑟 0 → dom ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐵 ) ) ⊆ ℝ )
24 2 23 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐵 ) ) ⊆ ℝ )
25 22 24 eqsstrrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐴 ⊆ ℝ )
27 rexanre ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ↔ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) )
28 26 27 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ↔ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) )
29 ressxr ⊢ ℝ ⊆ ℝ*
30 25 29 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
31 supxrunb1 ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑐 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
32 30 31 syl ⊢ ( 𝜑 → ( ∀ 𝑐 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
33 1 32 mpbird ⊢ ( 𝜑 → ∀ 𝑐 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∀ 𝑐 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 )
35 r19.29 ⊢ ( ( ∀ 𝑐 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) → ∃ 𝑐 ∈ ℝ ( ∃ 𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) )
36 r19.29r ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 ∧ ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) )
37 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
38 37 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → 𝐵 ∈ ℂ )
39 4 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≠ 0 )
40 39 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → 𝐵 ≠ 0 )
41 38 40 reccld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( 1 / 𝐵 ) ∈ ℂ )
42 41 subid1d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( ( 1 / 𝐵 ) − 0 ) = ( 1 / 𝐵 ) )
43 42 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) = ( abs ‘ ( 1 / 𝐵 ) ) )
44 1cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → 1 ∈ ℂ )
45 44 38 40 absdivd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( abs ‘ ( 1 / 𝐵 ) ) = ( ( abs ‘ 1 ) / ( abs ‘ 𝐵 ) ) )
46 10 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → 1 ∈ ℝ )
47 0le1 ⊢ 0 ≤ 1
48 47 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → 0 ≤ 1 )
49 46 48 absidd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( abs ‘ 1 ) = 1 )
50 49 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( ( abs ‘ 1 ) / ( abs ‘ 𝐵 ) ) = ( 1 / ( abs ‘ 𝐵 ) ) )
51 43 45 50 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) = ( 1 / ( abs ‘ 𝐵 ) ) )
52 17 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ∈ ℝ+ )
53 52 rprecred ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∈ ℝ )
54 37 39 absrpcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ+ )
55 54 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( abs ‘ 𝐵 ) ∈ ℝ+ )
56 55 rprecred ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( 1 / ( abs ‘ 𝐵 ) ) ∈ ℝ )
57 55 rpred ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
58 9 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → 𝑦 ∈ ℝ )
59 12 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ∈ ℝ )
60 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( abs ‘ 𝐵 ) ≤ 𝑦 )
61 max2 ⊢ ( ( 1 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ≤ if ( 1 ≤ 𝑦 , 𝑦 , 1 ) )
62 10 58 61 sylancr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → 𝑦 ≤ if ( 1 ≤ 𝑦 , 𝑦 , 1 ) )
63 57 58 59 60 62 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( abs ‘ 𝐵 ) ≤ if ( 1 ≤ 𝑦 , 𝑦 , 1 ) )
64 55 52 46 48 63 lediv2ad ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ≤ ( 1 / ( abs ‘ 𝐵 ) ) )
65 53 56 64 lensymd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ¬ ( 1 / ( abs ‘ 𝐵 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) )
66 51 65 eqnbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ¬ ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) )
67 66 pm2.21d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) → ⊥ ) )
68 67 expimpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( abs ‘ 𝐵 ) ≤ 𝑦 ∧ ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ) → ⊥ ) )
69 68 ancomsd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ⊥ ) )
70 69 imim2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) → ( 𝑐 ≤ 𝑥 → ⊥ ) ) )
71 70 impcomd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑐 ≤ 𝑥 ∧ ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) → ⊥ ) )
72 71 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 ∧ ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) → ⊥ ) )
73 36 72 syl5 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ∃ 𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) → ⊥ ) )
74 73 rexlimdvw ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ( ∃ 𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) → ⊥ ) )
75 35 74 syl5 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ∀ 𝑐 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) → ⊥ ) )
76 34 75 mpand ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ∧ ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) → ⊥ ) )
77 28 76 sylbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ ( ( 1 / 𝐵 ) − 0 ) ) < ( 1 / if ( 1 ≤ 𝑦 , 𝑦 , 1 ) ) ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) → ⊥ ) )
78 20 77 mpand ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ⊥ ) )
79 5 78 mtoi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ¬ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑦 ) )
80 79 nrexdv ⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑦 ) )
81 25 3 elo1mpt ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ∃ 𝑐 ∈ ℝ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) )
82 rexcom ⊢ ( ∃ 𝑐 ∈ ℝ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑦 ) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑦 ) )
83 81 82 bitrdi ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) )
84 80 83 mtbird ⊢ ( 𝜑 → ¬ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )