metakunt29 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > metakunt29		Structured version Visualization version GIF version

Theorem metakunt29 41740

Description: Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)

**Hypotheses**
Ref	Expression
metakunt29.1	⊢ (𝜑 → 𝑀 ∈ ℕ)
metakunt29.2	⊢ (𝜑 → 𝐼 ∈ ℕ)
metakunt29.3	⊢ (𝜑 → 𝐼 ≤ 𝑀)
metakunt29.4	⊢ (𝜑 → 𝑋 ∈ (1...𝑀))
metakunt29.5	⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))
metakunt29.6	⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))
metakunt29.7	⊢ (𝜑 → ¬ 𝑋 = 𝐼)
metakunt29.8	⊢ (𝜑 → 𝑋 < 𝐼)
metakunt29.9	⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))
metakunt29.10	⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)

**Assertion**
Ref	Expression
metakunt29	⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))

Distinct variable groups: 𝑦,𝐻 𝑦,𝐼 𝑧,𝐼 𝑥,𝑀 𝑦,𝑀 𝑧,𝑀 𝑥,𝑋 𝑦,𝑋 𝑧,𝑋 𝜑,𝑥 𝜑,𝑦 𝜑,𝑧 Allowed substitution hints: 𝐴(𝑥,𝑦,𝑧) 𝐵(𝑥,𝑦,𝑧) 𝐶(𝑥,𝑦,𝑧) 𝐻(𝑥,𝑧) 𝐼(𝑥)

