dedekindicclemlu - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > dedekindicclemlu		GIF version

Theorem dedekindicclemlu 14585

Description: Lemma for dedekindicc 14588. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.)

**Hypotheses**
Ref	Expression
dedekindicc.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
dedekindicc.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
dedekindicc.lss	⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))
dedekindicc.uss	⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))
dedekindicc.lm	⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
dedekindicc.um	⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)
dedekindicc.lr	⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
dedekindicc.ur	⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
dedekindicc.disj	⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)
dedekindicc.loc	⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))
dedekindicc.ab	⊢ (𝜑 → 𝐴 < 𝐵)

**Assertion**
Ref	Expression
dedekindicclemlu	⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))

Distinct variable groups: 𝐴,𝑞,𝑟,𝑥 𝐵,𝑞,𝑟,𝑥 𝐿,𝑞,𝑟,𝑥 𝑈,𝑞,𝑟 𝜑,𝑞,𝑟,𝑥 Allowed substitution hint: 𝑈(𝑥)

Proof of Theorem dedekindicclemlu Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dedekindicc.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		dedekindicc.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		dedekindicc.lss	. . 3 ⊢ (𝜑 → 𝐿 ⊆ (𝐴[,]𝐵))
4		dedekindicc.uss	. . 3 ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))
5		dedekindicc.lm	. . 3 ⊢ (𝜑 → ∃𝑞 ∈ (𝐴[,]𝐵)𝑞 ∈ 𝐿)
6		dedekindicc.um	. . 3 ⊢ (𝜑 → ∃𝑟 ∈ (𝐴[,]𝐵)𝑟 ∈ 𝑈)
7		dedekindicc.lr	. . 3 ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
8		dedekindicc.ur	. . 3 ⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
9		dedekindicc.disj	. . 3 ⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅)
10		dedekindicc.loc	. . 3 ⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈)))
11		dedekindicc.ab	. . 3 ⊢ (𝜑 → 𝐴 < 𝐵)
12	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11	dedekindicclemlub 14584	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)))
13		simpr 110	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝑞 ∈ 𝐿)
14	3	ad3antrrr 492	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝐿 ⊆ (𝐴[,]𝐵))
15	14, 13	sseldd 3171	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝑞 ∈ (𝐴[,]𝐵))
16		rsp 2537	. . . . . . . . . . 11 ⊢ (∀𝑞 ∈ (𝐴[,]𝐵)(𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟) → (𝑞 ∈ (𝐴[,]𝐵) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)))
17	7, 16	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (𝑞 ∈ (𝐴[,]𝐵) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)))
18	17	ad3antrrr 492	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → (𝑞 ∈ (𝐴[,]𝐵) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)))
19	15, 18	mpd 13	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
20	13, 19	mpbid 147	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)
21		iccssre 9987	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
22	1, 2, 21	syl2anc 411	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
23	22	ad4antr 494	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → (𝐴[,]𝐵) ⊆ ℝ)
24	15	adantr 276	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ (𝐴[,]𝐵))
25	23, 24	sseldd 3171	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ ℝ)
26	3	ad4antr 494	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝐿 ⊆ (𝐴[,]𝐵))
27		simprl 529	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ 𝐿)
28	26, 27	sseldd 3171	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ (𝐴[,]𝐵))
29	23, 28	sseldd 3171	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ ℝ)
30		simp-4r 542	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ (𝐴[,]𝐵))
31	23, 30	sseldd 3171	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ ℝ)
32		simprr 531	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 < 𝑟)
33		breq2 4022	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝑥 < 𝑦 ↔ 𝑥 < 𝑟))
34	33	notbid 668	. . . . . . . . . 10 ⊢ (𝑦 = 𝑟 → (¬ 𝑥 < 𝑦 ↔ ¬ 𝑥 < 𝑟))
35		simprl 529	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦)
36	35	ad2antrr 488	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → ∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦)
37	34, 36, 27	rspcdva 2861	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → ¬ 𝑥 < 𝑟)
38	29, 31, 37	nltled 8109	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ≤ 𝑥)
39	25, 29, 31, 32, 38	ltletrd 8411	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 < 𝑥)
40	20, 39	rexlimddv 2612	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝑞 < 𝑥)
41	40	ralrimiva 2563	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑞 ∈ 𝐿 𝑞 < 𝑥)
42		simpr 110	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑟 ∈ 𝑈)
43		simplll 533	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝜑)
44	4	ad3antrrr 492	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑈 ⊆ (𝐴[,]𝐵))
45	44, 42	sseldd 3171	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑟 ∈ (𝐴[,]𝐵))
46		rsp 2537	. . . . . . . . . 10 ⊢ (∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟) → (𝑟 ∈ (𝐴[,]𝐵) → (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟)))
47	8, 46	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝑟 ∈ (𝐴[,]𝐵) → (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟)))
48	43, 45, 47	sylc 62	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))
49	42, 48	mpbid 147	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → ∃𝑞 ∈ 𝑈 𝑞 < 𝑟)
50	22	ad4antr 494	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → (𝐴[,]𝐵) ⊆ ℝ)
51		simp-4r 542	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ (𝐴[,]𝐵))
52	50, 51	sseldd 3171	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ ℝ)
53	4	ad4antr 494	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑈 ⊆ (𝐴[,]𝐵))
54		simprl 529	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ 𝑈)
55	53, 54	sseldd 3171	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ (𝐴[,]𝐵))
56	50, 55	sseldd 3171	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ ℝ)
57	45	adantr 276	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ (𝐴[,]𝐵))
58	50, 57	sseldd 3171	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ ℝ)
59	54	adantr 276	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ 𝑈)
60	43	ad2antrr 488	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝜑)
61		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 < 𝑥)
62		breq1 4021	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑞 → (𝑦 < 𝑥 ↔ 𝑞 < 𝑥))
63		breq1 4021	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑞 → (𝑦 < 𝑧 ↔ 𝑞 < 𝑧))
64	63	rexbidv 2491	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑞 → (∃𝑧 ∈ 𝐿 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐿 𝑞 < 𝑧))
65	62, 64	imbi12d 234	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑞 → ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧) ↔ (𝑞 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑞 < 𝑧)))
66		simprr 531	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))
67	66	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))
68	55	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ (𝐴[,]𝐵))
69	65, 67, 68	rspcdva 2861	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑞 < 𝑧))
70	61, 69	mpd 13	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑧 ∈ 𝐿 𝑞 < 𝑧)
71		breq2 4022	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑟 → (𝑞 < 𝑧 ↔ 𝑞 < 𝑟))
72	71	cbvrexv 2719	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ 𝐿 𝑞 < 𝑧 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)
73	70, 72	sylib 122	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)
74	60, 68, 17	sylc 62	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))
75	73, 74	mpbird 167	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ 𝐿)
76		disj 3486	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∩ 𝑈) = ∅ ↔ ∀𝑞 ∈ 𝐿 ¬ 𝑞 ∈ 𝑈)
77	9, 76	sylib 122	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑞 ∈ 𝐿 ¬ 𝑞 ∈ 𝑈)
78	77	r19.21bi 2578	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐿) → ¬ 𝑞 ∈ 𝑈)
79	60, 75, 78	syl2anc 411	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ¬ 𝑞 ∈ 𝑈)
80	59, 79	pm2.65da 662	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → ¬ 𝑞 < 𝑥)
81	52, 56, 80	nltled 8109	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 ≤ 𝑞)
82		simprr 531	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 < 𝑟)
83	52, 56, 58, 81, 82	lelttrd 8113	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 < 𝑟)
84	49, 83	rexlimddv 2612	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑥 < 𝑟)
85	84	ralrimiva 2563	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)
86	41, 85	jca 306	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))
87	86	ex 115	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)) → (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)))
88	87	reximdva 2592	. 2 ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)) → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)))
89	12, 88	mpd 13	1 ⊢ (𝜑 → ∃𝑥 ∈ (𝐴[,]𝐵)(∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 = wceq 1364 ∈ wcel 2160 ∀wral 2468 ∃wrex 2469 ∩ cin 3143 ⊆ wss 3144 ∅c0 3437 class class class wbr 4018 (class class class)co 5897 ℝcr 7841 < clt 8023 [,]cicc 9923

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4192 ax-pr 4227 ax-un 4451 ax-setind 4554 ax-iinf 4605 ax-cnex 7933 ax-resscn 7934 ax-1cn 7935 ax-1re 7936 ax-icn 7937 ax-addcl 7938 ax-addrcl 7939 ax-mulcl 7940 ax-mulrcl 7941 ax-addcom 7942 ax-mulcom 7943 ax-addass 7944 ax-mulass 7945 ax-distr 7946 ax-i2m1 7947 ax-0lt1 7948 ax-1rid 7949 ax-0id 7950 ax-rnegex 7951 ax-precex 7952 ax-cnre 7953 ax-pre-ltirr 7954 ax-pre-ltwlin 7955 ax-pre-lttrn 7956 ax-pre-apti 7957 ax-pre-ltadd 7958 ax-pre-mulgt0 7959 ax-pre-mulext 7960 ax-arch 7961 ax-caucvg 7962 ax-pre-suploc 7963

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rmo 2476 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-if 3550 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4311 df-po 4314 df-iso 4315 df-iord 4384 df-on 4386 df-ilim 4387 df-suc 4389 df-iom 4608 df-xp 4650 df-rel 4651 df-cnv 4652 df-co 4653 df-dm 4654 df-rn 4655 df-res 4656 df-ima 4657 df-iota 5196 df-fun 5237 df-fn 5238 df-f 5239 df-f1 5240 df-fo 5241 df-f1o 5242 df-fv 5243 df-isom 5244 df-riota 5852 df-ov 5900 df-oprab 5901 df-mpo 5902 df-1st 6166 df-2nd 6167 df-recs 6331 df-frec 6417 df-sup 7014 df-inf 7015 df-pnf 8025 df-mnf 8026 df-xr 8027 df-ltxr 8028 df-le 8029 df-sub 8161 df-neg 8162 df-reap 8563 df-ap 8570 df-div 8661 df-inn 8951 df-2 9009 df-3 9010 df-4 9011 df-n0 9208 df-z 9285 df-uz 9560 df-rp 9686 df-icc 9927 df-seqfrec 10479 df-exp 10554 df-cj 10886 df-re 10887 df-im 10888 df-rsqrt 11042 df-abs 11043

This theorem is referenced by: dedekindicclemicc 14587

W3C validator