Metamath Proof Explorer


Theorem o1lo1

Description: A real function is eventually bounded iff it is eventually lower bounded and eventually upper bounded. (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypothesis o1lo1.1 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
Assertion o1lo1 ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) )

Proof

Step Hyp Ref Expression
1 o1lo1.1 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
2 o1dm ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) → dom ( 𝑥𝐴𝐵 ) ⊆ ℝ )
3 2 a1i ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) → dom ( 𝑥𝐴𝐵 ) ⊆ ℝ ) )
4 lo1dm ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) → dom ( 𝑥𝐴𝐵 ) ⊆ ℝ )
5 4 adantr ( ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) → dom ( 𝑥𝐴𝐵 ) ⊆ ℝ )
6 5 a1i ( 𝜑 → ( ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) → dom ( 𝑥𝐴𝐵 ) ⊆ ℝ ) )
7 1 ralrimiva ( 𝜑 → ∀ 𝑥𝐴 𝐵 ∈ ℝ )
8 dmmptg ( ∀ 𝑥𝐴 𝐵 ∈ ℝ → dom ( 𝑥𝐴𝐵 ) = 𝐴 )
9 7 8 syl ( 𝜑 → dom ( 𝑥𝐴𝐵 ) = 𝐴 )
10 9 sseq1d ( 𝜑 → ( dom ( 𝑥𝐴𝐵 ) ⊆ ℝ ↔ 𝐴 ⊆ ℝ ) )
11 simpr ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) → 𝑚 ∈ ℝ )
12 1 adantlr ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℝ )
13 12 adantlr ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℝ )
14 simplr ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥𝐴 ) → 𝑚 ∈ ℝ )
15 13 14 absled ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ 𝑚 ↔ ( - 𝑚𝐵𝐵𝑚 ) ) )
16 ancom ( ( - 𝑚𝐵𝐵𝑚 ) ↔ ( 𝐵𝑚 ∧ - 𝑚𝐵 ) )
17 lenegcon1 ( ( 𝑚 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝑚𝐵 ↔ - 𝐵𝑚 ) )
18 14 13 17 syl2anc ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥𝐴 ) → ( - 𝑚𝐵 ↔ - 𝐵𝑚 ) )
19 18 anbi2d ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥𝐴 ) → ( ( 𝐵𝑚 ∧ - 𝑚𝐵 ) ↔ ( 𝐵𝑚 ∧ - 𝐵𝑚 ) ) )
20 16 19 syl5bb ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥𝐴 ) → ( ( - 𝑚𝐵𝐵𝑚 ) ↔ ( 𝐵𝑚 ∧ - 𝐵𝑚 ) ) )
21 15 20 bitrd ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ 𝑚 ↔ ( 𝐵𝑚 ∧ - 𝐵𝑚 ) ) )
22 21 imbi2d ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥𝐴 ) → ( ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ( 𝑐𝑥 → ( 𝐵𝑚 ∧ - 𝐵𝑚 ) ) ) )
23 22 ralbidva ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑚 ∧ - 𝐵𝑚 ) ) ) )
24 23 rexbidv ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑚 ∧ - 𝐵𝑚 ) ) ) )
25 24 biimpd ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑚 ∧ - 𝐵𝑚 ) ) ) )
26 breq2 ( 𝑛 = 𝑚 → ( 𝐵𝑛𝐵𝑚 ) )
27 26 anbi1d ( 𝑛 = 𝑚 → ( ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ↔ ( 𝐵𝑚 ∧ - 𝐵𝑝 ) ) )
28 27 imbi2d ( 𝑛 = 𝑚 → ( ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) ↔ ( 𝑐𝑥 → ( 𝐵𝑚 ∧ - 𝐵𝑝 ) ) ) )
29 28 rexralbidv ( 𝑛 = 𝑚 → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑚 ∧ - 𝐵𝑝 ) ) ) )
30 breq2 ( 𝑝 = 𝑚 → ( - 𝐵𝑝 ↔ - 𝐵𝑚 ) )
31 30 anbi2d ( 𝑝 = 𝑚 → ( ( 𝐵𝑚 ∧ - 𝐵𝑝 ) ↔ ( 𝐵𝑚 ∧ - 𝐵𝑚 ) ) )
32 31 imbi2d ( 𝑝 = 𝑚 → ( ( 𝑐𝑥 → ( 𝐵𝑚 ∧ - 𝐵𝑝 ) ) ↔ ( 𝑐𝑥 → ( 𝐵𝑚 ∧ - 𝐵𝑚 ) ) ) )
33 32 rexralbidv ( 𝑝 = 𝑚 → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑚 ∧ - 𝐵𝑝 ) ) ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑚 ∧ - 𝐵𝑚 ) ) ) )
34 29 33 rspc2ev ( ( 𝑚 ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑚 ∧ - 𝐵𝑚 ) ) ) → ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) )
35 34 3anidm12 ( ( 𝑚 ∈ ℝ ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑚 ∧ - 𝐵𝑚 ) ) ) → ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) )
36 11 25 35 syl6an ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) → ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) ) )
37 36 rexlimdva ( ( 𝜑𝐴 ⊆ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) → ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) ) )
38 simplrr ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑛𝑝 ) → 𝑝 ∈ ℝ )
39 simplrl ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ ¬ 𝑛𝑝 ) → 𝑛 ∈ ℝ )
40 38 39 ifclda ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) → if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ∈ ℝ )
41 max2 ( ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → 𝑝 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) )
42 41 ad2antlr ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → 𝑝 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) )
43 12 adantlr ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℝ )
44 43 renegcld ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → - 𝐵 ∈ ℝ )
45 simplrr ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → 𝑝 ∈ ℝ )
46 simplrl ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → 𝑛 ∈ ℝ )
47 45 46 ifcld ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ∈ ℝ )
48 letr ( ( - 𝐵 ∈ ℝ ∧ 𝑝 ∈ ℝ ∧ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ∈ ℝ ) → ( ( - 𝐵𝑝𝑝 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) → - 𝐵 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) )
49 44 45 47 48 syl3anc ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( ( - 𝐵𝑝𝑝 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) → - 𝐵 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) )
50 42 49 mpan2d ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( - 𝐵𝑝 → - 𝐵 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) )
51 lenegcon1 ( ( 𝐵 ∈ ℝ ∧ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ∈ ℝ ) → ( - 𝐵 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ↔ - if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ≤ 𝐵 ) )
52 43 47 51 syl2anc ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( - 𝐵 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ↔ - if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ≤ 𝐵 ) )
53 50 52 sylibd ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( - 𝐵𝑝 → - if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ≤ 𝐵 ) )
54 max1 ( ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → 𝑛 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) )
55 54 ad2antlr ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → 𝑛 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) )
56 letr ( ( 𝐵 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ∈ ℝ ) → ( ( 𝐵𝑛𝑛 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) → 𝐵 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) )
57 43 46 47 56 syl3anc ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( ( 𝐵𝑛𝑛 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) → 𝐵 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) )
58 55 57 mpan2d ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( 𝐵𝑛𝐵 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) )
59 53 58 anim12d ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( ( - 𝐵𝑝𝐵𝑛 ) → ( - if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ≤ 𝐵𝐵 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) ) )
60 59 ancomsd ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( ( 𝐵𝑛 ∧ - 𝐵𝑝 ) → ( - if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ≤ 𝐵𝐵 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) ) )
61 43 47 absled ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ↔ ( - if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ≤ 𝐵𝐵 ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) ) )
62 60 61 sylibrd ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( ( 𝐵𝑛 ∧ - 𝐵𝑝 ) → ( abs ‘ 𝐵 ) ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) )
63 62 imim2d ( ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) → ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) ) )
64 63 ralimdva ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) → ( ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) → ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) ) )
65 64 reximdv ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) → ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) ) )
66 breq2 ( 𝑚 = if ( 𝑛𝑝 , 𝑝 , 𝑛 ) → ( ( abs ‘ 𝐵 ) ≤ 𝑚 ↔ ( abs ‘ 𝐵 ) ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) )
67 66 imbi2d ( 𝑚 = if ( 𝑛𝑝 , 𝑝 , 𝑛 ) → ( ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) ) )
68 67 rexralbidv ( 𝑚 = if ( 𝑛𝑝 , 𝑝 , 𝑛 ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) ) )
69 68 rspcev ( ( if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ∈ ℝ ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ if ( 𝑛𝑝 , 𝑝 , 𝑛 ) ) ) → ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) )
70 40 65 69 syl6an ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) → ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ) )
71 70 rexlimdvva ( ( 𝜑𝐴 ⊆ ℝ ) → ( ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) → ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ) )
72 37 71 impbid ( ( 𝜑𝐴 ⊆ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) ) )
73 rexanre ( 𝐴 ⊆ ℝ → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) ↔ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ) ) )
74 73 adantl ( ( 𝜑𝐴 ⊆ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) ↔ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ) ) )
75 74 2rexbidv ( ( 𝜑𝐴 ⊆ ℝ ) → ( ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( 𝐵𝑛 ∧ - 𝐵𝑝 ) ) ↔ ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ) ) )
76 72 75 bitrd ( ( 𝜑𝐴 ⊆ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ) ) )
77 reeanv ( ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ) ↔ ( ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ∧ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ) )
78 76 77 bitrdi ( ( 𝜑𝐴 ⊆ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ( ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ∧ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ) ) )
79 rexcom ( ∃ 𝑐 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) )
80 rexcom ( ∃ 𝑐 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ↔ ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) )
81 rexcom ( ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ↔ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) )
82 80 81 anbi12i ( ( ∃ 𝑐 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ) ↔ ( ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ∧ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ) )
83 78 79 82 3bitr4g ( ( 𝜑𝐴 ⊆ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ( ∃ 𝑐 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ) ) )
84 simpr ( ( 𝜑𝐴 ⊆ ℝ ) → 𝐴 ⊆ ℝ )
85 12 recnd ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℂ )
86 84 85 elo1mpt ( ( 𝜑𝐴 ⊆ ℝ ) → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ↔ ∃ 𝑐 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ) )
87 84 12 ello1mpt ( ( 𝜑𝐴 ⊆ ℝ ) → ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑐 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ) )
88 12 renegcld ( ( ( 𝜑𝐴 ⊆ ℝ ) ∧ 𝑥𝐴 ) → - 𝐵 ∈ ℝ )
89 84 88 ello1mpt ( ( 𝜑𝐴 ⊆ ℝ ) → ( ( 𝑥𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ) )
90 87 89 anbi12d ( ( 𝜑𝐴 ⊆ ℝ ) → ( ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ↔ ( ∃ 𝑐 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥𝐵𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥𝐴 ( 𝑐𝑥 → - 𝐵𝑝 ) ) ) )
91 83 86 90 3bitr4d ( ( 𝜑𝐴 ⊆ ℝ ) → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) )
92 91 ex ( 𝜑 → ( 𝐴 ⊆ ℝ → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) ) )
93 10 92 sylbid ( 𝜑 → ( dom ( 𝑥𝐴𝐵 ) ⊆ ℝ → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) ) )
94 3 6 93 pm5.21ndd ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) )