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

Theorem cnrefiisplem 40556
Description: Lemma for cnrefiisp 40557 (some local definitions are used). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
Hypotheses
Ref Expression
cnrefiisplem.a (𝜑𝐴 ∈ ℂ)
cnrefiisplem.n (𝜑 → ¬ 𝐴 ∈ ℝ)
cnrefiisplem.b (𝜑𝐵 ∈ Fin)
cnrefiisplem.c 𝐶 = (ℝ ∪ 𝐵)
cnrefiisplem.d 𝐷 = ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
cnrefiisplem.x 𝑋 = inf(𝐷, ℝ*, < )
Assertion
Ref Expression
cnrefiisplem (𝜑 → ∃𝑥 ∈ ℝ+𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))))
Distinct variable groups:   𝑦,𝐴,𝑥   𝑦,𝐵   𝑥,𝐶   𝑥,𝑋,𝑦   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐶(𝑦)   𝐷(𝑥,𝑦)

Proof of Theorem cnrefiisplem
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 simpr 479 . . . . . . 7 ((𝜑𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 = (abs‘(ℑ‘𝐴)))
2 cnrefiisplem.a . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
3 cnrefiisplem.n . . . . . . . . 9 (𝜑 → ¬ 𝐴 ∈ ℝ)
42, 3absimnre 40203 . . . . . . . 8 (𝜑 → (abs‘(ℑ‘𝐴)) ∈ ℝ+)
54adantr 472 . . . . . . 7 ((𝜑𝑤 = (abs‘(ℑ‘𝐴))) → (abs‘(ℑ‘𝐴)) ∈ ℝ+)
61, 5eqeltrd 2837 . . . . . 6 ((𝜑𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+)
76adantlr 753 . . . . 5 (((𝜑𝑤𝐷) ∧ 𝑤 = (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+)
8 simpll 807 . . . . . 6 (((𝜑𝑤𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝜑)
9 cnrefiisplem.d . . . . . . . . . . . 12 𝐷 = ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
109eleq2i 2829 . . . . . . . . . . 11 (𝑤𝐷𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
1110biimpi 206 . . . . . . . . . 10 (𝑤𝐷𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
12 nelsn 4355 . . . . . . . . . 10 (𝑤 ≠ (abs‘(ℑ‘𝐴)) → ¬ 𝑤 ∈ {(abs‘(ℑ‘𝐴))})
13 elunnel1 3895 . . . . . . . . . 10 ((𝑤 ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}) ∧ ¬ 𝑤 ∈ {(abs‘(ℑ‘𝐴))}) → 𝑤 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
1411, 12, 13syl2an 495 . . . . . . . . 9 ((𝑤𝐷𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝑤 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
15 eliun 4674 . . . . . . . . 9 (𝑤 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ↔ ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦𝐴))})
1614, 15sylib 208 . . . . . . . 8 ((𝑤𝐷𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦𝐴))})
17 velsn 4335 . . . . . . . . 9 (𝑤 ∈ {(abs‘(𝑦𝐴))} ↔ 𝑤 = (abs‘(𝑦𝐴)))
1817rexbii 3177 . . . . . . . 8 (∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 ∈ {(abs‘(𝑦𝐴))} ↔ ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)))
1916, 18sylib 208 . . . . . . 7 ((𝑤𝐷𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)))
2019adantll 752 . . . . . 6 (((𝜑𝑤𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → ∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)))
21 simpr 479 . . . . . . . 8 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑤 = (abs‘(𝑦𝐴)))
22 eldifi 3873 . . . . . . . . . . . 12 (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ∈ (𝐵 ∩ ℂ))
2322elin2d 3944 . . . . . . . . . . 11 (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦 ∈ ℂ)
2423ad2antlr 765 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑦 ∈ ℂ)
252ad2antrr 764 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝐴 ∈ ℂ)
2624, 25subcld 10582 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → (𝑦𝐴) ∈ ℂ)
27 eldifsni 4464 . . . . . . . . . . 11 (𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) → 𝑦𝐴)
2827ad2antlr 765 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑦𝐴)
2924, 25, 28subne0d 10591 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → (𝑦𝐴) ≠ 0)
3026, 29absrpcld 14384 . . . . . . . 8 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → (abs‘(𝑦𝐴)) ∈ ℝ+)
3121, 30eqeltrd 2837 . . . . . . 7 (((𝜑𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})) ∧ 𝑤 = (abs‘(𝑦𝐴))) → 𝑤 ∈ ℝ+)
3231rexlimdva2 39836 . . . . . 6 (𝜑 → (∃𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴})𝑤 = (abs‘(𝑦𝐴)) → 𝑤 ∈ ℝ+))
338, 20, 32sylc 65 . . . . 5 (((𝜑𝑤𝐷) ∧ 𝑤 ≠ (abs‘(ℑ‘𝐴))) → 𝑤 ∈ ℝ+)
347, 33pm2.61dane 3017 . . . 4 ((𝜑𝑤𝐷) → 𝑤 ∈ ℝ+)
3534ssd 39749 . . 3 (𝜑𝐷 ⊆ ℝ+)
36 cnrefiisplem.x . . . 4 𝑋 = inf(𝐷, ℝ*, < )
37 xrltso 12165 . . . . . 6 < Or ℝ*
3837a1i 11 . . . . 5 (𝜑 → < Or ℝ*)
39 snfi 8201 . . . . . . . 8 {(abs‘(ℑ‘𝐴))} ∈ Fin
4039a1i 11 . . . . . . 7 (𝜑 → {(abs‘(ℑ‘𝐴))} ∈ Fin)
41 cnrefiisplem.b . . . . . . . . 9 (𝜑𝐵 ∈ Fin)
42 inss1 3974 . . . . . . . . . . 11 (𝐵 ∩ ℂ) ⊆ 𝐵
4342a1i 11 . . . . . . . . . 10 (𝜑 → (𝐵 ∩ ℂ) ⊆ 𝐵)
4443ssdifssd 3889 . . . . . . . . 9 (𝜑 → ((𝐵 ∩ ℂ) ∖ {𝐴}) ⊆ 𝐵)
4541, 44ssfid 8346 . . . . . . . 8 (𝜑 → ((𝐵 ∩ ℂ) ∖ {𝐴}) ∈ Fin)
46 snfi 8201 . . . . . . . . 9 {(abs‘(𝑦𝐴))} ∈ Fin
4746rgenw 3060 . . . . . . . 8 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin
48 iunfi 8417 . . . . . . . 8 ((((𝐵 ∩ ℂ) ∖ {𝐴}) ∈ Fin ∧ ∀𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin) → 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin)
4945, 47, 48sylancl 697 . . . . . . 7 (𝜑 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} ∈ Fin)
5040, 49unfid 39842 . . . . . 6 (𝜑 → ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}) ∈ Fin)
519, 50syl5eqel 2841 . . . . 5 (𝜑𝐷 ∈ Fin)
52 fvex 6360 . . . . . . . . . 10 (abs‘(ℑ‘𝐴)) ∈ V
5352snid 4351 . . . . . . . . 9 (abs‘(ℑ‘𝐴)) ∈ {(abs‘(ℑ‘𝐴))}
54 elun1 3921 . . . . . . . . 9 ((abs‘(ℑ‘𝐴)) ∈ {(abs‘(ℑ‘𝐴))} → (abs‘(ℑ‘𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
5553, 54ax-mp 5 . . . . . . . 8 (abs‘(ℑ‘𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
5655, 9eleqtrri 2836 . . . . . . 7 (abs‘(ℑ‘𝐴)) ∈ 𝐷
5756a1i 11 . . . . . 6 (𝜑 → (abs‘(ℑ‘𝐴)) ∈ 𝐷)
5857ne0d 39805 . . . . 5 (𝜑𝐷 ≠ ∅)
59 rpssxr 40207 . . . . . 6 + ⊆ ℝ*
6035, 59syl6ss 3754 . . . . 5 (𝜑𝐷 ⊆ ℝ*)
61 fiinfcl 8570 . . . . 5 (( < Or ℝ* ∧ (𝐷 ∈ Fin ∧ 𝐷 ≠ ∅ ∧ 𝐷 ⊆ ℝ*)) → inf(𝐷, ℝ*, < ) ∈ 𝐷)
6238, 51, 58, 60, 61syl13anc 1479 . . . 4 (𝜑 → inf(𝐷, ℝ*, < ) ∈ 𝐷)
6336, 62syl5eqel 2841 . . 3 (𝜑𝑋𝐷)
6435, 63sseldd 3743 . 2 (𝜑𝑋 ∈ ℝ+)
6535, 62sseldd 3743 . . . . . . . . . 10 (𝜑 → inf(𝐷, ℝ*, < ) ∈ ℝ+)
6665rpred 12063 . . . . . . . . 9 (𝜑 → inf(𝐷, ℝ*, < ) ∈ ℝ)
6766adantr 472 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ∈ ℝ)
682imcld 14132 . . . . . . . . . . 11 (𝜑 → (ℑ‘𝐴) ∈ ℝ)
6968recnd 10258 . . . . . . . . . 10 (𝜑 → (ℑ‘𝐴) ∈ ℂ)
7069adantr 472 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → (ℑ‘𝐴) ∈ ℂ)
7170abscld 14372 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (abs‘(ℑ‘𝐴)) ∈ ℝ)
72 recn 10216 . . . . . . . . . . 11 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
7372adantl 473 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
742adantr 472 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → 𝐴 ∈ ℂ)
7573, 74subcld 10582 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → (𝑦𝐴) ∈ ℂ)
7675abscld 14372 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (abs‘(𝑦𝐴)) ∈ ℝ)
7760adantr 472 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝐷 ⊆ ℝ*)
78 infxrlb 12355 . . . . . . . . 9 ((𝐷 ⊆ ℝ* ∧ (abs‘(ℑ‘𝐴)) ∈ 𝐷) → inf(𝐷, ℝ*, < ) ≤ (abs‘(ℑ‘𝐴)))
7977, 56, 78sylancl 697 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ≤ (abs‘(ℑ‘𝐴)))
80 simpr 479 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
8174, 80absimlere 40206 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (abs‘(ℑ‘𝐴)) ≤ (abs‘(𝑦𝐴)))
8267, 71, 76, 79, 81letrd 10384 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → inf(𝐷, ℝ*, < ) ≤ (abs‘(𝑦𝐴)))
8336, 82syl5eqbr 4837 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦𝐴)))
8483ad4ant14 1209 . . . . 5 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦𝐴)))
85 cnrefiisplem.c . . . . . . . . 9 𝐶 = (ℝ ∪ 𝐵)
8685eleq2i 2829 . . . . . . . 8 (𝑦𝐶𝑦 ∈ (ℝ ∪ 𝐵))
87 elunnel1 3895 . . . . . . . 8 ((𝑦 ∈ (ℝ ∪ 𝐵) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦𝐵)
8886, 87sylanb 490 . . . . . . 7 ((𝑦𝐶 ∧ ¬ 𝑦 ∈ ℝ) → 𝑦𝐵)
8988ad4ant24 1213 . . . . . 6 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦𝐵)
9060ad2antrr 764 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → 𝐷 ⊆ ℝ*)
91 simpr 479 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦𝐵)
92 simpll 807 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
9391, 92elind 3939 . . . . . . . . . . . . . . 15 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦 ∈ (𝐵 ∩ ℂ))
94 nelsn 4355 . . . . . . . . . . . . . . . 16 (𝑦𝐴 → ¬ 𝑦 ∈ {𝐴})
9594ad2antlr 765 . . . . . . . . . . . . . . 15 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → ¬ 𝑦 ∈ {𝐴})
9693, 95eldifd 3724 . . . . . . . . . . . . . 14 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}))
97 fvex 6360 . . . . . . . . . . . . . . 15 (abs‘(𝑦𝐴)) ∈ V
9897snid 4351 . . . . . . . . . . . . . 14 (abs‘(𝑦𝐴)) ∈ {(abs‘(𝑦𝐴))}
99 oveq1 6818 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑦 → (𝑤𝐴) = (𝑦𝐴))
10099fveq2d 6354 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑦 → (abs‘(𝑤𝐴)) = (abs‘(𝑦𝐴)))
101100sneqd 4331 . . . . . . . . . . . . . . 15 (𝑤 = 𝑦 → {(abs‘(𝑤𝐴))} = {(abs‘(𝑦𝐴))})
102101eliuni 4676 . . . . . . . . . . . . . 14 ((𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}) ∧ (abs‘(𝑦𝐴)) ∈ {(abs‘(𝑦𝐴))}) → (abs‘(𝑦𝐴)) ∈ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤𝐴))})
10396, 98, 102sylancl 697 . . . . . . . . . . . . 13 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤𝐴))})
104101cbviunv 4709 . . . . . . . . . . . . 13 𝑤 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑤𝐴))} = 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}
105103, 104syl6eleq 2847 . . . . . . . . . . . 12 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))})
106 elun2 3922 . . . . . . . . . . . 12 ((abs‘(𝑦𝐴)) ∈ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))} → (abs‘(𝑦𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
107105, 106syl 17 . . . . . . . . . . 11 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ ({(abs‘(ℑ‘𝐴))} ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦𝐴))}))
108107, 9syl6eleqr 2848 . . . . . . . . . 10 (((𝑦 ∈ ℂ ∧ 𝑦𝐴) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝐷)
109108adantll 752 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → (abs‘(𝑦𝐴)) ∈ 𝐷)
110 infxrlb 12355 . . . . . . . . 9 ((𝐷 ⊆ ℝ* ∧ (abs‘(𝑦𝐴)) ∈ 𝐷) → inf(𝐷, ℝ*, < ) ≤ (abs‘(𝑦𝐴)))
11190, 109, 110syl2anc 696 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → inf(𝐷, ℝ*, < ) ≤ (abs‘(𝑦𝐴)))
11236, 111syl5eqbr 4837 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → 𝑋 ≤ (abs‘(𝑦𝐴)))
113112adantllr 757 . . . . . 6 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ 𝑦𝐵) → 𝑋 ≤ (abs‘(𝑦𝐴)))
11489, 113syldan 488 . . . . 5 ((((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) ∧ ¬ 𝑦 ∈ ℝ) → 𝑋 ≤ (abs‘(𝑦𝐴)))
11584, 114pm2.61dan 867 . . . 4 (((𝜑𝑦𝐶) ∧ (𝑦 ∈ ℂ ∧ 𝑦𝐴)) → 𝑋 ≤ (abs‘(𝑦𝐴)))
116115ex 449 . . 3 ((𝜑𝑦𝐶) → ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴))))
117116ralrimiva 3102 . 2 (𝜑 → ∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴))))
118 breq1 4805 . . . . 5 (𝑥 = 𝑋 → (𝑥 ≤ (abs‘(𝑦𝐴)) ↔ 𝑋 ≤ (abs‘(𝑦𝐴))))
119118imbi2d 329 . . . 4 (𝑥 = 𝑋 → (((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))) ↔ ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴)))))
120119ralbidv 3122 . . 3 (𝑥 = 𝑋 → (∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))) ↔ ∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴)))))
121120rspcev 3447 . 2 ((𝑋 ∈ ℝ+ ∧ ∀𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑋 ≤ (abs‘(𝑦𝐴)))) → ∃𝑥 ∈ ℝ+𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))))
12264, 117, 121syl2anc 696 1 (𝜑 → ∃𝑥 ∈ ℝ+𝑦𝐶 ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1630  wcel 2137  wne 2930  wral 3048  wrex 3049  cdif 3710  cun 3711  cin 3712  wss 3713  c0 4056  {csn 4319   ciun 4670   class class class wbr 4802   Or wor 5184  cfv 6047  (class class class)co 6811  Fincfn 8119  infcinf 8510  cc 10124  cr 10125  *cxr 10263   < clt 10264  cle 10265  cmin 10456  +crp 12023  cim 14035  abscabs 14171
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203  ax-pre-sup 10204
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-int 4626  df-iun 4672  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-om 7229  df-2nd 7332  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-1o 7727  df-oadd 7731  df-er 7909  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-sup 8511  df-inf 8512  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-div 10875  df-nn 11211  df-2 11269  df-3 11270  df-n0 11483  df-z 11568  df-uz 11878  df-rp 12024  df-seq 12994  df-exp 13053  df-cj 14036  df-re 14037  df-im 14038  df-sqrt 14172  df-abs 14173
This theorem is referenced by:  cnrefiisp  40557
  Copyright terms: Public domain W3C validator