**Proof of Theorem metakunt29**
Step	Hyp	Ref	Expression
1		metakunt29.1	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
2		metakunt29.2	. . . 4 ⊢ (𝜑 → 𝐼 ∈ ℕ)
3		metakunt29.3	. . . 4 ⊢ (𝜑 → 𝐼 ≤ 𝑀)
4		metakunt29.4	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))
5		metakunt29.5	. . . 4 ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))
6		metakunt29.6	. . . 4 ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))
7		metakunt29.7	. . . 4 ⊢ (𝜑 → ¬ 𝑋 = 𝐼)
8		metakunt29.8	. . . 4 ⊢ (𝜑 → 𝑋 < 𝐼)
9	1, 2, 3, 4, 5, 6, 7, 8	metakunt27 41738	. . 3 ⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 + (𝑀 − 𝐼)))
10	9	fveq2d 6895	. 2 ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = (𝐶‘(𝑋 + (𝑀 − 𝐼))))
11		metakunt29.9	. . . 4 ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))
12	11	a1i 11	. . 3 ⊢ (𝜑 → 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))))
13		elfznn 13560	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ)
14	4, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ℕ)
15		nnre 12247	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℕ → 𝑋 ∈ ℝ)
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
17	1	nnred 12255	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
18	2	nnred 12255	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℝ)
19	17, 18	resubcld 11670	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℝ)
20	16, 19	readdcld 11271	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ)
21	16	recnd 11270	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ℂ)
22	17	recnd 11270	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
23	18	recnd 11270	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℂ)
24	21, 22, 23	addsub12d 11622	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) = (𝑀 + (𝑋 − 𝐼)))
25	22, 23, 21	subsub2d 11628	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) = (𝑀 + (𝑋 − 𝐼)))
26	18, 16	resubcld 11670	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 − 𝑋) ∈ ℝ)
27	16, 18	posdifd 11829	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 < 𝐼 ↔ 0 < (𝐼 − 𝑋)))
28	8, 27	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (𝐼 − 𝑋))
29	26, 28	elrpd 13043	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 − 𝑋) ∈ ℝ⁺)
30	17, 29	ltsubrpd 13078	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) < 𝑀)
31	25, 30	eqbrtrrd 5167	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 + (𝑋 − 𝐼)) < 𝑀)
32	24, 31	eqbrtrd 5165	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) < 𝑀)
33	20, 32	ltned 11378	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀)
34	33	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀)
35		simpr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
36	35	neeq1d 2990	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑦 ≠ 𝑀 ↔ (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀))
37	34, 36	mpbird 256	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 ≠ 𝑀)
38	37	neneqd 2935	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 = 𝑀)
39	38	iffalsed 4535	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))
40		simpr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
41	18	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ∈ ℝ)
42	16	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑋 ∈ ℝ)
43	17	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑀 ∈ ℝ)
44	43, 41	resubcld 11670	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑀 − 𝐼) ∈ ℝ)
45	42, 44	readdcld 11271	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ)
46	41, 45	lenltd 11388	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
47	40, 46	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)
48	47	3adant2 1128	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)
49		simp2 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
50	49	breq1d 5153	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
51	50	notbid 317	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (¬ 𝑦 < 𝐼 ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
52	48, 51	mpbird 256	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 < 𝐼)
53	52	iffalsed 4535	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = (𝑦 + 1))
54	49	oveq1d 7430	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 + 1) = ((𝑋 + (𝑀 − 𝐼)) + 1))
55	53, 54	eqtrd 2765	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 1))
56		simp3 1135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
57	56	iftrued 4532	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 1)
58	57	eqcomd 2731	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
59		metakunt29.10	. . . . . . . . 9 ⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)
60	58, 59	eqtr4di 2783	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = 𝐻)
61	60	oveq2d 7431	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ((𝑋 + (𝑀 − 𝐼)) + 1) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
62	55, 61	eqtrd 2765	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
63	62	3expa 1115	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
64	20, 18	ltnled 11389	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 ↔ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))))
65	64	biimprd 247	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) < 𝐼))
66	65	imp 405	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼)
67	66	3adant2 1128	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼)
68		simp2 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
69	68	breq1d 5153	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
70	67, 69	mpbird 256	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 < 𝐼)
71	70	iftrued 4532	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = 𝑦)
72	21	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑋 ∈ ℂ)
73	22	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑀 ∈ ℂ)
74	23	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐼 ∈ ℂ)
75	73, 74	subcld 11599	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑀 − 𝐼) ∈ ℂ)
76	72, 75	addcld 11261	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) ∈ ℂ)
77	76	addridd 11442	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = (𝑋 + (𝑀 − 𝐼)))
78	77	eqcomd 2731	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 0))
79	64	biimpa 475	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
80	79	iffalsed 4535	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 0)
81	80	eqcomd 2731	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
82	59	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
83	82	eqcomd 2731	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 𝐻)
84	81, 83	eqtrd 2765	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = 𝐻)
85	84	oveq2d 7431	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
86	78, 85	eqtrd 2765	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
87	86	ex 411	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)))
88	65, 87	syld 47	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)))
89	88	imp 405	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
90	89	3adant2 1128	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
91	68, 90	eqtrd 2765	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
92	71, 91	eqtrd 2765	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
93	92	3expa 1115	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
94	63, 93	pm2.61dan 811	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
95	39, 94	eqtrd 2765	. . 3 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
96		1zzd 12621	. . . 4 ⊢ (𝜑 → 1 ∈ ℤ)
97	1	nnzd 12613	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℤ)
98	14	nnzd 12613	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℤ)
99	2	nnzd 12613	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
100	97, 99	zsubcld 12699	. . . . 5 ⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℤ)
101	98, 100	zaddcld 12698	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ)
102		1p0e1 12364	. . . . 5 ⊢ (1 + 0) = 1
103		1red 11243	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
104		0red 11245	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
105	14	nnge1d 12288	. . . . . 6 ⊢ (𝜑 → 1 ≤ 𝑋)
106	17, 18	subge0d 11832	. . . . . . 7 ⊢ (𝜑 → (0 ≤ (𝑀 − 𝐼) ↔ 𝐼 ≤ 𝑀))
107	3, 106	mpbird 256	. . . . . 6 ⊢ (𝜑 → 0 ≤ (𝑀 − 𝐼))
108	103, 104, 16, 19, 105, 107	le2addd 11861	. . . . 5 ⊢ (𝜑 → (1 + 0) ≤ (𝑋 + (𝑀 − 𝐼)))
109	102, 108	eqbrtrrid 5179	. . . 4 ⊢ (𝜑 → 1 ≤ (𝑋 + (𝑀 − 𝐼)))
110	20, 17, 32	ltled 11390	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≤ 𝑀)
111	96, 97, 101, 109, 110	elfzd 13522	. . 3 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ (1...𝑀))
112	111	elfzelzd 13532	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ)
113		0zd 12598	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℤ)
114	96, 113	ifcld 4570	. . . . 5 ⊢ (𝜑 → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ)
115	59	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
116	115	eleq1d 2810	. . . . 5 ⊢ (𝜑 → (𝐻 ∈ ℤ ↔ if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ))
117	114, 116	mpbird 256	. . . 4 ⊢ (𝜑 → 𝐻 ∈ ℤ)
118	112, 117	zaddcld 12698	. . 3 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) + 𝐻) ∈ ℤ)
119	12, 95, 111, 118	fvmptd 7006	. 2 ⊢ (𝜑 → (𝐶‘(𝑋 + (𝑀 − 𝐼))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
120	10, 119	eqtrd 2765	1 ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ≠ wne 2930 ifcif 4524 class class class wbr 5143 ↦ cmpt 5226 ‘cfv 6542 (class class class)co 7415 ℂcc 11134 ℝcr 11135 0cc0 11136 1c1 11137 + caddc 11139 < clt 11276 ≤ cle 11277 − cmin 11472 ℕcn 12240 ℤcz 12586 ...cfz 13514

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5294 ax-nul 5301 ax-pow 5359 ax-pr 5423 ax-un 7737 ax-cnex 11192 ax-resscn 11193 ax-1cn 11194 ax-icn 11195 ax-addcl 11196 ax-addrcl 11197 ax-mulcl 11198 ax-mulrcl 11199 ax-mulcom 11200 ax-addass 11201 ax-mulass 11202 ax-distr 11203 ax-i2m1 11204 ax-1ne0 11205 ax-1rid 11206 ax-rnegex 11207 ax-rrecex 11208 ax-cnre 11209 ax-pre-lttri 11210 ax-pre-lttrn 11211 ax-pre-ltadd 11212 ax-pre-mulgt0 11213

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3960 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5227 df-tr 5261 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7371 df-ov 7418 df-oprab 7419 df-mpo 7420 df-om 7868 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8388 df-rdg 8427 df-er 8721 df-en 8961 df-dom 8962 df-sdom 8963 df-pnf 11278 df-mnf 11279 df-xr 11280 df-ltxr 11281 df-le 11282 df-sub 11474 df-neg 11475 df-nn 12241 df-n0 12501 df-z 12587 df-uz 12851 df-rp 13005 df-fz 13515

This theorem is referenced by: metakunt31 41742

W3C validator