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

Theorem qndenserrnbllem 39818
Description: n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
Hypotheses
Ref Expression
qndenserrnbllem.i (𝜑𝐼 ∈ Fin)
qndenserrnbllem.n (𝜑𝐼 ≠ ∅)
qndenserrnbllem.x (𝜑𝑋 ∈ (ℝ ↑𝑚 𝐼))
qndenserrnbllem.d 𝐷 = (dist‘(ℝ^‘𝐼))
qndenserrnbllem.e (𝜑𝐸 ∈ ℝ+)
Assertion
Ref Expression
qndenserrnbllem (𝜑 → ∃𝑦 ∈ (ℚ ↑𝑚 𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸))
Distinct variable groups:   𝑦,𝐸   𝑦,𝐼   𝑦,𝑋   𝜑,𝑦
Allowed substitution hint:   𝐷(𝑦)

Proof of Theorem qndenserrnbllem
Dummy variables 𝑖 𝑘 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qndenserrnbllem.i . . . 4 (𝜑𝐼 ∈ Fin)
2 inss1 3811 . . . . . 6 (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ⊆ ℚ
3 qex 11744 . . . . . 6 ℚ ∈ V
4 ssexg 4764 . . . . . 6 (((ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ⊆ ℚ ∧ ℚ ∈ V) → (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ∈ V)
52, 3, 4mp2an 707 . . . . 5 (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ∈ V
65a1i 11 . . . 4 ((𝜑𝑘𝐼) → (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ∈ V)
7 qndenserrnbllem.x . . . . . . . . . . . 12 (𝜑𝑋 ∈ (ℝ ↑𝑚 𝐼))
8 elmapi 7823 . . . . . . . . . . . 12 (𝑋 ∈ (ℝ ↑𝑚 𝐼) → 𝑋:𝐼⟶ℝ)
97, 8syl 17 . . . . . . . . . . 11 (𝜑𝑋:𝐼⟶ℝ)
109adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐼) → 𝑋:𝐼⟶ℝ)
11 simpr 477 . . . . . . . . . 10 ((𝜑𝑘𝐼) → 𝑘𝐼)
1210, 11ffvelrnd 6316 . . . . . . . . 9 ((𝜑𝑘𝐼) → (𝑋𝑘) ∈ ℝ)
1312rexrd 10033 . . . . . . . 8 ((𝜑𝑘𝐼) → (𝑋𝑘) ∈ ℝ*)
14 qndenserrnbllem.e . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ+)
1514rpred 11816 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℝ)
1615adantr 481 . . . . . . . . . . 11 ((𝜑𝑘𝐼) → 𝐸 ∈ ℝ)
17 ne0i 3897 . . . . . . . . . . . . . . 15 (𝑘𝐼𝐼 ≠ ∅)
1817adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐼) → 𝐼 ≠ ∅)
19 hashnncl 13097 . . . . . . . . . . . . . . . 16 (𝐼 ∈ Fin → ((#‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅))
201, 19syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((#‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅))
2120adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐼) → ((#‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅))
2218, 21mpbird 247 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → (#‘𝐼) ∈ ℕ)
2322nnred 10979 . . . . . . . . . . . 12 ((𝜑𝑘𝐼) → (#‘𝐼) ∈ ℝ)
24 0red 9985 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → 0 ∈ ℝ)
2522nngt0d 11008 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → 0 < (#‘𝐼))
2624, 23, 25ltled 10129 . . . . . . . . . . . 12 ((𝜑𝑘𝐼) → 0 ≤ (#‘𝐼))
2723, 26resqrtcld 14090 . . . . . . . . . . 11 ((𝜑𝑘𝐼) → (√‘(#‘𝐼)) ∈ ℝ)
2823, 25elrpd 11813 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → (#‘𝐼) ∈ ℝ+)
2928sqrtgt0d 14085 . . . . . . . . . . . 12 ((𝜑𝑘𝐼) → 0 < (√‘(#‘𝐼)))
3024, 29gtned 10116 . . . . . . . . . . 11 ((𝜑𝑘𝐼) → (√‘(#‘𝐼)) ≠ 0)
3116, 27, 30redivcld 10797 . . . . . . . . . 10 ((𝜑𝑘𝐼) → (𝐸 / (√‘(#‘𝐼))) ∈ ℝ)
3212, 31readdcld 10013 . . . . . . . . 9 ((𝜑𝑘𝐼) → ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ)
3332rexrd 10033 . . . . . . . 8 ((𝜑𝑘𝐼) → ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ*)
3414adantr 481 . . . . . . . . . 10 ((𝜑𝑘𝐼) → 𝐸 ∈ ℝ+)
3527, 29elrpd 11813 . . . . . . . . . 10 ((𝜑𝑘𝐼) → (√‘(#‘𝐼)) ∈ ℝ+)
3634, 35rpdivcld 11833 . . . . . . . . 9 ((𝜑𝑘𝐼) → (𝐸 / (√‘(#‘𝐼))) ∈ ℝ+)
3712, 36ltaddrpd 11849 . . . . . . . 8 ((𝜑𝑘𝐼) → (𝑋𝑘) < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))
38 qbtwnxr 11974 . . . . . . . 8 (((𝑋𝑘) ∈ ℝ* ∧ ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ* ∧ (𝑋𝑘) < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))) → ∃𝑞 ∈ ℚ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))
3913, 33, 37, 38syl3anc 1323 . . . . . . 7 ((𝜑𝑘𝐼) → ∃𝑞 ∈ ℚ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))
40 df-rex 2913 . . . . . . 7 (∃𝑞 ∈ ℚ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))) ↔ ∃𝑞(𝑞 ∈ ℚ ∧ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))
4139, 40sylib 208 . . . . . 6 ((𝜑𝑘𝐼) → ∃𝑞(𝑞 ∈ ℚ ∧ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))
42 simprl 793 . . . . . . . . 9 (((𝜑𝑘𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → 𝑞 ∈ ℚ)
4313adantr 481 . . . . . . . . . 10 (((𝜑𝑘𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → (𝑋𝑘) ∈ ℝ*)
4433adantr 481 . . . . . . . . . 10 (((𝜑𝑘𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ*)
45 qre 11737 . . . . . . . . . . 11 (𝑞 ∈ ℚ → 𝑞 ∈ ℝ)
4645ad2antrl 763 . . . . . . . . . 10 (((𝜑𝑘𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → 𝑞 ∈ ℝ)
47 simprrl 803 . . . . . . . . . 10 (((𝜑𝑘𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → (𝑋𝑘) < 𝑞)
48 simprrr 804 . . . . . . . . . 10 (((𝜑𝑘𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → 𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))
4943, 44, 46, 47, 48eliood 39128 . . . . . . . . 9 (((𝜑𝑘𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → 𝑞 ∈ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))
5042, 49elind 3776 . . . . . . . 8 (((𝜑𝑘𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → 𝑞 ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))
5150ex 450 . . . . . . 7 ((𝜑𝑘𝐼) → ((𝑞 ∈ ℚ ∧ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) → 𝑞 ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))))
5251eximdv 1843 . . . . . 6 ((𝜑𝑘𝐼) → (∃𝑞(𝑞 ∈ ℚ ∧ ((𝑋𝑘) < 𝑞𝑞 < ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) → ∃𝑞 𝑞 ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))))
5341, 52mpd 15 . . . . 5 ((𝜑𝑘𝐼) → ∃𝑞 𝑞 ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))
54 n0 3907 . . . . 5 ((ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ≠ ∅ ↔ ∃𝑞 𝑞 ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))
5553, 54sylibr 224 . . . 4 ((𝜑𝑘𝐼) → (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ≠ ∅)
561, 6, 55choicefi 38863 . . 3 (𝜑 → ∃𝑦(𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))))
572a1i 11 . . . . . . . . . . . 12 (𝑦 Fn 𝐼 → (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ⊆ ℚ)
5857sseld 3582 . . . . . . . . . . 11 (𝑦 Fn 𝐼 → ((𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) → (𝑦𝑘) ∈ ℚ))
5958ralimdv 2957 . . . . . . . . . 10 (𝑦 Fn 𝐼 → (∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) → ∀𝑘𝐼 (𝑦𝑘) ∈ ℚ))
6059imdistani 725 . . . . . . . . 9 ((𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ ℚ))
61 ffnfv 6343 . . . . . . . . 9 (𝑦:𝐼⟶ℚ ↔ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ ℚ))
6260, 61sylibr 224 . . . . . . . 8 ((𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → 𝑦:𝐼⟶ℚ)
6362adantl 482 . . . . . . 7 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝑦:𝐼⟶ℚ)
643a1i 11 . . . . . . . . 9 (𝜑 → ℚ ∈ V)
65 elmapg 7815 . . . . . . . . 9 ((ℚ ∈ V ∧ 𝐼 ∈ Fin) → (𝑦 ∈ (ℚ ↑𝑚 𝐼) ↔ 𝑦:𝐼⟶ℚ))
6664, 1, 65syl2anc 692 . . . . . . . 8 (𝜑 → (𝑦 ∈ (ℚ ↑𝑚 𝐼) ↔ 𝑦:𝐼⟶ℚ))
6766adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝑦 ∈ (ℚ ↑𝑚 𝐼) ↔ 𝑦:𝐼⟶ℚ))
6863, 67mpbird 247 . . . . . 6 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝑦 ∈ (ℚ ↑𝑚 𝐼))
69 reex 9971 . . . . . . . . . . 11 ℝ ∈ V
7045ssriv 3587 . . . . . . . . . . 11 ℚ ⊆ ℝ
71 mapss 7844 . . . . . . . . . . 11 ((ℝ ∈ V ∧ ℚ ⊆ ℝ) → (ℚ ↑𝑚 𝐼) ⊆ (ℝ ↑𝑚 𝐼))
7269, 70, 71mp2an 707 . . . . . . . . . 10 (ℚ ↑𝑚 𝐼) ⊆ (ℝ ↑𝑚 𝐼)
7372a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (ℚ ↑𝑚 𝐼) ⊆ (ℝ ↑𝑚 𝐼))
7473, 68sseldd 3584 . . . . . . . 8 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝑦 ∈ (ℝ ↑𝑚 𝐼))
751adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝐼 ∈ Fin)
76 qndenserrnbllem.n . . . . . . . . . . 11 (𝜑𝐼 ≠ ∅)
7776adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝐼 ≠ ∅)
78 eqid 2621 . . . . . . . . . 10 (#‘𝐼) = (#‘𝐼)
797adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝑋 ∈ (ℝ ↑𝑚 𝐼))
80 simpll 789 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) ∧ 𝑖𝐼) → 𝜑)
81 fveq2 6148 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (𝑦𝑘) = (𝑦𝑖))
82 fveq2 6148 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (𝑋𝑘) = (𝑋𝑖))
8382oveq1d 6619 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → ((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))) = ((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))
8482, 83oveq12d 6622 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))) = ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))))
8584ineq2d 3792 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) = (ℚ ∩ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))))
8681, 85eleq12d 2692 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → ((𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ↔ (𝑦𝑖) ∈ (ℚ ∩ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))))))
8786cbvralv 3159 . . . . . . . . . . . . . . . . 17 (∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ↔ ∀𝑖𝐼 (𝑦𝑖) ∈ (ℚ ∩ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))))
8887biimpi 206 . . . . . . . . . . . . . . . 16 (∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) → ∀𝑖𝐼 (𝑦𝑖) ∈ (ℚ ∩ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))))
8988adantr 481 . . . . . . . . . . . . . . 15 ((∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ∧ 𝑖𝐼) → ∀𝑖𝐼 (𝑦𝑖) ∈ (ℚ ∩ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))))
90 simpr 477 . . . . . . . . . . . . . . 15 ((∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ∧ 𝑖𝐼) → 𝑖𝐼)
91 rspa 2925 . . . . . . . . . . . . . . 15 ((∀𝑖𝐼 (𝑦𝑖) ∈ (ℚ ∩ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))) ∧ 𝑖𝐼) → (𝑦𝑖) ∈ (ℚ ∩ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))))
9289, 90, 91syl2anc 692 . . . . . . . . . . . . . 14 ((∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ∧ 𝑖𝐼) → (𝑦𝑖) ∈ (ℚ ∩ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))))
9392adantll 749 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) ∧ 𝑖𝐼) → (𝑦𝑖) ∈ (ℚ ∩ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))))
94 elinel2 3778 . . . . . . . . . . . . 13 ((𝑦𝑖) ∈ (ℚ ∩ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))) → (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))))
9593, 94syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) ∧ 𝑖𝐼) → (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))))
96 simpr 477 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) ∧ 𝑖𝐼) → 𝑖𝐼)
979ffvelrnda 6315 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐼) → (𝑋𝑖) ∈ ℝ)
98973adant2 1078 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → (𝑋𝑖) ∈ ℝ)
99 simp2 1060 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))))
10099elioored 39184 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → (𝑦𝑖) ∈ ℝ)
10198rexrd 10033 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → (𝑋𝑖) ∈ ℝ*)
10215adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → 𝐸 ∈ ℝ)
10376, 20mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (#‘𝐼) ∈ ℕ)
104103nnred 10979 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (#‘𝐼) ∈ ℝ)
105104adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → (#‘𝐼) ∈ ℝ)
106 0red 9985 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ∈ ℝ)
107103nngt0d 11008 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 < (#‘𝐼))
108106, 104, 107ltled 10129 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 0 ≤ (#‘𝐼))
109108adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝐼) → 0 ≤ (#‘𝐼))
110105, 109resqrtcld 14090 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (√‘(#‘𝐼)) ∈ ℝ)
111 sqrtgt0 13933 . . . . . . . . . . . . . . . . . . . . . . 23 (((#‘𝐼) ∈ ℝ ∧ 0 < (#‘𝐼)) → 0 < (√‘(#‘𝐼)))
112104, 107, 111syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 0 < (√‘(#‘𝐼)))
113106, 112gtned 10116 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (√‘(#‘𝐼)) ≠ 0)
114113adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝐼) → (√‘(#‘𝐼)) ≠ 0)
115102, 110, 114redivcld 10797 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝐼) → (𝐸 / (√‘(#‘𝐼))) ∈ ℝ)
11697, 115readdcld 10013 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖𝐼) → ((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ)
117116rexrd 10033 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖𝐼) → ((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ*)
1181173adant2 1078 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → ((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ*)
119 ioogtlb 39125 . . . . . . . . . . . . . . . 16 (((𝑋𝑖) ∈ ℝ* ∧ ((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ* ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))) → (𝑋𝑖) < (𝑦𝑖))
120101, 118, 99, 119syl3anc 1323 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → (𝑋𝑖) < (𝑦𝑖))
12198, 100, 120ltled 10129 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → (𝑋𝑖) ≤ (𝑦𝑖))
12298, 100, 121abssuble0d 14105 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → (abs‘((𝑋𝑖) − (𝑦𝑖))) = ((𝑦𝑖) − (𝑋𝑖)))
1231163adant2 1078 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → ((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ)
124 iooltub 39143 . . . . . . . . . . . . . . . 16 (((𝑋𝑖) ∈ ℝ* ∧ ((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ* ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))) → (𝑦𝑖) < ((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))
125101, 118, 99, 124syl3anc 1323 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → (𝑦𝑖) < ((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))))
126100, 123, 98, 125ltsub1dd 10583 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → ((𝑦𝑖) − (𝑋𝑖)) < (((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))) − (𝑋𝑖)))
12798recnd 10012 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → (𝑋𝑖) ∈ ℂ)
128104, 108resqrtcld 14090 . . . . . . . . . . . . . . . . . 18 (𝜑 → (√‘(#‘𝐼)) ∈ ℝ)
12915, 128, 113redivcld 10797 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸 / (√‘(#‘𝐼))) ∈ ℝ)
130129recnd 10012 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 / (√‘(#‘𝐼))) ∈ ℂ)
1311303ad2ant1 1080 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → (𝐸 / (√‘(#‘𝐼))) ∈ ℂ)
132127, 131pncan2d 10338 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → (((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼)))) − (𝑋𝑖)) = (𝐸 / (√‘(#‘𝐼))))
133126, 132breqtrd 4639 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → ((𝑦𝑖) − (𝑋𝑖)) < (𝐸 / (√‘(#‘𝐼))))
134122, 133eqbrtrd 4635 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑖) ∈ ((𝑋𝑖)(,)((𝑋𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖𝐼) → (abs‘((𝑋𝑖) − (𝑦𝑖))) < (𝐸 / (√‘(#‘𝐼))))
13580, 95, 96, 134syl3anc 1323 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) ∧ 𝑖𝐼) → (abs‘((𝑋𝑖) − (𝑦𝑖))) < (𝐸 / (√‘(#‘𝐼))))
136135adantlrl 755 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) ∧ 𝑖𝐼) → (abs‘((𝑋𝑖) − (𝑦𝑖))) < (𝐸 / (√‘(#‘𝐼))))
13714adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝐸 ∈ ℝ+)
138104, 107elrpd 11813 . . . . . . . . . . . . 13 (𝜑 → (#‘𝐼) ∈ ℝ+)
139138adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (#‘𝐼) ∈ ℝ+)
140139rpsqrtcld 14084 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (√‘(#‘𝐼)) ∈ ℝ+)
141137, 140rpdivcld 11833 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝐸 / (√‘(#‘𝐼))) ∈ ℝ+)
142 qndenserrnbllem.d . . . . . . . . . 10 𝐷 = (dist‘(ℝ^‘𝐼))
14375, 77, 78, 79, 74, 136, 141, 142rrndistlt 39814 . . . . . . . . 9 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝑋𝐷𝑦) < ((√‘(#‘𝐼)) · (𝐸 / (√‘(#‘𝐼)))))
144137rpcnd 11818 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝐸 ∈ ℂ)
145139rpcnd 11818 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (#‘𝐼) ∈ ℂ)
146145sqrtcld 14110 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (√‘(#‘𝐼)) ∈ ℂ)
147140rpne0d 11821 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (√‘(#‘𝐼)) ≠ 0)
148144, 146, 147divcan2d 10747 . . . . . . . . 9 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → ((√‘(#‘𝐼)) · (𝐸 / (√‘(#‘𝐼)))) = 𝐸)
149143, 148breqtrd 4639 . . . . . . . 8 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝑋𝐷𝑦) < 𝐸)
15074, 149jca 554 . . . . . . 7 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝑦 ∈ (ℝ ↑𝑚 𝐼) ∧ (𝑋𝐷𝑦) < 𝐸))
151142rrxmetfi 39811 . . . . . . . . . . 11 (𝐼 ∈ Fin → 𝐷 ∈ (Met‘(ℝ ↑𝑚 𝐼)))
1521, 151syl 17 . . . . . . . . . 10 (𝜑𝐷 ∈ (Met‘(ℝ ↑𝑚 𝐼)))
153 metxmet 22049 . . . . . . . . . 10 (𝐷 ∈ (Met‘(ℝ ↑𝑚 𝐼)) → 𝐷 ∈ (∞Met‘(ℝ ↑𝑚 𝐼)))
154152, 153syl 17 . . . . . . . . 9 (𝜑𝐷 ∈ (∞Met‘(ℝ ↑𝑚 𝐼)))
15515rexrd 10033 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ*)
156 elbl 22103 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘(ℝ ↑𝑚 𝐼)) ∧ 𝑋 ∈ (ℝ ↑𝑚 𝐼) ∧ 𝐸 ∈ ℝ*) → (𝑦 ∈ (𝑋(ball‘𝐷)𝐸) ↔ (𝑦 ∈ (ℝ ↑𝑚 𝐼) ∧ (𝑋𝐷𝑦) < 𝐸)))
157154, 7, 155, 156syl3anc 1323 . . . . . . . 8 (𝜑 → (𝑦 ∈ (𝑋(ball‘𝐷)𝐸) ↔ (𝑦 ∈ (ℝ ↑𝑚 𝐼) ∧ (𝑋𝐷𝑦) < 𝐸)))
158157adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝑦 ∈ (𝑋(ball‘𝐷)𝐸) ↔ (𝑦 ∈ (ℝ ↑𝑚 𝐼) ∧ (𝑋𝐷𝑦) < 𝐸)))
159150, 158mpbird 247 . . . . . 6 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝑦 ∈ (𝑋(ball‘𝐷)𝐸))
16068, 159jca 554 . . . . 5 ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝑦 ∈ (ℚ ↑𝑚 𝐼) ∧ 𝑦 ∈ (𝑋(ball‘𝐷)𝐸)))
161160ex 450 . . . 4 (𝜑 → ((𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → (𝑦 ∈ (ℚ ↑𝑚 𝐼) ∧ 𝑦 ∈ (𝑋(ball‘𝐷)𝐸))))
162161eximdv 1843 . . 3 (𝜑 → (∃𝑦(𝑦 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑦𝑘) ∈ (ℚ ∩ ((𝑋𝑘)(,)((𝑋𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → ∃𝑦(𝑦 ∈ (ℚ ↑𝑚 𝐼) ∧ 𝑦 ∈ (𝑋(ball‘𝐷)𝐸))))
16356, 162mpd 15 . 2 (𝜑 → ∃𝑦(𝑦 ∈ (ℚ ↑𝑚 𝐼) ∧ 𝑦 ∈ (𝑋(ball‘𝐷)𝐸)))
164 df-rex 2913 . 2 (∃𝑦 ∈ (ℚ ↑𝑚 𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸) ↔ ∃𝑦(𝑦 ∈ (ℚ ↑𝑚 𝐼) ∧ 𝑦 ∈ (𝑋(ball‘𝐷)𝐸)))
165163, 164sylibr 224 1 (𝜑 → ∃𝑦 ∈ (ℚ ↑𝑚 𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3186  cin 3554  wss 3555  c0 3891   class class class wbr 4613   Fn wfn 5842  wf 5843  cfv 5847  (class class class)co 6604  𝑚 cmap 7802  Fincfn 7899  cc 9878  cr 9879  0cc0 9880   + caddc 9883   · cmul 9885  *cxr 10017   < clt 10018  cle 10019  cmin 10210   / cdiv 10628  cn 10964  cq 11732  +crp 11776  (,)cioo 12117  #chash 13057  csqrt 13907  abscabs 13908  distcds 15871  ∞Metcxmt 19650  Metcme 19651  ballcbl 19652  ℝ^crrx 23079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958  ax-addf 9959  ax-mulf 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-tpos 7297  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-map 7804  df-ixp 7853  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-q 11733  df-rp 11777  df-xadd 11891  df-ioo 12121  df-ico 12123  df-fz 12269  df-fzo 12407  df-seq 12742  df-exp 12801  df-hash 13058  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-clim 14153  df-sum 14351  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-mulr 15876  df-starv 15877  df-sca 15878  df-vsca 15879  df-ip 15880  df-tset 15881  df-ple 15882  df-ds 15885  df-unif 15886  df-hom 15887  df-cco 15888  df-0g 16023  df-gsum 16024  df-prds 16029  df-pws 16031  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-mhm 17256  df-grp 17346  df-minusg 17347  df-sbg 17348  df-subg 17512  df-ghm 17579  df-cntz 17671  df-cmn 18116  df-abl 18117  df-mgp 18411  df-ur 18423  df-ring 18470  df-cring 18471  df-oppr 18544  df-dvdsr 18562  df-unit 18563  df-invr 18593  df-dvr 18604  df-rnghom 18636  df-drng 18670  df-field 18671  df-subrg 18699  df-staf 18766  df-srng 18767  df-lmod 18786  df-lss 18852  df-sra 19091  df-rgmod 19092  df-psmet 19657  df-xmet 19658  df-met 19659  df-bl 19660  df-cnfld 19666  df-refld 19870  df-dsmm 19995  df-frlm 20010  df-nm 22297  df-tng 22299  df-tch 22877  df-rrx 23081
This theorem is referenced by:  qndenserrnbl  39819
  Copyright terms: Public domain W3C validator